diff options
28 files changed, 519 insertions, 445 deletions
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 4865ccead..d16513cfb 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -276,14 +276,6 @@ header = "options/arith_options.h" help = "use quick explain to minimize the sum of infeasibility conflicts" [[option]] - name = "rewriteDivk" - category = "regular" - long = "rewrite-divk" - type = "bool" - default = "false" - help = "rewrite division and mod when by a constant into linear terms" - -[[option]] name = "trySolveIntStandardEffort" category = "regular" long = "se-solve-int" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 899da4d4a..e06363883 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1097,11 +1097,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) { options::quantSplit.set(false); } - // rewrite divk - if (!options::rewriteDivk.wasSetByUser()) - { - options::rewriteDivk.set(true); - } // do not do macros if (!options::macrosQuant.wasSetByUser()) { @@ -1136,11 +1131,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } if (options::cegqi()) { - // must rewrite divk - if (!options::rewriteDivk.wasSetByUser()) - { - options::rewriteDivk.set(true); - } if (options::incrementalSolving()) { // cannot do nested quantifier elimination in incremental mode diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 7fdab2034..09b6d742a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -34,6 +34,7 @@ #include "expr/node.h" #include "expr/node_algorithm.h" #include "expr/node_builder.h" +#include "expr/proof_skolem_cache.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() #include "preprocessing/util/ite_utilities.h" @@ -226,100 +227,6 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec& // return safeConstructNary(nb); } -// Integer division axioms: -// These concenrate the high level constructs needed to constrain the functions: -// div, mod, div_total and mod_total. -// -// The high level constraint. -// (for all ((m Int) (n Int)) -// (=> (distinct n 0) -// (let ((q (div m n)) (r (mod m n))) -// (and (= m (+ (* n q) r)) -// (<= 0 r (- (abs n) 1)))))) -// -// We now add division by 0 functions. -// (for all ((m Int) (n Int)) -// (let ((q (div m n)) (r (mod m n))) -// (ite (= n 0) -// (and (= q (div_0_func m)) (= r (mod_0_func m))) -// (and (= m (+ (* n q) r)) -// (<= 0 r (- (abs n) 1))))))) -// -// We now express div and mod in terms of div_total and mod_total. -// (for all ((m Int) (n Int)) -// (let ((q (div m n)) (r (mod m n))) -// (ite (= n 0) -// (and (= q (div_0_func m)) (= r (mod_0_func m))) -// (and (= q (div_total m n)) (= r (mod_total m n)))))) -// -// Alternative div_total and mod_total without the abs function: -// (for all ((m Int) (n Int)) -// (let ((q (div_total m n)) (r (mod_total m n))) -// (ite (= n 0) -// (and (= q 0) (= r 0)) -// (and (r = m - n * q) -// (ite (> n 0) -// (n*q <= m < n*q + n) -// (n*q <= m < n*q - n)))))) - - -// Returns a formula that entails that q equals the total integer division of m -// by n. -// (for all ((m Int) (n Int)) -// (let ((q (div_total m n))) -// (ite (= n 0) -// (= q 0) -// (ite (> n 0) -// (n*q <= m < n*q + n) -// (n*q <= m < n*q - n))))) -Node mkAxiomForTotalIntDivision(Node m, Node n, Node q) { - NodeManager* nm = NodeManager::currentNM(); - Node zero = mkRationalNode(0); - // (n*q <= m < n*q + n) is equivalent to (0 <= m - n*q < n). - Node diff = nm->mkNode(kind::MINUS, m, mkMult(n, q)); - Node when_n_is_positive = mkInRange(diff, zero, n); - Node when_n_is_negative = mkInRange(diff, zero, nm->mkNode(kind::UMINUS, n)); - return n.eqNode(zero).iteNode( - q.eqNode(zero), nm->mkNode(kind::GT, n, zero) - .iteNode(when_n_is_positive, when_n_is_negative)); -} - -// Returns a formula that entails that r equals the integer division total of m -// by n assuming q is equal to (div_total m n). -// (for all ((m Int) (n Int)) -// (let ((q (div_total m n)) (r (mod_total m n))) -// (ite (= n 0) -// (= r 0) -// (= r (- m (n * q)))))) -Node mkAxiomForTotalIntMod(Node m, Node n, Node q, Node r) { - NodeManager* nm = NodeManager::currentNM(); - Node diff = nm->mkNode(kind::MINUS, m, mkMult(n, q)); - return mkOnZeroIte(n, r, mkRationalNode(0), diff); -} - -// Returns an expression that constrains a term to be the result of the -// [total] integer division of num by den. Equivalently: -// (and (=> (den > 0) (den*term <= num < den*term + den)) -// (=> (den < 0) (den*term <= num < den*term - den)) -// (=> (den = 0) (term = 0))) -// static Node mkIntegerDivisionConstraint(Node term, Node num, Node den) { -// // We actually encode: -// // (and (=> (den > 0) (0 <= num - den*term < den)) -// // (=> (den < 0) (0 <= num - den*term < -den)) -// // (=> (den = 0) (term = 0))) -// NodeManager* nm = NodeManager::currentNM(); -// Node zero = nm->mkConst(Rational(0)); -// Node den_is_positive = nm->mkNode(kind::GT, den, zero); -// Node den_is_negative = nm->mkNode(kind::LT, den, zero); -// Node diff = nm->mkNode(kind::MINUS, num, mkMult(den, term)); -// Node when_den_positive = den_positive.impNode(mkInRange(diff, zero, den)); -// Node when_den_negative = den_negative.impNode( -// mkInRange(diff, zero, nm->mkNode(kind::UMINUS, den))); -// Node when_den_is_zero = (den.eqNode(zero)).impNode(term.eqNode(zero)); -// return mk->mkNode(kind::AND, when_den_positive, when_den_negative, -// when_den_is_zero); -// } - void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_congruenceManager.setMasterEqualityEngine(eq); } @@ -1176,126 +1083,443 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) { if(Theory::theoryOf(n) != THEORY_ARITH) { return n; } + // Eliminate operators recursively. Notice we must do this here since other + // theories may generate lemmas that involve non-standard operators. For + // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may + // introduce non-standard arithmetic terms appearing in grammars. + // call eliminate operators + Node nn = eliminateOperators(n); + if (nn != n) + { + // since elimination may introduce new operators to eliminate, we must + // recursively eliminate result + return eliminateOperatorsRec(nn); + } + return n; +} + +void TheoryArithPrivate::checkNonLinearLogic(Node term) +{ + if (getLogicInfo().isLinear()) + { + Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << term + << std::endl; + std::stringstream serr; + serr << "A non-linear fact was asserted to arithmetic in a linear logic." + << std::endl; + serr << "The fact in question: " << term << endl; + throw LogicException(serr.str()); + } +} + +struct ArithElimOpAttributeId +{ +}; +typedef expr::Attribute<ArithElimOpAttributeId, Node> ArithElimOpAttribute; + +Node TheoryArithPrivate::eliminateOperatorsRec(Node n) +{ + ArithElimOpAttribute aeoa; + Trace("arith-elim") << "Begin elim: " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map<Node, Node, TNodeHashFunction> visited; + std::unordered_map<Node, Node, TNodeHashFunction>::iterator it; + std::vector<Node> visit; + Node cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + if (Theory::theoryOf(cur) != THEORY_ARITH) + { + visited[cur] = cur; + } + else if (it == visited.end()) + { + if (cur.hasAttribute(aeoa)) + { + visited[cur] = cur.getAttribute(aeoa); + } + else + { + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector<Node> children; + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + Node retElim = eliminateOperators(ret); + if (retElim != ret) + { + // recursively eliminate operators in result, since some eliminations + // are defined in terms of other non-standard operators. + ret = eliminateOperatorsRec(retElim); + } + cur.setAttribute(aeoa, ret); + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} +Node TheoryArithPrivate::eliminateOperators(Node node) +{ NodeManager* nm = NodeManager::currentNM(); - switch(Kind k = n.getKind()) { - - case kind::TO_INTEGER: - case kind::IS_INTEGER: { - Node toIntSkolem; - NodeMap::const_iterator it = d_to_int_skolem.find( n[0] ); - if( it==d_to_int_skolem.end() ){ - toIntSkolem = nm->mkSkolem("toInt", nm->integerType(), - "a conversion of a Real term to its Integer part"); - d_to_int_skolem[n[0]] = toIntSkolem; - // n[0] - 1 < toIntSkolem <= n[0] - // -1 < toIntSkolem - n[0] <= 0 - // 0 <= n[0] - toIntSkolem < 1 - Node one = mkRationalNode(1); - Node lem = mkAxiomForTotalIntDivision(n[0], one, toIntSkolem); - outputLemma(lem); - }else{ - toIntSkolem = (*it).second; + Kind k = node.getKind(); + switch (k) + { + case kind::TANGENT: + case kind::COSECANT: + case kind::SECANT: + case kind::COTANGENT: + { + // these are eliminated by rewriting + return Rewriter::rewrite(node); + break; } - if(k == kind::IS_INTEGER) { - return nm->mkNode(kind::EQUAL, n[0], toIntSkolem); + case kind::TO_INTEGER: + case kind::IS_INTEGER: + { + Node toIntSkolem; + NodeMap::const_iterator it = d_to_int_skolem.find(node[0]); + if (it == d_to_int_skolem.end()) + { + // node[0] - 1 < toIntSkolem <= node[0] + // -1 < toIntSkolem - node[0] <= 0 + // 0 <= node[0] - toIntSkolem < 1 + Node v = nm->mkBoundVar(nm->integerType()); + Node one = mkRationalNode(1); + Node zero = mkRationalNode(0); + Node diff = nm->mkNode(kind::MINUS, node[0], v); + Node lem = mkInRange(diff, zero, one); + toIntSkolem = ProofSkolemCache::mkSkolem( + v, lem, "toInt", "a conversion of a Real term to its Integer part"); + toIntSkolem = ProofSkolemCache::getWitnessForm(toIntSkolem); + d_to_int_skolem[node[0]] = toIntSkolem; + } + else + { + toIntSkolem = (*it).second; + } + if (k == kind::IS_INTEGER) + { + return nm->mkNode(kind::EQUAL, node[0], toIntSkolem); + } + Assert(k == kind::TO_INTEGER); + return toIntSkolem; } - Assert(k == kind::TO_INTEGER); - return toIntSkolem; - } - case kind::INTS_DIVISION: - case kind::INTS_MODULUS: - case kind::DIVISION: - // these should be removed during expand definitions - Assert(false); - break; - - case kind::INTS_DIVISION_TOTAL: - case kind::INTS_MODULUS_TOTAL: { - Node den = Rewriter::rewrite(n[1]); - if(!options::rewriteDivk() && den.isConst()) { - return n; - } - Node num = Rewriter::rewrite(n[0]); - Node intVar; - Node rw = nm->mkNode(k, num, den); - NodeMap::const_iterator it = d_int_div_skolem.find( rw ); - if( it==d_int_div_skolem.end() ){ - intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term"); - d_int_div_skolem[rw] = intVar; - Node lem; - if (den.isConst()) { - const Rational& rat = den.getConst<Rational>(); - Assert(!num.isConst()); - if(rat != 0) { - if(rat > 0) { - lem = nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), - nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1)))))); - } else { - lem = nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), - nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))); + + case kind::INTS_DIVISION_TOTAL: + case kind::INTS_MODULUS_TOTAL: + { + Node den = Rewriter::rewrite(node[1]); + Node num = Rewriter::rewrite(node[0]); + Node intVar; + Node rw = nm->mkNode(k, num, den); + NodeMap::const_iterator it = d_int_div_skolem.find(rw); + if (it == d_int_div_skolem.end()) + { + Node v = nm->mkBoundVar(nm->integerType()); + Node lem; + Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num); + if (den.isConst()) + { + const Rational& rat = den.getConst<Rational>(); + if (num.isConst() || rat == 0) + { + // just rewrite + return Rewriter::rewrite(node); + } + if (rat > 0) + { + lem = nm->mkNode( + AND, + leqNum, + nm->mkNode( + LT, + num, + nm->mkNode(MULT, + den, + nm->mkNode(PLUS, v, nm->mkConst(Rational(1)))))); + } + else + { + lem = nm->mkNode( + AND, + leqNum, + nm->mkNode( + LT, + num, + nm->mkNode( + MULT, + den, + nm->mkNode(PLUS, v, nm->mkConst(Rational(-1)))))); } } - }else{ - lem = nm->mkNode(kind::AND, - nm->mkNode(kind::IMPLIES, NodeManager::currentNM()->mkNode( kind::GT, den, nm->mkConst(Rational(0)) ), - nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), - nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1))))))), - nm->mkNode(kind::IMPLIES, NodeManager::currentNM()->mkNode( kind::LT, den, nm->mkConst(Rational(0)) ), - nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), - nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))))); - } - if( !lem.isNull() ){ - outputLemma(lem); + else + { + checkNonLinearLogic(node); + lem = nm->mkNode( + AND, + nm->mkNode( + IMPLIES, + nm->mkNode(GT, den, nm->mkConst(Rational(0))), + nm->mkNode( + AND, + leqNum, + nm->mkNode( + LT, + num, + nm->mkNode( + MULT, + den, + nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))), + nm->mkNode( + IMPLIES, + nm->mkNode(LT, den, nm->mkConst(Rational(0))), + nm->mkNode( + AND, + leqNum, + nm->mkNode( + LT, + num, + nm->mkNode( + MULT, + den, + nm->mkNode( + PLUS, v, nm->mkConst(Rational(-1)))))))); + } + intVar = ProofSkolemCache::mkSkolem( + v, lem, "linearIntDiv", "the result of an intdiv-by-k term"); + intVar = ProofSkolemCache::getWitnessForm(intVar); + d_int_div_skolem[rw] = intVar; } - }else{ - intVar = (*it).second; + else + { + intVar = (*it).second; + } + if (k == kind::INTS_MODULUS_TOTAL) + { + Node nn = + nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar)); + return nn; + } + else + { + return intVar; + } + break; } - if( k==kind::INTS_MODULUS_TOTAL ){ - Node node = nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar)); - return node; - }else{ - return intVar; + case kind::DIVISION_TOTAL: + { + Node num = Rewriter::rewrite(node[0]); + Node den = Rewriter::rewrite(node[1]); + if (den.isConst()) + { + // No need to eliminate here, can eliminate via rewriting later. + // Moreover, rewriting may change the type of this node from real to + // int, which impacts certain issues with subtyping. + return node; + } + checkNonLinearLogic(node); + Node var; + Node rw = nm->mkNode(k, num, den); + NodeMap::const_iterator it = d_div_skolem.find(rw); + if (it == d_div_skolem.end()) + { + Node v = nm->mkBoundVar(nm->realType()); + Node lem = nm->mkNode(IMPLIES, + den.eqNode(nm->mkConst(Rational(0))).negate(), + nm->mkNode(MULT, den, v).eqNode(num)); + var = ProofSkolemCache::mkSkolem( + v, lem, "nonlinearDiv", "the result of a non-linear div term"); + var = ProofSkolemCache::getWitnessForm(var); + d_div_skolem[rw] = var; + } + else + { + var = (*it).second; + } + return var; + break; } - break; - } - case kind::DIVISION_TOTAL: { - Node num = Rewriter::rewrite(n[0]); - Node den = Rewriter::rewrite(n[1]); - Assert(!den.isConst()); - Node var; - Node rw = nm->mkNode(k, num, den); - NodeMap::const_iterator it = d_div_skolem.find( rw ); - if( it==d_div_skolem.end() ){ - var = nm->mkSkolem("nonlinearDiv", nm->realType(), "the result of a non-linear div term"); - d_div_skolem[rw] = var; - outputLemma(nm->mkNode(kind::IMPLIES, den.eqNode(nm->mkConst(Rational(0))).negate(), nm->mkNode(kind::MULT, den, var).eqNode(num))); - }else{ - var = (*it).second; + case kind::DIVISION: + { + Node num = Rewriter::rewrite(node[0]); + Node den = Rewriter::rewrite(node[1]); + Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den); + if (!den.isConst() || den.getConst<Rational>().sgn() == 0) + { + checkNonLinearLogic(node); + Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO); + Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); + ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret); + } + return ret; + break; } - return var; - break; - } - default: - break; - } - for(TNode::const_iterator i = n.begin(); i != n.end(); ++i) { - Node rewritten = ppRewriteTerms(*i); - if(rewritten != *i) { - NodeBuilder<> b(n.getKind()); - b.append(n.begin(), i); - b << rewritten; - for(++i; i != n.end(); ++i) { - b << ppRewriteTerms(*i); + case kind::INTS_DIVISION: + { + // partial function: integer div + Node num = Rewriter::rewrite(node[0]); + Node den = Rewriter::rewrite(node[1]); + Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den); + if (!den.isConst() || den.getConst<Rational>().sgn() == 0) + { + checkNonLinearLogic(node); + Node intDivByZeroNum = + getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO); + Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); + ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret); } - rewritten = b; - return rewritten; + return ret; + break; } - } - return n; + case kind::INTS_MODULUS: + { + // partial function: mod + Node num = Rewriter::rewrite(node[0]); + Node den = Rewriter::rewrite(node[1]); + Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); + if (!den.isConst() || den.getConst<Rational>().sgn() == 0) + { + checkNonLinearLogic(node); + Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO); + Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); + ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret); + } + return ret; + break; + } + + case kind::ABS: + { + return nm->mkNode(kind::ITE, + nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), + nm->mkNode(kind::UMINUS, node[0]), + node[0]); + break; + } + case kind::SQRT: + case kind::ARCSINE: + case kind::ARCCOSINE: + case kind::ARCTANGENT: + case kind::ARCCOSECANT: + case kind::ARCSECANT: + case kind::ARCCOTANGENT: + { + checkNonLinearLogic(node); + // eliminate inverse functions here + NodeMap::const_iterator it = d_nlin_inverse_skolem.find(node); + if (it == d_nlin_inverse_skolem.end()) + { + Node var = nm->mkBoundVar(nm->realType()); + Node lem; + if (k == kind::SQRT) + { + Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT); + Node uf = skolemApp.eqNode(var); + Node nonNeg = nm->mkNode( + kind::AND, nm->mkNode(kind::MULT, var, var).eqNode(node[0]), uf); + + // sqrt(x) reduces to: + // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x)) + // + // Uf(x) makes sure that the reduction still behaves like a function, + // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be + // satisfiable. On the original formula, this would require that we + // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid + // model. + lem = nm->mkNode( + kind::ITE, + nm->mkNode(kind::GEQ, node[0], nm->mkConst(Rational(0))), + nonNeg, + uf); + } + else + { + Node pi = mkPi(); + + // range of the skolem + Node rlem; + if (k == kind::ARCSINE || k == ARCTANGENT || k == ARCCOSECANT) + { + Node half = nm->mkConst(Rational(1) / Rational(2)); + Node pi2 = nm->mkNode(kind::MULT, half, pi); + Node npi2 = nm->mkNode(kind::MULT, nm->mkConst(Rational(-1)), pi2); + // -pi/2 < var <= pi/2 + rlem = nm->mkNode( + AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2)); + } + else + { + // 0 <= var < pi + rlem = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConst(Rational(0)), var), + nm->mkNode(LT, var, pi)); + } + + Kind rk = k == kind::ARCSINE + ? kind::SINE + : (k == kind::ARCCOSINE + ? kind::COSINE + : (k == kind::ARCTANGENT + ? kind::TANGENT + : (k == kind::ARCCOSECANT + ? kind::COSECANT + : (k == kind::ARCSECANT + ? kind::SECANT + : kind::COTANGENT)))); + Node invTerm = nm->mkNode(rk, var); + lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0])); + } + Assert(!lem.isNull()); + Node ret = ProofSkolemCache::mkSkolem( + var, + lem, + "tfk", + "Skolem to eliminate a non-standard transcendental function"); + ret = ProofSkolemCache::getWitnessForm(ret); + d_nlin_inverse_skolem[node] = ret; + return ret; + } + return (*it).second; + break; + } + + default: break; + } + return node; } Node TheoryArithPrivate::ppRewrite(TNode atom) { @@ -1312,6 +1536,7 @@ Node TheoryArithPrivate::ppRewrite(TNode atom) { Node rewritten = Rewriter::rewrite(leq.andNode(geq)); Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; + // don't need to rewrite terms since rewritten is not a non-standard op return rewritten; } } @@ -1441,11 +1666,6 @@ void TheoryArithPrivate::setupVariable(const Variable& x){ //setupInitialValue(varN); markSetup(n); - - if(x.isDivLike()){ - setupDivLike(x); - } - } void TheoryArithPrivate::setupVariableList(const VarList& vl){ @@ -1508,52 +1728,6 @@ void TheoryArithPrivate::cautiousSetupPolynomial(const Polynomial& p){ } } -void TheoryArithPrivate::setupDivLike(const Variable& v){ - Assert(v.isDivLike()); - - if(getLogicInfo().isLinear()){ - throw LogicException( - "A non-linear fact (involving div/mod/divisibility) was asserted to " - "arithmetic in a linear logic;\nif you only use division (or modulus) " - "by a constant value, or if you only use the divisibility-by-k " - "predicate, try using the --rewrite-divk option."); - } - - Node vnode = v.getNode(); - Assert( - isSetup(vnode)); // Otherwise there is some invariant breaking recursion - Polynomial m = Polynomial::parsePolynomial(vnode[0]); - Polynomial n = Polynomial::parsePolynomial(vnode[1]); - - cautiousSetupPolynomial(m); - cautiousSetupPolynomial(n); - - Node lem; - switch(vnode.getKind()){ - case DIVISION: - case INTS_DIVISION: - case INTS_MODULUS: - // these should be removed during expand definitions - Assert(false); - break; - case DIVISION_TOTAL: - lem = axiomIteForTotalDivision(vnode); - break; - case INTS_DIVISION_TOTAL: - case INTS_MODULUS_TOTAL: - lem = axiomIteForTotalIntDivision(vnode); - break; - default: - /* intentionally blank */ - break; - } - - if(!lem.isNull()){ - Debug("arith::div") << lem << endl; - outputLemma(lem); - } -} - Node TheoryArithPrivate::axiomIteForTotalDivision(Node div_tot){ Assert(div_tot.getKind() == DIVISION_TOTAL); @@ -5056,157 +5230,15 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ Node TheoryArithPrivate::expandDefinition(Node node) { - NodeManager* nm = NodeManager::currentNM(); - - // eliminate here since the rewritten form of these may introduce division - Kind k = node.getKind(); - if (k == kind::TANGENT || k == kind::COSECANT || k == kind::SECANT - || k == kind::COTANGENT) + // call eliminate operators + Node nn = eliminateOperators(node); + if (nn != node) { - node = Rewriter::rewrite(node); - k = node.getKind(); + // since elimination may introduce new operators to eliminate, we must + // recursively eliminate result + return eliminateOperatorsRec(nn); } - - switch (k) - { - case kind::DIVISION: - { - TNode num = node[0], den = node[1]; - Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den); - if (!den.isConst() || den.getConst<Rational>().sgn() == 0) - { - Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO); - Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret); - } - return ret; - break; - } - - case kind::INTS_DIVISION: - { - // partial function: integer div - TNode num = node[0], den = node[1]; - Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den); - if (!den.isConst() || den.getConst<Rational>().sgn() == 0) - { - Node intDivByZeroNum = - getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO); - Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret); - } - return ret; - break; - } - - case kind::INTS_MODULUS: - { - // partial function: mod - TNode num = node[0], den = node[1]; - Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); - if (!den.isConst() || den.getConst<Rational>().sgn() == 0) - { - Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO); - Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret); - } - return ret; - break; - } - - case kind::ABS: - { - return nm->mkNode(kind::ITE, - nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), - nm->mkNode(kind::UMINUS, node[0]), - node[0]); - break; - } - case kind::SQRT: - case kind::ARCSINE: - case kind::ARCCOSINE: - case kind::ARCTANGENT: - case kind::ARCCOSECANT: - case kind::ARCSECANT: - case kind::ARCCOTANGENT: - { - // eliminate inverse functions here - NodeMap::const_iterator it = d_nlin_inverse_skolem.find(node); - if (it == d_nlin_inverse_skolem.end()) - { - Node var = nm->mkBoundVar(nm->realType()); - Node lem; - if (k == kind::SQRT) - { - Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT); - Node uf = skolemApp.eqNode(var); - Node nonNeg = nm->mkNode( - kind::AND, nm->mkNode(kind::MULT, var, var).eqNode(node[0]), uf); - - // sqrt(x) reduces to: - // witness y. ite(x >= 0.0, y * y = x ^ Uf(x), Uf(x)) - // - // Uf(x) makes sure that the reduction still behaves like a function, - // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be - // satisfiable. On the original formula, this would require that we - // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid - // model. - lem = nm->mkNode( - kind::ITE, - nm->mkNode(kind::GEQ, node[0], nm->mkConst(Rational(0))), - nonNeg, - uf); - } - else - { - Node pi = mkPi(); - - // range of the skolem - Node rlem; - if (k == kind::ARCSINE || k == ARCTANGENT || k == ARCCOSECANT) - { - Node half = nm->mkConst(Rational(1) / Rational(2)); - Node pi2 = nm->mkNode(kind::MULT, half, pi); - Node npi2 = nm->mkNode(kind::MULT, nm->mkConst(Rational(-1)), pi2); - // -pi/2 < var <= pi/2 - rlem = nm->mkNode( - AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2)); - } - else - { - // 0 <= var < pi - rlem = nm->mkNode(AND, - nm->mkNode(LEQ, nm->mkConst(Rational(0)), var), - nm->mkNode(LT, var, pi)); - } - - Kind rk = k == kind::ARCSINE - ? kind::SINE - : (k == kind::ARCCOSINE - ? kind::COSINE - : (k == kind::ARCTANGENT - ? kind::TANGENT - : (k == kind::ARCCOSECANT - ? kind::COSECANT - : (k == kind::ARCSECANT - ? kind::SECANT - : kind::COTANGENT)))); - Node invTerm = nm->mkNode(rk, var); - lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0])); - } - Assert(!lem.isNull()); - Node ret = nm->mkNode(WITNESS, nm->mkNode(BOUND_VAR_LIST, var), lem); - d_nlin_inverse_skolem[node] = ret; - return ret; - } - return (*it).second; - break; - } - - default: return node; break; - } - - Unreachable(); + return node; } Node TheoryArithPrivate::getArithSkolem(ArithSkolemId asi) diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index b5debe76d..8198dbcf1 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -189,9 +189,6 @@ public: d_setupNodes.insert(n); } private: - - void setupDivLike(const Variable& x); - void setupVariable(const Variable& x); void setupVariableList(const VarList& vl); void setupPolynomial(const Polynomial& poly); @@ -422,7 +419,39 @@ private: // handle linear /, div, mod, and also is_int, to_int Node ppRewriteTerms(TNode atom); -public: + /** + * Called when a non-linear term n is given to this class. Throw an exception + * if the logic is linear. + */ + void checkNonLinearLogic(Node term); + /** + * Eliminate operators in term n. If n has top symbol that is not a core + * one (including division, int division, mod, to_int, is_int, syntactic sugar + * transcendental functions), then we replace it by a form that eliminates + * that operator. This may involve the introduction of witness terms. + * + * One exception to the above rule is that we may leave certain applications + * like (/ 4 1) unchanged, since replacing this by 4 changes its type from + * real to int. This is important for some subtyping issues during + * expandDefinition. Moreover, applications like this can be eliminated + * trivially later by rewriting. + * + * This method is called both during expandDefinition and during ppRewrite. + * + * @param n The node to eliminate operators from. + * @return The (single step) eliminated form of n. + */ + Node eliminateOperators(Node n); + /** + * Recursively ensure that n has no non-standard operators. This applies + * the above method on all subterms of n. + * + * @param n The node to eliminate operators from. + * @return The eliminated form of n. + */ + Node eliminateOperatorsRec(Node n); + + public: TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryArithPrivate(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2df07db5a..5a59f2f54 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1121,6 +1121,9 @@ set(regress_0_tests regress0/uflra/simple.02.cvc regress0/uflra/simple.03.cvc regress0/uflra/simple.04.cvc + regress0/unconstrained/4481.smt2 + regress0/unconstrained/4484.smt2 + regress0/unconstrained/4486.smt2 regress0/unconstrained/arith.smt2 regress0/unconstrained/arith3.smt2 regress0/unconstrained/arith4.smt2 @@ -1472,6 +1475,7 @@ set(regress_1_tests regress1/push-pop/fuzz_7.smt2 regress1/push-pop/fuzz_8.smt2 regress1/push-pop/fuzz_9.smt2 + regress1/push-pop/model-unsound-ania.smt2 regress1/push-pop/quant-fun-proc-unmacro.smt2 regress1/push-pop/quant-fun-proc.smt2 regress1/quantifiers/006-cbqi-ite.smt2 diff --git a/test/regress/regress0/arith/bug547.2.smt2 b/test/regress/regress0/arith/bug547.2.smt2 index b7d114eb3..7ff2a538a 100644 --- a/test/regress/regress0/arith/bug547.2.smt2 +++ b/test/regress/regress0/arith/bug547.2.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: sat (set-logic QF_NIA) +(set-info :status sat) (declare-fun x () Int) (declare-fun y () Int) (declare-fun z () Int) diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2 index 9ddc80e98..76bc4095f 100644 --- a/test/regress/regress0/arith/div-chainable.smt2 +++ b/test/regress/regress0/arith/div-chainable.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: sat (set-logic QF_LIA) (set-info :status sat) diff --git a/test/regress/regress0/arith/mod-simp.smt2 b/test/regress/regress0/arith/mod-simp.smt2 index 7294cd863..1a9c50590 100644 --- a/test/regress/regress0/arith/mod-simp.smt2 +++ b/test/regress/regress0/arith/mod-simp.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: unsat (set-logic QF_LIA) (set-info :status unsat) diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2 index 75d82d98f..581c34f2d 100644 --- a/test/regress/regress0/bug548a.smt2 +++ b/test/regress/regress0/bug548a.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --rewrite-divk --tlimit 1000 +; COMMAND-LINE: --tlimit 1000 ; EXPECT: unknown (set-logic AUFLIA) (declare-fun f (Int) Int) diff --git a/test/regress/regress0/quantifiers/mix-match.smt2 b/test/regress/regress0/quantifiers/mix-match.smt2 index c6ac3b56f..fbf996a0a 100644 --- a/test/regress/regress0/quantifiers/mix-match.smt2 +++ b/test/regress/regress0/quantifiers/mix-match.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-check-unsat-cores +; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) (declare-fun P (Real) Bool) @@ -7,4 +9,4 @@ (assert (is_int a)) (assert (not (P a))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/unconstrained/4481.smt2 b/test/regress/regress0/unconstrained/4481.smt2 new file mode 100644 index 000000000..028607093 --- /dev/null +++ b/test/regress/regress0/unconstrained/4481.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --unconstrained-simp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () Int) +(assert (= (div a 2) 2)) +(assert (= (div a 3) 0)) +(check-sat) diff --git a/test/regress/regress0/unconstrained/4484.smt2 b/test/regress/regress0/unconstrained/4484.smt2 new file mode 100644 index 000000000..f2f11295b --- /dev/null +++ b/test/regress/regress0/unconstrained/4484.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --unconstrained-simp +; EXPECT: unsat +(set-logic QF_NIRA) +(set-info :status unsat) +(declare-fun a () Real) +(assert (= (to_int a) 2)) +(assert (= (to_int (/ a 2.0)) 2)) +(check-sat) diff --git a/test/regress/regress0/unconstrained/4486.smt2 b/test/regress/regress0/unconstrained/4486.smt2 new file mode 100644 index 000000000..01771ce66 --- /dev/null +++ b/test/regress/regress0/unconstrained/4486.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --unconstrained-simp +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Real) +(assert (is_int x)) +(assert (is_int (+ x 1))) +(check-sat) diff --git a/test/regress/regress1/arith/bug547.1.smt2 b/test/regress/regress1/arith/bug547.1.smt2 index 38d1dfcb1..75894eb60 100644 --- a/test/regress/regress1/arith/bug547.1.smt2 +++ b/test/regress/regress1/arith/bug547.1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --rewrite-divk --nl-ext-tplanes +; COMMAND-LINE: --nl-ext-tplanes --quiet ; EXPECT: sat (set-logic QF_NIA) (declare-fun x () Int) diff --git a/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 index 3d932a076..07f2dae6a 100644 --- a/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 +++ b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) (declare-fun t () Int) diff --git a/test/regress/regress1/bv/cmu-rdk-3.smt2 b/test/regress/regress1/bv/cmu-rdk-3.smt2 index 9e7733889..742dd593b 100644 --- a/test/regress/regress1/bv/cmu-rdk-3.smt2 +++ b/test/regress/regress1/bv/cmu-rdk-3.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/bv/issue3776.smt2 b/test/regress/regress1/bv/issue3776.smt2 index 30c034c70..3e86a4974 100644 --- a/test/regress/regress1/bv/issue3776.smt2 +++ b/test/regress/regress1/bv/issue3776.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: sat (set-logic QF_BVLIA) +(set-info :status sat) (declare-fun t () Int) (assert (= t (bv2nat ((_ int2bv 1) t)))) (check-sat) diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 index 0618e28cb..dd9cb6886 100644 --- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk +; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 index 07f1e6674..ea5a5e4b7 100644 --- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk +; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress1/fmf/issue3626.smt2 b/test/regress/regress1/fmf/issue3626.smt2 index 9f27dee01..25dc80223 100644 --- a/test/regress/regress1/fmf/issue3626.smt2 +++ b/test/regress/regress1/fmf/issue3626.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-bound +; COMMAND-LINE: --fmf-bound --no-cegqi ; EXPECT: sat (set-logic ALL) (assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0)))) diff --git a/test/regress/regress1/nl/issue3441.smt2 b/test/regress/regress1/nl/issue3441.smt2 index 19fe98bc5..6be4e7d7e 100644 --- a/test/regress/regress1/nl/issue3441.smt2 +++ b/test/regress/regress1/nl/issue3441.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --quiet +; EXPECT: sat (set-logic QF_NIA) (set-info :status sat) (declare-fun a () Int) diff --git a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 index 8aa8793df..21f26df2d 100644 --- a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 +++ b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --quiet
+; EXPECT: sat
(set-logic QF_UFNRA)
(set-option :snorm-infer-eq true)
(set-info :status sat)
diff --git a/test/regress/regress1/push-pop/model-unsound-ania.smt2 b/test/regress/regress1/push-pop/model-unsound-ania.smt2 new file mode 100644 index 000000000..6f7f2752a --- /dev/null +++ b/test/regress/regress1/push-pop/model-unsound-ania.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_ANIA) +(declare-fun _substvar_16_ () Int) +(push 1) +(assert (not (= (mod _substvar_16_ 2) 0))) +(check-sat) +(pop 1) +(assert (= (- (mod _substvar_16_ 2) 2) 0)) +(check-sat) diff --git a/test/regress/regress1/strings/chapman150408.smt2 b/test/regress/regress1/strings/chapman150408.smt2 index f03718556..e6047498e 100644 --- a/test/regress/regress1/strings/chapman150408.smt2 +++ b/test/regress/regress1/strings/chapman150408.smt2 @@ -1,7 +1,6 @@ (set-logic SLIA) (set-info :status sat) (set-option :strings-exp true) -(set-option :rewrite-divk true) (declare-fun string () String) (assert (and (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0) diff --git a/test/regress/regress1/strings/cmu-substr-rw.smt2 b/test/regress/regress1/strings/cmu-substr-rw.smt2 index 20bf979dd..a4d649d7f 100644 --- a/test/regress/regress1/strings/cmu-substr-rw.smt2 +++ b/test/regress/regress1/strings/cmu-substr-rw.smt2 @@ -1,8 +1,6 @@ (set-logic ALL_SUPPORTED) (set-info :status sat) (set-option :strings-exp true) -;(set-option :produce-models true) -;(set-option :rewrite-divk true) (declare-fun uri () String) diff --git a/test/regress/regress1/strings/crash-1019.smt2 b/test/regress/regress1/strings/crash-1019.smt2 index 9f2e99b02..317840ddb 100644 --- a/test/regress/regress1/strings/crash-1019.smt2 +++ b/test/regress/regress1/strings/crash-1019.smt2 @@ -1,6 +1,5 @@ (set-logic ALL_SUPPORTED) (set-option :strings-exp true) -(set-option :rewrite-divk true) (set-info :status unsat) (declare-fun s () String) diff --git a/test/regress/regress2/bug674.smt2 b/test/regress/regress2/bug674.smt2 index 31eaa5aba..cce0c963a 100644 --- a/test/regress/regress2/bug674.smt2 +++ b/test/regress/regress2/bug674.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --quant-ind --incremental --rewrite-divk +; COMMAND-LINE: --quant-ind --incremental (set-logic ALL_SUPPORTED) (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil)))) (define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite ((_ is nil) l1) l2 (cons (head l1) (app (tail l1) l2)))) diff --git a/test/regress/regress2/strings/cmi-split-cm-fail.smt2 b/test/regress/regress2/strings/cmi-split-cm-fail.smt2 index e2ae94a27..4782fa7f8 100644 --- a/test/regress/regress2/strings/cmi-split-cm-fail.smt2 +++ b/test/regress/regress2/strings/cmi-split-cm-fail.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp --rewrite-divk +; COMMAND-LINE: --strings-exp ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic QF_SLIA) |