Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.
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());
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 {
}
}
+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());
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);
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();}
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:
}
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) {
miplib4.cvc \
miplibtrick.smt \
bug547.1.smt2 \
- bug547.2.smt2
+ bug547.2.smt2 \
+ bug569.smt2
# problem__003.smt2
EXTRA_DIST = $(TESTS) \
--- /dev/null
+(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)
projects / cvc5.git / commitdiff