c-Z3_parse_smtlib_string使用问题

2019-10-09 13:20:07 阅读：188 来源： 互联网

标签：z3 c-3 c

在下面的代码中,我放置了一个显然无法令人满意的Z3声明,然后尝试使用C/C++ Z3 API来以编程方式解决该问题.

问题在于此代码始终触发输出检查的内容：“ SAT ?!”.即,显然无法满足的表达式在API调用的当前用法中被确定为可以满足.

我怎样才能使这种操作按预期进行？

#include "z3++.h"
int main(){
  z3::context c;

  std::string testing = "(declare-const p0 Bool)(assert(= p0 true))(assert(= p0 false))(check-sat)";

  Z3_ast parsed = Z3_parse_smtlib2_string(c,testing.c_str(),0,0,0,0,0,0);
  z3::expr e(c, parsed);

  z3::solver s(c);
  if(s.check() == z3::sat)
    std::cout << "SAT?!\n";
  return 0;
}

解决方法:

Z3在这种情况下是正确的,因为没有将任何约束添加到求解器,因此这是微不足道的.关键部分是：

Z3_ast parsed = Z3_parse_...
z3::expr e(c, parsed);

z3::solver s(c);
s.add(e); // <--- Add constraints to solver here
if(s.check() ...

标签：z3,c-3,c
来源： https://codeday.me/bug/20191009/1879390.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。

ICode9

c-Z3_parse_smtlib_string使用问题