diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/operator_elim.cpp | 65 | ||||
-rw-r--r-- | src/theory/arith/operator_elim.h | 24 |
2 files changed, 29 insertions, 60 deletions
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 600724f33..85db55f3f 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -18,7 +18,6 @@ #include "expr/attribute.h" #include "expr/bound_var_manager.h" -#include "expr/skolem_manager.h" #include "expr/term_conversion_proof_generator.h" #include "options/arith_options.h" #include "smt/logic_exception.h" @@ -265,7 +264,7 @@ Node OperatorElim::eliminateOperators(Node node, if (!den.isConst() || den.getConst<Rational>().sgn() == 0) { checkNonLinearLogic(node); - Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO); + Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO); Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0))); ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret); } @@ -283,7 +282,7 @@ Node OperatorElim::eliminateOperators(Node node, { checkNonLinearLogic(node); Node intDivByZeroNum = - getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO); + getArithSkolemApp(num, SkolemFunId::INT_DIV_BY_ZERO); Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0))); ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret); } @@ -300,7 +299,7 @@ Node OperatorElim::eliminateOperators(Node node, if (!den.isConst() || den.getConst<Rational>().sgn() == 0) { checkNonLinearLogic(node); - Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO); + Node modZeroNum = getArithSkolemApp(num, SkolemFunId::MOD_BY_ZERO); Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0))); ret = nm->mkNode(ITE, denEq0, modZeroNum, ret); } @@ -336,7 +335,7 @@ Node OperatorElim::eliminateOperators(Node node, Node lem; if (k == SQRT) { - Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT); + Node skolemApp = getArithSkolemApp(node[0], SkolemFunId::SQRT); Node uf = skolemApp.eqNode(var); Node nonNeg = nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf); @@ -407,64 +406,44 @@ Node OperatorElim::eliminateOperators(Node node, Node OperatorElim::getAxiomFor(Node n) { return Node::null(); } -Node OperatorElim::getArithSkolem(ArithSkolemId asi) +Node OperatorElim::getArithSkolem(SkolemFunId id) { - std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi); - if (it == d_arith_skolem.end()) + std::map<SkolemFunId, Node>::iterator it = d_arithSkolem.find(id); + if (it == d_arithSkolem.end()) { NodeManager* nm = NodeManager::currentNM(); - TypeNode tn; - std::string name; - std::string desc; - switch (asi) + if (id == SkolemFunId::DIV_BY_ZERO || id == SkolemFunId::SQRT) { - 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(); + tn = nm->realType(); + } + else + { + tn = nm->integerType(); } - Node skolem; + SkolemManager* sm = nm->getSkolemManager(); if (options::arithNoPartialFun()) { - // partial function: division - skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME); + // partial function: division, where we treat the skolem function as + // a constant + skolem = sm->mkSkolemFunction(id, tn); } else { // partial function: division - skolem = nm->mkSkolem(name, - nm->mkFunctionType(tn, tn), - desc, - NodeManager::SKOLEM_EXACT_NAME); + skolem = sm->mkSkolemFunction(id, nm->mkFunctionType(tn, tn)); } - d_arith_skolem[asi] = skolem; + // cache it + d_arithSkolem[id] = skolem; return skolem; } return it->second; } -Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi) +Node OperatorElim::getArithSkolemApp(Node n, SkolemFunId id) { - Node skolem = getArithSkolem(asi); + Node skolem = getArithSkolem(id); if (!options::arithNoPartialFun()) { skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n); diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 1b2f7190e..ec29bcf49 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -17,6 +17,7 @@ #include <map> #include "expr/node.h" +#include "expr/skolem_manager.h" #include "theory/eager_proof_generator.h" #include "theory/logic_info.h" #include "theory/skolem_lemma.h" @@ -59,20 +60,6 @@ class OperatorElim : public EagerProofGenerator private: /** Logic info of the owner of this class */ const LogicInfo& d_info; - - /** 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 @@ -85,8 +72,11 @@ class OperatorElim : public EagerProofGenerator * 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. + * + * Note that this cache is used only for performance reasons. Conceptually, + * these skolem functions actually live in SkolemManager. */ - std::map<ArithSkolemId, Node> d_arith_skolem; + std::map<SkolemFunId, Node> d_arithSkolem; /** * 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 @@ -113,7 +103,7 @@ class OperatorElim : public EagerProofGenerator * Returns the Skolem in the above map for the given id, creating it if it * does not already exist. */ - Node getArithSkolem(ArithSkolemId asi); + Node getArithSkolem(SkolemFunId asi); /** * Make the witness term, which creates a witness term based on the skolem * manager with this class as a proof generator. @@ -131,7 +121,7 @@ class OperatorElim : public EagerProofGenerator * 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); + Node getArithSkolemApp(Node n, SkolemFunId asi); /** * Called when a non-linear term n is given to this class. Throw an exception |