This PR removes a hack in counterexample-guided quantifier instantiation.
The issue is the CEGQI needs to know the form of certain lemmas, after theory preprocessing. CEGQI needs to know this since it must construct solutions (e.g. solved form of equalities) for free variables in these lemmas, which includes fresh variables in the lemma after postprocess like ITE skolems.
Previously, CEGQI was hacked so that it applied the preprocessing eagerly so that it had full knowledge of the postprocessed lemma. This PR updates CEGQI so that it uses the returned LemmaStatus as the way of getting the lemma after postprocess. It also fixes the lemma status returned by TheoryEngine so that all lemmas not just the "main lemma" are returned as a conjunction.
This PR is in preparation for major refactoring to theory preprocessing for the sake of proofs.
};
void BvInstantiatorPreprocess::registerCounterexampleLemma(
- std::vector<Node>& lems, std::vector<Node>& ce_vars)
+ Node lem, std::vector<Node>& ceVars, std::vector<Node>& auxLems)
{
// new variables
std::vector<Node> vars;
// map from terms to bitvector extracts applied to that term
std::map<Node, std::vector<Node> > extract_map;
std::unordered_set<TNode, TNodeHashFunction> visited;
- for (unsigned i = 0, size = lems.size(); i < size; i++)
- {
- Trace("cegqi-bv-pp-debug2")
- << "Register ce lemma # " << i << " : " << lems[i] << std::endl;
- collectExtracts(lems[i], extract_map, visited);
- }
+ Trace("cegqi-bv-pp-debug2") << "Register ce lemma " << lem << std::endl;
+ collectExtracts(lem, extract_map, visited);
for (std::pair<const Node, std::vector<Node> >& es : extract_map)
{
// sort based on the extract start position
Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..."
<< std::endl;
- lems.insert(lems.end(), new_lems.begin(), new_lems.end());
+ auxLems.insert(auxLems.end(), new_lems.begin(), new_lems.end());
Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..."
<< std::endl;
- ce_vars.insert(ce_vars.end(), vars.begin(), vars.end());
+ ceVars.insert(ceVars.end(), vars.begin(), vars.end());
}
}
~BvInstantiatorPreprocess() override {}
/** register counterexample lemma
*
- * This method modifies the contents of lems based on the extract terms
- * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces
+ * This method adds to auxLems based on the extract terms that lem
+ * contains when the option --cbqi-bv-rm-extract is enabled. It introduces
* a dummy equality so that segments of terms t under extracts can be solved
* independently.
*
- * For example:
+ * For example, if lem is:
* P[ ((extract 7 4) t), ((extract 3 0) t)]
- * becomes:
- * P[((extract 7 4) t), ((extract 3 0) t)] ^
+ * then we add:
* t = concat( x74, x30 )
- * where x74 and x30 are fresh variables of type BV_4.
+ * to auxLems, where x74 and x30 are fresh variables of type BV_4, which are
+ * added to ceVars.
*
- * Another example:
+ * Another example, for:
* P[ ((extract 7 3) t), ((extract 4 0) t)]
- * becomes:
- * P[((extract 7 4) t), ((extract 3 0) t)] ^
+ * we add:
* t = concat( x75, x44, x30 )
- * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4
- * respectively.
+ * to auxLems where x75, x44 and x30 are fresh variables of type BV_3, BV_1,
+ * and BV_4 respectively, which are added to ceVars.
*
- * Notice we leave the original conjecture alone. This is done for performance
+ * Notice we leave the original lem alone. This is done for performance
* since the added equalities ensure we are able to construct the proper
* solved forms for variables in t and for the intermediate variables above.
*/
- void registerCounterexampleLemma(std::vector<Node>& lems,
- std::vector<Node>& ce_vars) override;
+ void registerCounterexampleLemma(Node lem,
+ std::vector<Node>& ceVars,
+ std::vector<Node>& auxLems) override;
private:
/** collect extracts
#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
-#include "smt/term_formula_removal.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
#include "theory/quantifiers/first_order_model.h"
}
}
-void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
+void CegInstantiator::registerCounterexampleLemma(Node lem,
+ std::vector<Node>& ceVars,
+ std::vector<Node>& auxLems)
+{
Trace("cegqi-reg") << "Register counterexample lemma..." << std::endl;
d_input_vars.clear();
- d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end());
+ d_input_vars.insert(d_input_vars.end(), ceVars.begin(), ceVars.end());
//Assert( d_vars.empty() );
d_vars.clear();
registerTheoryId(THEORY_UF);
- for (unsigned i = 0; i < ce_vars.size(); i++)
+ for (const Node& cv : ceVars)
{
- Trace("cegqi-reg") << " register input variable : " << ce_vars[i] << std::endl;
- registerVariable(ce_vars[i]);
+ Trace("cegqi-reg") << " register input variable : " << cv << std::endl;
+ registerVariable(cv);
}
// preprocess with all relevant instantiator preprocessors
pvars.insert(pvars.end(), d_vars.begin(), d_vars.end());
for (std::pair<const TheoryId, InstantiatorPreprocess*>& p : d_tipp)
{
- p.second->registerCounterexampleLemma(lems, pvars);
+ p.second->registerCounterexampleLemma(lem, pvars, auxLems);
}
// must register variables generated by preprocessors
Trace("cegqi-debug") << "Register variables from theory-specific methods "
<< std::endl;
for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i)
{
- Trace("cegqi-reg") << " register theory preprocess variable : " << pvars[i]
- << std::endl;
+ Trace("cegqi-reg") << " register inst preprocess variable : " << pvars[i]
+ << std::endl;
registerVariable(pvars[i]);
}
- //remove ITEs
- IteSkolemMap iteSkolemMap;
- d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
- for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
- Trace("cegqi-reg") << " register aux variable : " << i->first << std::endl;
- registerVariable(i->first);
- }
- for( unsigned i=0; i<lems.size(); i++ ){
- Trace("cegqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl;
- Node rlem = lems[i];
- rlem = Rewriter::rewrite( rlem );
- // also must preprocess to ensure that the counterexample atoms we
- // collect below are identical to the atoms that we add to the CNF stream
- rlem = d_qe->getTheoryEngine()->preprocess(rlem);
- Trace("cegqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
- lems[i] = rlem;
+ // register variables that were introduced during TheoryEngine preprocessing
+ std::unordered_set<Node, NodeHashFunction> ceSyms;
+ expr::getSymbols(lem, ceSyms);
+ std::unordered_set<Node, NodeHashFunction> qSyms;
+ expr::getSymbols(d_quant, qSyms);
+ // all variables that are in counterexample lemma but not in quantified
+ // formula
+ for (const Node& ces : ceSyms)
+ {
+ if (qSyms.find(ces) != qSyms.end())
+ {
+ // a free symbol of the quantified formula.
+ continue;
+ }
+ if (std::find(d_vars.begin(), d_vars.end(), ces) != d_vars.end())
+ {
+ // already processed variable
+ continue;
+ }
+ if (ces.getType().isBoolean())
+ {
+ // Boolean variables, including the counterexample literal, don't matter
+ // since they are always assigned a model value.
+ continue;
+ }
+ Trace("cegqi-reg") << " register theory preprocess variable : " << ces
+ << std::endl;
+ // register the variable, which was introduced by TheoryEngine's preprocess
+ // method, e.g. an ITE skolem.
+ registerVariable(ces);
}
+
// determine variable order: must do Reals before Ints
Trace("cegqi-debug") << "Determine variable order..." << std::endl;
if (!d_vars.empty())
// the original body
d_is_nested_quant = false;
std::map< Node, bool > visited;
- for( unsigned i=0; i<lems.size(); i++ ){
- collectCeAtoms( lems[i], visited );
+ collectCeAtoms(lem, visited);
+ for (const Node& alem : auxLems)
+ {
+ collectCeAtoms(alem, visited);
}
}
void presolve(Node q);
/** Register the counterexample lemma
*
- * lems : contains the conjuncts of the counterexample lemma of the
- * quantified formula we are processing. The counterexample
- * lemma is the formula { ~phi[e/x] } in Figure 1 of Reynolds
- * et al. FMSD 2017.
- * ce_vars : contains the variables e. Notice these are variables of
- * INST_CONSTANT kind, since we do not permit bound
- * variables in assertions.
- *
- * This method may modify the set of lemmas lems based on:
- * - ITE removal,
- * - Theory-specific preprocessing of instantiation lemmas.
- * It may also introduce new variables to ce_vars if necessary.
- */
- void registerCounterexampleLemma(std::vector<Node>& lems,
- std::vector<Node>& ce_vars);
+ * @param lem contains the counterexample lemma of the quantified formula we
+ * are processing. The counterexample lemma is the formula { ~phi[e/x] } in
+ * Figure 1 of Reynolds et al. FMSD 2017.
+ * @param ce_vars contains the variables e. Notice these are variables of
+ * INST_CONSTANT kind, since we do not permit bound variables in assertions.
+ * This method may add additional variables to this vector if it decides there
+ * are additional auxiliary variables to solve for.
+ * @param auxLems : if this method decides that additional lemmas should be
+ * sent on the output channel, they are added to this vector, and sent out by
+ * the caller of this method.
+ */
+ void registerCounterexampleLemma(Node lem,
+ std::vector<Node>& ce_vars,
+ std::vector<Node>& auxLems);
//------------------------------interface for instantiators
/** get quantifiers engine */
QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
* of counterexample lemmas, with the same contract as
* CegInstantiation::registerCounterexampleLemma.
*/
- virtual void registerCounterexampleLemma(std::vector<Node>& lems,
- std::vector<Node>& ce_vars)
+ virtual void registerCounterexampleLemma(Node lem,
+ std::vector<Node>& ceVars,
+ std::vector<Node>& auxLems)
{
}
};
{
ce_vars.push_back(tutil->getInstantiationConstant(q, i));
}
- std::vector<Node> lems;
- lems.push_back(lem);
CegInstantiator* cinst = getInstantiator(q);
- cinst->registerCounterexampleLemma(lems, ce_vars);
- for (unsigned i = 0, size = lems.size(); i < size; i++)
+ LemmaStatus status = d_quantEngine->getOutputChannel().lemma(lem);
+ Node ppLem = status.getRewrittenLemma();
+ Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
+ << std::endl;
+ std::vector<Node> auxLems;
+ cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems);
+ for (unsigned i = 0, size = auxLems.size(); i < size; i++)
{
- Trace("cegqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
- << std::endl;
- d_quantEngine->addLemma(lems[i], false);
+ Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
+ << std::endl;
+ d_quantEngine->addLemma(auxLems[i], false);
}
}
// Lemma analysis isn't online yet; this lemma may only live for this
// user level.
- return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel());
+ Node retLemma = additionalLemmas[0];
+ if (additionalLemmas.size() > 1)
+ {
+ // the returned lemma is the conjunction of all additional lemmas.
+ retLemma =
+ NodeManager::currentNM()->mkNode(kind::AND, additionalLemmas.ref());
+ }
+ return theory::LemmaStatus(retLemma, d_userContext->getLevel());
}
void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
- RemoveTermFormulas* getTermFormulaRemover() { return &d_tform_remover; }
-
SortInference* getSortInference() { return &d_sortInfer; }
/** Prints the assertions to the debug stream */
projects / cvc5.git / commitdiff