CODEWITHSUNDEEP
z3
Zeinab Ganjei
Zeinab Ganjei

Reputation: 133

Simplifying z3 expression using C++ API

I have such an expression

  z3::expr expr = (exists ((flag Bool))
               (exists ((w Int))
                 (exists ((i Int))
                  (exists ((counter Int))
                      (and (= i (+ x y z))
                           flag
                           (not (= i 0))
                           (= i counter)
                           (not (= w counter))
                           (>= i 1)
                           (= w 0)))))))

I use C++ API to do quantifier elimination and simplification.

z3::goal g(ctx);
g.add(expr);
z3::apply_result  result = (qe & simplify & propagate_ineqs)(g);

I have defined the tactics.

I want to get such result:

(or (>= (+ x y z) 1 )
     (<= (+ x y z) -1 ))

but I get this output which is appropriate for my application:

 (let ((a!1 (or (<= (+ (* (- 1) x)
                          (* (- 1) y)
                          (* (- 1) z))
                       (- 1))
                   (<= (+ x y z) (- 1)))))
      (and (or (<= (+ x y z) (- 1))
               (>= (+ x y z) 1))
           a!1
           (>= (+ x y z) 1)))

what tactics should I use to make it work as I want?

Upvotes: 1

Views: 568

Answers (1)

Zeinab Ganjei
Zeinab Ganjei

Reputation: 133

I solved the issue by setting these options in the context, before defining the goal:

ctx.set(":pp-min-alias-size", 1000000);
ctx.set(":pp-max-depth", 1000000);

it didn't simplify as I wanted, but removed the "let"s and that's better than nothing!

Upvotes: 2

Related Questions