diff options
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp | 14 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_bv_instantiator.h | 28 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 73 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.h | 34 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 17 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 9 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 2 |
7 files changed, 100 insertions, 77 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index f94fee66b..472dabf68 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -633,7 +633,7 @@ struct SortBvExtractInterval }; 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; @@ -647,12 +647,8 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( // 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 @@ -721,10 +717,10 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( 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()); } } diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 3ad45d5be..6f6c216f6 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -168,32 +168,32 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess ~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 diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 186024219..95a4037fc 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -21,7 +21,6 @@ #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" @@ -1571,18 +1570,21 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) } } -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 @@ -1592,7 +1594,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st 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 " @@ -1600,28 +1602,43 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st << 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()) @@ -1673,8 +1690,10 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st // 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); } } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 7351e60f0..08f7a1262 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -224,21 +224,20 @@ class CegInstantiator { 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; } @@ -829,8 +828,9 @@ class InstantiatorPreprocess * 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) { } }; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 208eb0bf8..8693f97f4 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -593,15 +593,18 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) { 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); } } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2c27c6054..71c144daa 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1931,7 +1931,14 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // 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) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9c631ca60..233047321 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -890,8 +890,6 @@ public: 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 */ |