This updates the interface for arithmetic operator elimination for the new proof format.
The actual proof production of the operator elimination class (providing proofs for
introduced witness terms) will be done in a separate PR.
This also changes the witness terms introduced by this class so their body is in
Skolem form, which simplifies term formula removal.
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
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)
{
}
}
-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();
{
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;
}
return visited[n];
}
-Node OperatorElim::eliminateOperators(Node node)
+Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
{
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
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
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
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
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;
}
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);
#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 */
* 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
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)
{
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) {
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) {
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo)
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
: d_containing(containing),
d_nlIncomplete(false),
d_rowTracking(),
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())
}
}
-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())
{
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);
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){
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,
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo);
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm);
~TheoryArithPrivate();
TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
* 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);
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"); }
projects / cvc5.git / commitdiff