c++ - 在 Z3 C++ 绑定中定义有趣的宏和正则表达式
问题描述
我正在编写一些代码,使用 Z3 字符串来评估 ACL 中的权限。到目前为止,对于 SMT2,这相对容易。例如。我想要实现的代码是:
(declare-const Group String)
(declare-const Resource String)
(define-fun acl1() Bool
(or (and
(= Group "employee")
(str.prefixof "shared/News_" Resource))
(and
(= Group "manager")
(or (str.prefixof "shared/Internal_" Resource)
(str.prefixof "shared/News_" Resource))
)))
(define-fun acl2() Bool
(and (and (str.prefixof "shared/" Resource)
(str.in.re Group re.allchar))
(not (and (str.prefixof "shared/Internal_" Resource)
(= Group "employee")))))
;; perm(acl1) <= perm(acl) iff acl1 => acl2
(define-fun conjecture() Bool
(=> (= acl1 true)
(= acl2 true)))
(assert (not conjecture))
(check-sat)
阅读 z3 c++ 绑定,我不知道如何将 z3::function 粘贴到此。到目前为止,假设 define-fun 只是一个 lisp 宏,我有这个。
#include <z3++.h>
z3::expr acl1(z3::context& c, z3::expr& G, z3::expr& R)
{
return (((G == c.string_val("employee")) &&
z3::prefixof(c.string_val("shared/News_"), R)) ||
((G == c.string_val("manager")) &&
(z3::prefixof(c.string_val("shared/Internal_"), R) ||
z3::prefixof(c.string_val("shared/News_"), R))));
}
z3::expr acl2(z3::context& c, z3::expr& G, z3::expr& R)
{
return ((z3::prefixof(c.string_val(""), G) &&
z3::prefixof(c.string_val("shared/"), R)) &&
!((G == c.string_val("employee")) &&
(z3::prefixof(c.string_val("shared/Internal"), R))));
}
z3::expr MakeStringFunction(z3::context* c, std::string s) {
z3::sort sort = c->string_sort();
z3::symbol name = c->str_symbol(s.c_str());
return c->constant(name, sort);
}
void acl_eval()
{
z3::context c;
auto Group = MakeStringFunction(&c, "Group");
auto Resource = MakeStringFunction(&c, "Resource");
auto acl1_f = acl1(c, Group, Resource);
auto acl2_f = acl2(c, Group, Resource);
auto conjecture = implies(acl1_f == c.bool_val(true),
acl2_f == c.bool_val(true));
z3::solver s(c);
s.add(!conjecture);
std::cout << s.to_smt2() << std::endl;
switch(s.check()){
case z3::unsat: std::cout<< "Valid Conjecture" << std::endl; break;
case z3::sat: std::cout << "Invalid Conjecture" << std::endl; break;
case z3::unknown: [[fallthrough]]
default:
std::cout << "Unknown" << std::endl;
}
}
int main(){
acl_eval();
return 0;
}
这是如何在 C++ 绑定中完成函数的吗?虽然由 C++ 绑定生成的 smt2 代码看起来并不完全像另一个代码,但我在一个带有 let 绑定的断言中看到了一个完整的 expr ,它可以满足我的需求。此外,我还想知道 C++ 绑定是否支持正则表达式函数,如 z3 公开的 SMT 库?我找不到任何示例,文档也不是很清楚。
解决方案
通常,当您使用 C++(或任何其他高级)API 时,不需要在 SMTLib 中创建“函数”。相反,您只需用这些语言编写函数,直接生成所需的代码。这听起来确实令人困惑,但它是预期的用例:SMTLib 函数被宿主语言中的函数替换。以宿主语言运行它们,然后以对象语言生成必要的语法树;即,Z3 的内部 AST 表示。特别是在您的情况下,您不需要将任何“参数”传递给这些函数,因此您根本不应该创建任何“参数”。所以,你在这里做的是正确的。
(旁注:在某些情况下,您确实想在 SMTLib 中输出函数。例如,如果您想使用未解释的函数。或者您可能想使用递归函数定义,而这在宿主语言中是无法真正做到的。但我们不要在这里混为一谈。如果你觉得你确实需要它们,请提出一个单独的问题。根据你的描述,我认为没有理由。)
关于正则表达式:它们都在 C++ API 中可用,请看这里:https ://z3prover.github.io/api/html/z3_09_09_8h_source.html#l03334
特别是,您正在寻找的功能是:
希望这会让你开始!
推荐阅读
- javascript - 无法向 Google Smart Display 发送推送通知
- reactjs - 使用用户输入获取 API 的问题
- xaml - 与 Prism 导航绑定
- python - 使用 Python 从目录创建 zip
- reactjs - 如何自动从数据库中删除未经验证的用户?
- r - 如何根据条件将列添加到数据框中?(没有 ifelse)
- three.js - 下画布上的绘图模式以及如何在上画布而不是下画布上呈现控件
- flutter - Flutter - GraphQL 支持
- wordpress - 主页网站可用,但子页面给出 404 错误
- dynamics-crm - 使用 CRM Dynamics WebApi 创建“Global-OptionSet”属性时出现问题