Sygus inv templ refactor (#1110)

* Decouple single invocation techniques from deep embedding techniques. Embed templates for invariant synthesis into grammar instead of as a global substitution. Add regression.

* Update comment on class

* Cleanup

* Comments for sygus type construction.

2 files changed, 25 insertions, 1 deletions

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index c22f64b93..01f3be1a1 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -62,7 +62,8 @@ TESTS = commutative.sy \
         General_plus10.sy \
         qe.sy \
         cggmp.sy \
-        parse-bv-let.sy
+        parse-bv-let.sy \
+        cegar1.sy
 
 
 # sygus tests currently taking too long for make regress
diff --git a/test/regress/regress0/sygus/cegar1.sy b/test/regress/regress0/sygus/cegar1.sy
new file mode 100644
index 000000000..dd7f73e27
--- /dev/null
+++ b/test/regress/regress0/sygus/cegar1.sy
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth
+(set-logic LIA)
+
+(synth-inv inv-f ((x Int) (y Int)))
+
+(declare-primed-var x Int)
+(declare-primed-var y Int)
+
+(define-fun pre-f ((x Int) (y Int)) Bool
+(and (and (>= x 0)
+(and (<= x 2)  
+(<= y 2))) (>= y 0)))
+
+(define-fun trans-f ((x Int) (y Int) (x! Int) (y! Int)) Bool
+(and (= x! (+ x 2)) (= y! (+ y 2))))
+
+(define-fun post-f ((x Int) (y Int)) Bool
+(not (and (= x 4) (= y 0))))
+
+(inv-constraint inv-f pre-f trans-f post-f)
+
+(check-synth)