Towards eliminating dependencies on quantifiers engine.
This replaces the custom implementation of lemma management in quantifiers engine with the standard one.
It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers.
Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact.
class Command;
class CommandStatus;
class UnsatCore;
-class InstantiationList;
-class SkolemList;
+struct InstantiationList;
+struct SkolemList;
class Printer
{
return !d_pendingLem.empty();
}
-void InferenceManagerBuffered::addPendingLemma(Node lem,
+bool InferenceManagerBuffered::addPendingLemma(Node lem,
LemmaProperty p,
- ProofGenerator* pg)
+ ProofGenerator* pg,
+ bool checkCache)
{
+ if (checkCache)
+ {
+ // check if it is unique up to rewriting
+ Node lemr = Rewriter::rewrite(lem);
+ if (hasCachedLemma(lemr, p))
+ {
+ return false;
+ }
+ }
// make the simple theory lemma
d_pendingLem.emplace_back(new SimpleTheoryLemma(lem, p, pg));
+ return true;
}
void InferenceManagerBuffered::addPendingLemma(
* non-null, pg must be able to provide a proof for lem for the remainder
* of the user context. Pending lemmas are sent to the output channel using
* doPendingLemmas.
+ *
+ * @param lem The lemma to send
+ * @param p The property of the lemma
+ * @param pg The proof generator which can provide a proof for lem
+ * @param checkCache Whether we want to check that the lemma is already in
+ * the cache.
+ * @return true if the lemma was added to the list of pending lemmas and
+ * false if the lemma is already cached.
*/
- void addPendingLemma(Node lem,
+ bool addPendingLemma(Node lem,
LemmaProperty p = LemmaProperty::NONE,
- ProofGenerator* pg = nullptr);
+ ProofGenerator* pg = nullptr,
+ bool checkCache = true);
/**
* Add pending lemma, where lemma can be a (derived) class of the
* theory inference base class.
}
Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl;
bool ret = d_parent->doAddInstantiation(subs);
- for( unsigned i=0; i<lemmas.size(); i++ ){
- d_parent->addLemma(lemmas[i]);
+ for (const Node& l : lemmas)
+ {
+ d_parent->addPendingLemma(l);
}
return ret;
}
//add counterexample lemma
Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
//require any decision on cel to be phase=true
- d_quantEngine->addRequirePhase( ceLit, true );
+ d_qim.addPendingPhaseRequirement(ceLit, true);
Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
//add counterexample lemma
lem = Rewriter::rewrite( lem );
clSet = double(clock())/double(CLOCKS_PER_SEC);
Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
}
- unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+ size_t lastWaiting = d_qim.numPendingLemmas();
for( int ee=0; ee<=1; ee++ ){
//for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
// Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
break;
}
}
- if (d_qstate.isInConflict()
- || d_quantEngine->getNumLemmasWaiting() > lastWaiting)
+ if (d_qstate.isInConflict() || d_qim.numPendingLemmas() > lastWaiting)
{
break;
}
}
if( Trace.isOn("cegqi-engine") ){
- if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
- Trace("cegqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+ if (d_qim.numPendingLemmas() > lastWaiting)
+ {
+ Trace("cegqi-engine")
+ << "Added lemmas = " << (d_qim.numPendingLemmas() - lastWaiting)
+ << std::endl;
}
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
{
Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
<< std::endl;
- d_quantEngine->addLemma(auxLems[i], false);
+ d_qim.addPendingLemma(auxLems[i]);
}
}
}
}
-bool InstStrategyCegqi::addLemma( Node lem ) {
- return d_quantEngine->addLemma( lem );
+bool InstStrategyCegqi::addPendingLemma(Node lem) const
+{
+ return d_qim.addPendingLemma(lem);
}
-
CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
d_cinst.find(q);
// add lemmas to process
for (const Node& lem : lems)
{
- d_quantEngine->addLemma(lem);
+ d_qim.addPendingLemma(lem);
}
// don't need to process this, since it has been reduced
return true;
//------------------- interface for CegqiOutputInstStrategy
/** Instantiate the current quantified formula forall x. Q with x -> subs. */
bool doAddInstantiation(std::vector<Node>& subs);
- /** Add lemma lem via the output channel of this class. */
- bool addLemma(Node lem);
+ /** Add pending lemma lem via the inference manager of this class. */
+ bool addPendingLemma(Node lem) const;
//------------------- end interface for CegqiOutputInstStrategy
protected:
std::vector< Node > lem;
getEnumeratePredUfTerm( n, options::conjectureGenGtEnum(), lem );
if( !lem.empty() ){
- for( unsigned j=0; j<lem.size(); j++ ){
- d_quantEngine->addLemma( lem[j], false );
- d_hasAddedLemma = true;
+ for (const Node& l : lem)
+ {
+ d_qim.addPendingLemma(l);
}
+ d_hasAddedLemma = true;
return false;
}
}
d_eq_conjectures[rhs].push_back( lhs );
Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg );
- d_quantEngine->addLemma( lem, false );
- d_quantEngine->addRequirePhase( rsg, false );
+ d_qim.addPendingLemma(lem);
+ d_qim.addPendingPhaseRequirement(rsg, false);
addedLemmas++;
if( (int)addedLemmas>=options::conjectureGenPerRound() ){
break;
HigherOrderTrigger::HigherOrderTrigger(
QuantifiersEngine* qe,
+ quantifiers::QuantifiersInferenceManager& qim,
Node q,
std::vector<Node>& nodes,
std::map<Node, std::vector<Node> >& ho_apps)
- : Trigger(qe, q, nodes), d_ho_var_apps(ho_apps)
+ : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps)
{
NodeManager* nm = NodeManager::currentNM();
// process the higher-order variable applications
{
Node u = tdb->getHoTypeMatchPredicate(tn);
Node au = nm->mkNode(kind::APPLY_UF, u, f);
- if (d_quantEngine->addLemma(au))
+ if (d_qim.addPendingLemma(au))
{
// this forces f to be a first-class member of the quantifier-free
// equality engine, which in turn forces the quantifier-free
private:
HigherOrderTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersInferenceManager& qim,
Node q,
std::vector<Node>& nodes,
std::map<Node, std::vector<Node> >& ho_apps);
namespace quantifiers {
class QuantifiersState;
+class QuantifiersInferenceManager;
/** A status response to process */
enum class InstStrategyStatus
class InstStrategy
{
public:
- InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs)
- : d_quantEngine(qe), d_qstate(qs)
+ InstStrategy(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim)
+ : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
{
}
virtual ~InstStrategy() {}
QuantifiersEngine* d_quantEngine;
/** The quantifiers state object */
QuantifiersState& d_qstate;
+ /** The quantifiers inference manager object */
+ QuantifiersInferenceManager& d_qim;
}; /* class InstStrategy */
} // namespace quantifiers
}
};
-InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantRelevance* qr)
- : InstStrategy(qe, qs), d_quant_rel(qr)
+InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(
+ QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantRelevance* qr)
+ : InstStrategy(qe, qs, qim), d_quant_rel(qr)
{
//how to select trigger terms
d_tr_strategy = options::triggerSelMode();
if (d_is_single_trigger[patTerms[0]])
{
tr = Trigger::mkTrigger(d_quantEngine,
+ d_qim,
f,
patTerms[0],
false,
}
// will possibly want to get an old trigger
tr = Trigger::mkTrigger(d_quantEngine,
+ d_qim,
f,
patTerms,
false,
{
d_single_trigger_gen[patTerms[index]] = true;
Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
+ d_qim,
f,
patTerms[index],
false,
<< "Make partially specified user pattern: " << std::endl;
Trace("auto-gen-trigger-partial") << " " << qq << std::endl;
Node lem = nm->mkNode(OR, q.negate(), qq);
- d_quantEngine->addLemma(lem);
+ d_qim.addPendingLemma(lem);
return;
}
unsigned tindex;
public:
InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
QuantRelevance* qr);
~InstStrategyAutoGenTriggers() {}
namespace theory {
namespace quantifiers {
-InstStrategyUserPatterns::InstStrategyUserPatterns(QuantifiersEngine* ie,
- QuantifiersState& qs)
- : InstStrategy(ie, qs)
+InstStrategyUserPatterns::InstStrategyUserPatterns(
+ QuantifiersEngine* ie,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim)
+ : InstStrategy(ie, qs, qim)
{
}
InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
for (size_t i = 0, usize = ugw.size(); i < usize; i++)
{
Trigger* t = Trigger::mkTrigger(
- d_quantEngine, q, ugw[i], true, Trigger::TR_RETURN_NULL);
+ d_quantEngine, d_qim, q, ugw[i], true, Trigger::TR_RETURN_NULL);
if (t)
{
d_user_gen[q].push_back(t);
d_user_gen_wait[q].push_back(nodes);
return;
}
- Trigger* t =
- Trigger::mkTrigger(d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW);
+ Trigger* t = Trigger::mkTrigger(
+ d_quantEngine, d_qim, q, nodes, true, Trigger::TR_MAKE_NEW);
if (t)
{
d_user_gen[q].push_back(t);
class InstStrategyUserPatterns : public InstStrategy
{
public:
- InstStrategyUserPatterns(QuantifiersEngine* qe, QuantifiersState& qs);
+ InstStrategyUserPatterns(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim);
~InstStrategyUserPatterns();
/** add pattern */
void addUserPattern(Node q, Node pat);
// user-provided patterns
if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
{
- d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs));
+ d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim));
d_instStrategies.push_back(d_isup.get());
}
// auto-generated patterns
- d_i_ag.reset(
- new InstStrategyAutoGenTriggers(d_quantEngine, qs, d_quant_rel.get()));
+ d_i_ag.reset(new InstStrategyAutoGenTriggers(
+ d_quantEngine, qs, qim, d_quant_rel.get()));
d_instStrategies.push_back(d_i_ag.get());
}
}
}
void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
- unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+ size_t lastWaiting = d_qim.numPendingLemmas();
//iterate over an internal effort level e
int e = 0;
int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
}
}
//do not consider another level if already added lemma at this level
- if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+ if (d_qim.numPendingLemmas() > lastWaiting)
+ {
finished = true;
}
e++;
Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl;
if (quantActive)
{
- unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+ size_t lastWaiting = d_qim.numPendingLemmas();
doInstantiationRound(e);
if (d_qstate.isInConflict())
{
- Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting);
+ Assert(d_qim.numPendingLemmas() > lastWaiting);
Trace("inst-engine") << "Conflict, added lemmas = "
- << (d_quantEngine->getNumLemmasWaiting()
- - lastWaiting)
+ << (d_qim.numPendingLemmas() - lastWaiting)
<< std::endl;
}
- else if (d_quantEngine->hasAddedLemma())
+ else if (d_qim.hasPendingLemma())
{
Trace("inst-engine") << "Added lemmas = "
- << (d_quantEngine->getNumLemmasWaiting()
- - lastWaiting)
+ << (d_qim.numPendingLemmas() - lastWaiting)
<< std::endl;
}
}
#include "theory/quantifiers/ematching/pattern_term_selector.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
namespace inst {
/** trigger class constructor */
-Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
- : d_quantEngine(qe), d_quant(q)
+Trigger::Trigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersInferenceManager& qim,
+ Node q,
+ std::vector<Node>& nodes)
+ : d_quantEngine(qe), d_qim(qim), d_quant(q)
{
// We must ensure that the ground subterms of the trigger have been
// preprocessed.
Node eq = k.eqNode(gt);
Trace("trigger-gt-lemma")
<< "Trigger: ground term purify lemma: " << eq << std::endl;
- d_quantEngine->addLemma(eq);
+ d_qim.addPendingLemma(eq);
gtAddedLemmas++;
}
}
}
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersInferenceManager& qim,
Node f,
std::vector<Node>& nodes,
bool keepAll,
Trigger* t;
if (!ho_apps.empty())
{
- t = new HigherOrderTrigger(qe, f, trNodes, ho_apps);
+ t = new HigherOrderTrigger(qe, qim, f, trNodes, ho_apps);
}
else
{
- t = new Trigger(qe, f, trNodes);
+ t = new Trigger(qe, qim, f, trNodes);
}
qe->getTriggerDatabase()->addTrigger( trNodes, t );
}
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersInferenceManager& qim,
Node f,
Node n,
bool keepAll,
{
std::vector< Node > nodes;
nodes.push_back( n );
- return mkTrigger(qe, f, nodes, keepAll, trOption, useNVars);
+ return mkTrigger(qe, qim, f, nodes, keepAll, trOption, useNVars);
}
int Trigger::getActiveScore() {
class QuantifiersEngine;
+namespace quantifiers {
+class QuantifiersInferenceManager;
+}
+
namespace inst {
class IMGenerator;
class InstMatchGenerator;
-
/** A collection of nodes representing a trigger.
*
* This class encapsulates all implementations of E-matching in CVC4.
TR_RETURN_NULL //return null if a duplicate is found
};
static Trigger* mkTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersInferenceManager& qim,
Node q,
std::vector<Node>& nodes,
bool keepAll = true,
size_t useNVars = 0);
/** single trigger version that calls the above function */
static Trigger* mkTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersInferenceManager& qim,
Node q,
Node n,
bool keepAll = true,
protected:
/** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
- Trigger(QuantifiersEngine* ie, Node q, std::vector<Node>& nodes);
+ Trigger(QuantifiersEngine* ie,
+ quantifiers::QuantifiersInferenceManager& qim,
+ Node q,
+ std::vector<Node>& nodes);
/** add an instantiation (called by InstMatchGenerator)
*
* This calls Instantiate::addInstantiation(...) for instantiations
std::vector<Node> d_groundTerms;
/** The quantifiers engine associated with this trigger. */
QuantifiersEngine* d_quantEngine;
+ /** Reference to the quantifiers inference manager */
+ quantifiers::QuantifiersInferenceManager& d_qim;
/** The quantified formula this trigger is for. */
Node d_quant;
/** match generator
{
Trace("bound-int-lemma")
<< "*** bound int : proxy lemma : " << prangeLem << std::endl;
- d_quantEngine->addLemma(prangeLem);
+ d_qim.addPendingLemma(prangeLem);
addedLemma = true;
}
}
{
bool doCheck = false;
if( options::mbqiInterleave() ){
- doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
+ doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
}
if( !doCheck ){
doCheck = quant_e == QEFFORT_MODEL;
if (options::fullSaturateInterleave())
{
// we only add when interleaved with other strategies
- doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
+ doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
}
if (options::fullSaturateQuant() && !doCheck)
{
Instantiate::Instantiate(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
ProofNodeManager* pnm)
: d_qe(qe),
d_qstate(qs),
+ d_qim(qim),
d_pnm(pnm),
d_term_db(nullptr),
d_term_util(nullptr),
bool addedLem = false;
if (hasProof)
{
- // use trust interface
- TrustNode tlem = TrustNode::mkTrustLemma(lem, d_pfInst.get());
- addedLem = d_qe->addTrustedLemma(tlem, true, false);
+ // use proof generator
+ addedLem = d_qim.addPendingLemma(lem, LemmaProperty::NONE, d_pfInst.get());
}
else
{
- addedLem = d_qe->addLemma(lem, true, false);
+ addedLem = d_qim.addPendingLemma(lem);
}
if (!addedLem)
return true;
}
-bool Instantiate::removeInstantiation(Node q,
- Node lem,
- std::vector<Node>& terms)
-{
- // lem must occur in d_waiting_lemmas
- if (d_qe->removeLemma(lem))
- {
- return removeInstantiationInternal(q, terms);
- }
- return false;
-}
-
bool Instantiate::recordInstantiation(Node q,
std::vector<Node>& terms,
bool modEq,
*
* Its main interface is ::addInstantiation(...), which is called by many of
* the quantifiers modules, which enqueues instantiation lemmas in quantifiers
- * engine via calls to QuantifiersEngine::addLemma.
+ * engine via calls to QuantifiersInferenceManager::addPendingLemma.
*
* It also has utilities for constructing instantiations, and interfaces for
* getting the results of the instantiations produced during check-sat calls.
public:
Instantiate(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
ProofNodeManager* pnm = nullptr);
~Instantiate();
*
* This function returns true if the instantiation lemma for quantified
* formula q for the substitution specified by m is successfully enqueued
- * via a call to QuantifiersEngine::addLemma.
+ * via a call to QuantifiersInferenceManager::addPendingLemma.
* mkRep : whether to take the representatives of the terms in the range of
* the substitution m,
* modEq : whether to check for duplication modulo equality in instantiation
QuantifiersEngine* d_qe;
/** Reference to the quantifiers state */
QuantifiersState& d_qstate;
+ /** Reference to the quantifiers inference manager */
+ QuantifiersInferenceManager& d_qim;
/** pointer to the proof node manager */
ProofNodeManager* d_pnm;
/** cache of term database for quantifiers engine */
*
* This method attempts to construct a conflicting or propagating instance.
* If such an instance exists, then it makes a call to
- * Instantiation::addInstantiation or QuantifiersEngine::addLemma.
+ * Instantiation::addInstantiation.
*/
void check(Theory::Effort level, QEffort quant_e) override;
for (const Node& lem : lemmas)
{
Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
- d_quantEngine->addLemma(lem, false);
+ d_qim.addPendingLemma(lem);
}
Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
}
QuantifiersUtil(){}
virtual ~QuantifiersUtil(){}
/* reset
- * Called at the beginning of an instantiation round
- * Returns false if the reset failed. When reset fails, the utility should have
- * added a lemma via a call to qe->addLemma. TODO: improve this contract #1163
- */
+ * Called at the beginning of an instantiation round
+ * Returns false if the reset failed. When reset fails, the utility should
+ * have added a lemma via a call to d_qim.addPendingLemma.
+ */
virtual bool reset( Theory::Effort e ) = 0;
/* Called for new quantifiers */
virtual void registerQuantifier(Node q) = 0;
QuantifiersInferenceManager::~QuantifiersInferenceManager() {}
+void QuantifiersInferenceManager::doPending()
+{
+ doPendingLemmas();
+ doPendingPhaseRequirements();
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
QuantifiersState& state,
ProofNodeManager* pnm);
~QuantifiersInferenceManager();
+ /**
+ * Do all pending lemmas, then do all pending phase requirements.
+ */
+ void doPending();
};
} // namespace quantifiers
SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
SygusStatistics& s)
: d_qe(qe),
d_qstate(qs),
+ d_qim(qim),
d_stats(s),
d_tds(qe->getTermDatabaseSygus()),
d_hasSolution(false),
{
Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem
<< std::endl;
- bool res = d_qe->addLemma(lem);
+ bool res = d_qim.addPendingLemma(lem);
if (res)
{
++(d_stats.d_cegqi_lemmas_refine);
public:
SynthConjecture(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
SygusStatistics& s);
~SynthConjecture();
/** presolve */
QuantifiersEngine* d_qe;
/** Reference to the quantifiers state */
QuantifiersState& d_qstate;
+ /** Reference to the quantifiers inference manager */
+ QuantifiersInferenceManager& d_qim;
/** reference to the statistics of parent */
SygusStatistics& d_stats;
/** term database sygus of d_qe */
d_sqp(qe)
{
d_conjs.push_back(std::unique_ptr<SynthConjecture>(
- new SynthConjecture(d_quantEngine, qs, d_statistics)));
+ new SynthConjecture(d_quantEngine, qs, qim, d_statistics)));
d_conj = d_conjs.back().get();
}
if (d_conjs.back()->isAssigned())
{
d_conjs.push_back(std::unique_ptr<SynthConjecture>(
- new SynthConjecture(d_quantEngine, d_qstate, d_statistics)));
+ new SynthConjecture(d_quantEngine, d_qstate, d_qim, d_statistics)));
}
d_conjs.back()->assign(q);
}
bool addedLemma = false;
for (const Node& lem : cclems)
{
- if (d_quantEngine->addLemma(lem))
+ if (d_qim.addPendingLemma(lem))
{
++(d_statistics.d_cegqi_lemmas_ce);
addedLemma = true;
for (const Node& lem : lemmas)
{
Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
- added_lemma |= d_quantEngine->addLemma(lem);
+ added_lemma |= d_qim.addPendingLemma(lem);
}
return added_lemma;
}
d_var_eval.emplace(q, evals);
Node lit = getCeLiteral(q);
- d_quantEngine->addRequirePhase(lit, true);
+ d_qim.addPendingPhaseRequirement(lit, true);
/* The decision strategy for quantified formula 'q' ensures that its
* counterexample literal is decided on first. It is user-context dependent.
if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;
Node lem = d_ce_lemmas[q];
- d_quantEngine->addLemma(lem, false);
+ d_qim.addPendingLemma(lem);
d_ce_lemma_added.insert(q);
Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
}
}
Trace("term-db-lemma") << " add lemma : " << lem << std::endl;
}
- d_quantEngine->addLemma(lem);
+ d_qim.addPendingLemma(lem);
d_qstate.notifyInConflict();
d_consistent_ee = false;
return;
// equality is sent out as a lemma here.
Trace("term-db-lemma")
<< "Purify equality lemma: " << eq << std::endl;
- d_quantEngine->addLemma(eq);
+ d_qim.addPendingLemma(eq);
d_qstate.notifyInConflict();
d_consistent_ee = false;
return false;
d_eq_query(nullptr),
d_sygus_tdb(nullptr),
d_quant_attr(new quantifiers::QuantAttributes),
- d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)),
+ d_instantiate(new quantifiers::Instantiate(this, qstate, qim, pnm)),
d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
d_term_enum(new quantifiers::TermEnumeration),
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_util.push_back(d_instantiate.get());
- d_hasAddedLemma = 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;
void QuantifiersEngine::presolve() {
Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
- d_lemmas_waiting.clear();
- d_phase_req_waiting.clear();
+ d_qim.clearPending();
for( unsigned i=0; i<d_modules.size(); i++ ){
d_modules[i]->presolve();
}
// proceed with the check.
Assert(false);
}
- bool needsCheck = !d_lemmas_waiting.empty();
+ bool needsCheck = d_qim.hasPendingLemma();
QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
std::vector< QuantifiersModule* > qm;
if( d_model->checkNeeded() ){
}
}
- d_hasAddedLemma = false;
+ d_qim.reset();
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 interrupted), or other lemmas to process
- flushLemmas();
- if( d_hasAddedLemma ){
+ d_qim.doPending();
+ if (d_qim.hasSentLemma())
+ {
return;
}
}
Trace("quant-engine-debug") << std::endl;
Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
- if( !d_lemmas_waiting.empty() ){
- Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
+ if (d_qim.hasPendingLemma())
+ {
+ Trace("quant-engine-debug")
+ << " lemmas waiting = " << d_qim.numPendingLemmas() << std::endl;
}
Trace("quant-engine-debug")
<< " Theory engine finished : "
<< "..." << std::endl;
if (!util->reset(e))
{
- flushLemmas();
- if( d_hasAddedLemma ){
+ d_qim.doPending();
+ if (d_qim.hasSentLemma())
+ {
return;
}else{
//should only fail reset if added a lemma
}
Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
//reset may have added lemmas
- flushLemmas();
- if( d_hasAddedLemma ){
+ d_qim.doPending();
+ if (d_qim.hasSentLemma())
+ {
return;
}
{
// If we failed to build the model, flush all pending lemmas and
// finish.
- flushLemmas();
+ d_qim.doPending();
break;
}
}
- if( !d_hasAddedLemma ){
+ if (!d_qim.hasSentLemma())
+ {
//check each module
for (QuantifiersModule*& mdl : qm)
{
}
}
//flush all current lemmas
- flushLemmas();
+ d_qim.doPending();
}
//if we have added one, stop
- if( d_hasAddedLemma ){
+ if (d_qim.hasSentLemma())
+ {
break;
}else{
Assert(!d_qstate.isInConflict());
}
Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
// debug print
- if (d_hasAddedLemma)
+ if (d_qim.hasSentLemma())
{
bool debugInstTrace = Trace.isOn("inst-per-quant-round");
if (options::debugInst() || debugInstTrace)
if( Trace.isOn("quant-engine") ){
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
- Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
+ Trace("quant-engine") << ", sent lemma = " << d_qim.hasSentLemma();
Trace("quant-engine") << std::endl;
}
}
//SAT case
- if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
+ if (e == Theory::EFFORT_LAST_CALL && !d_qim.hasSentLemma())
+ {
if( setIncomplete ){
Trace("quant-engine") << "Set incomplete flag." << std::endl;
getOutputChannel().setIncomplete();
if( it==d_quants.end() ){
Trace("quant") << "QuantifiersEngine : Register quantifier ";
Trace("quant") << " : " << f << std::endl;
- unsigned prev_lemma_waiting = d_lemmas_waiting.size();
+ size_t prev_lemma_waiting = d_qim.numPendingLemmas();
++(d_statistics.d_num_quant);
Assert(f.getKind() == FORALL);
// register with utilities
mdl->registerQuantifier(f);
// since this is context-independent, we should not add any lemmas during
// this call
- Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
+ Assert(d_qim.numPendingLemmas() == prev_lemma_waiting);
}
Trace("quant-debug") << "...finish." << std::endl;
d_quants[f] = true;
- AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);
+ AlwaysAssert(d_qim.numPendingLemmas() == prev_lemma_waiting);
}
}
mdl->preRegisterQuantifier(q);
}
// flush the lemmas
- flushLemmas();
+ d_qim.doPending();
Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
}
addTermToDatabase( t );
}
-bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
- if( doCache ){
- if( doRewrite ){
- lem = Rewriter::rewrite(lem);
- }
- 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_lemmas_produced_c[ lem ] = true;
- d_lemmas_waiting.push_back( lem );
- Trace("inst-add-debug") << "Added lemma" << std::endl;
- return true;
- }else{
- Trace("inst-add-debug") << "Duplicate." << std::endl;
- return false;
- }
- }else{
- //do not need to rewrite, will be rewritten after sending
- d_lemmas_waiting.push_back( lem );
- return true;
- }
-}
-
-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() ){
- d_lemmas_waiting.erase( it, it + 1 );
- d_lemmas_produced_c[ lem ] = false;
- return true;
- }else{
- return false;
- }
-}
-
-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::getInstWhenNeedsCheck( Theory::Effort e ) {
Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
//determine if we should perform check, based on instWhenMode
}
}
-void QuantifiersEngine::flushLemmas(){
- OutputChannel& out = getOutputChannel();
- if( !d_lemmas_waiting.empty() ){
- //take default output channel if none is provided
- d_hasAddedLemma = 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;
- out.requirePhase(it->first, it->second);
- }
- d_phase_req_waiting.clear();
- }
-}
-
void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
d_instantiate->getInstantiationTermVectors(q, tvecs);
}
void registerQuantifierInternal(Node q);
/** reduceQuantifier, return true if reduced */
bool reduceQuantifier(Node q);
- /** flush lemmas */
- void flushLemmas();
public:
- /**
- * Add lemma to the lemma buffer of this quantifiers engine.
- * @param lem The lemma to send
- * @param doCache Whether to cache the lemma (to check for duplicate lemmas)
- * @param doRewrite Whether to rewrite the lemma
- * @return true if the lemma was successfully added to the buffer
- */
- bool addLemma(Node lem, bool doCache = true, bool doRewrite = true);
- /**
- * Add trusted lemma lem, same as above, but where a proof generator may be
- * provided along with the lemma.
- */
- bool addTrustedLemma(TrustNode tlem,
- bool doCache = true,
- bool doRewrite = true);
- /** remove pending lemma */
- bool removeLemma(Node lem);
- /** add require phase */
- void addRequirePhase(Node lit, bool req);
/** mark relevant quantified formula, this will indicate it should be checked
* before the others */
void markRelevant(Node q);
- /** has added lemma */
- bool hasAddedLemma() const;
- /** get number of waiting lemmas */
- unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
/** get needs check */
bool getInstWhenNeedsCheck(Theory::Effort e);
/** get user pat mode */
* The modules utility, which contains all of the quantifiers modules.
*/
std::unique_ptr<quantifiers::QuantifiersModules> d_qmodules;
- //------------- temporary information during check
- /** has added lemma this round */
- bool d_hasAddedLemma;
//------------- end temporary information during check
private:
/** list of all quantifiers seen */
/** quantifiers reduced */
BoolMap d_quants_red;
std::map<Node, Node> d_quants_red_lem;
- /** list of all lemmas produced */
- // std::map< Node, bool > d_lemmas_produced;
- BoolMap d_lemmas_produced_c;
- /** lemmas waiting */
- std::vector<Node> d_lemmas_waiting;
- /** map from waiting lemmas to their proof generators */
- std::map<Node, ProofGenerator*> d_lemmasWaitingPg;
- /** phase requirements waiting */
- std::map<Node, bool> d_phase_req_waiting;
/** inst round counters TODO: make context-dependent? */
context::CDO<int> d_ierCounter_c;
int d_ierCounter;
d_numCurrentLemmas(0),
d_numCurrentFacts(0)
{
+ // don't add true lemma
+ Node truen = NodeManager::currentNM()->mkConst(true);
+ d_lemmasSent.insert(truen);
}
void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
projects / cvc5.git / commitdiff