summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/cvc/Cvc.g7
-rw-r--r--src/parser/smt/smt.h2
-rw-r--r--src/parser/smt2/smt2.h2
-rw-r--r--src/smt/smt_engine.cpp89
-rw-r--r--src/theory/logic_info.h17
-rw-r--r--test/unit/theory/logic_info_white.h52
6 files changed, 128 insertions, 41 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1a85f45c3..05fed15ea 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -610,7 +610,12 @@ mainCommand[CVC4::Command*& cmd]
| OPTION_TOK
( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
symbolicExpr[sexpr]
- { cmd = new SetOptionCommand(s, sexpr); }
+ { if(s == "logic") {
+ cmd = new SetBenchmarkLogicCommand(sexpr.getValue());
+ } else {
+ cmd = new SetOptionCommand(s, sexpr);
+ }
+ }
/* push / pop */
| PUSH_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PushCommand()); }
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index b82d3a01c..1d550cd7e 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -122,4 +122,4 @@ private:
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__SMT_INPUT_H */
+#endif /* __CVC4__PARSER__SMT_H */
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index c55a5e430..9bd85d7bc 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -96,4 +96,4 @@ private:
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__SMT2_INPUT_H */
+#endif /* __CVC4__PARSER__SMT2_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 90b9ac774..32e72f40a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -351,6 +351,11 @@ void SmtEngine::finalOptionsAreSet() {
return;
}
+ if(! d_logic.isLocked()) {
+ // ensure that our heuristics are properly set up
+ setLogicInternal();
+ }
+
// finish initalization, creat the prop engine, etc.
finishInit();
@@ -359,7 +364,7 @@ void SmtEngine::finalOptionsAreSet() {
"hasn't finished initializing!" );
d_fullyInited = true;
- d_logic.lock();
+ Assert(d_logic.isLocked());
d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
@@ -557,47 +562,55 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
}
// Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV
// and also use it in stop-only mode for QF_AUFLIA, QF_LRA and Quantifiers
+ // BUT use neither in ALL_SUPPORTED mode (since it doesn't yet work well
+ // with incrementality)
if(!options::decisionMode.wasSetByUser()) {
decision::DecisionMode decMode =
- //QF_BV
- (not d_logic.isQuantified() &&
- d_logic.isPure(THEORY_BV)
- ) ||
- //QF_AUFBV
- (not d_logic.isQuantified() &&
- d_logic.isTheoryEnabled(THEORY_ARRAY) &&
- d_logic.isTheoryEnabled(THEORY_UF) &&
- d_logic.isTheoryEnabled(THEORY_BV)
- ) ||
- //QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
- (not d_logic.isQuantified() &&
- d_logic.isTheoryEnabled(THEORY_ARRAY) &&
- d_logic.isTheoryEnabled(THEORY_UF) &&
- d_logic.isTheoryEnabled(THEORY_ARITH)
- ) ||
- // QF_LRA
- (not d_logic.isQuantified() &&
- d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed()
- ) ||
- // Quantifiers
- d_logic.isQuantified()
- ? decision::DECISION_STRATEGY_JUSTIFICATION
- : decision::DECISION_STRATEGY_INTERNAL;
+ // ALL_SUPPORTED
+ d_logic.hasEverything() ? decision::DECISION_STRATEGY_INTERNAL :
+ ( // QF_BV
+ (not d_logic.isQuantified() &&
+ d_logic.isPure(THEORY_BV)
+ ) ||
+ // QF_AUFBV
+ (not d_logic.isQuantified() &&
+ d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+ d_logic.isTheoryEnabled(THEORY_UF) &&
+ d_logic.isTheoryEnabled(THEORY_BV)
+ ) ||
+ // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
+ (not d_logic.isQuantified() &&
+ d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+ d_logic.isTheoryEnabled(THEORY_UF) &&
+ d_logic.isTheoryEnabled(THEORY_ARITH)
+ ) ||
+ // QF_LRA
+ (not d_logic.isQuantified() &&
+ d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed()
+ ) ||
+ // Quantifiers
+ d_logic.isQuantified()
+ ? decision::DECISION_STRATEGY_JUSTIFICATION
+ : decision::DECISION_STRATEGY_INTERNAL
+ );
bool stoponly =
- // QF_AUFLIA
- (not d_logic.isQuantified() &&
- d_logic.isTheoryEnabled(THEORY_ARRAY) &&
- d_logic.isTheoryEnabled(THEORY_UF) &&
- d_logic.isTheoryEnabled(THEORY_ARITH)
- ) ||
- // QF_LRA
- (not d_logic.isQuantified() &&
- d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed()
- ) ||
- // Quantifiers
- d_logic.isQuantified()
- ? true : false;
+ // ALL_SUPPORTED
+ d_logic.hasEverything() ? false :
+ ( // QF_AUFLIA
+ (not d_logic.isQuantified() &&
+ d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+ d_logic.isTheoryEnabled(THEORY_UF) &&
+ d_logic.isTheoryEnabled(THEORY_ARITH)
+ ) ||
+ // QF_LRA
+ (not d_logic.isQuantified() &&
+ d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed()
+ ) ||
+ // Quantifiers
+ d_logic.isQuantified()
+ ? true : false
+ );
Trace("smt") << "setting decision mode to " << decMode << std::endl;
options::decisionMode.set(decMode);
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index 7fa6e157f..36b71e931 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -108,6 +108,7 @@ public:
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 {
Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
@@ -120,6 +121,22 @@ public:
return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
}
+ /** Is this the all-inclusive logic? */
+ bool hasEverything() const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ LogicInfo everything;
+ everything.lock();
+ return *this == everything;
+ }
+
+ /** Is this the all-exclusive logic? (Here, that means propositional logic) */
+ bool hasNothing() const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ LogicInfo nothing("");
+ nothing.lock();
+ return *this == nothing;
+ }
+
/**
* Is this a pure logic (only one "true" background theory). Quantifiers
* can exist in such logics though; to test for quantifier-free purity,
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 069f99d0b..a2f61f5d2 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -36,6 +36,8 @@ public:
TS_ASSERT( !info.isSharingEnabled() );
TS_ASSERT( info.isPure( THEORY_BOOL ) );
TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( info.hasNothing() );
info = LogicInfo("AUFLIA");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -51,6 +53,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("AUFLIRA");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -66,6 +70,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("AUFNIRA");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -81,6 +87,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("LRA");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -97,6 +105,8 @@ public:
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_ABV");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -109,6 +119,8 @@ public:
TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_AUFBV");
TS_ASSERT( !info.isQuantified() );
@@ -120,6 +132,8 @@ public:
TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_AUFLIA");
TS_ASSERT( !info.isQuantified() );
@@ -135,6 +149,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_AX");
TS_ASSERT( !info.isQuantified() );
@@ -146,6 +162,8 @@ public:
TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_BV");
TS_ASSERT( !info.isQuantified() );
@@ -157,6 +175,8 @@ public:
TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_IDL");
TS_ASSERT( !info.isQuantified() );
@@ -172,6 +192,8 @@ public:
TS_ASSERT( info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_LIA");
TS_ASSERT( !info.isQuantified() );
@@ -187,6 +209,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_LRA");
TS_ASSERT( !info.isQuantified() );
@@ -202,6 +226,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_NIA");
TS_ASSERT( !info.isQuantified() );
@@ -217,6 +243,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_NRA");
TS_ASSERT( !info.isQuantified() );
@@ -232,6 +260,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_RDL");
TS_ASSERT( !info.isQuantified() );
@@ -247,6 +277,8 @@ public:
TS_ASSERT( info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UF");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -259,6 +291,8 @@ public:
TS_ASSERT( info.isPure( THEORY_UF ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFBV");
TS_ASSERT( !info.isQuantified() );
@@ -271,6 +305,8 @@ public:
TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFIDL");
TS_ASSERT( !info.isQuantified() );
@@ -286,6 +322,8 @@ public:
TS_ASSERT( info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFLIA");
TS_ASSERT( !info.isQuantified() );
@@ -301,6 +339,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFLRA");
TS_ASSERT( !info.isQuantified() );
@@ -315,6 +355,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFNRA");
TS_ASSERT( !info.isQuantified() );
@@ -330,6 +372,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("UFLRA");
TS_ASSERT( info.isQuantified() );
@@ -345,6 +389,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("UFNIA");
TS_ASSERT( info.isQuantified() );
@@ -360,6 +406,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_ALL_SUPPORTED");
TS_ASSERT( info.isLocked() );
@@ -376,6 +424,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("ALL_SUPPORTED");
TS_ASSERT( info.isLocked() );
@@ -392,6 +442,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
}
void testDefaultLogic() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback