From e568f34e1f4713c678336fbef1006e585128d466 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 7 Jun 2012 20:45:13 +0000 Subject: [PATCH] LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved. ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list. --- src/parser/antlr_input.cpp | 4 + src/parser/antlr_input.h | 5 + src/parser/input.h | 5 + src/parser/parser.h | 5 + src/parser/smt/smt.cpp | 12 ++ src/parser/smt/smt.h | 4 +- src/parser/smt2/Smt2.g | 37 +++-- src/parser/smt2/smt2.cpp | 28 ++++ src/parser/smt2/smt2.h | 2 + src/prop/prop_engine.cpp | 4 + src/prop/prop_engine.h | 5 + src/smt/smt_engine.cpp | 83 +++++++--- src/smt/smt_engine.h | 20 ++- src/theory/logic_info.cpp | 51 +++++- src/theory/logic_info.h | 55 ++++++- test/unit/prop/cnf_stream_black.h | 15 +- test/unit/theory/logic_info_white.h | 235 +++++++++++++++++++++++++--- 17 files changed, 490 insertions(+), 80 deletions(-) diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 67d873a48..52d98435e 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -270,6 +270,10 @@ void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { } } +void AntlrInput::warning(const std::string& message) { + Warning() << getInputStream()->getName() << ':' << d_lexer->getLine(d_lexer) << '.' << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; +} + void AntlrInput::parseError(const std::string& message) throw (ParserException, AssertionException) { Debug("parser") << "Throwing exception: " diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index bdf5fe59e..84b5099fb 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -196,6 +196,11 @@ protected: * setLexer(). */ pANTLR3_COMMON_TOKEN_STREAM getTokenStream(); + /** + * Issue a non-fatal warning to the user with file, line, and column info. + */ + void warning(const std::string& msg); + /** * Throws a ParserException with the given message. */ diff --git a/src/parser/input.h b/src/parser/input.h index 8fa51a095..92b039eda 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -166,6 +166,11 @@ protected: virtual Command* parseCommand() throw (ParserException, TypeCheckingException, AssertionException) = 0; + /** + * Issue a warning to the user, with source file, line, and column info. + */ + virtual void warning(const std::string& msg) = 0; + /** * Throws a ParserException with the given message. */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 405e397b8..a3ddba013 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -457,6 +457,11 @@ public: /** Parse and return the next expression. */ Expr nextExpression() throw(ParserException); + /** Issue a warning to the user. */ + inline void warning(const std::string& msg) { + d_input->warning(msg); + } + /** Raise a parse error with the given message. */ inline void parseError(const std::string& msg) throw(ParserException) { d_input->parseError(msg); diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index b9db8dace..c3b81655c 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -54,6 +54,8 @@ std::hash_map Smt::newL logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; + logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED; + logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED; return logicMap; } @@ -248,6 +250,16 @@ void Smt::setLogic(const std::string& name) { addTheory(THEORY_REALS); break; + case ALL_SUPPORTED: + /* fall through */ + case QF_ALL_SUPPORTED: + addTheory(THEORY_ARRAYS_EX); + addUf(); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_BITVECTORS); + break; + case AUFLIA: case AUFLIRA: case AUFNIRA: diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index 34ec624bc..d77808930 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -65,7 +65,9 @@ public: QF_UFNIRA, // nonstandard QF_UFNRA, UFLRA, - UFNIA + UFNIA, + QF_ALL_SUPPORTED, // nonstandard + ALL_SUPPORTED // nonstandard }; enum Theory { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 19f77ac87..d711ddab5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -191,6 +191,7 @@ command returns [CVC4::Command* cmd = NULL] DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl; + PARSER_STATE->checkThatLogicIsSet(); unsigned arity = AntlrInput::tokenToUnsigned(n); if(arity == 0) { Type type = PARSER_STATE->mkSort(name); @@ -204,6 +205,7 @@ command returns [CVC4::Command* cmd = NULL] DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK { + PARSER_STATE->checkThatLogicIsSet(); PARSER_STATE->pushScope(); for(std::vector::const_iterator i = names.begin(), iend = names.end(); @@ -224,6 +226,7 @@ command returns [CVC4::Command* cmd = NULL] LPAREN_TOK sortList[sorts] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] { Debug("parser") << "declare fun: '" << name << "'" << std::endl; + PARSER_STATE->checkThatLogicIsSet(); if( sorts.size() > 0 ) { t = EXPR_MANAGER->mkFunctionType(sorts, t); } @@ -235,6 +238,7 @@ command returns [CVC4::Command* cmd = NULL] sortSymbol[t,CHECK_DECLARED] { /* add variables to parser state before parsing term */ Debug("parser") << "define fun: '" << name << "'" << std::endl; + PARSER_STATE->checkThatLogicIsSet(); if( sortedVarNames.size() > 0 ) { std::vector sorts; sorts.reserve(sortedVarNames.size()); @@ -263,13 +267,9 @@ command returns [CVC4::Command* cmd = NULL] $cmd = new DefineFunctionCommand(name, func, terms, expr); } | /* value query */ - ( GET_VALUE_TOK - { if(PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("Strict compliance mode doesn't recognize \"eval\". Maybe you want (get-value...)?"); - } - } ) - LPAREN_TOK termList[terms,expr] RPAREN_TOK - { if(terms.size() == 1) { + GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK + { PARSER_STATE->checkThatLogicIsSet(); + if(terms.size() == 1) { $cmd = new GetValueCommand(terms[0]); } else { CommandSequence* seq = new CommandSequence(); @@ -284,24 +284,31 @@ command returns [CVC4::Command* cmd = NULL] } | /* get-assignment */ GET_ASSIGNMENT_TOK - { cmd = new GetAssignmentCommand; } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new GetAssignmentCommand; } | /* assertion */ ASSERT_TOK term[expr] - { cmd = new AssertCommand(expr); } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new AssertCommand(expr); } | /* checksat */ CHECKSAT_TOK - { cmd = new CheckSatCommand(MK_CONST(bool(true))); } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new CheckSatCommand(MK_CONST(bool(true))); } | /* get-assertions */ GET_ASSERTIONS_TOK - { cmd = new GetAssertionsCommand; } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new GetAssertionsCommand; } | /* get-proof */ GET_PROOF_TOK - { cmd = new GetProofCommand; } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new GetProofCommand; } | /* get-unsat-core */ GET_UNSAT_CORE_TOK - { UNSUPPORTED("unsat cores not yet supported"); } + { PARSER_STATE->checkThatLogicIsSet(); + UNSUPPORTED("unsat cores not yet supported"); } | /* push */ PUSH_TOK + { PARSER_STATE->checkThatLogicIsSet(); } ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n == 0) { @@ -323,6 +330,7 @@ command returns [CVC4::Command* cmd = NULL] } } ) | POP_TOK + { PARSER_STATE->checkThatLogicIsSet(); } ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n == 0) { @@ -348,7 +356,8 @@ command returns [CVC4::Command* cmd = NULL] /* CVC4-extended SMT-LIBv2 commands */ | extendedCommand[cmd] - { if(PARSER_STATE->strictModeEnabled()) { + { PARSER_STATE->checkThatLogicIsSet(); + if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3fa00baae..709ba087f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -17,6 +17,7 @@ **/ #include "expr/type.h" +#include "expr/command.h" #include "parser/parser.h" #include "parser/smt/smt.h" #include "parser/smt2/smt2.h" @@ -193,6 +194,16 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_REALS); break; + case Smt::ALL_SUPPORTED: + /* fall through */ + case Smt::QF_ALL_SUPPORTED: + addTheory(THEORY_ARRAYS); + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_BITVECTORS); + break; + case Smt::AUFLIA: case Smt::AUFLIRA: case Smt::AUFNIRA: @@ -211,5 +222,22 @@ void Smt2::setOption(const std::string& flag, const SExpr& sexpr) { // TODO: ??? } +void Smt2::checkThatLogicIsSet() { + if( ! logicIsSet() ) { + if( strictModeEnabled() ) { + parseError("set-logic must appear before this point."); + } else { + warning("No set-logic command was given before this point."); + warning("CVC4 will assume the non-standard ALL_SUPPORTED logic."); + warning("Consider setting a stricter logic for (likely) better performance."); + warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED)."); + + setLogic("ALL_SUPPORTED"); + + preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED")); + } + } +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index e9363b970..b71f63558 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -72,6 +72,8 @@ public: void setOption(const std::string& flag, const SExpr& sexpr); + void checkThatLogicIsSet(); + private: void addArithmeticOperators(); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5b71e5ec5..58270b4d0 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -247,6 +247,10 @@ void PropEngine::pop() { Debug("prop") << "pop()" << endl; } +unsigned PropEngine::getAssertionLevel() const { + return d_satSolver->getAssertionLevel(); +} + bool PropEngine::isRunning() const { return d_inCheckSat; } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 9e49cf3f1..603cdb0e6 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -245,6 +245,11 @@ public: */ void pop(); + /** + * Get the assertion level of the SAT solver. + */ + unsigned getAssertionLevel() const; + /** * Return true if we are currently searching (either in this or * another thread). diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8b3e6b742..ed28c23a3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -242,7 +242,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_assertionList(NULL), d_assignments(NULL), d_logic(), - d_logicIsSet(false), + d_fullyInited(false), d_problemExtended(false), d_queryMade(false), d_needPostsolve(false), @@ -328,6 +328,19 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : if(Options::current()->cumulativeMillisecondLimit != 0) { setTimeLimit(Options::current()->cumulativeMillisecondLimit, true); } +} + +void SmtEngine::finalOptionsAreSet() { + if(d_fullyInited) { + return; + } + + AlwaysAssert( d_propEngine->getAssertionLevel() == 0, + "The PropEngine has pushed but the SmtEngine " + "hasn't finished initializing!" ); + + d_fullyInited = true; + d_logic.lock(); d_propEngine->assertFormula(NodeManager::currentNM()->mkConst(true)); d_propEngine->assertFormula(NodeManager::currentNM()->mkConst(false).notNode()); @@ -401,15 +414,12 @@ SmtEngine::~SmtEngine() throw() { void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { NodeManagerScope nms(d_nodeManager); - if(d_logicIsSet) { - throw ModalException("logic already set"); - } - if(Dump.isOn("benchmark")) { Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString()); } - setLogicInternal(logic); + d_logic = logic; + setLogicInternal(); } void SmtEngine::setLogic(const std::string& s) throw(ModalException) { @@ -418,57 +428,63 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { setLogic(LogicInfo(s)); } -void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() { - d_logic = logic; +// This function is called when d_logic has just been changed. +// The LogicInfo isn't passed in explicitly, because that might +// tempt people in the code to use the (potentially unlocked) +// version that's passed in, leading to assert-fails in certain +// uses of the CVC4 library. +void SmtEngine::setLogicInternal() throw(AssertionException) { + Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run"); + + d_logic.lock(); // by default, symmetry breaker is on only for QF_UF if(! Options::current()->ufSymmetryBreakerSetByUser) { - bool qf_uf = logic.isPure(theory::THEORY_UF) && !logic.isQuantified(); + bool qf_uf = d_logic.isPure(theory::THEORY_UF) && !d_logic.isQuantified(); Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl; NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf; } // by default, nonclausal simplification is off for QF_SAT if(! Options::current()->simplificationModeSetByUser) { - bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified(); - Trace("smt") << "setting simplification mode to <" << logic.getLogicString() << "> " << (!qf_sat) << std::endl; + bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified(); + Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << std::endl; NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH); } // If in arrays, set the UF handler to arrays - if(logic.isPure(theory::THEORY_ARRAY) && !logic.isQuantified()) { + if(d_logic.isPure(theory::THEORY_ARRAY) && !d_logic.isQuantified()) { theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY); } else { theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF); } // Turn on ite simplification for QF_LIA and QF_AUFBV if(! Options::current()->doITESimpSetByUser) { - bool iteSimp = !logic.isQuantified() && - ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() && !logic.areRealsUsed()) || - (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV))); + bool iteSimp = !d_logic.isQuantified() && + ((d_logic.isPure(theory::THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areRealsUsed()) || + (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_UF) && d_logic.isTheoryEnabled(theory::THEORY_BV))); Trace("smt") << "setting ite simplification to " << iteSimp << std::endl; NodeManager::currentNM()->getOptions()->doITESimp = iteSimp; } // Turn on multiple-pass non-clausal simplification for QF_AUFBV if(! Options::current()->repeatSimpSetByUser) { - bool repeatSimp = !logic.isQuantified() && - (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV)); + bool repeatSimp = !d_logic.isQuantified() && + (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_UF) && d_logic.isTheoryEnabled(theory::THEORY_BV)); Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl; NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp; } // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) { - bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified(); + bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified(); bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving; Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp; } // Turn on arith rewrite equalities only for pure arithmetic if(! Options::current()->arithRewriteEqSetByUser) { - bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified(); + bool arithRewriteEq = d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified(); Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl; NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq; } - } void SmtEngine::setInfo(const std::string& key, const SExpr& value) @@ -496,7 +512,8 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string"); } NodeManagerScope nms(d_nodeManager); - setLogicInternal(value.getValue()); + d_logic = value.getValue(); + setLogicInternal(); return; } } @@ -592,7 +609,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) } else { // The following options can only be set at the beginning; we throw // a ModalException if someone tries. - if(d_logicIsSet) { + if(d_logic.isLocked()) { throw ModalException("logic already set; cannot set options"); } @@ -761,8 +778,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapincrementalSolving) { @@ -1313,6 +1339,8 @@ Result SmtEngine::query(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); + Trace("smt") << "SMT query(" << e << ")" << endl; if(d_queryMade && !Options::current()->incrementalSolving) { @@ -1366,6 +1394,7 @@ Result SmtEngine::query(const BoolExpr& e) { Result SmtEngine::assertFormula(const BoolExpr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl; ensureBoolean(e); if(d_assertionList != NULL) { @@ -1378,6 +1407,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) { Expr SmtEngine::simplify(const Expr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); if( Options::current()->typeChecking ) { e.getType(true);// ensure expr is type-checked at this point } @@ -1435,6 +1465,7 @@ Expr SmtEngine::getValue(const Expr& e) bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); Type type = e.getType(Options::current()->typeChecking); // must be Boolean CheckArgument( type.isBoolean(), e, @@ -1463,6 +1494,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Trace("smt") << "SMT getAssignment()" << endl; NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetAssignmentCommand(); } @@ -1519,6 +1551,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { Trace("smt") << "SMT getProof()" << endl; NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetProofCommand(); } @@ -1566,6 +1599,7 @@ size_t SmtEngine::getStackLevel() const { void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); Trace("smt") << "SMT push()" << endl; d_private->processAssertions(); if(Dump.isOn("benchmark")) { @@ -1589,6 +1623,7 @@ void SmtEngine::push() { void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); Trace("smt") << "SMT pop()" << endl; if(Dump.isOn("benchmark")) { Dump("benchmark") << PopCommand(); @@ -1624,6 +1659,7 @@ void SmtEngine::pop() { } void SmtEngine::internalPush() { + Assert(d_fullyInited); Trace("smt") << "SmtEngine::internalPush()" << endl; if(Options::current()->incrementalSolving) { d_private->processAssertions(); @@ -1634,6 +1670,7 @@ void SmtEngine::internalPush() { } void SmtEngine::internalPop() { + Assert(d_fullyInited); Trace("smt") << "SmtEngine::internalPop()" << endl; if(Options::current()->incrementalSolving) { d_propEngine->pop(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f07815e2e..4c0fed74c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -135,9 +135,12 @@ class CVC4_PUBLIC SmtEngine { LogicInfo d_logic; /** - * Whether the logic has been set yet. + * Whether or not this SmtEngine has been fully initialized (that is, + * the ). This post-construction initialization is automatically + * triggered by the use of the SmtEngine; e.g. when setLogic() is + * called, or the first assertion is made, etc. */ - bool d_logicIsSet; + bool d_fullyInited; /** * Whether or not we have added any assertions/declarations/definitions @@ -184,6 +187,14 @@ class CVC4_PUBLIC SmtEngine { */ smt::SmtEnginePrivate* d_private; + /** + * This is something of an "init" procedure, but is idempotent; call + * as often as you like. Should be called whenever the final options + * and logic for the problem are set (at least, those options that are + * not permitted to change after assertions and queries are made). + */ + void finalOptionsAreSet(); + /** * This is called by the destructor, just before destroying the * PropEngine, TheoryEngine, and DecisionEngine (in that order). It @@ -216,9 +227,10 @@ class CVC4_PUBLIC SmtEngine { void internalPop(); /** - * Internally handle the setting of a logic. + * Internally handle the setting of a logic. This function should always + * be called when d_logic is updated. */ - void setLogicInternal(const LogicInfo& logic) throw(); + void setLogicInternal() throw(AssertionException); friend class ::CVC4::smt::SmtEnginePrivate; diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index ba7119071..d0c1e4b6a 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -37,7 +37,9 @@ LogicInfo::LogicInfo() : d_sharingTheories(0), d_integers(true), d_reals(true), - d_linear(false) { + d_linear(false), + d_differenceLogic(false), + d_locked(false) { for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { d_theories[id] = false;// ensure it's cleared @@ -51,11 +53,16 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) : d_sharingTheories(0), d_integers(false), d_reals(false), - d_linear(false) { + d_linear(false), + d_differenceLogic(false), + d_locked(false) { + setLogicString(logicString); + lock(); } std::string LogicInfo::getLogicString() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { size_t seen = 0; // make sure we support all the active theories @@ -108,6 +115,7 @@ std::string LogicInfo::getLogicString() const { } void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { d_theories[id] = false;// ensure it's cleared } @@ -124,6 +132,16 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc if(!strcmp(p, "QF_SAT") || *p == '\0') { // propositional logic only; we're done. p += 6; + } else if(!strcmp(p, "QF_ALL_SUPPORTED")) { + // the "all theories included" logic, no quantifiers + enableEverything(); + disableQuantifiers(); + p += 16; + } else if(!strcmp(p, "ALL_SUPPORTED")) { + // the "all theories included" logic, with quantifiers + enableEverything(); + enableQuantifiers(); + p += 13; } else { if(!strncmp(p, "QF_", 3)) { disableQuantifiers(); @@ -211,7 +229,18 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc d_logicString = logicString; } +void LogicInfo::enableEverything() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + *this = LogicInfo(); +} + +void LogicInfo::disableEverything() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + *this = LogicInfo(""); +} + void LogicInfo::enableTheory(theory::TheoryId theory) { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); if(!d_theories[theory]) { if(isTrueTheory(theory)) { ++d_sharingTheories; @@ -222,6 +251,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) { } void LogicInfo::disableTheory(theory::TheoryId theory) { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); if(d_theories[theory]) { if(isTrueTheory(theory)) { Assert(d_sharingTheories > 0); @@ -237,12 +267,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } void LogicInfo::enableIntegers() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_integers = true; } void LogicInfo::disableIntegers() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_integers = false; if(!d_reals) { @@ -251,12 +283,14 @@ void LogicInfo::disableIntegers() { } void LogicInfo::enableReals() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_reals = true; } void LogicInfo::disableReals() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_reals = false; if(!d_integers) { @@ -265,21 +299,34 @@ void LogicInfo::disableReals() { } void LogicInfo::arithOnlyDifference() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = true; } void LogicInfo::arithOnlyLinear() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = false; } void LogicInfo::arithNonLinear() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = false; d_differenceLogic = false; } +LogicInfo LogicInfo::getUnlockedCopy() const { + if(d_locked) { + LogicInfo info = *this; + info.d_locked = false; + return info; + } else { + return *this; + } +} + }/* CVC4 namespace */ diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index d5b8be58d..33a059bb9 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -54,6 +54,8 @@ class LogicInfo { bool d_linear; /**< linear-only arithmetic in this logic? */ bool d_differenceLogic; /**< difference-only arithmetic in this logic? */ + bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */ + /** * Returns true iff this is a "true" theory (one that must be worried * about for sharing @@ -95,12 +97,19 @@ public: std::string getLogicString() const; /** Is sharing enabled for this logic? */ - bool isSharingEnabled() const { return d_sharingTheories > 1; } + bool isSharingEnabled() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_sharingTheories > 1; + } /** Is the given theory module active in this logic? */ - bool isTheoryEnabled(theory::TheoryId theory) const { return d_theories[theory]; } + bool isTheoryEnabled(theory::TheoryId theory) const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_theories[theory]; + } /** Is this a quantified logic? */ bool isQuantified() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES); } @@ -110,6 +119,7 @@ public: * use "isPure(theory) && !isQuantified()". */ bool isPure(theory::TheoryId theory) const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); // the third and fourth conjucts are really just to rule out the misleading // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA return isTheoryEnabled(theory) && !isSharingEnabled() && @@ -120,13 +130,25 @@ public: // these are for arithmetic /** Are integers in this logic? */ - bool areIntegersUsed() const { return d_integers; } + bool areIntegersUsed() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_integers; + } /** Are reals in this logic? */ - bool areRealsUsed() const { return d_reals; } + bool areRealsUsed() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_reals; + } /** Does this logic only linear arithmetic? */ - bool isLinear() const { return d_linear || d_differenceLogic; } + bool isLinear() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_linear || d_differenceLogic; + } /** Does this logic only permit difference reasoning? (implies linear) */ - bool isDifferenceLogic() const { return d_differenceLogic; } + bool isDifferenceLogic() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_differenceLogic; + } // MUTATORS @@ -137,6 +159,18 @@ public: */ void setLogicString(std::string logicString) throw(IllegalArgumentException); + /** + * Enable all functionality. All theories, plus quantifiers, will be + * enabled. + */ + void enableEverything(); + + /** + * Disable all functionality. The result will be a LogicInfo with + * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT"). + */ + void disableEverything(); + /** * Enable the given theory module. */ @@ -181,6 +215,15 @@ public: /** Permit nonlinear arithmetic in this logic. */ void arithNonLinear(); + // LOCKING FUNCTIONALITY + + /** Lock this LogicInfo, disabling further mutation and allowing queries */ + void lock() { d_locked = true; } + /** Check whether this LogicInfo is locked, disallowing further mutation */ + bool isLocked() const { return d_locked; } + /** Get a copy of this LogicInfo that is identical, but unlocked */ + LogicInfo getUnlockedCopy() const; + };/* class LogicInfo */ }/* CVC4 namespace */ diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index c24104acc..de0510582 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -146,6 +146,7 @@ class CnfStreamBlack : public CxxTest::TestSuite { NodeManagerScope nms(d_nodeManager); d_satSolver = new FakeSatSolver(); d_logicInfo = new LogicInfo(); + d_logicInfo->lock(); d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo); d_theoryEngine->addTheory(theory::THEORY_BUILTIN); d_theoryEngine->addTheory(theory::THEORY_BOOL); @@ -200,9 +201,15 @@ public: TS_ASSERT( d_satSolver->addClauseCalled() ); } + void testTrue() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -255,12 +262,6 @@ public: TS_ASSERT( d_satSolver->addClauseCalled() ); } - void testTrue() { - NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); - } - void testVar() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index 8bb3b52df..70ebdc7f8 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -32,11 +32,12 @@ public: void testSmtlibLogics() { LogicInfo info("QF_SAT"); + TS_ASSERT( info.isLocked() ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( info.isPure( THEORY_BOOL ) ); TS_ASSERT( !info.isQuantified() ); - info.setLogicString("AUFLIA"); + info = LogicInfo("AUFLIA"); TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); @@ -44,13 +45,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( !info.areRealsUsed() ); - info.setLogicString("AUFLIRA"); + info = LogicInfo("AUFLIRA"); TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); @@ -58,13 +60,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areRealsUsed() ); - info.setLogicString("AUFNIRA"); + info = LogicInfo("AUFNIRA"); TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); @@ -72,13 +75,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( !info.isLinear() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areRealsUsed() ); - info.setLogicString("LRA"); + info = LogicInfo("LRA"); TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); @@ -87,13 +91,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( !info.areIntegersUsed() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areRealsUsed() ); - info.setLogicString("QF_ABV"); + info = LogicInfo("QF_ABV"); TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); @@ -102,9 +107,10 @@ public: TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARRAY ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - info.setLogicString("QF_AUFBV"); + info = LogicInfo("QF_AUFBV"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -112,9 +118,10 @@ public: TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARRAY ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - info.setLogicString("QF_AUFLIA"); + info = LogicInfo("QF_AUFLIA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -122,13 +129,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARRAY ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( !info.areRealsUsed() ); - info.setLogicString("QF_AX"); + info = LogicInfo("QF_AX"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -136,9 +144,10 @@ public: TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARRAY ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - info.setLogicString("QF_BV"); + info = LogicInfo("QF_BV"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -146,9 +155,10 @@ public: TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARRAY ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - info.setLogicString("QF_IDL"); + info = LogicInfo("QF_IDL"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -156,13 +166,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( info.isDifferenceLogic() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.areRealsUsed() ); - info.setLogicString("QF_LIA"); + info = LogicInfo("QF_LIA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -170,13 +181,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.areRealsUsed() ); - info.setLogicString("QF_LRA"); + info = LogicInfo("QF_LRA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -185,12 +197,13 @@ public: TS_ASSERT( info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( !info.areIntegersUsed() ); TS_ASSERT( info.areRealsUsed() ); - info.setLogicString("QF_NIA"); + info = LogicInfo("QF_NIA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -199,12 +212,13 @@ public: TS_ASSERT( info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( !info.isLinear() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.areRealsUsed() ); - info.setLogicString("QF_NRA"); + info = LogicInfo("QF_NRA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -212,13 +226,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( !info.isLinear() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( !info.areIntegersUsed() ); TS_ASSERT( info.areRealsUsed() ); - info.setLogicString("QF_RDL"); + info = LogicInfo("QF_RDL"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -226,13 +241,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( info.isDifferenceLogic() ); TS_ASSERT( !info.areIntegersUsed() ); TS_ASSERT( info.areRealsUsed() ); - info.setLogicString("QF_UF"); + info = LogicInfo("QF_UF"); TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); @@ -244,7 +260,7 @@ public: TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - info.setLogicString("QF_UFBV"); + info = LogicInfo("QF_UFBV"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -253,9 +269,10 @@ public: TS_ASSERT( !info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - info.setLogicString("QF_UFIDL"); + info = LogicInfo("QF_UFIDL"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -263,13 +280,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( info.isDifferenceLogic() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.areRealsUsed() ); - info.setLogicString("QF_UFLIA"); + info = LogicInfo("QF_UFLIA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -277,13 +295,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.areRealsUsed() ); - info.setLogicString("QF_UFLRA"); + info = LogicInfo("QF_UFLRA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -297,7 +316,7 @@ public: TS_ASSERT( !info.areIntegersUsed() ); TS_ASSERT( info.areRealsUsed() ); - info.setLogicString("QF_UFNRA"); + info = LogicInfo("QF_UFNRA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -305,13 +324,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( !info.isLinear() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( !info.areIntegersUsed() ); TS_ASSERT( info.areRealsUsed() ); - info.setLogicString("UFLRA"); + info = LogicInfo("UFLRA"); TS_ASSERT( info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -319,13 +339,14 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isLinear() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( !info.areIntegersUsed() ); TS_ASSERT( info.areRealsUsed() ); - info.setLogicString("UFNIA"); + info = LogicInfo("UFNIA"); TS_ASSERT( info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); @@ -333,15 +354,78 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( !info.isLinear() ); TS_ASSERT( !info.isDifferenceLogic() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( !info.areRealsUsed() ); + + info = LogicInfo("QF_ALL_SUPPORTED"); + TS_ASSERT( info.isLocked() ); + TS_ASSERT( !info.isPure( THEORY_BOOL ) ); + TS_ASSERT( info.isSharingEnabled() ); + TS_ASSERT( !info.isQuantified() ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); + TS_ASSERT( !info.isLinear() ); + TS_ASSERT( info.areIntegersUsed() ); + TS_ASSERT( !info.isDifferenceLogic() ); + TS_ASSERT( info.areRealsUsed() ); + + info = LogicInfo("ALL_SUPPORTED"); + TS_ASSERT( info.isLocked() ); + TS_ASSERT( !info.isPure( THEORY_BOOL ) ); + TS_ASSERT( info.isSharingEnabled() ); + TS_ASSERT( info.isQuantified() ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); + TS_ASSERT( !info.isLinear() ); + TS_ASSERT( info.areIntegersUsed() ); + TS_ASSERT( !info.isDifferenceLogic() ); + TS_ASSERT( info.areRealsUsed() ); } void testDefaultLogic() { LogicInfo info; + TS_ASSERT( !info.isLocked() ); + +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( info.getLogicString(), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.isQuantified(), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::AssertionException ); + TS_ASSERT_THROWS( ! info.isLinear(), CVC4::AssertionException ); +#endif /* CVC4_ASSERTIONS */ + + info.lock(); + TS_ASSERT( info.isLocked() ); TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTNIRA" ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isTheoryEnabled( THEORY_BUILTIN ) ); @@ -367,21 +451,126 @@ public: TS_ASSERT( info.areRealsUsed() ); TS_ASSERT( ! info.isLinear() ); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.disableIntegers(), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.enableIntegers(), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.disableReals(), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::AssertionException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::AssertionException ); +#endif /* CVC4_ASSERTIONS */ + + info = info.getUnlockedCopy(); + TS_ASSERT( !info.isLocked() ); info.arithOnlyLinear(); info.disableIntegers(); + info.lock(); TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLRA" ); + + info = info.getUnlockedCopy(); + TS_ASSERT( !info.isLocked() ); info.disableQuantifiers(); + info.lock(); TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVDTLRA" ); + + info = info.getUnlockedCopy(); + TS_ASSERT( !info.isLocked() ); info.disableTheory(THEORY_BV); info.disableTheory(THEORY_DATATYPES); info.enableIntegers(); info.disableReals(); + info.lock(); TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFLIA" ); + + info = info.getUnlockedCopy(); + TS_ASSERT( !info.isLocked() ); info.disableTheory(THEORY_ARITH); info.disableTheory(THEORY_UF); + info.lock(); TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" ); TS_ASSERT( info.isPure( THEORY_ARRAY ) ); TS_ASSERT( ! info.isQuantified() ); + + // check all-excluded logic + info = info.getUnlockedCopy(); + TS_ASSERT( !info.isLocked() ); + info.disableEverything(); + info.lock(); + TS_ASSERT( info.isLocked() ); + TS_ASSERT( !info.isSharingEnabled() ); + TS_ASSERT( !info.isQuantified() ); + TS_ASSERT( info.isPure( THEORY_BOOL ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); + TS_ASSERT( !info.isLinear() ); + TS_ASSERT( !info.areIntegersUsed() ); + TS_ASSERT( !info.isDifferenceLogic() ); + TS_ASSERT( !info.areRealsUsed() ); + + // check copy is unchanged + info = info.getUnlockedCopy(); + TS_ASSERT( !info.isLocked() ); + info.lock(); + TS_ASSERT( info.isLocked() ); + TS_ASSERT( !info.isSharingEnabled() ); + TS_ASSERT( !info.isQuantified() ); + TS_ASSERT( info.isPure( THEORY_BOOL ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); + TS_ASSERT( !info.isLinear() ); + TS_ASSERT( !info.areIntegersUsed() ); + TS_ASSERT( !info.isDifferenceLogic() ); + TS_ASSERT( !info.areRealsUsed() ); + + // check all-included logic + info = info.getUnlockedCopy(); + TS_ASSERT( !info.isLocked() ); + info.enableEverything(); + info.lock(); + TS_ASSERT( info.isLocked() ); + TS_ASSERT( !info.isPure( THEORY_BOOL ) ); + TS_ASSERT( info.isSharingEnabled() ); + TS_ASSERT( info.isQuantified() ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); + TS_ASSERT( !info.isLinear() ); + TS_ASSERT( info.areIntegersUsed() ); + TS_ASSERT( !info.isDifferenceLogic() ); + TS_ASSERT( info.areRealsUsed() ); + + // check copy is unchanged + info = info.getUnlockedCopy(); + TS_ASSERT( !info.isLocked() ); + info.lock(); + TS_ASSERT( info.isLocked() ); + TS_ASSERT( !info.isPure( THEORY_BOOL ) ); + TS_ASSERT( info.isSharingEnabled() ); + TS_ASSERT( info.isQuantified() ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); + TS_ASSERT( !info.isLinear() ); + TS_ASSERT( info.areIntegersUsed() ); + TS_ASSERT( !info.isDifferenceLogic() ); + TS_ASSERT( info.areRealsUsed() ); } };/* class LogicInfoWhite */ -- 2.30.2