diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 23 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 20 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.h | 2 |
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 { |