diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-19 12:39:07 -0400 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-19 12:39:07 -0400 |
commit | 7de5f26ca35f6b3b11dc8a7465f7a15e5d0d2e50 (patch) | |
tree | a0c0cd831361d7e872618fc9e8739f63db9760bb /test/regress | |
parent | 9fa66413709fbdb1a02f8986d0c332934523b110 (diff) |
Fixes for sygus with datatypes (#3103)
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/error1-dt.sy | 71 |
2 files changed, 72 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index af6a9b839..29f31960c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1641,6 +1641,7 @@ set(regress_1_tests regress1/sygus/double.sy regress1/sygus/dt-test-ns.sy regress1/sygus/dup-op.sy + regress1/sygus/error1-dt.sy regress1/sygus/extract.sy regress1/sygus/fg_polynomial3.sy regress1/sygus/find_sc_bvult_bvnot.sy diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy new file mode 100644 index 000000000..67f73aded --- /dev/null +++ b/test/regress/regress1/sygus/error1-dt.sy @@ -0,0 +1,71 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-active-gen=enum + +(set-logic ALL_SUPPORTED) + +(declare-datatypes ((IntRange 0)) + (((IntRange (lower Int) (upper Int))))) + +(declare-datatypes ((Loc 0)) + (((Loc (x Int) (y Int))))) + +(declare-datatypes ((LocRange 0)) + (((LocRange (xD IntRange) (yD IntRange))))) + +(declare-datatypes ((Ship 0)) + (((Ship (shipCapacity Int) (shipLoc Loc))))) + +(declare-datatypes ((ShipRange 0)) + (((ShipRange (shipCapacityD IntRange) (shipLocD LocRange))))) + +(define-fun betweenInt ((x Int) (r IntRange)) Bool + (and (< (lower r) x) (< x (upper r))) +) + +(define-fun betweenLoc ((l Loc) (lr LocRange)) Bool + (and (betweenInt (x l) (xD lr)) (betweenInt (y l) (yD lr))) +) + +(define-fun subsetInt ((r1 IntRange) (r2 IntRange)) Bool + (and (>= (lower r1) (lower r2)) (<= (upper r1) (upper r2))) +) + +(define-fun betweenShip ((s Ship) (sr ShipRange)) Bool + (and (betweenInt (shipCapacity s) (shipCapacityD sr)) (betweenLoc (shipLoc s) (shipLocD sr))) +) + +(define-fun atLeast ((s Ship)) Bool + (> (shipCapacity s) 50) +) + +(define-fun subsetLoc ((s1 LocRange) (s2 LocRange)) Bool + (and (subsetInt (xD s1) (xD s2)) (subsetInt (yD s1) (yD s2))) +) + +(define-fun subsetShip ((s1 ShipRange) (s2 ShipRange)) Bool + (and (subsetInt (shipCapacityD s1) (shipCapacityD s2)) (subsetLoc (shipLocD s1) (shipLocD s2))) +) + +(define-fun max ((x Int) (y Int)) Int + (ite (>= x y) x y) +) + +(define-fun min ((x Int) (y Int)) Int + (ite (<= x y) x y) +) + + +(synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange) + +(declare-var secret Ship) +(declare-var prior ShipRange) +(declare-var response Bool) + +(constraint + (=> (betweenShip secret (f secret prior response)) + (= response + (and (atLeast secret) + (subsetShip (f secret prior response) prior)))) +) + +(check-synth) |