Refactor and generalize PBE strategies (#1410)

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)