From: Tim King Date: Fri, 6 Jun 2014 15:45:16 +0000 (-0400) Subject: Patch for the subtype theoryof mode to make the equalities over disequal types get... X-Git-Tag: cvc5-1.0.0~6854 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6ec8f46e9a7315057ac8fb5c58a6b44cf5a5159e;p=cvc5.git 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. --- 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: diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 2dd474a19..d9281e8ba 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -50,75 +50,81 @@ Theory::~Theory() { } TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { - - Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl; - + TheoryId tid = THEORY_BUILTIN; switch(mode) { case THEORY_OF_TYPE_BASED: // Constants, variables, 0-ary constructors if (node.isVar() || node.isConst()) { - return theoryOf(node.getType()); - } - // Equality is owned by the theory that owns the domain - if (node.getKind() == kind::EQUAL) { - return theoryOf(node[0].getType()); + tid = Theory::theoryOf(node.getType()); + } else if (node.getKind() == kind::EQUAL) { + // Equality is owned by the theory that owns the domain + tid = Theory::theoryOf(node[0].getType()); + } else { + // Regular nodes are owned by the kind + tid = kindToTheoryId(node.getKind()); } - // Regular nodes are owned by the kind - return kindToTheoryId(node.getKind()); break; case THEORY_OF_TERM_BASED: // Variables if (node.isVar()) { - if (theoryOf(node.getType()) != theory::THEORY_BOOL) { + if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) { // We treat the variables as uninterpreted - return s_uninterpretedSortOwner; + tid = s_uninterpretedSortOwner; } else { // Except for the Boolean ones, which we just ignore anyhow - return theory::THEORY_BOOL; + tid = theory::THEORY_BOOL; } - } - // Constants - if (node.isConst()) { + } else if (node.isConst()) { // Constants go to the theory of the type - return theoryOf(node.getType()); - } - // Equality - if (node.getKind() == kind::EQUAL) { + tid = Theory::theoryOf(node.getType()); + } else if (node.getKind() == kind::EQUAL) { // Equality // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow if (node[0].getKind() == kind::ITE) { - return theoryOf(node[0].getType()); - } - if (node[1].getKind() == kind::ITE) { - return theoryOf(node[1].getType()); - } - // If both sides belong to the same theory the choice is easy - TheoryId T1 = theoryOf(node[0]); - TheoryId T2 = theoryOf(node[1]); - if (T1 == T2) { - return T1; - } - TheoryId T3 = theoryOf(node[0].getType()); - // This is a case of - // * x*y = f(z) -> UF - // * x = c -> UF - // * f(x) = read(a, y) -> either UF or ARRAY - // at least one of the theories has to be parametric, i.e. theory of the type is different - // from the theory of the term - if (T1 == T3) { - return T2; - } - if (T2 == T3) { - return T1; + tid = Theory::theoryOf(node[0].getType()); + } else if (node[1].getKind() == kind::ITE) { + tid = Theory::theoryOf(node[1].getType()); + } else { + TNode l = node[0]; + TNode r = node[1]; + TypeNode ltype = l.getType(); + TypeNode rtype = r.getType(); + if( ltype != rtype ){ + tid = Theory::theoryOf(l.getType()); + }else { + // If both sides belong to the same theory the choice is easy + TheoryId T1 = Theory::theoryOf(l); + TheoryId T2 = Theory::theoryOf(r); + if (T1 == T2) { + tid = T1; + } else { + TheoryId T3 = Theory::theoryOf(ltype); + // This is a case of + // * x*y = f(z) -> UF + // * x = c -> UF + // * f(x) = read(a, y) -> either UF or ARRAY + // at least one of the theories has to be parametric, i.e. theory of the type is different + // from the theory of the term + if (T1 == T3) { + tid = T2; + } else if (T2 == T3) { + tid = T1; + } else { + // If both are parametric, we take the smaller one (arbitrary) + tid = T1 < T2 ? T1 : T2; + } + } + } } - // If both are parametric, we take the smaller one (arbitraty) - return T1 < T2 ? T1 : T2; + } else { + // Regular nodes are owned by the kind + tid = kindToTheoryId(node.getKind()); } - // Regular nodes are owned by the kind - return kindToTheoryId(node.getKind()); break; default: Unreachable(); } + Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl; + return tid; } void Theory::addSharedTermInternal(TNode n) { diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 2bfc87fc0..2fd1925f1 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -47,7 +47,8 @@ TESTS = \ miplib4.cvc \ miplibtrick.smt \ bug547.1.smt2 \ - bug547.2.smt2 + bug547.2.smt2 \ + bug569.smt2 # problem__003.smt2 EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2 new file mode 100644 index 000000000..acb6ffcdf --- /dev/null +++ b/test/regress/regress0/arith/bug569.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_AUFLIRA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v1 () Int) +(declare-fun v3 () Int) +(declare-fun v5 () Real) +(assert (= (to_real v1) (+ (to_real v3) v5))) +(assert (< v5 1)) +(assert (> v5 0)) +(check-sat) +(exit)