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.cpp124
-rw-r--r--src/theory/arith/operator_elim.h16
-rw-r--r--src/theory/arith/theory_arith.cpp10
3 files changed, 34 insertions, 116 deletions
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index fbd1798cd..e34c0110e 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -52,86 +52,16 @@ TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
Node nn = eliminateOperators(n, tg, partialOnly);
if (nn != n)
{
- // since elimination may introduce new operators to eliminate, we must
- // recursively eliminate result
- Node nnr = eliminateOperatorsRec(nn, tg, partialOnly);
- return TrustNode::mkTrustRewrite(n, nnr, nullptr);
+ return TrustNode::mkTrustRewrite(n, nn, nullptr);
}
return TrustNode::null();
}
-Node OperatorElim::eliminateOperatorsRec(Node n,
- TConvProofGenerator* tg,
- bool partialOnly)
-{
- Trace("arith-elim") << "Begin elim: " << n << std::endl;
- NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<Node, Node, TNodeHashFunction> visited;
- std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
- std::vector<Node> visit;
- Node cur;
- visit.push_back(n);
- do
- {
- cur = visit.back();
- visit.pop_back();
- it = visited.find(cur);
- if (Theory::theoryOf(cur) != THEORY_ARITH)
- {
- visited[cur] = cur;
- }
- else if (it == visited.end())
- {
- visited[cur] = Node::null();
- visit.push_back(cur);
- for (const Node& cn : cur)
- {
- visit.push_back(cn);
- }
- }
- else if (it->second.isNull())
- {
- Node ret = cur;
- bool childChanged = false;
- std::vector<Node> children;
- if (cur.getMetaKind() == metakind::PARAMETERIZED)
- {
- children.push_back(cur.getOperator());
- }
- for (const Node& cn : cur)
- {
- it = visited.find(cn);
- Assert(it != visited.end());
- Assert(!it->second.isNull());
- childChanged = childChanged || cn != it->second;
- children.push_back(it->second);
- }
- if (childChanged)
- {
- ret = nm->mkNode(cur.getKind(), children);
- }
- Node retElim = eliminateOperators(ret, tg, partialOnly);
- if (retElim != ret)
- {
- // recursively eliminate operators in result, since some eliminations
- // are defined in terms of other non-standard operators.
- ret = eliminateOperatorsRec(retElim, tg, partialOnly);
- }
- visited[cur] = ret;
- }
- } while (!visit.empty());
- Assert(visited.find(n) != visited.end());
- Assert(!visited.find(n)->second.isNull());
- return visited[n];
-}
-
Node OperatorElim::eliminateOperators(Node node,
TConvProofGenerator* tg,
bool partialOnly)
{
NodeManager* nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
-
Kind k = node.getKind();
switch (k)
{
@@ -164,14 +94,8 @@ 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",
- NodeManager::SKOLEM_DEFAULT,
- this,
- true);
+ toIntSkolem = mkWitnessTerm(
+ v, lem, "toInt", "a conversion of a Real term to its Integer part");
d_to_int_skolem[node[0]] = toIntSkolem;
}
else
@@ -271,13 +195,8 @@ 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",
- NodeManager::SKOLEM_DEFAULT,
- this,
- true);
+ intVar = mkWitnessTerm(
+ v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
d_int_div_skolem[rw] = intVar;
}
else
@@ -321,13 +240,8 @@ 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",
- NodeManager::SKOLEM_DEFAULT,
- this,
- true);
+ var = mkWitnessTerm(
+ v, lem, "nonlinearDiv", "the result of a non-linear div term");
d_div_skolem[rw] = var;
}
else
@@ -404,6 +318,11 @@ Node OperatorElim::eliminateOperators(Node node,
case ARCSECANT:
case ARCCOTANGENT:
{
+ if (partialOnly)
+ {
+ // not eliminating total operators
+ return node;
+ }
checkNonLinearLogic(node);
// eliminate inverse functions here
std::map<Node, Node>::const_iterator it =
@@ -469,14 +388,11 @@ Node OperatorElim::eliminateOperators(Node node,
lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
}
Assert(!lem.isNull());
- Node ret = sm->mkSkolem(
+ Node ret = mkWitnessTerm(
var,
lem,
"tfk",
- "Skolem to eliminate a non-standard transcendental function",
- NodeManager::SKOLEM_DEFAULT,
- this,
- true);
+ "Skolem to eliminate a non-standard transcendental function");
Assert(ret.getKind() == WITNESS);
d_nlin_inverse_skolem[node] = ret;
return ret;
@@ -557,6 +473,18 @@ Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi)
return skolem;
}
+Node OperatorElim::mkWitnessTerm(Node v,
+ Node pred,
+ const std::string& prefix,
+ const std::string& comment)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ Node k = sm->mkSkolem(
+ v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this, true);
+ return k;
+}
+
} // namespace arith
} // namespace theory
} // namespace CVC4
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index bca80ea4d..cf5b9248c 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -102,20 +102,20 @@ class OperatorElim : public EagerProofGenerator
* @return The (single step) eliminated form of n.
*/
Node eliminateOperators(Node n, TConvProofGenerator* tg, bool partialOnly);
- /**
- * 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, bool partialOnly);
/** get arithmetic skolem
*
* Returns the Skolem in the above map for the given id, creating it if it
* does not already exist.
*/
Node getArithSkolem(ArithSkolemId asi);
+ /**
+ * Make the witness term, which creates a witness term based on the skolem
+ * manager with this class as a proof generator.
+ */
+ Node mkWitnessTerm(Node v,
+ Node pred,
+ const std::string& prefix,
+ const std::string& comment);
/** get arithmetic skolem application
*
* By default, this returns the term f( n ), where f is the Skolem function
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6de5c7221..9bca5e182 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -119,16 +119,6 @@ TrustNode TheoryArith::ppRewrite(TNode atom)
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];
- 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback