Can anyone help me how to get the total number of variables and clauses generated by Z3py?

[Ipsitakoley]

[Ipsitakoley]

Can anyone explain this?
(:max-memory 6.48
:memory 6.48
:mk-bool-var 1
:num-allocs 1102926
:total-time 0.05)
This is what I get when I run "z3 filename.smt -smt2 -st"

[NikolajBjorner]

In your case it didn't generate much. It created the Boolean variable for "true".

[Ipsitakoley]

We ran this following smt code

(declare-fun t11 () Int)
(declare-fun t12 () Int)
(declare-fun t21 () Int)
(declare-fun t22 () Int)
(declare-fun t31 () Int)
(declare-fun t32 () Int)
(assert (and (>= t11 0) (>= t12 (+ t11 2)) (<= (+ t12 1) 8)))
(assert (and (>= t21 0) (>= t22 (+ t21 3)) (<= (+ t22 1) 8)))
(assert (and (>= t31 0) (>= t32 (+ t31 2)) (<= (+ t32 3) 8)))
(assert (or (>= t11 (+ t21 3)) (>= t21 (+ t11 2))))
(assert (or (>= t11 (+ t31 2)) (>= t31 (+ t11 2))))
(assert (or (>= t21 (+ t31 2)) (>= t31 (+ t21 3))))
(assert (or (>= t12 (+ t22 1)) (>= t22 (+ t12 1))))
(assert (or (>= t12 (+ t32 3)) (>= t32 (+ t12 1))))
(assert (or (>= t22 (+ t32 3)) (>= t32 (+ t22 1))))
(check-sat)

and we got the following output while running with the command "z3 filename.smt2 -st"

sat
(:arith-add-rows      20
 :arith-assert-lower  15
 :arith-assert-upper  6
 :arith-pivots        10
 :binary-propagations 6
 :decisions           6
 :final-checks        1
 :max-memory          3.21
 :memory              2.83
 :mk-bool-var         27
 :num-allocs          1034760
 :num-checks          1
 :propagations        6
 :rlimit-count        1742
 :time                0.05
 :total-time          0.02)

will this be helpful to understand the number of variables or clauses? Is there any description of the above output variables?

[NikolajBjorner]

• there is no further description for statistics. The self-explanatory don't require code reviews, some others are best understood by looking at the source code.
• statistics don't include clause count. This is not a design constraint, simply we don't maintain any counter for when the solver creates new clauses. It is possible to add, but there is an alternative way to get information: you can run z3 with -v:10 (verbose mode) and it prints some information about active clauses.