summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/theory_arith_private.cpp23
-rw-r--r--src/theory/builtin/proof_checker.cpp20
-rw-r--r--src/theory/strings/skolem_cache.cpp5
-rw-r--r--src/theory/strings/skolem_cache.h2
4 files changed, 26 insertions, 24 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 3ff3966cc..443aaa9b7 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -34,7 +34,7 @@
#include "expr/node.h"
#include "expr/node_algorithm.h"
#include "expr/node_builder.h"
-#include "expr/proof_skolem_cache.h"
+#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "options/smt_options.h" // for incrementalSolving()
#include "preprocessing/util/ite_utilities.h"
@@ -1178,6 +1178,7 @@ Node TheoryArithPrivate::eliminateOperatorsRec(Node n)
Node TheoryArithPrivate::eliminateOperators(Node node)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Kind k = node.getKind();
switch (k)
@@ -1206,9 +1207,9 @@ Node TheoryArithPrivate::eliminateOperators(Node node)
Node zero = mkRationalNode(0);
Node diff = nm->mkNode(kind::MINUS, node[0], v);
Node lem = mkInRange(diff, zero, one);
- toIntSkolem = ProofSkolemCache::mkSkolem(
+ toIntSkolem = sm->mkSkolem(
v, lem, "toInt", "a conversion of a Real term to its Integer part");
- toIntSkolem = ProofSkolemCache::getWitnessForm(toIntSkolem);
+ toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem);
d_to_int_skolem[node[0]] = toIntSkolem;
}
else
@@ -1303,9 +1304,9 @@ Node TheoryArithPrivate::eliminateOperators(Node node)
nm->mkNode(
PLUS, v, nm->mkConst(Rational(-1))))))));
}
- intVar = ProofSkolemCache::mkSkolem(
+ intVar = sm->mkSkolem(
v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
- intVar = ProofSkolemCache::getWitnessForm(intVar);
+ intVar = SkolemManager::getWitnessForm(intVar);
d_int_div_skolem[rw] = intVar;
}
else
@@ -1345,9 +1346,9 @@ Node TheoryArithPrivate::eliminateOperators(Node node)
Node lem = nm->mkNode(IMPLIES,
den.eqNode(nm->mkConst(Rational(0))).negate(),
nm->mkNode(MULT, den, v).eqNode(num));
- var = ProofSkolemCache::mkSkolem(
+ var = sm->mkSkolem(
v, lem, "nonlinearDiv", "the result of a non-linear div term");
- var = ProofSkolemCache::getWitnessForm(var);
+ var = SkolemManager::getWitnessForm(var);
d_div_skolem[rw] = var;
}
else
@@ -1490,12 +1491,12 @@ Node TheoryArithPrivate::eliminateOperators(Node node)
lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
}
Assert(!lem.isNull());
- Node ret = ProofSkolemCache::mkSkolem(
+ Node ret = sm->mkSkolem(
var,
lem,
"tfk",
"Skolem to eliminate a non-standard transcendental function");
- ret = ProofSkolemCache::getWitnessForm(ret);
+ ret = SkolemManager::getWitnessForm(ret);
d_nlin_inverse_skolem[node] = ret;
return ret;
}
@@ -4269,8 +4270,8 @@ bool TheoryArithPrivate::needsCheckLastEffort() {
}
}
-Node TheoryArithPrivate::explain(TNode n) {
-
+Node TheoryArithPrivate::explain(TNode n)
+{
Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
ConstraintP c = d_constraintDatabase.lookup(n);
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 8d2a1540c..1884d3890 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -14,7 +14,7 @@
#include "theory/builtin/proof_checker.h"
-#include "expr/proof_skolem_cache.h"
+#include "expr/skolem_manager.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
@@ -63,9 +63,9 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
{
- Node nk = ProofSkolemCache::getSkolemForm(n);
+ Node nk = SkolemManager::getSkolemForm(n);
Node nkr = applyRewriteExternal(nk, idr);
- return ProofSkolemCache::getWitnessForm(nkr);
+ return SkolemManager::getWitnessForm(nkr);
}
Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
@@ -74,27 +74,27 @@ Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
{
return Node::null();
}
- Node nk = ProofSkolemCache::getSkolemForm(n);
+ Node nk = SkolemManager::getSkolemForm(n);
Node nks = applySubstitutionExternal(nk, exp, ids);
- return ProofSkolemCache::getWitnessForm(nks);
+ return SkolemManager::getWitnessForm(nks);
}
Node BuiltinProofRuleChecker::applySubstitution(Node n,
const std::vector<Node>& exp,
MethodId ids)
{
- Node nk = ProofSkolemCache::getSkolemForm(n);
+ Node nk = SkolemManager::getSkolemForm(n);
Node nks = applySubstitutionExternal(nk, exp, ids);
- return ProofSkolemCache::getWitnessForm(nks);
+ return SkolemManager::getWitnessForm(nks);
}
Node BuiltinProofRuleChecker::applySubstitutionRewrite(
Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr)
{
- Node nk = ProofSkolemCache::getSkolemForm(n);
+ Node nk = SkolemManager::getSkolemForm(n);
Node nks = applySubstitutionExternal(nk, exp, ids);
Node nksr = applyRewriteExternal(nks, idr);
- return ProofSkolemCache::getWitnessForm(nksr);
+ return SkolemManager::getWitnessForm(nksr);
}
Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr)
@@ -122,7 +122,7 @@ Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n,
MethodId ids)
{
Assert(!exp.isNull());
- Node expk = ProofSkolemCache::getSkolemForm(exp);
+ Node expk = SkolemManager::getSkolemForm(exp);
TNode var, subs;
if (ids == MethodId::SB_DEFAULT)
{
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 4af75f1cc..85a948567 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -82,12 +82,13 @@ Node SkolemCache::mkTypedSkolemCached(
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Node sk;
switch (id)
{
// exists k. k = a
case SK_PURIFY:
- sk = ProofSkolemCache::mkPurifySkolem(a, c, "string purify skolem");
+ sk = sm->mkPurifySkolem(a, c, "string purify skolem");
break;
// these are eliminated by normalizeStringSkolem
case SK_ID_V_SPT:
@@ -113,7 +114,7 @@ Node SkolemCache::mkTypedSkolemCached(
Notice() << "Don't know how to handle Skolem ID " << id << std::endl;
Node v = nm->mkBoundVar(tn);
Node cond = nm->mkConst(true);
- sk = ProofSkolemCache::mkSkolem(v, cond, c, "string skolem");
+ sk = sm->mkSkolem(v, cond, c, "string skolem");
}
break;
}
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 0ebbb3277..7ce507f29 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -22,7 +22,7 @@
#include <unordered_set>
#include "expr/node.h"
-#include "expr/proof_skolem_cache.h"
+#include "expr/skolem_manager.h"
namespace CVC4 {
namespace theory {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback