This is work towards replacing our old dump infrastructure. This PR also does some initial reorganization towards printing assertions using the print benchmark utility.
return true;
}
-void PropEngine::checkProof(context::CDList<Node>* assertions)
+void PropEngine::checkProof(const context::CDList<Node>& assertions)
{
if (!d_env.isSatProofProducing())
{
/** Checks that the proof is closed w.r.t. asserted formulas to this engine as
* well as to the given assertions. */
- void checkProof(context::CDList<Node>* assertions);
+ void checkProof(const context::CDList<Node>& assertions);
/**
* Return the prop engine proof. This should be called only when proofs are
d_assertions.push_back(assertion);
}
-void PropPfManager::checkProof(context::CDList<Node>* assertions)
+void PropPfManager::checkProof(const context::CDList<Node>& assertions)
{
Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution "
"proof of false is closed\n";
// connect it with CNF proof
d_pfpp->process(conflictProof);
// add given assertions d_assertions
- for (const Node& assertion : *assertions)
+ for (const Node& assertion : assertions)
{
d_assertions.push_back(assertion);
}
* engine's proof with the preprocessing proof) and these changes survive for
* a next check-sat call.
*/
- void checkProof(context::CDList<Node>* assertions);
+ void checkProof(const context::CDList<Node>& assertions);
private:
/** A node manager */
namespace smt {
Assertions::Assertions(Env& env, AbstractValues& absv)
- : d_env(env),
+ : EnvObj(env),
d_absValues(absv),
d_produceAssertions(false),
- d_assertionList(env.getUserContext()),
+ d_assertionList(userContext()),
+ d_assertionListDefs(userContext()),
d_globalNegation(false),
d_assertions()
{
Node n = d_absValues.substituteAbstractValues(e);
// Ensure expr is type-checked at this point.
ensureBoolean(n);
- addFormula(n, true, true, false, false);
+ addFormula(n, true, false, false);
}
if (d_globalDefineFunLemmas != nullptr)
{
// zero assertions)
for (const Node& lemma : *d_globalDefineFunLemmas)
{
- addFormula(lemma, true, false, true, false);
+ addFormula(lemma, false, true, false);
}
}
}
{
ensureBoolean(n);
bool maybeHasFv = language::isLangSygus(options::inputLanguage());
- addFormula(n, true, false, false, maybeHasFv);
+ addFormula(n, false, false, maybeHasFv);
}
std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
return d_assertions;
}
-context::CDList<Node>* Assertions::getAssertionList()
+const context::CDList<Node>& Assertions::getAssertionList() const
{
- return d_produceAssertions ? &d_assertionList : nullptr;
+ return d_assertionList;
+}
+
+const context::CDList<Node>& Assertions::getAssertionListDefinitions() const
+{
+ return d_assertionListDefs;
}
void Assertions::addFormula(TNode n,
- bool inInput,
bool isAssumption,
bool isFunDef,
bool maybeHasFv)
if (d_produceAssertions)
{
d_assertionList.push_back(n);
+ if (isFunDef)
+ {
+ d_assertionListDefs.push_back(n);
+ }
}
if (n.isConst() && n.getConst<bool>())
{
// true, nothing to do
return;
}
- Trace("smt") << "Assertions::addFormula(" << n << ", inInput = " << inInput
+ Trace("smt") << "Assertions::addFormula(" << n
<< ", isAssumption = " << isAssumption
<< ", isFunDef = " << isFunDef << std::endl;
if (isFunDef)
// definitions currently. Thus, we should check for free variables if the
// input language is SyGuS.
bool maybeHasFv = language::isLangSygus(options::inputLanguage());
- addFormula(n, true, false, true, maybeHasFv);
+ addFormula(n, false, true, maybeHasFv);
}
}
#include "context/cdlist.h"
#include "expr/node.h"
#include "preprocessing/assertion_pipeline.h"
+#include "smt/env_obj.h"
namespace cvc5 {
-
-class Env;
-
namespace smt {
class AbstractValues;
* check-sat calls. It is *not* responsible for the preprocessing itself, and
* instead is intended to be the input to a preprocessor utility.
*/
-class Assertions
+class Assertions : protected EnvObj
{
/** The type of our internal assertion list */
typedef context::CDList<Node> AssertionList;
preprocessing::AssertionPipeline& getAssertionPipeline();
/**
* Get assertions list corresponding to the original list of assertions,
- * before preprocessing.
+ * before preprocessing. This includes assertions corresponding to define-fun
+ * and define-fun-rec.
+ */
+ const context::CDList<Node>& getAssertionList() const;
+ /**
+ * Get assertions list corresponding to the original list of assertions
+ * that correspond to definitions (define-fun or define-fun-rec).
*/
- context::CDList<Node>* getAssertionList();
+ const context::CDList<Node>& getAssertionListDefinitions() const;
/**
* Get the list of assumptions, which are those registered to this class
* on initializeCheckSat.
* (this is used to distinguish assertions and assumptions)
*/
void addFormula(TNode n,
- bool inInput,
bool isAssumption,
bool isFunDef,
bool maybeHasFv);
- /** Reference to the environment. */
- Env& d_env;
/** Reference to the abstract values utility */
AbstractValues& d_absValues;
/** Whether we are producing assertions */
bool d_produceAssertions;
/**
- * The assertion list (before any conversion) for supporting
- * getAssertions(). Only maintained if in incremental mode.
+ * The assertion list (before any conversion) for supporting getAssertions().
*/
AssertionList d_assertionList;
+ /** The subset of above the correspond to define-fun or define-fun-rec */
+ AssertionList d_assertionListDefs;
/**
* List of lemmas generated for global (recursive) function definitions. We
* assert this list of definitions in each check-sat call.
CheckModels::~CheckModels() {}
void CheckModels::checkModel(TheoryModel* m,
- context::CDList<Node>* al,
+ const context::CDList<Node>& al,
bool hardFailure)
{
// Throughout, we use Notice() to give diagnostic output.
// the list of assertions that did not rewrite to true
std::vector<Node> noCheckList;
// Now go through all our user assertions checking if they're satisfied.
- for (const Node& assertion : *al)
+ for (const Node& assertion : al)
{
Notice() << "SolverEngine::checkModel(): checking assertion " << assertion
<< std::endl;
* given assertion list al based on the model checking policy.
*/
void checkModel(theory::TheoryModel* m,
- context::CDList<Node>* al,
+ const context::CDList<Node>& al,
bool hardFailure);
private:
namespace cvc5 {
namespace smt {
-Preprocessor::Preprocessor(SolverEngine& slv,
- Env& env,
+Preprocessor::Preprocessor(Env& env,
AbstractValues& abs,
SmtEngineStatistics& stats)
- : d_slv(slv),
- d_env(env),
+ : EnvObj(env),
d_absValues(abs),
d_propagator(true, true),
d_assertionsProcessed(env.getUserContext(), false),
d_exDefs(env, stats),
- d_processor(slv, *env.getResourceManager(), stats),
+ d_processor(env, stats),
d_pnm(nullptr)
{
}
}
}
-void Preprocessor::finishInit()
+void Preprocessor::finishInit(SolverEngine* slv)
{
- d_ppContext.reset(new preprocessing::PreprocessingPassContext(
- &d_slv, d_env, &d_propagator));
+ d_ppContext.reset(
+ new preprocessing::PreprocessingPassContext(slv, d_env, &d_propagator));
// initialize the preprocessing passes
d_processor.finishInit(d_ppContext.get());
Trace("smt") << "SMT simplify(" << node << ")" << endl;
if (Dump.isOn("benchmark"))
{
- d_slv.getOutputManager().getPrinter().toStreamCmdSimplify(
- d_slv.getOutputManager().getDumpOut(), node);
+ d_env.getPrinter().toStreamCmdSimplify(d_env.getDumpOut(), node);
}
Node ret = expandDefinitions(node);
ret = theory::Rewriter::rewrite(ret);
Assert(pppg != nullptr);
d_pnm = pppg->getManager();
d_exDefs.setProofNodeManager(d_pnm);
- d_propagator.setProof(d_pnm, d_env.getUserContext(), pppg);
+ d_propagator.setProof(d_pnm, userContext(), pppg);
}
} // namespace smt
#include <memory>
+#include "smt/env_obj.h"
#include "smt/expand_definitions.h"
#include "smt/process_assertions.h"
#include "theory/booleans/circuit_propagator.h"
namespace cvc5 {
-class Env;
+
+class SolverEngine;
+
namespace preprocessing {
class PreprocessingPassContext;
}
* (2) implementing methods for expanding and simplifying formulas. The latter
* takes into account the substitutions inferred by this class.
*/
-class Preprocessor
+class Preprocessor : protected EnvObj
{
public:
- Preprocessor(SolverEngine& smt,
- Env& env,
- AbstractValues& abs,
- SmtEngineStatistics& stats);
+ Preprocessor(Env& env, AbstractValues& abs, SmtEngineStatistics& stats);
~Preprocessor();
/**
* Finish initialization
*/
- void finishInit();
+ void finishInit(SolverEngine* slv);
/**
* Process the assertions that have been asserted in argument as. Returns
* true if no conflict was discovered while preprocessing them.
void setProofGenerator(PreprocessProofGenerator* pppg);
private:
- /** Reference to the parent SolverEngine */
- SolverEngine& d_slv;
- /** Reference to the env */
- Env& d_env;
/** Reference to the abstract values utility */
AbstractValues& d_absValues;
/**
#include "smt/assertions.h"
#include "smt/dump.h"
#include "smt/expand_definitions.h"
+#include "smt/print_benchmark.h"
#include "smt/smt_engine_stats.h"
-#include "smt/solver_engine.h"
#include "theory/logic_info.h"
#include "theory/theory_engine.h"
unsigned& d_depth;
};
-ProcessAssertions::ProcessAssertions(SolverEngine& slv,
- ResourceManager& rm,
- SmtEngineStatistics& stats)
- : d_slv(slv),
- d_resourceManager(rm),
- d_smtStats(stats),
- d_preprocessingPassContext(nullptr)
+ProcessAssertions::ProcessAssertions(Env& env, SmtEngineStatistics& stats)
+ : EnvObj(env), d_smtStats(stats), d_preprocessingPassContext(nullptr)
{
d_true = NodeManager::currentNM()->mkConst(true);
}
void ProcessAssertions::spendResource(Resource r)
{
- d_resourceManager.spendResource(r);
+ resourceManager()->spendResource(r);
}
bool ProcessAssertions::apply(Assertions& as)
AssertionPipeline& assertions = as.getAssertionPipeline();
Assert(d_preprocessingPassContext != nullptr);
// Dump the assertions
- dumpAssertions("pre-everything", assertions);
+ dumpAssertions("pre-everything", as);
Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
Trace("smt-proc")
<< "ProcessAssertions::processAssertions() : pre-definition-expansion"
<< endl;
- dumpAssertions("pre-definition-expansion", assertions);
+ dumpAssertions("pre-definition-expansion", as);
// Apply substitutions first. If we are non-incremental, this has only the
// effect of replacing defined functions with their definitions.
// We do not call theory-specific expand definitions here, since we want
Trace("smt-proc")
<< "ProcessAssertions::processAssertions() : post-definition-expansion"
<< endl;
- dumpAssertions("post-definition-expansion", assertions);
+ dumpAssertions("post-definition-expansion", as);
Debug("smt") << " assertions : " << assertions.size() << endl;
d_passes["sep-skolem-emp"]->apply(&assertions);
}
- if (d_slv.getLogicInfo().isQuantified())
+ if (logicInfo().isQuantified())
{
// remove rewrite rules, apply pre-skolemization to existential quantifiers
d_passes["quantifiers-preprocess"]->apply(&assertions);
}
// rephrasing normal inputs as sygus problems
- if (!d_slv.isInternalSubsolver())
+ if (options().quantifiers.sygusInference)
{
- if (options::sygusInference())
- {
- d_passes["sygus-infer"]->apply(&assertions);
- }
- else if (options::sygusRewSynthInput())
- {
- // do candidate rewrite rule synthesis
- d_passes["synth-rr"]->apply(&assertions);
- }
+ d_passes["sygus-infer"]->apply(&assertions);
+ }
+ else if (options().quantifiers.sygusRewSynthInput)
+ {
+ // do candidate rewrite rule synthesis
+ d_passes["synth-rr"]->apply(&assertions);
}
Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
<< endl;
- dumpAssertions("pre-simplify", assertions);
+ dumpAssertions("pre-simplify", as);
Chat() << "simplifying assertions..." << endl;
- noConflict = simplifyAssertions(assertions);
+ noConflict = simplifyAssertions(as);
if (!noConflict)
{
++(d_smtStats.d_simplifiedToFalse);
}
Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
<< endl;
- dumpAssertions("post-simplify", assertions);
+ dumpAssertions("post-simplify", as);
if (options::doStaticLearning())
{
d_smtStats.d_numAssertionsPost += assertions.size();
}
- dumpAssertions("pre-repeat-simplify", assertions);
+ dumpAssertions("pre-repeat-simplify", as);
if (options::repeatSimp())
{
Trace("smt-proc")
<< endl;
Chat() << "re-simplifying assertions..." << endl;
ScopeCounter depth(d_simplifyAssertionsDepth);
- noConflict &= simplifyAssertions(assertions);
+ noConflict &= simplifyAssertions(as);
Trace("smt-proc")
<< "ProcessAssertions::processAssertions() : post-repeat-simplify"
<< endl;
}
- dumpAssertions("post-repeat-simplify", assertions);
+ dumpAssertions("post-repeat-simplify", as);
if (options::ufHo())
{
d_passes["bv-eager-atoms"]->apply(&assertions);
}
- Trace("smt-proc") << "ProcessAssertions::apply() end" << endl;
- dumpAssertions("post-everything", assertions);
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
+ dumpAssertions("post-everything", as);
return noConflict;
}
// returns false if simplification led to "false"
-bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
+bool ProcessAssertions::simplifyAssertions(Assertions& as)
{
spendResource(Resource::PreprocessStep);
try
{
+ AssertionPipeline& assertions = as.getAssertionPipeline();
ScopeCounter depth(d_simplifyAssertionsDepth);
Trace("simplify") << "ProcessAssertions::simplify()" << endl;
if ( // check that option is on
options::arithMLTrick() &&
// only useful in arith
- d_slv.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
+ logicInfo().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)
}
}
- dumpAssertions("post-repeatsimp", assertions);
+ dumpAssertions("post-repeatsimp", as);
Trace("smt") << "POST repeatSimp" << endl;
Debug("smt") << " assertions : " << assertions.size() << endl;
}
return true;
}
-void ProcessAssertions::dumpAssertions(const char* key,
- const AssertionPipeline& assertionList)
+void ProcessAssertions::dumpAssertions(const char* key, Assertions& as)
{
if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
{
+ const AssertionPipeline& assertionList = as.getAssertionPipeline();
// Push the simplified assertions to the dump output stream
for (unsigned i = 0; i < assertionList.size(); ++i)
{
TNode n = assertionList[i];
- d_slv.getOutputManager().getPrinter().toStreamCmdAssert(
- d_slv.getOutputManager().getDumpOut(), n);
+ d_env.getPrinter().toStreamCmdAssert(d_env.getDumpOut(), n);
}
}
}
#include "context/cdlist.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "util/resource_manager.h"
namespace cvc5 {
-class SolverEngine;
-
namespace preprocessing {
class AssertionPipeline;
class PreprocessingPass;
* it processes assertions in a way that assumes that apply(...) could be
* applied multiple times to different sets of assertions.
*/
-class ProcessAssertions
+class ProcessAssertions : protected EnvObj
{
/** The types for the recursive function definitions */
typedef context::CDList<Node> NodeList;
typedef std::unordered_map<Node, bool> NodeToBoolHashMap;
public:
- ProcessAssertions(SolverEngine& smt,
- ResourceManager& rm,
- SmtEngineStatistics& stats);
+ ProcessAssertions(Env& env, SmtEngineStatistics& stats);
~ProcessAssertions();
/** Finish initialize
*
/**
* Process the formulas in as. Returns true if there was no conflict when
* processing the assertions.
+ *
+ * @param as The assertions.
*/
bool apply(Assertions& as);
private:
- /** Reference to the SMT engine */
- SolverEngine& d_slv;
- /** Reference to resource manager */
- ResourceManager& d_resourceManager;
/** Reference to the SMT stats */
SmtEngineStatistics& d_smtStats;
/** The preprocess context */
*
* Returns false if the formula simplifies to "false"
*/
- bool simplifyAssertions(preprocessing::AssertionPipeline& assertions);
+ bool simplifyAssertions(Assertions& as);
/**
* Dump assertions. Print the current assertion list to the dump
* assertions:`key` if it is enabled.
*/
- void dumpAssertions(const char* key,
- const preprocessing::AssertionPipeline& assertionList);
+ void dumpAssertions(const char* key, Assertions& as);
};
} // namespace smt
void PfManager::getAssertions(Assertions& as,
std::vector<Node>& assertions)
{
- context::CDList<Node>* al = as.getAssertionList();
- Assert(al != nullptr);
- for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
- ++i)
+ const context::CDList<Node>& al = as.getAssertionList();
+ Assert(options().smt.produceAssertions)
+ << "Expected produce assertions to be true when checking proof";
+ for (const Node& a : al)
{
- assertions.push_back(*i);
+ assertions.push_back(a);
}
}
opts.smt.checkProofs = false;
}
}
+ if (d_isInternalSubsolver)
+ {
+ // these options must be disabled on internal subsolvers, as they are
+ // used by the user to rephrase the input.
+ opts.quantifiers.sygusInference = false;
+ opts.quantifiers.sygusRewSynthInput = false;
+ }
}
void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
SmtSolver::~SmtSolver() {}
-void SmtSolver::finishInit(const LogicInfo& logicInfo)
+void SmtSolver::finishInit()
{
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
SmtEngineStatistics& stats);
~SmtSolver();
/**
- * Create theory engine, prop engine based on the logic info.
- *
- * @param logicInfo the logic information
+ * Create theory engine, prop engine based on the environment.
*/
- void finishInit(const LogicInfo& logicInfo);
+ void finishInit();
/** Reset all assertions, global declarations, etc. */
void resetAssertions();
/**
// make statistics
d_stats.reset(new SmtEngineStatistics());
// reset the preprocessor
- d_pp.reset(
- new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats));
+ d_pp.reset(new smt::Preprocessor(*d_env, *d_absValues, *d_stats));
// make the SMT solver
- d_smtSolver.reset(new SmtSolver(*d_env.get(), *d_state, *d_pp, *d_stats));
+ d_smtSolver.reset(new SmtSolver(*d_env, *d_state, *d_pp, *d_stats));
// make the SyGuS solver
d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver, *d_pp));
// make the quantifier elimination solver
}
Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;
- d_smtSolver->finishInit(logic);
+ d_smtSolver->finishInit();
// now can construct the SMT-level model object
TheoryEngine* te = d_smtSolver->getTheoryEngine();
if (d_env->getOptions().smt.produceInterpols
!= options::ProduceInterpols::NONE)
{
- d_interpolSolver.reset(new InterpolationSolver(*d_env.get()));
+ d_interpolSolver.reset(new InterpolationSolver(*d_env));
}
- d_pp->finishInit();
+ d_pp->finishInit(this);
AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
<< "The PropEngine has pushed but the SolverEngine "
std::vector<Node> SolverEngine::getAssertionsInternal()
{
Assert(d_state->isFullyInited());
- context::CDList<Node>* al = d_asserts->getAssertionList();
- Assert(al != nullptr);
+ const context::CDList<Node>& al = d_asserts->getAssertionList();
std::vector<Node> res;
- for (const Node& n : *al)
+ for (const Node& n : al)
{
res.emplace_back(n);
}
void SolverEngine::checkModel(bool hardFailure)
{
- context::CDList<Node>* al = d_asserts->getAssertionList();
+ const context::CDList<Node>& al = d_asserts->getAssertionList();
// --check-model implies --produce-assertions, which enables the
// assertion list, so we should be ok.
- Assert(al != nullptr)
+ Assert(d_env->getOptions().smt.produceAssertions)
<< "don't have an assertion list to check in SolverEngine::checkModel()";
TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
namespace smt {
SygusSolver::SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp)
- : d_env(env),
+ : EnvObj(env),
d_smtSolver(sms),
d_pp(pp),
- d_sygusConjectureStale(env.getUserContext(), true)
+ d_sygusConjectureStale(userContext(), true)
{
}
Trace("check-synth-sol") << "Retrieving assertions\n";
// Build conjecture from original assertions
- context::CDList<Node>* alist = as.getAssertionList();
- if (alist == nullptr)
- {
- Trace("check-synth-sol") << "No assertions to check\n";
- return;
- }
+ const context::CDList<Node>& alist = as.getAssertionList();
+ Assert(options().smt.produceAssertions)
+ << "Expected produce assertions to be true when checking synthesis "
+ "solution";
// auxiliary assertions
std::vector<Node> auxAssertions;
// expand definitions cache
std::unordered_map<Node, Node> cache;
- for (Node assertion : *alist)
+ for (const Node& assertion : alist)
{
Notice() << "SygusSolver::checkSynthSolution(): checking assertion "
<< assertion << std::endl;
#include "expr/node.h"
#include "expr/type_node.h"
#include "smt/assertions.h"
+#include "smt/env_obj.h"
#include "util/result.h"
namespace cvc5 {
* It also maintains a reference to a preprocessor for implementing
* checkSynthSolution.
*/
-class SygusSolver
+class SygusSolver : protected EnvObj
{
public:
SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp);
* expansion.
*/
void expandDefinitionsSygusDt(TypeNode tn) const;
- /** Reference to the env class */
- Env& d_env;
/** The SMT solver, which is used during checkSynth. */
SmtSolver& d_smtSolver;
/** The preprocessor, used for checkSynthSolution. */
expr::getFreeAssumptions(pfn->getChildren()[0].get(), fassumps);
Trace("unsat-core") << "UCManager::getUnsatCore: free assumptions: "
<< fassumps << "\n";
- context::CDList<Node>* al = as.getAssertionList();
- Assert(al != nullptr);
- for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
- ++i)
+ const context::CDList<Node>& al = as.getAssertionList();
+ for (const Node& a : al)
{
- Trace("unsat-core") << "is assertion " << *i << " there?\n";
- if (std::find(fassumps.begin(), fassumps.end(), *i) != fassumps.end())
+ Trace("unsat-core") << "is assertion " << a << " there?\n";
+ if (std::find(fassumps.begin(), fassumps.end(), a) != fassumps.end())
{
Trace("unsat-core") << "\tyes\n";
- core.push_back(*i);
+ core.push_back(a);
}
}
if (Trace.isOn("unsat-core"))
projects / cvc5.git / commitdiff