summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/arith_preprocess.cpp5
-rw-r--r--src/theory/arith/arith_preprocess.h7
-rw-r--r--src/theory/arith/operator_elim.cpp33
-rw-r--r--src/theory/arith/operator_elim.h6
-rw-r--r--src/theory/arith/theory_arith.cpp11
-rw-r--r--src/theory/arith/theory_arith.h6
6 files changed, 53 insertions, 15 deletions
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 577407c07..142f02eab 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -25,7 +25,10 @@ ArithPreprocess::ArithPreprocess(ArithState& state,
: d_im(im), d_opElim(pnm, info), d_reduced(state.getUserContext())
{
}
-TrustNode ArithPreprocess::eliminate(TNode n) { return d_opElim.eliminate(n); }
+TrustNode ArithPreprocess::eliminate(TNode n, bool partialOnly)
+{
+ return d_opElim.eliminate(n, partialOnly);
+}
bool ArithPreprocess::reduceAssertion(TNode atom)
{
context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it =
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index 165209bd9..622357e73 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -46,8 +46,13 @@ class ArithPreprocess
* Call eliminate operators on formula n, return the resulting trust node,
* which is of TrustNodeKind REWRITE and whose node is the result of
* eliminating extended operators from n.
+ *
+ * @param n The node to eliminate operators from
+ * @param partialOnly Whether we are eliminating partial operators only.
+ * @return the trust node proving (= n nr) where nr is the return of
+ * eliminating operators in n, or the null trust node if n was unchanged.
*/
- TrustNode eliminate(TNode n);
+ TrustNode eliminate(TNode n, bool partialOnly = false);
/**
* Reduce assertion. This sends a lemma via the inference manager if atom
* contains any extended operators. When applicable, the lemma is of the form:
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 4d4c4a6f5..fbd1798cd 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -46,21 +46,23 @@ void OperatorElim::checkNonLinearLogic(Node term)
}
}
-TrustNode OperatorElim::eliminate(Node n)
+TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
{
TConvProofGenerator* tg = nullptr;
- Node nn = eliminateOperators(n, tg);
+ Node nn = eliminateOperators(n, tg, partialOnly);
if (nn != n)
{
// since elimination may introduce new operators to eliminate, we must
// recursively eliminate result
- Node nnr = eliminateOperatorsRec(nn, tg);
+ Node nnr = eliminateOperatorsRec(nn, tg, partialOnly);
return TrustNode::mkTrustRewrite(n, nnr, nullptr);
}
return TrustNode::null();
}
-Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
+Node OperatorElim::eliminateOperatorsRec(Node n,
+ TConvProofGenerator* tg,
+ bool partialOnly)
{
Trace("arith-elim") << "Begin elim: " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
@@ -108,12 +110,12 @@ Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
{
ret = nm->mkNode(cur.getKind(), children);
}
- Node retElim = eliminateOperators(ret, tg);
+ Node retElim = eliminateOperators(ret, tg, partialOnly);
if (retElim != ret)
{
// recursively eliminate operators in result, since some eliminations
// are defined in terms of other non-standard operators.
- ret = eliminateOperatorsRec(retElim, tg);
+ ret = eliminateOperatorsRec(retElim, tg, partialOnly);
}
visited[cur] = ret;
}
@@ -123,7 +125,9 @@ Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
return visited[n];
}
-Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
+Node OperatorElim::eliminateOperators(Node node,
+ TConvProofGenerator* tg,
+ bool partialOnly)
{
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
@@ -143,6 +147,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
case TO_INTEGER:
case IS_INTEGER:
{
+ if (partialOnly)
+ {
+ // not eliminating total operators
+ return node;
+ }
Node toIntSkolem;
std::map<Node, Node>::const_iterator it = d_to_int_skolem.find(node[0]);
if (it == d_to_int_skolem.end())
@@ -180,6 +189,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
case INTS_DIVISION_TOTAL:
case INTS_MODULUS_TOTAL:
{
+ if (partialOnly)
+ {
+ // not eliminating total operators
+ return node;
+ }
Node den = Rewriter::rewrite(node[1]);
Node num = Rewriter::rewrite(node[0]);
Node intVar;
@@ -283,6 +297,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
}
case DIVISION_TOTAL:
{
+ if (partialOnly)
+ {
+ // not eliminating total operators
+ return node;
+ }
Node num = Rewriter::rewrite(node[0]);
Node den = Rewriter::rewrite(node[1]);
if (den.isConst())
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index c7b55caf1..bca80ea4d 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -37,7 +37,7 @@ class OperatorElim : public EagerProofGenerator
* transcendental functions), then we replace it by a form that eliminates
* that operator. This may involve the introduction of witness terms.
*/
- TrustNode eliminate(Node n);
+ TrustNode eliminate(Node n, bool partialOnly = false);
/**
* Get axiom for term n. This returns the axiom that this class uses to
* eliminate the term n, which is determined by its top-most symbol.
@@ -101,7 +101,7 @@ class OperatorElim : public EagerProofGenerator
* @param n The node to eliminate operators from.
* @return The (single step) eliminated form of n.
*/
- Node eliminateOperators(Node n, TConvProofGenerator* tg);
+ Node eliminateOperators(Node n, TConvProofGenerator* tg, bool partialOnly);
/**
* Recursively ensure that n has no non-standard operators. This applies
* the above method on all subterms of n.
@@ -109,7 +109,7 @@ class OperatorElim : public EagerProofGenerator
* @param n The node to eliminate operators from.
* @return The eliminated form of n.
*/
- Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg);
+ Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg, bool partialOnly);
/** get arithmetic skolem
*
* Returns the Skolem in the above map for the given id, creating it if it
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 247772897..b8cead4fc 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -97,6 +97,12 @@ void TheoryArith::preRegisterTerm(TNode n)
d_internal->preRegisterTerm(n);
}
+TrustNode TheoryArith::expandDefinition(Node node)
+{
+ // call eliminate operators, to eliminate partial operators only
+ return d_arithPreproc.eliminate(node, true);
+}
+
void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
TrustNode TheoryArith::ppRewrite(TNode atom)
@@ -140,8 +146,9 @@ TrustNode TheoryArith::ppRewriteTerms(TNode n)
// 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
- return d_arithPreproc.eliminate(n);
+ // call eliminate operators. In contrast to expandDefinitions, we eliminate
+ // *all* extended arithmetic operators here, including total ones.
+ return d_arithPreproc.eliminate(n, false);
}
Theory::PPAssertStatus TheoryArith::ppAssert(
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e6029faef..e26ff51ef 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -68,7 +68,11 @@ class TheoryArith : public Theory {
/** finish initialization */
void finishInit() override;
//--------------------------------- end initialization
-
+ /**
+ * Expand definition, which eliminates extended operators like div/mod in
+ * the given node.
+ */
+ TrustNode expandDefinition(Node node) override;
/**
* Does non-context dependent setup for a node connected to a theory.
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback