diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-09 07:42:03 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-09 07:42:03 -0600 |
commit | 6cb2e5743bd886115124256c2a3ad689a5b822a2 (patch) | |
tree | 9376134244e1fc6729bc10a1a78fcdf2ee73d76d /test | |
parent | 63df35c477ee9e6c7bdeae677656dd374563de55 (diff) |
Do not regress explanations of datatype lemmas (#5376)
This modifies datatypes to not regress explanations for lemmas. This avoids segfaults in some corner cases of sygus (see attached) and leads to slightly better performance on Facebook verification benchmarks.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress2/sygus/policyM.sy | 41 |
2 files changed, 42 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c6c55d847..58a43895e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2201,6 +2201,7 @@ set(regress_2_tests regress2/sygus/nia-max-square.sy regress2/sygus/no-syntax-test-no-si.sy regress2/sygus/pbe_bvurem.sy + regress2/sygus/policyM.sy regress2/sygus/process-10-vars-2fun.sy regress2/sygus/process-arg-invariance.sy regress2/sygus/real-grammar-neg.sy diff --git a/test/regress/regress2/sygus/policyM.sy b/test/regress/regress2/sygus/policyM.sy new file mode 100644 index 000000000..0e9b33148 --- /dev/null +++ b/test/regress/regress2/sygus/policyM.sy @@ -0,0 +1,41 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --lang=sygus2 +(set-logic ALL) + +(declare-datatype Pair ((pair (pmin Int) (pmax Int)))) + +(define-fun wf ((p Pair)) Bool + (<= (pmin p) (pmax p))) +(define-fun a ((p Pair) (q Pair)) Bool + (< (pmax p) (pmin q))) +(define-fun intMax ((x Int) (y Int)) Int + (ite (>= x y) x y)) +(define-fun intMin ((x Int) (y Int)) Int + (ite (>= x y) y x)) +(define-fun midpoint ((x Int) (y Int)) Int + (div (+ x y) 2)) + +(synth-fun pW ((p Pair) (q Pair)) Pair + ((StartPair Pair) (StartInt Int)) ( + (StartPair Pair ((pair StartInt StartInt))) + (StartInt Int ((pmin p) (pmax p) (pmin q) (pmax q) (intMax StartInt StartInt) (intMin StartInt StartInt) (midpoint StartInt StartInt))) +)) +(synth-fun pL ((p Pair) (q Pair)) Pair + ((StartPair Pair) (StartInt Int)) ( + (StartPair Pair ((pair StartInt StartInt))) + (StartInt Int ((+ StartInt StartInt) 0 1 (pmin p) (pmax p) (pmin q) (pmax q) (intMax StartInt StartInt) (intMin StartInt StartInt) (midpoint StartInt StartInt))) +)) + +(declare-var p Pair) +(declare-var q Pair) +(declare-var r Pair) + +(constraint (=> (and (wf p) (wf q)) (wf (pW p q)))) +(constraint (=> (and (wf p) (wf q)) (wf (pL p q)))) + +(constraint (=> (and (wf p) (wf q) (wf r) (a p r)) (a (pW p q) r))) +(constraint (=> (and (wf p) (wf q) (wf r) (a p r)) (a p (pL r q)))) + +(constraint (=> (and (wf p) (wf q)) (not (a (pL q p) (pW p q))))) + +(check-synth) |