diff options
author | Tim King <taking@google.com> | 2017-05-26 14:51:27 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2017-05-26 15:01:50 -0700 |
commit | 5b2d5430d08ae663d086d8d8e3944e01062935ec (patch) | |
tree | 2a04f0a0355d1f636dec6653bf92849a2989da72 /src/theory | |
parent | 0a425613d5108efa5f623d075135f2e08d3dfde2 (diff) |
Checking that equalities belong to the arithmetic theory in the solve() routine.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/normal_form.cpp | 10 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 3 |
2 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index f8de2f239..14607f4e4 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -14,11 +14,11 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/normal_form.h" #include <list> #include "base/output.h" -#include "theory/arith/normal_form.h" #include "theory/arith/arith_utilities.h" #include "theory/theory.h" @@ -805,6 +805,7 @@ DeltaRational Comparison::normalizedDeltaRational() const { } Comparison Comparison::parseNormalForm(TNode n) { + Debug("polynomial") << "Comparison::parseNormalForm(" << n << ")"; Comparison result(n); Assert(result.isNormalForm()); return result; @@ -1080,8 +1081,8 @@ bool Comparison::isNormalEqualityOrDisequality() const { /** This must be (= qvarlist qpolynomial) or (= zmonomial zpolynomial)*/ bool Comparison::isNormalEquality() const { Assert(getNode().getKind() == kind::EQUAL); - - return isNormalEqualityOrDisequality(); + return Theory::theoryOf(getNode()[0].getType()) == THEORY_ARITH && + isNormalEqualityOrDisequality(); } /** @@ -1092,7 +1093,8 @@ bool Comparison::isNormalDistinct() const { Assert(getNode().getKind() == kind::NOT); Assert(getNode()[0].getKind() == kind::EQUAL); - return isNormalEqualityOrDisequality(); + return Theory::theoryOf(getNode()[0][0].getType()) == THEORY_ARITH && + isNormalEqualityOrDisequality(); } Node Comparison::mkRatEquality(const Polynomial& p){ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index dfe092aa5..1b97dceb2 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1387,7 +1387,8 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o Rational minConstant = 0; Node minMonomial; Node minVar; - if (in.getKind() == kind::EQUAL) { + if (in.getKind() == kind::EQUAL && + Theory::theoryOf(in[0].getType()) == THEORY_ARITH) { Comparison cmp = Comparison::parseNormalForm(in); Polynomial left = cmp.getLeft(); |