From 956ffda5632b388a887003a5e030696091339bd2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 6 Aug 2020 08:29:17 -0500 Subject: [PATCH] Split preprocessor from SmtEngine (#4854) This splits a collection of utilities from SmtEngine that work in cooperation to preprocess assertions (Boolean circuit propagator, preprocessing context, process assertions, term formula removal). It updates various interfaces in SmtEngine from Expr -> Node and simplifies SmtEngine to use this utility. --- src/CMakeLists.txt | 2 + src/api/cvc4cpp.cpp | 2 +- src/printer/cvc/cvc_printer.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 3 +- src/smt/command.cpp | 2 +- src/smt/preprocessor.cpp | 156 +++++++++++ src/smt/preprocessor.h | 138 ++++++++++ src/smt/process_assertions.h | 8 +- src/smt/smt_engine.cpp | 258 ++++-------------- src/smt/smt_engine.h | 30 +- .../candidate_rewrite_database.cpp | 2 +- .../sygus/cegis_core_connective.cpp | 2 +- .../quantifiers/sygus/sygus_repair_const.cpp | 2 +- src/theory/smt_engine_subsolver.cpp | 4 +- src/theory/theory_model.cpp | 2 +- 15 files changed, 383 insertions(+), 230 deletions(-) create mode 100644 src/smt/preprocessor.cpp create mode 100644 src/smt/preprocessor.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 92f197252..6bbc2d29b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -249,6 +249,8 @@ libcvc4_add_sources( smt/model_blocker.h smt/options_manager.cpp smt/options_manager.h + smt/preprocessor.cpp + smt/preprocessor.h smt/preprocess_proof_generator.cpp smt/preprocess_proof_generator.h smt/process_assertions.cpp diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 0963c704b..e69c9a1de 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4952,7 +4952,7 @@ Term Solver::getValue(Term term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); - return Term(this, d_smtEngine->getValue(term.d_node->toExpr())); + return Term(this, d_smtEngine->getValue(*term.d_node)); CVC4_API_SOLVER_TRY_CATCH_END; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 900651e1d..9ec522141 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1185,7 +1185,7 @@ void DeclareFunctionCommandToStream(std::ostream& out, { out << tn; } - Node val = Node::fromExpr(model.getSmtEngine()->getValue(n.toExpr())); + Node val = model.getSmtEngine()->getValue(n); if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE) { TypeNode type_node = val[1].getType(); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 45cc2426c..7560b2ce4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1455,8 +1455,7 @@ void Smt2Printer::toStream(std::ostream& out, // don't print out internal stuff return; } - Node val = - Node::fromExpr(theory_model->getSmtEngine()->getValue(n.toExpr())); + Node val = theory_model->getSmtEngine()->getValue(n); if (val.getKind() == kind::LAMBDA) { out << "(define-fun " << n << " " << val[0] << " " diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 52a9578dd..4d8f6d910 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1509,7 +1509,7 @@ void SimplifyCommand::invoke(SmtEngine* smtEngine) { try { - d_result = smtEngine->simplify(d_term); + d_result = smtEngine->simplify(Node::fromExpr(d_term)).toExpr(); d_commandStatus = CommandSuccess::instance(); } catch (UnsafeInterruptException& e) diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp new file mode 100644 index 000000000..ea5ef2bad --- /dev/null +++ b/src/smt/preprocessor.cpp @@ -0,0 +1,156 @@ +/********************* */ +/*! \file preprocessor.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The preprocessor of the SMT engine. + **/ + +#include "smt/preprocessor.h" + +#include "options/smt_options.h" +#include "smt/abstract_values.h" +#include "smt/assertions.h" +#include "smt/command.h" +#include "smt/smt_engine.h" + +using namespace CVC4::theory; +using namespace CVC4::kind; + +namespace CVC4 { +namespace smt { + +Preprocessor::Preprocessor(SmtEngine& smt, + context::UserContext* u, + AbstractValues& abs) + : d_smt(smt), + d_absValues(abs), + d_propagator(true, true), + d_assertionsProcessed(u, false), + d_processor(smt, *smt.getResourceManager()), + d_rtf(u) +{ +} + +Preprocessor::~Preprocessor() +{ + if (d_propagator.getNeedsFinish()) + { + d_propagator.finish(); + d_propagator.setNeedsFinish(false); + } +} + +void Preprocessor::finishInit() +{ + d_ppContext.reset(new preprocessing::PreprocessingPassContext( + &d_smt, &d_rtf, &d_propagator)); + + // initialize the preprocessing passes + d_processor.finishInit(d_ppContext.get()); +} + +bool Preprocessor::process(Assertions& as) +{ + preprocessing::AssertionPipeline& ap = as.getAssertionPipeline(); + + // should not be called if empty + Assert(ap.size() != 0) << "Can only preprocess a non-empty list of assertions"; + + if (d_assertionsProcessed && options::incrementalSolving()) + { + // TODO(b/1255): Substitutions in incremental mode should be managed with a + // proper data structure. + ap.enableStoreSubstsInAsserts(); + } + else + { + ap.disableStoreSubstsInAsserts(); + } + + // process the assertions, return true if no conflict is discovered + return d_processor.apply(as); +} + +void Preprocessor::postprocess(Assertions& as) +{ + preprocessing::AssertionPipeline& ap = as.getAssertionPipeline(); + // if incremental, compute which variables are assigned + if (options::incrementalSolving()) + { + d_ppContext->recordSymbolsInAssertions(ap.ref()); + } + + // mark that we've processed assertions + d_assertionsProcessed = true; +} + +void Preprocessor::clearLearnedLiterals() +{ + d_propagator.getLearnedLiterals().clear(); +} + +void Preprocessor::cleanup() { d_processor.cleanup(); } + +RemoveTermFormulas& Preprocessor::getTermFormulaRemover() { return d_rtf; } + +Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly) +{ + std::unordered_map cache; + return expandDefinitions(n, cache, expandOnly); +} + +Node Preprocessor::expandDefinitions( + const Node& node, + std::unordered_map& cache, + bool expandOnly) +{ + Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl; + // Substitute out any abstract values in node. + Node n = d_absValues.substituteAbstractValues(node); + if (options::typeChecking()) + { + // Ensure node is type-checked at this point. + n.getType(true); + } + // expand only = true + return d_processor.expandDefinitions(n, cache, expandOnly); +} + +Node Preprocessor::simplify(const Node& node, bool removeItes) +{ + Trace("smt") << "SMT simplify(" << node << ")" << endl; + if (Dump.isOn("benchmark")) + { + Dump("benchmark") << SimplifyCommand(node.toExpr()); + } + Node nas = d_absValues.substituteAbstractValues(node); + if (options::typeChecking()) + { + // ensure node is type-checked at this point + nas.getType(true); + } + std::unordered_map cache; + Node n = d_processor.expandDefinitions(nas, cache); + Node ns = applySubstitutions(n); + if (removeItes) + { + // also remove ites if asked + ns = d_rtf.replace(ns); + } + return ns; +} + +Node Preprocessor::applySubstitutions(TNode node) +{ + return Rewriter::rewrite(d_ppContext->getTopLevelSubstitutions().apply(node)); +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h new file mode 100644 index 000000000..051fe8bee --- /dev/null +++ b/src/smt/preprocessor.h @@ -0,0 +1,138 @@ +/********************* */ +/*! \file preprocessor.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The preprocessor of the SmtEngine. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__PREPROCESSOR_H +#define CVC4__SMT__PREPROCESSOR_H + +#include + +#include "preprocessing/preprocessing_pass_context.h" +#include "smt/process_assertions.h" +#include "smt/term_formula_removal.h" +#include "theory/booleans/circuit_propagator.h" + +namespace CVC4 { +namespace smt { + +class AbstractValues; + +/** + * The preprocessor module of an SMT engine. + * + * This class is responsible for: + * (1) preprocessing the set of assertions from input before they are sent to + * the SMT solver, + * (2) implementing methods for expanding and simplifying formulas. The latter + * takes into account the substitutions inferred by this class. + */ +class Preprocessor +{ + public: + Preprocessor(SmtEngine& smt, context::UserContext* u, AbstractValues& abs); + ~Preprocessor(); + /** + * Finish initialization + */ + void finishInit(); + /** + * Process the assertions that have been asserted in argument as. Returns + * true if no conflict was discovered while preprocessing them. + */ + bool process(Assertions& as); + /** + * Postprocess assertions, called after the SmtEngine has finished + * giving the assertions to the SMT solver and before the assertions are + * cleared. + */ + void postprocess(Assertions& as); + /** + * Clear learned literals from the Boolean propagator. + */ + void clearLearnedLiterals(); + /** + * Cleanup, which deletes the processing passes owned by this module. This + * is required to be done explicitly so that passes are deleted before the + * objects they refer to in the SmtEngine destructor. + */ + void cleanup(); + /** + * Simplify a formula without doing "much" work. Does not involve + * the SAT Engine in the simplification, but uses the current + * definitions, assertions, and the current partial model, if one + * has been constructed. It also involves theory normalization. + * + * @param n The node to simplify + * @param removeItes Whether to remove ITE (and other terms with formulas in + * term positions) from the result. + * @return The simplified term. + */ + Node simplify(const Node& n, bool removeItes = false); + /** + * Expand the definitions in a term or formula n. No other + * simplification or normalization is done. + * + * @param n The node to expand + * @param expandOnly if true, then the expandDefinitions function of + * TheoryEngine is not called on subterms of n. + * @return The expanded term. + */ + Node expandDefinitions(const Node& n, bool expandOnly = false); + /** Same as above, with a cache of previous results. */ + Node expandDefinitions( + const Node& n, + std::unordered_map& cache, + bool expandOnly = false); + /** + * Get the underlying term formula remover utility. + */ + RemoveTermFormulas& getTermFormulaRemover(); + + private: + /** + * Apply substitutions that have been inferred by preprocessing, return the + * substituted form of node. + */ + Node applySubstitutions(TNode node); + /** Reference to the parent SmtEngine */ + SmtEngine& d_smt; + /** Reference to the abstract values utility */ + AbstractValues& d_absValues; + /** + * A circuit propagator for non-clausal propositional deduction. + */ + theory::booleans::CircuitPropagator d_propagator; + /** + * User-context-dependent flag of whether any assertions have been processed. + */ + context::CDO d_assertionsProcessed; + /** The preprocessing pass context */ + std::unique_ptr d_ppContext; + /** + * Process assertions module, responsible for implementing the preprocessing + * passes. + */ + ProcessAssertions d_processor; + /** + * The term formula remover, responsible for eliminating formulas that occur + * in term contexts. + */ + RemoveTermFormulas d_rtf; +}; + +} // namespace smt +} // namespace CVC4 + +#endif diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index 2a7efe1c0..b34682914 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -77,9 +77,11 @@ class ProcessAssertions /** * Expand definitions in term n. Return the expanded form of n. * - * If expandOnly is true, then the expandDefinitions function of TheoryEngine - * of the SmtEngine this calls is associated with is not called on subterms of - * n. + * @param n The node to expand + * @param cache Cache of previous results + * @param expandOnly if true, then the expandDefinitions function of + * TheoryEngine is not called on subterms of n. + * @return The expanded term. */ Node expandDefinitions(TNode n, NodeToNodeHashMap& cache, diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 43aa3b0c8..585c2819d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -83,16 +83,16 @@ #include "smt/abduction_solver.h" #include "smt/abstract_values.h" #include "smt/assertions.h" -#include "smt/expr_names.h" #include "smt/command.h" #include "smt/defined_function.h" #include "smt/dump_manager.h" +#include "smt/expr_names.h" #include "smt/listeners.h" #include "smt/logic_request.h" #include "smt/model_blocker.h" #include "smt/model_core_builder.h" #include "smt/options_manager.h" -#include "smt/process_assertions.h" +#include "smt/preprocessor.h" #include "smt/smt_engine_scope.h" #include "smt/smt_engine_stats.h" #include "smt/term_formula_removal.h" @@ -155,31 +155,8 @@ namespace smt { */ class SmtEnginePrivate { - SmtEngine& d_smt; - - typedef unordered_map NodeToNodeHashMap; - typedef unordered_map NodeToBoolHashMap; - - /** A circuit propagator for non-clausal propositional deduction */ - booleans::CircuitPropagator d_propagator; - - /** Whether any assertions have been processed */ - CDO d_assertionsProcessed; - - // Cached true value - Node d_true; - - /** The preprocessing pass context */ - std::unique_ptr d_preprocessingPassContext; - - /** Process assertions module */ - ProcessAssertions d_processor; - public: - /** Instance of the ITE remover */ - RemoveTermFormulas d_iteRemover; - /* Finishes the initialization of the private portion of SMTEngine. */ void finishInit(); @@ -203,66 +180,12 @@ class SmtEnginePrivate public: SmtEnginePrivate(SmtEngine& smt) - : d_smt(smt), - d_propagator(true, true), - d_assertionsProcessed(smt.getUserContext(), false), - d_processor(smt, *smt.getResourceManager()), - d_iteRemover(smt.getUserContext()), - d_sygusConjectureStale(smt.getUserContext(), true) + : d_sygusConjectureStale(smt.getUserContext(), true) { - d_true = NodeManager::currentNM()->mkConst(true); } ~SmtEnginePrivate() { - if(d_propagator.getNeedsFinish()) { - d_propagator.finish(); - d_propagator.setNeedsFinish(false); - } - } - - void spendResource(ResourceManager::Resource r) - { - d_smt.getResourceManager()->spendResource(r); - } - - ProcessAssertions* getProcessAssertions() { return &d_processor; } - - Node applySubstitutions(TNode node) - { - return Rewriter::rewrite( - d_preprocessingPassContext->getTopLevelSubstitutions().apply(node)); - } - - /** - * Process the assertions that have been asserted. - */ - void processAssertions(Assertions& as); - - /** 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_propagator.getLearnedLiterals().clear(); - } - /** - * 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(); - return applySubstitutions(n).toExpr(); } };/* class SmtEnginePrivate */ @@ -302,6 +225,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_statisticsRegistry(nullptr), d_stats(nullptr), d_resourceManager(nullptr), + d_optm(nullptr), + d_pp(nullptr), d_scope(nullptr) { // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine @@ -327,6 +252,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_resourceManager.reset( new ResourceManager(*d_statisticsRegistry.get(), d_options)); d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get())); + d_pp.reset( + new smt::Preprocessor(*this, d_userContext.get(), *d_absValues.get())); d_private.reset(new smt::SmtEnginePrivate(*this)); // listen to node manager events d_nodeManager->subscribeEvents(d_snmListener.get()); @@ -370,7 +297,7 @@ void SmtEngine::finishInit() d_theoryEngine.reset(new TheoryEngine(getContext(), getUserContext(), getResourceManager(), - d_private->d_iteRemover, + d_pp->getTermFormulaRemover(), const_cast(d_logic))); // Add the theories @@ -435,7 +362,7 @@ void SmtEngine::finishInit() finishRegisterTheory(d_theoryEngine->theoryOf(id)); } }); - d_private->finishInit(); + d_pp->finishInit(); Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; } @@ -495,7 +422,7 @@ SmtEngine::~SmtEngine() 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 @@ -522,6 +449,7 @@ SmtEngine::~SmtEngine() 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); @@ -990,15 +918,6 @@ bool SmtEngine::isDefinedFunction( Expr func ){ return d_definedFunctions->find(nf) != d_definedFunctions->end(); } -void SmtEnginePrivate::finishInit() -{ - 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); @@ -1017,7 +936,7 @@ Result SmtEngine::check() { // Make sure the prop layer has all of the assertions Trace("smt") << "SmtEngine::check(): processing assertions" << endl; - d_private->processAssertions(*d_asserts); + processAssertionsInternal(); Trace("smt") << "SmtEngine::check(): done processing assertions" << endl; TimerStat::CodeTimer solveTimer(d_stats->d_solveTime); @@ -1080,68 +999,52 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const return m; } -void SmtEnginePrivate::processAssertions(Assertions& as) +void SmtEngine::processAssertionsInternal() { - TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); - spendResource(ResourceManager::Resource::PreprocessStep); - Assert(d_smt.d_fullyInited); - Assert(d_smt.d_pendingPops == 0); + TimerStat::CodeTimer paTimer(d_stats->d_processAssertionsTime); + d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep); + Assert(d_fullyInited); + Assert(d_pendingPops == 0); - AssertionPipeline& ap = as.getAssertionPipeline(); + AssertionPipeline& ap = d_asserts->getAssertionPipeline(); if (ap.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. - - ap.enableStoreSubstsInAsserts(); - } - else - { - ap.disableStoreSubstsInAsserts(); - } - // process the assertions - bool noConflict = d_processor.apply(as); + // process the assertions with the preprocessor + bool noConflict = d_pp->process(*d_asserts); //notify theory engine new preprocessed assertions - d_smt.d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); + d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); // Push the formula to decision engine if (noConflict) { Chat() << "pushing to decision engine..." << endl; - d_smt.d_propEngine->addAssertionsToDecisionEngine(ap); + d_propEngine->addAssertionsToDecisionEngine(ap); } // end: INVARIANT to maintain: no reordering of assertions or // introducing new ones - // if incremental, compute which variables are assigned - if (options::incrementalSolving()) - { - d_preprocessingPassContext->recordSymbolsInAssertions(ap.ref()); - } + d_pp->postprocess(*d_asserts); // Push the formula to SAT { Chat() << "converting to CNF..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime); + TimerStat::CodeTimer codeTimer(d_stats->d_cnfConversionTime); for (const Node& assertion : ap.ref()) { Chat() << "+ " << assertion << std::endl; - d_smt.d_propEngine->assertFormula(assertion); + d_propEngine->assertFormula(assertion); } } - d_assertionsProcessed = true; - // clear the current assertions - as.clearCurrent(); + d_asserts->clearCurrent(); } Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) @@ -1617,85 +1520,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_absValues->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(*d_asserts); - Node n = d_private->simplify(Node::fromExpr(e)); - n = postprocess(n, TypeNode::fromType(e.getType())); - return n.toExpr(); + // ensure we've processed assertions + processAssertionsInternal(); + 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_absValues->substituteAbstractValues(ex); - if(options::typeChecking()) { - // Ensure expr is type-checked at this point. - e.getType(true); - } - - unordered_map cache; - Node n = d_private->getProcessAssertions()->expandDefinitions( - e, cache, /* expandOnly = */ true); - n = postprocess(n, e.getType()); - - return n; + // 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); + Dump("benchmark") << GetValueCommand(ex.toExpr()); } + TypeNode expectedType = ex.getType(); - // Substitute out any abstract values in ex. - Expr e = d_absValues->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - - // Ensure expr is type-checked at this point. - e.getType(options::typeChecking()); - - // do not need to apply preprocessing substitutions (should be recorded - // in model already) + // Substitute out any abstract values in ex and expand + Node n = d_pp->expandDefinitions(ex); - Node n = Node::fromExpr(e); Trace("smt") << "--- getting value of " << n << endl; - TypeNode expectedType = n.getType(); - - // Expand, then normalize - unordered_map 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 @@ -1714,10 +1574,8 @@ Expr SmtEngine::getValue(const Expr& ex) const 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 @@ -1736,7 +1594,7 @@ Expr SmtEngine::getValue(const Expr& ex) const Trace("smt") << "--- abstract value >> " << resultNode << endl; } - return resultNode.toExpr(); + return resultNode; } vector SmtEngine::getValues(const vector& exprs) @@ -1744,7 +1602,7 @@ vector SmtEngine::getValues(const vector& exprs) vector result; for (const Expr& e : exprs) { - result.push_back(getValue(e)); + result.push_back(getValue(e).toExpr()); } return result; } @@ -1817,8 +1675,8 @@ vector> SmtEngine::getAssignment() Trace("smt") << "--- getting value of " << as << endl; // Expand, then normalize - unordered_map cache; - Node n = d_private->getProcessAssertions()->expandDefinitions(as, cache); + std::unordered_map cache; + Node n = d_pp->expandDefinitions(as, cache); n = Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; @@ -1955,7 +1813,7 @@ std::vector SmtEngine::getExpandedAssertions() for (const Expr& e : easserts) { Node ea = Node::fromExpr(e); - Node eae = d_private->getProcessAssertions()->expandDefinitions(ea, cache); + Node eae = d_pp->expandDefinitions(ea, cache); eassertsProc.push_back(eae.toExpr()); } return eassertsProc; @@ -2208,7 +2066,7 @@ void SmtEngine::checkModel(bool hardFailure) { // Apply any define-funs from the problem. { unordered_map cache; - n = d_private->getProcessAssertions()->expandDefinitions(n, cache); + n = d_pp->expandDefinitions(n, cache); } Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl; @@ -2224,13 +2082,12 @@ void SmtEngine::checkModel(bool hardFailure) { 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; + // Simplify the result and replace the already-known ITEs (this is important + // for ground ITEs under quantifiers). + n = d_pp->simplify(n, true); + Notice() + << "SmtEngine::checkModel(): -- simplifies with ite replacement to " + << n << endl; // Apply our model value substitutions (again), as things may have been simplified. Debug("boolean-terms") << "applying subses to " << n << endl; @@ -2362,8 +2219,7 @@ void SmtEngine::checkSynthSolution() << 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); + Node n = d_pp->expandDefinitions(assertion, cache); Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << n << endl; Trace("check-synth-sol") << "Expanded assertion " << n << "\n"; if (conjs.find(n) == conjs.end()) @@ -2714,8 +2570,7 @@ void SmtEngine::push() finalOptionsAreSet(); doPendingPops(); Trace("smt") << "SMT push()" << endl; - d_private->notifyPush(); - d_private->processAssertions(*d_asserts); + processAssertionsInternal(); if(Dump.isOn("benchmark")) { Dump("benchmark") << PushCommand(); } @@ -2766,7 +2621,8 @@ void SmtEngine::pop() { // Clear out assertion queues etc., in case anything is still in there d_asserts->clearCurrent(); - d_private->notifyPop(); + // clear the learned literals from the preprocessor + d_pp->clearLearnedLiterals(); Trace("userpushpop") << "SmtEngine: popped to level " << d_userContext->getLevel() << endl; @@ -2779,7 +2635,7 @@ void SmtEngine::internalPush() { Trace("smt") << "SmtEngine::internalPush()" << endl; doPendingPops(); if(options::incrementalSolving()) { - d_private->processAssertions(*d_asserts); + processAssertionsInternal(); TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); d_userContext->push(); // the d_context push is done inside of the SAT solver diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5dc0d74fa..3ae04a720 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -99,6 +99,7 @@ class DumpManager; class ResourceOutListener; class SmtNodeManagerListener; class OptionsManager; +class Preprocessor; /** Subsolvers */ class AbductionSolver; /** @@ -506,7 +507,7 @@ class CVC4_PUBLIC SmtEngine * @todo (design) is this meant to give an equivalent or an * equisatisfiable formula? */ - Expr simplify(const Expr& e); + Node simplify(const Node& e); /** * Expand the definitions in a term or formula. No other @@ -524,7 +525,7 @@ class CVC4_PUBLIC SmtEngine * @throw ModalException, TypeCheckingException, LogicException, * UnsafeInterruptException */ - Expr getValue(const Expr& e) const; + Node getValue(const Node& e) const; /** * Same as getValue but for a vector of expressions @@ -986,13 +987,6 @@ class CVC4_PUBLIC SmtEngine */ void checkAbduct(Node a); - /** - * Postprocess a value for output to the user. Involves doing things - * like turning datatypes back into tuples, length-1-bitvectors back - * into booleans, etc. - */ - Node postprocess(TNode n, TypeNode expectedType) const; - /** * This is something of an "init" procedure, but is idempotent; call * as often as you like. Should be called whenever the final options @@ -1052,6 +1046,14 @@ class CVC4_PUBLIC SmtEngine */ void setLogicInternal(); + /** + * Process the assertions that have been asserted. This moves the set of + * assertions that have been buffered into the smt::Assertions object, + * preprocesses them, pushes them into the SMT solver, and clears the + * buffer. + */ + void processAssertionsInternal(); + /** * Add to Model command. This is used for recording a command * that should be reported during a get-model call. @@ -1197,12 +1199,6 @@ class CVC4_PUBLIC SmtEngine */ bool d_needPostsolve; - /* - * Whether to call theory preprocessing during simplification - on - * by default* but gets turned off if arithRewriteEq is on - */ - bool d_earlyTheoryPP; - /** * Most recent result of last checkSatisfiability/checkEntailed or * (set-info :status). @@ -1247,6 +1243,10 @@ class CVC4_PUBLIC SmtEngine * for set default options based on the logic. */ std::unique_ptr d_optm; + /** + * The preprocessor. + */ + std::unique_ptr d_pp; /** * The global scope object. Upon creation of this SmtEngine, it becomes the * SmtEngine in scope. It says the SmtEngine in scope until it is destructed, diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 835dc1dba..07d798901 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -172,7 +172,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol, if (val.isNull()) { Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE); - val = Node::fromExpr(rrChecker->getValue(refv.toExpr())); + val = rrChecker->getValue(refv); } Trace("rr-check") << " " << v << " -> " << val << std::endl; pt.push_back(val); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index a7f32155c..9126aad94 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -597,7 +597,7 @@ void CegisCoreConnective::getModel(SmtEngine& smt, { for (const Node& v : d_vars) { - Node mv = Node::fromExpr(smt.getValue(v.toExpr())); + Node mv = smt.getValue(v); Trace("sygus-ccore-model") << v << " -> " << mv << " "; vals.push_back(mv); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 2514b05e2..5ceac24b6 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -250,7 +250,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, { Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end()); Node fov = d_sk_to_fo[v]; - Node fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr())); + Node fov_m = repcChecker->getValue(fov); Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl; // convert to sygus Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m); diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 2419962aa..8810acbe8 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -112,8 +112,8 @@ Result checkWithSubsolver(Node query, { for (const Node& v : vars) { - Expr val = smte->getValue(v.toExpr()); - modelVals.push_back(Node::fromExpr(val)); + Node val = smte->getValue(v); + modelVals.push_back(val); } } return r; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 70f46d6e5..4c7600da2 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -174,7 +174,7 @@ bool TheoryModel::isModelCoreSymbol(Expr sym) const Expr TheoryModel::getValue( Expr expr ) const{ Node n = Node::fromExpr( expr ); Node ret = getValue( n ); - return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr(); + return ret.toExpr(); } /** get cardinality for sort */ -- 2.30.2