From d8d3c55afc94482fc05f68ba6be47f767ab3b5c6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 5 Aug 2020 14:14:23 -0500 Subject: [PATCH] Split Assertions from SmtEngine (#4788) This splits all things related to storing assertions in the SmtEngine into a separate class "Assertions". It also converts the interface for its methods from Expr to Node. --- src/CMakeLists.txt | 2 + src/api/cvc4cpp.cpp | 6 +- src/smt/assertions.cpp | 234 +++++++++++++++++++++++ src/smt/assertions.h | 170 +++++++++++++++++ src/smt/command.cpp | 7 +- src/smt/process_assertions.cpp | 5 +- src/smt/process_assertions.h | 7 +- src/smt/smt_engine.cpp | 328 +++++++++------------------------ src/smt/smt_engine.h | 50 +---- 9 files changed, 513 insertions(+), 296 deletions(-) create mode 100644 src/smt/assertions.cpp create mode 100644 src/smt/assertions.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index cd6f48178..92f197252 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -223,6 +223,8 @@ libcvc4_add_sources( smt/abduction_solver.h smt/abstract_values.cpp smt/abstract_values.h + smt/assertions.cpp + smt/assertions.h smt/command.cpp smt/command.h smt/defined_function.h diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index eef2b7052..0963c704b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4906,14 +4906,14 @@ std::vector Solver::getUnsatAssumptions(void) const == SmtEngine::SmtMode::SMT_MODE_UNSAT) << "Cannot get unsat assumptions unless in unsat mode."; - std::vector uassumptions = d_smtEngine->getUnsatAssumptions(); + std::vector uassumptions = d_smtEngine->getUnsatAssumptions(); /* Can not use * return std::vector(uassumptions.begin(), uassumptions.end()); * here since constructor is private */ std::vector res; - for (const Expr& e : uassumptions) + for (const Node& e : uassumptions) { - res.push_back(Term(this, e)); + res.push_back(Term(this, e.toExpr())); } return res; CVC4_API_SOLVER_TRY_CATCH_END; diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp new file mode 100644 index 000000000..ea3acf2d1 --- /dev/null +++ b/src/smt/assertions.cpp @@ -0,0 +1,234 @@ +/********************* */ +/*! \file assertions.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief The module for storing assertions for an SMT engine. + **/ + +#include "smt/assertions.h" + +#include "expr/node_algorithm.h" +#include "options/base_options.h" +#include "options/language.h" +#include "options/proof_options.h" +#include "options/smt_options.h" +#include "proof/proof_manager.h" +#include "smt/smt_engine.h" + +using namespace CVC4::theory; +using namespace CVC4::kind; + +namespace CVC4 { +namespace smt { + +Assertions::Assertions(context::UserContext* u, AbstractValues& absv) + : d_userContext(u), + d_absValues(absv), + d_assertionList(nullptr), + d_globalNegation(false), + d_assertions() +{ +} + +Assertions::~Assertions() +{ + if (d_assertionList != nullptr) + { + d_assertionList->deleteSelf(); + } +} + +void Assertions::finishInit() +{ + // [MGD 10/20/2011] keep around in incremental mode, due to a + // cleanup ordering issue and Nodes/TNodes. If SAT is popped + // first, some user-context-dependent TNodes might still exist + // with rc == 0. + if (options::produceAssertions() || options::incrementalSolving()) + { + // 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()); + } +} + +void Assertions::clearCurrent() +{ + d_assertions.clear(); + d_assertions.getIteSkolemMap().clear(); +} + +void Assertions::initializeCheckSat(const std::vector& assumptions, + bool inUnsatCore, + bool isEntailmentCheck) +{ + NodeManager* nm = NodeManager::currentNM(); + // reset global negation + d_globalNegation = false; + // clear the assumptions + d_assumptions.clear(); + if (isEntailmentCheck) + { + size_t size = assumptions.size(); + if (size > 1) + { + /* Assume: not (BIGAND assumptions) */ + d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode()); + } + else if (size == 1) + { + /* Assume: not expr */ + d_assumptions.push_back(assumptions[0].notNode()); + } + } + else + { + /* Assume: BIGAND assumptions */ + d_assumptions = assumptions; + } + + Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + for (const Node& e : d_assumptions) + { + // Substitute out any abstract values in ex. + Node n = d_absValues.substituteAbstractValues(e); + // Ensure expr is type-checked at this point. + ensureBoolean(n); + + /* Add assumption */ + if (d_assertionList != nullptr) + { + d_assertionList->push_back(n); + } + addFormula(n, inUnsatCore, true, true, false); + } + if (d_globalDefineFunRecLemmas != 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) + { + addFormula(lemma, false, true, false, false); + } + } +} + +void Assertions::assertFormula(const Node& n, bool inUnsatCore) +{ + ensureBoolean(n); + if (d_assertionList != nullptr) + { + d_assertionList->push_back(n); + } + bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); + addFormula(n, inUnsatCore, true, false, maybeHasFv); +} + +std::vector& Assertions::getAssumptions() { return d_assumptions; } +bool Assertions::isGlobalNegated() const { return d_globalNegation; } +void Assertions::flipGlobalNegated() { d_globalNegation = !d_globalNegation; } + +preprocessing::AssertionPipeline& Assertions::getAssertionPipeline() +{ + return d_assertions; +} + +context::CDList* Assertions::getAssertionList() +{ + return d_assertionList; +} + +void Assertions::addFormula( + TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv) +{ + if (n.isConst() && n.getConst()) + { + // true, nothing to do + return; + } + + Trace("smt") << "SmtEnginePrivate::addFormula(" << n + << "), inUnsatCore = " << inUnsatCore + << ", inInput = " << inInput + << ", isAssumption = " << isAssumption << std::endl; + + // Ensure that it does not contain free variables + if (maybeHasFv) + { + if (expr::hasFreeVar(n)) + { + std::stringstream se; + se << "Cannot process assertion with free variable."; + if (language::isInputLangSygus(options::inputLanguage())) + { + // Common misuse of SyGuS is to use top-level assert instead of + // constraint when defining the synthesis conjecture. + se << " Perhaps you meant `constraint` instead of `assert`?"; + } + throw ModalException(se.str().c_str()); + } + } + + // Give it to proof manager + PROOF(if (inInput) { + // n is an input assertion + if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() + || options::checkUnsatCores() || options::fewerPreprocessingHoles()) + { + ProofManager::currentPM()->addCoreAssertion(n.toExpr()); + } + } else { + // n is the result of an unknown preprocessing step, add it to dependency + // map to null + ProofManager::currentPM()->addDependence(n, Node::null()); + }); + + // Add the normalized formula to the queue + d_assertions.push_back(n, isAssumption); +} + +void Assertions::addDefineFunRecDefinition(Node n, bool global) +{ + n = d_absValues.substituteAbstractValues(n); + if (d_assertionList != nullptr) + { + d_assertionList->push_back(n); + } + if (global && d_globalDefineFunRecLemmas != 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); + } + else + { + bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); + addFormula(n, false, true, false, maybeHasFv); + } +} + +void Assertions::ensureBoolean(const Node& n) +{ + TypeNode type = n.getType(options::typeChecking()); + if (!type.isBoolean()) + { + std::stringstream ss; + ss << "Expected Boolean type\n" + << "The assertion : " << n << "\n" + << "Its type : " << type; + throw TypeCheckingException(n.toExpr(), ss.str()); + } +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/assertions.h b/src/smt/assertions.h new file mode 100644 index 000000000..c2a16db71 --- /dev/null +++ b/src/smt/assertions.h @@ -0,0 +1,170 @@ +/********************* */ +/*! \file assertions.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief The module for storing assertions for an SMT engine. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__ASSERTIONS_H +#define CVC4__SMT__ASSERTIONS_H + +#include + +#include "context/cdlist.h" +#include "context/context.h" +#include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" +#include "smt/abstract_values.h" + +namespace CVC4 { +namespace smt { + +/** + * Contains all information pertaining to the assertions of an SMT engine. + * + * This class is responsible for setting up the assertions pipeline for + * check-sat calls. It is *not* responsible for the preprocessing itself, and + * instead is intended to be the input to a preprocessor utility. + */ +class Assertions +{ + /** The type of our internal assertion list */ + typedef context::CDList AssertionList; + + public: + Assertions(context::UserContext* u, AbstractValues& absv); + ~Assertions(); + /** + * Finish initialization, called once after options are finalized. Sets up + * the required bookkeeping based on the options. + */ + void finishInit(); + /** + * Clears out the non-context-dependent data in this class. Necessary to + * clear out our assertion vectors in case someone does a push-assert-pop + * without a check-sat. + */ + void clearCurrent(); + /* + * Initialize a call to check satisfiability. This adds assumptions to + * the list of assumptions maintained by this class, and finalizes the + * set of formulas (in the assertions pipeline) that will be used for the + * upcoming check-sat call. + * + * @param assumptions The assumptions of the upcoming check-sat call. + * @param inUnsatCore Whether assumptions are in the unsat core. + * @param isEntailmentCheck Whether we are checking entailment of assumptions + * in the upcoming check-sat call. + */ + void initializeCheckSat(const std::vector& assumptions, + bool inUnsatCore, + bool isEntailmentCheck); + /** + * Add a formula to the current context: preprocess, do per-theory + * setup, use processAssertionList(), asserting to T-solver for + * literals and conjunction of literals. Returns false if + * immediately determined to be inconsistent. This version + * takes a Boolean flag to determine whether to include this asserted + * formula in an unsat core (if one is later requested). + * + * @throw TypeCheckingException, LogicException, UnsafeInterruptException + */ + void assertFormula(const Node& n, bool inUnsatCore = true); + /** + * Assert that n corresponds to an assertion from a 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); + /** + * Get the assertions pipeline, which contains the set of assertions we are + * currently processing. + */ + preprocessing::AssertionPipeline& getAssertionPipeline(); + /** + * Get assertions list corresponding to the original list of assertions, + * before preprocessing. + */ + context::CDList* getAssertionList(); + /** + * Get the list of assumptions, which are those registered to this class + * on initializeCheckSat. + */ + std::vector& getAssumptions(); + /** + * Is the set of assertions globally negated? When this flag is true, the + * overall result of check-sat should be inverted. + */ + bool isGlobalNegated() const; + /** Flip the global negation flag. */ + void flipGlobalNegated(); + + private: + /** + * Fully type-check the argument, and also type-check that it's + * actually Boolean. + * throw@ TypeCheckingException + */ + void ensureBoolean(const Node& n); + /** + * Adds a formula to the current context. Action here depends on + * the SimplificationMode (in the current Options scope); the + * formula might be pushed out to the propositional layer + * immediately, or it might be simplified and kept, or it might not + * even be simplified. + * The arguments isInput and isAssumption are used for bookkeeping for proofs. + * The argument maybeHasFv should be set to true if the assertion may have + * free variables. By construction, assertions from the smt2 parser are + * guaranteed not to have free variables. However, other cases such as + * assertions from the SyGuS parser may have free variables (say if the + * input contains an assert or define-fun-rec command). + * + * @param isAssumption If true, the formula is considered to be an assumption + * (this is used to distinguish assertions and assumptions) + */ + void addFormula(TNode n, + bool inUnsatCore, + bool inInput, + bool isAssumption, + bool maybeHasFv); + /** pointer to the user context */ + context::UserContext* d_userContext; + /** Reference to the abstract values utility */ + AbstractValues& d_absValues; + /** + * The assertion list (before any conversion) for supporting + * getAssertions(). Only maintained if in incremental mode. + */ + AssertionList* d_assertionList; + /** + * 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; + /** + * The list of assumptions from the previous call to checkSatisfiability. + * Note that if the last call to checkSatisfiability was an entailment check, + * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains + * one single assumption ~(a1 AND ... AND an). + */ + std::vector d_assumptions; + /** Whether we did a global negation of the formula. */ + bool d_globalNegation; + /** Assertions in the preprocessing pipeline */ + preprocessing::AssertionPipeline d_assertions; +}; + +} // namespace smt +} // namespace CVC4 + +#endif diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 97a51277b..52a9578dd 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2359,7 +2359,12 @@ void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine) { try { - d_result = smtEngine->getUnsatAssumptions(); + std::vector uassumps = smtEngine->getUnsatAssumptions(); + d_result.clear(); + for (const Node& n : uassumps) + { + d_result.push_back(n.toExpr()); + } d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 4fed33f3c..d2bf3ba46 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -91,8 +91,9 @@ void ProcessAssertions::spendResource(ResourceManager::Resource r) d_resourceManager.spendResource(r); } -bool ProcessAssertions::apply(AssertionPipeline& assertions) +bool ProcessAssertions::apply(Assertions& as) { + AssertionPipeline& assertions = as.getAssertionPipeline(); Assert(d_preprocessingPassContext != nullptr); // Dump the assertions dumpAssertions("pre-everything", assertions); @@ -158,7 +159,7 @@ bool ProcessAssertions::apply(AssertionPipeline& assertions) { // global negation of the formula d_passes["global-negate"]->apply(&assertions); - d_smt.d_globalNegation = !d_smt.d_globalNegation; + as.flipGlobalNegated(); } if (options::nlExtPurify()) diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index 4850d5589..2a7efe1c0 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -25,6 +25,7 @@ #include "expr/type_node.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" +#include "smt/assertions.h" #include "smt/smt_engine_stats.h" #include "util/resource_manager.h" @@ -69,10 +70,10 @@ class ProcessAssertions */ void cleanup(); /** - * Process the formulas in assertions. Returns true if there - * was no conflict when processing the assertions. + * Process the formulas in as. Returns true if there was no conflict when + * processing the assertions. */ - bool apply(preprocessing::AssertionPipeline& assertions); + bool apply(Assertions& as); /** * Expand definitions in term n. Return the expanded form of n. * diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e5b95d656..43aa3b0c8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -82,6 +82,7 @@ #include "prop/prop_engine.h" #include "smt/abduction_solver.h" #include "smt/abstract_values.h" +#include "smt/assertions.h" #include "smt/expr_names.h" #include "smt/command.h" #include "smt/defined_function.h" @@ -162,9 +163,6 @@ class SmtEnginePrivate /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; - /** Assertions in the preprocessing pipeline */ - AssertionPipeline d_assertions; - /** Whether any assertions have been processed */ CDO d_assertionsProcessed; @@ -178,7 +176,6 @@ class SmtEnginePrivate ProcessAssertions d_processor; public: - IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); } /** Instance of the ITE remover */ RemoveTermFormulas d_iteRemover; @@ -208,7 +205,6 @@ class SmtEnginePrivate SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), d_propagator(true, true), - d_assertions(), d_assertionsProcessed(smt.getUserContext(), false), d_processor(smt, *smt.getResourceManager()), d_iteRemover(smt.getUserContext()), @@ -241,12 +237,11 @@ class SmtEnginePrivate /** * Process the assertions that have been asserted. */ - void processAssertions(); + void processAssertions(Assertions& as); /** Process a user push. */ void notifyPush() { - } /** @@ -256,32 +251,8 @@ class SmtEnginePrivate * last map of expression names from notifyPush. */ void notifyPop() { - d_assertions.clear(); d_propagator.getLearnedLiterals().clear(); - getIteSkolemMap().clear(); } - - /** - * Adds a formula to the current context. Action here depends on - * the SimplificationMode (in the current Options scope); the - * formula might be pushed out to the propositional layer - * immediately, or it might be simplified and kept, or it might not - * even be simplified. - * The arguments isInput and isAssumption are used for bookkeeping for proofs. - * The argument maybeHasFv should be set to true if the assertion may have - * free variables. By construction, assertions from the smt2 parser are - * guaranteed not to have free variables. However, other cases such as - * assertions from the SyGuS parser may have free variables (say if the - * input contains an assert or define-fun-rec command). - * - * @param isAssumption If true, the formula is considered to be an assumption - * (this is used to distinguish assertions and assumptions) - */ - void addFormula(TNode n, - bool inUnsatCore, - bool inInput = true, - bool isAssumption = false, - bool maybeHasFv = false); /** * Simplify node "in" by expanding definitions and applying any * substitutions learned from preprocessing. @@ -291,8 +262,6 @@ class SmtEnginePrivate // Expand definitions. NodeToNodeHashMap cache; Node n = d_processor.expandDefinitions(in, cache).toExpr(); - // Make sure we've done all preprocessing, etc. - Assert(d_assertions.size() == 0); return applySubstitutions(n).toExpr(); } };/* class SmtEnginePrivate */ @@ -306,6 +275,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), d_absValues(new AbstractValues(d_nodeManager)), + d_asserts(new Assertions(d_userContext.get(), *d_absValues.get())), d_exprNames(new ExprNames(d_userContext.get())), d_dumpm(new DumpManager(d_userContext.get())), d_routListener(new ResourceOutListener(*this)), @@ -316,7 +286,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_rewriter(new theory::Rewriter()), d_definedFunctions(nullptr), d_abductSolver(nullptr), - d_assertionList(nullptr), d_assignments(nullptr), d_defineCommands(), d_logic(), @@ -326,7 +295,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_fullyInited(false), d_queryMade(false), d_needPostsolve(false), - d_globalNegation(false), d_status(), d_expectedStatus(), d_smtMode(SMT_MODE_START), @@ -434,18 +402,8 @@ void SmtEngine::finishInit() d_userContext->push(); d_context->push(); - Trace("smt-debug") << "Set up assertion list..." << std::endl; - // [MGD 10/20/2011] keep around in incremental mode, due to a - // cleanup ordering issue and Nodes/TNodes. If SAT is popped - // first, some user-context-dependent TNodes might still exist - // with rc == 0. - if(options::produceAssertions() || - options::incrementalSolving()) { - // In the case of incremental solving, we appear to need these to - // ensure the relevant Nodes remain live. - d_assertionList = new (true) AssertionList(getUserContext()); - d_globalDefineFunRecLemmas.reset(new std::vector()); - } + Trace("smt-debug") << "Set up assertions..." << std::endl; + d_asserts->finishInit(); // dump out a set-logic command only when raw-benchmark is disabled to avoid // dumping the command twice. @@ -534,12 +492,6 @@ SmtEngine::~SmtEngine() d_assignments->deleteSelf(); } - d_globalDefineFunRecLemmas.reset(); - - if(d_assertionList != NULL) { - d_assertionList->deleteSelf(); - } - d_definedFunctions->deleteSelf(); //destroy all passes before destroying things that they refer to @@ -557,6 +509,7 @@ SmtEngine::~SmtEngine() #endif d_absValues.reset(nullptr); + d_asserts.reset(nullptr); d_exprNames.reset(nullptr); d_dumpm.reset(nullptr); @@ -647,12 +600,6 @@ void SmtEngine::setLogicInternal() d_userLogic.lock(); } -void SmtEngine::setProblemExtended() -{ - d_smtMode = SMT_MODE_ASSERT; - d_assumptions.clear(); -} - void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) { SmtScope smts(this); @@ -983,7 +930,6 @@ void SmtEngine::defineFunctionsRec( } ExprManager* em = getExprManager(); - bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); for (unsigned i = 0, size = funcs.size(); i < size; i++) { // we assert a quantified formula @@ -1018,22 +964,9 @@ void SmtEngine::defineFunctionsRec( // assert the quantified formula // notice we don't call assertFormula directly, since this would // duplicate the output on raw-benchmark. - Node n = d_absValues->substituteAbstractValues(Node::fromExpr(lem)); - if (d_assertionList != nullptr) - { - d_assertionList->push_back(n); - } - if (global && d_globalDefineFunRecLemmas != 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); - } - else - { - d_private->addFormula(n, false, true, false, maybeHasFv); - } + Node lemn = Node::fromExpr(lem); + // add define recursive definition to the assertions + d_asserts->addDefineFunRecDefinition(lemn, global); } } @@ -1084,7 +1017,7 @@ Result SmtEngine::check() { // Make sure the prop layer has all of the assertions Trace("smt") << "SmtEngine::check(): processing assertions" << endl; - d_private->processAssertions(); + d_private->processAssertions(*d_asserts); Trace("smt") << "SmtEngine::check(): done processing assertions" << endl; TimerStat::CodeTimer solveTimer(d_stats->d_solveTime); @@ -1147,13 +1080,17 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const return m; } -void SmtEnginePrivate::processAssertions() { +void SmtEnginePrivate::processAssertions(Assertions& as) +{ TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); spendResource(ResourceManager::Resource::PreprocessStep); Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); - if (d_assertions.size() == 0) { + AssertionPipeline& ap = as.getAssertionPipeline(); + + if (ap.size() == 0) + { // nothing to do return; } @@ -1161,24 +1098,24 @@ void SmtEnginePrivate::processAssertions() { // TODO(b/1255): Substitutions in incremental mode should be managed with a // proper data structure. - d_assertions.enableStoreSubstsInAsserts(); + ap.enableStoreSubstsInAsserts(); } else { - d_assertions.disableStoreSubstsInAsserts(); + ap.disableStoreSubstsInAsserts(); } // process the assertions - bool noConflict = d_processor.apply(d_assertions); + bool noConflict = d_processor.apply(as); //notify theory engine new preprocessed assertions - d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() ); + d_smt.d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); // Push the formula to decision engine if (noConflict) { Chat() << "pushing to decision engine..." << endl; - d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions); + d_smt.d_propEngine->addAssertionsToDecisionEngine(ap); } // end: INVARIANT to maintain: no reordering of assertions or @@ -1187,91 +1124,30 @@ void SmtEnginePrivate::processAssertions() { // if incremental, compute which variables are assigned if (options::incrementalSolving()) { - d_preprocessingPassContext->recordSymbolsInAssertions(d_assertions.ref()); + d_preprocessingPassContext->recordSymbolsInAssertions(ap.ref()); } // Push the formula to SAT { Chat() << "converting to CNF..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Chat() << "+ " << d_assertions[i] << std::endl; - d_smt.d_propEngine->assertFormula(d_assertions[i]); - } - } - - d_assertionsProcessed = true; - - d_assertions.clear(); - getIteSkolemMap().clear(); -} - -void SmtEnginePrivate::addFormula( - TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv) -{ - if (n == d_true) { - // nothing to do - return; - } - - Trace("smt") << "SmtEnginePrivate::addFormula(" << n - << "), inUnsatCore = " << inUnsatCore - << ", inInput = " << inInput - << ", isAssumption = " << isAssumption << endl; - - // Ensure that it does not contain free variables - if (maybeHasFv) - { - if (expr::hasFreeVar(n)) + for (const Node& assertion : ap.ref()) { - std::stringstream se; - se << "Cannot process assertion with free variable."; - if (language::isInputLangSygus(options::inputLanguage())) - { - // Common misuse of SyGuS is to use top-level assert instead of - // constraint when defining the synthesis conjecture. - se << " Perhaps you meant `constraint` instead of `assert`?"; - } - throw ModalException(se.str().c_str()); + Chat() << "+ " << assertion << std::endl; + d_smt.d_propEngine->assertFormula(assertion); } } - // Give it to proof manager - PROOF( - if( inInput ){ - // n is an input assertion - if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) { - - ProofManager::currentPM()->addCoreAssertion(n.toExpr()); - } - }else{ - // n is the result of an unknown preprocessing step, add it to dependency map to null - ProofManager::currentPM()->addDependence(n, Node::null()); - } - ); - - // Add the normalized formula to the queue - d_assertions.push_back(n, isAssumption); - //d_assertions.push_back(Rewriter::rewrite(n)); -} + d_assertionsProcessed = true; -void SmtEngine::ensureBoolean(const Node& n) -{ - TypeNode type = n.getType(options::typeChecking()); - TypeNode boolType = NodeManager::currentNM()->booleanType(); - if(type != boolType) { - stringstream ss; - ss << "Expected " << boolType << "\n" - << "The assertion : " << n << "\n" - << "Its type : " << type; - throw TypeCheckingException(n.toExpr(), ss.str()); - } + // clear the current assertions + as.clearCurrent(); } Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) { Dump("benchmark") << CheckSatCommand(assumption); - return checkSatisfiability(assumption, inUnsatCore, false); + return checkSatisfiability(Node::fromExpr(assumption), inUnsatCore, false); } Result SmtEngine::checkSat(const vector& assumptions, bool inUnsatCore) @@ -1284,36 +1160,46 @@ Result SmtEngine::checkSat(const vector& assumptions, bool inUnsatCore) { Dump("benchmark") << CheckSatAssumingCommand(assumptions); } - - return checkSatisfiability(assumptions, inUnsatCore, false); + std::vector assumps; + for (const Expr& e : assumptions) + { + assumps.push_back(Node::fromExpr(e)); + } + return checkSatisfiability(assumps, inUnsatCore, false); } -Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore) +Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore) { - Dump("benchmark") << QueryCommand(expr, inUnsatCore); - return checkSatisfiability( - expr.isNull() ? std::vector() : std::vector{expr}, - inUnsatCore, - true) + Dump("benchmark") << QueryCommand(node, inUnsatCore); + return checkSatisfiability(node.isNull() + ? std::vector() + : std::vector{Node::fromExpr(node)}, + inUnsatCore, + true) .asEntailmentResult(); } -Result SmtEngine::checkEntailed(const vector& exprs, bool inUnsatCore) +Result SmtEngine::checkEntailed(const vector& nodes, bool inUnsatCore) { - return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult(); + std::vector ns; + for (const Expr& e : nodes) + { + ns.push_back(Node::fromExpr(e)); + } + return checkSatisfiability(ns, inUnsatCore, true).asEntailmentResult(); } -Result SmtEngine::checkSatisfiability(const Expr& expr, +Result SmtEngine::checkSatisfiability(const Node& node, bool inUnsatCore, bool isEntailmentCheck) { return checkSatisfiability( - expr.isNull() ? std::vector() : std::vector{expr}, + node.isNull() ? std::vector() : std::vector{node}, inUnsatCore, isEntailmentCheck); } -Result SmtEngine::checkSatisfiability(const vector& assumptions, +Result SmtEngine::checkSatisfiability(const vector& assumptions, bool inUnsatCore, bool isEntailmentCheck) { @@ -1333,70 +1219,23 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, "(try --incremental)"); } - // Note that a query has been made + // Note that a query has been made and we are in assert mode d_queryMade = true; - // reset global negation - d_globalNegation = false; + d_smtMode = SMT_MODE_ASSERT; + // push if there are assumptions bool didInternalPush = false; - - setProblemExtended(); - - if (isEntailmentCheck) - { - size_t size = assumptions.size(); - if (size > 1) - { - /* Assume: not (BIGAND assumptions) */ - d_assumptions.push_back( - d_exprManager->mkExpr(kind::AND, assumptions).notExpr()); - } - else if (size == 1) - { - /* Assume: not expr */ - d_assumptions.push_back(assumptions[0].notExpr()); - } - } - else - { - /* Assume: BIGAND assumptions */ - d_assumptions = assumptions; - } - - if (!d_assumptions.empty()) + if (!assumptions.empty()) { internalPush(); didInternalPush = true; } - Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - for (Expr e : d_assumptions) - { - // Substitute out any abstract values in ex. - Node n = d_absValues->substituteAbstractValues(Node::fromExpr(e)); - // Ensure expr is type-checked at this point. - ensureBoolean(n); + // then, initialize the assertions + d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck); - /* Add assumption */ - if (d_assertionList != NULL) - { - d_assertionList->push_back(n); - } - d_private->addFormula(n, inUnsatCore, true, true); - } - - if (d_globalDefineFunRecLemmas != 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) - { - d_private->addFormula(lemma, false, true, false, false); - } - } - - r = check(); + // make the check + Result r = check(); if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) @@ -1404,7 +1243,7 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); } // flipped if we did a global negation - if (d_globalNegation) + if (d_asserts->isGlobalNegated()) { Trace("smt") << "SmtEngine::process global negate " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) @@ -1492,7 +1331,7 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, } } -vector SmtEngine::getUnsatAssumptions(void) +std::vector SmtEngine::getUnsatAssumptions(void) { Trace("smt") << "SMT getUnsatAssumptions()" << endl; SmtScope smts(this); @@ -1514,10 +1353,14 @@ vector SmtEngine::getUnsatAssumptions(void) Dump("benchmark") << GetUnsatAssumptionsCommand(); } UnsatCore core = getUnsatCoreInternal(); - vector res; - for (const Expr& e : d_assumptions) + std::vector res; + std::vector& assumps = d_asserts->getAssumptions(); + for (const Node& e : assumps) { - if (find(core.begin(), core.end(), e) != core.end()) { res.push_back(e); } + if (std::find(core.begin(), core.end(), e.toExpr()) != core.end()) + { + res.push_back(e); + } } return res; } @@ -1537,12 +1380,7 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) // Substitute out any abstract values in ex Node n = d_absValues->substituteAbstractValues(formula); - ensureBoolean(n); - if(d_assertionList != NULL) { - d_assertionList->push_back(n); - } - bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); - d_private->addFormula(n, inUnsatCore, true, false, maybeHasFv); + d_asserts->assertFormula(n, inUnsatCore); return quickCheck().asEntailmentResult(); }/* SmtEngine::assertFormula() */ @@ -1801,7 +1639,7 @@ Expr SmtEngine::simplify(const Expr& ex) } // Make sure all preprocessing is done - d_private->processAssertions(); + d_private->processAssertions(*d_asserts); Node n = d_private->simplify(Node::fromExpr(e)); n = postprocess(n, TypeNode::fromType(e.getType())); return n.toExpr(); @@ -2233,9 +2071,10 @@ void SmtEngine::checkUnsatCore() { } void SmtEngine::checkModel(bool hardFailure) { + context::CDList* al = d_asserts->getAssertionList(); // --check-model implies --produce-assertions, which enables the // assertion list, so we should be ok. - Assert(d_assertionList != NULL) + Assert(al != nullptr) << "don't have an assertion list to check in SmtEngine::checkModel()"; TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); @@ -2354,7 +2193,7 @@ void SmtEngine::checkModel(bool hardFailure) { } // Now go through all our user assertions checking if they're satisfied. - for (const Node& assertion : *d_assertionList) + for (const Node& assertion : *al) { Notice() << "SmtEngine::checkModel(): checking assertion " << assertion << endl; @@ -2507,7 +2346,8 @@ void SmtEngine::checkSynthSolution() Trace("check-synth-sol") << "Retrieving assertions\n"; // Build conjecture from original assertions - if (d_assertionList == NULL) + context::CDList* al = d_asserts->getAssertionList(); + if (al == nullptr) { Trace("check-synth-sol") << "No assertions to check\n"; return; @@ -2516,7 +2356,7 @@ void SmtEngine::checkSynthSolution() std::vector auxAssertions; // expand definitions cache std::unordered_map cache; - for (const Node& assertion : *d_assertionList) + for (const Node& assertion : *al) { Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << assertion << endl; @@ -2857,9 +2697,10 @@ vector SmtEngine::getAssertions() { "Cannot query the current assertion list when not in produce-assertions mode."; throw ModalException(msg); } - Assert(d_assertionList != NULL); + context::CDList* al = d_asserts->getAssertionList(); + Assert(al != nullptr); std::vector res; - for (const Node& n : *d_assertionList) + for (const Node& n : *al) { res.emplace_back(n.toExpr()); } @@ -2874,7 +2715,7 @@ void SmtEngine::push() doPendingPops(); Trace("smt") << "SMT push()" << endl; d_private->notifyPush(); - d_private->processAssertions(); + d_private->processAssertions(*d_asserts); if(Dump.isOn("benchmark")) { Dump("benchmark") << PushCommand(); } @@ -2886,7 +2727,7 @@ void SmtEngine::push() // The problem isn't really "extended" yet, but this disallows // get-model after a push, simplifying our lives somewhat and // staying symmetric with pop. - setProblemExtended(); + d_smtMode = SMT_MODE_ASSERT; d_userLevels.push_back(d_userContext->getLevel()); internalPush(); @@ -2914,7 +2755,7 @@ void SmtEngine::pop() { // but also it would be weird to have a legally-executed (get-model) // that only returns a subset of the assignment (because the rest // is no longer in scope!). - setProblemExtended(); + d_smtMode = SMT_MODE_ASSERT; AlwaysAssert(d_userContext->getLevel() > 0); AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); @@ -2924,6 +2765,7 @@ void SmtEngine::pop() { d_userLevels.pop_back(); // Clear out assertion queues etc., in case anything is still in there + d_asserts->clearCurrent(); d_private->notifyPop(); Trace("userpushpop") << "SmtEngine: popped to level " @@ -2937,7 +2779,7 @@ void SmtEngine::internalPush() { Trace("smt") << "SmtEngine::internalPush()" << endl; doPendingPops(); if(options::incrementalSolving()) { - d_private->processAssertions(); + d_private->processAssertions(*d_asserts); TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); d_userContext->push(); // the d_context push is done inside of the SAT solver diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5a8c41652..5dc0d74fa 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -93,6 +93,7 @@ namespace prop { namespace smt { /** Utilities */ class AbstractValues; +class Assertions; class ExprNames; class DumpManager; class ResourceOutListener; @@ -409,7 +410,7 @@ class CVC4_PUBLIC SmtEngine * Note that the returned set of failed assumptions is not necessarily * minimal. */ - std::vector getUnsatAssumptions(void); + std::vector getUnsatAssumptions(void); /*---------------------------- sygus commands ---------------------------*/ @@ -1000,13 +1001,6 @@ class CVC4_PUBLIC SmtEngine */ void finalOptionsAreSet(); - /** - * Sets that the problem has been extended. This sets the smt mode of the - * solver to SMT_MODE_ASSERT, and clears the list of assumptions from the - * previous call to checkSatisfiability. - */ - void setProblemExtended(); - /** * Create theory engine, prop engine, decision engine. Called by * finalOptionsAreSet() @@ -1046,14 +1040,6 @@ class CVC4_PUBLIC SmtEngine */ theory::TheoryModel* getAvailableModel(const char* c) const; - /** - * Fully type-check the argument, and also type-check that it's - * actually Boolean. - * - * throw@ TypeCheckingException - */ - void ensureBoolean(const Node& n); - void internalPush(); void internalPop(bool immediate = false); @@ -1076,10 +1062,10 @@ class CVC4_PUBLIC SmtEngine const char* dumpTag = "declarations"); /* Check satisfiability (used to check satisfiability and entailment). */ - Result checkSatisfiability(const Expr& assumption, + Result checkSatisfiability(const Node& assumption, bool inUnsatCore, bool isEntailmentCheck); - Result checkSatisfiability(const std::vector& assumptions, + Result checkSatisfiability(const std::vector& assumptions, bool inUnsatCore, bool isEntailmentCheck); @@ -1124,6 +1110,8 @@ class CVC4_PUBLIC SmtEngine NodeManager* d_nodeManager; /** Abstract values */ std::unique_ptr d_absValues; + /** Assertions manager */ + std::unique_ptr d_asserts; /** Expression names */ std::unique_ptr d_exprNames; /** The dump manager */ @@ -1154,27 +1142,6 @@ class CVC4_PUBLIC SmtEngine /** The solver for abduction queries */ std::unique_ptr d_abductSolver; - - /** - * The assertion list (before any conversion) for supporting - * getAssertions(). Only maintained if in incremental mode. - */ - AssertionList* d_assertionList; - - /** - * 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; - - /** - * The list of assumptions from the previous call to checkSatisfiability. - * Note that if the last call to checkSatisfiability was an entailment check, - * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains - * one single assumption ~(a1 AND ... AND an). - */ - std::vector d_assumptions; - /** * List of items for which to retrieve values using getAssignment(). */ @@ -1236,11 +1203,6 @@ class CVC4_PUBLIC SmtEngine */ bool d_earlyTheoryPP; - /* - * Whether we did a global negation of the formula. - */ - bool d_globalNegation; - /** * Most recent result of last checkSatisfiability/checkEntailed or * (set-info :status). -- 2.30.2