This removes the expandOnly flag from expandDefinitions.
The use of expandOnly = true is equivalent to applying top-level substitutions only, which should be done explicitly via Env::getTopLevelSubstitutions. It updates the trust substitutions utility to distinguish apply vs applyTrusted for convenience for this purpose.
This also breaks several dependencies in e.g. expand definitions module.
<< 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;
}
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())
{
}
for (;;)
{
- assertionNew = constantPropagations->apply(assertion);
+ assertionNew = constantPropagations->applyTrusted(assertion);
if (assertionNew.isNull())
{
break;
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.
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());
}
}
TrustNode tlit;
if (subs != nullptr)
{
- tlit = subs->apply(lit);
+ tlit = subs->applyTrusted(lit);
if (!tlit.isNull())
{
lit = processRewrittenLearnedLit(tlit);
{
for (;;)
{
- tlit = cp->apply(lit);
+ tlit = cp->applyTrusted(lit);
if (tlit.isNull())
{
break;
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,
#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;
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;
#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"
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,
"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
// 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;
#include "expr/node.h"
namespace cvc5 {
+
+class Env;
+
namespace smt {
class Model;
-class SmtSolver;
/**
* This utility is responsible for checking the current model.
class CheckModels
{
public:
- CheckModels(SmtSolver& s);
+ CheckModels(Env& e);
~CheckModels();
/**
* Check model m against the current set of input assertions al.
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
#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;
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;
// 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
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(
class Env;
class ProofNodeManager;
-class SmtEngine;
class TConvProofGenerator;
-namespace preprocessing {
-class AssertionPipeline;
-}
-
namespace smt {
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
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 */
#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;
<< 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;
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)
{
}
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.
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;
}
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;
}
* 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.
*/
{
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
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.
}
return eassertsProc;
}
+Env& SmtEngine::getEnv() { return *d_env.get(); }
void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
{
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);
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);
* 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
* 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:
/* ....................................................................... */
#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"
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,
// expandDefinitions.
opn = smt::currentSmtEngine()->expandDefinitions(op);
opn = Rewriter::rewrite(opn);
- opn = eliminatePartialOperators(opn);
SygusOpRewrittenAttribute sora;
op.setAttribute(sora, opn);
}
* 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] )
{
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)
{
d_postRewritersEqual[tid] = fn;
}
+TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)
+{
+ return d_theoryRewriters[theoryId];
+}
+
Rewriter* Rewriter::getInstance()
{
return smt::currentSmtEngine()->getRewriter();
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.
}
}
-TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
+TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite)
{
Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
<< std::endl;
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);
* 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;
projects / cvc5.git / commitdiff