This PR centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine.
theory/quantifiers/ematching/pattern_term_selector.h
theory/quantifiers/ematching/trigger.cpp
theory/quantifiers/ematching/trigger.h
+ theory/quantifiers/ematching/trigger_database.cpp
+ theory/quantifiers/ematching/trigger_database.h
theory/quantifiers/ematching/trigger_term_info.cpp
theory/quantifiers/ematching/trigger_term_info.h
theory/quantifiers/ematching/trigger_trie.cpp
theory/quantifiers/quantifiers_rewriter.h
theory/quantifiers/quantifiers_state.cpp
theory/quantifiers/quantifiers_state.h
+ theory/quantifiers/quantifiers_statistics.cpp
+ theory/quantifiers/quantifiers_statistics.h
theory/quantifiers/query_generator.cpp
theory/quantifiers/query_generator.h
theory/quantifiers/relevant_domain.cpp
namespace inst {
HigherOrderTrigger::HigherOrderTrigger(
- QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
Node q,
std::vector<Node>& nodes,
std::map<Node, std::vector<Node> >& ho_apps)
- : Trigger(qe, qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps)
+ : Trigger(qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps)
{
NodeManager* nm = NodeManager::currentNM();
// process the higher-order variable applications
*/
class HigherOrderTrigger : public Trigger
{
- friend class Trigger;
-
- private:
- HigherOrderTrigger(QuantifiersEngine* qe,
- QuantifiersState& qs,
+ public:
+ HigherOrderTrigger(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
std::map<Node, std::vector<Node> >& ho_apps);
virtual ~HigherOrderTrigger();
- public:
/** Collect higher order var apply terms
*
* Collect all top-level HO_APPLY terms in n whose head is a variable x in
/** higher-order pattern unification algorithm
*
- * Sends an instantiation that is equivalent to m via
- * d_quantEngine->addInstantiation(...),
- * based on Huet's algorithm.
- *
- * This is a helper function of sendInstantiation( m ) above.
- *
- * var_index is the index of the variable in m that we are currently processing
- * i.e. we are processing the var_index^{th} higher-order variable.
- *
- * For example, say we are processing the match from (EX4) above.
- * when var_index = 0,1, we are processing possibilities for
- * instantiation of f1,f2 respectively.
- */
+ * Sends an instantiation that is equivalent to m via
+ * Instantiate::addInstantiation(...),
+ * based on Huet's algorithm.
+ *
+ * This is a helper function of sendInstantiation( m ) above.
+ *
+ * var_index is the index of the variable in m that we are currently
+ * processing i.e. we are processing the var_index^{th} higher-order variable.
+ *
+ * For example, say we are processing the match from (EX4) above.
+ * when var_index = 0,1, we are processing possibilities for
+ * instantiation of f1,f2 respectively.
+ */
bool sendInstantiation(std::vector<Node>& m, size_t var_index);
/** higher-order pattern unification algorithm
* Sends an instantiation that is equivalent to m via
- * d_quantEngine->addInstantiation(...).
+ * Instantiate::addInstantiation(...).
* This is a helper function of sendInstantiation( m, var_index ) above.
*
* var_index is the index of the variable in m that we are currently
return d_tparent->sendInstantiation(m, id);
}
-QuantifiersEngine* IMGenerator::getQuantifiersEngine()
-{
- return d_tparent->d_quantEngine;
-}
-
} // namespace inst
} // namespace quantifiers
} // namespace theory
QuantifiersState& d_qstate;
/** Reference to the term registry */
TermRegistry& d_treg;
- // !!!!!!!!! temporarily available (project #15)
- QuantifiersEngine* getQuantifiersEngine();
};/* class IMGenerator */
} // namespace inst
#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"
if( d_match_pattern.isNull() ){
return -1;
}
- quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ quantifiers::TermDb* tdb = d_treg.getTermDatabase();
if (TriggerTermInfo::isAtomicTrigger(d_match_pattern))
{
Node f = tdb->getMatchOperator(d_match_pattern);
d_match_pattern_type = d_match_pattern.getType();
Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is "
<< d_match_pattern << std::endl;
- quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ quantifiers::TermDb* tdb = d_treg.getTermDatabase();
d_match_pattern_op = tdb->getMatchOperator(d_match_pattern);
// now, collect children of d_match_pattern
#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/trigger_term_info.h"
-#include "theory/quantifiers/ematching/trigger_trie.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;
}
d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
}
- TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ TermDb* tdb = d_treg.getTermDatabase();
d_op = tdb->getMatchOperator(d_match_pattern);
}
{
uint64_t addedLemmas = 0;
TNodeTrie* tat;
- TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ TermDb* tdb = d_treg.getTermDatabase();
if (d_eqc.isNull())
{
tat = tdb->getTermArgTrie(d_op);
int InstMatchGeneratorSimple::getActiveScore()
{
- TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ TermDb* tdb = d_treg.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 theory {
namespace quantifiers {
-InstStrategy::InstStrategy(QuantifiersEngine* qe,
+InstStrategy::InstStrategy(inst::TriggerDatabase& td,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr)
- : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
+ : d_td(td), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
{
}
InstStrategy::~InstStrategy() {}
namespace CVC4 {
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
+namespace inst {
+class TriggerDatabase;
+}
+
class QuantifiersState;
class QuantifiersInferenceManager;
class QuantifiersRegistry;
class InstStrategy
{
public:
- InstStrategy(QuantifiersEngine* qe,
+ InstStrategy(inst::TriggerDatabase& td,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
* maintained by the quantifiers state.
*/
options::UserPatMode getInstUserPatMode() const;
- /** reference to the instantiation engine */
- QuantifiersEngine* d_quantEngine;
+ /** reference to the trigger database */
+ inst::TriggerDatabase& d_td;
/** The quantifiers state object */
QuantifiersState& d_qstate;
/** The quantifiers inference manager object */
#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
#include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/trigger_database.h"
#include "theory/quantifiers/quant_relevance.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
#include "theory/quantifiers/quantifiers_registry.h"
#include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers_engine.h"
#include "util/random.h"
using namespace CVC4::kind;
};
InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(
- QuantifiersEngine* qe,
+ inst::TriggerDatabase& td,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
QuantRelevance* qrlv)
- : InstStrategy(qe, qs, qim, qr, tr), d_quant_rel(qrlv)
+ : InstStrategy(td, qs, qim, qr, tr), d_quant_rel(qrlv)
{
//how to select trigger terms
d_tr_strategy = options::triggerSelMode();
Trigger* tr = NULL;
if (d_is_single_trigger[patTerms[0]])
{
- tr = Trigger::mkTrigger(d_quantEngine,
- d_qstate,
- d_qim,
- d_qreg,
- d_treg,
- f,
- patTerms[0],
- false,
- Trigger::TR_RETURN_NULL,
- d_num_trigger_vars[f]);
+ tr = d_td.mkTrigger(f,
+ patTerms[0],
+ false,
+ TriggerDatabase::TR_RETURN_NULL,
+ d_num_trigger_vars[f]);
d_single_trigger_gen[patTerms[0]] = true;
}
else
d_made_multi_trigger[f] = true;
}
// will possibly want to get an old trigger
- tr = Trigger::mkTrigger(d_quantEngine,
- d_qstate,
- d_qim,
- d_qreg,
- d_treg,
- f,
- patTerms,
- false,
- Trigger::TR_GET_OLD,
- d_num_trigger_vars[f]);
+ tr = d_td.mkTrigger(f,
+ patTerms,
+ false,
+ TriggerDatabase::TR_GET_OLD,
+ d_num_trigger_vars[f]);
}
if (tr == nullptr)
{
<= nqfs_curr)
{
d_single_trigger_gen[patTerms[index]] = true;
- Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
- d_qstate,
- d_qim,
- d_qreg,
- d_treg,
- f,
- patTerms[index],
- false,
- Trigger::TR_RETURN_NULL,
- d_num_trigger_vars[f]);
+ Trigger* tr2 = d_td.mkTrigger(f,
+ patTerms[index],
+ false,
+ TriggerDatabase::TR_RETURN_NULL,
+ d_num_trigger_vars[f]);
addTrigger(tr2, f);
success = true;
}
std::map<Node, bool> d_hasUserPatterns;
public:
- InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
+ InstStrategyAutoGenTriggers(inst::TriggerDatabase& td,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
#include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/trigger_database.h"
#include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
using namespace CVC4::theory::quantifiers::inst;
namespace quantifiers {
InstStrategyUserPatterns::InstStrategyUserPatterns(
- QuantifiersEngine* ie,
+ inst::TriggerDatabase& td,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr)
- : InstStrategy(ie, qs, qim, qr, tr)
+ : InstStrategy(td, qs, qim, qr, tr)
{
}
InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q];
for (size_t i = 0, usize = ugw.size(); i < usize; i++)
{
- Trigger* t = Trigger::mkTrigger(d_quantEngine,
- d_qstate,
- d_qim,
- d_qreg,
- d_treg,
- q,
- ugw[i],
- true,
- Trigger::TR_RETURN_NULL);
+ Trigger* t =
+ d_td.mkTrigger(q, ugw[i], true, TriggerDatabase::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,
- d_qstate,
- d_qim,
- d_qreg,
- d_treg,
- q,
- nodes,
- true,
- Trigger::TR_MAKE_NEW);
+ Trigger* t = d_td.mkTrigger(q, nodes, true, TriggerDatabase::TR_MAKE_NEW);
if (t)
{
d_user_gen[q].push_back(t);
class InstStrategyUserPatterns : public InstStrategy
{
public:
- InstStrategyUserPatterns(QuantifiersEngine* qe,
+ InstStrategyUserPatterns(inst::TriggerDatabase& td,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
d_isup(),
d_i_ag(),
d_quants(),
+ d_trdb(qs, qim, qr, tr),
d_quant_rel(nullptr)
{
if (options::relevantTriggers())
// user-provided patterns
if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
{
- d_isup.reset(
- new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr, tr));
+ d_isup.reset(new InstStrategyUserPatterns(d_trdb, 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, tr, d_quant_rel.get()));
+ d_trdb, qs, qim, qr, tr, d_quant_rel.get()));
d_instStrategies.push_back(d_i_ag.get());
}
}
void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
{
- CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time);
+ CodeTimer codeTimer(d_qstate.getStats().d_ematching_time);
if (quant_e != QEFFORT_STANDARD)
{
return;
size_t nquant = m->getNumAssertedQuantifiers();
for (size_t i = 0; i < nquant; i++)
{
- Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true);
+ Node q = m->getAssertedQuantifier(i, true);
if (shouldProcess(q) && m->isQuantifierActive(q))
{
quantActive = true;
#include <vector>
#include "theory/quantifiers/ematching/inst_strategy.h"
+#include "theory/quantifiers/ematching/trigger_database.h"
#include "theory/quantifiers/quant_module.h"
#include "theory/quantifiers/quant_relevance.h"
class InstStrategyAutoGenTriggers;
class InstantiationEngine : public QuantifiersModule {
- private:
- /** instantiation strategies */
- std::vector<InstStrategy*> d_instStrategies;
- /** user-pattern instantiation strategy */
- std::unique_ptr<InstStrategyUserPatterns> d_isup;
- /** auto gen triggers; only kept for destructor cleanup */
- std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag;
-
- /** current processing quantified formulas */
- std::vector<Node> d_quants;
-
- /** is the engine incomplete for this quantifier */
- bool isIncomplete(Node q);
- /** do instantiation round */
- void doInstantiationRound(Theory::Effort effort);
-
public:
InstantiationEngine(QuantifiersEngine* qe,
QuantifiersState& qs,
std::string identify() const override { return "InstEngine"; }
private:
+ /** is the engine incomplete for this quantifier */
+ bool isIncomplete(Node q);
+ /** do instantiation round */
+ void doInstantiationRound(Theory::Effort effort);
/** Return true if this module should process quantified formula q */
bool shouldProcess(Node q);
+ /** instantiation strategies */
+ std::vector<InstStrategy*> d_instStrategies;
+ /** user-pattern instantiation strategy */
+ std::unique_ptr<InstStrategyUserPatterns> d_isup;
+ /** auto gen triggers; only kept for destructor cleanup */
+ std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag;
+ /** current processing quantified formulas */
+ std::vector<Node> d_quants;
+ /** all triggers will be stored in this database */
+ inst::TriggerDatabase d_trdb;
/** for computing relevance of quantifiers */
std::unique_ptr<QuantRelevance> d_quant_rel;
}; /* class InstantiationEngine */
#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/candidate_generator.h"
-#include "theory/quantifiers/ematching/ho_trigger.h"
#include "theory/quantifiers/ematching/inst_match_generator.h"
#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
#include "theory/quantifiers/quantifiers_registry.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
#include "theory/valuation.h"
using namespace CVC4::kind;
namespace inst {
/** trigger class constructor */
-Trigger::Trigger(QuantifiersEngine* qe,
- QuantifiersState& qs,
+Trigger::Trigger(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_treg(tr),
- d_quant(q)
+ : 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.
Trace("trigger") << " " << n << std::endl;
}
}
+ QuantifiersStatistics& stats = qs.getStats();
if( d_nodes.size()==1 ){
if (TriggerTermInfo::isSimpleTrigger(d_nodes[0]))
{
d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]);
- ++(qe->d_statistics.d_triggers);
+ ++(stats.d_triggers);
}else{
d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]);
- ++(qe->d_statistics.d_simple_triggers);
+ ++(stats.d_simple_triggers);
}
}else{
if( options::multiTriggerCache() ){
Trace("multi-trigger") << " " << nc << std::endl;
}
}
- ++(qe->d_statistics.d_multi_triggers);
+ ++(stats.d_multi_triggers);
}
Trace("trigger-debug") << "Finished making trigger." << std::endl;
return sendInstantiation(m.d_vals, id);
}
-bool Trigger::mkTriggerTerms(Node q,
- std::vector<Node>& nodes,
- size_t nvars,
- std::vector<Node>& trNodes)
-{
- //only take nodes that contribute variables to the trigger when added
- std::vector< Node > temp;
- temp.insert( temp.begin(), nodes.begin(), nodes.end() );
- std::map< Node, bool > vars;
- std::map< Node, std::vector< Node > > patterns;
- size_t varCount = 0;
- std::map< Node, std::vector< Node > > varContains;
- for (const Node& pat : temp)
- {
- TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
- }
- for (const Node& t : temp)
- {
- const std::vector<Node>& vct = varContains[t];
- bool foundVar = false;
- for (const Node& v : vct)
- {
- Assert(TermUtil::getInstConstAttr(v) == q);
- if( vars.find( v )==vars.end() ){
- varCount++;
- vars[ v ] = true;
- foundVar = true;
- }
- }
- if( foundVar ){
- trNodes.push_back(t);
- for (const Node& v : vct)
- {
- patterns[v].push_back(t);
- }
- }
- if (varCount == nvars)
- {
- break;
- }
- }
- if (varCount < nvars)
- {
- Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
- Trace("trigger-debug") << nodes << std::endl;
- //do not generate multi-trigger if it does not contain all variables
- return false;
- }
- // now, minimize the trigger
- for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
- {
- bool keepPattern = false;
- Node n = trNodes[i];
- const std::vector<Node>& vcn = varContains[n];
- for (const Node& v : vcn)
- {
- if (patterns[v].size() == 1)
- {
- keepPattern = true;
- break;
- }
- }
- if (!keepPattern)
- {
- // remove from pattern vector
- for (const Node& v : vcn)
- {
- std::vector<Node>& pv = patterns[v];
- for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
- {
- if (pv[k] == n)
- {
- pv.erase(pv.begin() + k, pv.begin() + k + 1);
- break;
- }
- }
- }
- // remove from trigger nodes
- trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
- i--;
- }
- }
- return true;
-}
-
-Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr,
- TermRegistry& tr,
- Node f,
- std::vector<Node>& nodes,
- bool keepAll,
- int trOption,
- size_t useNVars)
-{
- std::vector< Node > trNodes;
- if( !keepAll ){
- size_t nvars = useNVars == 0 ? f[0].getNumChildren() : useNVars;
- if (!mkTriggerTerms(f, nodes, nvars, trNodes))
- {
- return nullptr;
- }
- }else{
- trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
- }
-
- //check for duplicate?
- if( trOption!=TR_MAKE_NEW ){
- Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
- if( t ){
- if( trOption==TR_GET_OLD ){
- //just return old trigger
- return t;
- }else{
- return nullptr;
- }
- }
- }
-
- // check if higher-order
- Trace("trigger-debug") << "Collect higher-order variable triggers..."
- << std::endl;
- std::map<Node, std::vector<Node> > ho_apps;
- HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
- Trace("trigger-debug") << "...got " << ho_apps.size()
- << " higher-order applications." << std::endl;
- Trigger* t;
- if (!ho_apps.empty())
- {
- t = new HigherOrderTrigger(qe, qs, qim, qr, tr, f, trNodes, ho_apps);
- }
- else
- {
- t = new Trigger(qe, qs, qim, qr, tr, f, trNodes);
- }
-
- qe->getTriggerDatabase()->addTrigger( trNodes, t );
- return t;
-}
-
-Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr,
- TermRegistry& tr,
- Node f,
- Node n,
- bool keepAll,
- int trOption,
- size_t useNVars)
-{
- std::vector< Node > nodes;
- nodes.push_back( n );
- return mkTrigger(qe, qs, qim, qr, tr, f, nodes, keepAll, trOption, useNVars);
-}
-
int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
friend class IMGenerator;
public:
+ /** trigger constructor */
+ Trigger(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
+ Node q,
+ std::vector<Node>& nodes);
virtual ~Trigger();
/** get the generator associated with this trigger */
IMGenerator* getGenerator() { return d_mg; }
int getActiveScore();
/** print debug information for the trigger */
void debugPrint(const char* c) const;
- /** mkTrigger method
- *
- * This makes an instance of a trigger object.
- * qe : pointer to the quantifier engine;
- * q : the quantified formula we are making a trigger for
- * nodes : the nodes comprising the (multi-)trigger
- * keepAll: don't remove unneeded patterns;
- * trOption : policy for dealing with triggers that already exist
- * (see below)
- * useNVars : number of variables that should be bound by the trigger
- * typically, the number of quantified variables in q.
- */
- enum{
- TR_MAKE_NEW, //make new trigger even if it already may exist
- TR_GET_OLD, //return a previous trigger if it had already been created
- TR_RETURN_NULL //return null if a duplicate is found
- };
- static Trigger* mkTrigger(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr,
- TermRegistry& tr,
- Node q,
- std::vector<Node>& nodes,
- bool keepAll = true,
- int trOption = TR_MAKE_NEW,
- size_t useNVars = 0);
- /** single trigger version that calls the above function */
- static Trigger* mkTrigger(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr,
- TermRegistry& tr,
- Node q,
- Node n,
- bool keepAll = true,
- int trOption = TR_MAKE_NEW,
- size_t useNVars = 0);
- /** make trigger terms
- *
- * This takes a set of eligible trigger terms and stores a subset of them in
- * trNodes, such that :
- * (1) the terms in trNodes contain at least n_vars of the quantified
- * variables in quantified formula q, and
- * (2) the set trNodes is minimal, i.e. removing one term from trNodes
- * always violates (1).
- */
- static bool mkTriggerTerms(Node q,
- std::vector<Node>& nodes,
- size_t nvars,
- std::vector<Node>& trNodes);
protected:
- /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
- Trigger(QuantifiersEngine* ie,
- QuantifiersState& qs,
- QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr,
- TermRegistry& tr,
- Node q,
- std::vector<Node>& nodes);
/** add an instantiation (called by InstMatchGenerator)
*
* This calls Instantiate::addInstantiation(...) for instantiations
* This example would fail to match when f(a) is not registered.
*/
std::vector<Node> d_groundTerms;
- // !!!!!!!!!!!!!!!!!! temporarily available (project #15)
- QuantifiersEngine* d_quantEngine;
/** Reference to the quantifiers state */
QuantifiersState& d_qstate;
/** Reference to the quantifiers inference manager */
--- /dev/null
+/********************* */
+/*! \file trigger_database.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief trigger database class
+ **/
+
+#include "theory/quantifiers/ematching/trigger_database.h"
+
+#include "theory/quantifiers/ematching/ho_trigger.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/term_util.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+namespace inst {
+
+TriggerDatabase::TriggerDatabase(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr)
+ : d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
+{
+}
+TriggerDatabase::~TriggerDatabase() {}
+
+Trigger* TriggerDatabase::mkTrigger(Node q,
+ const std::vector<Node>& nodes,
+ bool keepAll,
+ int trOption,
+ size_t useNVars)
+{
+ std::vector<Node> trNodes;
+ if (!keepAll)
+ {
+ size_t nvars = useNVars == 0 ? q[0].getNumChildren() : useNVars;
+ if (!mkTriggerTerms(q, nodes, nvars, trNodes))
+ {
+ return nullptr;
+ }
+ }
+ else
+ {
+ trNodes.insert(trNodes.begin(), nodes.begin(), nodes.end());
+ }
+
+ // check for duplicate?
+ if (trOption != TR_MAKE_NEW)
+ {
+ Trigger* t = d_trie.getTrigger(trNodes);
+ if (t)
+ {
+ if (trOption == TR_GET_OLD)
+ {
+ // just return old trigger
+ return t;
+ }
+ return nullptr;
+ }
+ }
+
+ // check if higher-order
+ Trace("trigger-debug") << "Collect higher-order variable triggers..."
+ << std::endl;
+ std::map<Node, std::vector<Node> > hoApps;
+ HigherOrderTrigger::collectHoVarApplyTerms(q, trNodes, hoApps);
+ Trace("trigger-debug") << "...got " << hoApps.size()
+ << " higher-order applications." << std::endl;
+ Trigger* t;
+ if (!hoApps.empty())
+ {
+ t = new HigherOrderTrigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps);
+ }
+ else
+ {
+ t = new Trigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes);
+ }
+ d_trie.addTrigger(trNodes, t);
+ return t;
+}
+
+Trigger* TriggerDatabase::mkTrigger(
+ Node q, Node n, bool keepAll, int trOption, size_t useNVars)
+{
+ std::vector<Node> nodes;
+ nodes.push_back(n);
+ return mkTrigger(q, nodes, keepAll, trOption, useNVars);
+}
+
+bool TriggerDatabase::mkTriggerTerms(Node q,
+ const std::vector<Node>& nodes,
+ size_t nvars,
+ std::vector<Node>& trNodes)
+{
+ // only take nodes that contribute variables to the trigger when added
+ std::map<Node, bool> vars;
+ std::map<Node, std::vector<Node> > patterns;
+ size_t varCount = 0;
+ std::map<Node, std::vector<Node> > varContains;
+ for (const Node& pat : nodes)
+ {
+ TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
+ }
+ for (const Node& t : nodes)
+ {
+ const std::vector<Node>& vct = varContains[t];
+ bool foundVar = false;
+ for (const Node& v : vct)
+ {
+ Assert(TermUtil::getInstConstAttr(v) == q);
+ if (vars.find(v) == vars.end())
+ {
+ varCount++;
+ vars[v] = true;
+ foundVar = true;
+ }
+ }
+ if (foundVar)
+ {
+ trNodes.push_back(t);
+ for (const Node& v : vct)
+ {
+ patterns[v].push_back(t);
+ }
+ }
+ if (varCount == nvars)
+ {
+ break;
+ }
+ }
+ if (varCount < nvars)
+ {
+ Trace("trigger-debug") << "Don't consider trigger since it does not "
+ "contain specified number of variables."
+ << std::endl;
+ Trace("trigger-debug") << nodes << std::endl;
+ // do not generate multi-trigger if it does not contain all variables
+ return false;
+ }
+ // now, minimize the trigger
+ for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
+ {
+ bool keepPattern = false;
+ Node n = trNodes[i];
+ const std::vector<Node>& vcn = varContains[n];
+ for (const Node& v : vcn)
+ {
+ if (patterns[v].size() == 1)
+ {
+ keepPattern = true;
+ break;
+ }
+ }
+ if (!keepPattern)
+ {
+ // remove from pattern vector
+ for (const Node& v : vcn)
+ {
+ std::vector<Node>& pv = patterns[v];
+ for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
+ {
+ if (pv[k] == n)
+ {
+ pv.erase(pv.begin() + k, pv.begin() + k + 1);
+ break;
+ }
+ }
+ }
+ // remove from trigger nodes
+ trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
+ i--;
+ }
+ }
+ return true;
+}
+
+} // namespace inst
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file trigger_database.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief trigger trie class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
+#define CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifiersInferenceManager;
+class QuantifiersState;
+class QuantifiersRegistry;
+class TermRegistry;
+
+namespace inst {
+
+/**
+ * A database of triggers, which manages how triggers are constructed.
+ */
+class TriggerDatabase
+{
+ public:
+ TriggerDatabase(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr);
+ ~TriggerDatabase();
+
+ /** mkTrigger method
+ *
+ * This makes an instance of a trigger object.
+ * qe : pointer to the quantifier engine;
+ * q : the quantified formula we are making a trigger for
+ * nodes : the nodes comprising the (multi-)trigger
+ * keepAll: don't remove unneeded patterns;
+ * trOption : policy for dealing with triggers that already exist
+ * (see below)
+ * useNVars : number of variables that should be bound by the trigger
+ * typically, the number of quantified variables in q.
+ */
+ enum
+ {
+ TR_MAKE_NEW, // make new trigger even if it already may exist
+ TR_GET_OLD, // return a previous trigger if it had already been created
+ TR_RETURN_NULL // return null if a duplicate is found
+ };
+ Trigger* mkTrigger(Node q,
+ const std::vector<Node>& nodes,
+ bool keepAll = true,
+ int trOption = TR_MAKE_NEW,
+ size_t useNVars = 0);
+ /** single trigger version that calls the above function */
+ Trigger* mkTrigger(Node q,
+ Node n,
+ bool keepAll = true,
+ int trOption = TR_MAKE_NEW,
+ size_t useNVars = 0);
+
+ /** make trigger terms
+ *
+ * This takes a set of eligible trigger terms and stores a subset of them in
+ * trNodes, such that :
+ * (1) the terms in trNodes contain at least n_vars of the quantified
+ * variables in quantified formula q, and
+ * (2) the set trNodes is minimal, i.e. removing one term from trNodes
+ * always violates (1).
+ */
+ static bool mkTriggerTerms(Node q,
+ const std::vector<Node>& nodes,
+ size_t nvars,
+ std::vector<Node>& trNodes);
+
+ private:
+ /** The trigger trie, containing the triggers */
+ TriggerTrie d_trie;
+ /** Reference to the quantifiers state */
+ QuantifiersState& d_qs;
+ /** Reference to the quantifiers inference manager */
+ QuantifiersInferenceManager& d_qim;
+ /** The quantifiers registry */
+ QuantifiersRegistry& d_qreg;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
+};
+
+} // namespace inst
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
-namespace CVC4 {
-
-using namespace kind;
-using namespace context;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+namespace CVC4 {
namespace theory {
namespace quantifiers {
-using namespace inst;
-
InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
/** check */
void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
{
- CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time);
+ CodeTimer codeTimer(d_qstate.getStats().d_qcf_time);
if (quant_e != QEFFORT_CONFLICT)
{
return;
const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; }
+QuantifiersStatistics& QuantifiersState::getStats() { return d_statistics; }
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
+#include "theory/quantifiers/quantifiers_statistics.h"
#include "theory/theory.h"
#include "theory/theory_state.h"
void debugPrintEqualityEngine(const char* c) const;
/** get the logic info */
const LogicInfo& getLogicInfo() const;
+ /** get the stats */
+ QuantifiersStatistics& getStats();
private:
/** The number of instantiation rounds in this SAT context */
uint64_t d_instWhenPhase;
/** Information about the logic we're operating within. */
const LogicInfo& d_logicInfo;
+ /** The statistics */
+ QuantifiersStatistics d_statistics;
};
} // namespace quantifiers
--- /dev/null
+/********************* */
+/*! \file quantifiers_statistics.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of quantifiers statistics class
+ **/
+
+#include "theory/quantifiers/quantifiers_statistics.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QuantifiersStatistics::QuantifiersStatistics()
+ : d_time("theory::QuantifiersEngine::time"),
+ d_qcf_time("theory::QuantifiersEngine::time_qcf"),
+ d_ematching_time("theory::QuantifiersEngine::time_ematching"),
+ d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
+ d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
+ d_instantiation_rounds_lc(
+ "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
+ d_triggers("QuantifiersEngine::Triggers", 0),
+ d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
+ d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
+ d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_time);
+ smtStatisticsRegistry()->registerStat(&d_qcf_time);
+ smtStatisticsRegistry()->registerStat(&d_ematching_time);
+ smtStatisticsRegistry()->registerStat(&d_num_quant);
+ smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
+ smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
+ smtStatisticsRegistry()->registerStat(&d_triggers);
+ smtStatisticsRegistry()->registerStat(&d_simple_triggers);
+ smtStatisticsRegistry()->registerStat(&d_multi_triggers);
+ smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
+}
+
+QuantifiersStatistics::~QuantifiersStatistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_time);
+ smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
+ smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
+ smtStatisticsRegistry()->unregisterStat(&d_num_quant);
+ smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
+ smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
+ smtStatisticsRegistry()->unregisterStat(&d_triggers);
+ smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
+ smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
+ smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file quantifiers_statistics.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Quantifiers statistics class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
+#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
+
+#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Statistics class for quantifiers, which contains all statistics that need
+ * to be tracked globally within the quantifiers theory.
+ */
+class QuantifiersStatistics
+{
+ public:
+ QuantifiersStatistics();
+ ~QuantifiersStatistics();
+ TimerStat d_time;
+ TimerStat d_qcf_time;
+ TimerStat d_ematching_time;
+ IntStat d_num_quant;
+ IntStat d_instantiation_rounds;
+ IntStat d_instantiation_rounds_lc;
+ IntStat d_triggers;
+ IntStat d_simple_triggers;
+ IntStat d_multi_triggers;
+ IntStat d_red_alpha_equiv;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */
#include "options/smt_options.h"
#include "options/uf_options.h"
#include "smt/smt_engine_scope.h"
-#include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/ematching/trigger_trie.h"
#include "theory/quantifiers/equality_query.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/first_order_model_fmc.h"
#include "theory/quantifiers/quantifiers_registry.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/quantifiers_statistics.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_registry.h"
-#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
-#include "theory/uf/equality_engine.h"
using namespace std;
using namespace CVC4::kind;
d_pnm(pnm),
d_qreg(qr),
d_treg(tr),
- d_tr_trie(new quantifiers::inst::TriggerTrie),
d_model(d_treg.getModel()),
d_quants_prereg(qstate.getUserContext()),
d_quants_red(qstate.getUserContext())
{
return d_treg.getTermDatabase();
}
-
-quantifiers::inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
-{
- return d_tr_trie.get();
-}
/// !!!!!!!!!!!!!!
void QuantifiersEngine::presolve() {
}
void QuantifiersEngine::check( Theory::Effort e ){
- CodeTimer codeTimer(d_statistics.d_time);
+ quantifiers::QuantifiersStatistics& stats = d_qstate.getStats();
+ CodeTimer codeTimer(stats.d_time);
Assert(d_qstate.getEqualityEngine() != nullptr);
if (!d_qstate.getEqualityEngine()->consistent())
{
}
if( e==Theory::EFFORT_LAST_CALL ){
- ++(d_statistics.d_instantiation_rounds_lc);
+ ++(stats.d_instantiation_rounds_lc);
}else if( e==Theory::EFFORT_FULL ){
- ++(d_statistics.d_instantiation_rounds);
+ ++(stats.d_instantiation_rounds);
}
Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
if( !lem.isNull() ){
Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
- ++(d_statistics.d_red_alpha_equiv);
+ ++(d_qstate.getStats().d_red_alpha_equiv);
}
}
d_quants_red_lem[q] = lem;
Trace("quant") << "QuantifiersEngine : Register quantifier ";
Trace("quant") << " : " << f << std::endl;
size_t prev_lemma_waiting = d_qim.numPendingLemmas();
- ++(d_statistics.d_num_quant);
+ ++(d_qstate.getStats().d_num_quant);
Assert(f.getKind() == FORALL);
// register with utilities
for (unsigned i = 0; i < d_util.size(); i++)
d_qim.getSkolemize()->getSkolemTermVectors(sks);
}
-QuantifiersEngine::Statistics::Statistics()
- : d_time("theory::QuantifiersEngine::time"),
- d_qcf_time("theory::QuantifiersEngine::time_qcf"),
- d_ematching_time("theory::QuantifiersEngine::time_ematching"),
- d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
- d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
- d_instantiation_rounds_lc(
- "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
- d_triggers("QuantifiersEngine::Triggers", 0),
- d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
- d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
- d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
-{
- smtStatisticsRegistry()->registerStat(&d_time);
- smtStatisticsRegistry()->registerStat(&d_qcf_time);
- smtStatisticsRegistry()->registerStat(&d_ematching_time);
- smtStatisticsRegistry()->registerStat(&d_num_quant);
- smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
- smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
- smtStatisticsRegistry()->registerStat(&d_triggers);
- smtStatisticsRegistry()->registerStat(&d_simple_triggers);
- smtStatisticsRegistry()->registerStat(&d_multi_triggers);
- smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
-}
-
-QuantifiersEngine::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_time);
- smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
- smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
- smtStatisticsRegistry()->unregisterStat(&d_num_quant);
- smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
- smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
- smtStatisticsRegistry()->unregisterStat(&d_triggers);
- smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
- smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
- smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
-}
-
Node QuantifiersEngine::getNameForQuant(Node q) const
{
return d_qreg.getNameForQuant(q);
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "theory/quantifiers/quant_util.h"
-#include "util/statistics_registry.h"
namespace CVC4 {
namespace quantifiers {
-namespace inst {
-class TriggerTrie;
-}
-
class FirstOrderModel;
class Instantiate;
class QModelBuilder;
class QuantifiersEngine {
friend class ::CVC4::TheoryEngine;
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
- typedef context::CDList<Node> NodeList;
- typedef context::CDList<bool> BoolList;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
quantifiers::FirstOrderModel* getModel() const;
/** get term database sygus */
quantifiers::TermDbSygus* getTermDatabaseSygus() const;
- /** get trigger database */
- quantifiers::inst::TriggerTrie* getTriggerDatabase() const;
//---------------------- end utilities
private:
//---------------------- private initialization
//----------end user interface for instantiations
- /** statistics class */
- class Statistics
- {
- public:
- TimerStat d_time;
- TimerStat d_qcf_time;
- TimerStat d_ematching_time;
- IntStat d_num_quant;
- IntStat d_instantiation_rounds;
- IntStat d_instantiation_rounds_lc;
- IntStat d_triggers;
- IntStat d_simple_triggers;
- IntStat d_multi_triggers;
- IntStat d_red_alpha_equiv;
- Statistics();
- ~Statistics();
- };/* class QuantifiersEngine::Statistics */
- Statistics d_statistics;
-
private:
/** The quantifiers state object */
quantifiers::QuantifiersState& d_qstate;
quantifiers::QuantifiersRegistry& d_qreg;
/** The term registry */
quantifiers::TermRegistry& d_treg;
- /** all triggers will be stored in this trie */
- std::unique_ptr<quantifiers::inst::TriggerTrie> d_tr_trie;
/** extended model object */
quantifiers::FirstOrderModel* d_model;
//------------- end quantifiers utilities
projects / cvc5.git / commitdiff