CODEWITHSUNDEEP
z3
Dingbao Xie
Dingbao Xie

Reputation: 736

How to get the model value in SAT problems using c++ api?

I am using c++ api of z3 to solve a sat problem. When the problem is sat, I want to get the satisfiable assignments of all the variables. I find it easy to print the value of a variable as the following code shows:

context c;
solver s(c);
expr x=c.bool_const("x");
s.add(x);
if(s.check()==sat){
     model m=s.get_model();
      std::cout<<"x:"<<m.eval(x);
}

But the question is that I need to use it in a 'if' condition statement. for example:

if(m.eval(x)==true)
     std::cout<<"x is true";

Does anybody know how to do that? Thanks in advance.

Upvotes: 0

Views: 578

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

There is a function "eq" that can be used to check structural equality between two terms. THe overloaded == creates a new term, but eq(m.eval(e),c.bool_val(true)) checks for structural equality.

Upvotes: 2

Related Questions