Model is now nested into term registry.
This PR also resolves some complications due to namespaces within quantifiers.
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/instantiate.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"
using namespace CVC4::kind;
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
+CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr)
+ : d_qs(qs), d_treg(tr)
+{
+}
+
bool CandidateGenerator::isLegalCandidate( Node n ){
- return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
+ return d_treg.getTermDatabase()->isTermActive(n)
+ && (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n));
}
-CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
- : CandidateGenerator(qe),
+CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs,
+ TermRegistry& tr,
+ Node pat)
+ : CandidateGenerator(qs, tr),
d_term_iter(-1),
d_term_iter_limit(0),
d_mode(cand_term_none)
{
- d_op = qe->getTermDatabase()->getMatchOperator( pat );
+ d_op = d_treg.getTermDatabase()->getMatchOperator(pat);
Assert(!d_op.isNull());
}
d_term_iter = 0;
d_eqc = eqc;
d_op = op;
- d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms(d_op);
+ d_term_iter_limit = d_treg.getTermDatabase()->getNumGroundTerms(d_op);
if( eqc.isNull() ){
d_mode = cand_term_db;
}else{
if( isExcludedEqc( eqc ) ){
d_mode = cand_term_none;
}else{
- eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+ eq::EqualityEngine* ee = d_qs.getEqualityEngine();
if( ee->hasTerm( eqc ) ){
- TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op);
+ TNodeTrie* tat = d_treg.getTermDatabase()->getTermArgTrie(eqc, op);
if( tat ){
//create an equivalence class iterator in eq class eqc
Node rep = ee->getRepresentative( eqc );
bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
if( n.hasOperator() ){
if( isLegalCandidate( n ) ){
- return d_qe->getTermDatabase()->getMatchOperator( n )==d_op;
+ return d_treg.getTermDatabase()->getMatchOperator(n) == d_op;
}
}
return false;
Node CandidateGeneratorQE::getNextCandidateInternal()
{
if( d_mode==cand_term_db ){
- quantifiers::QuantifiersState& qs = d_qe->getState();
Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
//get next candidate term in the uf term database
while( d_term_iter<d_term_iter_limit ){
- Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter );
+ Node n = d_treg.getTermDatabase()->getGroundTerm(d_op, d_term_iter);
d_term_iter++;
if( isLegalCandidate( n ) ){
- if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
+ if (d_treg.getTermDatabase()->hasTermCurrent(n))
+ {
if( d_exclude_eqc.empty() ){
return n;
}else{
- Node r = qs.getRepresentative(n);
+ Node r = d_qs.getRepresentative(n);
if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
Debug("cand-gen-qe") << "...returning " << n << std::endl;
return n;
return Node::null();
}
-CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
-CandidateGenerator( qe ), d_match_pattern( mpat ){
+CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq(QuantifiersState& qs,
+ TermRegistry& tr,
+ Node mpat)
+ : CandidateGenerator(qs, tr), d_match_pattern(mpat)
+{
Assert(d_match_pattern.getKind() == EQUAL);
d_match_pattern_type = d_match_pattern[0].getType();
}
void CandidateGeneratorQELitDeq::reset( Node eqc ){
- eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+ eq::EqualityEngine* ee = d_qs.getEqualityEngine();
Node falset = NodeManager::currentNM()->mkConst(false);
d_eqc_false = eq::EqClassIterator(falset, ee);
}
return Node::null();
}
-
-CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) :
- CandidateGenerator( qe ), d_match_pattern( mpat ){
+CandidateGeneratorQEAll::CandidateGeneratorQEAll(QuantifiersState& qs,
+ TermRegistry& tr,
+ Node mpat)
+ : CandidateGenerator(qs, tr), d_match_pattern(mpat)
+{
d_match_pattern_type = mpat.getType();
Assert(mpat.getKind() == INST_CONSTANT);
d_f = quantifiers::TermUtil::getInstConstAttr( mpat );
}
void CandidateGeneratorQEAll::reset( Node eqc ) {
- d_eq = eq::EqClassesIterator(d_qe->getState().getEqualityEngine());
+ d_eq = eq::EqClassesIterator(d_qs.getEqualityEngine());
d_firstTime = true;
}
Node CandidateGeneratorQEAll::getNextCandidate() {
- quantifiers::TermDb* tdb = d_qe->getTermDatabase();
+ quantifiers::TermDb* tdb = d_treg.getTermDatabase();
while( !d_eq.isFinished() ){
TNode n = (*d_eq);
++d_eq;
if( !nh.isNull() ){
if (options::instMaxLevel() != -1)
{
- nh = d_qe->getModel()->getInternalRepresentative(nh, d_f, d_index);
+ nh = d_treg.getModel()->getInternalRepresentative(nh, d_f, d_index);
//don't consider this if already the instantiation is ineligible
if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f))
{
if( d_firstTime ){
//must return something
d_firstTime = false;
- return d_qe->getInstantiate()->getTermForType(d_match_pattern_type);
+ return d_treg.getTermForType(d_match_pattern_type);
}
return Node::null();
}
-CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(
- QuantifiersEngine* qe, Node mpat)
- : CandidateGeneratorQE(qe, mpat)
+CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(QuantifiersState& qs,
+ TermRegistry& tr,
+ Node mpat)
+ : CandidateGeneratorQE(qs, tr, mpat)
{
Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
d_mpat_type = mpat.getType();
return isLegalCandidate(n);
}
-CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersEngine* qe,
+CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
+ TermRegistry& tr,
Node mpat)
- : CandidateGeneratorQE(qe, mpat)
+ : CandidateGeneratorQE(qs, tr, mpat)
{
Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
Assert(mpat.getKind() == APPLY_SELECTOR);
{
Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
Assert(mpatExp[2].getKind() == APPLY_UF);
- d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp[1]);
- d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp[2]);
+ d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]);
+ d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]);
}
else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL)
{
// corner case of datatype with one constructor
- d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp);
+ d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
}
else
{
// corner case of a wrongly applied selector as a trigger
Assert(mpatExp.getKind() == APPLY_UF);
- d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp);
+ d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
}
Assert(d_selOp != d_ufOp);
}
}
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
-class QuantifiersEngine;
+class QuantifiersState;
+class TermRegistry;
namespace inst {
*
*/
class CandidateGenerator {
-protected:
- QuantifiersEngine* d_qe;
-public:
- CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){}
+ public:
+ CandidateGenerator(QuantifiersState& qs, TermRegistry& tr);
virtual ~CandidateGenerator(){}
/** reset instantiation round
*
virtual void reset( Node eqc ) = 0;
/** get the next candidate */
virtual Node getNextCandidate() = 0;
-public:
- /** is n a legal candidate? */
- bool isLegalCandidate(Node n);
-};/* class CandidateGenerator */
+ /** is n a legal candidate? */
+ bool isLegalCandidate(Node n);
+
+ protected:
+ /** Reference to the quantifiers state */
+ QuantifiersState& d_qs;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
+};
/* the default candidate generator class
*
friend class CandidateGeneratorQEDisequal;
public:
- CandidateGeneratorQE(QuantifiersEngine* qe, Node pat);
+ CandidateGeneratorQE(QuantifiersState& qs, TermRegistry& tr, Node pat);
/** reset */
void reset(Node eqc) override;
/** get next candidate */
* mpat is an equality that we are matching to equalities in the equivalence
* class of false
*/
- CandidateGeneratorQELitDeq(QuantifiersEngine* qe, Node mpat);
+ CandidateGeneratorQELitDeq(QuantifiersState& qs, TermRegistry& tr, Node mpat);
/** reset */
void reset(Node eqc) override;
/** get next candidate */
bool d_firstTime;
public:
- CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
+ CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat);
/** reset */
void reset(Node eqc) override;
/** get next candidate */
class CandidateGeneratorConsExpand : public CandidateGeneratorQE
{
public:
- CandidateGeneratorConsExpand(QuantifiersEngine* qe, Node mpat);
+ CandidateGeneratorConsExpand(QuantifiersState& qs,
+ TermRegistry& tr,
+ Node mpat);
/** reset */
void reset(Node eqc) override;
/** get next candidate */
class CandidateGeneratorSelector : public CandidateGeneratorQE
{
public:
- CandidateGeneratorSelector(QuantifiersEngine* qe, Node mpat);
+ CandidateGeneratorSelector(QuantifiersState& qs, TermRegistry& tr, Node mpat);
/** reset */
void reset(Node eqc) override;
/**
};
}/* CVC4::theory::inst namespace */
+} // namespace quantifiers
}/* CVC4::theory namespace */
}/* CVC4 namespace */
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
HigherOrderTrigger::HigherOrderTrigger(
QuantifiersEngine* qe,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
Node q,
std::vector<Node>& nodes,
std::map<Node, std::vector<Node> >& ho_apps)
- : Trigger(qe, qs, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
+ : Trigger(qe, qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps)
{
NodeManager* nm = NodeManager::currentNM();
// process the higher-order variable applications
{
if (op.getKind() == kind::INST_CONSTANT)
{
- Assert(quantifiers::TermUtil::getInstConstAttr(ret) == q);
+ Assert(TermUtil::getInstConstAttr(ret) == q);
Trace("ho-quant-trigger-debug")
<< "Ho variable apply term : " << ret << " with head " << op
<< std::endl;
d_lchildren.clear();
d_arg_to_arg_rep.clear();
d_arg_vector.clear();
- quantifiers::QuantifiersState& qs = d_quantEngine->getState();
+ QuantifiersState& qs = d_quantEngine->getState();
for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
{
TNode var = ha.first;
Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
uint64_t numLemmas = 0;
// this forces expansion of APPLY_UF terms to curried HO_APPLY chains
- quantifiers::TermDb* tdb = d_quantEngine->getTermDatabase();
+ TermDb* tdb = d_quantEngine->getTermDatabase();
unsigned size = tdb->getNumOperators();
NodeManager* nm = NodeManager::currentNM();
for (unsigned j = 0; j < size; j++)
return numLemmas;
}
-} /* CVC4::theory::inst namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+} // namespace inst
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
class Trigger;
private:
HigherOrderTrigger(QuantifiersEngine* qe,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
Node q,
std::vector<Node>& nodes,
std::map<Node, std::vector<Node> >& ho_apps);
bool arg_changed);
};
-} /* CVC4::theory::inst namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+} // namespace inst
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
#endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
IMGenerator::IMGenerator(Trigger* tparent)
- : d_tparent(tparent), d_qstate(tparent->d_qstate)
+ : d_tparent(tparent), d_qstate(tparent->d_qstate), d_treg(tparent->d_treg)
{
}
return d_tparent->d_quantEngine;
}
-
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace inst
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
namespace quantifiers {
class QuantifiersState;
-} // namespace quantifiers
+class TermRegistry;
namespace inst {
bool sendInstantiation(InstMatch& m, InferenceId id);
/** The parent trigger that owns this */
Trigger* d_tparent;
- /** The state of the quantifiers engine */
- quantifiers::QuantifiersState& d_qstate;
+ /** Reference to the state of the quantifiers engine */
+ QuantifiersState& d_qstate;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
// !!!!!!!!! temporarily available (project #15)
QuantifiersEngine* getQuantifiersEngine();
};/* class IMGenerator */
+} // namespace inst
}
}
}
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat)
}
}
- QuantifiersEngine* qe = getQuantifiersEngine();
// create candidate generator
if (mpk == APPLY_SELECTOR)
{
// candidates for apply selector are a union of correctly and incorrectly
// applied selectors
- d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern);
+ d_cg =
+ new inst::CandidateGeneratorSelector(d_qstate, d_treg, d_match_pattern);
}
else if (TriggerTermInfo::isAtomicTriggerKind(mpk))
{
const DType& dt = d_match_pattern.getType().getDType();
if (dt.getNumConstructors() == 1)
{
- d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
+ d_cg = new inst::CandidateGeneratorConsExpand(
+ d_qstate, d_treg, d_match_pattern);
}
}
if (d_cg == nullptr)
{
- CandidateGeneratorQE* cg = new CandidateGeneratorQE(qe, d_match_pattern);
+ CandidateGeneratorQE* cg =
+ new CandidateGeneratorQE(d_qstate, d_treg, d_match_pattern);
// we will be scanning lists trying to find ground terms whose operator
// is the same as d_match_operator's.
d_cg = cg;
Trace("inst-match-gen")
<< "Purify dt trigger " << d_pattern << ", will match terms of op "
<< cOp << std::endl;
- d_cg = new inst::CandidateGeneratorQE(qe, cOp);
+ d_cg = new inst::CandidateGeneratorQE(d_qstate, d_treg, cOp);
}else{
- d_cg = new CandidateGeneratorQEAll(qe, d_match_pattern);
+ d_cg = new CandidateGeneratorQEAll(d_qstate, d_treg, d_match_pattern);
}
}
else if (mpk == EQUAL)
if (d_pattern.getKind() == NOT)
{
// candidates will be all disequalities
- d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
+ d_cg = new inst::CandidateGeneratorQELitDeq(
+ d_qstate, d_treg, d_match_pattern);
}
}
else
return new InstMatchGenerator(tparent, n);
}
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace inst
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
class CandidateGenerator;
Node n);
};/* class InstMatchGenerator */
+} // namespace inst
}
}
}
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent,
std::map<Node, std::vector<Node> > var_contains;
for (const Node& pat : pats)
{
- quantifiers::TermUtil::computeInstConstContainsForQuant(
- q, pat, var_contains[pat]);
+ TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]);
}
// convert to indicies
for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
{
return;
}
- quantifiers::QuantifiersState& qs = d_qstate;
+ QuantifiersState& qs = d_qstate;
// check modulo equality for other possible instantiations
if (!qs.hasTerm(n))
{
}
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
/** InstMatchGeneratorMulti
};
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
std::map<Node, std::vector<Node> > var_contains;
for (const Node& pat : pats)
{
- quantifiers::TermUtil::computeInstConstContainsForQuant(
- q, pat, var_contains[pat]);
+ TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]);
}
std::map<Node, std::vector<Node> > var_to_node;
for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
}
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
/** InstMatchGeneratorMultiLinear class
};
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
{
d_eqc = d_match_pattern[1];
d_match_pattern = d_match_pattern[0];
- Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc));
+ Assert(!TermUtil::hasInstConstAttr(d_eqc));
}
Assert(TriggerTermInfo::isSimpleTrigger(d_match_pattern));
for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
if (d_match_pattern[i].getKind() == INST_CONSTANT)
{
if (!options::cegqi()
- || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]) == q)
+ || TermUtil::getInstConstAttr(d_match_pattern[i]) == q)
{
d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
}
}
d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
}
- quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
d_op = tdb->getMatchOperator(d_match_pattern);
}
{
uint64_t addedLemmas = 0;
TNodeTrie* tat;
- quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
if (d_eqc.isNull())
{
tat = tdb->getTermArgTrie(d_op);
int InstMatchGeneratorSimple::getActiveScore()
{
- quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
Node f = tdb->getMatchOperator(d_match_pattern);
size_t ngt = tdb->getNumGroundTerms(f);
Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) "
}
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
/** InstMatchGeneratorSimple class
};
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
InstStrategy::InstStrategy(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr)
- : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
+ QuantifiersRegistry& qr,
+ TermRegistry& tr)
+ : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
{
}
InstStrategy::~InstStrategy() {}
class QuantifiersState;
class QuantifiersInferenceManager;
class QuantifiersRegistry;
+class TermRegistry;
/** A status response to process */
enum class InstStrategyStatus
InstStrategy(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr);
+ QuantifiersRegistry& qr,
+ TermRegistry& tr);
virtual ~InstStrategy();
/** presolve */
virtual void presolve();
QuantifiersState& d_qstate;
/** The quantifiers inference manager object */
QuantifiersInferenceManager& d_qim;
- /** The quantifiers registry */
+ /** Reference to the quantifiers registry */
QuantifiersRegistry& d_qreg;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
}; /* class InstStrategy */
} // namespace quantifiers
#include "util/random.h"
using namespace CVC4::kind;
-using namespace CVC4::theory::inst;
+using namespace CVC4::theory::quantifiers::inst;
namespace CVC4 {
namespace theory {
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
QuantRelevance* qrlv)
- : InstStrategy(qe, qs, qim, qr), d_quant_rel(qrlv)
+ : InstStrategy(qe, qs, qim, qr, tr), d_quant_rel(qrlv)
{
//how to select trigger terms
d_tr_strategy = options::triggerSelMode();
d_qstate,
d_qim,
d_qreg,
+ d_treg,
f,
patTerms[0],
false,
d_qstate,
d_qim,
d_qreg,
+ d_treg,
f,
patTerms,
false,
d_qstate,
d_qim,
d_qreg,
+ d_treg,
f,
patTerms[index],
false,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
QuantRelevance* qrlv);
~InstStrategyAutoGenTriggers() {}
#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
-using namespace CVC4::theory::inst;
+using namespace CVC4::theory::quantifiers::inst;
namespace CVC4 {
namespace theory {
QuantifiersEngine* ie,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr)
- : InstStrategy(ie, qs, qim, qr)
+ QuantifiersRegistry& qr,
+ TermRegistry& tr)
+ : InstStrategy(ie, qs, qim, qr, tr)
{
}
InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const
{
- std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
+ std::map<Node, std::vector<Trigger*> >::const_iterator it =
d_user_gen.find(q);
if (it == d_user_gen.end())
{
return it->second.size();
}
-inst::Trigger* InstStrategyUserPatterns::getUserGenerator(Node q,
- size_t i) const
+Trigger* InstStrategyUserPatterns::getUserGenerator(Node q, size_t i) const
{
- std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
+ std::map<Node, std::vector<Trigger*> >::const_iterator it =
d_user_gen.find(q);
if (it == d_user_gen.end())
{
d_qstate,
d_qim,
d_qreg,
+ d_treg,
q,
ugw[i],
true,
ugw.clear();
}
- std::vector<inst::Trigger*>& ug = d_user_gen[q];
+ std::vector<Trigger*>& ug = d_user_gen[q];
for (Trigger* t : ug)
{
if (Trace.isOn("process-trigger"))
d_qstate,
d_qim,
d_qreg,
+ d_treg,
q,
nodes,
true,
InstStrategyUserPatterns(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr);
+ QuantifiersRegistry& qr,
+ TermRegistry& tr);
~InstStrategyUserPatterns();
/** add pattern */
void addUserPattern(Node q, Node pat);
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
-using namespace std;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory::inst;
+using namespace CVC4::theory::quantifiers::inst;
namespace CVC4 {
namespace theory {
InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr)
+ QuantifiersRegistry& qr,
+ TermRegistry& tr)
: QuantifiersModule(qs, qim, qr, qe),
d_instStrategies(),
d_isup(),
// user-provided patterns
if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
{
- d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr));
+ d_isup.reset(
+ new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr, tr));
d_instStrategies.push_back(d_isup.get());
}
// auto-generated patterns
d_i_ag.reset(new InstStrategyAutoGenTriggers(
- d_quantEngine, qs, qim, qr, d_quant_rel.get()));
+ d_quantEngine, qs, qim, qr, tr, d_quant_rel.get()));
d_instStrategies.push_back(d_i_ag.get());
}
}
InstantiationEngine(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr);
+ QuantifiersRegistry& qr,
+ TermRegistry& tr);
~InstantiationEngine();
void presolve() override;
bool needsCheck(Theory::Effort e) override;
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
PatternTermSelector::PatternTermSelector(Node q,
}
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
/**
};
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
/** trigger class constructor */
Trigger::Trigger(QuantifiersEngine* qe,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
Node q,
std::vector<Node>& nodes)
- : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_quant(q)
+ : d_quantEngine(qe),
+ d_qstate(qs),
+ d_qim(qim),
+ d_qreg(qr),
+ d_treg(tr),
+ d_quant(q)
{
// We must ensure that the ground subterms of the trigger have been
// preprocessed.
}
if (Trace.isOn("trigger"))
{
- quantifiers::QuantAttributes& qa = d_qreg.getQuantAttributes();
+ QuantAttributes& qa = d_qreg.getQuantAttributes();
Trace("trigger") << "Trigger for " << qa.quantToString(q) << ": "
<< std::endl;
for (const Node& n : d_nodes)
std::map< Node, std::vector< Node > > varContains;
for (const Node& pat : temp)
{
- quantifiers::TermUtil::computeInstConstContainsForQuant(
- q, pat, varContains[pat]);
+ TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
}
for (const Node& t : temp)
{
bool foundVar = false;
for (const Node& v : vct)
{
- Assert(quantifiers::TermUtil::getInstConstAttr(v) == q);
+ Assert(TermUtil::getInstConstAttr(v) == q);
if( vars.find( v )==vars.end() ){
varCount++;
vars[ v ] = true;
}
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
Node f,
std::vector<Node>& nodes,
bool keepAll,
Trigger* t;
if (!ho_apps.empty())
{
- t = new HigherOrderTrigger(qe, qs, qim, qr, f, trNodes, ho_apps);
+ t = new HigherOrderTrigger(qe, qs, qim, qr, tr, f, trNodes, ho_apps);
}
else
{
- t = new Trigger(qe, qs, qim, qr, f, trNodes);
+ t = new Trigger(qe, qs, qim, qr, tr, f, trNodes);
}
qe->getTriggerDatabase()->addTrigger( trNodes, t );
}
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
Node f,
Node n,
bool keepAll,
{
std::vector< Node > nodes;
nodes.push_back( n );
- return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars);
+ return mkTrigger(qe, qs, qim, qr, tr, f, nodes, keepAll, trOption, useNVars);
}
int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
{
visited[cur] = cur;
}
- else if (!quantifiers::TermUtil::hasInstConstAttr(cur))
+ else if (!TermUtil::hasInstConstAttr(cur))
{
// cur has no INST_CONSTANT, thus is ground.
Node vcur = val.getPreprocessedTerm(cur);
Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl;
}
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace inst
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
class QuantifiersState;
class QuantifiersInferenceManager;
class QuantifiersRegistry;
-}
+class TermRegistry;
+class InstMatch;
namespace inst {
class IMGenerator;
-class InstMatch;
class InstMatchGenerator;
/** A collection of nodes representing a trigger.
*
TR_RETURN_NULL //return null if a duplicate is found
};
static Trigger* mkTrigger(QuantifiersEngine* qe,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
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::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
Node q,
Node n,
bool keepAll = true,
protected:
/** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
Trigger(QuantifiersEngine* ie,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
Node q,
std::vector<Node>& nodes);
/** add an instantiation (called by InstMatchGenerator)
// !!!!!!!!!!!!!!!!!! temporarily available (project #15)
QuantifiersEngine* d_quantEngine;
/** Reference to the quantifiers state */
- quantifiers::QuantifiersState& d_qstate;
+ QuantifiersState& d_qstate;
/** Reference to the quantifiers inference manager */
- quantifiers::QuantifiersInferenceManager& d_qim;
+ QuantifiersInferenceManager& d_qim;
/** The quantifiers registry */
- quantifiers::QuantifiersRegistry& d_qreg;
+ QuantifiersRegistry& d_qreg;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
/** The quantified formula this trigger is for. */
Node d_quant;
/** match generator
IMGenerator* d_mg;
}; /* class Trigger */
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace inst
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
void TriggerTermInfo::init(Node q, Node n, int reqPol, Node reqPolEq)
}
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
/** Information about a node used in a trigger.
};
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
TriggerTrie::TriggerTrie() {}
}
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
-
+namespace quantifiers {
namespace inst {
/** A trie of triggers.
}; /* class inst::Trigger::TriggerTrie */
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Trigger* tparent,
}
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace CVC4 {
namespace theory {
+namespace quantifiers {
namespace inst {
/** match generator for purified terms
};
} // namespace inst
+} // namespace quantifiers
} // namespace theory
} // namespace CVC4
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
-using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::theory::inst;
-using namespace CVC4::theory::quantifiers::fmcheck;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+namespace fmcheck {
struct ModelBasisArgSort
{
{
return d_unhandledQuant.find(q) == d_unhandledQuant.end();
}
+
+} // namespace fmcheck
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers_engine.h"
-using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
//Model Engine constructor
ModelEngine::ModelEngine(QuantifiersEngine* qe,
//d_quantEngine->getModel()->debugPrint( c );
}
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
namespace CVC4 {
namespace theory {
-namespace inst {
+namespace quantifiers {
InstMatch::InstMatch(TNode q)
{
return true;
}
-}/* CVC4::theory::inst namespace */
+} // namespace quantifiers
}/* CVC4::theory namespace */
}/* CVC4 namespace */
namespace CVC4 {
namespace theory {
-
namespace quantifiers {
-class QuantifiersState;
-}
-namespace inst {
+class QuantifiersState;
/** Inst match
*
return out;
}
-}/* CVC4::theory::inst namespace */
-
-typedef CVC4::theory::inst::InstMatch InstMatch;
-
+} // namespace quantifiers
}/* CVC4::theory namespace */
}/* CVC4 namespace */
namespace CVC4 {
namespace theory {
-namespace inst {
+namespace quantifiers {
bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
Node q,
return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
}
-} /* CVC4::theory::inst namespace */
+} // namespace quantifiers
} /* CVC4::theory namespace */
} /* CVC4 namespace */
namespace CVC4 {
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
-class QuantifiersState;
-}
-namespace inst {
+class QuantifiersState;
/** trie for InstMatch objects
*
* If modEq is true, we check for duplication modulo equality the current
* equalities in the equality engine of qs.
*/
- bool existsInstMatch(quantifiers::QuantifiersState& qs,
+ bool existsInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false,
* If modEq is true, we check for duplication modulo equality the current
* equalities in the equality engine of qs.
*/
- bool addInstMatch(quantifiers::QuantifiersState& qs,
+ bool addInstMatch(QuantifiersState& qs,
Node f,
const std::vector<Node>& m,
bool modEq = false,
* equalities in the equality engine of qs.
* It additionally takes a context c, for which the entry is valid in.
*/
- bool existsInstMatch(quantifiers::QuantifiersState& qs,
+ bool existsInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false,
* equalities in the equality engine of qs.
* It additionally takes a context c, for which the entry is valid in.
*/
- bool addInstMatch(quantifiers::QuantifiersState& qs,
+ bool addInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false,
* class. If modEq is true, we consider duplicates modulo the current
* equalities stored in the equality engine of qs.
*/
- bool addInstMatch(quantifiers::QuantifiersState& qs,
+ bool addInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false);
* class. If modEq is true, we consider duplicates modulo the current
* equalities stored in the equality engine of qs.
*/
- bool existsInstMatch(quantifiers::QuantifiersState& qs,
+ bool existsInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false);
InstMatchTrie d_imt;
};
-} /* CVC4::theory::inst namespace */
+} // namespace quantifiers
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */
using namespace context;
namespace theory {
+namespace quantifiers {
using namespace inst;
-namespace quantifiers {
-
InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
- FirstOrderModel* m,
ProofNodeManager* pnm)
: d_qstate(qs),
d_qim(qim),
d_qreg(qr),
d_treg(tr),
- d_model(m),
d_pnm(pnm),
d_total_inst_debug(qs.getUserContext()),
d_c_inst_match_trie_dom(qs.getUserContext()),
Instantiate::~Instantiate()
{
- for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+ for (std::pair<const Node, CDInstMatchTrie*>& t : d_c_inst_match_trie)
{
delete t.second;
}
TypeNode tn = q[0][i].getType();
if (terms[i].isNull())
{
- terms[i] = getTermForType(tn);
+ terms[i] = d_treg.getTermForType(tn);
}
// Ensure the type is correct, this for instance ensures that real terms
// are cast to integers for { x -> t } where x has type Int and t has
{
// pick the best possible representative for instantiation, based on past
// use and simplicity of term
- terms[i] = d_model->getInternalRepresentative(terms[i], q, i);
+ terms[i] = d_treg.getModel()->getInternalRepresentative(terms[i], q, i);
}
Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
if (terms[i].isNull())
{
if (options::incrementalSolving())
{
- std::map<Node, inst::CDInstMatchTrie*>::iterator it =
- d_c_inst_match_trie.find(q);
+ std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
if (it != d_c_inst_match_trie.end())
{
return it->second->existsInstMatch(d_qstate, q, terms, modEq);
}
else
{
- std::map<Node, inst::InstMatchTrie>::iterator it =
- d_inst_match_trie.find(q);
+ std::map<Node, InstMatchTrie>::iterator it = d_inst_match_trie.find(q);
if (it != d_inst_match_trie.end())
{
return it->second.existsInstMatch(d_qstate, q, terms, modEq);
Trace("inst-add-debug")
<< "Adding into context-dependent inst trie, modEq = " << modEq
<< std::endl;
- inst::CDInstMatchTrie* imt;
- std::map<Node, inst::CDInstMatchTrie*>::iterator it =
- d_c_inst_match_trie.find(q);
+ CDInstMatchTrie* imt;
+ std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
if (it != d_c_inst_match_trie.end())
{
imt = it->second;
}
else
{
- imt = new inst::CDInstMatchTrie(d_qstate.getUserContext());
+ imt = new CDInstMatchTrie(d_qstate.getUserContext());
d_c_inst_match_trie[q] = imt;
}
d_c_inst_match_trie_dom.insert(q);
{
if (options::incrementalSolving())
{
- std::map<Node, inst::CDInstMatchTrie*>::iterator it =
- d_c_inst_match_trie.find(q);
+ std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
if (it != d_c_inst_match_trie.end())
{
return it->second->removeInstMatch(q, terms);
return d_inst_match_trie[q].removeInstMatch(q, terms);
}
-Node Instantiate::getTermForType(TypeNode tn)
-{
- if (tn.isClosedEnumerable())
- {
- return d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0);
- }
- return d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn);
-}
-
void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
{
if (options::incrementalSolving())
}
else
{
- for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+ for (std::pair<const Node, InstMatchTrie>& t : d_inst_match_trie)
{
qs.push_back(t.first);
}
if (options::incrementalSolving())
{
- std::map<Node, inst::CDInstMatchTrie*>::const_iterator it =
+ std::map<Node, CDInstMatchTrie*>::const_iterator it =
d_c_inst_match_trie.find(q);
if (it != d_c_inst_match_trie.end())
{
}
else
{
- std::map<Node, inst::InstMatchTrie>::const_iterator it =
+ std::map<Node, InstMatchTrie>::const_iterator it =
d_inst_match_trie.find(q);
if (it != d_inst_match_trie.end())
{
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
- FirstOrderModel* m,
ProofNodeManager* pnm = nullptr);
~Instantiate();
* Same as above but with vars equal to the bound variables of q.
*/
Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false);
- /** get term for type
- *
- * This returns an arbitrary term for type tn.
- * This term is chosen heuristically to be the best
- * term for instantiation. Currently, this
- * heuristic enumerates the first term of the
- * type if the type is closed enumerable, otherwise
- * an existing ground term from the term database if
- * one exists, or otherwise a fresh variable.
- */
- Node getTermForType(TypeNode tn);
//--------------------------------------end general utilities
/**
QuantifiersRegistry& d_qreg;
/** Reference to the term registry */
TermRegistry& d_treg;
- /** Pointer to the model */
- FirstOrderModel* d_model;
/** pointer to the proof node manager */
ProofNodeManager* d_pnm;
/** instantiation rewriter classes */
* We store context (dependent, independent) versions. If incremental solving
* is disabled, we use d_inst_match_trie for performance reasons.
*/
- std::map<Node, inst::InstMatchTrie> d_inst_match_trie;
- std::map<Node, inst::CDInstMatchTrie*> d_c_inst_match_trie;
+ std::map<Node, InstMatchTrie> d_inst_match_trie;
+ std::map<Node, CDInstMatchTrie*> d_c_inst_match_trie;
/**
* The list of quantified formulas for which the domain of d_c_inst_match_trie
* is valid.
QuantifiersState& state,
QuantifiersRegistry& qr,
TermRegistry& tr,
- FirstOrderModel* m,
ProofNodeManager* pnm)
: InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"),
- d_instantiate(new Instantiate(state, *this, qr, tr, m, pnm)),
+ d_instantiate(new Instantiate(state, *this, qr, tr, pnm)),
d_skolemize(new Skolemize(state, pnm))
{
}
QuantifiersState& state,
QuantifiersRegistry& qr,
TermRegistry& tr,
- FirstOrderModel* m,
ProofNodeManager* pnm);
~QuantifiersInferenceManager();
/** get instantiate utility */
#include "theory/quantifiers/quantifiers_modules.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_registry.h"
+#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
DecisionManager* dm,
std::vector<QuantifiersModule*>& modules)
{
}
if (!options::finiteModelFind() || options::fmfInstEngine())
{
- d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr));
+ d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr, tr));
modules.push_back(d_inst_engine.get());
}
if (options::cegqi())
Trace("quant-init-debug")
<< "Initialize model engine, mbqi : " << options::mbqiMode() << " "
<< options::fmfBound() << std::endl;
- if (useFmcModel())
+ if (tr.useFmcModel())
{
Trace("quant-init-debug") << "...make fmc builder." << std::endl;
d_builder.reset(new fmcheck::FullModelChecker(qs, qr));
}
}
-bool QuantifiersModules::useFmcModel()
-{
- return options::mbqiMode() == options::MbqiMode::FMC
- || options::mbqiMode() == options::MbqiMode::TRUST
- || options::fmfBound();
-}
-
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
DecisionManager* dm,
std::vector<QuantifiersModule*>& modules);
- /** Whether we use the full model check builder and corresponding model */
- static bool useFmcModel();
-
private:
//------------------------------ quantifier utilities
/** relevant domain */
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
-using namespace std;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory::inst;
namespace CVC4 {
namespace theory {
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/first_order_model_fmc.h"
#include "theory/quantifiers/quantifiers_state.h"
namespace CVC4 {
TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
: d_presolve(qs.getUserContext(), true),
+ d_useFmcModel(false),
d_presolveCache(qs.getUserContext()),
d_termEnum(new TermEnumeration),
d_termDb(new TermDb(qs, qr)),
// must be constructed here since it is required for datatypes finistInit
d_sygusTdb.reset(new TermDbSygus(qs));
}
+ Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
+ Trace("quant-engine-debug")
+ << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
+ // Finite model finding requires specialized ways of building the model.
+ // We require constructing the model here, since it is required for
+ // initializing the CombinationEngine and the rest of quantifiers engine.
+ if ((options::finiteModelFind() || options::fmfBound())
+ && (options::mbqiMode() == options::MbqiMode::FMC
+ || options::mbqiMode() == options::MbqiMode::TRUST
+ || options::fmfBound()))
+ {
+ d_useFmcModel = true;
+ d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
+ qs, qr, *this, "FirstOrderModelFmc"));
+ }
+ else
+ {
+ d_qmodel.reset(
+ new quantifiers::FirstOrderModel(qs, qr, *this, "FirstOrderModel"));
+ }
}
void TermRegistry::finishInit(QuantifiersInferenceManager* qim)
}
}
+Node TermRegistry::getTermForType(TypeNode tn)
+{
+ if (tn.isClosedEnumerable())
+ {
+ return d_termEnum->getEnumerateTerm(tn, 0);
+ }
+ return d_termDb->getOrMakeTypeGroundTerm(tn);
+}
+
TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); }
TermDbSygus* TermRegistry::getTermDatabaseSygus() const
{
return d_termEnum.get();
}
+
+FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); }
+
+bool TermRegistry::useFmcModel() const { return d_useFmcModel; }
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
namespace theory {
namespace quantifiers {
+class FirstOrderModel;
+
/**
* Term Registry, which manages notifying modules within quantifiers about
* (ground) terms that exist in the current context.
*/
void addTerm(Node n, bool withinQuant = false);
+ /** get term for type
+ *
+ * This returns an arbitrary term for type tn.
+ * This term is chosen heuristically to be the best
+ * term for instantiation. Currently, this
+ * heuristic enumerates the first term of the
+ * type if the type is closed enumerable, otherwise
+ * an existing ground term from the term database if
+ * one exists, or otherwise a fresh variable.
+ */
+ Node getTermForType(TypeNode tn);
+
+ /** Whether we use the full model check builder and corresponding model */
+ bool useFmcModel() const;
+
/** get term database */
TermDb* getTermDatabase() const;
/** get term database sygus */
TermDbSygus* getTermDatabaseSygus() const;
/** get term enumeration utility */
TermEnumeration* getTermEnumeration() const;
+ /** get the model utility */
+ FirstOrderModel* getModel() const;
private:
/** has presolve been called */
context::CDO<bool> d_presolve;
+ /** Whether we are using the fmc model */
+ bool d_useFmcModel;
/** the set of terms we have seen before presolve */
NodeSet d_presolveCache;
/** term enumeration utility */
std::unique_ptr<TermDb> d_termDb;
/** sygus term database */
std::unique_ptr<TermDbSygus> d_sygusTdb;
+ /** extended model object */
+ std::unique_ptr<FirstOrderModel> d_qmodel;
};
} // namespace quantifiers
#include "theory/strings/word.h"
#include "theory/rewriter.h"
-using namespace std;
using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory::inst;
namespace CVC4 {
namespace theory {
#include "expr/proof_node_manager.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/first_order_model_fmc.h"
#include "theory/quantifiers/quantifiers_modules.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/valuation.h"
d_qstate(c, u, valuation, logicInfo),
d_qreg(),
d_treg(d_qstate, d_qreg),
- d_qim(nullptr),
+ d_qim(*this, d_qstate, d_qreg, d_treg, pnm),
d_qengine(nullptr)
{
out.handleUserAttribute( "fun-def", this );
d_qChecker.registerTo(pc);
}
- Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
- Trace("quant-engine-debug")
- << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
- // Finite model finding requires specialized ways of building the model.
- // We require constructing the model here, since it is required for
- // initializing the CombinationEngine and the rest of quantifiers engine.
- if ((options::finiteModelFind() || options::fmfBound())
- && QuantifiersModules::useFmcModel())
- {
- d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
- d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
- }
- else
- {
- d_qmodel.reset(new quantifiers::FirstOrderModel(
- d_qstate, d_qreg, d_treg, "FirstOrderModel"));
- }
-
- d_qim.reset(new QuantifiersInferenceManager(
- *this, d_qstate, d_qreg, d_treg, d_qmodel.get(), pnm));
-
// Finish initializing the term registry by hooking it up to the inference
// manager. This is required due to a cyclic dependency between the term
// database and the instantiate module. Term database needs inference manager
// since it sends out lemmas when term indexing is inconsistent, instantiate
// needs term database for entailment checks.
- d_treg.finishInit(d_qim.get());
+ d_treg.finishInit(&d_qim);
// construct the quantifiers engine
- d_qengine.reset(new QuantifiersEngine(
- d_qstate, d_qreg, d_treg, *d_qim.get(), d_qmodel.get(), pnm));
+ d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm));
//!!!!!!!!!!!!!! temporary (project #15)
- d_qmodel->finishInit(d_qengine.get());
+ d_treg.getModel()->finishInit(d_qengine.get());
// indicate we are using the quantifiers theory state object
d_theoryState = &d_qstate;
// use the inference manager as the official inference manager
- d_inferManager = d_qim.get();
+ d_inferManager = &d_qim;
// Set the pointer to the quantifiers engine, which this theory owns. This
// pointer will be retreived by TheoryEngine and set to all theories
// post-construction.
#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
#include "expr/node.h"
-#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/proof_checker.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
#include "theory/quantifiers/quantifiers_registry.h"
QuantifiersState d_qstate;
/** The quantifiers registry */
QuantifiersRegistry d_qreg;
- /** extended model object */
- std::unique_ptr<FirstOrderModel> d_qmodel;
/** The term registry */
TermRegistry d_treg;
/** The quantifiers inference manager */
- std::unique_ptr<QuantifiersInferenceManager> d_qim;
+ QuantifiersInferenceManager d_qim;
/** The quantifiers engine, which lives here */
std::unique_ptr<QuantifiersEngine> d_qengine;
};/* class TheoryQuantifiers */
quantifiers::QuantifiersRegistry& qr,
quantifiers::TermRegistry& tr,
quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::FirstOrderModel* qm,
ProofNodeManager* pnm)
: d_qstate(qstate),
d_qim(qim),
d_pnm(pnm),
d_qreg(qr),
d_treg(tr),
- d_tr_trie(new inst::TriggerTrie),
- d_model(qm),
+ d_tr_trie(new quantifiers::inst::TriggerTrie),
+ d_model(d_treg.getModel()),
d_quants_prereg(qstate.getUserContext()),
d_quants_red(qstate.getUserContext())
{
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_qreg, dm, d_modules);
+ d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_treg, dm, d_modules);
if (d_qmodules->d_rel_dom.get())
{
d_util.push_back(d_qmodules->d_rel_dom.get());
{
return d_qim.getSkolemize();
}
-inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
+quantifiers::inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
{
return d_tr_trie.get();
}
class QuantifiersModule;
class RepSetIterator;
+namespace quantifiers {
+
namespace inst {
class TriggerTrie;
}
-namespace quantifiers {
+
class FirstOrderModel;
class Instantiate;
class QModelBuilder;
quantifiers::QuantifiersRegistry& qr,
quantifiers::TermRegistry& tr,
quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::FirstOrderModel* qm,
ProofNodeManager* pnm);
~QuantifiersEngine();
//---------------------- external interface
/** get skolemize utility */
quantifiers::Skolemize* getSkolemize() const;
/** get trigger database */
- inst::TriggerTrie* getTriggerDatabase() const;
+ quantifiers::inst::TriggerTrie* getTriggerDatabase() const;
//---------------------- end utilities
private:
//---------------------- private initialization
/** The term registry */
quantifiers::TermRegistry& d_treg;
/** all triggers will be stored in this trie */
- std::unique_ptr<inst::TriggerTrie> d_tr_trie;
+ std::unique_ptr<quantifiers::inst::TriggerTrie> d_tr_trie;
/** extended model object */
quantifiers::FirstOrderModel* d_model;
//------------- end quantifiers utilities
projects / cvc5.git / commitdiff