This class will be undergoing further refactoring for the sake of proofs.
This also makes several classes of skolems context-independent instead of user-context-dependent, since this is the expected policy for skolems. Note these skolems will eventually be incorporated into the SkolemManager utility.
theory/arith/nl/transcendental_solver.h
theory/arith/normal_form.cpp
theory/arith/normal_form.h
+ theory/arith/operator_elim.cpp
+ theory/arith/operator_elim.h
theory/arith/partial_model.cpp
theory/arith/partial_model.h
theory/arith/simplex.cpp
--- /dev/null
+/********************* */
+/*! \file operator_elim.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Tim King, Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of operator elimination for arithmetic
+ **/
+
+#include "theory/arith/operator_elim.h"
+
+#include "expr/skolem_manager.h"
+#include "options/arith_options.h"
+#include "smt/logic_exception.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+OperatorElim::OperatorElim(const LogicInfo& info) : d_info(info) {}
+
+void OperatorElim::checkNonLinearLogic(Node term)
+{
+ if (d_info.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 << std::endl;
+ throw LogicException(serr.str());
+ }
+}
+
+Node OperatorElim::eliminateOperatorsRec(Node n)
+{
+ 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())
+ {
+ 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);
+ }
+ visited[cur] = ret;
+ }
+ } while (!visit.empty());
+ Assert(visited.find(n) != visited.end());
+ Assert(!visited.find(n)->second.isNull());
+ return visited[n];
+}
+
+Node OperatorElim::eliminateOperators(Node node)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+
+ Kind k = node.getKind();
+ switch (k)
+ {
+ case TANGENT:
+ case COSECANT:
+ case SECANT:
+ case COTANGENT:
+ {
+ // these are eliminated by rewriting
+ return Rewriter::rewrite(node);
+ break;
+ }
+ case TO_INTEGER:
+ case IS_INTEGER:
+ {
+ Node toIntSkolem;
+ std::map<Node, Node>::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(MINUS, node[0], v);
+ Node lem = mkInRange(diff, zero, one);
+ toIntSkolem = sm->mkSkolem(
+ v, lem, "toInt", "a conversion of a Real term to its Integer part");
+ toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem);
+ d_to_int_skolem[node[0]] = toIntSkolem;
+ }
+ else
+ {
+ toIntSkolem = (*it).second;
+ }
+ if (k == IS_INTEGER)
+ {
+ return nm->mkNode(EQUAL, node[0], toIntSkolem);
+ }
+ Assert(k == TO_INTEGER);
+ return toIntSkolem;
+ }
+
+ case INTS_DIVISION_TOTAL:
+ case INTS_MODULUS_TOTAL:
+ {
+ Node den = Rewriter::rewrite(node[1]);
+ Node num = Rewriter::rewrite(node[0]);
+ Node intVar;
+ Node rw = nm->mkNode(k, num, den);
+ std::map<Node, Node>::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
+ {
+ 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 = sm->mkSkolem(
+ v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
+ intVar = SkolemManager::getWitnessForm(intVar);
+ d_int_div_skolem[rw] = intVar;
+ }
+ else
+ {
+ intVar = (*it).second;
+ }
+ if (k == INTS_MODULUS_TOTAL)
+ {
+ Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
+ return nn;
+ }
+ else
+ {
+ return intVar;
+ }
+ break;
+ }
+ case 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);
+ std::map<Node, Node>::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 = sm->mkSkolem(
+ v, lem, "nonlinearDiv", "the result of a non-linear div term");
+ var = SkolemManager::getWitnessForm(var);
+ d_div_skolem[rw] = var;
+ }
+ else
+ {
+ var = (*it).second;
+ }
+ return var;
+ break;
+ }
+ case DIVISION:
+ {
+ Node num = Rewriter::rewrite(node[0]);
+ Node den = Rewriter::rewrite(node[1]);
+ Node ret = nm->mkNode(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(EQUAL, den, nm->mkConst(Rational(0)));
+ ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret);
+ }
+ return ret;
+ break;
+ }
+
+ case INTS_DIVISION:
+ {
+ // partial function: integer div
+ Node num = Rewriter::rewrite(node[0]);
+ Node den = Rewriter::rewrite(node[1]);
+ Node ret = nm->mkNode(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(EQUAL, den, nm->mkConst(Rational(0)));
+ ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret);
+ }
+ return ret;
+ break;
+ }
+
+ case INTS_MODULUS:
+ {
+ // partial function: mod
+ Node num = Rewriter::rewrite(node[0]);
+ Node den = Rewriter::rewrite(node[1]);
+ Node ret = nm->mkNode(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(EQUAL, den, nm->mkConst(Rational(0)));
+ ret = nm->mkNode(ITE, denEq0, modZeroNum, ret);
+ }
+ return ret;
+ break;
+ }
+
+ case ABS:
+ {
+ return nm->mkNode(ITE,
+ nm->mkNode(LT, node[0], nm->mkConst(Rational(0))),
+ nm->mkNode(UMINUS, node[0]),
+ node[0]);
+ break;
+ }
+ case SQRT:
+ case ARCSINE:
+ case ARCCOSINE:
+ case ARCTANGENT:
+ case ARCCOSECANT:
+ case ARCSECANT:
+ case ARCCOTANGENT:
+ {
+ checkNonLinearLogic(node);
+ // eliminate inverse functions here
+ std::map<Node, Node>::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 == SQRT)
+ {
+ Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
+ Node uf = skolemApp.eqNode(var);
+ Node nonNeg =
+ nm->mkNode(AND, nm->mkNode(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(ITE,
+ nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
+ nonNeg,
+ uf);
+ }
+ else
+ {
+ Node pi = mkPi();
+
+ // range of the skolem
+ Node rlem;
+ if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
+ {
+ Node half = nm->mkConst(Rational(1) / Rational(2));
+ Node pi2 = nm->mkNode(MULT, half, pi);
+ Node npi2 = nm->mkNode(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 == ARCSINE
+ ? SINE
+ : (k == ARCCOSINE
+ ? COSINE
+ : (k == ARCTANGENT
+ ? TANGENT
+ : (k == ARCCOSECANT
+ ? COSECANT
+ : (k == ARCSECANT ? SECANT
+ : COTANGENT))));
+ Node invTerm = nm->mkNode(rk, var);
+ lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
+ }
+ Assert(!lem.isNull());
+ Node ret = sm->mkSkolem(
+ var,
+ lem,
+ "tfk",
+ "Skolem to eliminate a non-standard transcendental function");
+ ret = SkolemManager::getWitnessForm(ret);
+ d_nlin_inverse_skolem[node] = ret;
+ return ret;
+ }
+ return (*it).second;
+ break;
+ }
+
+ default: break;
+ }
+ return node;
+}
+
+Node OperatorElim::getArithSkolem(ArithSkolemId asi)
+{
+ std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
+ if (it == d_arith_skolem.end())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+
+ TypeNode tn;
+ std::string name;
+ std::string desc;
+ switch (asi)
+ {
+ case ArithSkolemId::DIV_BY_ZERO:
+ tn = nm->realType();
+ name = std::string("divByZero");
+ desc = std::string("partial real division");
+ break;
+ case ArithSkolemId::INT_DIV_BY_ZERO:
+ tn = nm->integerType();
+ name = std::string("intDivByZero");
+ desc = std::string("partial int division");
+ break;
+ case ArithSkolemId::MOD_BY_ZERO:
+ tn = nm->integerType();
+ name = std::string("modZero");
+ desc = std::string("partial modulus");
+ break;
+ case ArithSkolemId::SQRT:
+ tn = nm->realType();
+ name = std::string("sqrtUf");
+ desc = std::string("partial sqrt");
+ break;
+ default: Unhandled();
+ }
+
+ Node skolem;
+ if (options::arithNoPartialFun())
+ {
+ // partial function: division
+ skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME);
+ }
+ else
+ {
+ // partial function: division
+ skolem = nm->mkSkolem(name,
+ nm->mkFunctionType(tn, tn),
+ desc,
+ NodeManager::SKOLEM_EXACT_NAME);
+ }
+ d_arith_skolem[asi] = skolem;
+ return skolem;
+ }
+ return it->second;
+}
+
+Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi)
+{
+ Node skolem = getArithSkolem(asi);
+ if (!options::arithNoPartialFun())
+ {
+ skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
+ }
+ return skolem;
+}
+
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file operator_elim.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Operator elimination for arithmetic
+ **/
+
+#pragma once
+
+#include <map>
+
+#include "expr/node.h"
+#include "theory/logic_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class OperatorElim
+{
+ public:
+ OperatorElim(const LogicInfo& info);
+ ~OperatorElim() {}
+ /**
+ * 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);
+
+ private:
+ /** Logic info of the owner of this class */
+ const LogicInfo& d_info;
+
+ /**
+ * Maps for Skolems for to-integer, real/integer div-by-k, and inverse
+ * non-linear operators that are introduced during ppRewriteTerms.
+ */
+ std::map<Node, Node> d_to_int_skolem;
+ std::map<Node, Node> d_div_skolem;
+ std::map<Node, Node> d_int_div_skolem;
+ std::map<Node, Node> d_nlin_inverse_skolem;
+
+ /** Arithmetic skolem identifier */
+ enum class ArithSkolemId
+ {
+ /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
+ DIV_BY_ZERO,
+ /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
+ INT_DIV_BY_ZERO,
+ /* an uninterpreted function f s.t. f(x) = x mod 0 */
+ MOD_BY_ZERO,
+ /* an uninterpreted function f s.t. f(x) = sqrt(x) */
+ SQRT,
+ };
+
+ /**
+ * Function symbols used to implement:
+ * (1) Uninterpreted division-by-zero semantics. Needed to deal with partial
+ * division function ("/"),
+ * (2) Uninterpreted int-division-by-zero semantics. Needed to deal with
+ * partial function "div",
+ * (3) Uninterpreted mod-zero semantics. Needed to deal with partial
+ * function "mod".
+ *
+ * If the option arithNoPartialFun() is enabled, then the range of this map
+ * stores Skolem constants instead of Skolem functions, meaning that the
+ * function-ness of e.g. division by zero is ignored.
+ */
+ std::map<ArithSkolemId, Node> d_arith_skolem;
+ /** get arithmetic skolem
+ *
+ * Returns the Skolem in the above map for the given id, creating it if it
+ * does not already exist.
+ */
+ Node getArithSkolem(ArithSkolemId asi);
+ /** get arithmetic skolem application
+ *
+ * By default, this returns the term f( n ), where f is the Skolem function
+ * for the identifier asi.
+ *
+ * If the option arithNoPartialFun is enabled, this returns f, where f is
+ * the Skolem constant for the identifier asi.
+ */
+ Node getArithSkolemApp(Node n, ArithSkolemId asi);
+
+ /**
+ * Called when a non-linear term n is given to this class. Throw an exception
+ * if the logic is linear.
+ */
+ void checkNonLinearLogic(Node term);
+};
+
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
d_solveIntMaybeHelp(0u),
d_solveIntAttempts(0u),
d_statistics(),
- d_to_int_skolem(u),
- d_div_skolem(u),
- d_int_div_skolem(u),
- d_nlin_inverse_skolem(u)
+ d_opElim(logicInfo)
{
if( options::nlExt() ){
d_nonlinearExtension = new nl::NonlinearExtension(
// 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);
+ Node nn = d_opElim.eliminateOperators(n);
if (nn != n)
{
// since elimination may introduce new operators to eliminate, we must
// recursively eliminate result
- return eliminateOperatorsRec(nn);
+ return d_opElim.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());
- }
-}
-
-Node TheoryArithPrivate::eliminateOperatorsRec(Node n)
-{
- 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())
- {
- 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);
- }
- 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();
- SkolemManager* sm = nm->getSkolemManager();
-
- 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;
- }
- 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 = sm->mkSkolem(
- v, lem, "toInt", "a conversion of a Real term to its Integer part");
- toIntSkolem = SkolemManager::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;
- }
-
- 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
- {
- 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 = sm->mkSkolem(
- v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
- intVar = SkolemManager::getWitnessForm(intVar);
- d_int_div_skolem[rw] = intVar;
- }
- 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;
- }
- 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 = sm->mkSkolem(
- v, lem, "nonlinearDiv", "the result of a non-linear div term");
- var = SkolemManager::getWitnessForm(var);
- d_div_skolem[rw] = var;
- }
- else
- {
- var = (*it).second;
- }
- return var;
- break;
- }
- 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;
- }
-
- 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);
- }
- return ret;
- break;
- }
-
- 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 = sm->mkSkolem(
- var,
- lem,
- "tfk",
- "Skolem to eliminate a non-standard transcendental function");
- ret = SkolemManager::getWitnessForm(ret);
- d_nlin_inverse_skolem[node] = ret;
- return ret;
- }
- return (*it).second;
- break;
- }
-
- default: break;
- }
- return node;
-}
-
Node TheoryArithPrivate::ppRewrite(TNode atom) {
Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
Node TheoryArithPrivate::expandDefinition(Node node)
{
// call eliminate operators
- Node nn = eliminateOperators(node);
+ Node nn = d_opElim.eliminateOperators(node);
if (nn != node)
{
// since elimination may introduce new operators to eliminate, we must
// recursively eliminate result
- return eliminateOperatorsRec(nn);
+ return d_opElim.eliminateOperatorsRec(nn);
}
return node;
}
-Node TheoryArithPrivate::getArithSkolem(ArithSkolemId asi)
-{
- std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
- if (it == d_arith_skolem.end())
- {
- NodeManager* nm = NodeManager::currentNM();
-
- TypeNode tn;
- std::string name;
- std::string desc;
- switch (asi)
- {
- case ArithSkolemId::DIV_BY_ZERO:
- tn = nm->realType();
- name = std::string("divByZero");
- desc = std::string("partial real division");
- break;
- case ArithSkolemId::INT_DIV_BY_ZERO:
- tn = nm->integerType();
- name = std::string("intDivByZero");
- desc = std::string("partial int division");
- break;
- case ArithSkolemId::MOD_BY_ZERO:
- tn = nm->integerType();
- name = std::string("modZero");
- desc = std::string("partial modulus");
- break;
- case ArithSkolemId::SQRT:
- tn = nm->realType();
- name = std::string("sqrtUf");
- desc = std::string("partial sqrt");
- break;
- default: Unhandled();
- }
-
- Node skolem;
- if (options::arithNoPartialFun())
- {
- // partial function: division
- skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME);
- }
- else
- {
- // partial function: division
- skolem = nm->mkSkolem(name,
- nm->mkFunctionType(tn, tn),
- desc,
- NodeManager::SKOLEM_EXACT_NAME);
- }
- d_arith_skolem[asi] = skolem;
- return skolem;
- }
- return it->second;
-}
-
-Node TheoryArithPrivate::getArithSkolemApp(Node n, ArithSkolemId asi)
-{
- Node skolem = getArithSkolem(asi);
- if (!options::arithNoPartialFun())
- {
- skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
- }
- return skolem;
-}
-
-// InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const
-// InferBoundsParameters& param){
-// Node t = Rewriter::rewrite(term);
-// Assert(Polynomial::isMember(t));
-// Polynomial p = Polynomial::parsePolynomial(t);
-// if(p.containsConstant()){
-// Constant c = p.getHead().getConstant();
-// if(p.isConstant()){
-// InferBoundsResult res(t, param.findLowerBound());
-// res.setBound((DeltaRational)c.getValue(), mkBoolNode(true));
-// return res;
-// }else{
-// Polynomial tail = p.getTail();
-// InferBoundsResult res = inferBound(tail.getNode(), param);
-// if(res.foundBound()){
-// DeltaRational newBound = res.getValue() + c.getValue();
-// if(tail.isIntegral()){
-// Integer asInt = (param.findLowerBound()) ? newBound.ceiling() :
-// newBound.floor(); newBound = DeltaRational(asInt);
-// }
-// res.setBound(newBound, res.getExplanation());
-// }
-// return res;
-// }
-// }else if(param.findLowerBound()){
-// InferBoundsParameters find_ub = param;
-// find_ub.setFindUpperBound();
-// if(param.useThreshold()){
-// find_ub.setThreshold(- param.getThreshold() );
-// }
-// Polynomial negP = -p;
-// InferBoundsResult res = inferBound(negP.getNode(), find_ub);
-// res.setFindLowerBound();
-// if(res.foundBound()){
-// res.setTerm(p.getNode());
-// res.setBound(-res.getValue(), res.getExplanation());
-// }
-// return res;
-// }else{
-// Assert(param.findUpperBound());
-// // does not contain a constant
-// switch(param.getEffort()){
-// case InferBoundsParameters::Lookup:
-// return inferUpperBoundLookup(t, param);
-// case InferBoundsParameters::Simplex:
-// return inferUpperBoundSimplex(t, param);
-// case InferBoundsParameters::LookupAndSimplexOnFailure:
-// case InferBoundsParameters::TryBoth:
-// {
-// InferBoundsResult lookup = inferUpperBoundLookup(t, param);
-// if(lookup.foundBound()){
-// if(param.getEffort() ==
-// InferBoundsParameters::LookupAndSimplexOnFailure ||
-// lookup.boundIsOptimal()){
-// return lookup;
-// }
-// }
-// InferBoundsResult simplex = inferUpperBoundSimplex(t, param);
-// if(lookup.foundBound() && simplex.foundBound()){
-// return (lookup.getValue() <= simplex.getValue()) ? lookup :
-// simplex;
-// }else if(lookup.foundBound()){
-// return lookup;
-// }else{
-// return simplex;
-// }
-// }
-// default:
-// Unreachable();
-// return InferBoundsResult();
-// }
-// }
-// }
-
std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
using namespace inferbounds;
#include "smt/logic_exception.h"
#include "smt_util/boolean_simplification.h"
#include "theory/arith/arith_rewriter.h"
-#include "theory/arith/arith_rewriter.h"
#include "theory/arith/arith_static_learner.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/attempt_solution_simplex.h"
#include "theory/arith/congruence_manager.h"
#include "theory/arith/constraint.h"
-#include "theory/arith/constraint.h"
-#include "theory/arith/delta_rational.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/dio_solver.h"
#include "theory/arith/dual_simplex.h"
#include "theory/arith/infer_bounds.h"
#include "theory/arith/linear_equality.h"
#include "theory/arith/matrix.h"
-#include "theory/arith/matrix.h"
#include "theory/arith/normal_form.h"
-#include "theory/arith/partial_model.h"
+#include "theory/arith/operator_elim.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/simplex.h"
#include "theory/arith/soi_simplex.h"
// handle linear /, div, mod, and also is_int, to_int
Node ppRewriteTerms(TNode atom);
- /**
- * 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(TheoryArith& containing,
+ context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo);
~TheoryArithPrivate();
TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
Statistics d_statistics;
- enum class ArithSkolemId
- {
- /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
- DIV_BY_ZERO,
- /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
- INT_DIV_BY_ZERO,
- /* an uninterpreted function f s.t. f(x) = x mod 0 */
- MOD_BY_ZERO,
- /* an uninterpreted function f s.t. f(x) = sqrt(x) */
- SQRT,
- };
-
- /**
- * Function symbols used to implement:
- * (1) Uninterpreted division-by-zero semantics. Needed to deal with partial
- * division function ("/"),
- * (2) Uninterpreted int-division-by-zero semantics. Needed to deal with
- * partial function "div",
- * (3) Uninterpreted mod-zero semantics. Needed to deal with partial
- * function "mod".
- *
- * If the option arithNoPartialFun() is enabled, then the range of this map
- * stores Skolem constants instead of Skolem functions, meaning that the
- * function-ness of e.g. division by zero is ignored.
- */
- std::map<ArithSkolemId, Node> d_arith_skolem;
- /** get arithmetic skolem
- *
- * Returns the Skolem in the above map for the given id, creating it if it
- * does not already exist.
- */
- Node getArithSkolem(ArithSkolemId asi);
- /** get arithmetic skolem application
- *
- * By default, this returns the term f( n ), where f is the Skolem function
- * for the identifier asi.
- *
- * If the option arithNoPartialFun is enabled, this returns f, where f is
- * the Skolem constant for the identifier asi.
- */
- Node getArithSkolemApp(Node n, ArithSkolemId asi);
-
- /**
- * Maps for Skolems for to-integer, real/integer div-by-k, and inverse
- * non-linear operators that are introduced during ppRewriteTerms.
- */
- typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
- NodeMap d_to_int_skolem;
- NodeMap d_div_skolem;
- NodeMap d_int_div_skolem;
- NodeMap d_nlin_inverse_skolem;
-
/** The theory rewriter for this theory. */
ArithRewriter d_rewriter;
+ /** The operator elimination utility */
+ OperatorElim d_opElim;
};/* class TheoryArithPrivate */
}/* CVC4::theory::arith namespace */
projects / cvc5.git / commitdiff