From cd1a8023502b0d6d268dafd22328d06840d04324 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Oct 2020 08:17:34 -0500 Subject: [PATCH] Split CheckModels utility to its own file (#5303) This utility will be undergoing major additions to make it more robust. Thus it should be moved to its own file. There are no major code changes in this PR, a few things were changed to be consistent to the coding standard. --- src/CMakeLists.txt | 2 + src/smt/check_models.cpp | 271 +++++++++++++++++++++++++++++++++++++++ src/smt/check_models.h | 52 ++++++++ src/smt/smt_engine.cpp | 263 +------------------------------------ src/smt/smt_engine.h | 6 + src/smt/smt_solver.cpp | 2 + src/smt/smt_solver.h | 2 + 7 files changed, 342 insertions(+), 256 deletions(-) create mode 100644 src/smt/check_models.cpp create mode 100644 src/smt/check_models.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ec8aaf8dc..29f5a57d4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -208,6 +208,8 @@ libcvc4_add_sources( smt/abstract_values.h smt/assertions.cpp smt/assertions.h + smt/check_models.cpp + smt/check_models.h smt/command.cpp smt/command.h smt/defined_function.h diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp new file mode 100644 index 000000000..a55f53f96 --- /dev/null +++ b/src/smt/check_models.cpp @@ -0,0 +1,271 @@ +/********************* */ +/*! \file check_models.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 Utility for constructing and maintaining abstract values. + **/ + +#include "smt/check_models.h" + +#include "options/smt_options.h" +#include "smt/node_command.h" +#include "smt/preprocessor.h" +#include "theory/rewriter.h" +#include "theory/substitutions.h" +#include "theory/theory_engine.h" + +using namespace CVC4::theory; + +namespace CVC4 { +namespace smt { + +CheckModels::CheckModels(SmtSolver& s) : d_smt(s) {} +CheckModels::~CheckModels() {} + +void CheckModels::checkModel(Model* m, + context::CDList* al, + bool hardFailure) +{ + // 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). + + // 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()) + { + TheoryEngine* te = d_smt.getTheoryEngine(); + Assert(te != nullptr); + te->checkTheoryAssertionsWithModel(hardFailure); + } + + // Output the model + Notice() << *m; + + NodeManager* nm = NodeManager::currentNM(); + Preprocessor* pp = d_smt.getPreprocessor(); + + // 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); + + Trace("check-model") << "checkModel: Collect substitution..." << std::endl; + for (size_t k = 0, ncmd = m->getNumCommands(); k < ncmd; ++k) + { + const DeclareFunctionNodeCommand* c = + dynamic_cast(m->getCommand(k)); + Notice() << "SmtEngine::checkModel(): model command " << k << " : " + << m->getCommand(k)->toString() << std::endl; + if (c == nullptr) + { + // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ... + Notice() << "SmtEngine::checkModel(): skipping..." << std::endl; + continue; + } + // We have a DECLARE-FUN: + // + // We'll first do some checks, then add to our substitution map + // the mapping: function symbol |-> value + + Node func = c->getFunction(); + Node val = m->getValue(func); + + Notice() << "SmtEngine::checkModel(): adding substitution: " << func + << " |-> " << val << std::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 + Node n = substitutions.apply(val[1]); + // 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 = + nm->mkSkolem("", 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 ***" + << std::endl; + std::stringstream ss; + ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH " + "MODEL:" + << std::endl + << "considering model value for " << func << std::endl + << "body of lambda is: " << val << std::endl; + if (n != val[1]) + { + ss << "body substitutes to: " << n << std::endl; + } + ss << "so " << func << " is defined in terms of itself." << std::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 << std::endl + << " is " << val << std::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 ***" + << std::endl; + InternalError() + << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH " + "MODEL:" + << std::endl + << "model value for " << func << std::endl + << " is " << val << std::endl + << "value type is " << val.getType() << std::endl + << "should be of type " << func.getType() << std::endl + << "Run with `--check-models -v' for additional diagnostics."; + } + + // (4) checks complete, add the substitution + Trace("check-model") << "Substitution: " << func << " :=> " << val + << std::endl; + substitutions.addSubstitution(func, val); + } + + Trace("check-model") << "checkModel: Check assertions..." << std::endl; + std::unordered_map cache; + // Now go through all our user assertions checking if they're satisfied. + for (const Node& assertion : *al) + { + Notice() << "SmtEngine::checkModel(): checking assertion " << assertion + << std::endl; + Node n = assertion; + Node nr = Rewriter::rewrite(substitutions.apply(n)); + if (nr.isConst() && nr.getConst()) + { + continue; + } + // Apply any define-funs from the problem. + n = pp->expandDefinitions(n, cache); + Notice() << "SmtEngine::checkModel(): -- expands to " << n << std::endl; + + // Apply our model value substitutions. + n = substitutions.apply(n); + Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << std::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 and replace the already-known ITEs (this is important + // for ground ITEs under quantifiers). + n = pp->simplify(n, true); + Notice() + << "SmtEngine::checkModel(): -- simplifies with ite replacement to " + << n << std::endl; + + // Apply our model value substitutions (again), as things may have been + // simplified. + n = substitutions.apply(n); + Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n + << std::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 + << std::endl; + + if (n.isConst() && n.getConst()) + { + // 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 << std::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' ***" + << std::endl; + std::stringstream ss; + ss << "SmtEngine::checkModel(): " + << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << std::endl + << "assertion: " << assertion << std::endl + << "simplifies to: " << n << std::endl + << "expected `true'." << std::endl + << "Run with `--check-models -v' for additional diagnostics."; + if (hardFailure) + { + // internal error if hardFailure is true + InternalError() << ss.str(); + } + else + { + Warning() << ss.str() << std::endl; + } + } + Trace("check-model") << "checkModel: Finish" << std::endl; + Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" + << std::endl; +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/check_models.h b/src/smt/check_models.h new file mode 100644 index 000000000..14af41b27 --- /dev/null +++ b/src/smt/check_models.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file check_models.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 Utility for checking models + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__CHECK_MODELS_H +#define CVC4__SMT__CHECK_MODELS_H + +#include "context/cdlist.h" +#include "expr/node.h" +#include "smt/model.h" +#include "smt/smt_solver.h" + +namespace CVC4 { +namespace smt { + +/** + * This utility is responsible for checking the current model. + */ +class CheckModels +{ + public: + CheckModels(SmtSolver& s); + ~CheckModels(); + /** + * Check model m against the current set of input assertions al. + * + * This throws an exception if we fail to verify that m is a proper model + * given assertion list al based on the model checking policy. + */ + void checkModel(Model* m, context::CDList* al, bool hardFailure); + + private: + /** Reference to the SMT solver */ + SmtSolver& d_smt; +}; + +} // namespace smt +} // namespace CVC4 + +#endif diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2f9918486..343b79966 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -16,19 +16,6 @@ #include "smt/smt_engine.h" -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - #include "api/cvc4cpp.h" #include "base/check.h" #include "base/configuration.h" @@ -36,41 +23,25 @@ #include "base/exception.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/base_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/prop_options.h" -#include "options/quantifiers_options.h" #include "options/set_language.h" #include "options/smt_options.h" #include "options/theory_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_manager.h" #include "proof/unsat_core.h" #include "smt/abduction_solver.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/expr_names.h" @@ -91,16 +62,10 @@ #include "smt/sygus_solver.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/logic_info.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/rewriter.h" -#include "theory/sort_inference.h" -#include "theory/substitutions.h" #include "theory/theory_engine.h" -#include "theory/theory_model.h" -#include "theory/theory_traits.h" #include "util/hash.h" #include "util/random.h" #include "util/resource_manager.h" @@ -128,6 +93,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_smtSolver(nullptr), d_proofManager(nullptr), d_model(nullptr), + d_checkModels(nullptr), d_pfManager(nullptr), d_rewriter(new theory::Rewriter()), d_definedFunctions(nullptr), @@ -282,6 +248,8 @@ void SmtEngine::finishInit() 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 @@ -1557,229 +1525,13 @@ void SmtEngine::checkModel(bool hardFailure) { 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; Model* m = getAvailableModel("check model"); Assert(m != nullptr); - // 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()) - { - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - te->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 DeclareFunctionNodeCommand* c = - dynamic_cast(m->getCommand(k)); - Notice() << "SmtEngine::checkModel(): model command " << k << " : " - << m->getCommand(k)->toString() << 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 - - Node 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( - "", 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 : *al) - { - Notice() << "SmtEngine::checkModel(): checking assertion " << assertion - << endl; - Node n = assertion; - Node nr = Rewriter::rewrite(substitutions.apply(n)); - Trace("boolean-terms") << "n: " << n << endl; - Trace("boolean-terms") << "nr: " << nr << endl; - if (nr.isConst() && nr.getConst()) - { - continue; - } - // Apply any define-funs from the problem. - { - unordered_map cache; - n = d_pp->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 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; - 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()) - { - // 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; + // 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. @@ -1892,7 +1644,6 @@ void SmtEngine::getInstantiationTermVectors( Node q, std::vector>& tvecs) { SmtScope smts(this); - Assert(options::trackInstLemmas()); TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); te->getInstantiationTermVectors(q, tvecs); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index da12d336b..53e982a2d 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -104,6 +104,7 @@ class ResourceOutListener; class SmtNodeManagerListener; class OptionsManager; class Preprocessor; +class CheckModels; /** Subsolvers */ class SmtSolver; class SygusSolver; @@ -1096,6 +1097,11 @@ class CVC4_PUBLIC SmtEngine */ std::unique_ptr d_model; + /** + * The utility used for checking models + */ + std::unique_ptr d_checkModels; + /** * The proof manager, which manages all things related to checking, * processing, and printing proofs. diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 8ff022556..26a2ff3e1 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -260,5 +260,7 @@ TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); } prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); } +Preprocessor* SmtSolver::getPreprocessor() { return &d_pp; } + } // namespace smt } // namespace CVC4 diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 037c9fb9c..e3cbea152 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -119,6 +119,8 @@ class SmtSolver TheoryEngine* getTheoryEngine(); /** Get a pointer to the PropEngine owned by this solver. */ prop::PropEngine* getPropEngine(); + /** Get a pointer to the preprocessor */ + Preprocessor* getPreprocessor(); //------------------------------------------ end access methods private: /** Reference to the parent SMT engine */ -- 2.30.2