diff options
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 28 |
1 files changed, 24 insertions, 4 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 9ed20cc99..9a23d5518 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -17,6 +17,7 @@ #include "theory/theory.h" #include "util/cvc4_assert.h" #include "theory/quantifiers_engine.h" +#include "theory/substitutions.h" #include <vector> @@ -28,9 +29,6 @@ namespace theory { /** Default value for the uninterpreted sorts is the UF theory */ TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF; -/** By default, we use the type based theoryOf */ -TheoryOfMode Theory::s_theoryOfMode = THEORY_OF_TYPE_BASED; - std::ostream& operator<<(std::ostream& os, Theory::Effort level){ switch(level){ case Theory::EFFORT_STANDARD: @@ -72,7 +70,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { // Variables if (node.isVar()) { if (theoryOf(node.getType()) != theory::THEORY_BOOL) { - // We treat the varibables as uninterpreted + // We treat the variables as uninterpreted return s_uninterpretedSortOwner; } else { // Except for the Boolean ones, which we just ignore anyhow @@ -209,5 +207,27 @@ void Theory::computeRelevantTerms(set<Node>& termSet) } +Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstitutions) +{ + if (in.getKind() == kind::EQUAL) { + if (in[0].isVar() && !in[1].hasSubterm(in[0])) { + outSubstitutions.addSubstitution(in[0], in[1]); + return PP_ASSERT_STATUS_SOLVED; + } + if (in[1].isVar() && !in[0].hasSubterm(in[1])) { + outSubstitutions.addSubstitution(in[1], in[0]); + return PP_ASSERT_STATUS_SOLVED; + } + if (in[0].isConst() && in[1].isConst()) { + if (in[0] != in[1]) { + return PP_ASSERT_STATUS_CONFLICT; + } + } + } + + return PP_ASSERT_STATUS_UNSOLVED; +} + + }/* CVC4::theory namespace */ }/* CVC4 namespace */ |