From 45a138c326da72890bf889a3670aad503ef4aa1e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 1 Mar 2012 14:48:04 +0000 Subject: Partial merge from kind-backend branch, including Minisat and CNF work to support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too! --- src/parser/smt/smt.cpp | 11 +++++++++++ src/parser/smt/smt.h | 3 +++ 2 files changed, 14 insertions(+) (limited to 'src/parser/smt') diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index 0ee6944d4..508bfe352 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -41,6 +41,9 @@ std::hash_map Smt::newL logicMap["QF_UFIDL"] = QF_UFIDL; logicMap["QF_UFLRA"] = QF_UFLRA; logicMap["QF_UFLIA"] = QF_UFLIA; + logicMap["QF_UFLIRA"] = QF_UFLIRA; + logicMap["QF_UFNIA"] = QF_UFNIA; + logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; return logicMap; @@ -159,6 +162,7 @@ void Smt::setLogic(const std::string& name) { case QF_UFIDL: case QF_UFLIA: + case QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addUf(); break; @@ -169,6 +173,13 @@ void Smt::setLogic(const std::string& name) { addUf(); break; + case QF_UFLIRA:// nonstandard logic + case QF_UFNIRA:// nonstandard logic + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addUf(); + break; + case QF_UF: addUf(); break; diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index a99f81998..62bb24336 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -54,7 +54,10 @@ public: QF_UF, QF_UFIDL, QF_UFLIA, + QF_UFNIA, // nonstandard QF_UFLRA, + QF_UFLIRA, // nonstandard + QF_UFNIRA, // nonstandard QF_UFNRA, UFNIA }; -- cgit v1.2.3