/*! \file quantifiers_engine.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Morgan Deters, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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
**
#include "theory/quantifiers_engine.h"
+#include "options/printer_options.h"
#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
#include "options/uf_options.h"
+#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/anti_skolem.h"
-#include "theory/quantifiers/conjecture_generator.h"
-#include "theory/quantifiers/ematching/instantiation_engine.h"
-#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/quantifiers/fmf/full_model_check.h"
-#include "theory/quantifiers/fmf/model_engine.h"
-#include "theory/quantifiers/inst_propagator.h"
-#include "theory/quantifiers/inst_strategy_enumerative.h"
-#include "theory/quantifiers/local_theory_ext.h"
-#include "theory/quantifiers/quant_conflict_find.h"
-#include "theory/quantifiers/quant_split.h"
+#include "theory/quantifiers/quantifiers_modules.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/sygus/synth_engine.h"
-#include "theory/sep/theory_sep.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
namespace CVC4 {
namespace theory {
-class QuantifiersEnginePrivate
-{
- public:
- QuantifiersEnginePrivate()
- : d_inst_prop(nullptr),
- d_rel_dom(nullptr),
- d_alpha_equiv(nullptr),
- d_inst_engine(nullptr),
- d_model_engine(nullptr),
- d_bint(nullptr),
- d_qcf(nullptr),
- d_sg_gen(nullptr),
- d_synth_e(nullptr),
- d_lte_part_inst(nullptr),
- d_fs(nullptr),
- d_i_cbqi(nullptr),
- d_qsplit(nullptr),
- d_anti_skolem(nullptr)
- {
- }
- ~QuantifiersEnginePrivate() {}
- //------------------------------ private quantifier utilities
- /** quantifiers instantiation propagator */
- std::unique_ptr<quantifiers::InstPropagator> d_inst_prop;
- /** relevant domain */
- std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
- //------------------------------ end private quantifier utilities
- //------------------------------ quantifiers modules
- /** alpha equivalence */
- std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv;
- /** instantiation engine */
- std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine;
- /** model engine */
- std::unique_ptr<quantifiers::ModelEngine> d_model_engine;
- /** bounded integers utility */
- std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
- /** Conflict find mechanism for quantifiers */
- std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
- /** subgoal generator */
- std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
- /** ceg instantiation */
- std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
- /** lte partial instantiation */
- std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst;
- /** full saturation */
- std::unique_ptr<quantifiers::InstStrategyEnum> d_fs;
- /** counterexample-based quantifier instantiation */
- std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi;
- /** quantifiers splitting */
- std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
- /** quantifiers anti-skolemization */
- std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
- //------------------------------ end quantifiers modules
- /** initialize
- *
- * This constructs the above modules based on the current options. It adds
- * a pointer to each module it constructs to modules. This method sets
- * needsBuilder to true if we require a strategy-specific model builder
- * utility.
- */
- void initialize(QuantifiersEngine* qe,
- context::Context* c,
- std::vector<QuantifiersModule*>& modules,
- bool& needsBuilder)
- {
- // add quantifiers modules
- if (options::quantConflictFind())
- {
- d_qcf.reset(new quantifiers::QuantConflictFind(qe, c));
- modules.push_back(d_qcf.get());
- }
- if (options::conjectureGen())
- {
- d_sg_gen.reset(new quantifiers::ConjectureGenerator(qe, c));
- modules.push_back(d_sg_gen.get());
- }
- if (!options::finiteModelFind() || options::fmfInstEngine())
- {
- d_inst_engine.reset(new quantifiers::InstantiationEngine(qe));
- modules.push_back(d_inst_engine.get());
- }
- if (options::cbqi())
- {
- d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe));
- modules.push_back(d_i_cbqi.get());
- qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
- }
- if (options::ceGuidedInst())
- {
- d_synth_e.reset(new quantifiers::SynthEngine(qe, c));
- modules.push_back(d_synth_e.get());
- }
- // finite model finding
- if (options::fmfBound())
- {
- d_bint.reset(new quantifiers::BoundedIntegers(c, qe));
- modules.push_back(d_bint.get());
- }
- if (options::finiteModelFind() || options::fmfBound())
- {
- d_model_engine.reset(new quantifiers::ModelEngine(c, qe));
- modules.push_back(d_model_engine.get());
- // finite model finder has special ways of building the model
- needsBuilder = true;
- }
- if (options::ltePartialInst())
- {
- d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c));
- modules.push_back(d_lte_part_inst.get());
- }
- if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
- {
- d_qsplit.reset(new quantifiers::QuantDSplit(qe, c));
- modules.push_back(d_qsplit.get());
- }
- if (options::quantAntiSkolem())
- {
- d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(qe));
- modules.push_back(d_anti_skolem.get());
- }
- if (options::quantAlphaEquiv())
- {
- d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(qe));
- }
- // full saturation : instantiate from relevant domain, then arbitrary terms
- if (options::fullSaturateQuant() || options::fullSaturateInterleave())
- {
- d_rel_dom.reset(new quantifiers::RelevantDomain(qe));
- d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get()));
- modules.push_back(d_fs.get());
- }
- }
-};
-
-QuantifiersEngine::QuantifiersEngine(context::Context* c,
- context::UserContext* u,
- TheoryEngine* te)
- : d_te(te),
- d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
+QuantifiersEngine::QuantifiersEngine(
+ quantifiers::QuantifiersState& qstate,
+ quantifiers::QuantifiersInferenceManager& qim,
+ ProofNodeManager* pnm)
+ : d_qstate(qstate),
+ d_qim(qim),
+ d_te(nullptr),
+ d_decManager(nullptr),
+ d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, this)),
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
d_builder(nullptr),
- d_qepr(nullptr),
- d_term_util(new quantifiers::TermUtil(this)),
- d_term_canon(new expr::TermCanonize),
- d_term_db(new quantifiers::TermDb(c, u, this)),
+ d_term_util(new quantifiers::TermUtil),
+ d_term_db(new quantifiers::TermDb(qstate, qim, this)),
d_sygus_tdb(nullptr),
d_quant_attr(new quantifiers::QuantAttributes(this)),
- d_instantiate(new quantifiers::Instantiate(this, u)),
- d_skolemize(new quantifiers::Skolemize(this, u)),
+ d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)),
+ d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
d_term_enum(new quantifiers::TermEnumeration),
- d_conflict_c(c, false),
- // d_quants(u),
- d_quants_prereg(u),
- d_quants_red(u),
- d_lemmas_produced_c(u),
- d_ierCounter_c(c),
- // d_ierCounter(c),
- // d_ierCounter_lc(c),
- // d_ierCounterLastLc(c),
- d_presolve(u, true),
- d_presolve_in(u),
- d_presolve_cache(u),
- d_presolve_cache_wq(u),
- d_presolve_cache_wic(u)
+ d_quants_prereg(qstate.getUserContext()),
+ d_quants_red(qstate.getUserContext()),
+ d_lemmas_produced_c(qstate.getUserContext()),
+ d_ierCounter_c(qstate.getSatContext()),
+ d_presolve(qstate.getUserContext(), true),
+ d_presolve_in(qstate.getUserContext()),
+ d_presolve_cache(qstate.getUserContext()),
+ d_presolve_cache_wq(qstate.getUserContext()),
+ d_presolve_cache_wic(qstate.getUserContext())
{
- // initialize the private utility
- d_private.reset(new QuantifiersEnginePrivate);
-
//---- utilities
d_util.push_back(d_eq_query.get());
// term util must come before the other utilities
d_util.push_back(d_term_util.get());
d_util.push_back(d_term_db.get());
- if (options::ceGuidedInst()) {
- d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
- }
-
- if( options::instPropagate() ){
- // notice that this option is incompatible with options::qcfAllConflict()
- d_private->d_inst_prop.reset(new quantifiers::InstPropagator(this));
- d_util.push_back(d_private->d_inst_prop.get());
- d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify());
+ if (options::sygus() || options::sygusInst())
+ {
+ // must be constructed here since it is required for datatypes finistInit
+ d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate, qim));
}
-
d_util.push_back(d_instantiate.get());
d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
- d_conflict = false;
d_hasAddedLemma = false;
- d_useModelEe = false;
//don't add true lemma
d_lemmas_produced_c[d_term_util->d_true] = true;
Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
- if( options::quantEpr() ){
- Assert(!options::incrementalSolving());
- d_qepr.reset(new quantifiers::QuantEPR);
- }
//---- end utilities
//allow theory combination to go first, once initially
d_ierCounterLastLc = 0;
d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
- bool needsBuilder = false;
- d_private->initialize(this, c, d_modules, needsBuilder);
-
- if (d_private->d_rel_dom.get())
+ // Finite model finding requires specialized ways of building the model.
+ // We require constructing the model and model builder here, since it is
+ // required for initializing the CombinationEngine.
+ if (options::finiteModelFind() || options::fmfBound())
{
- d_util.push_back(d_private->d_rel_dom.get());
- }
-
- // if we require specialized ways of building the model
- if( needsBuilder ){
Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
if (options::mbqiMode() == options::MbqiMode::FMC
|| options::mbqiMode() == options::MbqiMode::TRUST
{
Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
- this, c, "FirstOrderModelFmc"));
- d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this));
+ this, qstate, "FirstOrderModelFmc"));
+ d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate));
}else{
Trace("quant-engine-debug") << "...make default model builder." << std::endl;
d_model.reset(
- new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
- d_builder.reset(new quantifiers::QModelBuilder(c, this));
+ new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
+ d_builder.reset(new quantifiers::QModelBuilder(this, qstate));
}
}else{
- d_model.reset(new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
+ d_model.reset(
+ new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
}
}
QuantifiersEngine::~QuantifiersEngine() {}
-context::Context* QuantifiersEngine::getSatContext()
+void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
{
- return d_te->theoryOf(THEORY_QUANTIFIERS)->getSatContext();
+ d_te = te;
+ d_decManager = dm;
+ // Initialize the modules and the utilities here.
+ d_qmodules.reset(new quantifiers::QuantifiersModules);
+ d_qmodules->initialize(this, d_qstate, d_qim, d_modules);
+ if (d_qmodules->d_rel_dom.get())
+ {
+ d_util.push_back(d_qmodules->d_rel_dom.get());
+ }
}
-context::UserContext* QuantifiersEngine::getUserContext()
+TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; }
+
+DecisionManager* QuantifiersEngine::getDecisionManager()
{
- return d_te->theoryOf(THEORY_QUANTIFIERS)->getUserContext();
+ return d_decManager;
}
OutputChannel& QuantifiersEngine::getOutputChannel()
{
return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel();
}
-/** get default valuation for the quantifiers engine */
-Valuation& QuantifiersEngine::getValuation()
-{
- return d_te->theoryOf(THEORY_QUANTIFIERS)->getValuation();
-}
+Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); }
-const LogicInfo& QuantifiersEngine::getLogicInfo() const
+quantifiers::QuantifiersState& QuantifiersEngine::getState()
{
- return d_te->getLogicInfo();
+ return d_qstate;
}
-
-EqualityQuery* QuantifiersEngine::getEqualityQuery() const
+quantifiers::QuantifiersInferenceManager&
+QuantifiersEngine::getInferenceManager()
{
- return d_eq_query.get();
+ return d_qim;
}
quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
{
return d_builder.get();
}
-quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const
-{
- return d_qepr.get();
-}
quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
{
return d_model.get();
{
return d_term_util.get();
}
-expr::TermCanonize* QuantifiersEngine::getTermCanonize() const
-{
- return d_term_canon.get();
-}
quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
{
return d_quant_attr.get();
{
if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
{
- if (d_private->d_synth_e.get() == nullptr)
+ if (d_qmodules->d_synth_e.get() == nullptr)
{
Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
<< q << std::endl;
}
// set synth engine as owner since this is either a conjecture or a function
// definition to be used by sygus
- setOwner(q, d_private->d_synth_e.get(), 2);
+ setOwner(q, d_qmodules->d_synth_e.get(), 2);
}
}
bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
{
- quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+ quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
if (bi && bi->isBound(q, v))
{
return true;
BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const
{
- quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+ quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
if (bi)
{
return bi->getBoundVarType(q, v);
{
Assert(indices.empty());
// we take the bounded variables first
- quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+ quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
if (bi)
{
bi->getBoundVarIndices(q, indices);
Node v,
std::vector<Node>& elements) const
{
- quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+ quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
if (bi)
{
return bi->getBoundElements(rsi, initial, q, v, elements);
void QuantifiersEngine::presolve() {
Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
+ d_lemmas_waiting.clear();
+ d_phase_req_waiting.clear();
for( unsigned i=0; i<d_modules.size(); i++ ){
d_modules[i]->presolve();
}
const std::vector<Node>& assertions) {
Trace("quant-engine-proc")
<< "ppNotifyAssertions in QE, #assertions = " << assertions.size()
- << " check epr = " << (d_qepr != NULL) << std::endl;
+ << std::endl;
if (options::instLevelInputOnly() && options::instMaxLevel() != -1)
{
for (const Node& a : assertions)
quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0);
}
}
- if (d_qepr != NULL)
+ if (options::sygus())
{
+ quantifiers::SynthEngine* sye = d_qmodules->d_synth_e.get();
for (const Node& a : assertions)
{
- d_qepr->registerAssertion(a);
+ sye->preregisterAssertion(a);
}
- // must handle sources of other new constants e.g. separation logic
- // FIXME (as part of project 3) : cleanup
- sep::TheorySep* theory_sep =
- static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP));
- theory_sep->initializeBounds();
- d_qepr->finishInit();
}
- if (options::ceGuidedInst())
+ /* The SyGuS instantiation module needs a global view of all available
+ * assertions to collect global terms that get added to each grammar.
+ */
+ if (options::sygusInst())
{
- quantifiers::SynthEngine* sye = d_private->d_synth_e.get();
- for (const Node& a : assertions)
- {
- sye->preregisterAssertion(a);
- }
+ quantifiers::SygusInst* si = d_qmodules->d_sygus_inst.get();
+ si->ppNotifyAssertions(assertions);
}
}
void QuantifiersEngine::check( Theory::Effort e ){
CodeTimer codeTimer(d_statistics.d_time);
- d_useModelEe = options::quantModelEe() && ( e>=Theory::EFFORT_LAST_CALL );
- // if we want to use the model's equality engine, build the model now
- if( d_useModelEe && !d_model->isBuilt() ){
- Trace("quant-engine-debug") << "Build the model." << std::endl;
- if (!d_te->getModelBuilder()->buildModel(d_model.get()))
- {
- //we are done if model building was unsuccessful
- flushLemmas();
- if( d_hasAddedLemma ){
- Trace("quant-engine-debug") << "...failed." << std::endl;
- return;
- }
- }
- }
-
- if( !getActiveEqualityEngine()->consistent() ){
+ Assert(d_qstate.getEqualityEngine() != nullptr);
+ if (!d_qstate.getEqualityEngine()->consistent())
+ {
Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
return;
}
- if (d_conflict_c.get())
+ if (d_qstate.isInConflict())
{
if (e < Theory::EFFORT_LAST_CALL)
{
}
}
- d_conflict = false;
d_hasAddedLemma = false;
bool setIncomplete = false;
Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
if( needsCheck ){
- //flush previous lemmas (for instance, if was interupted), or other lemmas to process
+ //flush previous lemmas (for instance, if was interrupted), or other lemmas to process
flushLemmas();
if( d_hasAddedLemma ){
return;
}
-
+
double clSet = 0;
if( Trace.isOn("quant-engine") ){
clSet = double(clock())/double(CLOCKS_PER_SEC);
Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
}
Trace("quant-engine-debug")
- << " Theory engine finished : " << !theoryEngineNeedsCheck()
- << std::endl;
+ << " Theory engine finished : "
+ << !d_qstate.getValuation().needCheck() << std::endl;
Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl;
+ Trace("quant-engine-debug")
+ << " In conflict : " << d_qstate.isInConflict() << std::endl;
}
if( Trace.isOn("quant-engine-ee-pre") ){
Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
QuantifiersModule::QEffort quant_e =
static_cast<QuantifiersModule::QEffort>(qef);
d_curr_effort_level = quant_e;
- //build the model if any module requested it
+ // Force the theory engine to build the model if any module requested it.
if (needsModelE == quant_e)
{
- if (!d_model->isBuilt())
- {
- // theory engine's model builder is quantifier engine's builder if it
- // has one
- Assert(!getModelBuilder()
- || getModelBuilder() == d_te->getModelBuilder());
- Trace("quant-engine-debug") << "Build model..." << std::endl;
- if (!d_te->getModelBuilder()->buildModel(d_model.get()))
- {
- flushLemmas();
- }
- }
- if (!d_model->isBuiltSuccess())
+ Trace("quant-engine-debug") << "Build model..." << std::endl;
+ if (!d_te->buildModel())
{
+ // If we failed to build the model, flush all pending lemmas and
+ // finish.
+ flushLemmas();
break;
}
}
<< " at effort " << quant_e << "..."
<< std::endl;
mdl->check(e, quant_e);
- if( d_conflict ){
+ if (d_qstate.isInConflict())
+ {
Trace("quant-engine-debug") << "...conflict!" << std::endl;
break;
}
if( d_hasAddedLemma ){
break;
}else{
- Assert(!d_conflict);
+ Assert(!d_qstate.isInConflict());
if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
{
if( e==Theory::EFFORT_FULL ){
setIncomplete = true;
}
}
- if (d_conflict_c.get())
+ if (d_qstate.isInConflict())
{
// we reported a conflicting lemma, should return
setIncomplete = true;
}
d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
- if( d_hasAddedLemma ){
- d_instantiate->debugPrint();
+ // debug print
+ if (d_hasAddedLemma)
+ {
+ bool debugInstTrace = Trace.isOn("inst-per-quant-round");
+ if (options::debugInst() || debugInstTrace)
+ {
+ Options& sopts = smt::currentSmtEngine()->getOptions();
+ std::ostream& out = *sopts.getOut();
+ d_instantiate->debugPrint(out);
+ }
}
if( Trace.isOn("quant-engine") ){
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
Trace("quant-engine") << std::endl;
}
-
+
Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
}else{
Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
Node lem;
std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
if( itr==d_quants_red_lem.end() ){
- if (d_private->d_alpha_equiv)
+ if (d_qmodules->d_alpha_equiv)
{
Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
//add equivalence with another quantified formula
- lem = d_private->d_alpha_equiv->reduceQuantifier(q);
+ lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
if( !lem.isNull() ){
Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
++(d_statistics.d_red_alpha_equiv);
Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
}
-void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
- for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
- std::set< Node > added;
- getTermDatabase()->addTerm( *p, added );
- }
-}
-
void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
if (reduceQuantifier(f))
{
}
if( !pol ){
// do skolemization
- Node lem = d_skolemize->process(f);
+ TrustNode lem = d_skolemize->process(f);
if (!lem.isNull())
{
if (Trace.isOn("quantifiers-sk-debug"))
{
- Node slem = Rewriter::rewrite(lem);
+ Node slem = Rewriter::rewrite(lem.getNode());
Trace("quantifiers-sk-debug")
<< "Skolemize lemma : " << slem << std::endl;
}
- getOutputChannel().lemma(lem, false, true);
+ getOutputChannel().trustedLemma(lem, LemmaProperty::NEEDS_JUSTIFY);
}
return;
}
if (!withinQuant)
{
- if (d_sygus_tdb)
+ if (d_sygus_tdb && options::sygusEvalUnfold())
{
d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
}
Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
- //d_curr_out->lemma( lem, false, true );
d_lemmas_produced_c[ lem ] = true;
d_lemmas_waiting.push_back( lem );
Trace("inst-add-debug") << "Added lemma" << std::endl;
}
}
+bool QuantifiersEngine::addTrustedLemma(TrustNode tlem,
+ bool doCache,
+ bool doRewrite)
+{
+ Node lem = tlem.getProven();
+ if (!addLemma(lem, doCache, doRewrite))
+ {
+ return false;
+ }
+ d_lemmasWaitingPg[lem] = tlem.getGenerator();
+ return true;
+}
+
bool QuantifiersEngine::removeLemma( Node lem ) {
std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
if( it!=d_lemmas_waiting.end() ){
void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
d_phase_req_waiting[lit] = req;
}
-
+
void QuantifiersEngine::markRelevant( Node q ) {
d_model->markRelevant( q );
}
+
bool QuantifiersEngine::hasAddedLemma() const
{
return !d_lemmas_waiting.empty() || d_hasAddedLemma;
}
-bool QuantifiersEngine::theoryEngineNeedsCheck() const
-{
- return d_te->needCheck();
-}
-
-void QuantifiersEngine::setConflict() {
- d_conflict = true;
- d_conflict_c = true;
-}
bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
}
else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
{
- performCheck = (e >= Theory::EFFORT_FULL) && !theoryEngineNeedsCheck();
+ performCheck =
+ (e >= Theory::EFFORT_FULL) && !d_qstate.getValuation().needCheck();
}
else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
{
else if (options::instWhenMode()
== options::InstWhenMode::FULL_DELAY_LAST_CALL)
{
- performCheck = ((e == Theory::EFFORT_FULL && !theoryEngineNeedsCheck()
- && d_ierCounter % d_inst_when_phase != 0)
- || e == Theory::EFFORT_LAST_CALL);
+ performCheck =
+ ((e == Theory::EFFORT_FULL && !d_qstate.getValuation().needCheck()
+ && d_ierCounter % d_inst_when_phase != 0)
+ || e == Theory::EFFORT_LAST_CALL);
}
else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
{
{
performCheck = true;
}
- if( e==Theory::EFFORT_LAST_CALL ){
- //with bounded integers, skip every other last call,
- // since matching loops may occur with infinite quantification
- if( d_ierCounter_lc%2==0 && options::fmfBound() ){
- performCheck = false;
- }
- }
return performCheck;
}
}
void QuantifiersEngine::flushLemmas(){
+ OutputChannel& out = getOutputChannel();
if( !d_lemmas_waiting.empty() ){
- //filter based on notify classes
- if (d_instantiate->hasNotify())
- {
- unsigned prev_lem_sz = d_lemmas_waiting.size();
- d_instantiate->notifyFlushLemmas();
- if( prev_lem_sz!=d_lemmas_waiting.size() ){
- Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
- }
- }
//take default output channel if none is provided
d_hasAddedLemma = true;
- for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
- Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
- getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
+ std::map<Node, ProofGenerator*>::iterator itp;
+ // Note: Do not use foreach loop here and do not cache size() call.
+ // New lemmas can be added while iterating over d_lemmas_waiting.
+ for (size_t i = 0; i < d_lemmas_waiting.size(); ++i)
+ {
+ const Node& lemw = d_lemmas_waiting[i];
+ Trace("qe-lemma") << "Lemma : " << lemw << std::endl;
+ itp = d_lemmasWaitingPg.find(lemw);
+ LemmaProperty p = LemmaProperty::NEEDS_JUSTIFY;
+ if (itp != d_lemmasWaitingPg.end())
+ {
+ TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second);
+ out.trustedLemma(tlemw, p);
+ }
+ else
+ {
+ out.lemma(lemw, p);
+ }
}
d_lemmas_waiting.clear();
}
if( !d_phase_req_waiting.empty() ){
for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
- getOutputChannel().requirePhase( it->first, it->second );
+ out.requirePhase(it->first, it->second);
}
d_phase_req_waiting.clear();
}
}
-bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
- return d_instantiate->getUnsatCoreLemmas(active_lemmas);
-}
-
-bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) {
- return d_instantiate->getUnsatCoreLemmas(active_lemmas, weak_imp);
-}
-
void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
d_instantiate->getInstantiationTermVectors(q, tvecs);
}
d_instantiate->getInstantiationTermVectors(insts);
}
-void QuantifiersEngine::getExplanationForInstLemmas(
- const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec)
-{
- d_instantiate->getExplanationForInstLemmas(lems, quant, tvec);
-}
-
-void QuantifiersEngine::printInstantiations( std::ostream& out ) {
- bool printed = false;
- // print the skolemizations
- if (d_skolemize->printSkolemization(out))
- {
- printed = true;
- }
- // print the instantiations
- if (d_instantiate->printInstantiations(out))
- {
- printed = true;
- }
- if( !printed ){
- out << "No instantiations" << std::endl;
- }
-}
-
void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
- if (d_private->d_synth_e)
+ if (d_qmodules->d_synth_e)
{
- d_private->d_synth_e->printSynthSolution(out);
+ d_qmodules->d_synth_e->printSynthSolution(out);
}else{
out << "Internal error : module for synth solution not found." << std::endl;
}
}
-void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
+void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+{
d_instantiate->getInstantiatedQuantifiedFormulas(qs);
}
-void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
- d_instantiate->getInstantiations(insts);
-}
-
-void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
- d_instantiate->getInstantiations(q, insts);
-}
-
-Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
- return d_instantiate->getInstantiatedConjunction(q);
+void QuantifiersEngine::getSkolemTermVectors(
+ std::map<Node, std::vector<Node> >& sks) const
+{
+ d_skolemize->getSkolemTermVectors(sks);
}
QuantifiersEngine::Statistics::Statistics()
smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
}
-eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const
-{
- return d_te->getMasterEqualityEngine();
+Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
+ return d_eq_query->getInternalRepresentative(a, q, index);
}
-eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() const
+Node QuantifiersEngine::getNameForQuant(Node q) const
{
- if( d_useModelEe ){
- return d_model->getEqualityEngine();
+ Node name = d_quant_attr->getQuantName(q);
+ if (!name.isNull())
+ {
+ return name;
}
- return d_te->getMasterEqualityEngine();
+ return q;
}
-Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
- bool prevModelEe = d_useModelEe;
- d_useModelEe = false;
- Node ret = d_eq_query->getInternalRepresentative( a, q, index );
- d_useModelEe = prevModelEe;
- return ret;
+bool QuantifiersEngine::getNameForQuant(Node q, Node& name, bool req) const
+{
+ name = getNameForQuant(q);
+ // if we have a name, or we did not require one
+ return name != q || !req;
}
bool QuantifiersEngine::getSynthSolutions(
std::map<Node, std::map<Node, Node> >& sol_map)
{
- return d_private->d_synth_e->getSynthSolutions(sol_map);
+ return d_qmodules->d_synth_e->getSynthSolutions(sol_map);
}
void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
- eq::EqualityEngine* ee = getActiveEqualityEngine();
+ eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
std::map< TypeNode, int > typ_num;
while( !eqcs_i.isFinished() ){
projects / cvc5.git / blobdiff