1

Let say that I have some formulas that can be sat but I want to get the smaller (or larger) possible value so sat that formula.

Is there a way to tell the SMT solver to give that kind of small solution?

Example:

a+1>10

In that example I want the SMT solver to give me the solution 10 instead of 100.

Cheers

NOTE: I have just seen a similar question answered by one of the z3 authors saying, three years ago, that they were implementing that functionality in z3. Do you know if it is already implemented?

Community
  • 1
  • 1
user1618465
  • 1,813
  • 2
  • 32
  • 58

1 Answers1

1

It can be done using maximize and minimize More info

(declare-const x Int)
(assert (> (+ x 1) 10))
(minimize x)
(check-sat)
(get-model)
user1618465
  • 1,813
  • 2
  • 32
  • 58