diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/operator_elim.cpp | 67 | ||||
-rw-r--r-- | src/theory/arith/operator_elim.h | 67 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 12 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 47 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 9 |
5 files changed, 122 insertions, 80 deletions
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 593fbd584..938fe0a47 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -27,7 +27,10 @@ namespace CVC4 { namespace theory { namespace arith { -OperatorElim::OperatorElim(const LogicInfo& info) : d_info(info) {} +OperatorElim::OperatorElim(ProofNodeManager* pnm, const LogicInfo& info) + : EagerProofGenerator(pnm), d_info(info) +{ +} void OperatorElim::checkNonLinearLogic(Node term) { @@ -43,7 +46,21 @@ void OperatorElim::checkNonLinearLogic(Node term) } } -Node OperatorElim::eliminateOperatorsRec(Node n) +TrustNode OperatorElim::eliminate(Node n) +{ + TConvProofGenerator* tg = nullptr; + Node nn = eliminateOperators(n, tg); + if (nn != n) + { + // since elimination may introduce new operators to eliminate, we must + // recursively eliminate result + Node nnr = eliminateOperatorsRec(nn, tg); + return TrustNode::mkTrustRewrite(n, nnr, nullptr); + } + return TrustNode::null(); +} + +Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg) { Trace("arith-elim") << "Begin elim: " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); @@ -91,12 +108,12 @@ Node OperatorElim::eliminateOperatorsRec(Node n) { ret = nm->mkNode(cur.getKind(), children); } - Node retElim = eliminateOperators(ret); + Node retElim = eliminateOperators(ret, tg); if (retElim != ret) { // recursively eliminate operators in result, since some eliminations // are defined in terms of other non-standard operators. - ret = eliminateOperatorsRec(retElim); + ret = eliminateOperatorsRec(retElim, tg); } visited[cur] = ret; } @@ -106,7 +123,7 @@ Node OperatorElim::eliminateOperatorsRec(Node n) return visited[n]; } -Node OperatorElim::eliminateOperators(Node node) +Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg) { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); @@ -138,9 +155,14 @@ 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"); - toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem); + toIntSkolem = + sm->mkSkolem(v, + lem, + "toInt", + "a conversion of a Real term to its Integer part", + NodeManager::SKOLEM_DEFAULT, + this, + true); d_to_int_skolem[node[0]] = toIntSkolem; } else @@ -235,9 +257,13 @@ 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"); - intVar = SkolemManager::getWitnessForm(intVar); + intVar = sm->mkSkolem(v, + lem, + "linearIntDiv", + "the result of an intdiv-by-k term", + NodeManager::SKOLEM_DEFAULT, + this, + true); d_int_div_skolem[rw] = intVar; } else @@ -276,9 +302,13 @@ 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"); - var = SkolemManager::getWitnessForm(var); + var = sm->mkSkolem(v, + lem, + "nonlinearDiv", + "the result of a non-linear div term", + NodeManager::SKOLEM_DEFAULT, + this, + true); d_div_skolem[rw] = var; } else @@ -424,8 +454,11 @@ Node OperatorElim::eliminateOperators(Node node) var, lem, "tfk", - "Skolem to eliminate a non-standard transcendental function"); - ret = SkolemManager::getWitnessForm(ret); + "Skolem to eliminate a non-standard transcendental function", + NodeManager::SKOLEM_DEFAULT, + this, + true); + Assert(ret.getKind() == WITNESS); d_nlin_inverse_skolem[node] = ret; return ret; } @@ -438,6 +471,8 @@ Node OperatorElim::eliminateOperators(Node node) return node; } +Node OperatorElim::getAxiomFor(Node n) { return Node::null(); } + Node OperatorElim::getArithSkolem(ArithSkolemId asi) { std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi); diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 2cdf9bc49..4646a6f13 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -17,43 +17,32 @@ #include <map> #include "expr/node.h" +#include "expr/term_conversion_proof_generator.h" +#include "theory/eager_proof_generator.h" #include "theory/logic_info.h" namespace CVC4 { namespace theory { namespace arith { -class OperatorElim +class OperatorElim : public EagerProofGenerator { public: - OperatorElim(const LogicInfo& info); + OperatorElim(ProofNodeManager* pnm, const LogicInfo& info); ~OperatorElim() {} + /** Eliminate operators in this term. + * + * 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 + * 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); /** - * 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 - * transcendental functions), then we replace it by a form that eliminates - * that operator. This may involve the introduction of witness terms. - * - * One exception to the above rule is that we may leave certain applications - * like (/ 4 1) unchanged, since replacing this by 4 changes its type from - * real to int. This is important for some subtyping issues during - * expandDefinition. Moreover, applications like this can be eliminated - * trivially later by rewriting. - * - * This method is called both during expandDefinition and during ppRewrite. - * - * @param n The node to eliminate operators from. - * @return The (single step) eliminated form of n. + * 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. */ - Node eliminateOperators(Node n); - /** - * 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); + static Node getAxiomFor(Node n); private: /** Logic info of the owner of this class */ @@ -95,6 +84,32 @@ class OperatorElim * function-ness of e.g. division by zero is ignored. */ std::map<ArithSkolemId, Node> d_arith_skolem; + /** + * 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 + * transcendental functions), then we replace it by a form that eliminates + * that operator. This may involve the introduction of witness terms. + * + * One exception to the above rule is that we may leave certain applications + * like (/ 4 1) unchanged, since replacing this by 4 changes its type from + * real to int. This is important for some subtyping issues during + * expandDefinition. Moreover, applications like this can be eliminated + * trivially later by rewriting. + * + * This method is called both during expandDefinition and during ppRewrite. + * + * @param n The node to eliminate operators from. + * @return The (single step) eliminated form of n. + */ + Node eliminateOperators(Node n, TConvProofGenerator* tg); + /** + * 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); /** 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 fcbfd1baf..52321ffd4 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -39,7 +39,7 @@ TheoryArith::TheoryArith(context::Context* c, ProofNodeManager* pnm) : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm), d_internal( - new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)), + new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)), d_ppRewriteTimer("theory::arith::ppRewriteTimer"), d_proofRecorder(nullptr) { @@ -78,8 +78,7 @@ void TheoryArith::finishInit() TrustNode TheoryArith::expandDefinition(Node node) { - Node expNode = d_internal->expandDefinition(node); - return TrustNode::mkTrustRewrite(node, expNode, nullptr); + return d_internal->expandDefinition(node); } void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -93,12 +92,7 @@ void TheoryArith::addSharedTerm(TNode n){ TrustNode TheoryArith::ppRewrite(TNode atom) { CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true); - Node ret = d_internal->ppRewrite(atom); - if (ret != atom) - { - return TrustNode::mkTrustRewrite(atom, ret, nullptr); - } - return TrustNode::null(); + return d_internal->ppRewrite(atom); } Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index cdf3c16c7..6f47ffb0e 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -87,7 +87,8 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) + const LogicInfo& logicInfo, + ProofNodeManager* pnm) : d_containing(containing), d_nlIncomplete(false), d_rowTracking(), @@ -156,7 +157,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_solveIntMaybeHelp(0u), d_solveIntAttempts(0u), d_statistics(), - d_opElim(logicInfo) + d_opElim(pnm, logicInfo) { // only need to create if non-linear logic if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) @@ -1078,26 +1079,21 @@ Node TheoryArithPrivate::getModelValue(TNode term) { } } -Node TheoryArithPrivate::ppRewriteTerms(TNode n) { +TrustNode TheoryArithPrivate::ppRewriteTerms(TNode n) +{ if(Theory::theoryOf(n) != THEORY_ARITH) { - return n; + return TrustNode::null(); } // Eliminate operators recursively. Notice we must do this here since other // 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 - Node nn = d_opElim.eliminateOperators(n); - if (nn != n) - { - // since elimination may introduce new operators to eliminate, we must - // recursively eliminate result - return d_opElim.eliminateOperatorsRec(nn); - } - return n; + return d_opElim.eliminate(n); } -Node TheoryArithPrivate::ppRewrite(TNode atom) { +TrustNode TheoryArithPrivate::ppRewrite(TNode atom) +{ Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl; if (options::arithRewriteEq()) @@ -1106,13 +1102,21 @@ Node TheoryArithPrivate::ppRewrite(TNode atom) { { Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; - leq = ppRewriteTerms(leq); - geq = ppRewriteTerms(geq); + 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; // don't need to rewrite terms since rewritten is not a non-standard op - return rewritten; + return TrustNode::mkTrustRewrite(atom, rewritten, nullptr); } } return ppRewriteTerms(atom); @@ -4812,17 +4816,10 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ return d_rowTracking[ridx]; } -Node TheoryArithPrivate::expandDefinition(Node node) +TrustNode TheoryArithPrivate::expandDefinition(Node node) { // call eliminate operators - Node nn = d_opElim.eliminateOperators(node); - if (nn != node) - { - // since elimination may introduce new operators to eliminate, we must - // recursively eliminate result - return d_opElim.eliminateOperatorsRec(nn); - } - return node; + return d_opElim.eliminate(node); } std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 867029e3c..42ec7f47b 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -415,7 +415,7 @@ private: Node axiomIteForTotalIntDivision(Node int_div_like); // handle linear /, div, mod, and also is_int, to_int - Node ppRewriteTerms(TNode atom); + TrustNode ppRewriteTerms(TNode atom); public: TheoryArithPrivate(TheoryArith& containing, @@ -423,7 +423,8 @@ private: context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + const LogicInfo& logicInfo, + ProofNodeManager* pnm); ~TheoryArithPrivate(); TheoryRewriter* getTheoryRewriter() { return &d_rewriter; } @@ -432,7 +433,7 @@ private: * Does non-context dependent setup for a node connected to a theory. */ void preRegisterTerm(TNode n); - Node expandDefinition(Node node); + TrustNode expandDefinition(Node node); void setMasterEqualityEngine(eq::EqualityEngine* eq); @@ -452,7 +453,7 @@ private: void presolve(); void notifyRestart(); Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - Node ppRewrite(TNode atom); + TrustNode ppRewrite(TNode atom); void ppStaticLearn(TNode in, NodeBuilder<>& learned); std::string identify() const { return std::string("TheoryArith"); } |