summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preprocessing/passes/apply_substs.cpp2
-rw-r--r--src/preprocessing/passes/non_clausal_simp.cpp18
-rw-r--r--src/preprocessing/preprocessing_pass_context.cpp4
-rw-r--r--src/smt/abduction_solver.cpp4
-rw-r--r--src/smt/check_models.cpp18
-rw-r--r--src/smt/check_models.h10
-rw-r--r--src/smt/expand_definitions.cpp54
-rw-r--r--src/smt/expand_definitions.h16
-rw-r--r--src/smt/interpolation_solver.cpp4
-rw-r--r--src/smt/preprocessor.cpp25
-rw-r--r--src/smt/preprocessor.h8
-rw-r--r--src/smt/smt_engine.cpp22
-rw-r--r--src/smt/smt_engine.h10
-rw-r--r--src/theory/datatypes/sygus_datatype_utils.cpp56
-rw-r--r--src/theory/datatypes/sygus_datatype_utils.h5
-rw-r--r--src/theory/quantifiers/ematching/candidate_generator.cpp5
-rw-r--r--src/theory/rewriter.cpp5
-rw-r--r--src/theory/rewriter.h3
-rw-r--r--src/theory/trust_substitutions.cpp7
-rw-r--r--src/theory/trust_substitutions.h4
20 files changed, 111 insertions, 169 deletions
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 20c173316..2e40cbd5b 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -55,7 +55,7 @@ PreprocessingPassResult ApplySubsts::applyInternal(
<< std::endl;
d_preprocContext->spendResource(Resource::PreprocessStep);
assertionsToPreprocess->replaceTrusted(
- i, tlsm.apply((*assertionsToPreprocess)[i]));
+ i, tlsm.applyTrusted((*assertionsToPreprocess)[i]));
Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i]
<< std::endl;
}
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index af1e09eca..2fcc6f76f 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -298,7 +298,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
Node assertion = (*assertionsToPreprocess)[i];
- TrustNode assertionNew = newSubstitutions->apply(assertion);
+ TrustNode assertionNew = newSubstitutions->applyTrusted(assertion);
Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl;
if (!assertionNew.isNull())
{
@@ -310,7 +310,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
}
for (;;)
{
- assertionNew = constantPropagations->apply(assertion);
+ assertionNew = constantPropagations->applyTrusted(assertion);
if (assertionNew.isNull())
{
break;
@@ -332,7 +332,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos)
{
Node lhs = (*pos).first;
- TrustNode trhs = newSubstitutions->apply((*pos).second);
+ TrustNode trhs = newSubstitutions->applyTrusted((*pos).second);
Node rhs = trhs.isNull() ? (*pos).second : trhs.getNode();
// If using incremental, we must check whether this variable has occurred
// before now. If it hasn't we can add this as a substitution.
@@ -351,10 +351,10 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
Trace("non-clausal-simplify")
<< "substitute: will notify SAT layer of substitution: " << eq
<< std::endl;
- trhs = newSubstitutions->apply((*pos).first);
- Assert(!trhs.isNull());
- assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
- trhs.getGenerator());
+ trhs = newSubstitutions->applyTrusted((*pos).first);
+ Assert(!trhs.isNull());
+ assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
+ trhs.getGenerator());
}
}
@@ -450,7 +450,7 @@ Node NonClausalSimp::processLearnedLit(Node lit,
TrustNode tlit;
if (subs != nullptr)
{
- tlit = subs->apply(lit);
+ tlit = subs->applyTrusted(lit);
if (!tlit.isNull())
{
lit = processRewrittenLearnedLit(tlit);
@@ -463,7 +463,7 @@ Node NonClausalSimp::processLearnedLit(Node lit,
{
for (;;)
{
- tlit = cp->apply(lit);
+ tlit = cp->applyTrusted(lit);
if (tlit.isNull())
{
break;
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 99798e7d7..139fa4153 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -70,8 +70,8 @@ void PreprocessingPassContext::recordSymbolsInAssertions(
void PreprocessingPassContext::addModelSubstitution(const Node& lhs,
const Node& rhs)
{
- getTheoryEngine()->getModel()->addSubstitution(
- lhs, d_smt->expandDefinitions(rhs, false));
+ getTheoryEngine()->getModel()->addSubstitution(lhs,
+ d_smt->expandDefinitions(rhs));
}
void PreprocessingPassContext::addSubstitution(const Node& lhs,
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 23f46cc58..6be05c6b7 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -19,11 +19,13 @@
#include "base/modal_exception.h"
#include "options/smt_options.h"
+#include "smt/env.h"
#include "smt/smt_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/sygus_abduct.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/smt_engine_subsolver.h"
+#include "theory/trust_substitutions.h"
using namespace cvc5::theory;
@@ -46,7 +48,7 @@ bool AbductionSolver::getAbduct(const Node& goal,
std::vector<Node> axioms = d_parent->getExpandedAssertions();
std::vector<Node> asserts(axioms.begin(), axioms.end());
// must expand definitions
- Node conjn = d_parent->expandDefinitions(goal);
+ Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(goal);
// now negate
conjn = conjn.negate();
d_abdConj = conjn;
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index f6d1da345..3d5429635 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -17,6 +17,7 @@
#include "base/modal_exception.h"
#include "options/smt_options.h"
+#include "smt/env.h"
#include "smt/model.h"
#include "smt/node_command.h"
#include "smt/preprocessor.h"
@@ -30,7 +31,7 @@ using namespace cvc5::theory;
namespace cvc5 {
namespace smt {
-CheckModels::CheckModels(SmtSolver& s) : d_smt(s) {}
+CheckModels::CheckModels(Env& e) : d_env(e) {}
CheckModels::~CheckModels() {}
void CheckModels::checkModel(Model* m,
@@ -50,16 +51,7 @@ void CheckModels::checkModel(Model* m,
"Cannot run check-model on a model with approximate values.");
}
- // Check individual theory assertions
- if (options::debugCheckModels())
- {
- TheoryEngine* te = d_smt.getTheoryEngine();
- Assert(te != nullptr);
- te->checkTheoryAssertionsWithModel(hardFailure);
- }
-
- Preprocessor* pp = d_smt.getPreprocessor();
-
+ theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
Trace("check-model") << "checkModel: Check assertions..." << std::endl;
std::unordered_map<Node, Node, NodeHashFunction> cache;
// the list of assertions that did not rewrite to true
@@ -75,8 +67,8 @@ void CheckModels::checkModel(Model* m,
// evaluate e.g. divide-by-zero. This is intentional since the evaluation
// is not trustworthy, since the UF introduced by expanding definitions may
// not be properly constrained.
- Node n = pp->expandDefinitions(assertion, cache, true);
- Notice() << "SmtEngine::checkModel(): -- expands to " << n << std::endl;
+ Node n = sm.apply(assertion, false);
+ Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << std::endl;
n = Rewriter::rewrite(n);
Notice() << "SmtEngine::checkModel(): -- rewrites to " << n << std::endl;
diff --git a/src/smt/check_models.h b/src/smt/check_models.h
index 9b6780ddf..ce06bae07 100644
--- a/src/smt/check_models.h
+++ b/src/smt/check_models.h
@@ -22,10 +22,12 @@
#include "expr/node.h"
namespace cvc5 {
+
+class Env;
+
namespace smt {
class Model;
-class SmtSolver;
/**
* This utility is responsible for checking the current model.
@@ -33,7 +35,7 @@ class SmtSolver;
class CheckModels
{
public:
- CheckModels(SmtSolver& s);
+ CheckModels(Env& e);
~CheckModels();
/**
* Check model m against the current set of input assertions al.
@@ -44,8 +46,8 @@ class CheckModels
void checkModel(Model* m, context::CDList<Node>* al, bool hardFailure);
private:
- /** Reference to the SMT solver */
- SmtSolver& d_smt;
+ /** Reference to the environment */
+ Env& d_env;
};
} // namespace smt
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 14182a46d..349736d15 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -19,11 +19,14 @@
#include <utility>
#include "expr/node_manager_attributes.h"
+#include "expr/term_conversion_proof_generator.h"
#include "preprocessing/assertion_pipeline.h"
#include "smt/env.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_stats.h"
-#include "theory/theory_engine.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+#include "util/resource_manager.h"
using namespace cvc5::preprocessing;
using namespace cvc5::theory;
@@ -32,26 +35,23 @@ using namespace cvc5::kind;
namespace cvc5 {
namespace smt {
-ExpandDefs::ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats)
- : d_smt(smt), d_env(env), d_smtStats(stats), d_tpg(nullptr)
+ExpandDefs::ExpandDefs(Env& env, SmtEngineStatistics& stats)
+ : d_env(env), d_smtStats(stats), d_tpg(nullptr)
{
}
ExpandDefs::~ExpandDefs() {}
Node ExpandDefs::expandDefinitions(
- TNode n,
- std::unordered_map<Node, Node, NodeHashFunction>& cache,
- bool expandOnly)
+ TNode n, std::unordered_map<Node, Node, NodeHashFunction>& cache)
{
- TrustNode trn = expandDefinitions(n, cache, expandOnly, nullptr);
+ TrustNode trn = expandDefinitions(n, cache, nullptr);
return trn.isNull() ? Node(n) : trn.getNode();
}
TrustNode ExpandDefs::expandDefinitions(
TNode n,
std::unordered_map<Node, Node, NodeHashFunction>& cache,
- bool expandOnly,
TConvProofGenerator* tpg)
{
const TNode orig = n;
@@ -62,9 +62,11 @@ TrustNode ExpandDefs::expandDefinitions(
// output / rewritten node and finally a flag tracking whether the children
// have been explored (i.e. if this is a downward or upward pass).
+ ResourceManager* rm = d_env.getResourceManager();
+ Rewriter* rr = d_env.getRewriter();
do
{
- d_env.getResourceManager()->spendResource(Resource::PreprocessStep);
+ rm->spendResource(Resource::PreprocessStep);
// n is the input / original
// node is the output / result
@@ -93,30 +95,24 @@ TrustNode ExpandDefs::expandDefinitions(
result.push(ret.isNull() ? n : ret);
continue;
}
- if (!expandOnly)
- {
- // do not do any theory stuff if expandOnly is true
+ theory::TheoryId tid = theory::Theory::theoryOf(node);
+ theory::TheoryRewriter* tr = rr->getTheoryRewriter(tid);
- theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node);
- theory::TheoryRewriter* tr = t->getTheoryRewriter();
-
- Assert(t != NULL);
- TrustNode trn = tr->expandDefinition(n);
- if (!trn.isNull())
- {
- node = trn.getNode();
- if (tpg != nullptr)
- {
- tpg->addRewriteStep(
- n, node, trn.getGenerator(), true, PfRule::THEORY_EXPAND_DEF);
- }
- }
- else
+ Assert(tr != NULL);
+ TrustNode trn = tr->expandDefinition(n);
+ if (!trn.isNull())
+ {
+ node = trn.getNode();
+ if (tpg != nullptr)
{
- node = n;
+ tpg->addRewriteStep(
+ n, node, trn.getGenerator(), true, PfRule::THEORY_EXPAND_DEF);
}
}
-
+ else
+ {
+ node = n;
+ }
// the partial functions can fall through, in which case we still
// consider their children
worklist.push(std::make_tuple(
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index d6fe8ba0d..d4e591c31 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -27,13 +27,8 @@ namespace cvc5 {
class Env;
class ProofNodeManager;
-class SmtEngine;
class TConvProofGenerator;
-namespace preprocessing {
-class AssertionPipeline;
-}
-
namespace smt {
struct SmtEngineStatistics;
@@ -47,21 +42,17 @@ struct SmtEngineStatistics;
class ExpandDefs
{
public:
- ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats);
+ ExpandDefs(Env& env, SmtEngineStatistics& stats);
~ExpandDefs();
/**
* Expand definitions in term n. Return the expanded form of n.
*
* @param n The node to expand
* @param cache Cache of previous results
- * @param expandOnly if true, then the expandDefinitions function of
- * TheoryEngine is not called on subterms of n.
* @return The expanded term.
*/
Node expandDefinitions(
- TNode n,
- std::unordered_map<Node, Node, NodeHashFunction>& cache,
- bool expandOnly = false);
+ TNode n, std::unordered_map<Node, Node, NodeHashFunction>& cache);
/**
* Set proof node manager, which signals this class to enable proofs using the
@@ -77,10 +68,7 @@ class ExpandDefs
theory::TrustNode expandDefinitions(
TNode n,
std::unordered_map<Node, Node, NodeHashFunction>& cache,
- bool expandOnly,
TConvProofGenerator* tpg);
- /** Reference to the SMT engine */
- SmtEngine& d_smt;
/** Reference to the environment. */
Env& d_env;
/** Reference to the SMT stats */
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 813fc45cf..fbbdb1b90 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -19,11 +19,13 @@
#include "base/modal_exception.h"
#include "options/smt_options.h"
+#include "smt/env.h"
#include "smt/smt_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/sygus_interpol.h"
#include "theory/smt_engine_subsolver.h"
+#include "theory/trust_substitutions.h"
using namespace cvc5::theory;
@@ -50,7 +52,7 @@ bool InterpolationSolver::getInterpol(const Node& conj,
<< std::endl;
std::vector<Node> axioms = d_parent->getExpandedAssertions();
// must expand definitions
- Node conjn = d_parent->expandDefinitions(conj);
+ Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(conj);
std::string name("A");
quantifiers::SygusInterpol interpolSolver;
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index f434e13ca..a222568d3 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -43,8 +43,8 @@ Preprocessor::Preprocessor(SmtEngine& smt,
d_absValues(abs),
d_propagator(true, true),
d_assertionsProcessed(env.getUserContext(), false),
- d_exDefs(smt, d_env, stats),
- d_processor(smt, *smt.getResourceManager(), stats),
+ d_exDefs(env, stats),
+ d_processor(smt, *env.getResourceManager(), stats),
d_pnm(nullptr)
{
}
@@ -110,16 +110,14 @@ void Preprocessor::clearLearnedLiterals()
void Preprocessor::cleanup() { d_processor.cleanup(); }
-Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly)
+Node Preprocessor::expandDefinitions(const Node& n)
{
std::unordered_map<Node, Node, NodeHashFunction> cache;
- return expandDefinitions(n, cache, expandOnly);
+ return expandDefinitions(n, cache);
}
Node Preprocessor::expandDefinitions(
- const Node& node,
- std::unordered_map<Node, Node, NodeHashFunction>& cache,
- bool expandOnly)
+ const Node& node, std::unordered_map<Node, Node, NodeHashFunction>& cache)
{
Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl;
// Substitute out any abstract values in node.
@@ -130,13 +128,9 @@ Node Preprocessor::expandDefinitions(
n.getType(true);
}
// we apply substitutions here, before expanding definitions
- theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
- n = sm.apply(n);
- if (!expandOnly)
- {
- // expand only = true
- n = d_exDefs.expandDefinitions(n, cache, expandOnly);
- }
+ n = d_env.getTopLevelSubstitutions().apply(n, false);
+ // now call expand definitions
+ n = d_exDefs.expandDefinitions(n, cache);
return n;
}
@@ -148,8 +142,7 @@ Node Preprocessor::simplify(const Node& node)
d_smt.getOutputManager().getPrinter().toStreamCmdSimplify(
d_smt.getOutputManager().getDumpOut(), node);
}
- std::unordered_map<Node, Node, NodeHashFunction> cache;
- Node ret = expandDefinitions(node, cache, false);
+ Node ret = expandDefinitions(node);
ret = theory::Rewriter::rewrite(ret);
return ret;
}
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index e0ad2cc14..4c60a2898 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -85,16 +85,12 @@ class Preprocessor
* simplification or normalization is done.
*
* @param n The node to expand
- * @param expandOnly if true, then the expandDefinitions function of
- * TheoryEngine is not called on subterms of n.
* @return The expanded term.
*/
- Node expandDefinitions(const Node& n, bool expandOnly = false);
+ Node expandDefinitions(const Node& n);
/** Same as above, with a cache of previous results. */
Node expandDefinitions(
- const Node& n,
- std::unordered_map<Node, Node, NodeHashFunction>& cache,
- bool expandOnly = false);
+ const Node& n, std::unordered_map<Node, Node, NodeHashFunction>& cache);
/**
* Set proof node manager. Enables proofs in this preprocessor.
*/
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cccb4f544..780ed78ce 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -243,7 +243,7 @@ void SmtEngine::finishInit()
{
d_model.reset(new Model(tm));
// make the check models utility
- d_checkModels.reset(new CheckModels(*d_smtSolver.get()));
+ d_checkModels.reset(new CheckModels(*d_env.get()));
}
// global push/pop around everything, to ensure proper destruction
@@ -1129,15 +1129,13 @@ Node SmtEngine::simplify(const Node& ex)
return d_pp->simplify(ex);
}
-Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly)
+Node SmtEngine::expandDefinitions(const Node& ex)
{
- getResourceManager()->spendResource(
- Resource::PreprocessStep);
-
+ getResourceManager()->spendResource(Resource::PreprocessStep);
SmtScope smts(this);
finishInit();
d_state->doPendingPops();
- return d_pp->expandDefinitions(ex, expandOnly);
+ return d_pp->expandDefinitions(ex);
}
// TODO(#1108): Simplify the error reporting of this method.
@@ -1340,6 +1338,7 @@ std::vector<Node> SmtEngine::getExpandedAssertions()
}
return eassertsProc;
}
+Env& SmtEngine::getEnv() { return *d_env.get(); }
void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
{
@@ -1455,8 +1454,9 @@ void SmtEngine::checkUnsatCore() {
Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions"
<< std::endl;
+ theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions();
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
- Node assertionAfterExpansion = expandDefinitions(*i);
+ Node assertionAfterExpansion = tls.apply(*i, false);
Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< ", expanded to " << assertionAfterExpansion << "\n";
coreChecker->assertFormula(assertionAfterExpansion);
@@ -1493,6 +1493,14 @@ void SmtEngine::checkModel(bool hardFailure) {
Model* m = getAvailableModel("check model");
Assert(m != nullptr);
+ // check the model with the theory engine for debugging
+ if (options::debugCheckModels())
+ {
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ te->checkTheoryAssertionsWithModel(hardFailure);
+ }
+
// check the model with the check models utility
Assert(d_checkModels != nullptr);
d_checkModels->checkModel(m, al, hardFailure);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a7e39e004..22316b872 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -512,12 +512,10 @@ class CVC5_EXPORT SmtEngine
* Expand the definitions in a term or formula.
*
* @param n The node to expand
- * @param expandOnly if true, then the expandDefinitions function of
- * TheoryEngine is not called on subterms of n.
*
* @throw TypeCheckingException, LogicException, UnsafeInterruptException
*/
- Node expandDefinitions(const Node& n, bool expandOnly = true);
+ Node expandDefinitions(const Node& n);
/**
* Get the assigned value of an expr (only if immediately preceded by a SAT
@@ -887,6 +885,12 @@ class CVC5_EXPORT SmtEngine
* Return the set of assertions, after expanding definitions.
*/
std::vector<Node> getExpandedAssertions();
+
+ /**
+ * !!!!! temporary, until the environment is passsed to all classes that
+ * require it.
+ */
+ Env& getEnv();
/* ....................................................................... */
private:
/* ....................................................................... */
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 008e9c015..4b0c17bee 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -21,6 +21,7 @@
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
#include "expr/sygus_datatype.h"
+#include "smt/env.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/evaluator.h"
@@ -138,60 +139,6 @@ Kind getEliminateKind(Kind ok)
return nk;
}
-Node eliminatePartialOperators(Node n)
-{
- NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
- std::vector<TNode> visit;
- TNode cur;
- visit.push_back(n);
- do
- {
- cur = visit.back();
- visit.pop_back();
- it = visited.find(cur);
-
- 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);
- }
- Kind ok = cur.getKind();
- Kind nk = getEliminateKind(ok);
- if (nk != ok || childChanged)
- {
- ret = nm->mkNode(nk, children);
- }
- visited[cur] = ret;
- }
- } while (!visit.empty());
- Assert(visited.find(n) != visited.end());
- Assert(!visited.find(n)->second.isNull());
- return visited[n];
-}
-
Node mkSygusTerm(const DType& dt,
unsigned i,
const std::vector<Node>& children,
@@ -235,7 +182,6 @@ Node mkSygusTerm(const DType& dt,
// expandDefinitions.
opn = smt::currentSmtEngine()->expandDefinitions(op);
opn = Rewriter::rewrite(opn);
- opn = eliminatePartialOperators(opn);
SygusOpRewrittenAttribute sora;
op.setAttribute(sora, opn);
}
diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h
index 77aa7ac54..63e8a057a 100644
--- a/src/theory/datatypes/sygus_datatype_utils.h
+++ b/src/theory/datatypes/sygus_datatype_utils.h
@@ -86,11 +86,6 @@ Kind getOperatorKindForSygusBuiltin(Node op);
* otherwise k itself.
*/
Kind getEliminateKind(Kind k);
-/**
- * Returns a version of n where all partial functions such as bvudiv
- * have been replaced by their total versions like bvudiv_total.
- */
-Node eliminatePartialOperators(Node n);
/** make sygus term
*
* This function returns a builtin term f( children[0], ..., children[n] )
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 93ef072fa..5295302c4 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -289,7 +289,10 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
{
Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
Assert(mpat.getKind() == APPLY_SELECTOR);
- Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat, false);
+ // NOTE: could use qs.getValuation().getPreprocessedTerm(mpat); when
+ // expand definitions is eliminated, however, this also requires avoiding
+ // term formula removal.
+ Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat);
Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
if (mpatExp.getKind() == ITE)
{
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 5cea6592c..2b2604593 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -179,6 +179,11 @@ void Rewriter::registerPostRewriteEqual(
d_postRewritersEqual[tid] = fn;
}
+TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)
+{
+ return d_theoryRewriters[theoryId];
+}
+
Rewriter* Rewriter::getInstance()
{
return smt::currentSmtEngine()->getRewriter();
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 3f4676fa0..b3ea3b542 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -147,6 +147,9 @@ class Rewriter {
theory::TheoryId tid,
std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
+ /** Get the theory rewriter for the given id */
+ TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId);
+
private:
/**
* Get the rewriter associated with the SmtEngine in scope.
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index 47507bfe0..7a2fb19bd 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -146,7 +146,7 @@ void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
}
}
-TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
+TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite)
{
Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
<< std::endl;
@@ -169,6 +169,11 @@ TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
return TrustNode::mkTrustRewrite(n, ns, this);
}
+Node TrustSubstitutionMap::apply(Node n, bool doRewrite)
+{
+ return d_subs.apply(n, doRewrite);
+}
+
std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
{
Assert(eq.getKind() == kind::EQUAL);
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index ec5b2ffb5..b7b526205 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -89,7 +89,9 @@ class TrustSubstitutionMap : public ProofGenerator
* proving n = n*sigma, where the proof generator is provided by this class
* (when proofs are enabled).
*/
- TrustNode apply(Node n, bool doRewrite = true);
+ TrustNode applyTrusted(Node n, bool doRewrite = true);
+ /** Same as above, without proofs */
+ Node apply(Node n, bool doRewrite = true);
/** Get the proof for formula f */
std::shared_ptr<ProofNode> getProofFor(Node f) override;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback