z3
z3 copied to clipboard
Published
20 hours ago •
Z3Prover
Z3Prover
Instable Java API in comparison to commandline-tool
Hi, I attempted to run solver.check() using the Java API and (check-sat) in commandline-tool to compare the runtimes. I understand that the Java API may be slightly slower than commandline-tool, however the results I obtained do not seem so much expected. While with (check-sat) I found some stability as well being fast (given a flag is enabled as I explain below), with Java API I noticed instability (ranging from slow to extremely slow to timeout) and being much slower than (check-sat). Is this expected?
To benchmark both, I run the corresponding check function 10 times. Note that configured timeout is 20s, thus several attempts with Java API ended in timeout. To test with Java API I run:
Context context1 = new Context();
Solver solver1 = context1.mkSolver();
Params params = context1.mkParams();
params.add("candidate_models", true);
params.add("fail_if_inconclusive", false);
solver1.setParameters(params);
BoolExpr assertions = context1.parseSMTLIB2File("<path to file>.z3",null, null, null, null);
solver1.add(assertions);
for (int i = 0; i < 10; i++) {
long start = System.currentTimeMillis();
solver1.check();
long diff = System.currentTimeMillis() - start;
System.out.println(diff + "ms");
}
The measured times were:
- 10328ms
- 6590ms
- 20733ms
- 8091ms
- 20832ms
- 6793ms
- 20920ms
- 9347ms
- 20864ms
- 20869ms
With the commandline-tool I tried by two ways: with (set-option :produce-proofs true) and without (set-option :produce-proofs true). With (set-option :produce-proofs true) I got always a result after ~2.1-2.4s. Without (set-option :produce-proofs true) I got timeout every time.
So, my question is why the difference in runtime between solver.check() (including why there may be instability with it) and the commandline-tool with (set-option :produce-proofs true)? Besides that, why in the commandline-tool the line (set-option :produce-proofs true) produces such a radical difference?
The file I used was
(set-info :smt-lib-version 2.0)
(set-option :auto_config false)
(set-option :smt.mbqi false)
;(set-option :produce-proofs true)
(set-option :model_evaluator.completion false)
(set-option :model.v1 true)
(set-option :smt.phase_selection 0)
(set-option :smt.restart_strategy 0)
(set-option :smt.restart_factor 1.5)
(set-option :nnf.sk_hack true)
(set-option :smt.qi.eager_threshold 100.0)
(set-option :smt.arith.random_initial_value true)
(set-option :smt.case_split 3)
(set-option :smt.delay_units true)
(set-option :smt.delay_units_threshold 16)
(set-option :type_check true)
(set-option :smt.bv.reflect true)
(set-option :smt.timeout 20000)
(declare-datatypes () ((General (G_Boolean (of_G_Boolean Bool)) (G_Integer (of_G_Integer Int)) (G_String (of_G_String String)) (G_Null))))
(declare-sort SVMap)
(declare-sort IVMap)
(declare-datatypes () ((Value (G (out_G General)) (E (out_E SVMap)) (C (out_C IVMap)) (R (id Int) (type String) (identifiers Value)))))
(declare-datatypes () ((ValueOption (NoValue) (SomeValue (of_SomeValue Value)))))
(declare-fun r_resourceidof (Value Value) Value)
(declare-fun v_contains (Value Value) Value)
(declare-fun Good_R (Value) Bool)
(declare-fun In_String (Value) Bool)
(declare-fun v_nth (Value Value) Value)
(declare-fun v_integer (Int) Value)
(declare-fun v_length (Value) Value)
(declare-fun Good_C (Value) Bool)
(declare-fun r_representationof (Value Value) Value)
(declare-fun v_ff () Value)
(declare-fun v_tt () Value)
(declare-fun alphai (IVMap) (Array Int ValueOption))
(declare-fun In_Integer (Value) Bool)
(declare-fun betai ((Array Int ValueOption)) IVMap)
(declare-fun v_dot (String Value) Value)
(declare-fun alphas (SVMap) (Array String ValueOption))
(declare-fun v_has_field (String Value) Bool)
(declare-fun betas ((Array String ValueOption)) SVMap)
(declare-fun v_string (String) Value)
(declare-fun O_LE (Value Value) Value)
(declare-fun O_LT (Value Value) Value)
(declare-fun O_GT (Value Value) Value)
(declare-fun O_GE (Value Value) Value)
(declare-fun O_Or (Value Value) Value)
(declare-fun O_And (Value Value) Value)
(declare-fun O_Minus (Value) Value)
(declare-fun O_Not (Value) Value)
(declare-fun O_NE (Value Value) Value)
(declare-fun O_EQ (Value Value) Value)
(declare-fun O_Mult (Value Value) Value)
(declare-fun O_Sub (Value Value) Value)
(declare-fun O_Sum (Value Value) Value)
(declare-fun In_Boolean (Value) Bool)
(declare-fun v_boolean (Bool) Value)
(declare-fun v_null () Value)
(declare-fun Good_E (Value) Bool)
(declare-fun maze () Value)
(declare-fun root () Value)
(declare-fun request () Value)
(assert (let ((a!1 (forall ((b Bool))
(! (= (v_boolean b) (G (G_Boolean b))) :pattern ((v_boolean b)))))
(a!2 (forall ((i Int))
(! (= (v_integer i) (G (G_Integer i))) :pattern ((v_integer i)))))
(a!3 (forall ((s String))
(! (= (v_string s) (G (G_String s))) :pattern ((v_string s)))))
(a!4 (forall ((v Value))
(! (= (In_Boolean v) (and (is-G v) (is-G_Boolean (out_G v))))
:pattern ((In_Boolean v)))))
(a!5 (forall ((v Value))
(! (= (In_Integer v) (and (is-G v) (is-G_Integer (out_G v))))
:pattern ((In_Integer v)))))
(a!6 (forall ((v Value))
(! (= (In_String v) (and (is-G v) (is-G_String (out_G v))))
:pattern ((In_String v)))))
(a!7 (forall ((v1 Value) (v2 Value))
(! (= (O_EQ v1 v2) (ite (= v1 v2) v_tt v_ff))
:pattern ((O_EQ v1 v2)))))
(a!8 (forall ((v1 Value) (v2 Value))
(! (= (O_NE v1 v2) (ite (= v1 v2) v_ff v_tt))
:pattern ((O_NE v1 v2)))))
(a!9 (forall ((v Value))
(! (= (O_Not v) (ite (not (= v v_tt)) v_tt v_ff))
:pattern ((O_Not v)))))
(a!10 (forall ((v1 Value) (v2 Value))
(! (= (O_And v1 v2) (ite (and (= v1 v_tt) (= v2 v_tt)) v_tt v_ff))
:pattern ((O_And v1 v2)))))
(a!11 (forall ((v1 Value) (v2 Value))
(! (= (O_Or v1 v2) (ite (or (= v1 v_tt) (= v2 v_tt)) v_tt v_ff))
:pattern ((O_Or v1 v2)))))
(a!12 (forall ((v Value))
(! (let ((a!1 (= (str.len (of_G_String (out_G v)))
(of_G_Integer (out_G (v_length v))))))
(=> (and (is-G v) (is-G_String (out_G v))) a!1))
:pattern ((v_length v)))))
(a!13 (forall ((v1 Value) (v2 Value))
(! (let ((a!1 (ite (str.contains (of_G_String (out_G v1))
(of_G_String (out_G v2)))
v_tt
v_ff)))
(=> (and (is-G v1)
(is-G_String (out_G v1))
(is-G v2)
(is-G_String (out_G v2)))
(= (v_contains v1 v2) a!1)))
:pattern ((v_contains v1 v2)))))
(a!14 (forall ((v Value) (i Int))
(! (let ((a!1 (v_string (str.at (of_G_String (out_G v)) i))))
(=> (and (is-G v) (is-G_String (out_G v)))
(= (v_nth v (v_integer i)) a!1)))
:pattern ((v_nth v (v_integer i))))))
(a!15 (forall ((am (Array String ValueOption)))
(= (alphas (betas am)) am)))
(a!16 (forall ((svm SVMap)) (= (betas (alphas svm)) svm)))
(a!17 (forall ((l String) (svm SVMap))
(! (let ((a!1 (not (= (select (alphas svm) l) NoValue))))
(= (v_has_field l (E svm)) a!1))
:pattern ((v_has_field l (E svm))))))
(a!18 (forall ((l String) (svm SVMap))
(! (= (v_dot l (E svm)) (of_SomeValue (select (alphas svm) l)))
:pattern ((v_dot l (E svm))))))
(a!19 (forall ((am (Array Int ValueOption))) (= (alphai (betai am)) am)))
(a!20 (forall ((ivm IVMap)) (= (betai (alphai ivm)) ivm)))
(a!21 (forall ((v Value))
(! (let ((a!1 (>= (of_G_Integer (out_G (v_length v))) 0)))
(=> (Good_C v) (and (In_Integer (v_length v)) a!1)))
:pattern ((Good_C v)))))
(a!22 (forall ((v Value) (i Int))
(! (let ((a!1 (of_SomeValue (select (alphai (out_C v)) i))))
(=> (Good_C v) (= (v_nth v (v_integer i)) a!1)))
:pattern ((Good_C v) (v_nth v (v_integer i))))))
(a!23 (forall ((v1 Value) (v2 Value))
(! (let ((a!1 (exists ((i Int))
(let ((a!1 (< i
(of_G_Integer (out_G (v_length v1))))))
(and (<= 0 i)
a!1
(= (v_nth v1 (v_integer i)) v2))))))
(=> (and (is-C v1))
(= (v_contains v1 v2) (ite a!1 v_tt v_ff))))
:pattern ((v_contains v1 v2)))))
(a!24 (forall ((r1 Value) (r2 Value))
(! (= (= r1 r2) (= (id r1) (id r2)))
:pattern ((Good_R r1) (Good_R r2)))))
(a!25 (forall ((v Value) (r Value))
(! (=> (Good_R r) (=> (is-R v) (= (r_representationof v r) v_ff)))
:pattern ((Good_R r) (r_representationof v r)))))
(a!26 (forall ((r Value))
(! (let ((a!1 (forall ((i Int))
(let ((a!1 (of_G_Integer (out_G (v_length (identifiers r))))))
(=> (and (<= 0 i) (< i a!1))
(In_String (v_nth (identifiers r)
(v_integer i))))))))
(=> (Good_R r) (and (Good_C (identifiers r)) a!1)))
:pattern ((Good_R r)))))
(a!27 (forall ((id Value) (r Value))
(! (=> (and (In_String id) (Good_R r))
(= (r_resourceidof id r) (v_contains (identifiers r) id)))
:pattern ((r_resourceidof id r)))))
(a!28 (forall ((|\|\\\\\\\|#18\\\\\\\|\|| Int))
(let ((a!1 (< |\|\\\\\\\|#18\\\\\\\|\||
(of_G_Integer (out_G (v_length maze)))))
(a!2 (= (type (v_nth maze
(v_integer |\|\\\\\\\|#18\\\\\\\|\||)))
"Maze")))
(let ((a!3 (and (Good_R (v_nth maze
(v_integer |\|\\\\\\\|#18\\\\\\\|\||)))
a!2)))
(=> (and (<= 0 |\|\\\\\\\|#18\\\\\\\|\||) a!1) (or a!3 a!3 a!3))))))
(a!29 (= (type (v_nth maze (v_integer 0))) "Maze"))
(a!31 (= (type (v_nth maze (v_integer 1))) "Maze"))
(a!33 (= (type (v_nth maze (v_integer 2))) "Maze"))
(a!36 (forall ((|\|\\\\\\\|#19\\\\\\\|\|| Int))
(let ((a!1 (< |\|\\\\\\\|#19\\\\\\\|\||
(of_G_Integer (out_G (v_length request)))))
(a!2 (not (Good_R (v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))))
(a!3 (Good_R (v_dot "template"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))))
(a!4 (Good_E (v_dot "template"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))))
(a!5 (v_has_field "mazeId"
(v_dot "template"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))))
(a!6 (v_dot "mazeId"
(v_dot "template"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))))
(a!10 (Good_E (v_dot "header"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))))
(a!11 (In_String (v_dot "location"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))))
(a!12 (Good_R (v_dot "body"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||))))))
(let ((a!7 (v_boolean (and a!4 a!5 (not (Good_R a!6))))))
(let ((a!8 (O_And (O_And (v_boolean (and a!4))
(v_boolean (and a!4)))
(v_boolean (and (not a!3) (= a!7 v_tt))))))
(let ((a!9 (O_And (O_And a!8 (v_boolean (and a!4)))
(v_boolean (and a!4)))))
(let ((a!13 (and (Good_E (v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))
(v_has_field "template"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))
(not a!3)
(= a!9 v_tt)
(v_has_field "header"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))
a!10
(v_has_field "location"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))
a!11
(v_has_field "body"
(v_nth request
(v_integer |\|\\\\\\\|#19\\\\\\\|\||)))
(not a!12))))
(=> (and (<= 0 |\|\\\\\\\|#19\\\\\\\|\||) a!1)
(or a!2 a!13 a!2)))))))))
(a!37 (not (Good_R (v_nth request (v_integer 0)))))
(a!38 (Good_R (v_dot "template" (v_nth request (v_integer 1)))))
(a!39 (Good_E (v_dot "template" (v_nth request (v_integer 1)))))
(a!40 (v_has_field "mazeId"
(v_dot "template" (v_nth request (v_integer 1)))))
(a!41 (v_dot "mazeId" (v_dot "template" (v_nth request (v_integer 1)))))
(a!45 (Good_E (v_dot "header" (v_nth request (v_integer 1)))))
(a!46 (In_String (v_dot "location" (v_nth request (v_integer 1)))))
(a!47 (Good_R (v_dot "body" (v_nth request (v_integer 1)))))
(a!49 (not (Good_R (v_nth request (v_integer 2)))))
(a!51 (forall ((|\|\\\\\\\|#20\\\\\\\|\|| Int))
(let ((a!1 (< |\|\\\\\\\|#20\\\\\\\|\||
(of_G_Integer (out_G (v_length root)))))
(a!2 (not (Good_R (v_nth root
(v_integer |\|\\\\\\\|#20\\\\\\\|\||))))))
(let ((a!3 (or a!2
(In_String (v_nth root
(v_integer |\|\\\\\\\|#20\\\\\\\|\||)))
a!2)))
(=> (and (<= 0 |\|\\\\\\\|#20\\\\\\\|\||) a!1) a!3)))))
(a!52 (not (Good_R (v_nth root (v_integer 0)))))
(a!53 (v_boolean (In_String (v_nth root (v_integer 1)))))
(a!54 (not (Good_R (v_nth root (v_integer 2)))))
(a!56 (v_integer (id (v_nth maze (v_integer 1)))))
(a!57 (Good_E (v_dot "body" (v_nth request (v_integer 1)))))
(a!58 (v_has_field "name" (v_dot "body" (v_nth request (v_integer 1)))))
(a!59 (v_dot "name" (v_dot "body" (v_nth request (v_integer 1)))))
(a!60 (re.union (re.union (re.union (re.range "a" "z") (re.range "A" "Z"))
(re.range "0" "9"))
(re.union (re.range " " " ")
(re.union (re.range "\x09" "\x09")
(re.range "\n" "\n")))))
(a!66 (= (v_dot "location" (v_nth request (v_integer 0)))
(v_string "http://mazes-demo.herokuapp.com/rest/v1/mazes")))
(a!67 (v_has_field "name" (v_dot "body" (v_nth request (v_integer 0)))))
(a!68 (v_dot "name" (v_dot "body" (v_nth request (v_integer 0)))))
(a!69 (forall ((|\|\\\\\\\|#23\\\\\\\|\|| String))
(let ((a!1 (v_has_field |\|\\\\\\\|#23\\\\\\\|\||
(v_dot "body"
(v_nth request (v_integer 0))))))
(=> (not (= |\|\\\\\\\|#23\\\\\\\|\|| "name")) (not a!1)))))
(a!70 (forall ((|\|\\\\\\\|#24\\\\\\\|\|| String))
(let ((a!1 (not (v_has_field |\|\\\\\\\|#24\\\\\\\|\||
(v_nth request (v_integer 0))))))
(=> (and (not (= |\|\\\\\\\|#24\\\\\\\|\|| "template"))
(not (= |\|\\\\\\\|#24\\\\\\\|\|| "header"))
(not (= |\|\\\\\\\|#24\\\\\\\|\|| "location"))
(not (= |\|\\\\\\\|#24\\\\\\\|\|| "body")))
a!1)))))
(let ((a!30 (and (Good_R (v_nth maze (v_integer 0))) a!29))
(a!32 (and (Good_R (v_nth maze (v_integer 1))) a!31))
(a!34 (and (Good_R (v_nth maze (v_integer 2))) a!33))
(a!42 (v_boolean (and a!39 a!40 (not (Good_R a!41)))))
(a!55 (O_And (O_EQ (v_length root) (v_integer 3))
(O_And (O_And (v_boolean a!52) a!53) (v_boolean a!54))))
(a!61 (and (In_String a!59)
(str.in.re (of_G_String (out_G a!59)) ((_ re.loop 3 3) a!60)))))
(let ((a!35 (O_And (O_EQ (v_length maze) (v_integer 3))
(O_And (O_And (v_boolean a!30) (v_boolean a!32))
(v_boolean a!34))))
(a!43 (O_And (O_And (v_boolean (and a!39)) (v_boolean (and a!39)))
(v_boolean (and (not a!38) (= a!42 v_tt)))))
(a!62 (v_boolean (and a!57
a!58
(In_String a!59)
(= (ite a!61 v_tt v_ff) v_tt)))))
(let ((a!44 (O_And (O_And a!43 (v_boolean (and a!39))) (v_boolean (and a!39))))
(a!63 (O_And (O_And (v_boolean (In_Integer a!41)) a!62)
(O_EQ (v_integer 5997) a!41))))
(let ((a!48 (and (Good_E (v_nth request (v_integer 1)))
(v_has_field "template" (v_nth request (v_integer 1)))
(not a!38)
(= a!44 v_tt)
(v_has_field "header" (v_nth request (v_integer 1)))
a!45
(v_has_field "location" (v_nth request (v_integer 1)))
a!46
(v_has_field "body" (v_nth request (v_integer 1)))
(not a!47)))
(a!64 (O_Or (O_Not (O_EQ a!56 (v_integer 1))) a!63)))
(let ((a!50 (O_And (O_EQ (v_length request) (v_integer 3))
(O_And (O_And (v_boolean a!37) (v_boolean a!48))
(v_boolean a!49))))
(a!65 (= (O_And (O_EQ a!56 (v_integer 1)) a!64) v_tt)))
(and (forall ((v Value)) (! (= (Good_C v) (is-C v)) :pattern ((Good_C v))))
(forall ((v Value)) (! (= (Good_E v) (is-E v)) :pattern ((Good_E v))))
(forall ((v Value)) (! (= (Good_R v) (is-R v)) :pattern ((Good_R v))))
(= v_tt (G (G_Boolean true)))
(= v_ff (G (G_Boolean false)))
(= v_null (G G_Null))
a!1
a!2
a!3
a!4
a!5
a!6
(forall ((v1 Value) (v2 Value))
(! (let ((a!1 (v_integer (+ (of_G_Integer (out_G v1))
(of_G_Integer (out_G v2))))))
(= (O_Sum v1 v2) a!1))
:pattern ((O_Sum v1 v2))))
(forall ((v1 Value) (v2 Value))
(! (let ((a!1 (v_integer (- (of_G_Integer (out_G v1))
(of_G_Integer (out_G v2))))))
(= (O_Sub v1 v2) a!1))
:pattern ((O_Sub v1 v2))))
(forall ((v1 Value) (v2 Value))
(! (let ((a!1 (v_integer (* (of_G_Integer (out_G v1))
(of_G_Integer (out_G v2))))))
(= (O_Mult v1 v2) a!1))
:pattern ((O_Mult v1 v2))))
a!7
a!8
a!9
(forall ((v Value))
(! (let ((a!1 (v_integer (- (of_G_Integer (out_G v))))))
(= (O_Minus v) a!1))
:pattern ((O_Minus v))))
a!10
a!11
(forall ((v1 Value) (v2 Value))
(! (let ((a!1 (ite (>= (of_G_Integer (out_G v1))
(of_G_Integer (out_G v2)))
v_tt
v_ff)))
(= (O_GE v1 v2) a!1))
:pattern ((O_GE v1 v2))))
(forall ((v1 Value) (v2 Value))
(! (let ((a!1 (ite (> (of_G_Integer (out_G v1))
(of_G_Integer (out_G v2)))
v_tt
v_ff)))
(= (O_GT v1 v2) a!1))
:pattern ((O_GT v1 v2))))
(forall ((v1 Value) (v2 Value))
(! (let ((a!1 (ite (< (of_G_Integer (out_G v1))
(of_G_Integer (out_G v2)))
v_tt
v_ff)))
(= (O_LT v1 v2) a!1))
:pattern ((O_LT v1 v2))))
(forall ((v1 Value) (v2 Value))
(! (let ((a!1 (ite (<= (of_G_Integer (out_G v1))
(of_G_Integer (out_G v2)))
v_tt
v_ff)))
(= (O_LE v1 v2) a!1))
:pattern ((O_LE v1 v2))))
a!12
a!13
a!14
a!15
a!16
(forall ((svm (Array String ValueOption))) (= (default svm) NoValue))
a!17
a!18
a!19
a!20
(forall ((ivm (Array Int ValueOption))) (= (default ivm) NoValue))
a!21
(forall ((v Value))
(! (let ((a!1 (forall ((i Int))
(let ((a!1 (< i (of_G_Integer (out_G (v_length v)))))
(a!2 (is-SomeValue (select (alphai (out_C v)) i))))
(=> (and (<= 0 i) a!1) a!2)))))
(= (Good_C v) a!1))
:pattern ((Good_C v))))
a!22
a!23
a!24
a!25
a!26
a!27
(Good_C maze)
a!28
(= a!35 v_tt)
(Good_C request)
a!36
(= a!50 v_tt)
(Good_C root)
a!51
(= a!55 v_tt)
a!65
(Good_C request)
(= (v_length request) (v_integer 3))
(v_has_field "template" (v_nth request (v_integer 0)))
(forall ((|\|\\\\\\\|#21\\\\\\\|\|| String))
(let ((a!1 (v_has_field |\|\\\\\\\|#21\\\\\\\|\||
(v_dot "template"
(v_nth request (v_integer 0))))))
(=> true (not a!1))))
(v_has_field "header" (v_nth request (v_integer 0)))
(forall ((|\|\\\\\\\|#22\\\\\\\|\|| String))
(let ((a!1 (v_has_field |\|\\\\\\\|#22\\\\\\\|\||
(v_dot "header" (v_nth request (v_integer 0))))))
(=> true (not a!1))))
(v_has_field "location" (v_nth request (v_integer 0)))
a!66
(v_has_field "body" (v_nth request (v_integer 0)))
a!67
(= a!68 (v_string "p "))
a!69
a!70
true
true
(Good_C root)
(= (v_length root) (v_integer 3))
(= (v_nth root (v_integer 0)) (v_string ""))
true
true
(Good_C maze)
(= (v_length maze) (v_integer 3))
true
true
true))))))))
;(check-sat)
;(get-info :reason-unknown)
;(get-model)
Thanks
I haven't been able to reproduce this so far. I am using the following script:
from z3 import *
s = Solver()
set_option(verbose=1)
s.set(candidate_models=True)
s.set(fail_if_inconclusive=False)
fmls = parse_smt2_file("slow.smt2")
s.add(fmls)
#s.set("smt.random_seed",11)
print s.check()
print s.statistics()
# print s.model()
The results under random seeds seems stable enough. It finishes within the same time as the command-line. The behavior from Java should be the same (they call into the same underlying functions).
I tried a different example with the command-line as well with python and java, and it seems the random seed has a radical effect on it.
In Java, I ran:
import com.microsoft.z3.*;
import java.util.*;
class Z3Attempt {
public static void main(String[] args) {
Context context1 = new Context();
for (int i = 0; i < 10; i++) {
BoolExpr assertions =
context1.parseSMTLIB2File("./exp.smt2", null, null, null, null);
Solver solver1 = context1.mkSolver();
Params params = context1.mkParams();
params.add("candidate_models", true);
params.add("fail_if_inconclusive", false);
params.add("smt.random_seed", 11);
solver1.setParameters(params);
solver1.add(assertions);
long start = System.currentTimeMillis();
System.out.println(solver1.check());
long diff = System.currentTimeMillis() - start;
//System.out.println(solver1.getModel());
System.out.println(diff + "ms");
}
}
}
This measured the following times:
UNKNOWN
643ms
UNKNOWN
21837ms
UNKNOWN
21076ms
UNKNOWN
22159ms
UNKNOWN
21795ms
UNKNOWN
20571ms
UNKNOWN
21603ms
UNKNOWN
21919ms
UNKNOWN
21250ms
UNKNOWN
21106ms
Basically, only the first check() was successful (the others timed out). If I removed the line that is setting the random seed then every check() times out, so the random seed seems to affect here. Besides that, with the random seed set (to 11), if I moved the line initializing context1 to inside the for loop (just before the line parsing the file) then it takes always ~650ms (no exception). So, with this I have two questions:
- Should the random seed make such a difference?
- Is it expected that we have to create a new context whenever we need to check() with a given random seed?
In python, I ran:
from z3 import *
s = Solver()
set_option(verbose=1)
s.set(candidate_models=True)
s.set(fail_if_inconclusive=False)
fmls = parse_smt2_file("exp.smt2")
s.add(fmls)
s.set("smt.random_seed", 11)
print s.check()
print s.statistics()
#print s.model()
print ""
print s.check()
print s.statistics()
#print s.model()
And this had the same effect of Java, the first check() produced a response quickly (less than 1s) and the second check() timed out. Also, this outputted the following:
(smt.giveup quantifiers)
unknown
(:added-eqs 19837
:arith-add-rows 1841
:arith-assert-lower 396
:arith-assert-upper 396
:arith-bound-prop 7
:arith-conflicts 2
:arith-eq-adapter 357
:arith-fixed-eqs 516
:arith-offset-eqs 187
:arith-pivots 560
:array-ext-ax 40
:array-splits 20
:binary-propagations 446
:bv-bit2core 974
:bv-conflicts 53
:bv-dynamic-diseqs 939
:bv-dynamic-eqs 1609
:bv->core-eq 1609
:conflicts 99
:datatype-accessor-ax 514
:datatype-constructor-ax 506
:datatype-occurs-check 63918
:datatype-splits 603
:decisions 12545
:del-clause 1906
:final-checks 977
:interface-eqs 129
:max-generation 3
:max-memory 13.23
:memory 4.05
:minimized-lits 57
:mk-bool-var 31098
:mk-clause 2920
:num-allocs 1093919121
:propagations 2172
:quant-instantiations 315
:rlimit-count 256338
:seq-add-axiom 6995
:seq-extensionality 862
:seq-fixed-length 17
:seq-length-coherence 41
:seq-num-reductions 1940
:seq-unfold-def 3)
(smt.restarting :propagations 1706 :decisions 1880 :conflicts 101 :restart 300 :agility 0.0222865)
(smt.restarting :propagations 3367 :decisions 6342 :conflicts 402 :restart 900 :agility 0.026705)
(smt.restarting :propagations 28084 :decisions 98413 :conflicts 1303 :restart 2700 :agility 0.0208057)
unknown
(:added-eqs 1371594
:arith-add-rows 853997
:arith-assert-diseq 63695
:arith-assert-lower 128060
:arith-assert-upper 111017
:arith-bound-prop 46500
:arith-conflicts 771
:arith-eq-adapter 12066
:arith-fixed-eqs 186314
:arith-offset-eqs 180923
:arith-pivots 4091
:array-ext-ax 2124
:array-splits 2068
:binary-propagations 168671
:bv-bit2core 1996
:bv-conflicts 106
:bv-dynamic-diseqs 1817
:bv-dynamic-eqs 166313
:bv->core-eq 166313
:conflicts 1983
:datatype-accessor-ax 17609
:datatype-constructor-ax 15460
:datatype-occurs-check 258467
:datatype-splits 22257
:decisions 1488032
:del-clause 36302
:final-checks 5382
:interface-eqs 726
:max-generation 6
:max-memory 60.54
:memory 5.85
:minimized-lits 86323
:mk-bool-var 1619263
:mk-clause 42207
:num-allocs 11258601299.00
:propagations 467836
:quant-instantiations 11809
:restarts 3
:rlimit-count 420297591
:seq-add-axiom 21271
:seq-extensionality 1672
:seq-fixed-length 486
:seq-length-coherence 1581
:seq-num-reductions 355522
:seq-unfold-def 5)
Talking about the command-line now, I used the Z3 executable and uncommented the line (set-option :produce-proofs true) of the file (setting the parameter to solver "proof" as true in both python/java made no difference). It produced a response in ~1s and the statistics printed were:
(:added-eqs 39374
:arith-add-rows 1569
:arith-assert-diseq 474
:arith-assert-lower 1216
:arith-assert-upper 2056
:arith-bound-prop 49
:arith-conflicts 11
:arith-eq-adapter 1307
:arith-fixed-eqs 1518
:arith-offset-eqs 736
:arith-pivots 315
:array-ext-ax 380
:array-splits 304
:bv-bit2core 1247
:bv-conflicts 57
:bv-dynamic-diseqs 1089
:bv-dynamic-eqs 3379
:bv->core-eq 3379
:conflicts 191
:datatype-accessor-ax 1526
:datatype-constructor-ax 2212
:datatype-occurs-check 84480
:datatype-splits 2415
:decisions 30312
:del-clause 2879
:final-checks 1438
:interface-eqs 130
:max-generation 3
:max-memory 33.89
:memory 26.30
:minimized-lits 194
:mk-bool-var 60775
:mk-clause 4488
:num-allocs 1157623350
:num-checks 1
:propagations 11671
:quant-instantiations 743
:restarts 1
:rlimit-count 450838
:seq-add-axiom 8030
:seq-extensionality 1020
:seq-fixed-length 78
:seq-length-coherence 82
:seq-num-reductions 4930
:seq-unfold-def 3
:time 1.06)
One difference I noticed from these statistics to the ones obtained with python/java is the "binary-propagations", the Z3 executable didn't print that line (I suppose it had value 0?)...
Without setting a random seed to the Z3 executable it responds quickly (and with a candidate model) while python/java need a random seed... Is this expected?
I have a similar problem. For the following SMT input:
(set-option :smt.auto-config false)
(set-option :smt.mbqi true)
(set-option :sat.random_seed 488)
(set-option :smt.random_seed 599)
(set-option :nlsat.seed 611)
(set-option :memory_max_size 6000)
(set-option :produce-proofs true)
(declare-sort T@U 0)
(declare-sort T@T 0)
(declare-fun Ctor (T@T) Int)
(declare-const intType T@T)
(declare-const boolType T@T)
(declare-fun type (T@U) T@T)
(declare-const RefType T@T)
(declare-fun int_2_U (Int) T@U)
(declare-fun bool_2_U (Bool) T@U)
(declare-fun U_2_int (T@U) Int)
(declare-fun MapType1Type (T@T T@T) T@T)
(declare-fun MapType1TypeInv1 (T@T) T@T)
(declare-fun MapType1Select (T@U T@U T@U) T@U)
(declare-fun MapType1Store (T@U T@U T@U T@U) T@U)
(assert (= (Ctor intType) 1))
(assert (= (Ctor boolType) 2))
(assert (forall ((kt0 T@T) (vt0 T@T) ) (! (= (MapType1TypeInv1 (MapType1Type kt0 vt0)) vt0) :pattern ( (MapType1Type kt0 vt0)))))
(assert (forall ((m1 T@U) (k1 T@U) (v1 T@U) ) (! (let ((aVar1 (MapType1TypeInv1 (type m1)))) (= (type (MapType1Select m1 k1 v1)) aVar1)) :pattern ( (MapType1Select m1 k1 v1)))))
(assert (forall ((m2 T@U) (k2 T@U) (x2 T@U) (v2 T@U) ) (! (let ((aVar1@@0 (type v2))) (let ((aVar0@@0 (type k2))) (= (type (MapType1Store m2 k2 x2 v2)) (MapType1Type aVar0@@0 aVar1@@0)))) :pattern ( (MapType1Store m2 k2 x2 v2)))))
(assert (forall ((v3 T@U) (m3 T@U) (k3 T@U) (x3 T@U) (other_k3 T@U) (other_v3 T@U) ) (! (or (= k3 other_k3) (= (MapType1Select (MapType1Store m3 k3 x3 v3) other_k3 other_v3) (MapType1Select m3 other_k3 other_v3))) :pattern ( (MapType1Select (MapType1Store m3 k3 x3 v3) other_k3 other_v3)))))
(assert (forall ((arg4 Int) ) (! (= (type (int_2_U arg4)) intType) :pattern ( (int_2_U arg4)))))
(assert (forall ((arg5 Bool) ) (! (= (type (bool_2_U arg5)) boolType) :pattern ( (bool_2_U arg5)))))
(assert (forall ((arg6 Int) ) (! (= (U_2_int (int_2_U arg6)) arg6) :pattern ( (int_2_U arg6)))))
(check-sat-using smt)
(get-proof)
if I run Z3 from command line, I obtain unsat and a proof immediately. However, with the Java API, the solver times out:
Map<String, String> context_settings = new HashMap<String, String>() {{
put("auto_config", "false");
put("proof", "true");
put("model", "false");
}};
context = new Context(context_settings);
Tactic tactic = context.andThen(context.mkTactic("solve-eqs"), context.mkTactic("simplify"),
context.mkTactic("normalize-bounds"), context.mkTactic("propagate-values"), context.mkTactic("smt"));
Solver solver = context.mkSolver(tactic);
Params solver_settings = context.mkParams();
solver_settings.add("auto-config", false);
solver_settings.add("mbqi", true);
solver_settings.add("ematching", false);
solver_settings.add("proof", true);
solver_settings.add("timeout", 600000);
solver_settings.add("max_memory", 6000);
solver_settings.add("smt.random_seed", 599));
solver.setParameters(solver_settings);
solver.add(context.parseSMTLIB2File("input.smt2", null, null, null, null));
Status status = solver.check(); // unknown due to timeout
Is there a way in which I could use the Java API to obtain similar performance with the command line? Thank you very much.
Loading files with parseSMTLIB2File (and similar in the other APIs) is not the same as running the solver on the command-line. IIRC, for example, set-option in the input file is completely ignored when loaded with parseSMTLIB2File. @alebugariu: you set ematching to false in the Java API settings, but not in the .smt2 file. This will obviously have a huge impact on performance.
