CODEWITHSUNDEEP
z3solver
Anna K.
Anna K.

Reputation: 205

Z3 solver - Unsatisfiable model values

Z3 can output the model and we can extract the values when the input is satisfiable.

Is there a way to obtain values for our model when we want unsatisfiability? (note: I'm using the c++ API)

Another way to see this question: when z3 proves that the equations return false, can we print a combination that lead to that unsat (false) value?

Upvotes: 0

Views: 360

Answers (2)

Heisenbug
Heisenbug

Reputation: 464

/* Comment the below line while solving for Unsatisfiable */            
solver.add(constr);

/* This block gets us Unsatisfiable Constraints, Uncomment the below line */
/*
  * BoolExpr negConstr = ctx.mkNot(constr); solver.add(negConstr);
*/

So what we are effectively doing is negating the constraint for which we were solving and this will produce us UN-satisfiable contraint values while extracting from Model values as shown below:

Status checkResult = solver.check();
if (checkResult == Status.SATISFIABLE) {
  System.out.println("Satisfiable");
                
  // Get the model for the constraints
  Model model = solver.getModel();
                
  // Extract the values for the string variables
  System.out.println("s = " + model.eval(xExpr, false));
  System.out.println("t = " + model.eval(yExpr, false));
}

Upvotes: 0

alias
alias

Reputation: 30428

If your input is unsat, no assignment to inputs will make it true, i.e., all assignments will lead to false. So, you can just pick arbitrary values for your inputs.

From a practical perspective, however, one easy way to achieve what you want is to assert the negation of your original goal and ask for a model of that from the solver. The model that "satisfies" the negation of your goal will make your original goal "false."

Upvotes: 2

Related Questions