summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/antlr_input.cpp4
-rw-r--r--src/parser/antlr_input.h5
-rw-r--r--src/parser/input.h5
-rw-r--r--src/parser/parser.h5
-rw-r--r--src/parser/smt/smt.cpp12
-rw-r--r--src/parser/smt/smt.h4
-rw-r--r--src/parser/smt2/Smt2.g37
-rw-r--r--src/parser/smt2/smt2.cpp28
-rw-r--r--src/parser/smt2/smt2.h2
-rw-r--r--src/prop/prop_engine.cpp4
-rw-r--r--src/prop/prop_engine.h5
-rw-r--r--src/smt/smt_engine.cpp83
-rw-r--r--src/smt/smt_engine.h20
-rw-r--r--src/theory/logic_info.cpp51
-rw-r--r--src/theory/logic_info.h55
-rw-r--r--test/unit/prop/cnf_stream_black.h15
-rw-r--r--test/unit/theory/logic_info_white.h235
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
@@ -197,6 +197,11 @@ protected:
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 <code>ParserException</code> with the given message.
*/
void parseError(const std::string& msg)
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
@@ -167,6 +167,11 @@ protected:
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 <code>ParserException</code> with the given message.
*/
virtual void parseError(const std::string& msg)
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<const std::string, Smt::Logic, CVC4::StringHashFunction> 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<std::string>::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<CVC4::Type> 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
@@ -246,6 +246,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<bool>(true));
d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(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_map<TNode, Node, TNodeHas
}
}
-
void SmtEnginePrivate::removeITEs() {
+ d_smt.finalOptionsAreSet();
+
Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
// Remove all of the ITE occurrences and normalize
@@ -774,6 +792,7 @@ void SmtEnginePrivate::removeITEs() {
}
void SmtEnginePrivate::staticLearning() {
+ d_smt.finalOptionsAreSet();
TimerStat::CodeTimer staticLearningTimer(d_smt.d_staticLearningTime);
@@ -793,6 +812,7 @@ void SmtEnginePrivate::staticLearning() {
}
void SmtEnginePrivate::nonClausalSimplify() {
+ d_smt.finalOptionsAreSet();
TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime);
@@ -1072,6 +1092,8 @@ void SmtEnginePrivate::simplifyAssertions()
}
Result SmtEngine::check() {
+ Assert(d_fullyInited);
+
Trace("smt") << "SmtEngine::check()" << endl;
// Make sure the prop layer has all of the assertions
@@ -1124,11 +1146,13 @@ Result SmtEngine::check() {
}
Result SmtEngine::quickCheck() {
+ Assert(d_fullyInited);
Trace("smt") << "SMT quickCheck()" << endl;
return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK);
}
void SmtEnginePrivate::processAssertions() {
+ Assert(d_smt.d_fullyInited);
Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
@@ -1252,6 +1276,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
NodeManagerScope nms(d_nodeManager);
+ finalOptionsAreSet();
+
Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl;
if(d_queryMade && !Options::current()->incrementalSolving) {
@@ -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
@@ -185,6 +188,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
* is important because there are destruction ordering issues
@@ -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
@@ -138,6 +160,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.
*/
void enableTheory(theory::TheoryId theory);
@@ -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::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
d_theoryEngine->addTheory<theory::booleans::TheoryBool>(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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback