diff options
-rw-r--r-- | src/parser/cvc/Cvc.g | 7 | ||||
-rw-r--r-- | src/parser/smt/smt.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 89 | ||||
-rw-r--r-- | src/theory/logic_info.h | 17 | ||||
-rw-r--r-- | test/unit/theory/logic_info_white.h | 52 |
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() { |