summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/operator_elim.cpp65
-rw-r--r--src/theory/arith/operator_elim.h24
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback