From 6ec8f46e9a7315057ac8fb5c58a6b44cf5a5159e Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 6 Jun 2014 11:45:16 -0400 Subject: Patch for the subtype theoryof mode to make the equalities over disequal types get sent to the theory of the type. Adding a new test case for bug 569. Fixes to the normal form of arithmetic so that real terms are before integer terms. --- src/theory/arith/arith_rewriter.cpp | 3 ++ src/theory/arith/normal_form.cpp | 55 ++++++++++++++++++++++- src/theory/arith/normal_form.h | 90 +++++++++++++++---------------------- 3 files changed, 92 insertions(+), 56 deletions(-) (limited to 'src/theory/arith') diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 5aa904aed..1d9abc38b 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -355,6 +355,9 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ Polynomial pleft = Polynomial::parsePolynomial(left); Polynomial pright = Polynomial::parsePolynomial(right); + Debug("arith::rewriter") << "pleft " << pleft.getNode() << std::endl; + Debug("arith::rewriter") << "pright " << pright.getNode() << std::endl; + Comparison cmp = Comparison::mkComparison(atom.getKind(), pleft, pright); Assert(cmp.isNormalForm()); return RewriteResponse(REWRITE_DONE, cmp.getNode()); diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 9ccf057b1..afaaedbf9 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -118,10 +118,32 @@ bool VarList::isMember(Node n) { return false; } } + int VarList::cmp(const VarList& vl) const { int dif = this->size() - vl.size(); if (dif == 0) { - return this->getNode().getId() - vl.getNode().getId(); + if(this->getNode() == vl.getNode()) { + return 0; + } + + Assert(!empty()); + Assert(!vl.empty()); + if(this->size() == 1){ + return Variable::VariableNodeCmp::cmp(this->getNode(), vl.getNode()); + } + + + internal_iterator ii=this->internalBegin(), ie=this->internalEnd(); + internal_iterator ci=vl.internalBegin(), ce=vl.internalEnd(); + for(; ii != ie; ++ii, ++ci){ + Node vi = *ii; + Node vc = *ci; + int tmp = Variable::VariableNodeCmp::cmp(vi, vc); + if(tmp != 0){ + return tmp; + } + } + Unreachable(); } else if(dif < 0) { return -1; } else { @@ -559,6 +581,36 @@ bool Polynomial::variableMonomialAreStrictlyGreater(const Monomial& m) const{ } } +bool Polynomial::isMember(TNode n) { + if(Monomial::isMember(n)){ + return true; + }else if(n.getKind() == kind::PLUS){ + Assert(n.getNumChildren() >= 2); + Node::iterator currIter = n.begin(), end = n.end(); + Node prev = *currIter; + if(!Monomial::isMember(prev)){ + return false; + } + + Monomial mprev = Monomial::parseMonomial(prev); + ++currIter; + for(; currIter != end; ++currIter){ + Node curr = *currIter; + if(!Monomial::isMember(curr)){ + return false; + } + Monomial mcurr = Monomial::parseMonomial(curr); + if(!(mprev < mcurr)){ + return false; + } + mprev = mcurr; + } + return true; + } else { + return false; + } +} + Node SumPair::computeQR(const SumPair& sp, const Integer& div){ Assert(sp.isIntegral()); @@ -1156,6 +1208,7 @@ Comparison Comparison::mkComparison(Kind k, const Polynomial& l, const Polynomia VarList vRight = r.asVarList(); if(vLeft == vRight){ + // return true for equalities and false for disequalities return Comparison(k == kind::EQUAL); }else{ Node eqNode = vLeft < vRight ? toNode( kind::EQUAL, l, r) : toNode( kind::EQUAL, r, l); diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 7e8ff556d..3267834b5 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -270,40 +270,48 @@ public: bool operator<(const Variable& v) const { VariableNodeCmp cmp; return cmp(this->getNode(), v.getNode()); - - // bool thisIsVariable = isMetaKindVariable(); - // bool vIsVariable = v.isMetaKindVariable(); - - // if(thisIsVariable == vIsVariable){ - // bool thisIsInteger = isIntegral(); - // bool vIsInteger = v.isIntegral(); - // if(thisIsInteger == vIsInteger){ - // return getNode() < v.getNode(); - // }else{ - // return thisIsInteger && !vIsInteger; - // } - // }else{ - // return thisIsVariable && !vIsVariable; - // } } struct VariableNodeCmp { - bool operator()(Node n, Node m) const { - bool nIsVariable = n.isVar(); - bool mIsVariable = m.isVar(); - - if(nIsVariable == mIsVariable){ - bool nIsInteger = n.getType().isInteger(); - bool mIsInteger = m.getType().isInteger(); - if(nIsInteger == mIsInteger){ - return n < m; + static inline int cmp(Node n, Node m) { + if ( n == m ) { return 0; } + + // this is now slightly off of the old variable order. + + bool nIsInteger = n.getType().isInteger(); + bool mIsInteger = m.getType().isInteger(); + + if(nIsInteger == mIsInteger){ + bool nIsVariable = n.isVar(); + bool mIsVariable = m.isVar(); + + if(nIsVariable == mIsVariable){ + if(n < m){ + return -1; + }else{ + Assert( n != m ); + return 1; + } }else{ - return nIsInteger && !mIsInteger; + if(nIsVariable){ + return -1; // nIsVariable => !mIsVariable + }else{ + return 1; // !nIsVariable => mIsVariable + } } }else{ - return nIsVariable && !mIsVariable; + Assert(nIsInteger != mIsInteger); + if(nIsInteger){ + return 1; // nIsInteger => !mIsInteger + }else{ + return -1; // !nIsInteger => mIsInteger + } } } + + bool operator()(Node n, Node m) const { + return VariableNodeCmp::cmp(n,m) < 0; + } }; bool operator==(const Variable& v) const { return getNode() == v.getNode();} @@ -821,35 +829,7 @@ private: bool singleton() const { return d_singleton; } public: - static bool isMember(TNode n) { - if(Monomial::isMember(n)){ - return true; - }else if(n.getKind() == kind::PLUS){ - Assert(n.getNumChildren() >= 2); - Node::iterator currIter = n.begin(), end = n.end(); - Node prev = *currIter; - if(!Monomial::isMember(prev)){ - return false; - } - - Monomial mprev = Monomial::parseMonomial(prev); - ++currIter; - for(; currIter != end; ++currIter){ - Node curr = *currIter; - if(!Monomial::isMember(curr)){ - return false; - } - Monomial mcurr = Monomial::parseMonomial(curr); - if(!(mprev < mcurr)){ - return false; - } - mprev = mcurr; - } - return true; - } else { - return false; - } - } + static bool isMember(TNode n); class iterator { private: -- cgit v1.2.3