Towards breaking dependencies on quantifers engine.
bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
Assert(!d_curr_quant.isNull());
+ Instantiate* inst = d_qim.getInstantiate();
//if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
{
d_cbqi_set_quant_inactive = true;
d_incomplete_check = true;
- d_quantEngine->getInstantiate()->recordInstantiation(
- d_curr_quant, subs, false, false);
+ inst->recordInstantiation(d_curr_quant, subs, false, false);
return true;
- }else{
- //check if we need virtual term substitution (if used delta or infinity)
- bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
- if (d_quantEngine->getInstantiate()->addInstantiation(
- d_curr_quant,
- subs,
- InferenceId::QUANTIFIERS_INST_CEGQI,
- false,
- false,
- used_vts))
- {
- return true;
- }else{
- //this should never happen for monotonic selection strategies
- Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
- return false;
- }
}
+ // check if we need virtual term substitution (if used delta or infinity)
+ bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
+ if (inst->addInstantiation(d_curr_quant,
+ subs,
+ InferenceId::QUANTIFIERS_INST_CEGQI,
+ false,
+ false,
+ used_vts))
+ {
+ return true;
+ }
+ // this should never happen for monotonic selection strategies
+ Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
+ return false;
}
bool InstStrategyCegqi::addPendingLemma(Node lem) const
#include "theory/quantifiers/skolemize.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
//check each skolem variable
bool disproven = true;
std::vector<Node> skolems;
- d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems);
+ d_qim.getSkolemize()->getSkolemConstants(q, skolems);
Trace("sg-conjecture") << " CONJECTURE : ";
std::vector< Node > ce;
for (unsigned j = 0; j < skolems.size(); j++)
if( n.getNumChildren()>0 ){
Trace("sg-gt-enum-debug") << "Get enumerate uf terms " << n << " (" << num
<< ")" << std::endl;
- TermEnumeration* te = d_quantEngine->getTermEnumeration();
+ TermEnumeration* te = d_quantEngine->getTermRegistry().getTermEnumeration();
// below, we do a fair enumeration of vectors vec of indices whose sum is
// 1,2,3, ...
std::vector< int > vec;
#include "theory/quantifiers/quantifiers_registry.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/uf/theory_uf_rewriter.h"
d_lchildren.clear();
d_arg_to_arg_rep.clear();
d_arg_vector.clear();
- QuantifiersState& qs = d_quantEngine->getState();
for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
{
TNode var = ha.first;
}
else if (!itf->second.isNull())
{
- if (!qs.areEqual(itf->second, args[k]))
+ if (!d_qstate.areEqual(itf->second, args[k]))
{
- if (!d_quantEngine->getTermDatabase()->isEntailed(
+ if (!d_treg.getTermDatabase()->isEntailed(
itf->second.eqNode(args[k]), true))
{
fixed_vals[k] = Node::null();
{
if (!itf->second.isNull())
{
- Node r = qs.getRepresentative(itf->second);
+ Node r = d_qstate.getRepresentative(itf->second);
std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
if (itfr != arg_to_rep.end())
{
else
{
// do not run higher-order matching
- return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
+ return d_qim.getInstantiate()->addInstantiation(d_quant, m, id);
}
}
if (var_index == d_ho_var_list.size())
{
// we now have an instantiation to try
- return d_quantEngine->getInstantiate()->addInstantiation(
+ return d_qim.getInstantiate()->addInstantiation(
d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO);
}
else
Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
uint64_t numLemmas = 0;
// this forces expansion of APPLY_UF terms to curried HO_APPLY chains
- TermDb* tdb = d_quantEngine->getTermDatabase();
+ TermDb* tdb = d_treg.getTermDatabase();
unsigned size = tdb->getNumOperators();
NodeManager* nm = NodeManager::currentNM();
for (unsigned j = 0; j < size; j++)
class Trigger;
/** IMGenerator class
-*
-* Virtual base class for generating InstMatch objects, which correspond to
-* quantifier instantiations. The main use of this class is as a backend utility
-* to Trigger (see theory/quantifiers/ematching/trigger.h).
-*
-* Some functions below take as argument a pointer to the current quantifiers
-* engine, which is used for making various queries about what terms and
-* equalities exist in the current context.
-*
-* Some functions below take a pointer to a parent Trigger object, which is used
-* to post-process and finalize the instantiations through
-* sendInstantiation(...), where the parent trigger will make calls to
-* qe->getInstantiate()->addInstantiation(...). The latter function is the entry
-* point in which instantiate lemmas are enqueued to be sent on the output
-* channel.
-*/
+ *
+ * Virtual base class for generating InstMatch objects, which correspond to
+ * quantifier instantiations. The main use of this class is as a backend utility
+ * to Trigger (see theory/quantifiers/ematching/trigger.h).
+ *
+ * Some functions below take as argument a pointer to the current quantifiers
+ * engine, which is used for making various queries about what terms and
+ * equalities exist in the current context.
+ *
+ * Some functions below take a pointer to a parent Trigger object, which is used
+ * to post-process and finalize the instantiations through
+ * sendInstantiation(...), where the parent trigger will make calls to
+ * Instantiate::addInstantiation(...). The latter function is the entry
+ * point in which instantiate lemmas are enqueued to be sent on the output
+ * channel.
+ */
class IMGenerator {
public:
IMGenerator(Trigger* tparent);
* The implementation traverses the term indices in TermDatabase for adding
* instantiations, which is more efficient than the techniques required for
* handling non-simple single triggers.
- *
- * In contrast to other instantiation generators, it does not call
- * IMGenerator::sendInstantiation and for performance reasons instead calls
- * qe->getInstantiate()->addInstantiation(...) directly.
*/
class InstMatchGeneratorSimple : public IMGenerator
{
std::map<size_t, int> d_var_num;
/** add instantiations, helper function.
*
- * m is the current match we are building,
- * addedLemmas is the number of lemmas we have added via calls to
- * qe->getInstantiate()->aaddInstantiation(...),
- * argIndex is the argument index in d_match_pattern we are currently
- * matching,
- * tat is the term index we are currently traversing.
+ * @param m the current match we are building,
+ * @param addedLemmas the number of lemmas we have added via calls to
+ * Instantiate::addInstantiation(...),
+ * @param argIndex the argument index in d_match_pattern we are currently
+ * matching,
+ * @param tat the term index we are currently traversing.
*/
void addInstantiations(InstMatch& m,
uint64_t& addedLemmas,
bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
{
- return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
+ return d_qim.getInstantiate()->addInstantiation(d_quant, m, id);
}
bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)
}
FullModelChecker::FullModelChecker(QuantifiersState& qs,
- QuantifiersRegistry& qr)
- : QModelBuilder(qs, qr)
+ QuantifiersRegistry& qr,
+ QuantifiersInferenceManager& qim)
+ : QModelBuilder(qs, qr, qim)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
Trace("fmc") << std::endl;
// consider all entries going to non-true
- Instantiate* instq = d_qe->getInstantiate();
+ Instantiate* instq = d_qim.getInstantiate();
for (unsigned i = 0, msize = mcond.size(); i < msize; i++)
{
if (d_quant_models[f].d_value[i] == d_true)
Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
int addedLemmas = 0;
//now do full iteration
+ Instantiate* ie = d_qim.getInstantiate();
while( !riter.isFinished() ){
d_triedLemmas++;
Trace("fmc-exh-debug") << "Inst : ";
if (ev!=d_true) {
Trace("fmc-exh-debug") << ", add!";
//add as instantiation
- if (d_qe->getInstantiate()->addInstantiation(
+ if (ie->addInstantiation(
f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true))
{
Trace("fmc-exh-debug") << " ...success.";
Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
public:
- FullModelChecker(QuantifiersState& qs, QuantifiersRegistry& qr);
+ FullModelChecker(QuantifiersState& qs,
+ QuantifiersRegistry& qr,
+ QuantifiersInferenceManager& qim);
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr)
+QModelBuilder::QModelBuilder(QuantifiersState& qs,
+ QuantifiersRegistry& qr,
+ QuantifiersInferenceManager& qim)
: TheoryEngineModelBuilder(),
d_addedLemmas(0),
d_triedLemmas(0),
- d_qe(nullptr),
d_qstate(qs),
- d_qreg(qr)
+ d_qreg(qr),
+ d_qim(qim)
{
}
int tests = 0;
int bad = 0;
QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
+ Instantiate* inst = d_qim.getInstantiate();
for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
std::vector< Node > vars;
{
terms.push_back( riter.getCurrentTerm( k ) );
}
- Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms);
+ Node n = inst->getInstantiation(f, vars, terms);
Node val = fm->getValue( n );
if (!val.isConst() || !val.getConst<bool>())
{
class FirstOrderModel;
class QuantifiersState;
class QuantifiersRegistry;
+class QuantifiersInferenceManager;
class QModelBuilder : public TheoryEngineModelBuilder
{
unsigned d_triedLemmas;
public:
- QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr);
- //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
- void finishInit(QuantifiersEngine* qe) { d_qe = qe; }
+ QModelBuilder(QuantifiersState& qs,
+ QuantifiersRegistry& qr,
+ QuantifiersInferenceManager& qim);
//do exhaustive instantiation
// 0 : failed, but resorting to true exhaustive instantiation may work
QuantifiersState& d_qstate;
/** Reference to the quantifiers registry */
QuantifiersRegistry& d_qreg;
+ /** The quantifiers inference manager */
+ quantifiers::QuantifiersInferenceManager& d_qim;
};
}/* CVC4::theory::quantifiers namespace */
if( !riter.isIncomplete() ){
int triedLemmas = 0;
int addedLemmas = 0;
- Instantiate* inst = d_quantEngine->getInstantiate();
+ Instantiate* inst = d_qim.getInstantiate();
while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
//instantiation was not shown to be true, construct the match
InstMatch m( f );
mkTermTupleEnumerator(quantifier, &ttec));
std::vector<Node> terms;
std::vector<bool> failMask;
- Instantiate* ie = d_quantEngine->getInstantiate();
+ Instantiate* ie = d_qim.getInstantiate();
for (enumerator->init(); enumerator->hasNext();)
{
if (d_qstate.isInConflict())
namespace theory {
namespace quantifiers {
-QuantInfo::QuantInfo() : d_unassigned_nvar(0), d_una_index(0), d_mg(nullptr) {}
+QuantInfo::QuantInfo()
+ : d_unassigned_nvar(0), d_una_index(0), d_parent(nullptr), d_mg(nullptr)
+{
+}
QuantInfo::~QuantInfo() {
delete d_mg;
d_var_mg.clear();
}
+QuantifiersInferenceManager& QuantInfo::getInferenceManager()
+{
+ Assert(d_parent != nullptr);
+ return d_parent->getInferenceManager();
+}
void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
+ d_parent = p;
d_q = q;
d_extra_var.clear();
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
}
}else{
Node inst =
- p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms);
+ getInferenceManager().getInstantiate()->getInstantiation(d_q, terms);
inst = Rewriter::rewrite(inst);
Node inst_eval = p->getTermDatabase()->evaluateTerm(
inst, options::qcfTConstraint(), true);
}
// try to make a matches making the body false or propagating
Trace("qcf-check-debug") << "Get next match..." << std::endl;
- Instantiate* qinst = d_quantEngine->getInstantiate();
+ Instantiate* qinst = d_qim.getInstantiate();
while (qi->getNextMatch(this))
{
if (d_qstate.isInConflict())
public:
QuantInfo();
~QuantInfo();
+ /** Get quantifiers inference manager */
+ QuantifiersInferenceManager& getInferenceManager();
std::vector< TNode > d_vars;
std::vector< TypeNode > d_var_types;
std::map< TNode, int > d_var_num;
typedef std::map< int, MatchGen * > VarMgMap;
private:
+ /** The parent who owns this class */
+ QuantConflictFind* d_parent;
MatchGen * d_mg;
VarMgMap d_var_mg;
public:
{
d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr));
modules.push_back(d_i_cbqi.get());
- qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
+ qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
}
if (options::sygus())
{
if (tr.useFmcModel())
{
Trace("quant-init-debug") << "...make fmc builder." << std::endl;
- d_builder.reset(new fmcheck::FullModelChecker(qs, qr));
+ d_builder.reset(new fmcheck::FullModelChecker(qs, qr, qim));
}
else
{
Trace("quant-init-debug")
<< "...make default model builder." << std::endl;
- d_builder.reset(new QModelBuilder(qs, qr));
+ d_builder.reset(new QModelBuilder(qs, qr, qim));
}
- // !!!!!!!!!!!!! temporary (project #15)
- d_builder->finishInit(qe);
}
if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
{
#include "theory/quantifiers/sygus/sygus_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
ptn = ptn.getRangeType();
}
Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
- s = d_qe->getTermEnumeration()->getEnumerateTerm(ptn, 0);
+ s = d_qe->getTermRegistry().getTermEnumeration()->getEnumerateTerm(ptn, 0);
}
else
{
Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
<< std::endl;
// construct base instantiation
- d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation(
+ d_base_inst = Rewriter::rewrite(d_qim.getInstantiate()->getInstantiation(
d_embed_quant, vars, d_candidates));
if (!d_embedSideCondition.isNull())
{
if (quant_e != QEFFORT_STANDARD) return;
FirstOrderModel* model = d_quantEngine->getModel();
- Instantiate* inst = d_quantEngine->getInstantiate();
+ Instantiate* inst = d_qim.getInstantiate();
TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
SygusExplain syexplain(db);
NodeManager* nm = NodeManager::currentNM();
{
return d_qreg;
}
+quantifiers::TermRegistry& QuantifiersEngine::getTermRegistry()
+{
+ return d_treg;
+}
quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
{
/// !!!!!!!!!!!!!! temporary (project #15)
-quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
-{
- return d_treg.getTermDatabase();
-}
quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
{
return d_treg.getTermDatabaseSygus();
}
-quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
-{
- return d_treg.getTermEnumeration();
-}
-quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
-{
- return d_qim.getInstantiate();
-}
-quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
+
+quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
{
- return d_qim.getSkolemize();
+ return d_treg.getTermDatabase();
}
+
quantifiers::inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
{
return d_tr_trie.get();
quantifiers::QuantifiersInferenceManager& getInferenceManager();
/** The quantifiers registry */
quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
+ /** The term registry */
+ quantifiers::TermRegistry& getTermRegistry();
//---------------------- end external interface
//---------------------- utilities
/** get the model builder */
quantifiers::QModelBuilder* getModelBuilder() const;
- /** get model */
- quantifiers::FirstOrderModel* getModel() const;
/** get term database */
quantifiers::TermDb* getTermDatabase() const;
+ /** get model */
+ quantifiers::FirstOrderModel* getModel() const;
/** get term database sygus */
quantifiers::TermDbSygus* getTermDatabaseSygus() const;
- /** get term enumeration utility */
- quantifiers::TermEnumeration* getTermEnumeration() const;
- /** get instantiate utility */
- quantifiers::Instantiate* getInstantiate() const;
- /** get skolemize utility */
- quantifiers::Skolemize* getSkolemize() const;
/** get trigger database */
quantifiers::inst::TriggerTrie* getTriggerDatabase() const;
//---------------------- end utilities
projects / cvc5.git / commitdiff