This makes quantifiers use standard inference ids.
This eliminates the need to track ad-hoc statistics, per instantiation type.
This makes minor modifications to a few interfaces in quantifiers to enable this.
return "DATATYPES_SYGUS_MT_BOUND";
case InferenceId::DATATYPES_SYGUS_MT_POS: return "DATATYPES_SYGUS_MT_POS";
+ case InferenceId::QUANTIFIERS_INST_E_MATCHING:
+ return "QUANTIFIERS_INST_E_MATCHING";
+ case InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE:
+ return "QUANTIFIERS_INST_E_MATCHING_SIMPLE";
+ case InferenceId::QUANTIFIERS_INST_E_MATCHING_MT:
+ return "QUANTIFIERS_INST_E_MATCHING_MT";
+ case InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL:
+ return "QUANTIFIERS_INST_E_MATCHING_MTL";
+ case InferenceId::QUANTIFIERS_INST_E_MATCHING_HO:
+ return "QUANTIFIERS_INST_E_MATCHING_HO";
+ case InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN:
+ return "QUANTIFIERS_INST_E_MATCHING_VAR_GEN";
+ case InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT:
+ return "QUANTIFIERS_INST_CBQI_CONFLICT";
+ case InferenceId::QUANTIFIERS_INST_CBQI_PROP:
+ return "QUANTIFIERS_INST_CBQI_PROP";
+ case InferenceId::QUANTIFIERS_INST_FMF_EXH:
+ return "QUANTIFIERS_INST_FMF_EXH";
+ case InferenceId::QUANTIFIERS_INST_FMF_FMC:
+ return "QUANTIFIERS_INST_FMF_FMC";
+ case InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH:
+ return "QUANTIFIERS_INST_FMF_FMC_EXH";
+ case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI";
+ case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI";
+ case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM";
+ case InferenceId::QUANTIFIERS_CEGQI_CEX_DEP:
+ return "QUANTIFIERS_CEGQI_CEX_DEP";
+ case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA:
+ return "QUANTIFIERS_CEGQI_VTS_LB_DELTA";
+ case InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA:
+ return "QUANTIFIERS_CEGQI_VTS_UB_DELTA";
+ case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF:
+ return "QUANTIFIERS_CEGQI_VTS_LB_INF";
+ case InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD:
+ return "QUANTIFIERS_SYQI_EVAL_UNFOLD";
+ case InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC:
+ return "QUANTIFIERS_SYGUS_QE_PREPROC";
+ case InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT:
+ return "QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT";
+ case InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT:
+ return "QUANTIFIERS_SYGUS_EXCLUDE_CURRENT";
+ case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT:
+ return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT";
+ case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA:
+ return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA";
+ case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE";
+ case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ:
+ return "QUANTIFIERS_REDUCE_ALPHA_EQ";
+
case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";
// ---------------------------------- end datatypes theory
//-------------------------------------- quantifiers theory
- // skolemization
- QUANTIFIERS_SKOLEMIZE,
- // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent
- QUANTIFIERS_REDUCE_ALPHA_EQ,
+ //-------------------- types of instantiations.
+ // Notice the identifiers in this section cover all the techniques used for
+ // quantifier instantiation. The subcategories below are for specific lemmas
+ // that are not instantiation lemmas added, per technique.
+ // instantiation from E-matching
+ QUANTIFIERS_INST_E_MATCHING,
+ // E-matching using simple trigger implementation
+ QUANTIFIERS_INST_E_MATCHING_SIMPLE,
+ // E-matching using multi-triggers
+ QUANTIFIERS_INST_E_MATCHING_MT,
+ // E-matching using linear implementation of multi-triggers
+ QUANTIFIERS_INST_E_MATCHING_MTL,
+ // instantiation due to higher-order matching on top of e-matching
+ QUANTIFIERS_INST_E_MATCHING_HO,
+ // E-matching based on variable triggers
+ QUANTIFIERS_INST_E_MATCHING_VAR_GEN,
+ // conflicting instantiation from conflict-based instantiation
+ QUANTIFIERS_INST_CBQI_CONFLICT,
+ // propagating instantiation from conflict-based instantiation
+ QUANTIFIERS_INST_CBQI_PROP,
+ // instantiation from naive exhaustive instantiation in finite model finding
+ QUANTIFIERS_INST_FMF_EXH,
+ // instantiation from finite model finding based on its model-based algorithm
+ QUANTIFIERS_INST_FMF_FMC,
+ // instantiation from running exhaustive instantiation on a subdomain of
+ // the quantified formula in finite model finding based on its model-based
+ // algorithm
+ QUANTIFIERS_INST_FMF_FMC_EXH,
+ // instantiations from counterexample-guided instantiation
+ QUANTIFIERS_INST_CEGQI,
+ // instantiations from syntax-guided instantiation
+ QUANTIFIERS_INST_SYQI,
+ // instantiations from enumerative instantiation
+ QUANTIFIERS_INST_ENUM,
//-------------------- counterexample-guided instantiation
// G2 => G1 where G2 is a counterexample literal for a nested quantifier whose
// counterexample literal is G1.
QUANTIFIERS_CEGQI_VTS_UB_DELTA,
// infinity > c
QUANTIFIERS_CEGQI_VTS_LB_INF,
+ //-------------------- syntax-guided instantiation
+ // evaluation unfolding for syntax-guided instantiation
+ QUANTIFIERS_SYQI_EVAL_UNFOLD,
//-------------------- sygus solver
// preprocessing a sygus conjecture based on quantifier elimination, of the
// form Q <=> Q_preprocessed
QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT,
// ~Q where Q is a PBE conjecture with conflicting examples
QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA,
+ //-------------------- reductions
+ // skolemization
+ QUANTIFIERS_SKOLEMIZE,
+ // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent
+ QUANTIFIERS_REDUCE_ALPHA_EQ,
//-------------------------------------- end quantifiers theory
// ---------------------------------- sep theory
//check if we need virtual term substitution (if used delta or infinity)
bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
if (d_quantEngine->getInstantiate()->addInstantiation(
- d_curr_quant, subs, false, false, used_vts))
+ d_curr_quant,
+ subs,
+ InferenceId::QUANTIFIERS_INST_CEGQI,
+ false,
+ false,
+ used_vts))
{
- ++(d_quantEngine->d_statistics.d_instantiations_cbqi);
- //d_added_inst.insert( d_curr_quant );
return true;
}else{
//this should never happen for monotonic selection strategies
return addedHoLemmas + addedFoLemmas;
}
-bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
+bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
{
if (options::hoMatching())
{
std::vector<TNode> subs;
for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
{
- subs.push_back(m.d_vals[i]);
+ subs.push_back(m[i]);
vars.push_back(d_qreg.getInstantiationConstant(d_quant, i));
}
{
TNode var = ha.first;
unsigned vnum = var.getAttribute(InstVarNumAttribute());
- TNode value = m.d_vals[vnum];
+ TNode value = m[vnum];
Trace("ho-unif-debug") << " val[" << var << "] = " << value << std::endl;
Trace("ho-unif-debug2") << "initialize lambda information..."
else
{
// do not run higher-order matching
- return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
}
}
// recursion depth limited by number of arguments of higher order variables
// occurring as pattern operators (very small)
-bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
+bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m,
+ size_t var_index)
{
Trace("ho-unif-debug2") << "send inst " << var_index << " / "
<< d_ho_var_list.size() << std::endl;
if (var_index == d_ho_var_list.size())
{
// we now have an instantiation to try
- return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
+ return d_quantEngine->getInstantiate()->addInstantiation(
+ d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO);
}
else
{
Node var = d_ho_var_list[var_index];
unsigned vnum = var.getAttribute(InstVarNumAttribute());
- Assert(vnum < m.d_vals.size());
- Node value = m.d_vals[vnum];
+ Assert(vnum < m.size());
+ Node value = m[vnum];
Assert(d_lchildren[vnum][0] == value);
Assert(d_ho_var_bvl.find(var) != d_ho_var_bvl.end());
sendInstantiationArg(m, var_index, vnum, 0, d_ho_var_bvl[var], false);
// reset the value
- m.d_vals[vnum] = value;
+ m[vnum] = value;
return ret;
}
}
-bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
+bool HigherOrderTrigger::sendInstantiationArg(std::vector<Node>& m,
unsigned var_index,
unsigned vnum,
unsigned arg_index,
NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_lchildren[vnum]);
Trace("ho-unif-debug2") << " got " << body << std::endl;
Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, lbvl, body);
- m.d_vals[vnum] = lam;
+ m[vnum] = lam;
Trace("ho-unif-debug2") << " try " << vnum << " -> " << lam << std::endl;
}
return sendInstantiation(m, var_index + 1);
/** HigherOrder trigger
*
* This extends the trigger class with techniques that post-process
- * instantiations, specified by InstMatch objects, according to a variant of
+ * instantiations, specified by vectors of terms, according to a variant of
* Huet's algorithm. For details, see Chapter 16 of the Handbook of Automated
* Reasoning (vol. 2), by Gilles Dowek.
*
* The main difference between HigherOrderTrigger and Trigger is the function
* sendInstantiation(...). Recall that this function is called when its
- * underlying IMGenerator generates an InstMatch m using E-matching technique.
- * We enumerate additional instantiations based on m, when the domain of m
- * contains variables of function type.
+ * underlying IMGenerator generates a vectors of terms m using E-matching
+ * technique. We enumerate additional instantiations based on m, when the
+ * domain of m contains variables of function type.
*
* Examples below (f, x, y are universal variables):
*
* matching ground terms to function applications with variable heads.
* See examples (EX1)-(EX3) above.
*/
- bool sendInstantiation(InstMatch& m) override;
+ bool sendInstantiation(std::vector<Node>& m, InferenceId id) override;
private:
//-------------------- current information about the match
* when var_index = 0,1, we are processing possibilities for
* instantiation of f1,f2 respectively.
*/
- bool sendInstantiation(InstMatch& m, unsigned var_index);
+ 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(...).
* arg_changed is true, since we modified at least one previous
* argument of f1 or f2.
*/
- bool sendInstantiationArg(InstMatch& m,
+ bool sendInstantiationArg(std::vector<Node>& m,
unsigned var_index,
unsigned vnum,
unsigned arg_index,
{
}
-bool IMGenerator::sendInstantiation(Trigger* tparent, InstMatch& m)
+bool IMGenerator::sendInstantiation(Trigger* tparent,
+ InstMatch& m,
+ InferenceId id)
{
- return tparent->sendInstantiation(m);
+ return tparent->sendInstantiation(m, id);
}
InstMatchGenerator::InstMatchGenerator(
if (success)
{
Trace("matching-debug2") << "Continue next " << d_next << std::endl;
- ret_val = continueNextMatch(f, m, qe, tparent);
+ ret_val = continueNextMatch(
+ f, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING);
}
}
if (ret_val < 0)
int InstMatchGenerator::continueNextMatch(Node q,
InstMatch& m,
QuantifiersEngine* qe,
- Trigger* tparent)
+ Trigger* tparent,
+ InferenceId id)
{
if( d_next!=NULL ){
return d_next->getNextMatch(q, m, qe, tparent);
}
if (d_active_add)
{
- return sendInstantiation(tparent, m) ? 1 : -1;
+ return sendInstantiation(tparent, m, id) ? 1 : -1;
}
return 1;
}
while (getNextMatch(f, m, qe, tparent) > 0)
{
if( !d_active_add ){
- if (sendInstantiation(tparent, m))
+ if (sendInstantiation(tparent, m, InferenceId::UNKNOWN))
{
addedLemmas++;
if (d_qstate.isInConflict())
#include <map>
#include "expr/node_trie.h"
+#include "theory/inference_id.h"
#include "theory/quantifiers/inst_match.h"
namespace CVC4 {
* indicating that an instantiation was enqueued in the quantifier engine's
* lemma cache.
*/
- bool sendInstantiation(Trigger* tparent, InstMatch& m);
+ bool sendInstantiation(Trigger* tparent, InstMatch& m, InferenceId id);
/** The state of the quantifiers engine */
quantifiers::QuantifiersState& d_qstate;
/** The quantifiers inference manager */
int continueNextMatch(Node q,
InstMatch& m,
QuantifiersEngine* qe,
- Trigger* tparent);
+ Trigger* tparent,
+ InferenceId id);
/** Get inst match generator
*
* Gets the InstMatchGenerator that implements the
if (childIndex == endChildIndex)
{
// m is an instantiation
- if (sendInstantiation(tparent, m))
+ if (sendInstantiation(
+ tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
{
addedLemmas++;
Trace("multi-trigger-cache-debug")
<< "InstMatchGeneratorMultiLinear::getNextMatch : continue match "
<< std::endl;
Assert(d_next != nullptr);
- int ret_val = continueNextMatch(q, m, qe, tparent);
+ int ret_val = continueNextMatch(
+ q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
if (ret_val > 0)
{
Trace("multi-trigger-linear")
if (t.first != r)
{
InstMatch m(q);
- addInstantiations(m, qe, addedLemmas, 0, &(t.second));
+ addInstantiations(m, qe, addedLemmas, 0, &(t.second), tparent);
if (qs.isInConflict())
{
break;
if (tat && !qs.isInConflict())
{
InstMatch m(q);
- addInstantiations(m, qe, addedLemmas, 0, tat);
+ addInstantiations(m, qe, addedLemmas, 0, tat, tparent);
}
return addedLemmas;
}
QuantifiersEngine* qe,
uint64_t& addedLemmas,
size_t argIndex,
- TNodeTrie* tat)
+ TNodeTrie* tat,
+ Trigger* tparent)
{
Debug("simple-trigger-debug")
<< "Add inst " << argIndex << " " << d_match_pattern << std::endl;
}
// we do not need the trigger parent for simple triggers (no post-processing
// required)
- if (qe->getInstantiate()->addInstantiation(d_quant, m.d_vals))
+ if (sendInstantiation(
+ tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
{
addedLemmas++;
Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
if (prev.isNull() || prev == t)
{
m.setValue(v, t);
- addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
+ addInstantiations(
+ m, qe, addedLemmas, argIndex + 1, &(tt.second), tparent);
m.setValue(v, prev);
if (qs.isInConflict())
{
std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
if (it != tat->d_data.end())
{
- addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second));
+ addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second), tparent);
}
}
QuantifiersEngine* qe,
uint64_t& addedLemmas,
size_t argIndex,
- TNodeTrie* tat);
+ TNodeTrie* tat,
+ Trigger* tparent);
};
} // namespace inst
hasInst = numInst > 0 || hasInst;
Trace("process-trigger")
<< " Done, numInst = " << numInst << "." << std::endl;
- d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
- if (r == 1)
- {
- d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
- }
if (d_qstate.isInConflict())
{
break;
unsigned numInst = t->addInstantiations();
Trace("process-trigger")
<< " Done, numInst = " << numInst << "." << std::endl;
- d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
- if (t->isMultiTrigger())
- {
- d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
- }
if (d_qstate.isInConflict())
{
// we are already in conflict
return gtAddedLemmas + addedLemmas;
}
-bool Trigger::sendInstantiation(InstMatch& m)
+bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
{
- return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
+}
+
+bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)
+{
+ return sendInstantiation(m.d_vals, id);
}
bool Trigger::mkTriggerTerms(Node q,
#define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
#include "expr/node.h"
+#include "theory/inference_id.h"
namespace CVC4 {
namespace theory {
* but in some cases (e.g. higher-order) we may modify m before calling
* Instantiate::addInstantiation(...).
*/
- virtual bool sendInstantiation(InstMatch& m);
+ virtual bool sendInstantiation(std::vector<Node>& m, InferenceId id);
+ /** inst match version, calls the above method */
+ bool sendInstantiation(InstMatch& m, InferenceId id);
/**
* Ensure that all ground subterms of n have been preprocessed. This makes
* calls to the provided valuation to obtain the preprocessed form of these
}
else
{
- ret_val = continueNextMatch(q, m, qe, tparent);
+ ret_val = continueNextMatch(
+ q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
if (ret_val > 0)
{
return ret_val;
// just exhaustive instantiate
Node c = mkCondDefault(fmfmc, f);
d_quant_models[f].addEntry(fmfmc, c, d_false);
- if (!exhaustiveInstantiate(fmfmc, f, c, -1))
+ if (!exhaustiveInstantiate(fmfmc, f, c))
{
return 0;
}
// (should only add one instance)
Node c = mkCond(cond);
unsigned prevInst = d_addedLemmas;
- exhaustiveInstantiate(fmfmc, f, c, -1);
+ exhaustiveInstantiate(fmfmc, f, c);
if (d_addedLemmas == prevInst)
{
d_star_insts[f].push_back(i);
}
// just add the instance
d_triedLemmas++;
- if (instq->addInstantiation(f, inst, true))
+ if (instq->addInstantiation(
+ f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, true))
{
Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
d_addedLemmas++;
int j = d_star_insts[f][i];
if (temp.addEntry(fmfmc, mcond[j], d_quant_models[f].d_value[j]))
{
- if (!exhaustiveInstantiate(fmfmc, f, mcond[j], j))
+ if (!exhaustiveInstantiate(fmfmc, f, mcond[j]))
{
// something went wrong, resort to exhaustive instantiation
return 0;
FirstOrderModelFmc* d_fm;
};
-bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
- Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " ";
+bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm,
+ Node f,
+ Node c)
+{
+ Trace("fmc-exh") << "----Exhaustive instantiate based on " << c << " ";
debugPrintCond("fmc-exh", c, true);
Trace("fmc-exh")<< std::endl;
RepBoundFmcEntry rbfe(d_qe, c, fm);
if (ev!=d_true) {
Trace("fmc-exh-debug") << ", add!";
//add as instantiation
- if (d_qe->getInstantiate()->addInstantiation(f, inst, true))
+ if (d_qe->getInstantiate()->addInstantiation(
+ f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true))
{
Trace("fmc-exh-debug") << " ...success.";
addedLemmas++;
std::map<TypeNode, bool> d_preinitialized_types;
//--------------------end for preinitialization
Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
- bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
-private:
+ /**
+ * Exhaustively instantiate quantified formula q based on condition c, which
+ * indicate the domain to instantiate.
+ */
+ bool exhaustiveInstantiate(FirstOrderModelFmc* fm, Node q, Node c);
+
+ private:
void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );
void doNegate( Def & dc );
}
d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem;
d_addedLemmas += mb->getNumAddedLemmas()-prev_alem;
- d_quantEngine->d_statistics.d_instantiations_fmf_mbqi +=
- (mb->getNumAddedLemmas() - prev_alem);
}else{
if( Trace.isOn("fmf-exh-inst-debug") ){
Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
triedLemmas++;
//add as instantiation
- if (inst->addInstantiation(f, m.d_vals, true))
+ if (inst->addInstantiation(
+ f, m.d_vals, InferenceId::QUANTIFIERS_INST_FMF_EXH, true))
{
addedLemmas++;
if (d_qstate.isInConflict())
}
d_addedLemmas += addedLemmas;
d_triedLemmas += triedLemmas;
- d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas;
}
}else{
Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
// try instantiation
failMask.clear();
/* if (ie->addInstantiation(quantifier, terms)) */
- if (ie->addInstantiationExpFail(quantifier, terms, failMask, false))
+ if (ie->addInstantiationExpFail(
+ quantifier, terms, failMask, InferenceId::QUANTIFIERS_INST_ENUM))
{
Trace("inst-alg-rd") << "Success!" << std::endl;
- ++(d_quantEngine->d_statistics.d_instantiations_guess);
return true;
}
else
d_instRewrite.push_back(ir);
}
-bool Instantiate::addInstantiation(
- Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
+bool Instantiate::addInstantiation(Node q,
+ std::vector<Node>& terms,
+ InferenceId id,
+ bool mkRep,
+ bool modEq,
+ bool doVts)
{
// For resource-limiting (also does a time check).
d_qim.safePoint(ResourceManager::Resource::QuantifierStep);
if (hasProof)
{
// use proof generator
- addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, d_pfInst.get());
+ addedLem =
+ d_qim.addPendingLemma(lem, id, LemmaProperty::NONE, d_pfInst.get());
}
else
{
- addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
+ addedLem = d_qim.addPendingLemma(lem, id);
}
if (!addedLem)
bool Instantiate::addInstantiationExpFail(Node q,
std::vector<Node>& terms,
std::vector<bool>& failMask,
+ InferenceId id,
bool mkRep,
bool modEq,
bool doVts,
bool expFull)
{
- if (addInstantiation(q, terms, mkRep, modEq, doVts))
+ if (addInstantiation(q, terms, id, mkRep, modEq, doVts))
{
return true;
}
#include "context/cdhashset.h"
#include "expr/node.h"
#include "expr/proof.h"
+#include "theory/inference_id.h"
#include "theory/quantifiers/inst_match_trie.h"
#include "theory/quantifiers/quant_util.h"
#include "util/statistics_registry.h"
* This function returns true if the instantiation lemma for quantified
* formula q for the substitution specified by terms is successfully enqueued
* via a call to QuantifiersInferenceManager::addPendingLemma.
- * mkRep : whether to take the representatives of the terms in the range of
- * the substitution m,
- * modEq : whether to check for duplication modulo equality in instantiation
- * tries (for performance),
- * doVts : whether we must apply virtual term substitution to the
- * instantiation lemma.
+ * @param q the quantified formula to instantiate
+ * @param terms the terms to instantiate with
+ * @param id the identifier of the instantiation lemma sent via the inference
+ * manager
+ * @param mkRep whether to take the representatives of the terms in the
+ * range of the substitution m,
+ * @param modEq whether to check for duplication modulo equality in
+ * instantiation tries (for performance),
+ * @param doVts whether we must apply virtual term substitution to the
+ * instantiation lemma.
*
* This call may fail if it can be determined that the instantiation is not
* relevant or legal in the current context. This happens if:
*/
bool addInstantiation(Node q,
std::vector<Node>& terms,
+ InferenceId id,
bool mkRep = false,
bool modEq = false,
bool doVts = false);
bool addInstantiationExpFail(Node q,
std::vector<Node>& terms,
std::vector<bool>& failMask,
+ InferenceId id,
bool mkRep = false,
bool modEq = false,
bool doVts = false,
}
// Process the lemma: either add an instantiation or specific lemmas
// constructed during the isTConstraintSpurious call, or both.
- if (!qinst->addInstantiation(q, terms))
+ InferenceId id = (d_effort == EFFORT_CONFLICT
+ ? InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT
+ : InferenceId::QUANTIFIERS_INST_CBQI_PROP);
+ if (!qinst->addInstantiation(q, terms, id))
{
Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl;
// This should only happen if the algorithm generates the same
// ensure that quantified formulas that are more likely to have
// conflicting instances are checked earlier.
d_quantEngine->markRelevant(q);
- ++(d_quantEngine->d_statistics.d_instantiations_qcf);
if (options::qcfAllConflict())
{
isConflict = true;
else if (d_effort == EFFORT_PROP_EQ)
{
d_quantEngine->markRelevant(q);
- ++(d_quantEngine->d_statistics.d_instantiations_qcf);
}
}
// clean up assigned
if (mode == options::SygusInstMode::PRIORITY_INST)
{
- if (!inst->addInstantiation(q, terms))
+ if (!inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI))
{
sendEvalUnfoldLemmas(eval_unfold_lemmas);
}
{
if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
{
- inst->addInstantiation(q, terms);
+ inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
}
}
else
{
Assert(mode == options::SygusInstMode::INTERLEAVE);
- inst->addInstantiation(q, terms);
+ inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
sendEvalUnfoldLemmas(eval_unfold_lemmas);
}
}
for (const Node& lem : lemmas)
{
Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
- added_lemma |= d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
+ added_lemma |=
+ d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD);
}
return added_lemma;
}
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_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_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
- d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
- d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
- d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
- d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
- d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
- d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
- d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
- d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
- d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
- d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
+ d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
{
smtStatisticsRegistry()->registerStat(&d_time);
smtStatisticsRegistry()->registerStat(&d_qcf_time);
smtStatisticsRegistry()->registerStat(&d_triggers);
smtStatisticsRegistry()->registerStat(&d_simple_triggers);
smtStatisticsRegistry()->registerStat(&d_multi_triggers);
- smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
- smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
- smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
- smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
- smtStatisticsRegistry()->registerStat(&d_instantiations_qcf);
- smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop);
- smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh);
- smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi);
- smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi);
- smtStatisticsRegistry()->registerStat(&d_instantiations_rr);
}
QuantifiersEngine::Statistics::~Statistics(){
smtStatisticsRegistry()->unregisterStat(&d_triggers);
smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
- smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
}
Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
IntStat d_triggers;
IntStat d_simple_triggers;
IntStat d_multi_triggers;
- IntStat d_multi_trigger_instantiations;
IntStat d_red_alpha_equiv;
- IntStat d_instantiations_user_patterns;
- IntStat d_instantiations_auto_gen;
- IntStat d_instantiations_guess;
- IntStat d_instantiations_qcf;
- IntStat d_instantiations_qcf_prop;
- IntStat d_instantiations_fmf_exh;
- IntStat d_instantiations_fmf_mbqi;
- IntStat d_instantiations_cbqi;
- IntStat d_instantiations_rr;
Statistics();
~Statistics();
};/* class QuantifiersEngine::Statistics */
projects / cvc5.git / commitdiff