summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/CMakeLists.txt4
-rw-r--r--src/expr/node_manager.cpp4
-rw-r--r--src/expr/node_manager.h20
-rw-r--r--src/expr/proof_checker.cpp16
-rw-r--r--src/expr/proof_checker.h4
-rw-r--r--src/expr/skolem_manager.cpp (renamed from src/expr/proof_skolem_cache.cpp)92
-rw-r--r--src/expr/skolem_manager.h (renamed from src/expr/proof_skolem_cache.h)61
-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
11 files changed, 157 insertions, 94 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 3d41b7a72..6415e2132 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -49,10 +49,10 @@ libcvc4_add_sources(
proof_node_manager.h
proof_rule.cpp
proof_rule.h
- proof_skolem_cache.cpp
- proof_skolem_cache.h
proof_step_buffer.cpp
proof_step_buffer.h
+ skolem_manager.cpp
+ skolem_manager.h
symbol_table.cpp
symbol_table.h
term_canonize.cpp
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 427afd5af..6f8934645 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -27,6 +27,7 @@
#include "expr/dtype.h"
#include "expr/node_manager_attributes.h"
#include "expr/node_manager_listeners.h"
+#include "expr/skolem_manager.h"
#include "expr/type_checker.h"
#include "options/options.h"
#include "options/smt_options.h"
@@ -95,6 +96,7 @@ NodeManager::NodeManager(ExprManager* exprManager)
: d_options(new Options()),
d_statisticsRegistry(new StatisticsRegistry()),
d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)),
+ d_skManager(new SkolemManager),
d_registrations(new ListenerRegistrationList()),
next_id(0),
d_attrManager(new expr::attr::AttributeManager()),
@@ -111,6 +113,7 @@ NodeManager::NodeManager(ExprManager* exprManager, const Options& options)
: d_options(new Options()),
d_statisticsRegistry(new StatisticsRegistry()),
d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)),
+ d_skManager(new SkolemManager),
d_registrations(new ListenerRegistrationList()),
next_id(0),
d_attrManager(new expr::attr::AttributeManager()),
@@ -230,6 +233,7 @@ NodeManager::~NodeManager() {
// defensive coding, in case destruction-order issues pop up (they often do)
delete d_resourceManager;
d_resourceManager = NULL;
+ d_skManager = nullptr;
delete d_statisticsRegistry;
d_statisticsRegistry = NULL;
delete d_registrations;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1fab328e9..7fa2d147a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -42,6 +42,7 @@ namespace CVC4 {
class StatisticsRegistry;
class ResourceManager;
+class SkolemManager;
class DType;
@@ -113,6 +114,9 @@ class NodeManager {
ResourceManager* d_resourceManager;
+ /** The skolem manager */
+ std::shared_ptr<SkolemManager> d_skManager;
+
/**
* A list of registrations on d_options to that call into d_resourceManager.
* These must be garbage collected before d_options and d_resourceManager.
@@ -405,6 +409,8 @@ public:
/** Get this node manager's resource manager */
ResourceManager* getResourceManager() { return d_resourceManager; }
+ /** Get this node manager's skolem manager */
+ SkolemManager* getSkolemManager() { return d_skManager.get(); }
/** Get this node manager's statistics registry */
StatisticsRegistry* getStatisticsRegistry() const
@@ -539,13 +545,13 @@ public:
* "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT
* cannot be composed in such a manner.
*/
- enum SkolemFlags {
- SKOLEM_DEFAULT = 0, /**< default behavior */
- SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
- SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */
- SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */
- };/* enum SkolemFlags */
-
+ enum SkolemFlags
+ {
+ SKOLEM_DEFAULT = 0, /**< default behavior */
+ SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
+ SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */
+ SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */
+ };
/**
* Create a skolem constant with the given name, type, and comment.
*
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index 7e7a26c5b..ffd1bdc9c 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -14,7 +14,7 @@
#include "expr/proof_checker.h"
-#include "expr/proof_skolem_cache.h"
+#include "expr/skolem_manager.h"
#include "smt/smt_statistics_registry.h"
using namespace CVC4::kind;
@@ -28,11 +28,11 @@ Node ProofRuleChecker::check(PfRule id,
// convert to witness form
std::vector<Node> childrenw = children;
std::vector<Node> argsw = args;
- ProofSkolemCache::convertToWitnessFormVec(childrenw);
- ProofSkolemCache::convertToWitnessFormVec(argsw);
+ SkolemManager::convertToWitnessFormVec(childrenw);
+ SkolemManager::convertToWitnessFormVec(argsw);
Node res = checkInternal(id, childrenw, argsw);
// res is in terms of witness form, convert back to Skolem form
- return ProofSkolemCache::getSkolemForm(res);
+ return SkolemManager::getSkolemForm(res);
}
Node ProofRuleChecker::checkChildrenArg(PfRule id,
@@ -92,14 +92,17 @@ bool ProofRuleChecker::getBool(TNode n, bool& b)
}
ProofCheckerStatistics::ProofCheckerStatistics()
- : d_ruleChecks("ProofCheckerStatistics::ruleChecks")
+ : d_ruleChecks("ProofCheckerStatistics::ruleChecks"),
+ d_totalRuleChecks("ProofCheckerStatistics::totalRuleChecks", 0)
{
smtStatisticsRegistry()->registerStat(&d_ruleChecks);
+ smtStatisticsRegistry()->registerStat(&d_totalRuleChecks);
}
ProofCheckerStatistics::~ProofCheckerStatistics()
{
smtStatisticsRegistry()->unregisterStat(&d_ruleChecks);
+ smtStatisticsRegistry()->unregisterStat(&d_totalRuleChecks);
}
Node ProofChecker::check(ProofNode* pn, Node expected)
@@ -123,6 +126,7 @@ Node ProofChecker::check(
}
// record stat
d_stats.d_ruleChecks << id;
+ ++d_stats.d_totalRuleChecks;
Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
std::vector<Node> cchildren;
for (const std::shared_ptr<ProofNode>& pc : children)
@@ -183,6 +187,8 @@ Node ProofChecker::checkDebug(PfRule id,
{
Trace(traceTag) << " success" << std::endl;
}
+ Trace(traceTag) << "cchildren: " << cchildren << std::endl;
+ Trace(traceTag) << " args: " << args << std::endl;
return res;
}
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index 99c02b8dc..f04587a7d 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -77,7 +77,7 @@ class ProofRuleChecker
/**
* This checks a single step in a proof. It is identical to check above
* except that children and args have been converted to "witness form"
- * (see ProofSkolemCache). Likewise, its output should be in witness form.
+ * (see SkolemManager). Likewise, its output should be in witness form.
*
* @param id The id of the proof node to check
* @param children The premises of the proof node to check. These are nodes
@@ -100,6 +100,8 @@ class ProofCheckerStatistics
~ProofCheckerStatistics();
/** Counts the number of checks for each kind of proof rule */
HistogramStat<PfRule> d_ruleChecks;
+ /** Total number of rule checks */
+ IntStat d_totalRuleChecks;
};
/** A class for checking proofs */
diff --git a/src/expr/proof_skolem_cache.cpp b/src/expr/skolem_manager.cpp
index da991415e..0570af687 100644
--- a/src/expr/proof_skolem_cache.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -1,5 +1,5 @@
/********************* */
-/*! \file proof_skolem_cache.cpp
+/*! \file skolem_manager.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
@@ -9,10 +9,10 @@
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Implementation of proof skolem cache
+ ** \brief Implementation of skolem manager class
**/
-#include "expr/proof_skolem_cache.h"
+#include "expr/skolem_manager.h"
#include "expr/attribute.h"
@@ -35,11 +35,12 @@ struct PurifySkolemAttributeId
};
typedef expr::Attribute<PurifySkolemAttributeId, Node> PurifySkolemAttribute;
-Node ProofSkolemCache::mkSkolem(Node v,
- Node pred,
- const std::string& prefix,
- const std::string& comment,
- int flags)
+Node SkolemManager::mkSkolem(Node v,
+ Node pred,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags,
+ ProofGenerator* pg)
{
Assert(v.getKind() == BOUND_VARIABLE);
// make the witness term
@@ -49,14 +50,17 @@ Node ProofSkolemCache::mkSkolem(Node v,
Node predw = getWitnessForm(pred);
// make the witness term, which should not contain any skolem
Node w = nm->mkNode(WITNESS, bvl, predw);
+ // store the mapping to proof generator
+ d_gens[w] = pg;
return getOrMakeSkolem(w, prefix, comment, flags);
}
-Node ProofSkolemCache::mkSkolemExists(Node v,
- Node q,
- const std::string& prefix,
- const std::string& comment,
- int flags)
+Node SkolemManager::mkSkolemExists(Node v,
+ Node q,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags,
+ ProofGenerator* pg)
{
Assert(q.getKind() == EXISTS);
bool foundVar = false;
@@ -82,13 +86,13 @@ Node ProofSkolemCache::mkSkolemExists(Node v,
Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
pred = nm->mkNode(EXISTS, bvl, pred);
}
- return mkSkolem(v, pred, prefix, comment, flags);
+ return mkSkolem(v, pred, prefix, comment, flags, pg);
}
-Node ProofSkolemCache::mkPurifySkolem(Node t,
- const std::string& prefix,
- const std::string& comment,
- int flags)
+Node SkolemManager::mkPurifySkolem(Node t,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags)
{
PurifySkolemAttribute psa;
if (t.hasAttribute(psa))
@@ -107,23 +111,27 @@ Node ProofSkolemCache::mkPurifySkolem(Node t,
return k;
}
-Node ProofSkolemCache::getWitnessForm(Node n)
+ProofGenerator* SkolemManager::getProofGenerator(Node t)
{
- return convertInternal(n, true);
+ std::map<Node, ProofGenerator*>::iterator it = d_gens.find(t);
+ if (it != d_gens.end())
+ {
+ return it->second;
+ }
+ return nullptr;
}
-Node ProofSkolemCache::getSkolemForm(Node n)
-{
- return convertInternal(n, false);
-}
+Node SkolemManager::getWitnessForm(Node n) { return convertInternal(n, true); }
+
+Node SkolemManager::getSkolemForm(Node n) { return convertInternal(n, false); }
-Node ProofSkolemCache::convertInternal(Node n, bool toWitness)
+Node SkolemManager::convertInternal(Node n, bool toWitness)
{
if (n.isNull())
{
return n;
}
- Trace("pf-skolem-debug") << "ProofSkolemCache::convertInternal: " << toWitness
+ Trace("pf-skolem-debug") << "SkolemManager::convertInternal: " << toWitness
<< " " << n << std::endl;
WitnessFormAttribute wfa;
SkolemFormAttribute sfa;
@@ -153,6 +161,10 @@ Node ProofSkolemCache::convertInternal(Node n, bool toWitness)
{
visited[cur] = Node::null();
visit.push_back(cur);
+ if (cur.getMetaKind() == metakind::PARAMETERIZED)
+ {
+ visit.push_back(cur.getOperator());
+ }
for (const Node& cn : cur)
{
visit.push_back(cn);
@@ -166,7 +178,11 @@ Node ProofSkolemCache::convertInternal(Node n, bool toWitness)
std::vector<Node> children;
if (cur.getMetaKind() == metakind::PARAMETERIZED)
{
- children.push_back(cur.getOperator());
+ it = visited.find(cur.getOperator());
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ childChanged = childChanged || cur.getOperator() != it->second;
+ children.push_back(it->second);
}
for (const Node& cn : cur)
{
@@ -186,6 +202,14 @@ Node ProofSkolemCache::convertInternal(Node n, bool toWitness)
}
else
{
+ // notice that WITNESS terms t may be assigned a skolem form that is
+ // of kind WITNESS here, if t contains a free variable. This is due to
+ // the fact that witness terms in the bodies of quantified formulas are
+ // not eliminated and thus may appear in places where getSkolemForm is
+ // called on them. Regardless, witness terms with free variables
+ // should never be themselves assigned skolems (otherwise we would have
+ // assertions with free variables), and thus they can be treated like
+ // ordinary terms here.
cur.setAttribute(sfa, ret);
}
visited[cur] = ret;
@@ -197,14 +221,14 @@ Node ProofSkolemCache::convertInternal(Node n, bool toWitness)
return visited[n];
}
-void ProofSkolemCache::convertToWitnessFormVec(std::vector<Node>& vec)
+void SkolemManager::convertToWitnessFormVec(std::vector<Node>& vec)
{
for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
{
vec[i] = getWitnessForm(vec[i]);
}
}
-void ProofSkolemCache::convertToSkolemFormVec(std::vector<Node>& vec)
+void SkolemManager::convertToSkolemFormVec(std::vector<Node>& vec)
{
for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
{
@@ -212,10 +236,10 @@ void ProofSkolemCache::convertToSkolemFormVec(std::vector<Node>& vec)
}
}
-Node ProofSkolemCache::getOrMakeSkolem(Node w,
- const std::string& prefix,
- const std::string& comment,
- int flags)
+Node SkolemManager::getOrMakeSkolem(Node w,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags)
{
Assert(w.getKind() == WITNESS);
SkolemFormAttribute sfa;
@@ -232,7 +256,7 @@ Node ProofSkolemCache::getOrMakeSkolem(Node w,
k.setAttribute(wfa, w);
// set skolem form attribute for w
w.setAttribute(sfa, k);
- Trace("pf-skolem") << "ProofSkolemCache::mkSkolem: " << k << " : " << w
+ Trace("pf-skolem") << "SkolemManager::mkSkolem: " << k << " : " << w
<< std::endl;
return k;
}
diff --git a/src/expr/proof_skolem_cache.h b/src/expr/skolem_manager.h
index c0de1e472..eaf74bcce 100644
--- a/src/expr/proof_skolem_cache.h
+++ b/src/expr/skolem_manager.h
@@ -1,5 +1,5 @@
/********************* */
-/*! \file proof_skolem_cache.h
+/*! \file skolem_manager.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
@@ -9,13 +9,13 @@
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Proof skolem cache utility
+ ** \brief Skolem manager utility
**/
#include "cvc4_private.h"
-#ifndef CVC4__EXPR__PROOF_SKOLEM_CACHE_H
-#define CVC4__EXPR__PROOF_SKOLEM_CACHE_H
+#ifndef CVC4__EXPR__SKOLEM_MANAGER_H
+#define CVC4__EXPR__SKOLEM_MANAGER_H
#include <string>
@@ -23,6 +23,8 @@
namespace CVC4 {
+class ProofGenerator;
+
/**
* A manager for skolems that can be used in proofs. This is designed to be
* a trusted interface to NodeManager::mkSkolem, where one
@@ -34,11 +36,11 @@ namespace CVC4 {
* reference counting of skolem variables which may be deleted if they are not
* used.
*/
-class ProofSkolemCache
+class SkolemManager
{
public:
- ProofSkolemCache() {}
- ~ProofSkolemCache() {}
+ SkolemManager() {}
+ ~SkolemManager() {}
/**
* This makes a skolem of same type as bound variable v, (say its type is T),
* whose definition is (witness ((v T)) pred). This definition is maintained
@@ -81,13 +83,17 @@ class ProofSkolemCache
* @param prefix The prefix of the name of the Skolem
* @param comment Debug information about the Skolem
* @param flags The flags for the Skolem (see NodeManager::mkSkolem)
+ * @param pg The proof generator for this skolem. If non-null, this proof
+ * generator must respond to a call to getProofFor(exists x. pred) during
+ * the lifetime of the current node manager.
* @return The skolem whose witness form is registered by this class.
*/
- static Node mkSkolem(Node v,
- Node pred,
- const std::string& prefix,
- const std::string& comment = "",
- int flags = NodeManager::SKOLEM_DEFAULT);
+ Node mkSkolem(Node v,
+ Node pred,
+ const std::string& prefix,
+ const std::string& comment = "",
+ int flags = NodeManager::SKOLEM_DEFAULT,
+ ProofGenerator* pg = nullptr);
/**
* Same as above, but where pred is an existential quantified formula
* whose bound variable list contains v. For example, calling this method on:
@@ -97,21 +103,30 @@ class ProofSkolemCache
* If the variable v is not in the bound variable list of q, then null is
* returned and an assertion failure is thrown.
*/
- static Node mkSkolemExists(Node v,
- Node q,
- const std::string& prefix,
- const std::string& comment = "",
- int flags = NodeManager::SKOLEM_DEFAULT);
+ Node mkSkolemExists(Node v,
+ Node q,
+ const std::string& prefix,
+ const std::string& comment = "",
+ int flags = NodeManager::SKOLEM_DEFAULT,
+ ProofGenerator* pg = nullptr);
/**
* Same as above, but for special case of (witness ((x T)) (= x t))
* where T is the type of t. This skolem is unique for each t, which we
* implement via an attribute on t. This attribute is used to ensure to
* associate a unique skolem for each t.
+ *
+ * Notice that a purification skolem is trivial to justify, and hence it
+ * does not require a proof generator.
+ */
+ Node mkPurifySkolem(Node t,
+ const std::string& prefix,
+ const std::string& comment = "",
+ int flags = NodeManager::SKOLEM_DEFAULT);
+ /**
+ * Get proof generator for witness term t. This returns the proof generator
+ * that was provided in a call to mkSkolem above.
*/
- static Node mkPurifySkolem(Node t,
- const std::string& prefix,
- const std::string& comment = "",
- int flags = NodeManager::SKOLEM_DEFAULT);
+ ProofGenerator* getProofGenerator(Node t);
/** convert to witness form
*
* @param n The term or formula to convert to witness form described above
@@ -130,6 +145,10 @@ class ProofSkolemCache
static void convertToSkolemFormVec(std::vector<Node>& vec);
private:
+ /**
+ * Mapping from witness terms to proof generators.
+ */
+ std::map<Node, ProofGenerator*> d_gens;
/** Convert to witness or skolem form */
static Node convertInternal(Node n, bool toWitness);
/** Get or make skolem attribute for witness term w */
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