diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-14 10:29:08 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-14 10:29:08 -0500 |
commit | 33420e77e9f7ee7a429708db3a7f6c28aef7d0ec (patch) | |
tree | de1d33cc21a9453caf0c0c1799b375d7ab53d5c9 /test | |
parent | 53c73505c5aed92401cfe02b669abaf8e6a30e32 (diff) |
Flag to check invariance of entire values in sygus explain (#1908)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/Makefile.tests | 3 | ||||
-rw-r--r-- | test/regress/regress1/sygus/crci-ssb-unk.sy | 43 | ||||
-rw-r--r-- | test/regress/regress2/sygus/sixfuncs.sy | 81 | ||||
-rw-r--r-- | test/regress/regress2/sygus/vcb.sy | 54 |
4 files changed, 181 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 52eb63789..5cb24d072 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1475,6 +1475,7 @@ REG1_TESTS = \ regress1/sygus/commutative.sy \ regress1/sygus/constant.sy \ regress1/sygus/constant-ite-bv.sy \ + regress1/sygus/crci-ssb-unk.sy \ regress1/sygus/dt-test-ns.sy \ regress1/sygus/dup-op.sy \ regress1/sygus/fg_polynomial3.sy \ @@ -1598,7 +1599,9 @@ REG2_TESTS = \ regress2/sygus/process-10-vars-2fun.sy \ regress2/sygus/process-arg-invariance.sy \ regress2/sygus/real-grammar-neg.sy \ + regress2/sygus/sixfuncs.sy \ regress2/sygus/three.sy \ + regress2/sygus/vcb.sy \ regress2/typed_v1l50016-simp.cvc \ regress2/uflia-error0.smt2 \ regress2/xs-09-16-3-4-1-5.decn.smt \ diff --git a/test/regress/regress1/sygus/crci-ssb-unk.sy b/test/regress/regress1/sygus/crci-ssb-unk.sy new file mode 100644 index 000000000..f2b28db9c --- /dev/null +++ b/test/regress/regress1/sygus/crci-ssb-unk.sy @@ -0,0 +1,43 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic BV) + + +(define-fun origCir ( (LN4 Bool) (LN91 Bool) ) Bool + (and LN91 LN4 ) +) + + +(synth-fun skel ( (LN4 Bool) (LN91 Bool) ) Bool + ((Start Bool ( + (and depth1 depth1) + (xor depth1 depth1) + )) + (depth1 Bool ( + (not depth2) + LN91 + )) + (depth2 Bool ( + (and depth3 depth3) + (not depth3) + (or depth3 depth3) + )) + (depth3 Bool ( + (and depth4 depth4) + (not depth4) + (or depth4 depth4) + (xor depth4 depth4) + )) + (depth4 Bool ( + LN4 + ))) +) + + +(declare-var LN4 Bool) +(declare-var LN91 Bool) + +(constraint (= (origCir LN4 LN91 ) (skel LN4 LN91 ))) + +(check-synth) diff --git a/test/regress/regress2/sygus/sixfuncs.sy b/test/regress/regress2/sygus/sixfuncs.sy new file mode 100644 index 000000000..5280ffb20 --- /dev/null +++ b/test/regress/regress2/sygus/sixfuncs.sy @@ -0,0 +1,81 @@ +(set-logic LIA) + +(synth-fun f1 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + +(synth-fun f2 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (+ Start Start) + ) + ))) + +(synth-fun f3 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + +(synth-fun f4 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + +(synth-fun f5 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + +(synth-fun g1 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (+ (f1 x y) (f1 x y)) (f2 x y))) +(constraint (= (- (+ (f1 x y) (f2 x y)) y) (f3 x y))) +(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y))) +(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y))) + +(constraint (= (- (f1 x y) y) (g1 x y))) + + +(check-synth) + +;; possible solution +;; f1: y+x+1 +;; f2: y+2x+2 +;; f3: y+3x+3 +;; f4: 4y+4x+4 +;; f5: 5y+5x+5 +;; g1: x+1 +;; g2: y+2 +;; g3: y+3 +;; g4: 2y+6 +;; g5: 3y+x+7 + diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy new file mode 100644 index 000000000..9cc2389f3 --- /dev/null +++ b/test/regress/regress2/sygus/vcb.sy @@ -0,0 +1,54 @@ +(set-logic LIA) + +(synth-fun f1 ((x1 Int) (x2 Int)) Int) + +(synth-fun f2 ((x1 Int) (x2 Int)) Int) + +(define-fun vmin () Int 1) +(define-fun vmax () Int 2) + +(define-fun AllZero ((v1 Int) (v2 Int)) Bool + (and (= v1 0) (= v2 0))) + +(define-fun InV ((v1 Int) (v2 Int)) Bool + (and (and (and (>= v1 vmin) (<= v1 vmax)) (>= v2 vmin)) (<= v2 vmax))) + +(define-fun InVorZero ((v1 Int) (v2 Int)) Bool + (or (InV v1 v2) (AllZero v1 v2))) + +(define-fun UnsafeSame ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool + (or (and (>= x1 x2) (>= (+ x2 v2) (+ x1 v1))) + (and (>= x2 x1) (>= (+ x1 v1) (+ x2 v2))))) + +(define-fun BadSame ((x1 Int) (x2 Int)) Bool + (= x1 x2)) + +(define-fun Bad ((x1 Int) (x2 Int)) Bool + (BadSame x1 x2)) + +(define-fun Unsafe ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool + (UnsafeSame x1 x2 v1 v2)) + + +(declare-var x1 Int) +(declare-var x2 Int) +(declare-var v1 Int) +(declare-var v2 Int) + +(constraint (InVorZero (f1 x1 x2) (f2 x1 x2))) + +(constraint (or (or (not (InV v1 v2)) + (AllZero (f1 x1 x2) (f2 x1 x2))) + (and (not (Unsafe x1 x2 (f1 x1 x2) (f2 x1 x2))) + (not (AllZero (f1 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2))) + (f2 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2)))))))) + +(constraint (or (or (or (not (InV v1 v2)) + (Unsafe x1 x2 v1 v2)) + (AllZero (f1 (+ x1 v1) (+ x2 v2)) (f2 (+ x1 v1) (+ x2 v2)))) + (not (AllZero (f1 x1 x2) (f2 x1 x2))))) + + +(constraint (or (Bad x1 x2) (not (AllZero (f1 x1 x2) (f2 x1 x2))))) + +(check-synth)
\ No newline at end of file |