summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/operator_elim.cpp67
-rw-r--r--src/theory/arith/operator_elim.h67
-rw-r--r--src/theory/arith/theory_arith.cpp12
-rw-r--r--src/theory/arith/theory_arith_private.cpp47
-rw-r--r--src/theory/arith/theory_arith_private.h9
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"); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback