Suppport SAT logic (#1310)

* Support SAT logic.

* Add lustre example.

* Add to smt1 as well.

* Fix.

* Fix.

* Fix for new option.

4 files changed, 82 insertions, 2 deletions

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index b2ed657d0..122f9219b 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -78,7 +78,8 @@ TESTS =	\
 	cruanes-no-minimal-unk.smt2 \
 	no-minimal-sat.smt2 \
 	issue916-fmf-or.smt2 \
-	pow2-bool.smt2 
+	pow2-bool.smt2 \
+	sat-logic.smt2 
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/sat-logic.smt2 b/test/regress/regress0/fmf/sat-logic.smt2
new file mode 100644
index 000000000..678ea3079
--- /dev/null
+++ b/test/regress/regress0/fmf/sat-logic.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic SAT)
+(set-info :status sat)
+(assert (forall ((x Bool) (y Bool)) (exists ((z Bool)) (= z (and x y)))))
+(check-sat)
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 6dfcb922a..3c118a007 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -66,7 +66,8 @@ TESTS = commutative.sy \
         cegar1.sy \
         triv-type-mismatch-si.sy \
         nia-max-square-ns.sy \
-        strings-concat-3-args.sy
+        strings-concat-3-args.sy \
+        ccp16.lus.sy
 
 
 # sygus tests currently taking too long for make regress
diff --git a/test/regress/regress0/sygus/ccp16.lus.sy b/test/regress/regress0/sygus/ccp16.lus.sy
new file mode 100644
index 000000000..662069105
--- /dev/null
+++ b/test/regress/regress0/sygus/ccp16.lus.sy
@@ -0,0 +1,72 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic SAT)
+
+(define-fun
+  __node_init_top_0 (
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+  ) Bool
+  
+  (and (= top.usr.OK_a_0 true) top.res.init_flag_a_0)
+)
+
+(define-fun
+  __node_trans_top_0 (
+    (top.usr.OK_a_1 Bool)
+    (top.res.init_flag_a_1 Bool)
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+  ) Bool
+  
+  (and (= top.usr.OK_a_1 true) (not top.res.init_flag_a_1))
+)
+
+
+
+(synth-inv str_invariant(
+  (top.usr.OK Bool)
+  (top.res.init_flag Bool)
+))
+
+
+(declare-primed-var top.usr.OK Bool)
+(declare-primed-var top.res.init_flag Bool)
+
+(define-fun
+  init (
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+  ) Bool
+  
+  (and (= top.usr.OK true) top.res.init_flag)
+)
+
+(define-fun
+  trans (
+    
+    ;; Current state.
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    
+    ;; Next state.
+    (top.usr.OK! Bool)
+    (top.res.init_flag! Bool)
+  
+  ) Bool
+  
+  (and (= top.usr.OK! true) (not top.res.init_flag!))
+)
+
+(define-fun
+  prop (
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+  ) Bool
+  
+  top.usr.OK
+)
+
+(inv-constraint str_invariant init trans prop)
+
+(check-synth)