diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-29 13:03:03 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-29 13:03:03 -0400 |
commit | 79052f8209cb871e6159d148b0586c562948a2fd (patch) | |
tree | d2c7ba8c1688addfaeb284eebf85b922a8eb91b6 | |
parent | fbc81b67ac1cfeb3afe37f3299180177faaa1ca6 (diff) | |
parent | e6dc2c46fced4d8121d6d7bdd739d977f32d0462 (diff) |
Merge branch '1.2.x'
-rw-r--r-- | NEWS | 2 | ||||
-rw-r--r-- | src/expr/command.cpp | 3 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 139 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 3 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 16 | ||||
-rw-r--r-- | src/theory/logic_info.h | 4 | ||||
-rw-r--r-- | test/unit/theory/logic_info_white.h | 16 |
7 files changed, 51 insertions, 132 deletions
@@ -6,7 +6,7 @@ Changes since 1.2 * We no longer permit model or proof generation if there's been an intervening push/pop. * Increased compliance to SMT-LIBv2, numerous bugs and usability issues - resolved + resolved. Changes since 1.1 ================= diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 36336a959..423bf3234 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1118,7 +1118,8 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { smtEngine->setInfo(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); + // As per SMT-LIB spec, silently accept unknown set-info keys + d_commandStatus = CommandSuccess::instance(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a7f7796cd..c042c3992 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -36,7 +36,6 @@ void Smt2::addArithmeticOperators() { addOperator(kind::MINUS); addOperator(kind::UMINUS); addOperator(kind::MULT); - addOperator(kind::DIVISION); addOperator(kind::LT); addOperator(kind::LEQ); addOperator(kind::GT); @@ -106,16 +105,20 @@ void Smt2::addTheory(Theory theory) { case THEORY_REALS_INTS: defineType("Real", getExprManager()->realType()); - // falling-through on purpose, to add Ints part of RealsInts + addOperator(kind::DIVISION); + // falling through on purpose, to add Ints part of Reals_Ints case THEORY_INTS: defineType("Int", getExprManager()->integerType()); addArithmeticOperators(); + addOperator(kind::INTS_DIVISION); + addOperator(kind::INTS_MODULUS); break; case THEORY_REALS: defineType("Real", getExprManager()->realType()); addArithmeticOperators(); + addOperator(kind::DIVISION); break; case THEORY_BITVECTORS: @@ -138,135 +141,35 @@ bool Smt2::logicIsSet() { void Smt2::setLogic(const std::string& name) { d_logicSet = true; - d_logic = Smt1::toLogic(name); + d_logic = name; // Core theory belongs to every logic addTheory(THEORY_CORE); - switch(d_logic) { - case Smt1::QF_SAT: - /* No extra symbols necessary */ - break; - - case Smt1::QF_AX: - addTheory(THEORY_ARRAYS); - break; - - case Smt1::QF_IDL: - case Smt1::QF_LIA: - case Smt1::QF_NIA: - addTheory(THEORY_INTS); - break; - - case Smt1::QF_RDL: - case Smt1::QF_LRA: - case Smt1::QF_NRA: - addTheory(THEORY_REALS); - break; - - case Smt1::QF_UF: - addOperator(kind::APPLY_UF); - break; - - case Smt1::QF_UFIDL: - case Smt1::QF_UFLIA: - case Smt1::QF_UFNIA:// nonstandard logic - addTheory(THEORY_INTS); - addOperator(kind::APPLY_UF); - break; - - case Smt1::QF_UFLRA: - case Smt1::QF_UFNRA: - addTheory(THEORY_REALS); - addOperator(kind::APPLY_UF); - break; - - case Smt1::QF_UFLIRA:// nonstandard logic - case Smt1::QF_UFNIRA:// nonstandard logic - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - break; - - case Smt1::QF_BV: - addTheory(THEORY_BITVECTORS); - break; - - case Smt1::QF_ABV: - addTheory(THEORY_ARRAYS); - addTheory(THEORY_BITVECTORS); - break; - - case Smt1::QF_UFBV: - addOperator(kind::APPLY_UF); - addTheory(THEORY_BITVECTORS); - break; - - case Smt1::QF_AUFBV: + if(d_logic.isTheoryEnabled(theory::THEORY_UF)) { addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS); - addTheory(THEORY_BITVECTORS); - break; - - case Smt1::QF_AUFBVLIA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS); - addTheory(THEORY_BITVECTORS); - addTheory(THEORY_INTS); - break; + } - case Smt1::QF_AUFBVLRA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS); - addTheory(THEORY_BITVECTORS); - addTheory(THEORY_REALS); - break; + if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) { + if(d_logic.areIntegersUsed()) { + addTheory(THEORY_INTS); + } - case Smt1::QF_AUFLIA: - addTheory(THEORY_ARRAYS); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - break; + if(d_logic.areRealsUsed()) { + addTheory(THEORY_REALS); + } + } - case Smt1::QF_AUFLIRA: + if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) { addTheory(THEORY_ARRAYS); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - break; + } - case Smt1::ALL_SUPPORTED: - addTheory(THEORY_QUANTIFIERS); - /* fall through */ - case Smt1::QF_ALL_SUPPORTED: - addTheory(THEORY_ARRAYS); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); + if(d_logic.isTheoryEnabled(theory::THEORY_BV)) { addTheory(THEORY_BITVECTORS); - break; + } - case Smt1::AUFLIA: - case Smt1::AUFLIRA: - case Smt1::AUFNIRA: - case Smt1::LRA: - case Smt1::UFNIA: - case Smt1::UFNIRA: - case Smt1::UFLRA: - if(d_logic != Smt1::AUFLIA && d_logic != Smt1::UFNIA) { - addTheory(THEORY_REALS); - } - if(d_logic != Smt1::LRA) { - addOperator(kind::APPLY_UF); - if(d_logic != Smt1::UFLRA) { - addTheory(THEORY_INTS); - if(d_logic != Smt1::UFNIA && d_logic != Smt1::UFNIRA) { - addTheory(THEORY_ARRAYS); - } - } - } + if(d_logic.isQuantified()) { addTheory(THEORY_QUANTIFIERS); - break; } }/* Smt2::setLogic() */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 5762ff5f9..7a464c773 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -21,6 +21,7 @@ #include "parser/parser.h" #include "parser/smt1/smt1.h" +#include "theory/logic_info.h" #include "util/abstract_value.h" #include <sstream> @@ -47,7 +48,7 @@ public: private: bool d_logicSet; - Smt1::Logic d_logic; + LogicInfo d_logic; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index a2fe96271..fc2574036 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -241,11 +241,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::MULT: case kind::MINUS: case kind::UMINUS: - case kind::DIVISION: case kind::LT: case kind::LEQ: case kind::GT: - case kind::GEQ: out << smtKindString(k) << " "; break; + case kind::GEQ: + case kind::DIVISION: + case kind::DIVISION_TOTAL: + case kind::INTS_DIVISION: + case kind::INTS_DIVISION_TOTAL: + case kind::INTS_MODULUS: + case kind::INTS_MODULUS_TOTAL: out << smtKindString(k) << " "; break; // arrays theory case kind::SELECT: @@ -421,11 +426,16 @@ static string smtKindString(Kind k) throw() { case kind::MULT: return "*"; case kind::MINUS: return "-"; case kind::UMINUS: return "-"; - case kind::DIVISION: return "/"; case kind::LT: return "<"; case kind::LEQ: return "<="; case kind::GT: return ">"; case kind::GEQ: return ">="; + case kind::DIVISION: + case kind::DIVISION_TOTAL: return "/"; + case kind::INTS_DIVISION: + case kind::INTS_DIVISION_TOTAL: return "div"; + case kind::INTS_MODULUS: + case kind::INTS_MODULUS_TOTAL: return "mod"; // arrays theory case kind::SELECT: return "select"; diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index c7b5c58f9..2448898c0 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -155,21 +155,25 @@ public: /** Are integers in this logic? */ bool areIntegersUsed() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used"); return d_integers; } /** Are reals in this logic? */ bool areRealsUsed() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used"); return d_reals; } /** Does this logic only linear arithmetic? */ bool isLinear() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear"); return d_linear || d_differenceLogic; } /** Does this logic only permit difference reasoning? (implies linear) */ bool isDifferenceLogic() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); return d_differenceLogic; } diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index a0d415296..39d8aadb1 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -555,10 +555,10 @@ public: 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() ); + TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException ); // check copy is unchanged info = info.getUnlockedCopy(); @@ -574,10 +574,10 @@ public: 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() ); + TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException ); // check all-included logic info = info.getUnlockedCopy(); |