diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-29 11:11:05 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-29 16:11:05 +0000 |
commit | b685ed411b6814f0810ce8f61d07aa49bd75ea3b (patch) | |
tree | 75029fdd0b7b8d82f6296047c10818cb745c9cdb /test | |
parent | f2672e53fae29abe40fc69b004d1df5be0ce1e8b (diff) |
Integrate central equality engine approach into theory engine, add option and regressions (#6943)
This commit makes TheoryEngine take into account whether theories are using the central equality engine.
With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 11 | ||||
-rw-r--r-- | test/regress/regress0/aufbv/cee-small-shared-eq.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/sets/sets-deq-dd.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress1/cee-bug0909-dd-scope.smt2 | 23 | ||||
-rw-r--r-- | test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress1/push-pop/cee-prs-small.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/cee-npnt-dd.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/cee-os-delta.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress1/strings/cee-norn-aes-trivially.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 | 43 | ||||
-rw-r--r-- | test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 | 41 |
12 files changed, 202 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 151e01088..902037088 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -120,6 +120,7 @@ set(regress_0_tests regress0/aufbv/bug493.smtv1.smt2 regress0/aufbv/bug509.smtv1.smt2 regress0/aufbv/bug580.delta.smt2 + regress0/aufbv/cee-small-shared-eq.smt2 regress0/aufbv/diseqprop.01.smtv1.smt2 regress0/aufbv/dubreva005ue.delta01.smtv1.smt2 regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2 @@ -468,6 +469,7 @@ set(regress_0_tests regress0/datatypes/bug597-rbt.smt2 regress0/datatypes/bug604.smt2 regress0/datatypes/bug625.smt2 + regress0/datatypes/canExp-dtPendingMerge.smt2 regress0/datatypes/cdt-model-cade15.smt2 regress0/datatypes/cdt-non-canon-stream.smt2 regress0/datatypes/coda_simp_model.smt2 @@ -1084,6 +1086,7 @@ set(regress_0_tests regress0/sets/pre-proc-univ.smt2 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 regress0/sets/setel-eq.smt2 + regress0/sets/sets-deq-dd.smt2 regress0/sets/sets-equal.smt2 regress0/sets/sets-extr.smt2 regress0/sets/sets-inter.smt2 @@ -1542,10 +1545,12 @@ set(regress_1_tests regress1/bv/test-bv-abstraction.smt2 regress1/bv/unsound1.smt2 regress1/bvdiv2.smt2 + regress1/cee-bug0909-dd-scope.smt2 regress1/constarr3.cvc regress1/constarr3.smt2 regress1/cores/issue5604.smt2 regress1/datatypes/acyclicity-sr-ground096.smt2 + regress1/datatypes/cee-prs-small-dd2.smt2 regress1/datatypes/dt-color-2.6.smt2 regress1/datatypes/dt-param-card4-unsat.smt2 regress1/datatypes/error.cvc @@ -1734,6 +1739,7 @@ set(regress_1_tests regress1/push-pop/arith_lra_02.smt2 regress1/push-pop/bug-fmf-fun-skolem.smt2 regress1/push-pop/bug216.smt2 + regress1/push-pop/cee-prs-small.smt2 regress1/push-pop/fuzz_1.smt2 regress1/push-pop/fuzz_10.smt2 regress1/push-pop/fuzz_11.smt2 @@ -1813,6 +1819,8 @@ set(regress_1_tests regress1/quantifiers/burns13.smt2 regress1/quantifiers/burns4.smt2 regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 + regress1/quantifiers/cee-npnt-dd.smt2 + regress1/quantifiers/cee-os-delta.smt2 regress1/quantifiers/cdt-0208-to.smt2 regress1/quantifiers/const.cvc regress1/quantifiers/constfunc.cvc @@ -2088,6 +2096,7 @@ set(regress_1_tests regress1/strings/bug686dd.smt2 regress1/strings/bug768.smt2 regress1/strings/bug799-min.smt2 + regress1/strings/cee-norn-aes-trivially.smt2 regress1/strings/chapman150408.smt2 regress1/strings/cmu-2db2-extf-reg.smt2 regress1/strings/cmu-5042-0707-2.smt2 @@ -2482,6 +2491,7 @@ set(regress_2_tests regress2/piVC_5581bd.smt2 regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 + regress2/quantifiers/cee-event-wrong-sat.smt2 regress2/quantifiers/gn-wrong-091018.smt2 regress2/quantifiers/issue3481-unsat1.smt2 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 @@ -2722,6 +2732,7 @@ set(regression_disabled_tests # previously sygus inference did not apply, now (correctly) times out regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 + regress2/quantifiers/exp-trivially-dd3.smt2 regress2/nl/dumortier-050317.smt2 # timeout on some builds after changes to justification heuristic regress2/nl/nt-lemmas-bad.smt2 diff --git a/test/regress/regress0/aufbv/cee-small-shared-eq.smt2 b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2 new file mode 100644 index 000000000..fa91fe7de --- /dev/null +++ b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun a () (Array (_ BitVec 1) (_ BitVec 16))) +(assert (not (= (_ bv0 16) (select a ((_ extract 14 14) (select a (_ bv0 1))))))) +(check-sat) diff --git a/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 new file mode 100644 index 000000000..d81c3723d --- /dev/null +++ b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((T 0)) (((A) (B (proj0B T) (proj1B T)) (C (proj0C T)) (D (proj0D T) )))) +(declare-fun w () T) +(declare-fun u () T) +(assert (= w (B (D u) (B (D u) (C w))))) +(check-sat) diff --git a/test/regress/regress0/sets/sets-deq-dd.smt2 b/test/regress/regress0/sets/sets-deq-dd.smt2 new file mode 100644 index 000000000..17ca1fce2 --- /dev/null +++ b/test/regress/regress0/sets/sets-deq-dd.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun S () (Set (_ BitVec 1))) +(assert (not (= S (as emptyset (Set (_ BitVec 1)))))) +(check-sat) diff --git a/test/regress/regress1/cee-bug0909-dd-scope.smt2 b/test/regress/regress1/cee-bug0909-dd-scope.smt2 new file mode 100644 index 000000000..6ce621a98 --- /dev/null +++ b/test/regress/regress1/cee-bug0909-dd-scope.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((x5 0)) (((x3) (x4)))) +(declare-sort x 0) +(declare-sort x1 0) +(declare-datatypes ((x22 0)) (((x2)))) +(declare-datatypes ((x2 0)) (((x2 (x2 x5) (x24 x5) (x25 Int) (x26 Int) (x27 Int))))) +(declare-sort x30 0) +(declare-sort x3 0) +(declare-datatypes ((x4 0)) (((x44 (x43 x3))))) +(declare-fun x46 (x3) x1) +(declare-datatypes ((x54 0)) (((x49 (x48 x22)) (x5 (x5 x2)) (d (s x1))))) +(declare-fun x5 (x22) x2) +(declare-fun x67 () (Array x x54)) +(declare-fun x6 () (Array x x54)) +(declare-fun x7 () (Array x30 x4)) +(declare-fun x63 () x30) +(declare-fun x () x) +(assert (distinct x3 (ite (or (distinct x6 (store x67 x (d (x46 (x43 (select x7 x63)))))) (= x67 (store x67 x (x5 (x2 x4 x3 (x25 (x5 (x48 (select x67 x)))) (x26 (x5 (x48 (select x67 x)))) (x27 (x5 (x48 (select x6 x))))))))) x3 x4))) +(check-sat) diff --git a/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 b/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 new file mode 100644 index 000000000..fe422d9e4 --- /dev/null +++ b/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((r 0)) (((R (x Int))))) +(declare-datatype t ((M (t1 (Array Int Int)) (t2 (Array Int Int))))) +(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y t))))) +(declare-fun z () q) +(assert (= z (R ((as const (Array Int r)) (R 0)) (M ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0))))) +(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1))) +(check-sat) diff --git a/test/regress/regress1/push-pop/cee-prs-small.smt2 b/test/regress/regress1/push-pop/cee-prs-small.smt2 new file mode 100644 index 000000000..4c0b06764 --- /dev/null +++ b/test/regress/regress1/push-pop/cee-prs-small.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: -i --ee-mode=distributed +; COMMAND-LINE: -i --ee-mode=central +; EXPECT: sat +; EXPECT: unsat +(set-logic ALL) +(declare-datatypes ((r 0)) (((r_ctor (x Int))))) +(declare-datatype tup ((mkt (t1 (Array Int Int)) (t2 (Array Int Int))))) +(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y tup))))) +(declare-fun z () q) +(assert (not (= 1 (select (t2 (y z)) 1)))) +(assert (= z (R ((as const (Array Int r)) (r_ctor 0)) (mkt ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0))))) +(check-sat) +(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/regress1/quantifiers/cee-npnt-dd.smt2 new file mode 100644 index 000000000..15727589d --- /dev/null +++ b/test/regress/regress1/quantifiers/cee-npnt-dd.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(set-option :fmf-bound true) +(declare-datatype N ((o) (f) (s))) +(declare-datatype P ((P))) +(declare-fun G (N P Int) Bool) +(declare-datatype c ((c (_p P)))) +(declare-fun g (N Int Int) c) +(assert (forall ((x N)) (not (G x P 0)))) +(assert (forall ((t Int)) (or (< t 0) (> t 1) (and (forall ((p P)) (or (exists ((y N)) (and (G y (_p (g y 0 0)) t))))))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/cee-os-delta.smt2 b/test/regress/regress1/quantifiers/cee-os-delta.smt2 new file mode 100644 index 000000000..803291aa3 --- /dev/null +++ b/test/regress/regress1/quantifiers/cee-os-delta.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed +; COMMAND-LINE: --full-saturate-quant --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(declare-fun o (Int) Int) +(declare-fun f (Int Int) Int) +(assert (forall ((x Int)) (forall ((y Int)) (! (= 1 (* y (div y y))) :pattern ((f x y)))))) +(assert (= 0 (f (o 0) (o 1)))) +(check-sat) diff --git a/test/regress/regress1/strings/cee-norn-aes-trivially.smt2 b/test/regress/regress1/strings/cee-norn-aes-trivially.smt2 new file mode 100644 index 000000000..2f8d9904d --- /dev/null +++ b/test/regress/regress1/strings/cee-norn-aes-trivially.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --arith-eq-solver --ee-mode=distributed +; COMMAND-LINE: --arith-eq-solver --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(declare-fun v () String) +(assert (str.in_re (str.++ "" v) (re.* (str.to_re "z")))) +(assert (str.in_re v (re.* (re.range "a" "u")))) +(assert (not (str.in_re v (str.to_re "")))) +(check-sat) diff --git a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 new file mode 100644 index 000000000..c0b3aac7c --- /dev/null +++ b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 @@ -0,0 +1,43 @@ +; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed +; COMMAND-LINE: --full-saturate-quant --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((T@$TypeValue 0) (T@A 0)) (((A)) ((T)))) +(declare-datatypes ((T@$Location 0)) (((P) (G (|t# | T@$TypeValue) (|a#G| Int))))) +(declare-sort |T@[Int]$Value| 0) +(declare-datatypes ((T@$Value 0) (T@R 0)) (((E) ($Boolean (|b#$Boolean| Bool)) (I (|i#I| Int)) (D (|a#D| Int)) (V (|v#V| T@R))) ((R (|v#R| |T@[Int]$Value|) (|l#R| Int))))) +(declare-sort b 0) +(declare-sort l 0) +(declare-datatypes ((T@M 0)) (((M (|domain#M| b) (|contents#M| l))))) +(declare-fun $EmptyValueArray () T@R) +(declare-fun m (T@$Value) |T@[Int]$Value|) +(declare-fun $IsEqual_stratified (T@$Value T@$Value) Bool) +(declare-fun sel (|T@[Int]$Value| Int) T@$Value) +(declare-fun st (|T@[Int]$Value| Int T@$Value) |T@[Int]$Value|) +(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?x2 T@$Value)) (= ?x2 (sel (st ?x0 ?x1 ?x2) ?x1)))) +(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?y1 Int) (?x2 T@$Value)) (= (sel ?x0 ?y1) (sel (st ?x0 ?x1 ?x2) ?y1)))) +(declare-fun $LibraAccount_T_type_value () T@$TypeValue) +(declare-fun s (l T@$Location) T@$Value) +(declare-fun $Event_EventHandleGenerator_counter () Int) +(declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue) +(assert (= 0 (|l#R| $EmptyValueArray))) +(assert (forall ((v1 T@$Value) (v2 T@$Value)) (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (forall ((i Int)) (or (> 0 i) (>= i (|l#R| (|v#V| v1))) ($IsEqual_stratified (sel (|v#R| (|v#V| v1)) i) (sel (|v#R| (|v#V| v2)) i)))))))) +(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid :skolemid))) +(declare-fun |Select_[$Location]$bool| (b T@$Location) Bool) +(declare-fun $m@@0 () T@M) +(declare-fun $abort_flag@2 () Bool) +(declare-fun $m@3 () T@M) +(declare-fun mv () T@$TypeValue) +(declare-fun inline$$MoveToRaw$0$a@0 () Int) +(declare-fun |Store_[$Location]$bool| (b T@$Location Bool) b) +(assert (forall ((?x0 b) (?x1 T@$Location) (?y1 T@$Location) (?x2 Bool)) (or (= ?x1 ?y1) (= (|Select_[$Location]$bool| ?x0 ?y1) (|Select_[$Location]$bool| (|Store_[$Location]$bool| ?x0 ?x1 ?x2) ?y1))))) +(declare-fun inline$$MoveToRaw$0$l@1 () T@$Location) +(declare-fun |Store_[$Location]$Value| (l T@$Location T@$Value) l) +(assert (forall ((?x0 l) (?x1 T@$Location) (?x2 T@$Value)) (= ?x2 (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?x1)))) +(assert (forall ((?x0 l) (?x1 T@$Location) (?y1 T@$Location) (?x2 T@$Value)) (= (s ?x0 ?y1) (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?y1)))) +(declare-fun inline$$Event_EventHandleGenerator_pack$0$$struct@1 () T@$Value) +(declare-fun inline$$Event_publish_generator$0$$tmp@1 () T@$Value) +(declare-fun i () T@$Value) +(assert (and (not $abort_flag@2) (= inline$$Event_publish_generator$0$$tmp@1 (I 0)) (|b#$Boolean| ($Boolean (forall ((addr@@9 T@$Value)) (or (is-D addr@@9) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@9))))))))))) (or (not (=> $abort_flag@2 (|b#$Boolean| ($Boolean (forall ((addr@@4 T@$Value)) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@4)))))))))))))))) (and (= inline$$Event_EventHandleGenerator_pack$0$$struct@1 (V (R (st (st (m E) 0 inline$$Event_publish_generator$0$$tmp@1) 1 i) 1))) (not (=> (= inline$$MoveToRaw$0$a@0 (|a#D| i)) (= inline$$MoveToRaw$0$l@1 (G mv inline$$MoveToRaw$0$a@0)) (or (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| i))))) (not (= $m@3 (M (|Store_[$Location]$bool| (|domain#M| $m@@0) inline$$MoveToRaw$0$l@1 true) (|Store_[$Location]$Value| (|contents#M| $m@@0) inline$$MoveToRaw$0$l@1 inline$$Event_EventHandleGenerator_pack$0$$struct@1)))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (|v#R| $EmptyValueArray) 0)) 1))))) (or (not (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (st (|v#R| $EmptyValueArray) (|l#R| $EmptyValueArray) (I 0)) 1)) 0)))))) (and (|b#$Boolean| ($Boolean (forall ((addr@@1 T@$Value)) (|b#$Boolean| ($Boolean (or (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@1)))))) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean ($IsEqual_stratified (sel (|v#R| (|v#V| (s (|contents#M| $m@3) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter)))))))))))) (|b#$Boolean| ($Boolean (forall ((addr@@3 T@$Value)) (|b#$Boolean| ($Boolean (or (|b#$Boolean| ($Boolean ($IsEqual_stratified (I 0) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| addr@@3))))) $Event_EventHandleGenerator_counter)))) (not (|b#$Boolean| ($Boolean (and (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@3) (G mv (|a#D| addr@@3))))) (|b#$Boolean| ($Boolean (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G $LibraAccount_T_type_value (|a#D| addr@@3)))))))))))))))))))))))))))) +(check-sat) diff --git a/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 new file mode 100644 index 000000000..7f2e3084f --- /dev/null +++ b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 @@ -0,0 +1,41 @@ +; COMMAND-LINE: --ee-mode=distributed --no-check-unsat-cores +; COMMAND-LINE: --ee-mode=central --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((dA 0)) (((A)))) +(declare-datatypes ((Loc 0)) (((G (g dA) (ag Int))))) +(declare-sort v 0) +(declare-datatypes ((T 0) (U 0)) (((E) (I (ii Int)) (D (d Int)) (V (vv U))) ((R (rr v))))) +(declare-sort b 0) +(declare-sort l 0) +(declare-datatypes ((T@M 0)) (((M (dom b) (cnt l))))) +(declare-fun e () U) +(declare-fun m (T) v) +(declare-fun iseq (T T) Bool) +(declare-fun sel (v Int) T) +(declare-fun st (v) v) +(declare-fun s (l Loc) T) +(declare-fun sb (Loc) Bool) +(declare-fun m0 () T@M) +(declare-fun a () Bool) +(declare-fun im () Loc) +(declare-fun o (Loc T) l) +(declare-fun i () T) +(assert (forall ((?x0 v) (?x1 Int) (?x2 T)) (= ?x2 (sel (st ?x0) ?x1)))) +(assert (forall ((v1 T) (v2 T)) (= (iseq v1 v2) (forall ((i Int)) (iseq (sel (rr (vv v1)) i) (sel (rr (vv v2)) i)))))) +(assert (forall ((?x1 Loc) (?x2 T)) (= ?x2 (s (o ?x1 ?x2) ?x1)))) +(assert (and +(not a) +(forall ((?a9 T)) (or (is-D ?a9) (sb (G A (d ?a9))))) +(or +(not (=> a (forall (($a T)) (sb (G A (d $a)))))) +(and + (not (sb (G A (d i)))) + (= im (G A (d (I 0)))) + (= m0 (M (dom m0) (o im (V (R (st (m E))))))) + (iseq (s (cnt m0) (G A (d i))) (V (R (rr e)))) + (or + (exists ((?a1 T)) (not (iseq (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0) (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0)))) + (forall ((?a3 T)) (sb (G A (d ?a3))))))))) +(check-sat) |