diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-10 14:35:25 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-10 14:35:37 +0100 |
commit | 81dca680f6c88d10b56a0ed065d470d907766e21 (patch) | |
tree | 4410fa473ecb6848f7976b2b6a00188ac5e44775 /test | |
parent | 50c8533760bfd5b1f803d52bc4318c544521e6af (diff) |
Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 | 75 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 | 26 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/matching-lia-1arg.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/sygus/dt-test-ns.sy | 14 |
7 files changed, 130 insertions, 3 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 45a9d6f30..d06fb1b9b 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -67,7 +67,8 @@ TESTS = \ manos-model.smt2 \ bug625.smt2 \ cdt-model-cade15.smt2 \ - sc-cdt1.smt2 + sc-cdt1.smt2 \ + conqueue-dt-enum-iloop.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 new file mode 100644 index 000000000..6f82cd842 --- /dev/null +++ b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 @@ -0,0 +1,75 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun start!13 () Bool) + +(assert start!13) + +(declare-fun b!39 () Bool) + +(declare-sort T!14 0) + +(declare-datatypes () ( +(LazyConQ!5 + (Lazyarg1!5 (carry!37 Conc!6) (srear!9 LazyConQ!5)) + (Lazyarg2!5 (t!270 ConQ!6)) + (Lazyarg3!5 (carry!38 Conc!6) (t!271 ConQ!6)) + (Lazyarg4!5 (tree!19 Conc!6) (carry!39 Conc!6)) + (Lazyarg5!5 (tree!20 Conc!6) (carry!40 Conc!6)) + (PushLeft!5 (ys!22 Conc!6) (xs!60 LazyConQ!5)) + (PushLeftLazy!5 (ys!23 Conc!6) (xs!61 LazyConQ!5))) +(Conc!6 + (CC!5 (left!9 Conc!6) (right!9 Conc!6)) + (Empty!5) + (Single!5 (x!106 T!14))) +(ConQ!6 + (Spine!5 (head!10 Conc!6) (rear!5 LazyConQ!5)) + (Tip!5 (t!272 Conc!6))) +)) + +(declare-fun e!41 () LazyConQ!5) + +(declare-fun l!2 () LazyConQ!5) + +(declare-fun st!3 () (Set LazyConQ!5)) + +(declare-fun firstUnevaluated!3 (LazyConQ!5 (Set LazyConQ!5)) LazyConQ!5) + +(declare-fun evalLazyConQ2!7 (LazyConQ!5) ConQ!6) + +(assert (=> b!39 (= e!41 (firstUnevaluated!3 (rear!5 (evalLazyConQ2!7 l!2)) st!3)))) + +(declare-fun b!40 () Bool) + +(declare-fun e!42 () LazyConQ!5) + +(assert (=> b!40 (= e!42 e!41))) + +(assert (=> b!40 (= b!39 (is-Spine!5 (evalLazyConQ2!7 l!2))))) + +(declare-fun b!41 () Bool) + +(assert (=> b!40 (or (not b!39) (not b!41)))) + +(assert (=> b!40 (or b!39 b!41))) + +(assert (=> b!41 (= e!41 l!2))) + +(declare-fun b!42 () Bool) + +(assert (=> b!42 (= e!42 l!2))) + +(declare-fun lt!14 () LazyConQ!5) + +(declare-fun isTip!5 (ConQ!6) Bool) + +(assert (=> start!13 (and (not (isTip!5 (evalLazyConQ2!7 lt!14))) (member lt!14 st!3)))) + +(assert (=> start!13 (= lt!14 e!42))) + +(assert (=> start!13 (= b!40 (member l!2 st!3)))) + +(assert (=> start!13 (or (not b!40) (not b!42)))) + +(assert (=> start!13 (or b!40 b!42))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index e6b0a59fc..939b0d22c 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -61,7 +61,9 @@ TESTS = \ mix-simp.smt2 \ mix-coeff.smt2 \ mix-match.smt2 \ - ari056.smt2 + ari056.smt2 \ + ext-ex-deq-trigger.smt2 \ + matching-lia-1arg.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 new file mode 100644 index 000000000..f6f96fe02 --- /dev/null +++ b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-const k U) +(declare-const ff U) +(declare-const ffk U) +(declare-fun fun1 (Int) Int) +(declare-fun fun2 (Int) Int) +(declare-fun c (U U) U) +(declare-fun app (U Int) Int) + +(assert (forall ((f U) (g U)) (=> (forall ((x Int)) (= (app f x) (app g x))) (= f g)) )) + +(assert (forall ((x Int)) (= (app ff x) (+ (fun1 x) (fun2 x))))) +(assert (forall ((x Int)) (= (app ffk x) (+ (fun1 (app k x)) (fun2 (app k x)))))) + +(assert (forall ((f U) (g U) (x Int)) (= (app (c f g) x) (app f (app g x))))) + +(assert (not (= (c ff k) ffk))) + +(check-sat) + diff --git a/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 new file mode 100644 index 000000000..aaf9b2c1f --- /dev/null +++ b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --purify-triggers +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (P (* 2 x)))) +(assert (not (P 38))) +(check-sat) + diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index a1f91a6ce..71ca64aea 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -45,7 +45,8 @@ TESTS = commutative.sy \ sygus-dt.sy \ dt-no-syntax.sy \ list-head-x.sy \ - clock-inc-tuple.sy + clock-inc-tuple.sy \ + dt-test-ns.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy new file mode 100644 index 000000000..ed17f4ff2 --- /dev/null +++ b/test/regress/regress0/sygus/dt-test-ns.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si --no-dump-synth +(set-logic LIA) + +(declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) + +(synth-fun f ((x Int)) List) + +(declare-var x Int) + +(constraint (is-cons (f x))) +(constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x))))))) +(check-synth) + |