diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_preprocess.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/arith_preprocess.h | 7 | ||||
-rw-r--r-- | src/theory/arith/operator_elim.cpp | 33 | ||||
-rw-r--r-- | src/theory/arith/operator_elim.h | 6 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 11 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 6 |
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. */ |