summaryrefslogtreecommitdiff
path: root/src/theory/arith/operator_elim.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/operator_elim.cpp')
-rw-r--r--src/theory/arith/operator_elim.cpp349
1 files changed, 174 insertions, 175 deletions
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index e34c0110e..8aaab3f69 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -14,6 +14,8 @@
#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"
@@ -27,6 +29,31 @@ namespace CVC4 {
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)
{
@@ -46,10 +73,12 @@ void OperatorElim::checkNonLinearLogic(Node term)
}
}
-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);
@@ -58,10 +87,12 @@ TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
}
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)
{
@@ -82,26 +113,21 @@ Node OperatorElim::eliminateOperators(Node node,
// 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);
@@ -120,89 +146,77 @@ Node OperatorElim::eliminateOperators(Node node,
}
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));
@@ -231,24 +245,13 @@ Node OperatorElim::eliminateOperators(Node node,
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:
@@ -325,79 +328,72 @@ Node OperatorElim::eliminateOperators(Node node,
}
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;
}
@@ -476,12 +472,15 @@ Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi)
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback