#include "theory/arith/operator_elim.h"
+#include "expr/attribute.h"
+#include "expr/bound_var_manager.h"
#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "smt/logic_exception.h"
namespace theory {
namespace arith {
+/**
+ * Attribute used for constructing unique bound variables that are binders
+ * for witness terms below. In other words, this attribute maps nodes to
+ * the bound variable of a witness term for eliminating that node.
+ *
+ * Notice we use the same attribute for most bound variables below, since using
+ * a node itself is a sufficient cache key for constructing a bound variable.
+ * The exception is to_int / is_int, which share a skolem based on their
+ * argument.
+ */
+struct ArithWitnessVarAttributeId
+{
+};
+using ArithWitnessVarAttribute = expr::Attribute<ArithWitnessVarAttributeId, Node>;
+/**
+ * Similar to above, shared for to_int and is_int. This is used for introducing
+ * an integer bound variable used to construct the witness term for t in the
+ * contexts (to_int t) and (is_int t).
+ */
+struct ToIntWitnessVarAttributeId
+{
+};
+using ToIntWitnessVarAttribute
+ = expr::Attribute<ToIntWitnessVarAttributeId, Node>;
+
OperatorElim::OperatorElim(ProofNodeManager* pnm, const LogicInfo& info)
: EagerProofGenerator(pnm), d_info(info)
{
}
}
-TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
+TrustNode OperatorElim::eliminate(Node n,
+ std::vector<SkolemLemma>& lems,
+ bool partialOnly)
{
TConvProofGenerator* tg = nullptr;
- Node nn = eliminateOperators(n, tg, partialOnly);
+ Node nn = eliminateOperators(n, lems, tg, partialOnly);
if (nn != n)
{
return TrustNode::mkTrustRewrite(n, nn, nullptr);
}
Node OperatorElim::eliminateOperators(Node node,
+ std::vector<SkolemLemma>& lems,
TConvProofGenerator* tg,
bool partialOnly)
{
NodeManager* nm = NodeManager::currentNM();
+ BoundVarManager* bvm = nm->getBoundVarManager();
Kind k = node.getKind();
switch (k)
{
// 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())
- {
- // node[0] - 1 < toIntSkolem <= node[0]
- // -1 < toIntSkolem - node[0] <= 0
- // 0 <= node[0] - toIntSkolem < 1
- Node v = nm->mkBoundVar(nm->integerType());
- Node one = mkRationalNode(1);
- Node zero = mkRationalNode(0);
- Node diff = nm->mkNode(MINUS, node[0], v);
- Node lem = mkInRange(diff, zero, one);
- toIntSkolem = mkWitnessTerm(
- v, lem, "toInt", "a conversion of a Real term to its Integer part");
- d_to_int_skolem[node[0]] = toIntSkolem;
- }
- else
- {
- toIntSkolem = (*it).second;
- }
+ // node[0] - 1 < toIntSkolem <= node[0]
+ // -1 < toIntSkolem - node[0] <= 0
+ // 0 <= node[0] - toIntSkolem < 1
+ Node v =
+ bvm->mkBoundVar<ToIntWitnessVarAttribute>(node[0], nm->integerType());
+ Node one = mkRationalNode(1);
+ Node zero = mkRationalNode(0);
+ Node diff = nm->mkNode(MINUS, node[0], v);
+ Node lem = mkInRange(diff, zero, one);
+ Node toIntSkolem =
+ mkWitnessTerm(v,
+ lem,
+ "toInt",
+ "a conversion of a Real term to its Integer part",
+ lems);
if (k == IS_INTEGER)
{
return nm->mkNode(EQUAL, node[0], toIntSkolem);
}
Node den = Rewriter::rewrite(node[1]);
Node num = Rewriter::rewrite(node[0]);
- Node intVar;
Node rw = nm->mkNode(k, num, den);
- std::map<Node, Node>::const_iterator it = d_int_div_skolem.find(rw);
- if (it == d_int_div_skolem.end())
+ Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->integerType());
+ Node lem;
+ Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num);
+ if (den.isConst())
{
- Node v = nm->mkBoundVar(nm->integerType());
- Node lem;
- Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num);
- if (den.isConst())
+ const Rational& rat = den.getConst<Rational>();
+ if (num.isConst() || rat == 0)
{
- const Rational& rat = den.getConst<Rational>();
- if (num.isConst() || rat == 0)
- {
- // just rewrite
- return Rewriter::rewrite(node);
- }
- if (rat > 0)
- {
- lem = nm->mkNode(
- AND,
- leqNum,
- nm->mkNode(
- LT,
- num,
- nm->mkNode(MULT,
- den,
- nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
- }
- else
- {
- lem = nm->mkNode(
- AND,
- leqNum,
- nm->mkNode(
- LT,
- num,
- nm->mkNode(
- MULT,
- den,
- nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
- }
+ // just rewrite
+ return Rewriter::rewrite(node);
}
- else
+ if (rat > 0)
{
- checkNonLinearLogic(node);
lem = nm->mkNode(
AND,
+ leqNum,
nm->mkNode(
- IMPLIES,
- nm->mkNode(GT, den, nm->mkConst(Rational(0))),
- nm->mkNode(
- AND,
- leqNum,
- nm->mkNode(
- LT,
- num,
- nm->mkNode(
- MULT,
- den,
- nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
+ LT,
+ num,
+ nm->mkNode(MULT,
+ den,
+ nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
+ }
+ else
+ {
+ lem = nm->mkNode(
+ AND,
+ leqNum,
nm->mkNode(
- IMPLIES,
- nm->mkNode(LT, den, nm->mkConst(Rational(0))),
- nm->mkNode(
- AND,
- leqNum,
- nm->mkNode(
- LT,
- num,
- nm->mkNode(
- MULT,
- den,
- nm->mkNode(
- PLUS, v, nm->mkConst(Rational(-1))))))));
+ LT,
+ num,
+ nm->mkNode(MULT,
+ den,
+ nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
}
- intVar = mkWitnessTerm(
- v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
- d_int_div_skolem[rw] = intVar;
}
else
{
- intVar = (*it).second;
+ checkNonLinearLogic(node);
+ lem = nm->mkNode(
+ AND,
+ nm->mkNode(
+ IMPLIES,
+ nm->mkNode(GT, den, nm->mkConst(Rational(0))),
+ nm->mkNode(
+ AND,
+ leqNum,
+ nm->mkNode(
+ LT,
+ num,
+ nm->mkNode(
+ MULT,
+ den,
+ nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
+ nm->mkNode(
+ IMPLIES,
+ nm->mkNode(LT, den, nm->mkConst(Rational(0))),
+ nm->mkNode(
+ AND,
+ leqNum,
+ nm->mkNode(
+ LT,
+ num,
+ nm->mkNode(
+ MULT,
+ den,
+ nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))))));
}
+ Node intVar = mkWitnessTerm(
+ v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems);
if (k == INTS_MODULUS_TOTAL)
{
Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
return node;
}
checkNonLinearLogic(node);
- Node var;
Node rw = nm->mkNode(k, num, den);
- std::map<Node, Node>::const_iterator it = d_div_skolem.find(rw);
- if (it == d_div_skolem.end())
- {
- Node v = nm->mkBoundVar(nm->realType());
- Node lem = nm->mkNode(IMPLIES,
- den.eqNode(nm->mkConst(Rational(0))).negate(),
- nm->mkNode(MULT, den, v).eqNode(num));
- var = mkWitnessTerm(
- v, lem, "nonlinearDiv", "the result of a non-linear div term");
- d_div_skolem[rw] = var;
- }
- else
- {
- var = (*it).second;
- }
- return var;
+ Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->realType());
+ Node lem = nm->mkNode(IMPLIES,
+ den.eqNode(nm->mkConst(Rational(0))).negate(),
+ nm->mkNode(MULT, den, v).eqNode(num));
+ return mkWitnessTerm(
+ v, lem, "nonlinearDiv", "the result of a non-linear div term", lems);
break;
}
case DIVISION:
}
checkNonLinearLogic(node);
// eliminate inverse functions here
- std::map<Node, Node>::const_iterator it =
- d_nlin_inverse_skolem.find(node);
- if (it == d_nlin_inverse_skolem.end())
+ Node var =
+ bvm->mkBoundVar<ArithWitnessVarAttribute>(node, nm->realType());
+ Node lem;
+ if (k == SQRT)
{
- Node var = nm->mkBoundVar(nm->realType());
- Node lem;
- if (k == SQRT)
- {
- Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
- Node uf = skolemApp.eqNode(var);
- Node nonNeg =
- nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);
+ Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
+ Node uf = skolemApp.eqNode(var);
+ Node nonNeg =
+ nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);
+
+ // sqrt(x) reduces to:
+ // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x))
+ //
+ // Uf(x) makes sure that the reduction still behaves like a function,
+ // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
+ // satisfiable. On the original formula, this would require that we
+ // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
+ // model.
+ lem = nm->mkNode(ITE,
+ nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
+ nonNeg,
+ uf);
+ }
+ else
+ {
+ Node pi = mkPi();
- // sqrt(x) reduces to:
- // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x))
- //
- // Uf(x) makes sure that the reduction still behaves like a function,
- // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
- // satisfiable. On the original formula, this would require that we
- // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
- // model.
- lem = nm->mkNode(ITE,
- nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
- nonNeg,
- uf);
+ // range of the skolem
+ Node rlem;
+ if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
+ {
+ Node half = nm->mkConst(Rational(1) / Rational(2));
+ Node pi2 = nm->mkNode(MULT, half, pi);
+ Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2);
+ // -pi/2 < var <= pi/2
+ rlem = nm->mkNode(
+ AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
}
else
{
- Node pi = mkPi();
-
- // range of the skolem
- Node rlem;
- if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
- {
- Node half = nm->mkConst(Rational(1) / Rational(2));
- Node pi2 = nm->mkNode(MULT, half, pi);
- Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2);
- // -pi/2 < var <= pi/2
- rlem = nm->mkNode(
- AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
- }
- else
- {
- // 0 <= var < pi
- rlem = nm->mkNode(AND,
- nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
- nm->mkNode(LT, var, pi));
- }
-
- Kind rk = k == ARCSINE
- ? SINE
- : (k == ARCCOSINE
- ? COSINE
- : (k == ARCTANGENT
- ? TANGENT
- : (k == ARCCOSECANT
- ? COSECANT
- : (k == ARCSECANT ? SECANT
- : COTANGENT))));
- Node invTerm = nm->mkNode(rk, var);
- lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
+ // 0 <= var < pi
+ rlem = nm->mkNode(AND,
+ nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
+ nm->mkNode(LT, var, pi));
}
- Assert(!lem.isNull());
- Node ret = mkWitnessTerm(
- var,
- lem,
- "tfk",
- "Skolem to eliminate a non-standard transcendental function");
- Assert(ret.getKind() == WITNESS);
- d_nlin_inverse_skolem[node] = ret;
- return ret;
+
+ Kind rk =
+ k == ARCSINE
+ ? SINE
+ : (k == ARCCOSINE
+ ? COSINE
+ : (k == ARCTANGENT
+ ? TANGENT
+ : (k == ARCCOSECANT
+ ? COSECANT
+ : (k == ARCSECANT ? SECANT : COTANGENT))));
+ Node invTerm = nm->mkNode(rk, var);
+ lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
}
- return (*it).second;
+ Assert(!lem.isNull());
+ return mkWitnessTerm(
+ var,
+ lem,
+ "tfk",
+ "Skolem to eliminate a non-standard transcendental function",
+ lems);
break;
}
Node OperatorElim::mkWitnessTerm(Node v,
Node pred,
const std::string& prefix,
- const std::string& comment)
+ const std::string& comment,
+ std::vector<SkolemLemma>& lems)
{
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
+ // we mark that we should send a lemma
Node k = sm->mkSkolem(
v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this, true);
+ // TODO: (project #37) add to lems
return k;
}
#include "expr/term_conversion_proof_generator.h"
#include "theory/eager_proof_generator.h"
#include "theory/logic_info.h"
+#include "theory/skolem_lemma.h"
namespace CVC4 {
namespace theory {
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, bool partialOnly = false);
+ *
+ * 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.
+ *
+ * @param n The node to eliminate
+ * @param lems The lemmas that we wish to add concerning n. It is the
+ * responsbility of the caller to process these lemmas.
+ * @param partialOnly Whether we only want to eliminate partial operators.
+ * @return the trust node of kind REWRITE encapsulating the eliminated form
+ * of n and a proof generator for proving this equivalence.
+ */
+ TrustNode eliminate(Node n,
+ std::vector<SkolemLemma>& lems,
+ 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.
/** Logic info of the owner of this class */
const LogicInfo& d_info;
- /**
- * Maps for Skolems for to-integer, real/integer div-by-k, and inverse
- * non-linear operators that are introduced during ppRewriteTerms.
- */
- std::map<Node, Node> d_to_int_skolem;
- std::map<Node, Node> d_div_skolem;
- std::map<Node, Node> d_int_div_skolem;
- std::map<Node, Node> d_nlin_inverse_skolem;
-
/** Arithmetic skolem identifier */
enum class ArithSkolemId
{
* @param n The node to eliminate operators from.
* @return The (single step) eliminated form of n.
*/
- Node eliminateOperators(Node n, TConvProofGenerator* tg, bool partialOnly);
+ Node eliminateOperators(Node n,
+ std::vector<SkolemLemma>& lems,
+ TConvProofGenerator* tg,
+ bool partialOnly);
/** get arithmetic skolem
*
* Returns the Skolem in the above map for the given id, creating it if it
Node mkWitnessTerm(Node v,
Node pred,
const std::string& prefix,
- const std::string& comment);
+ const std::string& comment,
+ std::vector<SkolemLemma>& lems);
/** get arithmetic skolem application
*
* By default, this returns the term f( n ), where f is the Skolem function
TrustNode TheoryArith::expandDefinition(Node node)
{
// call eliminate operators, to eliminate partial operators only
- return d_arithPreproc.eliminate(node, true);
+ std::vector<SkolemLemma> lems;
+ TrustNode ret = d_arithPreproc.eliminate(node, lems, true);
+ Assert(lems.empty());
+ return ret;
}
void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
- if (options::arithRewriteEq())
+ if (atom.getKind() == kind::EQUAL)
{
- if (atom.getKind() == kind::EQUAL)
- {
- 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];
- 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
- if (proofsEnabled())
- {
- return d_ppPfGen.mkTrustedRewrite(
- atom,
- rewritten,
- d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
- }
- else
- {
- return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
- }
- }
+ return ppRewriteEq(atom);
}
- return ppRewriteTerms(atom);
-}
-
-TrustNode TheoryArith::ppRewriteTerms(TNode n)
-{
- Assert(Theory::theoryOf(n) == THEORY_ARITH);
- // Eliminate operators recursively. Notice we must do this here since other
+ // TODO (project #37): this will be passed to ppRewrite
+ std::vector<SkolemLemma> lems;
+ Assert(Theory::theoryOf(atom) == THEORY_ARITH);
+ // Eliminate operators. 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. In contrast to expandDefinitions, we eliminate
// *all* extended arithmetic operators here, including total ones.
- return d_arithPreproc.eliminate(n, false);
+ return d_arithPreproc.eliminate(atom, lems, false);
+}
+
+TrustNode TheoryArith::ppRewriteEq(TNode atom)
+{
+ Assert(atom.getKind() == kind::EQUAL);
+ if (!options::arithRewriteEq())
+ {
+ return TrustNode::null();
+ }
+ 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];
+ 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
+ if (proofsEnabled())
+ {
+ return d_ppPfGen.mkTrustedRewrite(
+ atom,
+ rewritten,
+ d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
+ }
+ return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
}
Theory::PPAssertStatus TheoryArith::ppAssert(
projects / cvc5.git / commitdiff