From d4fb7022845f3ec595cff3fb1b6324e2364d25d3 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 17 May 2013 08:43:24 -0400 Subject: Fix to empty response to (get-assignment). Thanks to David Cok for reporting this issue. --- src/smt/smt_engine.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0bfc6e634..284f39d54 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3313,7 +3313,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { } if(d_assignments == NULL) { - return SExpr(); + return SExpr(vector()); } vector sexprs; -- cgit v1.2.3 From 59cb1ace343f74af41fae55933be48d1b3995780 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 17 May 2013 10:19:54 -0400 Subject: Better error on invalid logic strings. Thanks to David Cok for reporting this issue. Conflicts: library_versions --- src/smt/smt_engine.cpp | 16 ++++++++-------- src/smt/smt_engine.h | 4 ++-- src/theory/logic_info.cpp | 7 ++++++- 3 files changed, 16 insertions(+), 11 deletions(-) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 284f39d54..3ee6b1d74 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -791,21 +791,21 @@ SmtEngine::~SmtEngine() throw() { void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { SmtScope smts(this); - d_logic = logic; setLogicInternal(); } -void SmtEngine::setLogic(const std::string& s) throw(ModalException) { +void SmtEngine::setLogic(const std::string& s) throw(ModalException, LogicException) { SmtScope smts(this); - - setLogic(LogicInfo(s)); + try { + setLogic(LogicInfo(s)); + } catch(IllegalArgumentException& e) { + throw LogicException(e.what()); + } } -void SmtEngine::setLogic(const char* logic) throw(ModalException){ - SmtScope smts(this); - - setLogic(LogicInfo(string(logic))); +void SmtEngine::setLogic(const char* logic) throw(ModalException, LogicException) { + setLogic(string(logic)); } LogicInfo SmtEngine::getLogicInfo() const { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a22e34c21..8266bb1ed 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -350,12 +350,12 @@ public: /** * Set the logic of the script. */ - void setLogic(const std::string& logic) throw(ModalException); + void setLogic(const std::string& logic) throw(ModalException, LogicException); /** * Set the logic of the script. */ - void setLogic(const char* logic) throw(ModalException); + void setLogic(const char* logic) throw(ModalException, LogicException); /** * Set the logic of the script. diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index dc9de8662..cbd0b510e 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -241,7 +241,12 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } if(*p != '\0') { stringstream err; - err << "LogicInfo::setLogicString(): junk (\"" << p << "\") at end of logic string: " << logicString; + err << "LogicInfo::setLogicString(): "; + if(p == logicString) { + err << "cannot parse logic string: " << logicString; + } else { + err << "junk (\"" << p << "\") at end of logic string: " << logicString; + } IllegalArgument(logicString, err.str().c_str()); } -- cgit v1.2.3 From 611c12a19eaf359dd26da9d0a2b2e2215066180d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 17 May 2013 11:12:36 -0400 Subject: Fix for equality-chaining of Booleans in SMT-LIBv2. Thanks to David Cok for reporting this. --- src/smt/boolean_terms.cpp | 2 +- test/regress/regress0/Makefile.am | 1 + test/regress/regress0/chained-equality.smt2 | 10 ++++++++++ 3 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/chained-equality.smt2 (limited to 'src/smt') diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 0063035ff..166a695a4 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -715,7 +715,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa // push children for(int i = top.getNumChildren() - 1; i >= 0; --i) { Debug("bt") << "rewriting: " << top[i] << endl; - worklist.push(triple(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), false)); + worklist.push(triple(top[i], top.getKind() == kind::CHAIN ? parentTheory : (isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN)), false)); //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars); //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl; } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 12d7ab397..fec081ca8 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -42,6 +42,7 @@ SMT_TESTS = \ # Regression tests for SMT2 inputs SMT2_TESTS = \ + chained-equality.smt2 \ ite2.smt2 \ ite3.smt2 \ ite4.smt2 \ diff --git a/test/regress/regress0/chained-equality.smt2 b/test/regress/regress0/chained-equality.smt2 new file mode 100644 index 000000000..fb3a25b94 --- /dev/null +++ b/test/regress/regress0/chained-equality.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-info :status unsat) +(set-logic QF_UF) +(declare-fun x () Bool) +(declare-fun y () Bool) +(declare-fun z () Bool) +(assert (= x y z)) +(assert (not x)) +(assert z) +(check-sat) -- cgit v1.2.3 From a8d4a41201ea8be04a2464ca734848b8cdff30cc Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 17 May 2013 12:03:29 -0400 Subject: Don't allow get-model & co after a user push/pop This makes us more strictly adhere to the spec, but it's useful anyway: previously we would support a get-model until the problem was explicitly changed with e.g. a new assertion. That meant you could check-sat, then pop, then get-model, but you'd only get the part of the model still in scope. This is strange, and would likely lead to problems, so it's now disabled. Thanks to David Cok for inquiring about this. --- NEWS | 5 ++++- src/smt/smt_engine.cpp | 13 +++++++++++++ src/smt/smt_engine.h | 6 +++--- 3 files changed, 20 insertions(+), 4 deletions(-) (limited to 'src/smt') diff --git a/NEWS b/NEWS index b8f1177d0..eb991f74c 100644 --- a/NEWS +++ b/NEWS @@ -3,7 +3,10 @@ This file contains a summary of important user-visible changes. Changes since 1.2 ================= -* nothing yet +* We no longer permit model or proof generation if there's been an + intervening push/pop. +* Increased compliance to SMT-LIBv2, numerous bugs and usability issues + resolved Changes since 1.1 ================= diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3ee6b1d74..3cc6e7502 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3625,6 +3625,11 @@ void SmtEngine::push() throw(ModalException, LogicException) { d_needPostsolve = false; } + // The problem isn't really "extended" yet, but this disallows + // get-model after a push, simplifying our lives somewhat and + // staying symmtric with pop. + d_problemExtended = true; + d_userLevels.push_back(d_userContext->getLevel()); internalPush(); Trace("userpushpop") << "SmtEngine: pushed to level " @@ -3651,6 +3656,14 @@ void SmtEngine::pop() throw(ModalException) { d_needPostsolve = false; } + // The problem isn't really "extended" yet, but this disallows + // get-model after a pop, simplifying our lives somewhat. It might + // not be strictly necessary to do so, since the pops occur lazily, + // but also it would be weird to have a legally-executed (get-model) + // that only returns a subset of the assignment (because the rest + // is no longer in scope!). + d_problemExtended = true; + AlwaysAssert(d_userContext->getLevel() > 0); AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); while (d_userLevels.back() < d_userContext->getLevel()) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8266bb1ed..1b5af415f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -189,9 +189,9 @@ class CVC4_PUBLIC SmtEngine { bool d_fullyInited; /** - * Whether or not we have added any assertions/declarations/definitions - * since the last checkSat/query (and therefore we're not responsible - * for an assignment). + * Whether or not we have added any assertions/declarations/definitions, + * or done push/pop, since the last checkSat/query, and therefore we're + * not responsible for models or proofs. */ bool d_problemExtended; -- cgit v1.2.3 From f72907de5dc6e3f2edec85b67b0ac987bb0f252a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 17 May 2013 16:53:21 -0400 Subject: Fix error reporting on use of (nonlinear) div,mod,/ symbols --- src/smt/smt_engine.cpp | 41 ++++++++++++++++++++--------------------- 1 file changed, 20 insertions(+), 21 deletions(-) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3cc6e7502..76d4c973f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -822,15 +822,6 @@ void SmtEngine::setLogicInternal() throw() { d_logic.lock(); - // may need to force uninterpreted functions to be on for non-linear - if(((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) || - d_logic.isTheoryEnabled(THEORY_BV)) && - !d_logic.isTheoryEnabled(THEORY_UF)){ - d_logic = d_logic.getUnlockedCopy(); - d_logic.enableTheory(THEORY_UF); - d_logic.lock(); - } - // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) { @@ -1314,6 +1305,11 @@ Node SmtEnginePrivate::expandBVDivByZero(TNode n) { Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL, num, den); Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } return node; } @@ -1364,13 +1360,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapmkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()), "partial real division", NodeManager::SKOLEM_EXACT_NAME); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } } TNode num = n[0], den = n[1]; Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); @@ -1382,13 +1379,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapmkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()), "partial integer division", NodeManager::SKOLEM_EXACT_NAME); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } } TNode num = n[0], den = n[1]; Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); @@ -1400,13 +1398,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapmkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()), "partial modulus", NodeManager::SKOLEM_EXACT_NAME); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } } TNode num = n[0], den = n[1]; Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); -- cgit v1.2.3