diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-23 23:08:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-23 23:08:03 +0000 |
commit | 5a20a19a30929ad58a9e64a9d8d1f877f3a07ae6 (patch) | |
tree | 2a800e6b1d6773e1c844767f5daed51148b5660b /src/theory | |
parent | 1f2590541aa60f4b62b7c96659362ee4431d2d63 (diff) |
Added ability to set a "cvc4-specific logic" in standards-compliant
SMT-LIBv1 and SMT-LIBv2 input:
In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance:
(benchmark actually_a_sat_benchmark_but_looks_like_uf
:logic QF_UF
:cvc4_logic { QF_SAT }
[...]
In SMT-LIBv2, you use a set-info; for instance:
(set-logic QF_UF)
(set-info :cvc4-logic "QF_SAT")
[...]
Right now, the only thing this does is disable the symmetry breaker for
benchmarks like the above ones.
As part of this work, TheoryEngine::setLogic() was removed (the logic field there
wasn't actually used anywhere, its need disappeared when
Theory::setUninterpretedSortOwner() was provided).
Also, Theory::d_uninterpretedSortOwner got a name change to
Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory
class. This represents a breakage of our separation goals for CVC4, since it
means that two SmtEngines cannot be created separately to solve a QF_AX and
QF_UF problem. A bug report is pending.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory.h | 9 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 3 |
4 files changed, 7 insertions, 14 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index ff2feb121..fa2eed861 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -27,7 +27,7 @@ namespace CVC4 { namespace theory { /** Default value for the uninterpreted sorts is the UF theory */ -TheoryId Theory::d_uninterpretedSortOwner = THEORY_UF; +TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF; std::ostream& operator<<(std::ostream& os, Theory::Effort level){ switch(level){ diff --git a/src/theory/theory.h b/src/theory/theory.h index cf986a1f2..fade1e3c7 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -208,7 +208,7 @@ protected: /** * The theory that owns the uninterpreted sort. */ - static TheoryId d_uninterpretedSortOwner; + static TheoryId s_uninterpretedSortOwner; public: @@ -216,6 +216,7 @@ public: * Return the ID of the theory responsible for the given type. */ static inline TheoryId theoryOf(TypeNode typeNode) { + Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl; TheoryId id; if (typeNode.getKind() == kind::TYPE_CONSTANT) { id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>()); @@ -223,7 +224,8 @@ public: id = kindToTheoryId(typeNode.getKind()); } if (id == THEORY_BUILTIN) { - return d_uninterpretedSortOwner; + Trace("theory") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl; + return s_uninterpretedSortOwner; } return id; } @@ -233,6 +235,7 @@ public: * Returns the ID of the theory responsible for the given node. */ static inline TheoryId theoryOf(TNode node) { + Trace("theory") << "theoryOf(" << node << ")" << std::endl; // Constants, variables, 0-ary constructors if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) { return theoryOf(node.getType()); @@ -249,7 +252,7 @@ public: * Set the owner of the uninterpreted sort. */ static void setUninterpretedSortOwner(TheoryId theory) { - d_uninterpretedSortOwner = theory; + s_uninterpretedSortOwner = theory; } /** diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c4a8dc591..3486d9075 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -52,7 +52,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_hasShutDown(false), d_incomplete(context, false), d_sharedAssertions(context), - d_logic(""), d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_decisionRequests(context), @@ -78,12 +77,6 @@ TheoryEngine::~TheoryEngine() { } } -void TheoryEngine::setLogic(std::string logic) { - Assert(d_logic.empty()); - // Set the logic - d_logic = logic; -} - void TheoryEngine::preRegister(TNode preprocessed) { if(Dump.isOn("missed-t-propagations")) { d_possiblePropagations.push_back(preprocessed); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index be1c3abaf..2c1c9a436 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -323,9 +323,6 @@ class TheoryEngine { */ void assertSharedEqualities(); - /** The logic of the problem */ - std::string d_logic; - /** * Literals that are propagated by the theory. Note that these are TNodes. * The theory can only propagate nodes that have an assigned literal in the |