: PreprocessingPass(preprocContext, "unconstrained-simplifier"),
d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
d_context(preprocContext->getDecisionContext()),
- d_substitutions(preprocContext->getDecisionContext()),
- d_logicInfo(preprocContext->getLogicInfo())
+ d_substitutions(preprocContext->getDecisionContext())
{
smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim);
}
// Uninterpreted function - if domain is infinite, no quantifiers are
// used, and any child is unconstrained, result is unconstrained
case kind::APPLY_UF:
- if (d_logicInfo.isQuantified()
+ if (d_preprocContext->getLogicInfo().isQuantified()
|| !current.getType().getCardinality().isInfinite())
{
break;
context::Context* d_context;
theory::SubstitutionMap d_substitutions;
- const LogicInfo& d_logicInfo;
/**
* Visit all subterms in assertion. This method throws a LogicException if
* there is a subterm that is unhandled by this preprocessing pass (e.g. a
d_resourceManager->spendResource(r);
}
- const LogicInfo& getLogicInfo() { return d_smt->d_logic; }
+ /** Get the current logic info of the SmtEngine */
+ const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); }
/* Widen the logic to include the given theory. */
void widenLogic(theory::TheoryId id);
Preprocessor::Preprocessor(SmtEngine& smt,
context::UserContext* u,
- AbstractValues& abs)
+ AbstractValues& abs,
+ SmtEngineStatistics& stats)
: d_context(u),
d_smt(smt),
d_absValues(abs),
d_propagator(true, true),
d_assertionsProcessed(u, false),
- d_processor(smt, *smt.getResourceManager()),
+ d_processor(smt, *smt.getResourceManager(), stats),
d_rtf(u),
d_pnm(nullptr)
{
class Preprocessor
{
public:
- Preprocessor(SmtEngine& smt, context::UserContext* u, AbstractValues& abs);
+ Preprocessor(SmtEngine& smt,
+ context::UserContext* u,
+ AbstractValues& abs,
+ SmtEngineStatistics& stats);
~Preprocessor();
/**
* Finish initialization
unsigned& d_depth;
};
-ProcessAssertions::ProcessAssertions(SmtEngine& smt, ResourceManager& rm)
- : d_smt(smt), d_resourceManager(rm), d_preprocessingPassContext(nullptr)
+ProcessAssertions::ProcessAssertions(SmtEngine& smt,
+ ResourceManager& rm,
+ SmtEngineStatistics& stats)
+ : d_smt(smt),
+ d_resourceManager(rm),
+ d_smtStats(stats),
+ d_preprocessingPassContext(nullptr)
{
d_true = NodeManager::currentNM()->mkConst(true);
}
Chat() << "expanding definitions..." << endl;
Trace("simplify") << "ProcessAssertions::simplify(): expanding definitions"
<< endl;
- TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
+ TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime);
unordered_map<Node, Node, NodeHashFunction> cache;
for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
{
d_passes["sep-skolem-emp"]->apply(&assertions);
}
- if (d_smt.d_logic.isQuantified())
+ if (d_smt.getLogicInfo().isQuantified())
{
// remove rewrite rules, apply pre-skolemization to existential quantifiers
d_passes["quantifiers-preprocess"]->apply(&assertions);
}
// rephrasing normal inputs as sygus problems
- if (!d_smt.d_isInternalSubsolver)
+ if (!d_smt.isInternalSubsolver())
{
if (options::sygusInference())
{
noConflict = simplifyAssertions(assertions);
if (!noConflict)
{
- ++(d_smt.d_stats->d_simplifiedToFalse);
+ ++(d_smtStats.d_simplifiedToFalse);
}
Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
<< endl;
Debug("smt") << " assertions : " << assertions.size() << endl;
{
- d_smt.d_stats->d_numAssertionsPre += assertions.size();
+ d_smtStats.d_numAssertionsPre += assertions.size();
d_passes["ite-removal"]->apply(&assertions);
// This is needed because when solving incrementally, removeITEs may
// introduce skolems that were solved for earlier and thus appear in the
// substitution map.
d_passes["apply-substs"]->apply(&assertions);
- d_smt.d_stats->d_numAssertionsPost += assertions.size();
+ d_smtStats.d_numAssertionsPost += assertions.size();
}
dumpAssertions("pre-repeat-simplify", assertions);
if ( // check that option is on
options::arithMLTrick() &&
// only useful in arith
- d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
+ d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
// we add new assertions and need this (in practice, this
// restriction only disables miplib processing during
// re-simplification, which we don't expect to be useful anyway)
unordered_map<Node, Node, NodeHashFunction>& cache,
bool expandOnly)
{
- NodeManager* nm = d_smt.d_nodeManager;
+ NodeManager* nm = d_smt.getNodeManager();
std::stack<std::tuple<Node, Node, bool>> worklist;
std::stack<Node> result;
worklist.push(std::make_tuple(Node(n), Node(n), false));
// we can short circuit (variable) leaves
if (n.isVar())
{
- SmtEngine::DefinedFunctionMap::const_iterator i =
- d_smt.d_definedFunctions->find(n);
- if (i != d_smt.d_definedFunctions->end())
+ SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
+ SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n);
+ if (i != dfuns->end())
{
Node f = (*i).second.getFormula();
// must expand its definition
{
// application of a user-defined symbol
TNode func = n.getOperator();
- SmtEngine::DefinedFunctionMap::const_iterator i =
- d_smt.d_definedFunctions->find(func);
- if (i == d_smt.d_definedFunctions->end())
+ SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
+ SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func);
+ if (i == dfuns->end())
{
throw TypeCheckingException(
n.toExpr(),
typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
public:
- ProcessAssertions(SmtEngine& smt, ResourceManager& rm);
+ ProcessAssertions(SmtEngine& smt,
+ ResourceManager& rm,
+ SmtEngineStatistics& stats);
~ProcessAssertions();
/** Finish initialize
*
SmtEngine& d_smt;
/** Reference to resource manager */
ResourceManager& d_resourceManager;
+ /** Reference to the SMT stats */
+ SmtEngineStatistics& d_smtStats;
/** The preprocess context */
preprocessing::PreprocessingPassContext* d_preprocessingPassContext;
/** True node */
#include "api/cvc4cpp.h"
#include "base/check.h"
-#include "base/configuration.h"
-#include "base/configuration_private.h"
#include "base/exception.h"
#include "base/modal_exception.h"
#include "base/output.h"
#include "decision/decision_engine.h"
#include "expr/node.h"
-#include "expr/node_self_iterator.h"
-#include "expr/node_visitor.h"
#include "options/base_options.h"
#include "options/language.h"
#include "options/main_options.h"
-#include "options/option_exception.h"
#include "options/printer_options.h"
-#include "options/set_language.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "printer/printer.h"
#include "smt/smt_engine_stats.h"
#include "smt/smt_solver.h"
#include "smt/sygus_solver.h"
-#include "smt/term_formula_removal.h"
-#include "smt/update_ostream.h"
-#include "theory/logic_info.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/rewriter.h"
#include "theory/smt_engine_subsolver.h"
#include "theory/theory_engine.h"
-#include "util/hash.h"
#include "util/random.h"
#include "util/resource_manager.h"
+// 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;
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, getUserContext(), *d_absValues.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());
+ // 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));
}
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
{
typedef NodeTemplate<false> TNode;
struct NodeHashFunction;
-class Command;
-class GetModelCommand;
-
class SmtEngine;
class DecisionEngine;
class TheoryEngine;
-
class ProofManager;
class UnsatCore;
-
class LogicRequest;
class StatisticsRegistry;
-
class Printer;
/* -------------------------------------------------------------------------- */
class Rewriter;
}/* CVC4::theory namespace */
-// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
-// hood): use a type parameter and have check() delegate, or subclass
-// SmtEngine and override check()?
-//
-// Probably better than that is to have a configuration object that
-// indicates which passes are desired. The configuration occurs
-// elsewhere (and can even occur at runtime). A simple "pass manager"
-// of sorts determines check()'s behavior.
-//
-// The CNF conversion can go on in PropEngine.
/* -------------------------------------------------------------------------- */
class CVC4_PUBLIC SmtEngine
{
friend class ::CVC4::api::Solver;
- // TODO (Issue #1096): Remove this friend relationship.
- friend class ::CVC4::preprocessing::PreprocessingPassContext;
friend class ::CVC4::smt::SmtEngineState;
friend class ::CVC4::smt::SmtScope;
- friend class ::CVC4::smt::ProcessAssertions;
- friend class ::CVC4::smt::SmtSolver;
- friend ProofManager* ::CVC4::smt::currentProofManager();
friend class ::CVC4::LogicRequest;
- friend class ::CVC4::theory::TheoryModel;
- friend class ::CVC4::theory::Rewriter;
/* ....................................................................... */
public:
void setLogic(const LogicInfo& logic);
/** Get the logic information currently set. */
- LogicInfo getLogicInfo() const;
+ const LogicInfo& getLogicInfo() const;
/** Get the logic information set by the user. */
LogicInfo getUserLogicInfo() const;
Options& getOptions();
const Options& getOptions() const;
+ /** Get a pointer to the UserContext owned by this SmtEngine. */
+ context::UserContext* getUserContext();
+
+ /** Get a pointer to the Context owned by this SmtEngine. */
+ context::Context* getContext();
+
+ /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
+ TheoryEngine* getTheoryEngine();
+
+ /** Get a pointer to the PropEngine owned by this SmtEngine. */
+ prop::PropEngine* getPropEngine();
+
+ /**
+ * Get a pointer to the ProofManager owned by this SmtEngine.
+ * TODO (project #37): this is the old proof manager and will be deleted
+ */
+ ProofManager* getProofManager() { return d_proofManager.get(); };
+
/** Get the resource manager of this SMT engine */
ResourceManager* getResourceManager();
/** Get a pointer to the Rewriter owned by this SmtEngine. */
theory::Rewriter* getRewriter() { return d_rewriter.get(); }
+ /** The type of our internal map of defined functions */
+ using DefinedFunctionMap =
+ context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>;
+
+ /** Get the defined function map */
+ DefinedFunctionMap* getDefinedFunctionMap() { return d_definedFunctions; }
/**
* Get expanded assertions.
*
/* ....................................................................... */
private:
/* ....................................................................... */
-
- /** The type of our internal map of defined functions */
- typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
- DefinedFunctionMap;
/** The type of our internal assertion list */
typedef context::CDList<Node> AssertionList;
/** Set solver instance that owns this SmtEngine. */
void setSolver(api::Solver* solver) { d_solver = solver; }
- /** Get a pointer to the UserContext owned by this SmtEngine. */
- context::UserContext* getUserContext();
-
- /** Get a pointer to the Context owned by this SmtEngine. */
- context::Context* getContext();
-
- /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
- TheoryEngine* getTheoryEngine();
-
- /** Get a pointer to the PropEngine owned by this SmtEngine. */
- prop::PropEngine* getPropEngine();
-
- /**
- * Get a pointer to the ProofManager owned by this SmtEngine.
- * TODO (project #37): this is the old proof manager and will be deleted
- */
- ProofManager* getProofManager() { return d_proofManager.get(); };
-
/** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
StatisticsRegistry* getStatisticsRegistry()
{
*/
void setLogicInternal();
- /**
- * Add to Model command. This is used for recording a command
- * that should be reported during a get-model call.
- */
- void addToModelCommandAndDump(const Command& c,
- uint32_t flags = 0,
- bool userVisible = true,
- const char* dumpTag = "declarations");
-
/*
* Check satisfiability (used to check satisfiability and entailment).
*/
*/
std::map<std::string, Integer> d_commandVerbosity;
+ /** The statistics registry */
std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
+ /** The statistics class */
std::unique_ptr<smt::SmtEngineStatistics> d_stats;
/** The options object */
projects / cvc5.git / commitdiff