diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-01 09:07:42 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-01 09:07:42 -0600 |
commit | f40d813048599b58327fc968344301d39f156da2 (patch) | |
tree | 6441035d51eccca0156ed15d142ced27eb7187d4 /test | |
parent | 9f3ea3328213e08bf39b8ceeea272205255fd7ed (diff) |
Refactor and generalize PBE strategies (#1410)
Diffstat (limited to 'test')
6 files changed, 145 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 82c2c2458..b2cf8a069 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -71,7 +71,12 @@ TESTS = commutative.sy \ process-10-vars-2fun.sy \ inv-unused.sy \ ccp16.lus.sy \ - Base16_1.sy + Base16_1.sy \ + icfp_14.12-flip-args.sy \ + strings-template-infer-unused.sy \ + strings-trivial-two-type.sy \ + strings-double-rec.sy \ + hd-19-d1-prog-dup-op.sy # sygus tests currently taking too long for make regress @@ -79,6 +84,8 @@ EXTRA_DIST = $(TESTS) \ max.smt2 \ sygus-uf.sl \ enum-test.sy + +# strings-concat-3-args.sy #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy new file mode 100644 index 000000000..abcfc2217 --- /dev/null +++ b/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy @@ -0,0 +1,32 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status + +(set-logic BV) + +(define-fun hd19 ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) + (bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m)))) + +; bvand is a duplicate +(synth-fun f ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) + ((Start (BitVec 32) ((bvand Start Start) + (bvsub Start Start) + (bvxor Start Start) + (bvor Start Start) + (bvand Start Start) + (bvshl Start Start) + (bvlshr Start Start) + (bvashr Start Start) + (bvnot Start) + (bvneg Start) + x + m + k)))) + + +(declare-var x (BitVec 32)) +(declare-var m (BitVec 32)) +(declare-var k (BitVec 32)) + +(constraint (= (hd19 x m k) (f x m k))) +(check-synth) + diff --git a/test/regress/regress0/sygus/icfp_14.12-flip-args.sy b/test/regress/regress0/sygus/icfp_14.12-flip-args.sy new file mode 100644 index 000000000..a1e93cc44 --- /dev/null +++ b/test/regress/regress0/sygus/icfp_14.12-flip-args.sy @@ -0,0 +1,55 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic BV) + +(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) +(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004)) +(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010)) +(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001)) +(define-fun if0 ((y (BitVec 64)) (x (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z)) + +(synth-fun f ( (x (BitVec 64))) (BitVec 64) +( + +(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) + )) +) +) +(constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) +(constraint (= (f #xFDA75AD598A27135) #x812C529533AEC765)) +(constraint (= (f #x58682C0FA4F8DB6D) #xD3CBE9F82D839249)) +(constraint (= (f #x58FDC0941A7E079F) #xD3811FB5F2C0FC30)) +(constraint (= (f #xBDC9B88103ECB0C9) #xA11B23BF7E09A79B)) +(constraint (= (f #x000000000001502F) #xFFFFFFFFFFFF57E8)) +(constraint (= (f #x0000000000010999) #xFFFFFFFFFFFF7B33)) +(constraint (= (f #x0000000000013169) #xFFFFFFFFFFFF674B)) +(constraint (= (f #x000000000001B1A9) #xFFFFFFFFFFFF272B)) +(constraint (= (f #x0000000000016D77) #xFFFFFFFFFFFF4944)) +(constraint (= (f #x0000000000000001) #xFFFFFFFFFFFFFFFF)) +(constraint (= (f #x1ED2E25068744C80) #x0000000000000000)) +(constraint (= (f #x2D2144F9D8CDCBD6) #x0000000000000000)) +(constraint (= (f #xF0F0F0F0F0F0F0F2) #x0000000000000000)) +(constraint (= (f #x83163CFD5DDCCCFB) #xBE74E18151119982)) +(constraint (= (f #xEA31B6A50EF4E399) #x8AE724AD78858E33)) +(constraint (= (f #xE0B1EF549BB6D4B9) #x8FA70855B22495A3)) +(constraint (= (f #x086F9E13A16C363D) #xFBC830F62F49E4E1)) +(constraint (= (f #x2426824D3E67E342) #x0000000000000000)) +(constraint (= (f #xDD518DEFFF18308A) #x0000000000000000)) +(constraint (= (f #x21ECDADB06B3CB03) #xEF0992927CA61A7E)) +(constraint (= (f #x72B1976FBB63A82B) #xC6A73448224E2BEA)) +(constraint (= (f #x16CB47AE0281B27F) #xF49A5C28FEBF26C0)) +(constraint (= (f #x82DE7A1FCA0C0B8F) #xBE90C2F01AF9FA38)) +(constraint (= (f #x0000000000000001) #xFFFFFFFFFFFFFFFF)) +(constraint (= (f #xF0F0F0F0F0F0F0F2) #x0000000000000000)) +(constraint (= (f #x000000000001F0D4) #x0000000000000000)) +(constraint (= (f #x0000000000010067) #xFFFFFFFFFFFF7FCC)) +(check-synth) diff --git a/test/regress/regress0/sygus/strings-double-rec.sy b/test/regress/regress0/sygus/strings-double-rec.sy new file mode 100644 index 000000000..ea9caadea --- /dev/null +++ b/test/regress/regress0/sygus/strings-double-rec.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((name String)) String + ((Start String (name "A" "B" "" (str.++ Start1 Start2))) + (Start1 String (name "A" "B" "")) + (Start2 String (name "B" "A" (str.++ Start2 Start))) +)) + + +(declare-var name String) + +(constraint (= (f "BB") "AAAAAAAAAAAA")) + +(check-synth) diff --git a/test/regress/regress0/sygus/strings-template-infer-unused.sy b/test/regress/regress0/sygus/strings-template-infer-unused.sy new file mode 100644 index 000000000..d0bee5564 --- /dev/null +++ b/test/regress/regress0/sygus/strings-template-infer-unused.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(define-fun cA ((x String) (w String) (y String) (z String)) String (str.++ (str.++ x "A") y)) + +(synth-fun f ((name String)) String + ((Start String (name "A" "B" "" + (cA Start Start Start Start))))) + + +(declare-var name String) + +(constraint (= (f "BB") "AAAAAAAAAAAA")) + +(check-synth) diff --git a/test/regress/regress0/sygus/strings-trivial-two-type.sy b/test/regress/regress0/sygus/strings-trivial-two-type.sy new file mode 100644 index 000000000..86c71aa3a --- /dev/null +++ b/test/regress/regress0/sygus/strings-trivial-two-type.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((name String)) String + ((Start String (ntString)) + (ntString String (name "B" "" + (str.++ ntStringC ntString))) + (ntStringC String (name "A" "")) + + )) + + +(declare-var name String) + +(constraint (= (f "B") "AAAAAAAAAAAAAAAAAAAAAAAAA")) + +(check-synth) |