smt/solver_engine_scope.h
smt/smt_engine_state.cpp
smt/smt_engine_state.h
- smt/smt_engine_stats.cpp
- smt/smt_engine_stats.h
+ smt/solver_engine_stats.cpp
+ smt/solver_engine_stats.h
smt/smt_mode.cpp
smt/smt_mode.h
smt/smt_solver.cpp
#include "printer/printer.h"
#include "proof/conv_proof_generator.h"
#include "smt/dump_manager.h"
-#include "smt/smt_engine_stats.h"
+#include "smt/solver_engine_stats.h"
#include "theory/evaluator.h"
#include "theory/rewriter.h"
#include "theory/trust_substitutions.h"
#include "preprocessing/assertion_pipeline.h"
#include "proof/conv_proof_generator.h"
#include "smt/env.h"
-#include "smt/smt_engine_stats.h"
#include "smt/solver_engine.h"
+#include "smt/solver_engine_stats.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "util/resource_manager.h"
namespace cvc5 {
namespace smt {
-ExpandDefs::ExpandDefs(Env& env, SmtEngineStatistics& stats)
+ExpandDefs::ExpandDefs(Env& env, SolverEngineStatistics& stats)
: d_env(env), d_smtStats(stats), d_tpg(nullptr)
{
}
namespace smt {
-struct SmtEngineStatistics;
+struct SolverEngineStatistics;
/**
* Module in charge of expanding definitions for an SMT engine.
class ExpandDefs
{
public:
- ExpandDefs(Env& env, SmtEngineStatistics& stats);
+ ExpandDefs(Env& env, SolverEngineStatistics& stats);
~ExpandDefs();
/**
* Expand definitions in term n. Return the expanded form of n.
/** Reference to the environment. */
Env& d_env;
/** Reference to the SMT stats */
- SmtEngineStatistics& d_smtStats;
+ SolverEngineStatistics& d_smtStats;
/** A proof generator for the term conversion. */
std::unique_ptr<TConvProofGenerator> d_tpg;
};
Preprocessor::Preprocessor(Env& env,
AbstractValues& abs,
- SmtEngineStatistics& stats)
+ SolverEngineStatistics& stats)
: EnvObj(env),
d_absValues(abs),
d_propagator(true, true),
class Preprocessor : protected EnvObj
{
public:
- Preprocessor(Env& env, AbstractValues& abs, SmtEngineStatistics& stats);
+ Preprocessor(Env& env, AbstractValues& abs, SolverEngineStatistics& stats);
~Preprocessor();
/**
* Finish initialization
#include "smt/dump.h"
#include "smt/expand_definitions.h"
#include "smt/print_benchmark.h"
-#include "smt/smt_engine_stats.h"
+#include "smt/solver_engine_stats.h"
#include "theory/logic_info.h"
#include "theory/theory_engine.h"
unsigned& d_depth;
};
-ProcessAssertions::ProcessAssertions(Env& env, SmtEngineStatistics& stats)
+ProcessAssertions::ProcessAssertions(Env& env, SolverEngineStatistics& stats)
: EnvObj(env), d_smtStats(stats), d_preprocessingPassContext(nullptr)
{
d_true = NodeManager::currentNM()->mkConst(true);
namespace smt {
class Assertions;
-struct SmtEngineStatistics;
+struct SolverEngineStatistics;
/**
* Module in charge of processing assertions for an SMT engine.
typedef std::unordered_map<Node, bool> NodeToBoolHashMap;
public:
- ProcessAssertions(Env& env, SmtEngineStatistics& stats);
+ ProcessAssertions(Env& env, SolverEngineStatistics& stats);
~ProcessAssertions();
/** Finish initialize
*
private:
/** Reference to the SMT stats */
- SmtEngineStatistics& d_smtStats;
+ SolverEngineStatistics& d_smtStats;
/** The preprocess context */
preprocessing::PreprocessingPassContext* d_preprocessingPassContext;
/** True node */
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Tim King, Gereon Kremer, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of statistics for SMT engine.
- */
-
-#include "smt/smt_engine_stats.h"
-
-#include "smt/smt_statistics_registry.h"
-
-namespace cvc5 {
-namespace smt {
-
-SmtEngineStatistics::SmtEngineStatistics(const std::string& name)
- : d_definitionExpansionTime(smtStatisticsRegistry().registerTimer(
- name + "definitionExpansionTime")),
- d_numConstantProps(
- smtStatisticsRegistry().registerInt(name + "numConstantProps")),
- d_numAssertionsPre(smtStatisticsRegistry().registerInt(
- name + "numAssertionsPreITERemoval")),
- d_numAssertionsPost(smtStatisticsRegistry().registerInt(
- name + "numAssertionsPostITERemoval")),
- d_checkModelTime(
- smtStatisticsRegistry().registerTimer(name + "checkModelTime")),
- d_checkUnsatCoreTime(
- smtStatisticsRegistry().registerTimer(name + "checkUnsatCoreTime")),
- d_solveTime(smtStatisticsRegistry().registerTimer(name + "solveTime")),
- d_pushPopTime(
- smtStatisticsRegistry().registerTimer(name + "pushPopTime")),
- d_processAssertionsTime(smtStatisticsRegistry().registerTimer(
- name + "processAssertionsTime")),
- d_simplifiedToFalse(
- smtStatisticsRegistry().registerInt(name + "simplifiedToFalse"))
-{
-}
-
-} // namespace smt
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Statistics for SMT engine.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SMT__SMT_ENGINE_STATS_H
-#define CVC5__SMT__SMT_ENGINE_STATS_H
-
-#include "util/statistics_stats.h"
-
-namespace cvc5 {
-namespace smt {
-
-struct SmtEngineStatistics
-{
- SmtEngineStatistics(const std::string& name = "smt::SolverEngine::");
- /** time spent in definition-expansion */
- TimerStat d_definitionExpansionTime;
- /** number of constant propagations found during nonclausal simp */
- IntStat d_numConstantProps;
- /** Number of assertions before ite removal */
- IntStat d_numAssertionsPre;
- /** Number of assertions after ite removal */
- IntStat d_numAssertionsPost;
- /** time spent in checkModel() */
- TimerStat d_checkModelTime;
- /** time spent in checkUnsatCore() */
- TimerStat d_checkUnsatCoreTime;
- /** time spent in PropEngine::checkSat() */
- TimerStat d_solveTime;
- /** time spent in pushing/popping */
- TimerStat d_pushPopTime;
- /** time spent in processAssertions() */
- TimerStat d_processAssertionsTime;
-
- /** Has something simplified to false? */
- IntStat d_simplifiedToFalse;
-}; /* struct SmtEngineStatistics */
-
-} // namespace smt
-} // namespace cvc5
-
-#endif /* CVC5__SMT__SMT_ENGINE_STATS_H */
#include "smt/env.h"
#include "smt/preprocessor.h"
#include "smt/smt_engine_state.h"
-#include "smt/smt_engine_stats.h"
#include "smt/solver_engine.h"
+#include "smt/solver_engine_stats.h"
#include "theory/logic_info.h"
#include "theory/theory_engine.h"
#include "theory/theory_traits.h"
SmtSolver::SmtSolver(Env& env,
SmtEngineState& state,
AbstractValues& abs,
- SmtEngineStatistics& stats)
+ SolverEngineStatistics& stats)
: d_env(env),
d_state(state),
d_pp(env, abs, stats),
class Assertions;
class SmtEngineState;
-struct SmtEngineStatistics;
+struct SolverEngineStatistics;
/**
* A solver for SMT queries.
SmtSolver(Env& env,
SmtEngineState& state,
AbstractValues& abs,
- SmtEngineStatistics& stats);
+ SolverEngineStatistics& stats);
~SmtSolver();
/**
* Create theory engine, prop engine based on the environment.
/** The preprocessor of this SMT solver */
Preprocessor d_pp;
/** Reference to the statistics of SolverEngine */
- SmtEngineStatistics& d_stats;
+ SolverEngineStatistics& d_stats;
/** The theory engine */
std::unique_ptr<TheoryEngine> d_theoryEngine;
/** The propositional engine */
#include "smt/quant_elim_solver.h"
#include "smt/set_defaults.h"
#include "smt/smt_engine_state.h"
-#include "smt/smt_engine_stats.h"
#include "smt/smt_solver.h"
#include "smt/solver_engine_scope.h"
+#include "smt/solver_engine_stats.h"
#include "smt/sygus_solver.h"
#include "smt/unsat_core_manager.h"
#include "theory/quantifiers/instantiation_list.h"
// listen to resource out
getResourceManager()->registerListener(d_routListener.get());
// make statistics
- d_stats.reset(new SmtEngineStatistics());
+ d_stats.reset(new SolverEngineStatistics());
// make the SMT solver
d_smtSolver.reset(new SmtSolver(*d_env, *d_state, *d_absValues, *d_stats));
// make the SyGuS solver
class InterpolationSolver;
class QuantElimSolver;
-struct SmtEngineStatistics;
+struct SolverEngineStatistics;
class SolverEngineScope;
class PfManager;
class UnsatCoreManager;
std::map<std::string, int> d_commandVerbosity;
/** The statistics class */
- std::unique_ptr<smt::SmtEngineStatistics> d_stats;
+ std::unique_ptr<smt::SolverEngineStatistics> d_stats;
/** the output manager for commands */
mutable OutputManager d_outMgr;
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Tim King, Gereon Kremer, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Implementation of statistics for SMT engine.
+ */
+
+#include "smt/solver_engine_stats.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace cvc5 {
+namespace smt {
+
+SolverEngineStatistics::SolverEngineStatistics(const std::string& name)
+ : d_definitionExpansionTime(smtStatisticsRegistry().registerTimer(
+ name + "definitionExpansionTime")),
+ d_numConstantProps(
+ smtStatisticsRegistry().registerInt(name + "numConstantProps")),
+ d_numAssertionsPre(smtStatisticsRegistry().registerInt(
+ name + "numAssertionsPreITERemoval")),
+ d_numAssertionsPost(smtStatisticsRegistry().registerInt(
+ name + "numAssertionsPostITERemoval")),
+ d_checkModelTime(
+ smtStatisticsRegistry().registerTimer(name + "checkModelTime")),
+ d_checkUnsatCoreTime(
+ smtStatisticsRegistry().registerTimer(name + "checkUnsatCoreTime")),
+ d_solveTime(smtStatisticsRegistry().registerTimer(name + "solveTime")),
+ d_pushPopTime(
+ smtStatisticsRegistry().registerTimer(name + "pushPopTime")),
+ d_processAssertionsTime(smtStatisticsRegistry().registerTimer(
+ name + "processAssertionsTime")),
+ d_simplifiedToFalse(
+ smtStatisticsRegistry().registerInt(name + "simplifiedToFalse"))
+{
+}
+
+} // namespace smt
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Morgan Deters, Andrew Reynolds, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Statistics for SMT engine.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__SMT__SOLVER_ENGINE_STATS_H
+#define CVC5__SMT__SOLVER_ENGINE_STATS_H
+
+#include "util/statistics_stats.h"
+
+namespace cvc5 {
+namespace smt {
+
+struct SolverEngineStatistics
+{
+ SolverEngineStatistics(const std::string& name = "smt::SolverEngine::");
+ /** time spent in definition-expansion */
+ TimerStat d_definitionExpansionTime;
+ /** number of constant propagations found during nonclausal simp */
+ IntStat d_numConstantProps;
+ /** Number of assertions before ite removal */
+ IntStat d_numAssertionsPre;
+ /** Number of assertions after ite removal */
+ IntStat d_numAssertionsPost;
+ /** time spent in checkModel() */
+ TimerStat d_checkModelTime;
+ /** time spent in checkUnsatCore() */
+ TimerStat d_checkUnsatCoreTime;
+ /** time spent in PropEngine::checkSat() */
+ TimerStat d_solveTime;
+ /** time spent in pushing/popping */
+ TimerStat d_pushPopTime;
+ /** time spent in processAssertions() */
+ TimerStat d_processAssertionsTime;
+
+ /** Has something simplified to false? */
+ IntStat d_simplifiedToFalse;
+}; /* struct SolverEngineStatistics */
+
+} // namespace smt
+} // namespace cvc5
+
+#endif /* CVC5__SMT__SMT_ENGINE_STATS_H */