diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3077 |
1 files changed, 650 insertions, 2427 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ff5cff5b6..2a0cde015 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5,7 +5,7 @@ ** Andrew Reynolds, Morgan Deters, Aina Niemetz ** 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. + ** 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 ** @@ -16,113 +16,55 @@ #include "smt/smt_engine.h" -#include <algorithm> -#include <cctype> -#include <iterator> -#include <memory> -#include <sstream> -#include <stack> -#include <string> -#include <tuple> -#include <unordered_map> -#include <unordered_set> -#include <utility> -#include <vector> - #include "api/cvc4cpp.h" #include "base/check.h" -#include "base/configuration.h" -#include "base/configuration_private.h" #include "base/exception.h" -#include "base/listener.h" #include "base/modal_exception.h" #include "base/output.h" -#include "context/cdhashmap.h" -#include "context/cdhashset.h" -#include "context/cdlist.h" -#include "context/context.h" #include "decision/decision_engine.h" -#include "expr/attribute.h" -#include "expr/expr.h" -#include "expr/kind.h" -#include "expr/metakind.h" #include "expr/node.h" -#include "expr/node_algorithm.h" -#include "expr/node_builder.h" -#include "expr/node_self_iterator.h" -#include "expr/node_visitor.h" -#include "options/arith_options.h" -#include "options/arrays_options.h" #include "options/base_options.h" -#include "options/booleans_options.h" -#include "options/bv_options.h" -#include "options/datatypes_options.h" -#include "options/decision_options.h" #include "options/language.h" #include "options/main_options.h" -#include "options/open_ostream.h" -#include "options/option_exception.h" #include "options/printer_options.h" -#include "options/proof_options.h" -#include "options/prop_options.h" -#include "options/quantifiers_options.h" -#include "options/sep_options.h" -#include "options/set_language.h" #include "options/smt_options.h" -#include "options/strings_options.h" #include "options/theory_options.h" -#include "options/uf_options.h" -#include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" -#include "preprocessing/preprocessing_pass_registry.h" #include "printer/printer.h" -#include "proof/proof.h" #include "proof/proof_manager.h" -#include "proof/theory_proof.h" #include "proof/unsat_core.h" -#include "prop/prop_engine.h" #include "smt/abduction_solver.h" -#include "smt/command.h" -#include "smt/command_list.h" +#include "smt/abstract_values.h" +#include "smt/assertions.h" +#include "smt/check_models.h" #include "smt/defined_function.h" +#include "smt/dump_manager.h" +#include "smt/interpolation_solver.h" +#include "smt/listeners.h" #include "smt/logic_request.h" -#include "smt/managed_ostreams.h" #include "smt/model_blocker.h" #include "smt/model_core_builder.h" -#include "smt/process_assertions.h" -#include "smt/set_defaults.h" +#include "smt/node_command.h" +#include "smt/options_manager.h" +#include "smt/preprocessor.h" +#include "smt/proof_manager.h" +#include "smt/quant_elim_solver.h" #include "smt/smt_engine_scope.h" +#include "smt/smt_engine_state.h" #include "smt/smt_engine_stats.h" -#include "smt/term_formula_removal.h" -#include "smt/update_ostream.h" -#include "smt_util/boolean_simplification.h" -#include "smt_util/nary_builder.h" -#include "theory/booleans/circuit_propagator.h" -#include "theory/bv/theory_bv_rewriter.h" -#include "theory/logic_info.h" -#include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/single_inv_partition.h" -#include "theory/quantifiers/sygus/synth_engine.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" +#include "smt/smt_solver.h" +#include "smt/sygus_solver.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/rewriter.h" -#include "theory/sort_inference.h" -#include "theory/strings/theory_strings.h" -#include "theory/substitutions.h" +#include "theory/smt_engine_subsolver.h" #include "theory/theory_engine.h" -#include "theory/theory_model.h" -#include "theory/theory_traits.h" -#include "util/hash.h" -#include "util/proof.h" #include "util/random.h" #include "util/resource_manager.h" -#if (IS_LFSC_BUILD && IS_PROOFS_BUILD) -#include "lfscc.h" -#endif +// required for hacks related to old proofs for unsat cores +#include "base/configuration.h" +#include "base/configuration_private.h" using namespace std; -using namespace CVC4; using namespace CVC4::smt; using namespace CVC4::preprocessing; using namespace CVC4::prop; @@ -131,539 +73,35 @@ using namespace CVC4::theory; namespace CVC4 { -namespace proof { -extern const char* const plf_signatures; -} // namespace proof - -namespace smt { - -struct DeleteCommandFunction : public std::unary_function<const Command*, void> -{ - void operator()(const Command* command) { delete command; } -}; - -void DeleteAndClearCommandVector(std::vector<Command*>& commands) { - std::for_each(commands.begin(), commands.end(), DeleteCommandFunction()); - commands.clear(); -} - -class SoftResourceOutListener : public Listener { - public: - SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} - void notify() override - { - SmtScope scope(d_smt); - Assert(smt::smtEngineInScope()); - d_smt->interrupt(); - } - private: - SmtEngine* d_smt; -}; /* class SoftResourceOutListener */ - - -class HardResourceOutListener : public Listener { - public: - HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} - void notify() override - { - SmtScope scope(d_smt); - theory::Rewriter::clearCaches(); - } - private: - SmtEngine* d_smt; -}; /* class HardResourceOutListener */ - -class BeforeSearchListener : public Listener { - public: - BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {} - void notify() override { d_smt->beforeSearch(); } - - private: - SmtEngine* d_smt; -}; /* class BeforeSearchListener */ - -class SetDefaultExprDepthListener : public Listener { - public: - void notify() override - { - int depth = options::defaultExprDepth(); - Debug.getStream() << expr::ExprSetDepth(depth); - Trace.getStream() << expr::ExprSetDepth(depth); - Notice.getStream() << expr::ExprSetDepth(depth); - Chat.getStream() << expr::ExprSetDepth(depth); - Message.getStream() << expr::ExprSetDepth(depth); - Warning.getStream() << expr::ExprSetDepth(depth); - // intentionally exclude Dump stream from this list - } -}; - -class SetDefaultExprDagListener : public Listener { - public: - void notify() override - { - int dag = options::defaultDagThresh(); - Debug.getStream() << expr::ExprDag(dag); - Trace.getStream() << expr::ExprDag(dag); - Notice.getStream() << expr::ExprDag(dag); - Chat.getStream() << expr::ExprDag(dag); - Message.getStream() << expr::ExprDag(dag); - Warning.getStream() << expr::ExprDag(dag); - Dump.getStream() << expr::ExprDag(dag); - } -}; - -class SetPrintExprTypesListener : public Listener { - public: - void notify() override - { - bool value = options::printExprTypes(); - Debug.getStream() << expr::ExprPrintTypes(value); - Trace.getStream() << expr::ExprPrintTypes(value); - Notice.getStream() << expr::ExprPrintTypes(value); - Chat.getStream() << expr::ExprPrintTypes(value); - Message.getStream() << expr::ExprPrintTypes(value); - Warning.getStream() << expr::ExprPrintTypes(value); - // intentionally exclude Dump stream from this list - } -}; - -class DumpModeListener : public Listener { - public: - void notify() override - { - const std::string& value = options::dumpModeString(); - Dump.setDumpFromString(value); - } -}; - -class PrintSuccessListener : public Listener { - public: - void notify() override - { - bool value = options::printSuccess(); - Debug.getStream() << Command::printsuccess(value); - Trace.getStream() << Command::printsuccess(value); - Notice.getStream() << Command::printsuccess(value); - Chat.getStream() << Command::printsuccess(value); - Message.getStream() << Command::printsuccess(value); - Warning.getStream() << Command::printsuccess(value); - *options::out() << Command::printsuccess(value); - } -}; - - - -/** - * This is an inelegant solution, but for the present, it will work. - * The point of this is to separate the public and private portions of - * the SmtEngine class, so that smt_engine.h doesn't - * include "expr/node.h", which is a private CVC4 header (and can lead - * to linking errors due to the improper inlining of non-visible symbols - * into user code!). - * - * The "real" solution (that which is usually implemented) is to move - * ALL the implementation to SmtEnginePrivate and maintain a - * heap-allocated instance of it in SmtEngine. SmtEngine (the public - * one) becomes an "interface shell" which simply acts as a forwarder - * of method calls. - */ -class SmtEnginePrivate : public NodeManagerListener { - SmtEngine& d_smt; - - typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap; - typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap; - - /** Manager for the memory of regular-output-channel. */ - ManagedRegularOutputChannel d_managedRegularChannel; - - /** Manager for the memory of diagnostic-output-channel. */ - ManagedDiagnosticOutputChannel d_managedDiagnosticChannel; - - /** Manager for the memory of --dump-to. */ - ManagedDumpOStream d_managedDumpChannel; - - /** - * This list contains: - * softResourceOut - * hardResourceOut - * beforeSearchListener - * - * This needs to be deleted before both NodeManager's Options, - * SmtEngine, d_resourceManager, and TheoryEngine. - */ - ListenerRegistrationList* d_listenerRegistrations; - - /** 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<bool> d_assertionsProcessed; - - // Cached true value - Node d_true; - - /** - * A context that never pushes/pops, for use by CD structures (like - * SubstitutionMaps) that should be "global". - */ - context::Context d_fakeContext; - - /** - * A map of AbsractValues to their actual constants. Only used if - * options::abstractValues() is on. - */ - SubstitutionMap d_abstractValueMap; - - /** - * A mapping of all abstract values (actual value |-> abstract) that - * we've handed out. This is necessary to ensure that we give the - * same AbstractValues for the same real constants. Only used if - * options::abstractValues() is on. - */ - NodeToNodeHashMap d_abstractValues; - - /** TODO: whether certain preprocess steps are necessary */ - //bool d_needsExpandDefs; - - /** The preprocessing pass context */ - std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext; - - /** Process assertions module */ - ProcessAssertions d_processor; - - //------------------------------- expression names - /** mapping from expressions to name */ - context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames; - //------------------------------- end expression names - public: - IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); } - - /** Instance of the ITE remover */ - RemoveTermFormulas d_iteRemover; - - /* Finishes the initialization of the private portion of SMTEngine. */ - void finishInit(); - - /*------------------- sygus utils ------------------*/ - /** - * sygus variables declared (from "declare-var" and "declare-fun" commands) - * - * The SyGuS semantics for declared variables is that they are implicitly - * universally quantified in the constraints. - */ - std::vector<Node> d_sygusVars; - /** sygus constraints */ - std::vector<Node> d_sygusConstraints; - /** functions-to-synthesize */ - std::vector<Node> d_sygusFunSymbols; - /** - * Whether we need to reconstruct the sygus conjecture. - */ - CDO<bool> d_sygusConjectureStale; - /*------------------- end of sygus utils ------------------*/ - - public: - SmtEnginePrivate(SmtEngine& smt) - : d_smt(smt), - d_managedRegularChannel(), - d_managedDiagnosticChannel(), - d_managedDumpChannel(), - d_listenerRegistrations(new ListenerRegistrationList()), - d_propagator(true, true), - d_assertions(), - d_assertionsProcessed(smt.getUserContext(), false), - d_fakeContext(), - d_abstractValueMap(&d_fakeContext), - d_abstractValues(), - d_processor(smt, *smt.getResourceManager()), - // d_needsExpandDefs(true), //TODO? - d_exprNames(smt.getUserContext()), - d_iteRemover(smt.getUserContext()), - d_sygusConjectureStale(smt.getUserContext(), true) - { - d_smt.d_nodeManager->subscribeEvents(this); - d_true = NodeManager::currentNM()->mkConst(true); - ResourceManager* rm = d_smt.getResourceManager(); - - d_listenerRegistrations->add( - rm->registerSoftListener(new SoftResourceOutListener(d_smt))); - - d_listenerRegistrations->add( - rm->registerHardListener(new HardResourceOutListener(d_smt))); - - try - { - Options& opts = d_smt.getOptions(); - // Multiple options reuse BeforeSearchListener so registration requires an - // extra bit of care. - // We can safely not call notify on this before search listener at - // registration time. This d_smt cannot be beforeSearch at construction - // time. Therefore the BeforeSearchListener is a no-op. Therefore it does - // not have to be called. - d_listenerRegistrations->add( - opts.registerBeforeSearchListener(new BeforeSearchListener(d_smt))); - - // These do need registration calls. - d_listenerRegistrations->add(opts.registerSetDefaultExprDepthListener( - new SetDefaultExprDepthListener(), true)); - d_listenerRegistrations->add(opts.registerSetDefaultExprDagListener( - new SetDefaultExprDagListener(), true)); - d_listenerRegistrations->add(opts.registerSetPrintExprTypesListener( - new SetPrintExprTypesListener(), true)); - d_listenerRegistrations->add( - opts.registerSetDumpModeListener(new DumpModeListener(), true)); - d_listenerRegistrations->add(opts.registerSetPrintSuccessListener( - new PrintSuccessListener(), true)); - d_listenerRegistrations->add(opts.registerSetRegularOutputChannelListener( - new SetToDefaultSourceListener(&d_managedRegularChannel), true)); - d_listenerRegistrations->add( - opts.registerSetDiagnosticOutputChannelListener( - new SetToDefaultSourceListener(&d_managedDiagnosticChannel), - true)); - d_listenerRegistrations->add(opts.registerDumpToFileNameListener( - new SetToDefaultSourceListener(&d_managedDumpChannel), true)); - } - catch (OptionException& e) - { - // Registering the option listeners can lead to OptionExceptions, e.g. - // when the user chooses a dump tag that does not exist. In that case, we - // have to make sure that we delete existing listener registrations and - // that we unsubscribe from NodeManager events. Otherwise we will have - // errors in the deconstructors of the NodeManager (because the - // NodeManager tries to notify an SmtEnginePrivate that does not exist) - // and the ListenerCollection (because not all registrations have been - // removed before calling the deconstructor). - delete d_listenerRegistrations; - d_smt.d_nodeManager->unsubscribeEvents(this); - throw OptionException(e.getRawMessage()); - } - } - - ~SmtEnginePrivate() - { - delete d_listenerRegistrations; - - if(d_propagator.getNeedsFinish()) { - d_propagator.finish(); - d_propagator.setNeedsFinish(false); - } - d_smt.d_nodeManager->unsubscribeEvents(this); - } - - void spendResource(ResourceManager::Resource r) - { - d_smt.getResourceManager()->spendResource(r); - } - - ProcessAssertions* getProcessAssertions() { return &d_processor; } - - void nmNotifyNewSort(TypeNode tn, uint32_t flags) override - { - DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), - 0, - tn.toType()); - if((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) { - d_smt.addToModelCommandAndDump(c, flags); - } - } - - void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override - { - DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), - tn.getAttribute(expr::SortArityAttr()), - tn.toType()); - if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) - { - d_smt.addToModelCommandAndDump(c); - } - } - - void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts, - uint32_t flags) override - { - if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0) - { - std::vector<Type> types(dtts.begin(), dtts.end()); - DatatypeDeclarationCommand c(types); - d_smt.addToModelCommandAndDump(c); - } - } - - void nmNotifyNewVar(TNode n, uint32_t flags) override - { - DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()), - n.toExpr(), - n.getType().toType()); - if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) { - d_smt.addToModelCommandAndDump(c, flags); - } - } - - void nmNotifyNewSkolem(TNode n, - const std::string& comment, - uint32_t flags) override - { - string id = n.getAttribute(expr::VarNameAttr()); - DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType()); - if(Dump.isOn("skolems") && comment != "") { - Dump("skolems") << CommentCommand(id + " is " + comment); - } - if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) { - d_smt.addToModelCommandAndDump(c, flags, false, "skolems"); - } - } - - void nmNotifyDeleteNode(TNode n) override {} - - Node applySubstitutions(TNode node) - { - return Rewriter::rewrite( - d_preprocessingPassContext->getTopLevelSubstitutions().apply(node)); - } - - /** - * Process the assertions that have been asserted. - */ - void processAssertions(); - - /** Process a user push. - */ - void notifyPush() { - - } - - /** - * Process a user pop. Clears out the non-context-dependent stuff in this - * SmtEnginePrivate. Necessary to clear out our assertion vectors in case - * someone does a push-assert-pop without a check-sat. It also pops the - * 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. - */ - Node simplify(TNode in) { - // Substitute out any abstract values in ex. - // 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(); - } - - /** - * Substitute away all AbstractValues in a node. - */ - Node substituteAbstractValues(TNode n) { - // We need to do this even if options::abstractValues() is off, - // since the setting might have changed after we already gave out - // some abstract values. - return d_abstractValueMap.apply(n); - } - - /** - * Make a new (or return an existing) abstract value for a node. - * Can only use this if options::abstractValues() is on. - */ - Node mkAbstractValue(TNode n) { - Assert(options::abstractValues()); - Node& val = d_abstractValues[n]; - if(val.isNull()) { - val = d_smt.d_nodeManager->mkAbstractValue(n.getType()); - d_abstractValueMap.addSubstitution(val, n); - } - // We are supposed to ascribe types to all abstract values that go out. - NodeManager* current = d_smt.d_nodeManager; - Node ascription = current->mkConst(AscriptionType(n.getType().toType())); - Node retval = current->mkNode(kind::APPLY_TYPE_ASCRIPTION, ascription, val); - return retval; - } - - //------------------------------- expression names - // implements setExpressionName, as described in smt_engine.h - void setExpressionName(Expr e, std::string name) { - d_exprNames[Node::fromExpr(e)] = name; - } - - // implements getExpressionName, as described in smt_engine.h - bool getExpressionName(Expr e, std::string& name) const { - context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e); - if(it!=d_exprNames.end()) { - name = (*it).second; - return true; - }else{ - return false; - } - } - //------------------------------- end expression names -};/* class SmtEnginePrivate */ - -}/* namespace CVC4::smt */ - SmtEngine::SmtEngine(ExprManager* em, Options* optr) - : d_context(new Context()), - d_userContext(new UserContext()), - d_userLevels(), + : d_state(new SmtEngineState(*this)), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), - d_theoryEngine(nullptr), - d_propEngine(nullptr), + d_absValues(new AbstractValues(d_nodeManager)), + d_asserts(new Assertions(getUserContext(), *d_absValues.get())), + d_dumpm(new DumpManager(getUserContext())), + d_routListener(new ResourceOutListener(*this)), + d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)), + d_smtSolver(nullptr), d_proofManager(nullptr), + d_model(nullptr), + d_checkModels(nullptr), + d_pfManager(nullptr), d_rewriter(new theory::Rewriter()), d_definedFunctions(nullptr), + d_sygusSolver(nullptr), d_abductSolver(nullptr), - d_assertionList(nullptr), - d_assignments(nullptr), - d_modelGlobalCommands(), - d_modelCommands(nullptr), - d_dumpCommands(), - d_defineCommands(), + d_interpolSolver(nullptr), + d_quantElimSolver(nullptr), d_logic(), d_originalOptions(), d_isInternalSubsolver(false), - d_pendingPops(0), - d_fullyInited(false), - d_queryMade(false), - d_needPostsolve(false), - d_globalNegation(false), - d_status(), - d_expectedStatus(), - d_smtMode(SMT_MODE_START), - d_private(nullptr), d_statisticsRegistry(nullptr), d_stats(nullptr), + d_outMgr(this), d_resourceManager(nullptr), + d_optm(nullptr), + d_pp(nullptr), d_scope(nullptr) { // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine @@ -688,9 +126,24 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_statisticsRegistry.reset(new StatisticsRegistry()); d_resourceManager.reset( new ResourceManager(*d_statisticsRegistry.get(), d_options)); - d_private.reset(new smt::SmtEnginePrivate(*this)); + d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get())); + // listen to node manager events + d_nodeManager->subscribeEvents(d_snmListener.get()); + // listen to resource out + d_resourceManager->registerListener(d_routListener.get()); + // make statistics d_stats.reset(new SmtEngineStatistics()); - d_stats->d_resourceUnitsUsed.setData(d_resourceManager->getResourceUsage()); + // reset the preprocessor + d_pp.reset(new smt::Preprocessor( + *this, getUserContext(), *d_absValues.get(), *d_stats)); + // make the SMT solver + d_smtSolver.reset( + new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats)); + // make the SyGuS solver + d_sygusSolver.reset( + new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr)); + // make the quantifier elimination solver + d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver)); // The ProofManager is constructed before any other proof objects such as // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are @@ -705,96 +158,103 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) #endif d_definedFunctions = new (true) DefinedFunctionMap(getUserContext()); - d_modelCommands = new (true) smt::CommandList(getUserContext()); } -void SmtEngine::finishInit() +bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); } +bool SmtEngine::isQueryMade() const { return d_state->isQueryMade(); } +size_t SmtEngine::getNumUserLevels() const { - // Notice that finishInit is called when options are finalized. If we are - // parsing smt2, this occurs at the moment we enter "Assert mode", page 52 - // of SMT-LIB 2.6 standard. + return d_state->getNumUserLevels(); +} +SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); } +bool SmtEngine::isSmtModeSat() const +{ + SmtMode mode = getSmtMode(); + return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN; +} +Result SmtEngine::getStatusOfLastCommand() const +{ + return d_state->getStatus(); +} +context::UserContext* SmtEngine::getUserContext() +{ + return d_state->getUserContext(); +} +context::Context* SmtEngine::getContext() { return d_state->getContext(); } - // Inialize the resource manager based on the options. - d_resourceManager->setHardLimit(options::hardLimit()); - if (options::perCallResourceLimit() != 0) - { - d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false); - } - if (options::cumulativeResourceLimit() != 0) - { - d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(), - true); - } - if (options::perCallMillisecondLimit() != 0) - { - d_resourceManager->setTimeLimit(options::perCallMillisecondLimit(), false); - } - if (options::cumulativeMillisecondLimit() != 0) +TheoryEngine* SmtEngine::getTheoryEngine() +{ + return d_smtSolver->getTheoryEngine(); +} + +prop::PropEngine* SmtEngine::getPropEngine() +{ + return d_smtSolver->getPropEngine(); +} + +void SmtEngine::finishInit() +{ + if (d_state->isFullyInited()) { - d_resourceManager->setTimeLimit(options::cumulativeMillisecondLimit(), - true); + // already initialized, return + return; } - if (options::cpuTime()) + + // Notice that finishInitInternal is called when options are finalized. If we + // are parsing smt2, this occurs at the moment we enter "Assert mode", page 52 + // of SMT-LIB 2.6 standard. + + // set the logic + if (!d_logic.isLocked()) { - d_resourceManager->useCPUTime(true); + setLogicInternal(); } // set the random seed Random::getRandom().setSeed(options::seed()); - // ensure that our heuristics are properly set up - setDefaults(d_logic, d_isInternalSubsolver); - - Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; - // We have mutual dependency here, so we add the prop engine to the theory - // engine later (it is non-essential there) - d_theoryEngine.reset(new TheoryEngine(getContext(), - getUserContext(), - getResourceManager(), - d_private->d_iteRemover, - const_cast<const LogicInfo&>(d_logic))); - - // Add the theories - for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { - TheoryConstructor::addTheory(getTheoryEngine(), id); - //register with proof engine if applicable -#ifdef CVC4_PROOF - ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); -#endif - } + // Call finish init on the options manager. This inializes the resource + // manager based on the options, and sets up the best default options + // based on our heuristics. + d_optm->finishInit(d_logic, d_isInternalSubsolver); - Trace("smt-debug") << "Making decision engine..." << std::endl; + ProofNodeManager* pnm = nullptr; + if (options::proofNew()) + { + d_pfManager.reset(new PfManager(getUserContext(), this)); + PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator(); + // use this proof node manager + pnm = d_pfManager->getProofNodeManager(); + // enable proof support in the rewriter + d_rewriter->setProofNodeManager(pnm); + // enable it in the assertions pipeline + d_asserts->setProofGenerator(pppg); + // enable it in the SmtSolver + d_smtSolver->setProofNodeManager(pnm); + // enabled proofs in the preprocessor + d_pp->setProofGenerator(pppg); + } - Trace("smt-debug") << "Making prop engine..." << std::endl; - /* force destruction of referenced PropEngine to enforce that statistics - * are unregistered by the obsolete PropEngine object before registered - * again by the new PropEngine object */ - d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - getTheoryEngine(), getContext(), getUserContext(), getResourceManager())); + Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; + d_smtSolver->finishInit(const_cast<const LogicInfo&>(d_logic)); - Trace("smt-debug") << "Setting up theory engine..." << std::endl; - d_theoryEngine->setPropEngine(getPropEngine()); - Trace("smt-debug") << "Finishing init for theory engine..." << std::endl; - d_theoryEngine->finishInit(); + // now can construct the SMT-level model object + TheoryEngine* te = d_smtSolver->getTheoryEngine(); + Assert(te != nullptr); + TheoryModel* tm = te->getModel(); + if (tm != nullptr) + { + d_model.reset(new Model(*this, tm)); + // make the check models utility + d_checkModels.reset(new CheckModels(*d_smtSolver.get())); + } // global push/pop around everything, to ensure proper destruction // of context-dependent data structures - 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<Node>()); - } + d_state->setup(); + + 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. @@ -802,74 +262,45 @@ void SmtEngine::finishInit() { LogicInfo everything; everything.lock(); - Dump("benchmark") << CommentCommand( + getOutputManager().getPrinter().toStreamCmdComment( + getOutputManager().getDumpOut(), "CVC4 always dumps the most general, all-supported logic (below), as " "some internals might require the use of a logic more general than " - "the input.") - << SetBenchmarkLogicCommand( - everything.getLogicString()); + "the input."); + getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic( + getOutputManager().getDumpOut(), everything.getLogicString()); } - Trace("smt-debug") << "Dump declaration commands..." << std::endl; - // dump out any pending declaration commands - for(unsigned i = 0; i < d_dumpCommands.size(); ++i) { - Dump("declarations") << *d_dumpCommands[i]; - delete d_dumpCommands[i]; - } - d_dumpCommands.clear(); + // initialize the dump manager + d_dumpm->finishInit(); // subsolvers if (options::produceAbducts()) { d_abductSolver.reset(new AbductionSolver(this)); } - - PROOF( ProofManager::currentPM()->setLogic(d_logic); ); - PROOF({ - for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { - ProofManager::currentPM()->getTheoryProofEngine()-> - finishRegisterTheory(d_theoryEngine->theoryOf(id)); - } - }); - d_private->finishInit(); - Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; -} - -void SmtEngine::finalOptionsAreSet() { - if(d_fullyInited) { - return; - } - - if(! d_logic.isLocked()) { - setLogicInternal(); + if (options::produceInterpols() != options::ProduceInterpols::NONE) + { + d_interpolSolver.reset(new InterpolationSolver(this)); } - // finish initialization, create the prop engine, etc. - finishInit(); + d_pp->finishInit(); - AlwaysAssert(d_propEngine->getAssertionLevel() == 0) + AlwaysAssert(getPropEngine()->getAssertionLevel() == 0) << "The PropEngine has pushed but the SmtEngine " "hasn't finished initializing!"; - d_fullyInited = true; Assert(d_logic.isLocked()); + + // store that we are finished initializing + d_state->finishInit(); + Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; } void SmtEngine::shutdown() { - doPendingPops(); + d_state->shutdown(); - while(options::incrementalSolving() && d_userContext->getLevel() > 1) { - internalPop(true); - } - - if (d_propEngine != nullptr) - { - d_propEngine->shutdown(); - } - if (d_theoryEngine != nullptr) - { - d_theoryEngine->shutdown(); - } + d_smtSolver->shutdown(); } SmtEngine::~SmtEngine() @@ -881,35 +312,12 @@ SmtEngine::~SmtEngine() // global push/pop around everything, to ensure proper destruction // of context-dependent data structures - d_context->popto(0); - d_userContext->popto(0); - - if(d_assignments != NULL) { - d_assignments->deleteSelf(); - } - - d_globalDefineFunRecLemmas.reset(); - - if(d_assertionList != NULL) { - d_assertionList->deleteSelf(); - } - - for(unsigned i = 0; i < d_dumpCommands.size(); ++i) { - delete d_dumpCommands[i]; - d_dumpCommands[i] = NULL; - } - d_dumpCommands.clear(); - - DeleteAndClearCommandVector(d_modelGlobalCommands); - - if(d_modelCommands != NULL) { - d_modelCommands->deleteSelf(); - } + d_state->cleanup(); d_definedFunctions->deleteSelf(); //destroy all passes before destroying things that they refer to - d_private->getProcessAssertions()->cleanup(); + d_pp->cleanup(); // d_proofManager is always created when proofs are enabled at configure // time. Because of this, this code should not be wrapped in PROOF() which @@ -922,18 +330,25 @@ SmtEngine::~SmtEngine() d_proofManager.reset(nullptr); #endif - d_theoryEngine.reset(nullptr); - d_propEngine.reset(nullptr); + d_absValues.reset(nullptr); + d_asserts.reset(nullptr); + d_dumpm.reset(nullptr); + + d_sygusSolver.reset(nullptr); + + d_smtSolver.reset(nullptr); d_stats.reset(nullptr); - d_private.reset(nullptr); + d_nodeManager->unsubscribeEvents(d_snmListener.get()); + d_snmListener.reset(nullptr); + d_routListener.reset(nullptr); + d_optm.reset(nullptr); + d_pp.reset(nullptr); // d_resourceManager must be destroyed before d_statisticsRegistry d_resourceManager.reset(nullptr); d_statisticsRegistry.reset(nullptr); - - - d_userContext.reset(nullptr); - d_context.reset(nullptr); + // destroy the state + d_state.reset(nullptr); } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << endl << e << endl; @@ -943,7 +358,8 @@ SmtEngine::~SmtEngine() void SmtEngine::setLogic(const LogicInfo& logic) { SmtScope smts(this); - if(d_fullyInited) { + if (d_state->isFullyInited()) + { throw ModalException("Cannot set logic in SmtEngine after the engine has " "finished initializing."); } @@ -961,8 +377,8 @@ void SmtEngine::setLogic(const std::string& s) // dump out a set-logic command if (Dump.isOn("raw-benchmark")) { - Dump("raw-benchmark") - << SetBenchmarkLogicCommand(d_logic.getLogicString()); + getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic( + getOutputManager().getDumpOut(), d_logic.getLogicString()); } } catch (IllegalArgumentException& e) @@ -972,9 +388,8 @@ void SmtEngine::setLogic(const std::string& s) } void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } -LogicInfo SmtEngine::getLogicInfo() const { - return d_logic; -} + +const LogicInfo& SmtEngine::getLogicInfo() const { return d_logic; } LogicInfo SmtEngine::getUserLogicInfo() const { @@ -987,30 +402,26 @@ LogicInfo SmtEngine::getUserLogicInfo() const void SmtEngine::notifyStartParsing(std::string filename) { - d_filename = filename; - + d_state->setFilename(filename); // Copy the original options. This is called prior to beginning parsing. // Hence reset should revert to these options, which note is after reading // the command line. d_originalOptions.copyValues(d_options); } -std::string SmtEngine::getFilename() const { return d_filename; } +const std::string& SmtEngine::getFilename() const +{ + return d_state->getFilename(); +} void SmtEngine::setLogicInternal() { - Assert(!d_fullyInited) + Assert(!d_state->isFullyInited()) << "setting logic in SmtEngine but the engine has already" " finished initializing for this run"; d_logic.lock(); 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); @@ -1020,12 +431,14 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) if(Dump.isOn("benchmark")) { if(key == "status") { string s = value.getValue(); - BenchmarkStatus status = - (s == "sat") ? SMT_SATISFIABLE : - ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN); - Dump("benchmark") << SetBenchmarkStatusCommand(status); + Result::Sat status = + (s == "sat") ? Result::SAT + : ((s == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN); + getOutputManager().getPrinter().toStreamCmdSetBenchmarkStatus( + getOutputManager().getDumpOut(), status); } else { - Dump("benchmark") << SetInfoCommand(key, value); + getOutputManager().getPrinter().toStreamCmdSetInfo( + getOutputManager().getDumpOut(), key, value); } } @@ -1038,7 +451,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) } else if (key == "filename") { - d_filename = value.getValue(); + d_state->setFilename(value.getValue()); return; } else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser()) @@ -1082,7 +495,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) throw OptionException("argument to (set-info :status ..) must be " "`sat' or `unsat' or `unknown'"); } - d_expectedStatus = Result(s, d_filename); + d_state->notifyExpectedStatus(s); return; } throw UnrecognizedOptionException(); @@ -1157,7 +570,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const if (key == "status") { // sat | unsat | unknown - switch (d_status.asSatisfiabilityResult().isSat()) + Result status = d_state->getStatus(); + switch (status.asSatisfiabilityResult().isSat()) { case Result::SAT: return SExpr(SExpr::Keyword("sat")); case Result::UNSAT: return SExpr(SExpr::Keyword("unsat")); @@ -1166,10 +580,11 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const } if (key == "reason-unknown") { - if (!d_status.isNull() && d_status.isUnknown()) + Result status = d_state->getStatus(); + if (!status.isNull() && status.isUnknown()) { - stringstream ss; - ss << d_status.whyUnknown(); + std::stringstream ss; + ss << status.whyUnknown(); string s = ss.str(); transform(s.begin(), s.end(), s.begin(), ::tolower); return SExpr(SExpr::Keyword(s)); @@ -1183,9 +598,9 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const } if (key == "assertion-stack-levels") { - AlwaysAssert(d_userLevels.size() - <= std::numeric_limits<unsigned long int>::max()); - return SExpr(static_cast<unsigned long int>(d_userLevels.size())); + size_t ulevel = d_state->getNumUserLevels(); + AlwaysAssert(ulevel <= std::numeric_limits<unsigned long int>::max()); + return SExpr(static_cast<unsigned long int>(ulevel)); } Assert(key == "all-options"); // get the options, like all-statistics @@ -1194,33 +609,36 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const return SExpr::parseListOfListOfAtoms(current_options); } -void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func) +void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func) { - for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) { + for (std::vector<Node>::const_iterator i = formals.begin(); + i != formals.end(); + ++i) + { if((*i).getKind() != kind::BOUND_VARIABLE) { stringstream ss; ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n" << "definition of function " << func << ", formal\n" << " " << *i << "\n" << "has kind " << (*i).getKind(); - throw TypeCheckingException(func, ss.str()); + throw TypeCheckingException(func.toExpr(), ss.str()); } } } -void SmtEngine::debugCheckFunctionBody(Expr formula, - const std::vector<Expr>& formals, - Expr func) +void SmtEngine::debugCheckFunctionBody(Node formula, + const std::vector<Node>& formals, + Node func) { - Type formulaType = formula.getType(options::typeChecking()); - Type funcType = func.getType(); + TypeNode formulaType = formula.getType(options::typeChecking()); + TypeNode funcType = func.getType(); // We distinguish here between definitions of constants and functions, // because the type checking for them is subtly different. Perhaps we // should instead have SmtEngine::defineFunction() and // SmtEngine::defineConstant() for better clarity, although then that // doesn't match the SMT-LIBv2 standard... if(formals.size() > 0) { - Type rangeType = FunctionType(funcType).getRangeType(); + TypeNode rangeType = funcType.getRangeType(); if(! formulaType.isComparableTo(rangeType)) { stringstream ss; ss << "Type of defined function does not match its declaration\n" @@ -1228,29 +646,29 @@ void SmtEngine::debugCheckFunctionBody(Expr formula, << "Declared type : " << rangeType << "\n" << "The body : " << formula << "\n" << "Body type : " << formulaType; - throw TypeCheckingException(func, ss.str()); + throw TypeCheckingException(func.toExpr(), ss.str()); } } else { if(! formulaType.isComparableTo(funcType)) { stringstream ss; ss << "Declared type of defined constant does not match its definition\n" << "The constant : " << func << "\n" - << "Declared type : " << funcType << " " << Type::getTypeNode(funcType)->getId() << "\n" + << "Declared type : " << funcType << "\n" << "The definition : " << formula << "\n" - << "Definition type: " << formulaType << " " << Type::getTypeNode(formulaType)->getId(); - throw TypeCheckingException(func, ss.str()); + << "Definition type: " << formulaType; + throw TypeCheckingException(func.toExpr(), ss.str()); } } } -void SmtEngine::defineFunction(Expr func, - const std::vector<Expr>& formals, - Expr formula, +void SmtEngine::defineFunction(Node func, + const std::vector<Node>& formals, + Node formula, bool global) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); Trace("smt") << "SMT defineFunction(" << func << ")" << endl; debugCheckFormals(formals, func); @@ -1258,53 +676,48 @@ void SmtEngine::defineFunction(Expr func, ss << language::SetLanguage( language::SetLanguage::getLanguage(Dump.getStream())) << func; - DefineFunctionCommand c(ss.str(), func, formals, formula, global); - addToModelCommandAndDump( - c, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); + std::vector<Node> nFormals; + nFormals.reserve(formals.size()); + + for (const Node& formal : formals) + { + nFormals.push_back(formal); + } - PROOF(if (options::checkUnsatCores()) { - d_defineCommands.push_back(c.clone()); - }); + DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula); + d_dumpm->addToModelCommandAndDump( + nc, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); // type check body debugCheckFunctionBody(formula, formals, func); // Substitute out any abstract values in formula - Node formNode = d_private->substituteAbstractValues(Node::fromExpr(formula)); - - TNode funcNode = func.getTNode(); - vector<Node> formalsNodes; - for(vector<Expr>::const_iterator i = formals.begin(), - iend = formals.end(); - i != iend; - ++i) { - formalsNodes.push_back((*i).getNode()); - } - DefinedFunction def(funcNode, formalsNodes, formNode); + 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 " << funcNode << " " << formNode << endl; + Debug("smt") << "definedFunctions insert " << func << " " << formNode << endl; if (global) { - d_definedFunctions->insertAtContextLevelZero(funcNode, def); + d_definedFunctions->insertAtContextLevelZero(func, def); } else { - d_definedFunctions->insert(funcNode, def); + d_definedFunctions->insert(func, def); } } void SmtEngine::defineFunctionsRec( - const std::vector<Expr>& funcs, - const std::vector<std::vector<Expr>>& formals, - const std::vector<Expr>& formulas, + const std::vector<Node>& funcs, + const std::vector<std::vector<Node>>& formals, + const std::vector<Node>& formulas, bool global) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); Trace("smt") << "SMT defineFunctionsRec(...)" << endl; if (funcs.size() != formals.size() && funcs.size() != formulas.size()) @@ -1328,24 +741,15 @@ void SmtEngine::defineFunctionsRec( if (Dump.isOn("raw-benchmark")) { - std::vector<api::Term> tFuncs = api::exprVectorToTerms(d_solver, funcs); - std::vector<std::vector<api::Term>> tFormals; - for (const std::vector<Expr>& formal : formals) - { - tFormals.emplace_back(api::exprVectorToTerms(d_solver, formal)); - } - std::vector<api::Term> tFormulas = - api::exprVectorToTerms(d_solver, formulas); - Dump("raw-benchmark") << DefineFunctionRecCommand( - d_solver, tFuncs, tFormals, tFormulas, global); + getOutputManager().getPrinter().toStreamCmdDefineFunctionRec( + getOutputManager().getDumpOut(), funcs, formals, formulas); } - ExprManager* em = getExprManager(); - bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); + NodeManager* nm = getNodeManager(); for (unsigned i = 0, size = funcs.size(); i < size; i++) { // we assert a quantified formula - Expr func_app; + Node func_app; // make the function application if (formals[i].empty()) { @@ -1354,120 +758,60 @@ void SmtEngine::defineFunctionsRec( } else { - std::vector<Expr> children; + std::vector<Node> children; children.push_back(funcs[i]); children.insert(children.end(), formals[i].begin(), formals[i].end()); - func_app = em->mkExpr(kind::APPLY_UF, children); + func_app = nm->mkNode(kind::APPLY_UF, children); } - Expr lem = em->mkExpr(kind::EQUAL, func_app, formulas[i]); + Node lem = nm->mkNode(kind::EQUAL, func_app, formulas[i]); if (!formals[i].empty()) { // set the attribute to denote this is a function definition - std::string attr_name("fun-def"); - Expr aexpr = em->mkExpr(kind::INST_ATTRIBUTE, func_app); - aexpr = em->mkExpr(kind::INST_PATTERN_LIST, aexpr); - std::vector<Expr> expr_values; - std::string str_value; - setUserAttribute(attr_name, func_app, expr_values, str_value); + Node aexpr = nm->mkNode(kind::INST_ATTRIBUTE, func_app); + aexpr = nm->mkNode(kind::INST_PATTERN_LIST, aexpr); + FunDefAttribute fda; + func_app.setAttribute(fda, true); // make the quantified formula - Expr boundVars = em->mkExpr(kind::BOUND_VAR_LIST, formals[i]); - lem = em->mkExpr(kind::FORALL, boundVars, lem, aexpr); + Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]); + lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr); } // assert the quantified formula // notice we don't call assertFormula directly, since this would // duplicate the output on raw-benchmark. - Node n = d_private->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); - } + // add define recursive definition to the assertions + d_asserts->addDefineFunRecDefinition(lem, global); } } -void SmtEngine::defineFunctionRec(Expr func, - const std::vector<Expr>& formals, - Expr formula, +void SmtEngine::defineFunctionRec(Node func, + const std::vector<Node>& formals, + Node formula, bool global) { - std::vector<Expr> funcs; + std::vector<Node> funcs; funcs.push_back(func); - std::vector<std::vector<Expr> > formals_multi; + std::vector<std::vector<Node>> formals_multi; formals_multi.push_back(formals); - std::vector<Expr> formulas; + std::vector<Node> formulas; formulas.push_back(formula); defineFunctionsRec(funcs, formals_multi, formulas, global); } -bool SmtEngine::isDefinedFunction( Expr func ){ - Node nf = Node::fromExpr( func ); - Debug("smt") << "isDefined function " << nf << "?" << std::endl; - return d_definedFunctions->find(nf) != d_definedFunctions->end(); -} - -void SmtEnginePrivate::finishInit() +bool SmtEngine::isDefinedFunction(Node func) { - d_preprocessingPassContext.reset( - new PreprocessingPassContext(&d_smt, &d_iteRemover, &d_propagator)); - - // initialize the preprocessing passes - d_processor.finishInit(d_preprocessingPassContext.get()); -} - -Result SmtEngine::check() { - Assert(d_fullyInited); - Assert(d_pendingPops == 0); - - Trace("smt") << "SmtEngine::check()" << endl; - - d_resourceManager->beginCall(); - - // Only way we can be out of resource is if cumulative budget is on - if (d_resourceManager->cumulativeLimitOn() && d_resourceManager->out()) - { - Result::UnknownExplanation why = d_resourceManager->outOfResources() - ? Result::RESOURCEOUT - : Result::TIMEOUT; - return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename); - } - - // Make sure the prop layer has all of the assertions - Trace("smt") << "SmtEngine::check(): processing assertions" << endl; - d_private->processAssertions(); - Trace("smt") << "SmtEngine::check(): done processing assertions" << endl; - - TimerStat::CodeTimer solveTimer(d_stats->d_solveTime); - - Chat() << "solving..." << endl; - Trace("smt") << "SmtEngine::check(): running check" << endl; - Result result = d_propEngine->checkSat(); - - d_resourceManager->endCall(); - Trace("limit") << "SmtEngine::check(): cumulative millis " - << d_resourceManager->getTimeUsage() << ", resources " - << d_resourceManager->getResourceUsage() << endl; - - return Result(result, d_filename); + Debug("smt") << "isDefined function " << func << "?" << std::endl; + return d_definedFunctions->find(func) != d_definedFunctions->end(); } Result SmtEngine::quickCheck() { - Assert(d_fullyInited); + Assert(d_state->isFullyInited()); Trace("smt") << "SMT quickCheck()" << endl; + const std::string& filename = d_state->getFilename(); return Result( - Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename); + Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename); } -theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const +Model* SmtEngine::getAvailableModel(const char* c) const { if (!options::assignFunctionValues()) { @@ -1476,7 +820,8 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const throw RecoverableModalException(ss.str().c_str()); } - if (d_smtMode != SMT_MODE_SAT && d_smtMode != SMT_MODE_SAT_UNKNOWN) + if (d_state->getMode() != SmtMode::SAT + && d_state->getMode() != SmtMode::SAT_UNKNOWN) { std::stringstream ss; ss << "Cannot " << c @@ -1492,330 +837,128 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const throw ModalException(ss.str().c_str()); } - TheoryModel* m = d_theoryEngine->getBuiltModel(); + TheoryEngine* te = d_smtSolver->getTheoryEngine(); + Assert(te != nullptr); + TheoryModel* m = te->getBuiltModel(); if (m == nullptr) { std::stringstream ss; ss << "Cannot " << c << " since model is not available. Perhaps the most recent call to " - "check-sat was interupted?"; + "check-sat was interrupted?"; throw RecoverableModalException(ss.str().c_str()); } - return m; + return d_model.get(); } -void SmtEnginePrivate::processAssertions() { - 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) { - // nothing to do - return; - } - if (d_assertionsProcessed && options::incrementalSolving()) { - // TODO(b/1255): Substitutions in incremental mode should be managed with a - // proper data structure. +void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); } - d_assertions.enableStoreSubstsInAsserts(); - } - else - { - d_assertions.disableStoreSubstsInAsserts(); - } +void SmtEngine::notifyPushPost() +{ + TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); + Assert(getPropEngine() != nullptr); + getPropEngine()->push(); +} - // process the assertions - bool noConflict = d_processor.apply(d_assertions); +void SmtEngine::notifyPopPre() +{ + TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + pe->pop(); +} - //notify theory engine new preprocessed assertions - d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() ); +void SmtEngine::notifyPostSolvePre() +{ + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + pe->resetTrail(); +} - // Push the formula to decision engine - if (noConflict) - { - Chat() << "pushing to decision engine..." << endl; - d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions); - } +void SmtEngine::notifyPostSolvePost() +{ + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->postsolve(); +} - // end: INVARIANT to maintain: no reordering of assertions or - // introducing new ones +Result SmtEngine::checkSat() +{ + Node nullNode; + return checkSat(nullNode); +} - // if incremental, compute which variables are assigned - if (options::incrementalSolving()) +Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore) +{ + if (Dump.isOn("benchmark")) { - d_preprocessingPassContext->recordSymbolsInAssertions(d_assertions.ref()); + getOutputManager().getPrinter().toStreamCmdCheckSat( + getOutputManager().getDumpOut(), assumption); } - - // Push the formula to SAT + std::vector<Node> assump; + if (!assumption.isNull()) { - 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]); - } + assump.push_back(assumption); } - - d_assertionsProcessed = true; - - d_assertions.clear(); - getIteSkolemMap().clear(); + return checkSatInternal(assump, inUnsatCore, false); } -void SmtEnginePrivate::addFormula( - TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv) +Result SmtEngine::checkSat(const std::vector<Node>& assumptions, + bool inUnsatCore) { - 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 (Dump.isOn("benchmark")) { - if (expr::hasFreeVar(n)) + if (assumptions.empty()) { - 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()); + getOutputManager().getPrinter().toStreamCmdCheckSat( + getOutputManager().getDumpOut()); } - } - - // 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()); + else + { + getOutputManager().getPrinter().toStreamCmdCheckSatAssuming( + getOutputManager().getDumpOut(), assumptions); } - ); - - // Add the normalized formula to the queue - d_assertions.push_back(n, isAssumption); - //d_assertions.push_back(Rewriter::rewrite(n)); -} - -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()); } + return checkSatInternal(assumptions, inUnsatCore, false); } -Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) +Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore) { - Dump("benchmark") << CheckSatCommand(assumption); - return checkSatisfiability(assumption, inUnsatCore, false); -} - -Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) -{ - if (assumptions.empty()) - { - Dump("benchmark") << CheckSatCommand(); - } - else + if (Dump.isOn("benchmark")) { - Dump("benchmark") << CheckSatAssumingCommand(assumptions); + getOutputManager().getPrinter().toStreamCmdQuery( + getOutputManager().getDumpOut(), node); } - - return checkSatisfiability(assumptions, inUnsatCore, false); -} - -Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore) -{ - Dump("benchmark") << QueryCommand(expr, inUnsatCore); - return checkSatisfiability( - expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr}, + return checkSatInternal( + node.isNull() ? std::vector<Node>() : std::vector<Node>{node}, inUnsatCore, true) .asEntailmentResult(); } -Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore) +Result SmtEngine::checkEntailed(const std::vector<Node>& nodes, + bool inUnsatCore) { - return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult(); + return checkSatInternal(nodes, inUnsatCore, true).asEntailmentResult(); } -Result SmtEngine::checkSatisfiability(const Expr& expr, - bool inUnsatCore, - bool isEntailmentCheck) -{ - return checkSatisfiability( - expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr}, - inUnsatCore, - isEntailmentCheck); -} - -Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, - bool inUnsatCore, - bool isEntailmentCheck) +Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions, + bool inUnsatCore, + bool isEntailmentCheck) { try { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "(" << assumptions << ")" << endl; - - if(d_queryMade && !options::incrementalSolving()) { - throw ModalException("Cannot make multiple queries unless " - "incremental solving is enabled " - "(try --incremental)"); - } - - // Note that a query has been made - d_queryMade = true; - // reset global negation - d_globalNegation = false; - - 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()) - { - 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_private->substituteAbstractValues(Node::fromExpr(e)); - // Ensure expr is type-checked at this point. - ensureBoolean(n); - - /* 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(); - - if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) - && r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - } - // flipped if we did a global negation - if (d_globalNegation) - { - Trace("smt") << "SmtEngine::process global negate " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - r = Result(Result::SAT); - } - else if (r.asSatisfiabilityResult().isSat() == Result::SAT) - { - // only if satisfaction complete - if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)) - { - r = Result(Result::UNSAT); - } - else - { - r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - } - } - Trace("smt") << "SmtEngine::global negate returned " << r << std::endl; - } - - d_needPostsolve = true; - - // Pop the context - if (didInternalPush) - { - internalPop(); - } - - // Remember the status - d_status = r; - // Check against expected status - if (!d_expectedStatus.isUnknown() && !d_status.isUnknown() - && d_status != d_expectedStatus) - { - CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got " - << d_status; - } - d_expectedStatus = Result(); - // Update the SMT mode - if (d_status.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - d_smtMode = SMT_MODE_UNSAT; - } - else if (d_status.asSatisfiabilityResult().isSat() == Result::SAT) - { - d_smtMode = SMT_MODE_SAT; - } - else - { - d_smtMode = SMT_MODE_SAT_UNKNOWN; - } + // check the satisfiability with the solver object + Result r = d_smtSolver->checkSatisfiability( + *d_asserts.get(), assumptions, inUnsatCore, isEntailmentCheck); Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat") << "(" << assumptions << ") => " << r << endl; @@ -1827,12 +970,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, checkModel(); } } - // Check that UNSAT results generate a proof correctly. - if(options::checkProofs()) { - if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - checkProof(); - } - } // Check that UNSAT results generate an unsat core correctly. if(options::checkUnsatCores()) { if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { @@ -1844,14 +981,18 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, return r; } catch (UnsafeInterruptException& e) { AlwaysAssert(d_resourceManager->out()); + // Notice that we do not notify the state of this result. If we wanted to + // make the solver resume a working state after an interupt, then we would + // implement a different callback and use it here, e.g. + // d_state.notifyCheckSatInterupt. Result::UnknownExplanation why = d_resourceManager->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; - return Result(Result::SAT_UNKNOWN, why, d_filename); + return Result(Result::SAT_UNKNOWN, why, d_state->getFilename()); } } -vector<Expr> SmtEngine::getUnsatAssumptions(void) +std::vector<Node> SmtEngine::getUnsatAssumptions(void) { Trace("smt") << "SMT getUnsatAssumptions()" << endl; SmtScope smts(this); @@ -1861,22 +1002,27 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void) "Cannot get unsat assumptions when produce-unsat-assumptions option " "is off."); } - if (d_smtMode != SMT_MODE_UNSAT) + if (d_state->getMode() != SmtMode::UNSAT) { throw RecoverableModalException( "Cannot get unsat assumptions unless immediately preceded by " "UNSAT/ENTAILED."); } - finalOptionsAreSet(); + finishInit(); if (Dump.isOn("benchmark")) { - Dump("benchmark") << GetUnsatAssumptionsCommand(); + getOutputManager().getPrinter().toStreamCmdGetUnsatAssumptions( + getOutputManager().getDumpOut()); } UnsatCore core = getUnsatCoreInternal(); - vector<Expr> res; - for (const Expr& e : d_assumptions) + std::vector<Node> res; + std::vector<Node>& 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) != core.end()) + { + res.push_back(e); + } } return res; } @@ -1884,24 +1030,20 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void) Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl; if (Dump.isOn("raw-benchmark")) { - Dump("raw-benchmark") << AssertCommand(formula.toExpr()); + getOutputManager().getPrinter().toStreamCmdAssert( + getOutputManager().getDumpOut(), formula); } // Substitute out any abstract values in ex - Node n = d_private->substituteAbstractValues(formula); + 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() */ @@ -1911,223 +1053,77 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) -------------------------------------------------------------------------- */ -void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) -{ - SmtScope smts(this); - finalOptionsAreSet(); - d_private->d_sygusVars.push_back(Node::fromExpr(var)); - Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n"; - Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type); - // don't need to set that the conjecture is stale -} - -void SmtEngine::declareSygusFunctionVar(const std::string& id, - Expr var, - Type type) +void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type) { SmtScope smts(this); - finalOptionsAreSet(); - d_private->d_sygusVars.push_back(Node::fromExpr(var)); - Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n"; - Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type); - + d_sygusSolver->declareSygusVar(id, var, type); + if (Dump.isOn("raw-benchmark")) + { + getOutputManager().getPrinter().toStreamCmdDeclareVar( + getOutputManager().getDumpOut(), var, type); + } // don't need to set that the conjecture is stale } void SmtEngine::declareSynthFun(const std::string& id, - Expr func, - Type sygusType, + Node func, + TypeNode sygusType, bool isInv, - const std::vector<Expr>& vars) + const std::vector<Node>& vars) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); - Node fn = Node::fromExpr(func); - d_private->d_sygusFunSymbols.push_back(fn); - if (!vars.empty()) - { - Expr bvl = d_exprManager->mkExpr(kind::BOUND_VAR_LIST, vars); - std::vector<Expr> attr_val_bvl; - attr_val_bvl.push_back(bvl); - setUserAttribute("sygus-synth-fun-var-list", func, attr_val_bvl, ""); - } - // whether sygus type encodes syntax restrictions - if (sygusType.isDatatype() - && static_cast<DatatypeType>(sygusType).getDatatype().isSygus()) + d_state->doPendingPops(); + d_sygusSolver->declareSynthFun(id, func, sygusType, isInv, vars); + + // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot + // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we + // must print the command using the Node-level utility method for now. + + if (Dump.isOn("raw-benchmark")) { - TypeNode stn = TypeNode::fromType(sygusType); - Node sym = d_nodeManager->mkBoundVar("sfproxy", stn); - std::vector<Expr> attr_value; - attr_value.push_back(sym.toExpr()); - setUserAttribute("sygus-synth-grammar", func, attr_value, ""); + getOutputManager().getPrinter().toStreamCmdSynthFun( + getOutputManager().getDumpOut(), + id, + vars, + func.getType().isFunction() ? func.getType().getRangeType() + : func.getType(), + isInv, + sygusType); } - Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n"; - Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars); - // sygus conjecture is now stale - setSygusConjectureStale(); } -void SmtEngine::assertSygusConstraint(Expr constraint) +void SmtEngine::assertSygusConstraint(Node constraint) { SmtScope smts(this); - finalOptionsAreSet(); - d_private->d_sygusConstraints.push_back(constraint); - - Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n"; - Dump("raw-benchmark") << SygusConstraintCommand(constraint); - // sygus conjecture is now stale - setSygusConjectureStale(); + finishInit(); + d_sygusSolver->assertSygusConstraint(constraint); + if (Dump.isOn("raw-benchmark")) + { + getOutputManager().getPrinter().toStreamCmdConstraint( + getOutputManager().getDumpOut(), constraint); + } } -void SmtEngine::assertSygusInvConstraint(const Expr& inv, - const Expr& pre, - const Expr& trans, - const Expr& post) +void SmtEngine::assertSygusInvConstraint(Node inv, + Node pre, + Node trans, + Node post) { SmtScope smts(this); - finalOptionsAreSet(); - // build invariant constraint - - // get variables (regular and their respective primed versions) - std::vector<Node> terms, vars, primed_vars; - terms.push_back(Node::fromExpr(inv)); - terms.push_back(Node::fromExpr(pre)); - terms.push_back(Node::fromExpr(trans)); - terms.push_back(Node::fromExpr(post)); - // variables are built based on the invariant type - FunctionType t = static_cast<FunctionType>(inv.getType()); - std::vector<Type> argTypes = t.getArgTypes(); - for (const Type& ti : argTypes) - { - TypeNode tn = TypeNode::fromType(ti); - vars.push_back(d_nodeManager->mkBoundVar(tn)); - d_private->d_sygusVars.push_back(vars.back()); - std::stringstream ss; - ss << vars.back() << "'"; - primed_vars.push_back(d_nodeManager->mkBoundVar(ss.str(), tn)); - d_private->d_sygusVars.push_back(primed_vars.back()); - } - - // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post - for (unsigned i = 0; i < 4; ++i) + finishInit(); + d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post); + if (Dump.isOn("raw-benchmark")) { - Node op = terms[i]; - Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op - << " with type " << op.getType() << "...\n"; - std::vector<Node> children; - children.push_back(op); - // transition relation applied over both variable lists - if (i == 2) - { - children.insert(children.end(), vars.begin(), vars.end()); - children.insert(children.end(), primed_vars.begin(), primed_vars.end()); - } - else - { - children.insert(children.end(), vars.begin(), vars.end()); - } - terms[i] = d_nodeManager->mkNode(kind::APPLY_UF, children); - // make application of Inv on primed variables - if (i == 0) - { - children.clear(); - children.push_back(op); - children.insert(children.end(), primed_vars.begin(), primed_vars.end()); - terms.push_back(d_nodeManager->mkNode(kind::APPLY_UF, children)); - } + getOutputManager().getPrinter().toStreamCmdInvConstraint( + getOutputManager().getDumpOut(), inv, pre, trans, post); } - // make constraints - std::vector<Node> conj; - conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[1], terms[0])); - Node term0_and_2 = d_nodeManager->mkNode(kind::AND, terms[0], terms[2]); - conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, term0_and_2, terms[4])); - conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[0], terms[3])); - Node constraint = d_nodeManager->mkNode(kind::AND, conj); - - d_private->d_sygusConstraints.push_back(constraint); - - Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint << "\n"; - Dump("raw-benchmark") << SygusInvConstraintCommand(inv, pre, trans, post); - // sygus conjecture is now stale - setSygusConjectureStale(); } Result SmtEngine::checkSynth() { SmtScope smts(this); - - if (options::incrementalSolving()) - { - // TODO (project #7) - throw ModalException( - "Cannot make check-synth commands when incremental solving is enabled"); - } - Expr query; - if (d_private->d_sygusConjectureStale) - { - // build synthesis conjecture from asserted constraints and declared - // variables/functions - Node sygusVar = - d_nodeManager->mkSkolem("sygus", d_nodeManager->booleanType()); - Node inst_attr = d_nodeManager->mkNode(kind::INST_ATTRIBUTE, sygusVar); - Node sygusAttr = d_nodeManager->mkNode(kind::INST_PATTERN_LIST, inst_attr); - std::vector<Node> bodyv; - Trace("smt") << "Sygus : Constructing sygus constraint...\n"; - unsigned n_constraints = d_private->d_sygusConstraints.size(); - Node body = n_constraints == 0 - ? d_nodeManager->mkConst(true) - : (n_constraints == 1 - ? d_private->d_sygusConstraints[0] - : d_nodeManager->mkNode( - kind::AND, d_private->d_sygusConstraints)); - body = body.notNode(); - Trace("smt") << "...constructed sygus constraint " << body << std::endl; - if (!d_private->d_sygusVars.empty()) - { - Node boundVars = - d_nodeManager->mkNode(kind::BOUND_VAR_LIST, d_private->d_sygusVars); - body = d_nodeManager->mkNode(kind::EXISTS, boundVars, body); - Trace("smt") << "...constructed exists " << body << std::endl; - } - if (!d_private->d_sygusFunSymbols.empty()) - { - Node boundVars = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, - d_private->d_sygusFunSymbols); - body = d_nodeManager->mkNode(kind::FORALL, boundVars, body, sygusAttr); - } - Trace("smt") << "...constructed forall " << body << std::endl; - - // set attribute for synthesis conjecture - setUserAttribute("sygus", sygusVar.toExpr(), {}, ""); - - Trace("smt") << "Check synthesis conjecture: " << body << std::endl; - Dump("raw-benchmark") << CheckSynthCommand(); - - d_private->d_sygusConjectureStale = false; - - if (options::incrementalSolving()) - { - // we push a context so that this conjecture is removed if we modify it - // later - internalPush(); - assertFormula(body, true); - } - else - { - query = body.toExpr(); - } - } - - Result r = checkSatisfiability(query, true, false); - - // Check that synthesis solutions satisfy the conjecture - if (options::checkSynthSol() - && r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - checkSynthSolution(); - } - return r; + finishInit(); + return d_sygusSolver->checkSynth(*d_asserts); } /* @@ -2136,85 +1132,42 @@ Result SmtEngine::checkSynth() -------------------------------------------------------------------------- */ -Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { - return node; -} - -Expr SmtEngine::simplify(const Expr& ex) +Node SmtEngine::simplify(const Node& ex) { - Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); - Trace("smt") << "SMT simplify(" << ex << ")" << endl; - - if(Dump.isOn("benchmark")) { - Dump("benchmark") << SimplifyCommand(ex); - } - - Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - if( options::typeChecking() ) { - e.getType(true); // ensure expr is type-checked at this point - } - - // Make sure all preprocessing is done - d_private->processAssertions(); - Node n = d_private->simplify(Node::fromExpr(e)); - n = postprocess(n, TypeNode::fromType(e.getType())); - return n.toExpr(); + finishInit(); + d_state->doPendingPops(); + // ensure we've processed assertions + d_smtSolver->processAssertions(*d_asserts); + return d_pp->simplify(ex); } Node SmtEngine::expandDefinitions(const Node& ex) { - d_private->spendResource(ResourceManager::Resource::PreprocessStep); + d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep); SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); - Trace("smt") << "SMT expandDefinitions(" << ex << ")" << endl; - - // Substitute out any abstract values in ex. - Node e = d_private->substituteAbstractValues(ex); - if(options::typeChecking()) { - // Ensure expr is type-checked at this point. - e.getType(true); - } - - unordered_map<Node, Node, NodeHashFunction> cache; - Node n = d_private->getProcessAssertions()->expandDefinitions( - e, cache, /* expandOnly = */ true); - n = postprocess(n, e.getType()); - - return n; + finishInit(); + d_state->doPendingPops(); + // set expandOnly flag to true + return d_pp->expandDefinitions(ex, true); } // TODO(#1108): Simplify the error reporting of this method. -Expr SmtEngine::getValue(const Expr& ex) const +Node SmtEngine::getValue(const Node& ex) const { - Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); Trace("smt") << "SMT getValue(" << ex << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetValueCommand(ex); + d_outMgr.getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex}); } + TypeNode expectedType = ex.getType(); - // Substitute out any abstract values in ex. - Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - - // Ensure expr is type-checked at this point. - e.getType(options::typeChecking()); + // Substitute out any abstract values in ex and expand + Node n = d_pp->expandDefinitions(ex); - // do not need to apply preprocessing substitutions (should be recorded - // in model already) - - Node n = Node::fromExpr(e); Trace("smt") << "--- getting value of " << n << endl; - TypeNode expectedType = n.getType(); - - // Expand, then normalize - unordered_map<Node, Node, NodeHashFunction> cache; - n = d_private->getProcessAssertions()->expandDefinitions(n, cache); // There are two ways model values for terms are computed (for historical // reasons). One way is that used in check-model; the other is that // used by the Model classes. It's not clear to me exactly how these @@ -2227,16 +1180,12 @@ Expr SmtEngine::getValue(const Expr& ex) const } Trace("smt") << "--- getting value of " << n << endl; - TheoryModel* m = getAvailableModel("get-value"); - Node resultNode; - if(m != NULL) { - resultNode = m->getValue(n); - } + Model* m = getAvailableModel("get-value"); + Assert(m != nullptr); + Node resultNode = m->getValue(n); Trace("smt") << "--- got value " << n << " = " << resultNode << endl; - resultNode = postprocess(resultNode, expectedType); - Trace("smt") << "--- model-post returned " << resultNode << endl; - Trace("smt") << "--- model-post returned " << resultNode.getType() << endl; - Trace("smt") << "--- model-post expected " << expectedType << endl; + Trace("smt") << "--- type " << resultNode.getType() << endl; + Trace("smt") << "--- expected type " << expectedType << endl; // type-check the result we got // Notice that lambdas have function type, which does not respect the subtype @@ -2251,171 +1200,56 @@ Expr SmtEngine::getValue(const Expr& ex) const || resultNode.isConst()); if(options::abstractValues() && resultNode.getType().isArray()) { - resultNode = d_private->mkAbstractValue(resultNode); + resultNode = d_absValues->mkAbstractValue(resultNode); Trace("smt") << "--- abstract value >> " << resultNode << endl; } - return resultNode.toExpr(); + return resultNode; } -vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs) +std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs) { - vector<Expr> result; - for (const Expr& e : exprs) + std::vector<Node> result; + for (const Node& e : exprs) { result.push_back(getValue(e)); } return result; } -bool SmtEngine::addToAssignment(const Expr& ex) { - SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); - // Substitute out any abstract values in ex - Node n = d_private->substituteAbstractValues(Node::fromExpr(ex)); - TypeNode type = n.getType(options::typeChecking()); - // must be Boolean - PrettyCheckArgument(type.isBoolean(), - n, - "expected Boolean-typed variable or function application " - "in addToAssignment()"); - // must be a defined constant, or a variable - PrettyCheckArgument( - (((d_definedFunctions->find(n) != d_definedFunctions->end()) - && n.getNumChildren() == 0) - || n.isVar()), - n, - "expected variable or defined-function application " - "in addToAssignment(),\ngot %s", - n.toString().c_str()); - if(!options::produceAssignments()) { - return false; - } - if(d_assignments == NULL) { - d_assignments = new (true) AssignmentSet(getContext()); - } - d_assignments->insert(n); - - return true; -} - -// TODO(#1108): Simplify the error reporting of this method. -vector<pair<Expr, Expr>> SmtEngine::getAssignment() -{ - Trace("smt") << "SMT getAssignment()" << endl; - SmtScope smts(this); - finalOptionsAreSet(); - if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetAssignmentCommand(); - } - if(!options::produceAssignments()) { - const char* msg = - "Cannot get the current assignment when " - "produce-assignments option is off."; - throw ModalException(msg); - } - - // Get the model here, regardless of whether d_assignments is null, since - // we should throw errors related to model availability whether or not - // assignments is null. - TheoryModel* m = getAvailableModel("get assignment"); - - vector<pair<Expr,Expr>> res; - if (d_assignments != nullptr) - { - TypeNode boolType = d_nodeManager->booleanType(); - for (AssignmentSet::key_iterator i = d_assignments->key_begin(), - iend = d_assignments->key_end(); - i != iend; - ++i) - { - Node as = *i; - Assert(as.getType() == boolType); - - Trace("smt") << "--- getting value of " << as << endl; - - // Expand, then normalize - unordered_map<Node, Node, NodeHashFunction> cache; - Node n = d_private->getProcessAssertions()->expandDefinitions(as, cache); - n = Rewriter::rewrite(n); - - Trace("smt") << "--- getting value of " << n << endl; - Node resultNode; - if (m != nullptr) - { - resultNode = m->getValue(n); - } - - // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType() == boolType); - - // ensure it's a constant - Assert(resultNode.isConst()); - - Assert(as.isVar()); - res.emplace_back(as.toExpr(), resultNode.toExpr()); - } - } - return res; -} - -void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool userVisible, const char* dumpTag) { - Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl; - SmtScope smts(this); - // If we aren't yet fully inited, the user might still turn on - // produce-models. So let's keep any commands around just in - // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares - // sort "U" in QF_UF before setLogic() is run and we still want to - // support finding card(U) with --finite-model-find, and (2) to - // decouple SmtEngine and ExprManager if the user does a few - // ExprManager::mkSort() before SmtEngine::setOption("produce-models") - // and expects to find their cardinalities in the model. - if(/* userVisible && */ - (!d_fullyInited || options::produceModels()) && - (flags & ExprManager::VAR_FLAG_DEFINED) == 0) { - if(flags & ExprManager::VAR_FLAG_GLOBAL) { - d_modelGlobalCommands.push_back(c.clone()); - } else { - d_modelCommands->push_back(c.clone()); - } - } - if(Dump.isOn(dumpTag)) { - if(d_fullyInited) { - Dump(dumpTag) << c; - } else { - d_dumpCommands.push_back(c.clone()); - } - } -} - // TODO(#1108): Simplify the error reporting of this method. Model* SmtEngine::getModel() { Trace("smt") << "SMT getModel()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetModelCommand(); + getOutputManager().getPrinter().toStreamCmdGetModel( + getOutputManager().getDumpOut()); } - TheoryModel* m = getAvailableModel("get model"); + Model* m = getAvailableModel("get model"); // Since model m is being returned to the user, we must ensure that this // model object remains valid with future check-sat calls. Hence, we set // the theory engine into "eager model building" mode. TODO #2648: revisit. - d_theoryEngine->setEagerModelBuilding(); + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->setEagerModelBuilding(); if (options::modelCoresMode() != options::ModelCoresMode::NONE) { // If we enabled model cores, we compute a model core for m based on our // (expanded) assertions using the model core builder utility - std::vector<Expr> eassertsProc = getExpandedAssertions(); - ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode()); - } - m->d_inputName = d_filename; - m->d_isKnownSat = (d_smtMode == SMT_MODE_SAT); + std::vector<Node> eassertsProc = getExpandedAssertions(); + ModelCoreBuilder::setModelCore( + eassertsProc, m->getTheoryModel(), options::modelCoresMode()); + } + // set the information on the SMT-level model + Assert(m != nullptr); + m->d_inputName = d_state->getFilename(); + m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT); return m; } @@ -2424,55 +1258,57 @@ Result SmtEngine::blockModel() Trace("smt") << "SMT blockModel()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if (Dump.isOn("benchmark")) { - Dump("benchmark") << BlockModelCommand(); + getOutputManager().getPrinter().toStreamCmdBlockModel( + getOutputManager().getDumpOut()); } - TheoryModel* m = getAvailableModel("block model"); + Model* m = getAvailableModel("block model"); if (options::blockModelsMode() == options::BlockModelsMode::NONE) { std::stringstream ss; ss << "Cannot block model when block-models is set to none."; - throw ModalException(ss.str().c_str()); + throw RecoverableModalException(ss.str().c_str()); } // get expanded assertions - std::vector<Expr> eassertsProc = getExpandedAssertions(); - Expr eblocker = ModelBlocker::getModelBlocker( - eassertsProc, m, options::blockModelsMode()); - return assertFormula(Node::fromExpr(eblocker)); + std::vector<Node> eassertsProc = getExpandedAssertions(); + Node eblocker = ModelBlocker::getModelBlocker( + eassertsProc, m->getTheoryModel(), options::blockModelsMode()); + return assertFormula(eblocker); } -Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs) +Result SmtEngine::blockModelValues(const std::vector<Node>& exprs) { Trace("smt") << "SMT blockModelValues()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); - PrettyCheckArgument( - !exprs.empty(), - "block model values must be called on non-empty set of terms"); if (Dump.isOn("benchmark")) { - Dump("benchmark") << BlockModelValuesCommand(exprs); + getOutputManager().getPrinter().toStreamCmdBlockModelValues( + getOutputManager().getDumpOut(), exprs); } - TheoryModel* m = getAvailableModel("block model values"); + Model* m = getAvailableModel("block model values"); // get expanded assertions - std::vector<Expr> eassertsProc = getExpandedAssertions(); + std::vector<Node> eassertsProc = getExpandedAssertions(); // we always do block model values mode here - Expr eblocker = ModelBlocker::getModelBlocker( - eassertsProc, m, options::BlockModelsMode::VALUES, exprs); - return assertFormula(Node::fromExpr(eblocker)); + Node eblocker = + ModelBlocker::getModelBlocker(eassertsProc, + m->getTheoryModel(), + options::BlockModelsMode::VALUES, + exprs); + return assertFormula(eblocker); } -std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void) +std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void) { if (!d_logic.isTheoryEnabled(THEORY_SEP)) { @@ -2482,74 +1318,60 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void) throw RecoverableModalException(msg); } NodeManagerScope nms(d_nodeManager); - Expr heap; - Expr nil; + Node heap; + Node nil; Model* m = getAvailableModel("get separation logic heap and nil"); - if (!m->getHeapModel(heap, nil)) + TheoryModel* tm = m->getTheoryModel(); + if (!tm->getHeapModel(heap, nil)) { - InternalError() - << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil " - "expressions from theory model."; + const char* msg = + "Failed to obtain heap/nil " + "expressions from theory model."; + throw RecoverableModalException(msg); } return std::make_pair(heap, nil); } -std::vector<Expr> SmtEngine::getExpandedAssertions() +std::vector<Node> SmtEngine::getExpandedAssertions() { - std::vector<Expr> easserts = getAssertions(); + std::vector<Node> easserts = getAssertions(); // must expand definitions - std::vector<Expr> eassertsProc; + std::vector<Node> eassertsProc; std::unordered_map<Node, Node, NodeHashFunction> cache; - for (const Expr& e : easserts) + for (const Node& e : easserts) { - Node ea = Node::fromExpr(e); - Node eae = d_private->getProcessAssertions()->expandDefinitions(ea, cache); - eassertsProc.push_back(eae.toExpr()); + Node eae = d_pp->expandDefinitions(e, cache); + eassertsProc.push_back(eae); } return eassertsProc; } -Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } - -Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } - -void SmtEngine::checkProof() +void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT) { -#if (IS_LFSC_BUILD && IS_PROOFS_BUILD) - - Chat() << "generating proof..." << endl; - - const Proof& pf = getProof(); - - Chat() << "checking proof..." << endl; - - std::string logicString = d_logic.getLogicString(); - - std::stringstream pfStream; - - pfStream << proof::plf_signatures << endl; - int64_t sizeBeforeProof = static_cast<int64_t>(pfStream.tellp()); - - pf.toStream(pfStream); - d_stats->d_proofsSize += - static_cast<int64_t>(pfStream.tellp()) - sizeBeforeProof; - + if (!d_logic.isTheoryEnabled(THEORY_SEP)) { - TimerStat::CodeTimer checkProofTimer(d_stats->d_lfscCheckProofTime); - lfscc_init(); - lfscc_check_file(pfStream, false, false, false, false, false, false, false); + const char* msg = + "Cannot declare heap if not using the separation logic theory."; + throw RecoverableModalException(msg); } - // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup - // segfaults on regress0/bv/core/bitvec7.smt - // lfscc_cleanup(); + SmtScope smts(this); + finishInit(); + TheoryEngine* te = getTheoryEngine(); + te->declareSepHeap(locT, dataT); +} -#else /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */ - Unreachable() - << "This version of CVC4 was built without proof support; cannot check " - "proofs."; -#endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */ +bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT) +{ + SmtScope smts(this); + finishInit(); + TheoryEngine* te = getTheoryEngine(); + return te->getSepHeapTypes(locT, dataT); } +Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } + +Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } + UnsatCore SmtEngine::getUnsatCoreInternal() { #if IS_PROOFS_BUILD @@ -2558,7 +1380,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() throw ModalException( "Cannot get an unsat core when produce-unsat-cores option is off."); } - if (d_smtMode != SMT_MODE_UNSAT) + if (d_state->getMode() != SmtMode::UNSAT) { throw RecoverableModalException( "Cannot get an unsat core unless immediately preceded by " @@ -2566,7 +1388,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() } d_proofManager->traceUnsatCore(); // just to trigger core creation - return UnsatCore(this, d_proofManager->extractUnsatCore()); + return UnsatCore(d_proofManager->extractUnsatCore()); #else /* IS_PROOFS_BUILD */ throw ModalException( "This build of CVC4 doesn't have proof support (required for unsat " @@ -2581,27 +1403,29 @@ void SmtEngine::checkUnsatCore() { Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; UnsatCore core = getUnsatCore(); - SmtEngine coreChecker(d_exprManager, &d_options); - coreChecker.setIsInternalSubsolver(); - coreChecker.setLogic(getLogicInfo()); - coreChecker.getOptions().set(options::checkUnsatCores, false); - coreChecker.getOptions().set(options::checkProofs, false); + // initialize the core checker + std::unique_ptr<SmtEngine> coreChecker; + initializeSubsolver(coreChecker); + coreChecker->getOptions().set(options::checkUnsatCores, false); - PROOF( - std::vector<Command*>::const_iterator itg = d_defineCommands.begin(); - for (; itg != d_defineCommands.end(); ++itg) { - (*itg)->invoke(&coreChecker); + // set up separation logic heap if necessary + TypeNode sepLocType, sepDataType; + if (getSepHeapTypes(sepLocType, sepDataType)) + { + coreChecker->declareSepHeap(sepLocType, sepDataType); } - ); - Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl; + Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions" + << std::endl; for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { - Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl; - coreChecker.assertFormula(Node::fromExpr(*i)); + Node assertionAfterExpansion = expandDefinitions(*i); + Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i + << ", expanded to " << assertionAfterExpansion << "\n"; + coreChecker->assertFormula(assertionAfterExpansion); } Result r; try { - r = coreChecker.checkSat(); + r = coreChecker->checkSat(); } catch(...) { throw; } @@ -2619,543 +1443,93 @@ void SmtEngine::checkUnsatCore() { } void SmtEngine::checkModel(bool hardFailure) { + context::CDList<Node>* 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); - // Throughout, we use Notice() to give diagnostic output. - // - // If this function is running, the user gave --check-model (or equivalent), - // and if Notice() is on, the user gave --verbose (or equivalent). - Notice() << "SmtEngine::checkModel(): generating model" << endl; - TheoryModel* m = getAvailableModel("check model"); - - // check-model is not guaranteed to succeed if approximate values were used. - // Thus, we intentionally abort here. - if (m->hasApproximations()) - { - throw RecoverableModalException( - "Cannot run check-model on a model with approximate values."); - } - - // Check individual theory assertions - if (options::debugCheckModels()) - { - d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure); - } - - // Output the model - Notice() << *m; - - // We have a "fake context" for the substitution map (we don't need it - // to be context-dependent) - context::Context fakeContext; - SubstitutionMap substitutions(&fakeContext, /* substituteUnderQuantifiers = */ false); - - for(size_t k = 0; k < m->getNumCommands(); ++k) { - const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k)); - Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl; - if(c == NULL) { - // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ... - Notice() << "SmtEngine::checkModel(): skipping..." << endl; - } else { - // We have a DECLARE-FUN: - // - // We'll first do some checks, then add to our substitution map - // the mapping: function symbol |-> value - - Expr func = c->getFunction(); - Node val = m->getValue(func); - - Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl; - - // (1) if the value is a lambda, ensure the lambda doesn't contain the - // function symbol (since then the definition is recursive) - if (val.getKind() == kind::LAMBDA) { - // first apply the model substitutions we have so far - Debug("boolean-terms") << "applying subses to " << val[1] << endl; - Node n = substitutions.apply(val[1]); - Debug("boolean-terms") << "++ got " << n << endl; - // now check if n contains func by doing a substitution - // [func->func2] and checking equality of the Nodes. - // (this just a way to check if func is in n.) - SubstitutionMap subs(&fakeContext); - Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY); - subs.addSubstitution(func, func2); - if(subs.apply(n) != n) { - Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl; - stringstream ss; - ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl - << "considering model value for " << func << endl - << "body of lambda is: " << val << endl; - if(n != val[1]) { - ss << "body substitutes to: " << n << endl; - } - ss << "so " << func << " is defined in terms of itself." << endl - << "Run with `--check-models -v' for additional diagnostics."; - InternalError() << ss.str(); - } - } - - // (2) check that the value is actually a value - else if (!val.isConst()) - { - // This is only a warning since it could have been assigned an - // unevaluable term (e.g. an application of a transcendental function). - // This parallels the behavior (warnings for non-constant expressions) - // when checking whether assertions are satisfied below. - Warning() << "Warning : SmtEngine::checkModel(): " - << "model value for " << func << endl - << " is " << val << endl - << "and that is not a constant (.isConst() == false)." - << std::endl - << "Run with `--check-models -v' for additional diagnostics." - << std::endl; - } - - // (3) check that it's the correct (sub)type - // This was intended to be a more general check, but for now we can't do that because - // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.). - else if(func.getType().isInteger() && !val.getType().isInteger()) { - Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl; - InternalError() - << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH " - "MODEL:" - << endl - << "model value for " << func << endl - << " is " << val << endl - << "value type is " << val.getType() << endl - << "should be of type " << func.getType() << endl - << "Run with `--check-models -v' for additional diagnostics."; - } - - // (4) checks complete, add the substitution - Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl; - substitutions.addSubstitution(func, val); - } - } - - // Now go through all our user assertions checking if they're satisfied. - for (const Node& assertion : *d_assertionList) - { - Notice() << "SmtEngine::checkModel(): checking assertion " << assertion - << endl; - Node n = assertion; - - // Apply any define-funs from the problem. - { - unordered_map<Node, Node, NodeHashFunction> cache; - n = d_private->getProcessAssertions()->expandDefinitions(n, cache); - } - Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl; - - // Apply our model value substitutions. - Debug("boolean-terms") << "applying subses to " << n << endl; - n = substitutions.apply(n); - Debug("boolean-terms") << "++ got " << n << endl; - Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl; - - // We look up the value before simplifying. If n contains quantifiers, - // this may increases the chance of finding its value before the node is - // altered by simplification below. - n = m->getValue(n); - Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl; - - // Simplify the result. - n = d_private->simplify(n); - Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl; - - // Replace the already-known ITEs (this is important for ground ITEs under quantifiers). - n = d_private->d_iteRemover.replace(n); - Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl; - - // Apply our model value substitutions (again), as things may have been simplified. - Debug("boolean-terms") << "applying subses to " << n << endl; - n = substitutions.apply(n); - Debug("boolean-terms") << "++ got " << n << endl; - Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n << endl; - - // As a last-ditch effort, ask model to simplify it. - // Presently, this is only an issue for quantifiers, which can have a value - // but don't show up in our substitution map above. - n = m->getValue(n); - Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl; - - if (n.isConst()) - { - if (n.getConst<bool>()) - { - // assertion is true, everything is fine - continue; - } - } - - // Otherwise, we did not succeed in showing the current assertion to be - // true. This may either indicate that our model is wrong, or that we cannot - // check it. The latter may be the case for several reasons. - // For example, quantified formulas are not checkable, although we assign - // them to true/false based on the satisfying assignment. However, - // quantified formulas can be modified during preprocess, so they may not - // correspond to those in the satisfying assignment. Hence we throw - // warnings for assertions that do not simplify to either true or false. - // Other theories such as non-linear arithmetic (in particular, - // transcendental functions) also have the property of not being able to - // be checked precisely here. - // Note that warnings like these can be avoided for quantified formulas - // by making preprocessing passes explicitly record how they - // rewrite quantified formulas (see cvc4-wishues#43). - if (!n.isConst()) - { - // Not constant, print a less severe warning message here. - Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified " - "assertion : " - << n << endl; - continue; - } - // Assertions that simplify to false result in an InternalError or - // Warning being thrown below (when hardFailure is false). - Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" - << endl; - stringstream ss; - ss << "SmtEngine::checkModel(): " - << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl - << "assertion: " << assertion << endl - << "simplifies to: " << n << endl - << "expected `true'." << endl - << "Run with `--check-models -v' for additional diagnostics."; - if (hardFailure) - { - // internal error if hardFailure is true - InternalError() << ss.str(); - } - else - { - Warning() << ss.str() << endl; - } - } - Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; -} - -void SmtEngine::checkSynthSolution() -{ - NodeManager* nm = NodeManager::currentNM(); - Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl; - std::map<Node, std::map<Node, Node>> sol_map; - /* Get solutions and build auxiliary vectors for substituting */ - if (!d_theoryEngine->getSynthSolutions(sol_map)) - { - InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!"; - return; - } - if (sol_map.empty()) - { - InternalError() << "SmtEngine::checkSynthSolution(): Got empty solution!"; - return; - } - Trace("check-synth-sol") << "Got solution map:\n"; - // the set of synthesis conjectures in our assertions - std::unordered_set<Node, NodeHashFunction> conjs; - // For each of the above conjectures, the functions-to-synthesis and their - // solutions. This is used as a substitution below. - std::map<Node, std::vector<Node>> fvarMap; - std::map<Node, std::vector<Node>> fsolMap; - for (const std::pair<const Node, std::map<Node, Node>>& cmap : sol_map) - { - Trace("check-synth-sol") << "For conjecture " << cmap.first << ":\n"; - conjs.insert(cmap.first); - std::vector<Node>& fvars = fvarMap[cmap.first]; - std::vector<Node>& fsols = fsolMap[cmap.first]; - for (const std::pair<const Node, Node>& pair : cmap.second) - { - Trace("check-synth-sol") - << " " << pair.first << " --> " << pair.second << "\n"; - fvars.push_back(pair.first); - fsols.push_back(pair.second); - } - } - Trace("check-synth-sol") << "Starting new SMT Engine\n"; - /* Start new SMT engine to check solutions */ - SmtEngine solChecker(d_exprManager, &d_options); - solChecker.setIsInternalSubsolver(); - solChecker.setLogic(getLogicInfo()); - solChecker.getOptions().set(options::checkSynthSol, false); - solChecker.getOptions().set(options::sygusRecFun, false); + Model* m = getAvailableModel("check model"); + Assert(m != nullptr); - Trace("check-synth-sol") << "Retrieving assertions\n"; - // Build conjecture from original assertions - if (d_assertionList == NULL) - { - Trace("check-synth-sol") << "No assertions to check\n"; - return; - } - // auxiliary assertions - std::vector<Node> auxAssertions; - // expand definitions cache - std::unordered_map<Node, Node, NodeHashFunction> cache; - for (const Node& assertion : *d_assertionList) - { - Notice() << "SmtEngine::checkSynthSolution(): checking assertion " - << assertion << endl; - Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n"; - // Apply any define-funs from the problem. - Node n = - d_private->getProcessAssertions()->expandDefinitions(assertion, cache); - Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << n << endl; - Trace("check-synth-sol") << "Expanded assertion " << n << "\n"; - if (conjs.find(n) == conjs.end()) - { - Trace("check-synth-sol") << "It is an auxiliary assertion\n"; - auxAssertions.push_back(n); - } - else - { - Trace("check-synth-sol") << "It is a synthesis conjecture\n"; - } - } - // check all conjectures - for (const Node& conj : conjs) - { - // get the solution for this conjecture - std::vector<Node>& fvars = fvarMap[conj]; - std::vector<Node>& fsols = fsolMap[conj]; - // Apply solution map to conjecture body - Node conjBody; - /* Whether property is quantifier free */ - if (conj[1].getKind() != kind::EXISTS) - { - conjBody = conj[1].substitute( - fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); - } - else - { - conjBody = conj[1][1].substitute( - fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); - - /* Skolemize property */ - std::vector<Node> vars, skos; - for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j) - { - vars.push_back(conj[1][0][j]); - std::stringstream ss; - ss << "sk_" << j; - skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType())); - Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to " - << skos.back() << "\n"; - } - conjBody = conjBody.substitute( - vars.begin(), vars.end(), skos.begin(), skos.end()); - } - Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to " - << conjBody << endl; - Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody - << "\n"; - solChecker.assertFormula(conjBody); - // Assert all auxiliary assertions. This may include recursive function - // definitions that were added as assertions to the sygus problem. - for (const Node& a : auxAssertions) - { - solChecker.assertFormula(a); - } - Result r = solChecker.checkSat(); - Notice() << "SmtEngine::checkSynthSolution(): result is " << r << endl; - Trace("check-synth-sol") << "Satsifiability check: " << r << "\n"; - if (r.asSatisfiabilityResult().isUnknown()) - { - InternalError() << "SmtEngine::checkSynthSolution(): could not check " - "solution, result " - "unknown."; - } - else if (r.asSatisfiabilityResult().isSat()) - { - InternalError() - << "SmtEngine::checkSynthSolution(): produced solution leads to " - "satisfiable negated conjecture."; - } - solChecker.resetAssertions(); - } -} - -void SmtEngine::checkInterpol(Expr interpol, - const std::vector<Expr>& easserts, - const Node& conj) -{ -} - -void SmtEngine::checkAbduct(Node a) -{ - Assert(a.getType().isBoolean()); - // check it with the abduction solver - return d_abductSolver->checkAbduct(a); + // check the model with the check models utility + Assert(d_checkModels != nullptr); + d_checkModels->checkModel(m, al, hardFailure); } // TODO(#1108): Simplify the error reporting of this method. UnsatCore SmtEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetUnsatCoreCommand(); + getOutputManager().getPrinter().toStreamCmdGetUnsatCore( + getOutputManager().getDumpOut()); } return getUnsatCoreInternal(); } -// TODO(#1108): Simplify the error reporting of this method. -const Proof& SmtEngine::getProof() -{ - Trace("smt") << "SMT getProof()" << endl; - SmtScope smts(this); - finalOptionsAreSet(); - if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetProofCommand(); - } -#if IS_PROOFS_BUILD - if(!options::proof()) { - throw ModalException("Cannot get a proof when produce-proofs option is off."); - } - if (d_smtMode != SMT_MODE_UNSAT) - { - throw RecoverableModalException( - "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED " - "response."); - } - - return ProofManager::getProof(this); -#else /* IS_PROOFS_BUILD */ - throw ModalException("This build of CVC4 doesn't have proof support."); -#endif /* IS_PROOFS_BUILD */ -} - void SmtEngine::printInstantiations( std::ostream& out ) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if (options::instFormatMode() == options::InstFormatMode::SZS) { - out << "% SZS output start Proof for " << d_filename.c_str() << std::endl; - } - if( d_theoryEngine ){ - d_theoryEngine->printInstantiations( out ); - }else{ - Assert(false); + out << "% SZS output start Proof for " << d_state->getFilename() + << std::endl; } + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->printInstantiations(out); if (options::instFormatMode() == options::InstFormatMode::SZS) { - out << "% SZS output end Proof for " << d_filename.c_str() << std::endl; + out << "% SZS output end Proof for " << d_state->getFilename() << std::endl; } } void SmtEngine::printSynthSolution( std::ostream& out ) { SmtScope smts(this); - finalOptionsAreSet(); - if( d_theoryEngine ){ - d_theoryEngine->printSynthSolution( out ); - }else{ - Assert(false); - } + finishInit(); + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->printSynthSolution(out); } -bool SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map) +bool SmtEngine::getSynthSolutions(std::map<Node, Node>& solMap) { SmtScope smts(this); - finalOptionsAreSet(); - std::map<Node, std::map<Node, Node>> sol_mapn; - Assert(d_theoryEngine != nullptr); - // fail if the theory engine does not have synthesis solutions - if (!d_theoryEngine->getSynthSolutions(sol_mapn)) - { - return false; - } - for (std::pair<const Node, std::map<Node, Node>>& cs : sol_mapn) - { - for (std::pair<const Node, Node>& s : cs.second) - { - sol_map[s.first.toExpr()] = s.second.toExpr(); - } - } - return true; + finishInit(); + return d_sygusSolver->getSynthSolutions(solMap); } -Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) +Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } - Trace("smt-qe") << "Do quantifier elimination " << e << std::endl; - Node n_e = Node::fromExpr( e ); - if (n_e.getKind() != kind::EXISTS && n_e.getKind() != kind::FORALL) - { - throw ModalException( - "Expecting a quantified formula as argument to get-qe."); - } - //tag the quantified formula with the quant-elim attribute - TypeNode t = NodeManager::currentNM()->booleanType(); - Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr."); - std::vector< Node > node_values; - d_theoryEngine->setUserAttribute( doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, ""); - n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr); - n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr); - std::vector< Node > e_children; - e_children.push_back( n_e[0] ); - e_children.push_back(n_e.getKind() == kind::EXISTS ? n_e[1] - : n_e[1].negate()); - e_children.push_back( n_attr ); - Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children ); - Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl; - Assert(nn_e.getNumChildren() == 3); - Result r = checkSatisfiability(nn_e.toExpr(), true, true); - Trace("smt-qe") << "Query returned " << r << std::endl; - if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) { - if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){ - Notice() - << "While performing quantifier elimination, unexpected result : " - << r << " for query."; - // failed, return original - return e; - } - std::vector< Node > inst_qs; - d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs ); - Assert(inst_qs.size() <= 1); - Node ret_n; - if( inst_qs.size()==1 ){ - Node top_q = inst_qs[0]; - //Node top_q = Rewriter::rewrite( nn_e ).negate(); - Assert(top_q.getKind() == kind::FORALL); - Trace("smt-qe") << "Get qe for " << top_q << std::endl; - ret_n = d_theoryEngine->getInstantiatedConjunction( top_q ); - Trace("smt-qe") << "Returned : " << ret_n << std::endl; - if (n_e.getKind() == kind::EXISTS) - { - ret_n = Rewriter::rewrite(ret_n.negate()); - } - }else{ - ret_n = NodeManager::currentNM()->mkConst(n_e.getKind() != kind::EXISTS); - } - // do extended rewrite to minimize the size of the formula aggressively - theory::quantifiers::ExtendedRewriter extr(true); - ret_n = extr.extendedRewrite(ret_n); - return ret_n.toExpr(); - }else { - return NodeManager::currentNM() - ->mkConst(n_e.getKind() == kind::EXISTS) - .toExpr(); - } + return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull); } -bool SmtEngine::getInterpol(const Expr& conj, - const Type& grammarType, - Expr& interpol) +bool SmtEngine::getInterpol(const Node& conj, + const TypeNode& grammarType, + Node& interpol) { - return false; + SmtScope smts(this); + finishInit(); + bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol); + // notify the state of whether the get-interpol call was successfuly, which + // impacts the SMT mode. + d_state->notifyGetInterpol(success); + return success; } -bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol) +bool SmtEngine::getInterpol(const Node& conj, Node& interpol) { - Type grammarType; + TypeNode grammarType; return getInterpol(conj, grammarType, interpol); } @@ -3163,15 +1537,13 @@ bool SmtEngine::getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd) { - if (d_abductSolver->getAbduct(conj, grammarType, abd)) - { - // successfully generated an abduct, update to abduct state - d_smtMode = SMT_MODE_ABDUCT; - return true; - } - // failed, we revert to the assert state - d_smtMode = SMT_MODE_ASSERT; - return false; + SmtScope smts(this); + finishInit(); + bool success = d_abductSolver->getAbduct(conj, grammarType, abd); + // notify the state of whether the get-abduct call was successfuly, which + // impacts the SMT mode. + d_state->notifyGetAbduct(success); + return success; } bool SmtEngine::getAbduct(const Node& conj, Node& abd) @@ -3180,56 +1552,31 @@ bool SmtEngine::getAbduct(const Node& conj, Node& abd) return getAbduct(conj, grammarType, abd); } -void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) { +void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) +{ SmtScope smts(this); - if( d_theoryEngine ){ - std::vector< Node > qs_n; - d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n ); - for( unsigned i=0; i<qs_n.size(); i++ ){ - qs.push_back( qs_n[i].toExpr() ); - } - }else{ - Assert(false); - } + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->getInstantiatedQuantifiedFormulas(qs); } -void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) { - SmtScope smts(this); - if( d_theoryEngine ){ - std::vector< Node > insts_n; - d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n ); - for( unsigned i=0; i<insts_n.size(); i++ ){ - insts.push_back( insts_n[i].toExpr() ); - } - }else{ - Assert(false); - } -} - -void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) { +void SmtEngine::getInstantiationTermVectors( + Node q, std::vector<std::vector<Node>>& tvecs) +{ SmtScope smts(this); - Assert(options::trackInstLemmas()); - if( d_theoryEngine ){ - std::vector< std::vector< Node > > tvecs_n; - d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n ); - for( unsigned i=0; i<tvecs_n.size(); i++ ){ - std::vector< Expr > tvec; - for( unsigned j=0; j<tvecs_n[i].size(); j++ ){ - tvec.push_back( tvecs_n[i][j].toExpr() ); - } - tvecs.push_back( tvec ); - } - }else{ - Assert(false); - } + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->getInstantiationTermVectors(q, tvecs); } -vector<Expr> SmtEngine::getAssertions() { +std::vector<Node> SmtEngine::getAssertions() +{ SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetAssertionsCommand(); + getOutputManager().getPrinter().toStreamCmdGetAssertions( + getOutputManager().getDumpOut()); } Trace("smt") << "SMT getAssertions()" << endl; if(!options::produceAssertions()) { @@ -3237,11 +1584,12 @@ vector<Expr> SmtEngine::getAssertions() { "Cannot query the current assertion list when not in produce-assertions mode."; throw ModalException(msg); } - Assert(d_assertionList != NULL); - std::vector<Expr> res; - for (const Node& n : *d_assertionList) + context::CDList<Node>* al = d_asserts->getAssertionList(); + Assert(al != nullptr); + std::vector<Node> res; + for (const Node& n : *al) { - res.emplace_back(n.toExpr()); + res.emplace_back(n); } // copy the result out return res; @@ -3250,188 +1598,102 @@ vector<Expr> SmtEngine::getAssertions() { void SmtEngine::push() { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); Trace("smt") << "SMT push()" << endl; - d_private->notifyPush(); - d_private->processAssertions(); + d_smtSolver->processAssertions(*d_asserts); if(Dump.isOn("benchmark")) { - Dump("benchmark") << PushCommand(); - } - if(!options::incrementalSolving()) { - throw ModalException("Cannot push when not solving incrementally (use --incremental)"); + getOutputManager().getPrinter().toStreamCmdPush( + getOutputManager().getDumpOut()); } - - - // 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_userLevels.push_back(d_userContext->getLevel()); - internalPush(); - Trace("userpushpop") << "SmtEngine: pushed to level " - << d_userContext->getLevel() << endl; + d_state->userPush(); } void SmtEngine::pop() { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); Trace("smt") << "SMT pop()" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << PopCommand(); - } - if(!options::incrementalSolving()) { - throw ModalException("Cannot pop when not solving incrementally (use --incremental)"); + getOutputManager().getPrinter().toStreamCmdPop( + getOutputManager().getDumpOut()); } - if(d_userLevels.size() == 0) { - throw ModalException("Cannot pop beyond the first user frame"); - } - - // The problem isn't really "extended" yet, but this disallows - // get-model after a pop, simplifying our lives somewhat. It might - // not be strictly necessary to do so, since the pops occur lazily, - // 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(); - - AlwaysAssert(d_userContext->getLevel() > 0); - AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); - while (d_userLevels.back() < d_userContext->getLevel()) { - internalPop(true); - } - d_userLevels.pop_back(); + d_state->userPop(); // Clear out assertion queues etc., in case anything is still in there - d_private->notifyPop(); + d_asserts->clearCurrent(); + // clear the learned literals from the preprocessor + d_pp->clearLearnedLiterals(); Trace("userpushpop") << "SmtEngine: popped to level " - << d_userContext->getLevel() << endl; - // FIXME: should we reset d_status here? + << getUserContext()->getLevel() << endl; + // should we reset d_status here? // SMT-LIBv2 spec seems to imply no, but it would make sense to.. } -void SmtEngine::internalPush() { - Assert(d_fullyInited); - Trace("smt") << "SmtEngine::internalPush()" << endl; - doPendingPops(); - if(options::incrementalSolving()) { - d_private->processAssertions(); - TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); - d_userContext->push(); - // the d_context push is done inside of the SAT solver - d_propEngine->push(); - } -} - -void SmtEngine::internalPop(bool immediate) { - Assert(d_fullyInited); - Trace("smt") << "SmtEngine::internalPop()" << endl; - if(options::incrementalSolving()) { - ++d_pendingPops; - } - if(immediate) { - doPendingPops(); - } -} - -void SmtEngine::doPendingPops() { - Trace("smt") << "SmtEngine::doPendingPops()" << endl; - Assert(d_pendingPops == 0 || options::incrementalSolving()); - // check to see if a postsolve() is pending - if (d_needPostsolve) - { - d_propEngine->resetTrail(); - } - while(d_pendingPops > 0) { - TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); - d_propEngine->pop(); - // the d_context pop is done inside of the SAT solver - d_userContext->pop(); - --d_pendingPops; - } - if (d_needPostsolve) - { - d_theoryEngine->postsolve(); - d_needPostsolve = false; - } -} - void SmtEngine::reset() { SmtScope smts(this); ExprManager *em = d_exprManager; Trace("smt") << "SMT reset()" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << ResetCommand(); + getOutputManager().getPrinter().toStreamCmdReset( + getOutputManager().getDumpOut()); } + std::string filename = d_state->getFilename(); Options opts; opts.copyValues(d_originalOptions); this->~SmtEngine(); new (this) SmtEngine(em, &opts); + // Restore data set after creation + notifyStartParsing(filename); } void SmtEngine::resetAssertions() { SmtScope smts(this); - if (!d_fullyInited) + if (!d_state->isFullyInited()) { // We're still in Start Mode, nothing asserted yet, do nothing. // (see solver execution modes in the SMT-LIB standard) - Assert(d_context->getLevel() == 0); - Assert(d_userContext->getLevel() == 0); - DeleteAndClearCommandVector(d_modelGlobalCommands); + Assert(getContext()->getLevel() == 0); + Assert(getUserContext()->getLevel() == 0); + d_dumpm->resetAssertions(); return; } - doPendingPops(); Trace("smt") << "SMT resetAssertions()" << endl; if (Dump.isOn("benchmark")) { - Dump("benchmark") << ResetAssertionsCommand(); - } - - while (!d_userLevels.empty()) - { - pop(); + getOutputManager().getPrinter().toStreamCmdResetAssertions( + getOutputManager().getDumpOut()); } - // Remember the global push/pop around everything when beyond Start mode - // (see solver execution modes in the SMT-LIB standard) - Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1); - d_context->popto(0); - d_userContext->popto(0); - DeleteAndClearCommandVector(d_modelGlobalCommands); - d_userContext->push(); - d_context->push(); + d_asserts->clearCurrent(); + d_state->notifyResetAssertions(); + d_dumpm->resetAssertions(); + // push the state to maintain global context around everything + d_state->setup(); - /* Create new PropEngine. - * First force destruction of referenced PropEngine to enforce that - * statistics are unregistered by the obsolete PropEngine object before - * registered again by the new PropEngine object */ - d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - getTheoryEngine(), getContext(), getUserContext(), getResourceManager())); - d_theoryEngine->setPropEngine(getPropEngine()); + d_smtSolver->resetAssertions(); } void SmtEngine::interrupt() { - if(!d_fullyInited) { + if (!d_state->isFullyInited()) + { return; } - d_propEngine->interrupt(); - d_theoryEngine->interrupt(); + d_smtSolver->interrupt(); } void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { d_resourceManager->setResourceLimit(units, cumulative); } -void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) { - d_resourceManager->setTimeLimit(milis, cumulative); +void SmtEngine::setTimeLimit(unsigned long milis) +{ + d_resourceManager->setTimeLimit(milis); } unsigned long SmtEngine::getResourceUsage() const { @@ -3447,11 +1709,6 @@ unsigned long SmtEngine::getResourceRemaining() const return d_resourceManager->getResourceRemaining(); } -unsigned long SmtEngine::getTimeRemaining() const -{ - return d_resourceManager->getTimeRemaining(); -} - NodeManager* SmtEngine::getNodeManager() const { return d_exprManager->getNodeManager(); @@ -3477,52 +1734,32 @@ void SmtEngine::setUserAttribute(const std::string& attr, const std::string& str_value) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); std::vector<Node> node_values; - for( unsigned i=0; i<expr_values.size(); i++ ){ + for (std::size_t i = 0, n = expr_values.size(); i < n; i++) + { node_values.push_back( expr_values[i].getNode() ); } - d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value); -} - -void SmtEngine::setPrintFuncInModel(Expr f, bool p) { - Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl; - for( unsigned i=0; i<d_modelGlobalCommands.size(); i++ ){ - Command * c = d_modelGlobalCommands[i]; - DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c); - if(dfc != NULL) { - if( dfc->getFunction()==f ){ - dfc->setPrintInModel( p ); - } - } - } - for( unsigned i=0; i<d_modelCommands->size(); i++ ){ - Command * c = (*d_modelCommands)[i]; - DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c); - if(dfc != NULL) { - if( dfc->getFunction()==f ){ - dfc->setPrintInModel( p ); - } - } - } -} - -void SmtEngine::beforeSearch() -{ - if(d_fullyInited) { - throw ModalException( - "SmtEngine::beforeSearch called after initialization."); - } + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->setUserAttribute(attr, expr.getNode(), node_values, str_value); } - void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) { + // Always check whether the SmtEngine has been initialized (which is done + // upon entering Assert mode the first time). No option can be set after + // initialized. + if (d_state->isFullyInited()) + { + throw ModalException("SmtEngine::setOption called after initialization."); + } NodeManagerScope nms(d_nodeManager); Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << SetOptionCommand(key, value); + getOutputManager().getPrinter().toStreamCmdSetOption( + getOutputManager().getDumpOut(), key, value); } if(key == "command-verbosity") { @@ -3575,7 +1812,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const } if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetOptionCommand(key); + d_outMgr.getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key); } if(key == "command-verbosity") { @@ -3610,15 +1847,6 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const return SExpr::parseAtom(d_options.getOption(key)); } -bool SmtEngine::getExpressionName(Expr e, std::string& name) const { - return d_private->getExpressionName(e, name); -} - -void SmtEngine::setExpressionName(Expr e, const std::string& name) { - Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl; - d_private->setExpressionName(e,name); -} - Options& SmtEngine::getOptions() { return d_options; } const Options& SmtEngine::getOptions() const { return d_options; } @@ -3628,18 +1856,13 @@ ResourceManager* SmtEngine::getResourceManager() return d_resourceManager.get(); } -void SmtEngine::setSygusConjectureStale() +DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); } + +const Printer* SmtEngine::getPrinter() const { - if (d_private->d_sygusConjectureStale) - { - // already stale - return; - } - d_private->d_sygusConjectureStale = true; - if (options::incrementalSolving()) - { - internalPop(); - } + return Printer::getPrinter(d_options[options::outputLanguage]); } +OutputManager& SmtEngine::getOutputManager() { return d_outMgr; } + }/* CVC4 namespace */ |