Suppport SAT logic (#1310)

* Support SAT logic.

* Add lustre example.

* Add to smt1 as well.

* Fix.

* Fix.

* Fix for new option.

diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index c4e670f6d0ec0d475c164e0ddb0960b49fc93383..9a6d880e99730113c3bc0e53b9e6211b0ecb116b 100644 (file)
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -53,6 +53,7 @@ std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
+  logicMap["SAT"] = SAT;
   logicMap["UFNIA"] = UFNIA;
   logicMap["UFNIRA"] = UFNIRA;
   logicMap["UFLRA"] = UFLRA;
@@ -205,6 +206,9 @@ void Smt1::setLogic(const std::string& name) {
   case QF_SAT:
     /* no extra symbols needed */
     break;
+  case SAT:
+    addTheory(THEORY_QUANTIFIERS);
+    break;
 
   case QF_UFIDL:
   case QF_UFLIA:

diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index e9dbea1a9152c3f07fcb25c14e86458a7dd579ce..0364536756b8d7a12e37352f968866b0f8af02e5 100644 (file)
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -62,6 +62,7 @@ public:
     QF_UFLIRA, // nonstandard
     QF_UFNIRA, // nonstandard
     QF_UFNRA,
+    SAT,
     UFLRA,
     UFNIRA, // nonstandard
     UFNIA,

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index ad3a010c0e313170a3cc3b4cf0f17476d2381ec8..335a8750168b4cc4c4c223d893bd08250aae5730 100644 (file)
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -336,6 +336,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
   } else if(!strcmp(p, "QF_SAT")) {
     // propositional logic only; we're done.
     p += 6;
+  } else if(!strcmp(p, "SAT")) {
+    // quantified Boolean formulas only; we're done.
+    enableQuantifiers();
+    p += 3;
   } else if(!strcmp(p, "QF_ALL_SUPPORTED")) {
     // the "all theories included" logic, no quantifiers
     enableEverything();

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index b2ed657d07ade9863e3665aefbf4c948681f52a6..122f9219b7c679805f684923eb2326467bf1650b 100644 (file)
--- 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 (file)
index 0000000..678ea30
--- /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 6dfcb922ae06c1a5367fd043c35bda1d631c0636..3c118a00795b7ef39dd39932f03ecd2270871e4e 100644 (file)
--- 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 (file)
index 0000000..6620691
--- /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)