diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/operator_elim.cpp | 124 | ||||
-rw-r--r-- | src/theory/arith/operator_elim.h | 16 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 10 |
3 files changed, 34 insertions, 116 deletions
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index fbd1798cd..e34c0110e 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -52,86 +52,16 @@ TrustNode OperatorElim::eliminate(Node n, bool partialOnly) 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, partialOnly); - return TrustNode::mkTrustRewrite(n, nnr, nullptr); + return TrustNode::mkTrustRewrite(n, nn, nullptr); } return TrustNode::null(); } -Node OperatorElim::eliminateOperatorsRec(Node n, - TConvProofGenerator* tg, - bool partialOnly) -{ - 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, 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, partialOnly); - } - 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, TConvProofGenerator* tg, bool partialOnly) { NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - Kind k = node.getKind(); switch (k) { @@ -164,14 +94,8 @@ Node OperatorElim::eliminateOperators(Node node, 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", - NodeManager::SKOLEM_DEFAULT, - this, - true); + toIntSkolem = mkWitnessTerm( + v, lem, "toInt", "a conversion of a Real term to its Integer part"); d_to_int_skolem[node[0]] = toIntSkolem; } else @@ -271,13 +195,8 @@ Node OperatorElim::eliminateOperators(Node node, nm->mkNode( PLUS, v, nm->mkConst(Rational(-1)))))))); } - intVar = sm->mkSkolem(v, - lem, - "linearIntDiv", - "the result of an intdiv-by-k term", - NodeManager::SKOLEM_DEFAULT, - this, - true); + intVar = mkWitnessTerm( + v, lem, "linearIntDiv", "the result of an intdiv-by-k term"); d_int_div_skolem[rw] = intVar; } else @@ -321,13 +240,8 @@ Node OperatorElim::eliminateOperators(Node node, 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", - NodeManager::SKOLEM_DEFAULT, - this, - true); + var = mkWitnessTerm( + v, lem, "nonlinearDiv", "the result of a non-linear div term"); d_div_skolem[rw] = var; } else @@ -404,6 +318,11 @@ Node OperatorElim::eliminateOperators(Node node, case ARCSECANT: case ARCCOTANGENT: { + if (partialOnly) + { + // not eliminating total operators + return node; + } checkNonLinearLogic(node); // eliminate inverse functions here std::map<Node, Node>::const_iterator it = @@ -469,14 +388,11 @@ Node OperatorElim::eliminateOperators(Node node, lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0])); } Assert(!lem.isNull()); - Node ret = sm->mkSkolem( + Node ret = mkWitnessTerm( var, lem, "tfk", - "Skolem to eliminate a non-standard transcendental function", - NodeManager::SKOLEM_DEFAULT, - this, - true); + "Skolem to eliminate a non-standard transcendental function"); Assert(ret.getKind() == WITNESS); d_nlin_inverse_skolem[node] = ret; return ret; @@ -557,6 +473,18 @@ Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi) return skolem; } +Node OperatorElim::mkWitnessTerm(Node v, + Node pred, + const std::string& prefix, + const std::string& comment) +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node k = sm->mkSkolem( + v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this, true); + return k; +} + } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index bca80ea4d..cf5b9248c 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -102,20 +102,20 @@ class OperatorElim : public EagerProofGenerator * @return The (single step) eliminated form of n. */ 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. - * - * @param n The node to eliminate operators from. - * @return The eliminated form of n. - */ - 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 * does not already exist. */ Node getArithSkolem(ArithSkolemId asi); + /** + * Make the witness term, which creates a witness term based on the skolem + * manager with this class as a proof generator. + */ + Node mkWitnessTerm(Node v, + Node pred, + const std::string& prefix, + const std::string& comment); /** get arithmetic skolem application * * By default, this returns the term f( n ), where f is the Skolem function diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6de5c7221..9bca5e182 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -119,16 +119,6 @@ TrustNode TheoryArith::ppRewrite(TNode atom) Assert(atom[0].getType().isReal()); Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; - TrustNode tleq = ppRewriteTerms(leq); - TrustNode tgeq = ppRewriteTerms(geq); - if (!tleq.isNull()) - { - leq = tleq.getNode(); - } - if (!tgeq.isNull()) - { - geq = tgeq.getNode(); - } Node rewritten = Rewriter::rewrite(leq.andNode(geq)); Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; |