From: Andrew Reynolds Date: Fri, 30 Apr 2021 19:12:56 +0000 (-0500) Subject: Use substitutions for implementing defined functions (#6437) X-Git-Tag: cvc5-1.0.0~1809 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=327a24508ed1d02a3fa233e680ffd0b30aa685a9;p=cvc5.git Use substitutions for implementing defined functions (#6437) This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions. In other words, the effect of: (define-fun f X t) is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when (= f (lambda X t)) was an equality solved by non-clausal simplification The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula. In this PR: define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline. Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit. The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions. The proof manager does not require a special case of using the define-function maps. Define-function maps are eliminated from SmtEngine. Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e59832896..af206c14d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -220,7 +220,6 @@ libcvc5_add_sources( smt/check_models.h smt/command.cpp smt/command.h - smt/defined_function.h smt/dump.cpp smt/dump.h smt/dump_manager.cpp diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 4be6b4aac..99798e7d7 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -16,6 +16,7 @@ #include "preprocessing/preprocessing_pass_context.h" #include "expr/node_algorithm.h" +#include "smt/env.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" @@ -24,23 +25,33 @@ namespace preprocessing { PreprocessingPassContext::PreprocessingPassContext( SmtEngine* smt, - theory::booleans::CircuitPropagator* circuitPropagator, - ProofNodeManager* pnm) + Env& env, + theory::booleans::CircuitPropagator* circuitPropagator) : d_smt(smt), - d_resourceManager(smt->getResourceManager()), - d_topLevelSubstitutions(smt->getUserContext(), pnm), + d_env(env), d_circuitPropagator(circuitPropagator), - d_pnm(pnm), - d_symsInAssertions(smt->getUserContext()) + d_symsInAssertions(env.getUserContext()) { } theory::TrustSubstitutionMap& PreprocessingPassContext::getTopLevelSubstitutions() { - return d_topLevelSubstitutions; + return d_env.getTopLevelSubstitutions(); } +context::Context* PreprocessingPassContext::getUserContext() +{ + return d_env.getUserContext(); +} +context::Context* PreprocessingPassContext::getDecisionContext() +{ + return d_env.getContext(); +} +void PreprocessingPassContext::spendResource(Resource r) +{ + d_env.getResourceManager()->spendResource(r); +} void PreprocessingPassContext::recordSymbolsInAssertions( const std::vector& assertions) { @@ -67,14 +78,24 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs, const Node& rhs, ProofGenerator* pg) { - d_topLevelSubstitutions.addSubstitution(lhs, rhs, pg); + getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg); + // also add as a model substitution + addModelSubstitution(lhs, rhs); +} + +void PreprocessingPassContext::addSubstitution(const Node& lhs, + const Node& rhs, + PfRule id, + const std::vector& args) +{ + getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args); // also add as a model substitution addModelSubstitution(lhs, rhs); } ProofNodeManager* PreprocessingPassContext::getProofNodeManager() { - return d_pnm; + return d_env.getProofNodeManager(); } } // namespace preprocessing diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index a7e9b0deb..a4ca166d8 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -43,14 +43,14 @@ class PreprocessingPassContext public: PreprocessingPassContext( SmtEngine* smt, - theory::booleans::CircuitPropagator* circuitPropagator, - ProofNodeManager* pnm); + Env& env, + theory::booleans::CircuitPropagator* circuitPropagator); SmtEngine* getSmt() { return d_smt; } TheoryEngine* getTheoryEngine() { return d_smt->getTheoryEngine(); } prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); } - context::Context* getUserContext() { return d_smt->getUserContext(); } - context::Context* getDecisionContext() { return d_smt->getContext(); } + context::Context* getUserContext(); + context::Context* getDecisionContext(); theory::booleans::CircuitPropagator* getCircuitPropagator() { @@ -62,10 +62,7 @@ class PreprocessingPassContext return d_symsInAssertions; } - void spendResource(Resource r) - { - d_resourceManager->spendResource(r); - } + void spendResource(Resource r); /** Get the current logic info of the SmtEngine */ const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); } @@ -97,6 +94,11 @@ class PreprocessingPassContext void addSubstitution(const Node& lhs, const Node& rhs, ProofGenerator* pg = nullptr); + /** Same as above, with proof id */ + void addSubstitution(const Node& lhs, + const Node& rhs, + PfRule id, + const std::vector& args); /** The the proof node manager associated with this context, if it exists */ ProofNodeManager* getProofNodeManager(); @@ -104,18 +106,10 @@ class PreprocessingPassContext private: /** Pointer to the SmtEngine that this context was created in. */ SmtEngine* d_smt; - - /** Pointer to the ResourceManager for this context. */ - ResourceManager* d_resourceManager; - - /* The top level substitutions */ - theory::TrustSubstitutionMap d_topLevelSubstitutions; - + /** Reference to the environment. */ + Env& d_env; /** Instance of the circuit propagator */ theory::booleans::CircuitPropagator* d_circuitPropagator; - /** Pointer to the proof node manager, if it exists */ - ProofNodeManager* d_pnm; - /** * The (user-context-dependent) set of symbols that occur in at least one * assertion in the current user context. diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 779a63c29..7dc2e915d 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -25,7 +25,9 @@ #include "options/smt_options.h" #include "proof/proof_manager.h" #include "smt/abstract_values.h" +#include "smt/env.h" #include "smt/smt_engine.h" +#include "theory/trust_substitutions.h" using namespace cvc5::theory; using namespace cvc5::kind; @@ -33,10 +35,11 @@ using namespace cvc5::kind; namespace cvc5 { namespace smt { -Assertions::Assertions(context::UserContext* u, AbstractValues& absv) - : d_userContext(u), +Assertions::Assertions(Env& env, AbstractValues& absv) + : d_env(env), d_absValues(absv), - d_assertionList(nullptr), + d_produceAssertions(false), + d_assertionList(env.getUserContext()), d_globalNegation(false), d_assertions() { @@ -44,10 +47,6 @@ Assertions::Assertions(context::UserContext* u, AbstractValues& absv) Assertions::~Assertions() { - if (d_assertionList != nullptr) - { - d_assertionList->deleteSelf(); - } } void Assertions::finishInit() @@ -60,8 +59,8 @@ void Assertions::finishInit() { // In the case of incremental solving, we appear to need these to // ensure the relevant Nodes remain live. - d_assertionList = new (true) AssertionList(d_userContext); - d_globalDefineFunRecLemmas.reset(new std::vector()); + d_produceAssertions = true; + d_globalDefineFunLemmas.reset(new std::vector()); } } @@ -107,16 +106,16 @@ void Assertions::initializeCheckSat(const std::vector& assumptions, Node n = d_absValues.substituteAbstractValues(e); // Ensure expr is type-checked at this point. ensureBoolean(n); - addFormula(n, inUnsatCore, true, true, false); + addFormula(n, inUnsatCore, true, true, false, false); } - if (d_globalDefineFunRecLemmas != nullptr) + if (d_globalDefineFunLemmas != nullptr) { // Global definitions are asserted at check-sat-time because we have to // make sure that they are always present (they are essentially level // zero assertions) - for (const Node& lemma : *d_globalDefineFunRecLemmas) + for (const Node& lemma : *d_globalDefineFunLemmas) { - addFormula(lemma, false, true, false, false); + addFormula(lemma, false, true, false, true, false); } } } @@ -125,7 +124,7 @@ void Assertions::assertFormula(const Node& n, bool inUnsatCore) { ensureBoolean(n); bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); - addFormula(n, inUnsatCore, true, false, maybeHasFv); + addFormula(n, inUnsatCore, true, false, false, maybeHasFv); } std::vector& Assertions::getAssumptions() { return d_assumptions; } @@ -139,27 +138,43 @@ preprocessing::AssertionPipeline& Assertions::getAssertionPipeline() context::CDList* Assertions::getAssertionList() { - return d_assertionList; + return d_produceAssertions ? &d_assertionList : nullptr; } -void Assertions::addFormula( - TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv) +void Assertions::addFormula(TNode n, + bool inUnsatCore, + bool inInput, + bool isAssumption, + bool isFunDef, + bool maybeHasFv) { // add to assertion list if it exists - if (d_assertionList != nullptr) + if (d_produceAssertions) { - d_assertionList->push_back(n); + d_assertionList.push_back(n); } if (n.isConst() && n.getConst()) { // true, nothing to do return; } - Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput - << ", isAssumption = " << isAssumption << std::endl; + << ", isAssumption = " << isAssumption + << ", isFunDef = " << isFunDef << std::endl; + if (isFunDef) + { + // if a non-recursive define-fun, just add as a top-level substitution + if (n.getKind() == EQUAL && n[0].isVar()) + { + // A define-fun is an assumption in the overall proof, thus + // we justify the substitution with ASSUME here. + d_env.getTopLevelSubstitutions().addSubstitution( + n[0], n[1], PfRule::ASSUME, {}, {n}); + return; + } + } // Ensure that it does not contain free variables if (maybeHasFv) @@ -201,24 +216,21 @@ void Assertions::addFormula( d_assertions.push_back(n, isAssumption, true); } -void Assertions::addDefineFunRecDefinition(Node n, bool global) +void Assertions::addDefineFunDefinition(Node n, bool global) { n = d_absValues.substituteAbstractValues(n); - if (d_assertionList != nullptr) - { - d_assertionList->push_back(n); - } - if (global && d_globalDefineFunRecLemmas != nullptr) + if (global && d_globalDefineFunLemmas != nullptr) { // Global definitions are asserted at check-sat-time because we have to // make sure that they are always present Assert(!language::isInputLangSygus(options::inputLanguage())); - d_globalDefineFunRecLemmas->emplace_back(n); + d_globalDefineFunLemmas->emplace_back(n); } else { - bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); - addFormula(n, false, true, false, maybeHasFv); + // we don't check for free variables here, since even if we are sygus, + // we could contain functions-to-synthesize within definitions. + addFormula(n, false, true, false, true, false); } } diff --git a/src/smt/assertions.h b/src/smt/assertions.h index 6ac3e58f5..c922cbaea 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -25,6 +25,9 @@ #include "preprocessing/assertion_pipeline.h" namespace cvc5 { + +class Env; + namespace smt { class AbstractValues; @@ -42,7 +45,7 @@ class Assertions typedef context::CDList AssertionList; public: - Assertions(context::UserContext* u, AbstractValues& absv); + Assertions(Env& env, AbstractValues& absv); ~Assertions(); /** * Finish initialization, called once after options are finalized. Sets up @@ -81,12 +84,13 @@ class Assertions */ void assertFormula(const Node& n, bool inUnsatCore = true); /** - * Assert that n corresponds to an assertion from a define-fun-rec command. + * Assert that n corresponds to an assertion from a define-fun or + * define-fun-rec command. * This assertion is added to the set of assertions maintained by this class. * If this has a global definition, this assertion is persistent for any * subsequent check-sat calls. */ - void addDefineFunRecDefinition(Node n, bool global); + void addDefineFunDefinition(Node n, bool global); /** * Get the assertions pipeline, which contains the set of assertions we are * currently processing. @@ -144,21 +148,24 @@ class Assertions bool inUnsatCore, bool inInput, bool isAssumption, + bool isFunDef, bool maybeHasFv); - /** pointer to the user context */ - context::UserContext* d_userContext; + /** Reference to the environment. */ + Env& d_env; /** Reference to the abstract values utility */ AbstractValues& d_absValues; + /** Whether we are producing assertions */ + bool d_produceAssertions; /** * The assertion list (before any conversion) for supporting * getAssertions(). Only maintained if in incremental mode. */ - AssertionList* d_assertionList; + AssertionList d_assertionList; /** - * List of lemmas generated for global recursive function definitions. We + * List of lemmas generated for global (recursive) function definitions. We * assert this list of definitions in each check-sat call. */ - std::unique_ptr> d_globalDefineFunRecLemmas; + std::unique_ptr> d_globalDefineFunLemmas; /** * The list of assumptions from the previous call to checkSatisfiability. * Note that if the last call to checkSatisfiability was an entailment check, diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h deleted file mode 100644 index 89e636a65..000000000 --- a/src/smt/defined_function.h +++ /dev/null @@ -1,61 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Defined function data structure. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__SMT__DEFINED_FUNCTION_H -#define CVC5__SMT__DEFINED_FUNCTION_H - -#include - -#include "expr/node.h" - -namespace cvc5 { -namespace smt { - -/** - * Representation of a defined function. We keep these around in - * SmtEngine to permit expanding definitions late (and lazily), to - * support getValue() over defined functions, to support user output - * in terms of defined functions, etc. - */ -class DefinedFunction -{ - public: - DefinedFunction() {} - DefinedFunction(Node func, const std::vector& formals, Node formula) - : d_func(func), d_formals(formals), d_formula(formula) - { - } - /** get the function */ - Node getFunction() const { return d_func; } - /** get the formal argument list of the function */ - const std::vector& getFormals() const { return d_formals; } - /** get the formula that defines it */ - Node getFormula() const { return d_formula; } - - private: - /** the function */ - Node d_func; - /** the formal argument list */ - std::vector d_formals; - /** the formula */ - Node d_formula; -}; /* class DefinedFunction */ - -} // namespace smt -} // namespace cvc5 - -#endif /* CVC5__SMT__DEFINED_FUNCTION_H */ diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 9bb66f649..f9e2a8458 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -24,6 +24,7 @@ #include "smt/dump_manager.h" #include "smt/smt_engine_stats.h" #include "theory/rewriter.h" +#include "theory/trust_substitutions.h" #include "util/resource_manager.h" #include "util/statistics_registry.h" @@ -37,6 +38,7 @@ Env::Env(NodeManager* nm, Options* opts) d_nodeManager(nm), d_proofNodeManager(nullptr), d_rewriter(new theory::Rewriter()), + d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())), d_dumpManager(new DumpManager(d_userContext.get())), d_logic(), d_statisticsRegistry(std::make_unique()), @@ -54,8 +56,11 @@ Env::~Env() {} void Env::setProofNodeManager(ProofNodeManager* pnm) { + Assert(pnm != nullptr); + Assert(d_proofNodeManager == nullptr); d_proofNodeManager = pnm; d_rewriter->setProofNodeManager(pnm); + d_topLevelSubs->setProofNodeManager(pnm); } void Env::shutdown() @@ -76,6 +81,11 @@ ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); } +theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions() +{ + return *d_topLevelSubs.get(); +} + DumpManager* Env::getDumpManager() { return d_dumpManager.get(); } const LogicInfo& Env::getLogicInfo() const { return d_logic; } diff --git a/src/smt/env.h b/src/smt/env.h index 12e0983cb..667497683 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -44,6 +44,7 @@ class DumpManager; namespace theory { class Rewriter; +class TrustSubstitutionMap; } /** @@ -84,6 +85,9 @@ class Env /** Get a pointer to the Rewriter owned by this Env. */ theory::Rewriter* getRewriter(); + /** Get a reference to the top-level substitution map */ + theory::TrustSubstitutionMap& getTopLevelSubstitutions(); + /** Get a pointer to the underlying dump manager. */ smt::DumpManager* getDumpManager(); @@ -122,8 +126,6 @@ class Env private: /* Private initialization ------------------------------------------------- */ - /** Set the statistics registry */ - void setStatisticsRegistry(StatisticsRegistry* statReg); /** Set proof node manager if it exists */ void setProofNodeManager(ProofNodeManager* pnm); @@ -157,6 +159,8 @@ class Env * specific to an SmtEngine/TheoryEngine instance. */ std::unique_ptr d_rewriter; + /** The top level substitutions */ + std::unique_ptr d_topLevelSubs; /** The dump manager */ std::unique_ptr d_dumpManager; /** diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index d331e8e78..14182a46d 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -20,7 +20,7 @@ #include "expr/node_manager_attributes.h" #include "preprocessing/assertion_pipeline.h" -#include "smt/defined_function.h" +#include "smt/env.h" #include "smt/smt_engine.h" #include "smt/smt_engine_stats.h" #include "theory/theory_engine.h" @@ -32,10 +32,8 @@ using namespace cvc5::kind; namespace cvc5 { namespace smt { -ExpandDefs::ExpandDefs(SmtEngine& smt, - ResourceManager& rm, - SmtEngineStatistics& stats) - : d_smt(smt), d_resourceManager(rm), d_smtStats(stats), d_tpg(nullptr) +ExpandDefs::ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats) + : d_smt(smt), d_env(env), d_smtStats(stats), d_tpg(nullptr) { } @@ -57,7 +55,6 @@ TrustNode ExpandDefs::expandDefinitions( TConvProofGenerator* tpg) { const TNode orig = n; - NodeManager* nm = d_smt.getNodeManager(); std::stack> worklist; std::stack result; worklist.push(std::make_tuple(Node(n), Node(n), false)); @@ -67,7 +64,7 @@ TrustNode ExpandDefs::expandDefinitions( do { - d_resourceManager.spendResource(Resource::PreprocessStep); + d_env.getResourceManager()->spendResource(Resource::PreprocessStep); // n is the input / original // node is the output / result @@ -79,38 +76,9 @@ TrustNode ExpandDefs::expandDefinitions( // Working downwards if (!childrenPushed) { - Kind k = n.getKind(); - // we can short circuit (variable) leaves if (n.isVar()) { - SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); - SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n); - if (i != dfuns->end()) - { - Node f = (*i).second.getFormula(); - const std::vector& formals = (*i).second.getFormals(); - // replacement must be closed - if (!formals.empty()) - { - f = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, formals), f); - } - // are we are producing proofs for this call? - if (tpg != nullptr) - { - // if this is a variable, we can simply assume it - // ------- ASSUME - // n = f - Node conc = n.eqNode(f); - tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}, true); - } - // must recursively expand its definition - TrustNode tfe = expandDefinitions(f, cache, expandOnly, tpg); - Node fe = tfe.isNull() ? f : tfe.getNode(); - // don't bother putting in the cache - result.push(fe); - continue; - } // don't bother putting in the cache result.push(n); continue; @@ -125,132 +93,7 @@ TrustNode ExpandDefs::expandDefinitions( result.push(ret.isNull() ? n : ret); continue; } - - // otherwise expand it - bool doExpand = false; - if (k == APPLY_UF) - { - // Always do beta-reduction here. The reason is that there may be - // operators such as INTS_MODULUS in the body of the lambda that would - // otherwise be introduced by beta-reduction via the rewriter, but are - // not expanded here since the traversal in this function does not - // traverse the operators of nodes. Hence, we beta-reduce here to - // ensure terms in the body of the lambda are expanded during this - // call. - if (n.getOperator().getKind() == LAMBDA) - { - doExpand = true; - } - else - { - // We always check if this operator corresponds to a defined function. - doExpand = d_smt.isDefinedFunction(n.getOperator()); - } - } - // the premise of the proof of expansion (if we are expanding a definition - // and proofs are enabled) - std::vector pfExpChildren; - if (doExpand) - { - std::vector formals; - TNode fm; - if (n.getOperator().getKind() == LAMBDA) - { - TNode op = n.getOperator(); - // lambda - for (unsigned i = 0; i < op[0].getNumChildren(); i++) - { - formals.push_back(op[0][i]); - } - fm = op[1]; - } - else - { - // application of a user-defined symbol - TNode func = n.getOperator(); - SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); - SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func); - if (i == dfuns->end()) - { - throw TypeCheckingExceptionPrivate( - n, - std::string("Undefined function: `") + func.toString() + "'"); - } - DefinedFunction def = (*i).second; - formals = def.getFormals(); - - if (Debug.isOn("expand")) - { - Debug("expand") << "found: " << n << std::endl; - Debug("expand") << " func: " << func << std::endl; - std::string name = func.getAttribute(expr::VarNameAttr()); - Debug("expand") << " : \"" << name << "\"" << std::endl; - } - if (Debug.isOn("expand")) - { - Debug("expand") << " defn: " << def.getFunction() << std::endl - << " ["; - if (formals.size() > 0) - { - copy(formals.begin(), - formals.end() - 1, - std::ostream_iterator(Debug("expand"), ", ")); - Debug("expand") << formals.back(); - } - Debug("expand") - << "]" << std::endl - << " " << def.getFunction().getType() << std::endl - << " " << def.getFormula() << std::endl; - } - - fm = def.getFormula(); - // are we producing proofs for this call? - if (tpg != nullptr) - { - Node pfRhs = fm; - if (!formals.empty()) - { - Node bvl = nm->mkNode(BOUND_VAR_LIST, formals); - pfRhs = nm->mkNode(LAMBDA, bvl, pfRhs); - } - Assert(func.getType().isComparableTo(pfRhs.getType())); - pfExpChildren.push_back(func.eqNode(pfRhs)); - } - } - - Node instance = fm.substitute(formals.begin(), - formals.end(), - n.begin(), - n.begin() + formals.size()); - Debug("expand") << "made : " << instance << std::endl; - // are we producing proofs for this call? - if (tpg != nullptr) - { - if (n != instance) - { - // This code is run both when we are doing expand definitions and - // simple beta reduction. - // - // f = (lambda ((x T)) t) [if we are expanding a definition] - // ---------------------- MACRO_SR_PRED_INTRO - // n = instance - Node conc = n.eqNode(instance); - tpg->addRewriteStep(n, - instance, - PfRule::MACRO_SR_PRED_INTRO, - pfExpChildren, - {conc}, - true); - } - } - // now, call expand definitions again on the result - TrustNode texp = expandDefinitions(instance, cache, expandOnly, tpg); - Node expanded = texp.isNull() ? instance : texp.getNode(); - cache[n] = n == expanded ? Node::null() : expanded; - result.push(expanded); - continue; - } - else if (!expandOnly) + if (!expandOnly) { // do not do any theory stuff if expandOnly is true @@ -331,35 +174,12 @@ TrustNode ExpandDefs::expandDefinitions( return TrustNode::mkTrustRewrite(orig, res, tpg); } -void ExpandDefs::expandAssertions(AssertionPipeline& assertions, - bool expandOnly) -{ - Chat() << "expanding definitions in assertions..." << std::endl; - Trace("exp-defs") << "ExpandDefs::simplify(): expanding definitions" - << std::endl; - TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime); - std::unordered_map cache; - for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) - { - Node assert = assertions[i]; - // notice we call this method with only one value of expandOnly currently, - // hence we maintain only a single set of proof steps in d_tpg. - TrustNode expd = expandDefinitions(assert, cache, expandOnly, d_tpg.get()); - if (!expd.isNull()) - { - Trace("exp-defs") << "ExpandDefs::expandAssertions: " << assert << " -> " - << expd.getNode() << std::endl; - assertions.replaceTrusted(i, expd); - } - } -} - void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm) { if (d_tpg == nullptr) { d_tpg.reset(new TConvProofGenerator(pnm, - d_smt.getUserContext(), + d_env.getUserContext(), TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, "ExpandDefs::TConvProofGenerator", diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index c0a92214a..d6fe8ba0d 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -25,8 +25,8 @@ namespace cvc5 { +class Env; class ProofNodeManager; -class ResourceManager; class SmtEngine; class TConvProofGenerator; @@ -47,7 +47,7 @@ struct SmtEngineStatistics; class ExpandDefs { public: - ExpandDefs(SmtEngine& smt, ResourceManager& rm, SmtEngineStatistics& stats); + ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats); ~ExpandDefs(); /** * Expand definitions in term n. Return the expanded form of n. @@ -62,12 +62,6 @@ class ExpandDefs TNode n, std::unordered_map& cache, bool expandOnly = false); - /** - * Expand defintitions in assertions. This applies this above method to each - * assertion in the given pipeline. - */ - void expandAssertions(preprocessing::AssertionPipeline& assertions, - bool expandOnly = false); /** * Set proof node manager, which signals this class to enable proofs using the @@ -87,8 +81,8 @@ class ExpandDefs TConvProofGenerator* tpg); /** Reference to the SMT engine */ SmtEngine& d_smt; - /** Reference to resource manager */ - ResourceManager& d_resourceManager; + /** Reference to the environment. */ + Env& d_env; /** Reference to the SMT stats */ SmtEngineStatistics& d_smtStats; /** A proof generator for the term conversion. */ diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 859eb84fc..f434e13ca 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -22,8 +22,10 @@ #include "smt/abstract_values.h" #include "smt/assertions.h" #include "smt/dump.h" +#include "smt/env.h" #include "smt/preprocess_proof_generator.h" #include "smt/smt_engine.h" +#include "theory/rewriter.h" using namespace std; using namespace cvc5::theory; @@ -33,16 +35,16 @@ namespace cvc5 { namespace smt { Preprocessor::Preprocessor(SmtEngine& smt, - context::UserContext* u, + Env& env, AbstractValues& abs, SmtEngineStatistics& stats) - : d_context(u), - d_smt(smt), + : d_smt(smt), + d_env(env), d_absValues(abs), d_propagator(true, true), - d_assertionsProcessed(u, false), - d_exDefs(smt, *smt.getResourceManager(), stats), - d_processor(smt, d_exDefs, *smt.getResourceManager(), stats), + d_assertionsProcessed(env.getUserContext(), false), + d_exDefs(smt, d_env, stats), + d_processor(smt, *smt.getResourceManager(), stats), d_pnm(nullptr) { } @@ -59,7 +61,7 @@ Preprocessor::~Preprocessor() void Preprocessor::finishInit() { d_ppContext.reset(new preprocessing::PreprocessingPassContext( - &d_smt, &d_propagator, d_pnm)); + &d_smt, d_env, &d_propagator)); // initialize the preprocessing passes d_processor.finishInit(d_ppContext.get()); @@ -111,7 +113,7 @@ void Preprocessor::cleanup() { d_processor.cleanup(); } Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly) { std::unordered_map cache; - return d_exDefs.expandDefinitions(n, cache, expandOnly); + return expandDefinitions(n, cache, expandOnly); } Node Preprocessor::expandDefinitions( @@ -127,8 +129,15 @@ Node Preprocessor::expandDefinitions( // Ensure node is type-checked at this point. n.getType(true); } - // expand only = true - return d_exDefs.expandDefinitions(n, cache, expandOnly); + // 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); + } + return n; } Node Preprocessor::simplify(const Node& node) @@ -139,17 +148,10 @@ Node Preprocessor::simplify(const Node& node) d_smt.getOutputManager().getPrinter().toStreamCmdSimplify( d_smt.getOutputManager().getDumpOut(), node); } - Node nas = d_absValues.substituteAbstractValues(node); - if (options::typeChecking()) - { - // ensure node is type-checked at this point - nas.getType(true); - } std::unordered_map cache; - Node n = d_exDefs.expandDefinitions(nas, cache); - TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n); - Node ns = ts.isNull() ? n : ts.getNode(); - return ns; + Node ret = expandDefinitions(node, cache, false); + ret = theory::Rewriter::rewrite(ret); + return ret; } void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) @@ -157,7 +159,7 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) Assert(pppg != nullptr); d_pnm = pppg->getManager(); d_exDefs.setProofNodeManager(d_pnm); - d_propagator.setProof(d_pnm, d_context, pppg); + d_propagator.setProof(d_pnm, d_env.getUserContext(), pppg); } } // namespace smt diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index c590b7164..e0ad2cc14 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -25,6 +25,7 @@ #include "theory/booleans/circuit_propagator.h" namespace cvc5 { +class Env; namespace preprocessing { class PreprocessingPassContext; } @@ -46,7 +47,7 @@ class Preprocessor { public: Preprocessor(SmtEngine& smt, - context::UserContext* u, + Env& env, AbstractValues& abs, SmtEngineStatistics& stats); ~Preprocessor(); @@ -94,17 +95,16 @@ class Preprocessor const Node& n, std::unordered_map& cache, bool expandOnly = false); - /** * Set proof node manager. Enables proofs in this preprocessor. */ void setProofGenerator(PreprocessProofGenerator* pppg); private: - /** A copy of the current context */ - context::Context* d_context; /** Reference to the parent SmtEngine */ SmtEngine& d_smt; + /** Reference to the env */ + Env& d_env; /** Reference to the abstract values utility */ AbstractValues& d_absValues; /** diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index fa230cd54..cf747c360 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -31,7 +31,6 @@ #include "preprocessing/preprocessing_pass_registry.h" #include "printer/printer.h" #include "smt/assertions.h" -#include "smt/defined_function.h" #include "smt/dump.h" #include "smt/expand_definitions.h" #include "smt/smt_engine.h" @@ -59,11 +58,9 @@ class ScopeCounter }; ProcessAssertions::ProcessAssertions(SmtEngine& smt, - ExpandDefs& exDefs, ResourceManager& rm, SmtEngineStatistics& stats) : d_smt(smt), - d_exDefs(exDefs), d_resourceManager(rm), d_smtStats(stats), d_preprocessingPassContext(nullptr) @@ -136,11 +133,11 @@ bool ProcessAssertions::apply(Assertions& as) << "ProcessAssertions::processAssertions() : pre-definition-expansion" << endl; dumpAssertions("pre-definition-expansion", assertions); - // Expand definitions, which replaces defined functions with their definition - // and does beta reduction. Notice we pass true as the second argument since - // we do not want to call theories to expand definitions here, since we want + // Apply substitutions first. If we are non-incremental, this has only the + // effect of replacing defined functions with their definitions. + // We do not call theory-specific expand definitions here, since we want // to give the opportunity to rewrite/preprocess terms before expansion. - d_exDefs.expandAssertions(assertions, true); + d_passes["apply-substs"]->apply(&assertions); Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-definition-expansion" << endl; diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index aeea68ef6..3cdf8a463 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -37,7 +37,6 @@ class PreprocessingPassContext; namespace smt { class Assertions; -class ExpandDefs; struct SmtEngineStatistics; /** @@ -62,7 +61,6 @@ class ProcessAssertions public: ProcessAssertions(SmtEngine& smt, - ExpandDefs& exDefs, ResourceManager& rm, SmtEngineStatistics& stats); ~ProcessAssertions(); @@ -85,8 +83,6 @@ class ProcessAssertions private: /** Reference to the SMT engine */ SmtEngine& d_smt; - /** Reference to expand definitions module */ - ExpandDefs& d_exDefs; /** Reference to resource manager */ ResourceManager& d_resourceManager; /** Reference to the SMT stats */ diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 422efac6a..53633a123 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -23,7 +23,6 @@ #include "options/smt_options.h" #include "proof/dot/dot_printer.h" #include "smt/assertions.h" -#include "smt/defined_function.h" #include "smt/preprocess_proof_generator.h" #include "smt/proof_post_processor.h" @@ -85,9 +84,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) PfManager::~PfManager() {} -void PfManager::setFinalProof(std::shared_ptr pfn, - Assertions& as, - DefinedFunctionMap& df) +void PfManager::setFinalProof(std::shared_ptr pfn, Assertions& as) { // Note this assumes that setFinalProof is only called once per unsat // response. This method would need to cache its result otherwise. @@ -102,7 +99,7 @@ void PfManager::setFinalProof(std::shared_ptr pfn, } std::vector assertions; - getAssertions(as, df, assertions); + getAssertions(as, assertions); if (Trace.isOn("smt-proof")) { @@ -140,11 +137,10 @@ void PfManager::setFinalProof(std::shared_ptr pfn, void PfManager::printProof(std::ostream& out, std::shared_ptr pfn, - Assertions& as, - DefinedFunctionMap& df) + Assertions& as) { Trace("smt-proof") << "PfManager::printProof: start" << std::endl; - std::shared_ptr fp = getFinalProof(pfn, as, df); + std::shared_ptr fp = getFinalProof(pfn, as); // if we are in incremental mode, we don't want to invalidate the proof // nodes in fp, since these may be reused in further check-sat calls if (options::incrementalSolving() @@ -166,12 +162,10 @@ void PfManager::printProof(std::ostream& out, out << "\n)\n"; } } -void PfManager::checkProof(std::shared_ptr pfn, - Assertions& as, - DefinedFunctionMap& df) +void PfManager::checkProof(std::shared_ptr pfn, Assertions& as) { Trace("smt-proof") << "PfManager::checkProof: start" << std::endl; - std::shared_ptr fp = getFinalProof(pfn, as, df); + std::shared_ptr fp = getFinalProof(pfn, as); Trace("smt-proof-debug") << "PfManager::checkProof: returned " << *fp.get() << std::endl; } @@ -186,15 +180,14 @@ smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const } std::shared_ptr PfManager::getFinalProof( - std::shared_ptr pfn, Assertions& as, DefinedFunctionMap& df) + std::shared_ptr pfn, Assertions& as) { - setFinalProof(pfn, as, df); + setFinalProof(pfn, as); Assert(d_finalProof); return d_finalProof; } void PfManager::getAssertions(Assertions& as, - DefinedFunctionMap& df, std::vector& assertions) { context::CDList* al = as.getAssertionList(); @@ -204,20 +197,6 @@ void PfManager::getAssertions(Assertions& as, { assertions.push_back(*i); } - NodeManager* nm = NodeManager::currentNM(); - for (const std::pair& dfn : df) - { - Node def = dfn.second.getFormula(); - const std::vector& formals = dfn.second.getFormals(); - if (!formals.empty()) - { - Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, formals); - def = nm->mkNode(kind::LAMBDA, bvl, def); - } - // assume the (possibly higher order) equality - Node eq = dfn.first.eqNode(def); - assertions.push_back(eq); - } } } // namespace smt diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 60e93306a..57478573c 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -31,7 +31,6 @@ class SmtEngine; namespace smt { class Assertions; -class DefinedFunction; class PreprocessProofGenerator; class ProofPostproccess; @@ -70,10 +69,6 @@ class ProofPostproccess; */ class PfManager { - /** The type of our internal map of defined functions */ - using DefinedFunctionMap = - context::CDHashMap; - public: PfManager(context::UserContext* u, SmtEngine* smte); ~PfManager(); @@ -83,20 +78,17 @@ class PfManager * The argument pfn is the proof for false in the current context. * * Throws an assertion failure if pg cannot provide a closed proof with - * respect to assertions in as and df. For the latter, entries in the defined - * function map correspond to equalities of the form (= f (lambda (...) t)), - * which are considered assertions in the final proof. + * respect to assertions in as. Note this includes equalities of the form + * (= f (lambda (...) t)) which originate from define-fun commands for f. + * These are considered assertions in the final proof. */ void printProof(std::ostream& out, std::shared_ptr pfn, - Assertions& as, - DefinedFunctionMap& df); + Assertions& as); /** * Check proof, same as above, without printing. */ - void checkProof(std::shared_ptr pfn, - Assertions& as, - DefinedFunctionMap& df); + void checkProof(std::shared_ptr pfn, Assertions& as); /** * Get final proof. @@ -104,8 +96,7 @@ class PfManager * The argument pfn is the proof for false in the current context. */ std::shared_ptr getFinalProof(std::shared_ptr pfn, - Assertions& as, - DefinedFunctionMap& df); + Assertions& as); //--------------------------- access to utilities /** Get a pointer to the ProofChecker owned by this. */ ProofChecker* getProofChecker() const; @@ -119,14 +110,11 @@ class PfManager * Set final proof, which initializes d_finalProof to the given proof node of * false, postprocesses it, and stores it in d_finalProof. */ - void setFinalProof(std::shared_ptr pfn, - Assertions& as, - DefinedFunctionMap& df); + void setFinalProof(std::shared_ptr pfn, Assertions& as); /** * Get assertions from the assertions */ void getAssertions(Assertions& as, - DefinedFunctionMap& df, std::vector& assertions); /** The false node */ Node d_false; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ef338fdfe..cee07a3dc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -40,7 +40,6 @@ #include "smt/abstract_values.h" #include "smt/assertions.h" #include "smt/check_models.h" -#include "smt/defined_function.h" #include "smt/dump.h" #include "smt/dump_manager.h" #include "smt/env.h" @@ -88,7 +87,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) : d_env(new Env(nm, optr)), d_state(new SmtEngineState(getContext(), getUserContext(), *this)), d_absValues(new AbstractValues(getNodeManager())), - d_asserts(new Assertions(getUserContext(), *d_absValues.get())), + d_asserts(new Assertions(*d_env.get(), *d_absValues.get())), d_routListener(new ResourceOutListener(*this)), d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)), d_smtSolver(nullptr), @@ -97,7 +96,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) d_checkModels(nullptr), d_pfManager(nullptr), d_ucManager(nullptr), - d_definedFunctions(nullptr), d_sygusSolver(nullptr), d_abductSolver(nullptr), d_interpolSolver(nullptr), @@ -131,8 +129,8 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // make statistics d_stats.reset(new SmtEngineStatistics()); // reset the preprocessor - d_pp.reset(new smt::Preprocessor( - *this, getUserContext(), *d_absValues.get(), *d_stats)); + d_pp.reset( + new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats)); // make the SMT solver d_smtSolver.reset( new SmtSolver(*this, *d_state, getResourceManager(), *d_pp, *d_stats)); @@ -151,8 +149,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // being parsed from the input file. Because of this, we cannot trust // that d_env->getOption(options::unsatCores) is set correctly yet. d_proofManager.reset(new ProofManager(getUserContext())); - - d_definedFunctions = new (true) DefinedFunctionMap(getUserContext()); } bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); } @@ -318,8 +314,6 @@ SmtEngine::~SmtEngine() // of context-dependent data structures d_state->cleanup(); - d_definedFunctions->deleteSelf(); - //destroy all passes before destroying things that they refer to d_pp->cleanup(); @@ -646,36 +640,26 @@ void SmtEngine::defineFunction(Node func, ss << language::SetLanguage( language::SetLanguage::getLanguage(Dump.getStream())) << func; - std::vector nFormals; - nFormals.reserve(formals.size()); - for (const Node& formal : formals) - { - nFormals.push_back(formal); - } - - DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula); + DefineFunctionNodeCommand nc(ss.str(), func, formals, formula); getDumpManager()->addToDump(nc, "declarations"); // type check body debugCheckFunctionBody(formula, formals, func); // Substitute out any abstract values in formula - Node formNode = d_absValues->substituteAbstractValues(formula); - DefinedFunction def(func, formals, formNode); - // Permit (check-sat) (define-fun ...) (get-value ...) sequences. - // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks - // d_haveAdditions = true; - Debug("smt") << "definedFunctions insert " << func << " " << formNode << endl; - - if (global) - { - d_definedFunctions->insertAtContextLevelZero(func, def); - } - else + Node def = d_absValues->substituteAbstractValues(formula); + if (!formals.empty()) { - d_definedFunctions->insert(func, def); + NodeManager* nm = NodeManager::currentNM(); + def = nm->mkNode( + kind::LAMBDA, nm->mkNode(kind::BOUND_VAR_LIST, formals), def); } + // A define-fun is treated as a (higher-order) assertion. It is provided + // to the assertions object. It will be added as a top-level substitution + // within this class, possibly multiple times if global is true. + Node feq = func.eqNode(def); + d_asserts->addDefineFunDefinition(feq, global); } void SmtEngine::defineFunctionsRec( @@ -748,7 +732,7 @@ void SmtEngine::defineFunctionsRec( // notice we don't call assertFormula directly, since this would // duplicate the output on raw-benchmark. // add define recursive definition to the assertions - d_asserts->addDefineFunRecDefinition(lem, global); + d_asserts->addDefineFunDefinition(lem, global); } } @@ -766,12 +750,6 @@ void SmtEngine::defineFunctionRec(Node func, defineFunctionsRec(funcs, formals_multi, formulas, global); } -bool SmtEngine::isDefinedFunction(Node func) -{ - Debug("smt") << "isDefined function " << func << "?" << std::endl; - return d_definedFunctions->find(func) != d_definedFunctions->end(); -} - Result SmtEngine::quickCheck() { Assert(d_state->isFullyInited()); Trace("smt") << "SMT quickCheck()" << endl; @@ -1295,6 +1273,7 @@ Result SmtEngine::blockModel() ModelBlocker::getModelBlocker(eassertsProc, m->getTheoryModel(), d_env->getOption(options::blockModelsMode)); + Trace("smt") << "Block formula: " << eblocker << std::endl; return assertFormula(eblocker); } @@ -1402,7 +1381,7 @@ void SmtEngine::checkProof() std::shared_ptr pePfn = pe->getProof(); if (d_env->getOption(options::checkProofs)) { - d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions); + d_pfManager->checkProof(pePfn, *d_asserts); } } @@ -1445,8 +1424,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() pepf = pe->getProof(); } Assert(pepf != nullptr); - std::shared_ptr pfn = - d_pfManager->getFinalProof(pepf, *d_asserts, *d_definedFunctions); + std::shared_ptr pfn = d_pfManager->getFinalProof(pepf, *d_asserts); std::vector core; d_ucManager->getUnsatCore(pfn, *d_asserts, core); return UnsatCore(core); @@ -1539,8 +1517,8 @@ void SmtEngine::getRelevantInstantiationTermVectors( PropEngine* pe = getPropEngine(); Assert(pe != nullptr); Assert(pe->getProof() != nullptr); - std::shared_ptr pfn = d_pfManager->getFinalProof( - pe->getProof(), *d_asserts, *d_definedFunctions); + std::shared_ptr pfn = + d_pfManager->getFinalProof(pe->getProof(), *d_asserts); d_ucManager->getRelevantInstantiations(pfn, insts); } @@ -1569,7 +1547,7 @@ std::string SmtEngine::getProof() Assert(pe->getProof() != nullptr); Assert(d_pfManager); std::ostringstream ss; - d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions); + d_pfManager->printProof(ss, pe->getProof(), *d_asserts); return ss.str(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 860caffa8..a7e39e004 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -94,13 +94,6 @@ class SygusSolver; class AbductionSolver; class InterpolationSolver; class QuantElimSolver; -/** - * Representation of a defined function. We keep these around in - * SmtEngine to permit expanding definitions late (and lazily), to - * support getValue() over defined functions, to support user output - * in terms of defined functions, etc. - */ -class DefinedFunction; struct SmtEngineStatistics; class SmtScope; @@ -335,9 +328,6 @@ class CVC5_EXPORT SmtEngine Node formula, bool global = false); - /** Return true if given expression is a defined function. */ - bool isDefinedFunction(Node func); - /** * Define functions recursive * @@ -891,13 +881,6 @@ class CVC5_EXPORT SmtEngine /** Get a pointer to the Rewriter owned by this SmtEngine. */ theory::Rewriter* getRewriter(); - - /** The type of our internal map of defined functions */ - using DefinedFunctionMap = - context::CDHashMap; - - /** Get the defined function map */ - DefinedFunctionMap* getDefinedFunctionMap() { return d_definedFunctions; } /** * Get expanded assertions. * @@ -1115,9 +1098,6 @@ class CVC5_EXPORT SmtEngine * from refutations. */ std::unique_ptr d_ucManager; - /** An index of our defined functions */ - DefinedFunctionMap* d_definedFunctions; - /** The solver for sygus queries */ std::unique_ptr d_sygusSolver; diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 0976442e1..317bb2646 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -31,6 +31,7 @@ #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" using namespace cvc5::theory; @@ -384,7 +385,12 @@ void SygusSolver::checkSynthSolution(Assertions& as) // definitions that were added as assertions to the sygus problem. for (Node a : auxAssertions) { - solChecker->assertFormula(a); + // We require rewriting here, e.g. so that define-fun from the original + // problem are rewritten to true. If this is not the case, then the + // assertions module of the subsolver will complain about assertions + // with free variables. + Node ar = theory::Rewriter::rewrite(a); + solChecker->assertFormula(ar); } Result r = solChecker->checkSat(); Notice() << "SygusSolver::checkSynthSolution(): result is " << r diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index 4088deb94..47507bfe0 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -27,21 +27,32 @@ TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, MethodId ids) : d_ctx(c), d_subs(c), - d_pnm(pnm), d_tsubs(c), - d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr), - d_subsPg( - pnm ? new LazyCDProof(pnm, nullptr, c, "TrustSubstitutionMap::subsPg") - : nullptr), - d_applyPg(pnm ? new LazyCDProof( - pnm, nullptr, c, "TrustSubstitutionMap::applyPg") - : nullptr), - d_helperPf(pnm, c), + d_tspb(nullptr), + d_subsPg(nullptr), + d_applyPg(nullptr), + d_helperPf(nullptr), d_name(name), d_trustId(trustId), d_ids(ids), d_eqtIndex(c) { + setProofNodeManager(pnm); +} + +void TrustSubstitutionMap::setProofNodeManager(ProofNodeManager* pnm) +{ + if (pnm != nullptr) + { + // should not set the proof node manager more than once + Assert(d_tspb == nullptr); + d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())), + d_subsPg.reset(new LazyCDProof( + pnm, nullptr, d_ctx, "TrustSubstitutionMap::subsPg")); + d_applyPg.reset( + new LazyCDProof(pnm, nullptr, d_ctx, "TrustSubstitutionMap::applyPg")); + d_helperPf.reset(new CDProofSet(pnm, d_ctx)); + } } void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg) @@ -69,7 +80,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x, addSubstitution(x, t, nullptr); return; } - LazyCDProof* stepPg = d_helperPf.allocateProof(nullptr, d_ctx); + LazyCDProof* stepPg = d_helperPf->allocateProof(nullptr, d_ctx); Node eq = x.eqNode(t); stepPg->addStep(eq, id, children, args); addSubstitution(x, t, stepPg); @@ -100,7 +111,7 @@ ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x, Trace("trust-subs") << "...use generator directly" << std::endl; return tn.getGenerator(); } - LazyCDProof* solvePg = d_helperPf.allocateProof(nullptr, d_ctx); + LazyCDProof* solvePg = d_helperPf->allocateProof(nullptr, d_ctx); // Try to transform tn.getProven() to (= x t) here, if necessary if (!d_tspb->applyPredTransform(proven, eq, {})) { diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index e8b627249..ec5b2ffb5 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -42,10 +42,12 @@ class TrustSubstitutionMap : public ProofGenerator public: TrustSubstitutionMap(context::Context* c, - ProofNodeManager* pnm, + ProofNodeManager* pnm = nullptr, std::string name = "TrustSubstitutionMap", PfRule trustId = PfRule::PREPROCESS_LEMMA, MethodId ids = MethodId::SB_DEFAULT); + /** Set proof node manager */ + void setProofNodeManager(ProofNodeManager* pnm); /** Gets a reference to the underlying substitution map */ SubstitutionMap& get(); /** @@ -105,8 +107,6 @@ class TrustSubstitutionMap : public ProofGenerator context::Context* d_ctx; /** The substitution map */ SubstitutionMap d_subs; - /** The proof node manager */ - ProofNodeManager* d_pnm; /** A context-dependent list of trust nodes */ context::CDList d_tsubs; /** Theory proof step buffer */ @@ -118,7 +118,7 @@ class TrustSubstitutionMap : public ProofGenerator /** * A context-dependent list of LazyCDProof, allocated for internal steps. */ - CDProofSet d_helperPf; + std::unique_ptr> d_helperPf; /** Name for debugging */ std::string d_name; /** diff --git a/test/regress/regress1/bug516.smt2 b/test/regress/regress1/bug516.smt2 index a01eb97e9..43d18575e 100644 --- a/test/regress/regress1/bug516.smt2 +++ b/test/regress/regress1/bug516.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --fmf-bound-int +; COMMAND-LINE: --finite-model-find --fmf-bound-int -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/model-blocker-values.smt2 b/test/regress/regress1/model-blocker-values.smt2 index 65db79ca4..1c9e80642 100644 --- a/test/regress/regress1/model-blocker-values.smt2 +++ b/test/regress/regress1/model-blocker-values.smt2 @@ -1,7 +1,8 @@ ; COMMAND-LINE: --incremental --produce-models --block-models=values ; EXPECT: sat ; EXPECT: sat -; EXPECT: sat +; if we only block models restricted to (a,b), then there are only 2 models +; EXPECT: unsat (set-logic QF_UFLIA) (declare-fun a () Int) (declare-fun b () Int) diff --git a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 index fdbac9996..585ea0602 100644 --- a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 +++ b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv +; COMMAND-LINE: --cegqi-bv -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/issue3664.smt2 b/test/regress/regress1/quantifiers/issue3664.smt2 index 28e999604..e1a923f98 100644 --- a/test/regress/regress1/quantifiers/issue3664.smt2 +++ b/test/regress/regress1/quantifiers/issue3664.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun-rlv --sygus-inference +; COMMAND-LINE: --fmf-fun-rlv --sygus-inference --no-check-models ; EXPECT: sat (set-logic QF_NRA) (declare-fun a () Real)