There is no reason to disable --produce-assertions, this simplifies the code to assume that assertions are always available, and always warns if the user disables this option.
CVC5_API_CHECK(d_slv->getOptions().smt.produceModels)
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
- CVC5_API_CHECK(d_slv->getOptions().smt.produceAssertions)
- << "Cannot block model value unless produce-assertions is enabled "
- "(try --produce-assertions)";
CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
<< "Can only block model values after SAT or UNKNOWN response.";
CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms)
*
* Requires enabling option
* :ref:`produce-models <lbl-option-produce-models>`.
- * 'produce-models' and setting option
- * :ref:`block-models <lbl-option-block-models>`.
- * to a mode other than ``none``.
+ * 'produce-models'.
* \endverbatim
*/
void blockModelValues(const std::vector<Term>& terms) const;
* {@code
* ( block-model-values ( <terms>+ ) )
* }
- * Requires enabling 'produce-models' option and setting 'block-models' option
- * to a mode other than "none".
+ * Requires enabling 'produce-models' option.
*/
public void blockModelValues(Term[] terms)
{
long = "produce-assertions"
type = "bool"
alias = ["interactive-mode"]
- help = "keep an assertions list (enables get-assertions command)"
+ default = "true"
+ help = "keep an assertions list. Note this option is always enabled."
[[option]]
name = "doITESimp"
Assertions::Assertions(Env& env, AbstractValues& absv)
: EnvObj(env),
d_absValues(absv),
- d_produceAssertions(false),
d_assertionList(userContext()),
d_assertionListDefs(userContext()),
d_globalDefineFunLemmasIndex(userContext(), 0),
void Assertions::refresh()
{
- if (d_globalDefineFunLemmas != nullptr)
+ // Global definitions are asserted now to ensure they always exist. This is
+ // done at the beginning of preprocessing, to ensure that definitions take
+ // priority over, e.g. solving during preprocessing. See issue #7479.
+ size_t numGlobalDefs = d_globalDefineFunLemmas.size();
+ for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++)
{
- // Global definitions are asserted now to ensure they always exist. This is
- // done at the beginning of preprocessing, to ensure that definitions take
- // priority over, e.g. solving during preprocessing. See issue #7479.
- size_t numGlobalDefs = d_globalDefineFunLemmas->size();
- for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++)
- {
- addFormula((*d_globalDefineFunLemmas)[i], false, true, false);
- }
- d_globalDefineFunLemmasIndex = numGlobalDefs;
- }
-}
-
-void Assertions::finishInit()
-{
- // [MGD 10/20/2011] keep around in incremental mode, due to a
- // cleanup ordering issue and Nodes/TNodes. If SAT is popped
- // first, some user-context-dependent TNodes might still exist
- // with rc == 0.
- if (options().smt.produceAssertions || options().base.incrementalSolving)
- {
- // In the case of incremental solving, we appear to need these to
- // ensure the relevant Nodes remain live.
- d_produceAssertions = true;
- d_globalDefineFunLemmas.reset(new std::vector<Node>());
+ addFormula(d_globalDefineFunLemmas[i], false, true, false);
}
+ d_globalDefineFunLemmasIndex = numGlobalDefs;
}
void Assertions::clearCurrent()
bool isFunDef,
bool maybeHasFv)
{
- // add to assertion list if it exists
- if (d_produceAssertions)
+ // add to assertion list
+ d_assertionList.push_back(n);
+ if (isFunDef)
{
- d_assertionList.push_back(n);
- if (isFunDef)
- {
- d_assertionListDefs.push_back(n);
- }
+ d_assertionListDefs.push_back(n);
}
if (n.isConst() && n.getConst<bool>())
{
void Assertions::addDefineFunDefinition(Node n, bool global)
{
n = d_absValues.substituteAbstractValues(n);
- if (global && d_globalDefineFunLemmas != nullptr)
+ if (global)
{
// Global definitions are asserted at check-sat-time because we have to
// make sure that they are always present
Assert(!language::isLangSygus(options().base.inputLanguage));
- d_globalDefineFunLemmas->emplace_back(n);
+ d_globalDefineFunLemmas.emplace_back(n);
}
else
{
public:
Assertions(Env& env, AbstractValues& absv);
~Assertions();
- /**
- * Finish initialization, called once after options are finalized. Sets up
- * the required bookkeeping based on the options.
- */
- void finishInit();
/**
* Clears out the non-context-dependent data in this class. Necessary to
* clear out our assertion vectors in case someone does a push-assert-pop
bool maybeHasFv);
/** 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().
*/
* List of lemmas generated for global (recursive) function definitions. We
* assert this list of definitions in each check-sat call.
*/
- std::unique_ptr<std::vector<Node>> d_globalDefineFunLemmas;
+ std::vector<Node> d_globalDefineFunLemmas;
/** The index of the above list that we have processed */
context::CDO<size_t> d_globalDefineFunLemmasIndex;
/**
void ProcessAssertions::dumpAssertionsToStream(std::ostream& os, Assertions& as)
{
- // Cannot print unless produce assertions is enabled. Otherwise, the printing
- // is misleading, since it does not capture what symbols were provided
- // as definitions.
- if (!options().smt.produceAssertions)
- {
- warning()
- << "Assertions not available for dumping (use --produce-assertions)."
- << std::endl;
- return;
- }
PrintBenchmark pb(&d_env.getPrinter());
std::vector<Node> assertions;
// Notice that the following list covers define-fun and define-fun-rec
void PfManager::getAssertions(Assertions& as,
std::vector<Node>& assertions)
{
+ // note that the assertion list is always available
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(a);
void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
{
- if ((opts.smt.checkModels || opts.smt.checkSynthSol || opts.smt.produceAbducts
- || opts.smt.produceInterpols != options::ProduceInterpols::NONE
- || opts.smt.modelCoresMode != options::ModelCoresMode::NONE
- || opts.smt.blockModelsMode != options::BlockModelsMode::NONE
- || opts.smt.produceProofs || isSygus(opts))
- && !opts.smt.produceAssertions)
- {
- verbose(1) << "SolverEngine: turning on produce-assertions to support "
- << "option requiring assertions." << std::endl;
+ if (!opts.smt.produceAssertions)
+ {
+ verbose(1) << "SolverEngine: turning on produce-assertions." << std::endl;
opts.smt.produceAssertions = true;
}
// of context-dependent data structures
d_state->setup();
- Trace("smt-debug") << "Set up assertions..." << std::endl;
- d_asserts->finishInit();
-
// subsolvers
if (d_env->getOptions().smt.produceAbducts)
{
void SolverEngine::checkModel(bool hardFailure)
{
const context::CDList<Node>& al = d_asserts->getAssertionList();
- // --check-model implies --produce-assertions, which enables the
- // assertion list, so we should be ok.
- Assert(d_env->getOptions().smt.produceAssertions)
- << "don't have an assertion list to check in SolverEngine::checkModel()";
+ // we always enable the assertion list, so it is able to be checked
TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
finishInit();
d_state->doPendingPops();
Trace("smt") << "SMT getAssertions()" << endl;
- if (!d_env->getOptions().smt.produceAssertions)
- {
- const char* msg =
- "Cannot query the current assertion list when not in "
- "produce-assertions mode.";
- throw ModalException(msg);
- }
+ // note we always enable assertions, so it is available here
return getAssertionsInternal();
}
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
d_solver.assertFormula(x.eqTerm(x));
d_solver.checkSat();
- ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException);
+ ASSERT_NO_THROW(d_solver.blockModelValues({x}));
}
TEST_F(TestApiBlackSolver, blockModelValues3)
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
d_solver.assertFormula(x.eqTerm(x));
d_solver.checkSat();
- assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x}));
+ assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x}));
}
@Test void blockModelValues3() throws CVC5ApiException
projects / cvc5.git / commitdiff