From 2ef8fe2eefaecdb62653d36c88169fe906512b9d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Nov 2017 21:18:01 -0500 Subject: [PATCH] Suppport SAT logic (#1310) * Support SAT logic. * Add lustre example. * Add to smt1 as well. * Fix. * Fix. * Fix for new option. --- src/parser/smt1/smt1.cpp | 4 ++ src/parser/smt1/smt1.h | 1 + src/theory/logic_info.cpp | 4 ++ test/regress/regress0/fmf/Makefile.am | 3 +- test/regress/regress0/fmf/sat-logic.smt2 | 6 ++ test/regress/regress0/sygus/Makefile.am | 3 +- test/regress/regress0/sygus/ccp16.lus.sy | 72 ++++++++++++++++++++++++ 7 files changed, 91 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/fmf/sat-logic.smt2 create mode 100644 test/regress/regress0/sygus/ccp16.lus.sy diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index c4e670f6d..9a6d880e9 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -53,6 +53,7 @@ std::unordered_map 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 e9dbea1a9..036453675 100644 --- 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 ad3a010c0..335a87501 100644 --- 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 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) -- 2.30.2