This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation.
The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly.
Fixes #5365, fixes #5279, fixes #4849, fixes #4433.
This PR also required fixes related to how quantifier elimination is computed.
#include "smt/quant_elim_solver.h"
+#include "expr/subs.h"
#include "smt/smt_solver.h"
#include "theory/quantifiers/extended_rewrite.h"
#include "theory/rewriter.h"
Node q,
bool doFull)
{
- Trace("smt-qe") << "Do quantifier elimination " << q << std::endl;
+ Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl;
if (q.getKind() != EXISTS && q.getKind() != FORALL)
{
throw ModalException(
// failed, return original
return q;
}
+ // must use original quantified formula to compute QE, which ensures that
+ // e.g. term formula removal is not run on the body. Notice that we assume
+ // that the (single) quantified formula is preprocessed, rewritten
+ // version of the input quantified formula q.
std::vector<Node> inst_qs;
te->getInstantiatedQuantifiedFormulas(inst_qs);
Assert(inst_qs.size() <= 1);
{
Node topq = inst_qs[0];
Assert(topq.getKind() == FORALL);
- Trace("smt-qe") << "Get qe for " << topq << std::endl;
- ret = te->getInstantiatedConjunction(topq);
- Trace("smt-qe") << "Returned : " << ret << std::endl;
+ Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
+ << topq << std::endl;
+ std::vector<std::vector<Node>> insts;
+ te->getInstantiationTermVectors(topq, insts);
+ std::vector<Node> vars(ne[0].begin(), ne[0].end());
+ std::vector<Node> conjs;
+ // apply the instantiation on the original body
+ for (const std::vector<Node>& inst : insts)
+ {
+ // note we do not convert to witness form here, since we could be
+ // an internal subsolver
+ Subs s;
+ s.add(vars, inst);
+ Node c = s.apply(ne[1].negate());
+ conjs.push_back(c);
+ }
+ ret = nm->mkAnd(conjs);
+ Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl;
if (q.getKind() == EXISTS)
{
ret = Rewriter::rewrite(ret.negate());
options::cegqi.set(false);
}
// Do we need to track instantiations?
- // Needed for sygus due to single invocation techniques.
- if (options::cegqiNestedQE()
- || (options::unsatCores() && !options::trackInstLemmas.wasSetByUser())
- || is_sygus)
+ if (options::unsatCores() && !options::trackInstLemmas.wasSetByUser())
{
options::trackInstLemmas.set(true);
}
// only supported in pure arithmetic or pure BV
options::cegqiNestedQE.set(false);
}
- // prenexing
- if (options::cegqiNestedQE())
- {
- // only complete with prenex = normal
- options::prenexQuant.set(options::PrenexQuantMode::NORMAL);
- }
- else if (options::globalNegate())
+ if (options::globalNegate())
{
if (!options::prenexQuant.wasSetByUser())
{
te->getInstantiatedQuantifiedFormulas(qs);
}
-void SmtEngine::getInstantiations(Node q, std::vector<Node>& insts)
-{
- SmtScope smts(this);
- TheoryEngine* te = getTheoryEngine();
- Assert(te != nullptr);
- te->getInstantiations(q, insts);
-}
-
void SmtEngine::getInstantiationTermVectors(
Node q, std::vector<std::vector<Node>>& tvecs)
{
*/
void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
- /**
- * Get instantiations for quantified formula q.
- *
- * If q was a quantified formula that was instantiated on the last call to
- * check-sat (i.e. q is returned as part of the vector in the method
- * getInstantiatedQuantifiedFormulas above), then the list of instantiations
- * of that formula that were generated are added to insts.
- *
- * In particular, if q is of the form forall x. P(x), then insts is a list
- * of formulas of the form P(t1), ..., P(tn).
- */
- void getInstantiations(Node q, std::vector<Node>& insts);
/**
* Get instantiation term vectors for quantified formula q.
*
&& (vinst->useModelValue(this, sf, pv, d_effort) || is_sv)
&& vinst->allowModelValue(this, sf, pv, d_effort))
{
-#ifdef CVC4_ASSERTIONS
- // the instantiation strategy for quantified linear integer/real
- // arithmetic with arbitrary quantifier nesting is "monotonic" as a
- // consequence of Lemmas 5, 9 and Theorem 4 of Reynolds et al, "Solving
- // Quantified Linear Arithmetic by Counterexample Guided Instantiation",
- // FMSD 2017. We throw an assertion failure if we detect a case where the
- // strategy was not monotonic.
- if (options::cegqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH)
- && d_qe->getLogicInfo().isLinear())
- {
- Trace("cegqi-warn") << "Had to resort to model value." << std::endl;
- Assert(false);
- }
-#endif
Node mv = getModelValue( pv );
TermProperties pv_prop_m;
Trace("cegqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
d_cbqi_set_quant_inactive(false),
d_incomplete_check(false),
d_added_cbqi_lemma(qe->getUserContext()),
- d_elim_quants(qe->getSatContext()),
d_vtsCache(new VtsTermCache(qe)),
- d_bv_invert(nullptr),
- d_nested_qe_waitlist_size(qe->getUserContext()),
- d_nested_qe_waitlist_proc(qe->getUserContext())
+ d_bv_invert(nullptr)
{
- d_qid_count = 0;
d_small_const =
NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
d_check_vts_lemma_lc = false;
if (options::cegqiBv())
{
// if doing instantiation for BV, need the inverter class
- d_bv_invert.reset(new quantifiers::BvInverter);
+ d_bv_invert.reset(new BvInverter);
+ }
+ if (options::cegqiNestedQE())
+ {
+ d_nestedQe.reset(new NestedQe(qe->getUserContext()));
}
}
if( doCbqi( quants[i] ) ){
registerCbqiLemma( quants[i] );
}
- if( options::cegqiNestedQE() ){
- //record these as counterexample quantifiers
- QAttributes qa;
- QuantAttributes::computeQuantAttributes( quants[i], qa );
- if( !qa.d_qid_num.isNull() ){
- d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
- d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
- Trace("cegqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
- }
- }
}
}
// The decision strategy for this quantified formula ensures that its
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
if( doCbqi( q ) ){
- Assert(hasAddedCbqiLemma(q));
if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
d_active_quant[q] = true;
Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
d_quantEngine->getModel()->setQuantifierActive( q, false );
d_cbqi_set_quant_inactive = true;
d_active_quant.erase( q );
- d_elim_quants.insert( q );
- Trace("cegqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
- //process from waitlist
- while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
- int index = d_nested_qe_waitlist_proc[q];
- Assert(index >= 0);
- Assert(index < (int)d_nested_qe_waitlist[q].size());
- Node nq = d_nested_qe_waitlist[q][index];
- Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
- Node dqelem = nq.eqNode( nqeqn );
- Trace("cegqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
- d_quantEngine->getOutputChannel().lemma( dqelem );
- d_nested_qe_waitlist_proc[q] = index + 1;
- }
}
}
}else{
for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
Node q = it->first;
Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
- if( d_nested_qe.find( q )==d_nested_qe.end() ){
- process( q, e, ee );
- if( d_quantEngine->inConflict() ){
- break;
- }
- }else{
- Trace("cegqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
- Assert(false);
+ process(q, e, ee);
+ if (d_quantEngine->inConflict())
+ {
+ break;
}
}
if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
}
}
-Node InstStrategyCegqi::getIdMarkedQuantNode(Node n,
- std::map<Node, Node>& visited)
-{
- std::map< Node, Node >::iterator it = visited.find( n );
- if( it==visited.end() ){
- Node ret = n;
- if( n.getKind()==FORALL ){
- QAttributes qa;
- QuantAttributes::computeQuantAttributes( n, qa );
- if( qa.d_qid_num.isNull() ){
- std::vector< Node > rc;
- rc.push_back( n[0] );
- rc.push_back( getIdMarkedQuantNode( n[1], visited ) );
- Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
- QuantIdNumAttribute ida;
- avar.setAttribute(ida,d_qid_count);
- d_qid_count++;
- std::vector< Node > iplc;
- iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
- if( n.getNumChildren()==3 ){
- for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
- iplc.push_back( n[2][i] );
- }
- }
- rc.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
- ret = NodeManager::currentNM()->mkNode( FORALL, rc );
- }
- }else if( n.getNumChildren()>0 ){
- std::vector< Node > children;
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- bool childChanged = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node nc = getIdMarkedQuantNode( n[i], visited );
- childChanged = childChanged || nc!=n[i];
- children.push_back( nc );
- }
- if( childChanged ){
- ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
- }
- visited[n] = ret;
- return ret;
- }else{
- return it->second;
- }
-}
-
void InstStrategyCegqi::checkOwnership(Node q)
{
if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
void InstStrategyCegqi::preRegisterQuantifier(Node q)
{
- // mark all nested quantifiers with id
- if (options::cegqiNestedQE())
+ if (doCbqi(q))
{
- if( d_quantEngine->getOwner(q)==this )
+ if (processNestedQe(q, true))
{
- std::map<Node, Node> visited;
- Node mq = getIdMarkedQuantNode(q[1], visited);
- if (mq != q[1])
- {
- // do not do cbqi, we are reducing this quantified formula to a marked
- // one
- d_do_cbqi[q] = CEG_UNHANDLED;
- // instead do reduction
- std::vector<Node> qqc;
- qqc.push_back(q[0]);
- qqc.push_back(mq);
- if (q.getNumChildren() == 3)
- {
- qqc.push_back(q[2]);
- }
- Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc);
- Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq);
- Trace("cegqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
- d_quantEngine->addLemma(mlem);
- }
+ // will process using nested quantifier elimination
+ return;
}
- }
- if( doCbqi( q ) ){
// get the instantiator
if (options::cegqiPreRegInst())
{
inst = d_vtsCache->rewriteVtsSymbols(inst);
Trace("quant-vts-debug") << "...got " << inst << std::endl;
}
- if (options::cegqiNestedQE())
- {
- inst = doNestedQE(q, terms, inst, doVts);
- }
if (prevInst != inst)
{
// not proof producing yet
return d_irew.get();
}
-Node InstStrategyCegqi::doNestedQENode(
- Node q, Node ceq, Node n, std::vector<Node>& inst_terms, bool doVts)
-{
- // there is a nested quantified formula (forall y. nq[y,x]) such that
- // q is (forall y. nq[y,t]) for ground terms t,
- // ceq is (forall y. nq[y,e]) for CE variables e.
- // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e].
- // in this case, q is equivalent to the quantifier-free formula C[t].
- if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
- d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
- Trace("cegqi-nqe") << "CE quantifier elimination : " << std::endl;
- Trace("cegqi-nqe") << " " << ceq << std::endl;
- Trace("cegqi-nqe") << " " << d_nested_qe[ceq] << std::endl;
- //should not contain quantifiers
- Assert(!expr::hasClosure(d_nested_qe[ceq]));
- }
- Assert(d_quantEngine->getTermUtil()->d_inst_constants[q].size()
- == inst_terms.size());
- //replace inst constants with instantiation
- Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(),
- d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
- inst_terms.begin(), inst_terms.end() );
- if( doVts ){
- //do virtual term substitution
- ret = Rewriter::rewrite( ret );
- ret = d_vtsCache->rewriteVtsSymbols(ret);
- }
- Trace("cegqi-nqe") << "Nested quantifier elimination: " << std::endl;
- Trace("cegqi-nqe") << " " << n << std::endl;
- Trace("cegqi-nqe") << " " << ret << std::endl;
- return ret;
-}
-
-Node InstStrategyCegqi::doNestedQERec(Node q,
- Node n,
- std::map<Node, Node>& visited,
- std::vector<Node>& inst_terms,
- bool doVts)
-{
- if( visited.find( n )==visited.end() ){
- Node ret = n;
- if( n.getKind()==FORALL ){
- QAttributes qa;
- QuantAttributes::computeQuantAttributes( n, qa );
- if( !qa.d_qid_num.isNull() ){
- //if it has an id, check whether we have done quantifier elimination for this id
- std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
- if( it!=d_id_to_ce_quant.end() ){
- Node ceq = it->second;
- bool doNestedQe = d_elim_quants.contains( ceq );
- if( doNestedQe ){
- ret = doNestedQENode( q, ceq, n, inst_terms, doVts );
- }else{
- Trace("cegqi-nqe") << "Add to nested qe waitlist : " << std::endl;
- Node nr = Rewriter::rewrite( n );
- Trace("cegqi-nqe") << " " << ceq << std::endl;
- Trace("cegqi-nqe") << " " << nr << std::endl;
- int wlsize = d_nested_qe_waitlist_size[ceq] + 1;
- d_nested_qe_waitlist_size[ceq] = wlsize;
- if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){
- d_nested_qe_waitlist[ceq][wlsize] = nr;
- }else{
- d_nested_qe_waitlist[ceq].push_back( nr );
- }
- d_nested_qe_info[nr].d_q = q;
- d_nested_qe_info[nr].d_inst_terms.clear();
- d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
- d_nested_qe_info[nr].d_doVts = doVts;
- //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
- Assert(!options::cegqiInnermost());
- }
- }
- }
- }else if( n.getNumChildren()>0 ){
- std::vector< Node > children;
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- bool childChanged = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node nc = doNestedQERec( q, n[i], visited, inst_terms, doVts );
- childChanged = childChanged || nc!=n[i];
- children.push_back( nc );
- }
- if( childChanged ){
- ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
- }
- visited[n] = ret;
- return ret;
- }else{
- return n;
- }
-}
-
-Node InstStrategyCegqi::doNestedQE(Node q,
- std::vector<Node>& inst_terms,
- Node lem,
- bool doVts)
-{
- std::map< Node, Node > visited;
- return doNestedQERec( q, lem, visited, inst_terms, doVts );
-}
-
void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
{
// must register with the instantiator
}
void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
+ // If we are doing nested quantifier elimination, check if q was already
+ // processed.
+ if (processNestedQe(q, false))
+ {
+ // don't need to process this, since it has been reduced
+ return;
+ }
if( e==0 ){
CegInstantiator * cinst = getInstantiator( q );
Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
}
}
+bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
+{
+ if (d_nestedQe != nullptr)
+ {
+ if (isPreregister)
+ {
+ // If at preregister, we are done if we have nested quantification.
+ // We will process nested quantification.
+ return NestedQe::hasNestedQuantification(q);
+ }
+ // if not a preregister, we process, which may trigger quantifier
+ // elimination in subsolvers.
+ std::vector<Node> lems;
+ if (d_nestedQe->process(q, lems))
+ {
+ // add lemmas to process
+ for (const Node& lem : lems)
+ {
+ d_quantEngine->addLemma(lem);
+ }
+ // don't need to process this, since it has been reduced
+ return true;
+ }
+ }
+ return false;
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
#include "theory/decision_manager.h"
#include "theory/quantifiers/bv_inverter.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/cegqi/nested_qe.h"
#include "theory/quantifiers/cegqi/vts_term_cache.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_util.h"
bool d_incomplete_check;
/** whether we have added cbqi lemma */
NodeSet d_added_cbqi_lemma;
- /** whether we have added cbqi lemma */
- NodeSet d_elim_quants;
/** parent guards */
std::map< Node, std::vector< Node > > d_parent_quant;
std::map< Node, std::vector< Node > > d_children_quant;
void registerCounterexampleLemma(Node q, Node lem);
/** has added cbqi lemma */
bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
+ /**
+ * Return true if q can be processed with nested quantifier elimination.
+ * This may add a lemma on the output channel of quantifiers engine if so.
+ *
+ * @param q The quantified formula to process
+ * @param isPreregister Whether this method is being called at preregister.
+ */
+ bool processNestedQe(Node q, bool isPreregister);
/** process functions */
void process(Node q, Theory::Effort effort, int e);
/**
Node getCounterexampleLiteral(Node q);
/** map from universal quantifiers to their counterexample literals */
std::map<Node, Node> d_ce_lit;
-
- //for identification
- uint64_t d_qid_count;
- //nested qe map
- std::map< Node, Node > d_nested_qe;
- //mark ids on quantifiers
- Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited );
- // id to ce quant
- std::map< Node, Node > d_id_to_ce_quant;
- std::map< Node, Node > d_ce_quant_to_id;
- //do nested quantifier elimination recursive
- Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts );
- Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts );
- //elimination information (for delayed elimination)
- class NestedQEInfo {
- public:
- NestedQEInfo() : d_doVts(false){}
- ~NestedQEInfo(){}
- Node d_q;
- std::vector< Node > d_inst_terms;
- bool d_doVts;
- };
- std::map< Node, NestedQEInfo > d_nested_qe_info;
- NodeIntMap d_nested_qe_waitlist_size;
- NodeIntMap d_nested_qe_waitlist_proc;
- std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
-
- /** Do nested quantifier elimination.
- *
- * This rewrites the quantified formulas in inst based on nested quantifier
- * elimination. In this method, inst is the instantiation of quantified
- * formula q for the vector terms. The flag doVts indicates whether we must
- * apply virtual term substitution (if terms contains virtual terms).
- */
- Node doNestedQE(Node q, std::vector<Node>& terms, Node inst, bool doVts);
+ /** The nested quantifier elimination utility */
+ std::unique_ptr<NestedQe> d_nestedQe;
};
-
}
}
}
}
}
+void InstMatchTrie::getInstantiations(
+ Node q, std::vector<std::vector<Node>>& insts) const
+{
+ std::vector<Node> terms;
+ getInstantiations(q, insts, terms);
+}
+
+void InstMatchTrie::getInstantiations(Node q,
+ std::vector<std::vector<Node>>& insts,
+ std::vector<Node>& terms) const
+{
+ if (terms.size() == q[0].getNumChildren())
+ {
+ insts.push_back(terms);
+ }
+ else
+ {
+ for (const std::pair<const Node, InstMatchTrie>& d : d_data)
+ {
+ terms.push_back(d.first);
+ d.second.getInstantiations(q, insts, terms);
+ terms.pop_back();
+ }
+ }
+}
+
CDInstMatchTrie::~CDInstMatchTrie()
{
for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
}
}
+void CDInstMatchTrie::getInstantiations(
+ Node q, std::vector<std::vector<Node>>& insts) const
+{
+ std::vector<Node> terms;
+ getInstantiations(q, insts, terms);
+}
+
+void CDInstMatchTrie::getInstantiations(Node q,
+ std::vector<std::vector<Node>>& insts,
+ std::vector<Node>& terms) const
+{
+ if (!d_valid.get())
+ {
+ // do nothing
+ }
+ else if (terms.size() == q[0].getNumChildren())
+ {
+ insts.push_back(terms);
+ }
+ else
+ {
+ for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+ {
+ terms.push_back(d.first);
+ d.second->getInstantiations(q, insts, terms);
+ terms.pop_back();
+ }
+ }
+}
+
} /* CVC4::theory::inst namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
Node lem,
ImtIndexOrder* imtio = NULL,
unsigned index = 0);
+ /**
+ * Adds the instantiations for q into insts.
+ */
+ void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
/** get instantiations
*
std::map<Node, InstMatchTrie> d_data;
private:
+ /** Helper for getInstantiations.*/
+ void getInstantiations(Node q,
+ std::vector<std::vector<Node>>& insts,
+ std::vector<Node>& terms) const;
/** helper for print
* terms accumulates the path we are on in the trie.
*/
std::vector<Node>& m,
Node lem,
unsigned index = 0);
+ /**
+ * Adds the instantiations for q into insts.
+ */
+ void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
/** get instantiations
*
}
private:
+ /** Helper for getInstantiations.*/
+ void getInstantiations(Node q,
+ std::vector<std::vector<Node>>& insts,
+ std::vector<Node>& terms) const;
/** the data */
std::map<Node, CDInstMatchTrie*> d_data;
/** is valid */
void Instantiate::getInstantiationTermVectors(
Node q, std::vector<std::vector<Node> >& tvecs)
{
- std::vector<Node> lemmas;
- getInstantiations(q, lemmas);
- std::map<Node, Node> quant;
- std::map<Node, std::vector<Node> > tvec;
- getExplanationForInstLemmas(lemmas, quant, tvec);
- for (std::pair<const Node, std::vector<Node> >& t : tvec)
+ // if track instantiations is true, we use the instantiation + explanation
+ // methods for doing minimization based on unsat cores.
+ if (options::trackInstLemmas())
+ {
+ std::vector<Node> lemmas;
+ getInstantiations(q, lemmas);
+ std::map<Node, Node> quant;
+ std::map<Node, std::vector<Node> > tvec;
+ getExplanationForInstLemmas(lemmas, quant, tvec);
+ for (std::pair<const Node, std::vector<Node> >& t : tvec)
+ {
+ tvecs.push_back(t.second);
+ }
+ return;
+ }
+
+ if (options::incrementalSolving())
+ {
+ std::map<Node, inst::CDInstMatchTrie*>::const_iterator it =
+ d_c_inst_match_trie.find(q);
+ if (it != d_c_inst_match_trie.end())
+ {
+ it->second->getInstantiations(q, tvecs);
+ }
+ }
+ else
{
- tvecs.push_back(t.second);
+ std::map<Node, inst::InstMatchTrie>::const_iterator it =
+ d_inst_match_trie.find(q);
+ if (it != d_inst_match_trie.end())
+ {
+ it->second.getInstantiations(q, tvecs);
+ }
}
}
{
if (options::incrementalSolving())
{
- for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+ for (const auto& t : d_c_inst_match_trie)
{
getInstantiationTermVectors(t.first, insts[t.first]);
}
}
else
{
- for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+ for (const auto& t : d_inst_match_trie)
{
getInstantiationTermVectors(t.first, insts[t.first]);
}
Node body = siq[1];
for (unsigned i = 0, ninsts = d_inst.size(); i < ninsts; i++)
{
+ // note we do not convert to witness form here, since we could be
+ // an internal subsolver
std::vector<Node>& inst = d_inst[i];
Trace("sygus-si") << " Instantiation: " << inst << std::endl;
// instantiation should have same arity since we are not allowed to
}
}
-bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
- return d_instantiate->getUnsatCoreLemmas(active_lemmas);
-}
-
void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
d_instantiate->getInstantiationTermVectors(q, tvecs);
}
d_instantiate->getInstantiationTermVectors(insts);
}
-void QuantifiersEngine::getExplanationForInstLemmas(
- const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec)
-{
- d_instantiate->getExplanationForInstLemmas(lems, quant, tvec);
-}
-
void QuantifiersEngine::printInstantiations( std::ostream& out ) {
bool printed = false;
// print the skolemizations
d_instantiate->getInstantiatedQuantifiedFormulas(qs);
}
-void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
- d_instantiate->getInstantiations(insts);
-}
-
-void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
- d_instantiate->getInstantiations(q, insts);
-}
-
-Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
- return d_instantiate->getInstantiatedConjunction(q);
-}
-
QuantifiersEngine::Statistics::Statistics()
: d_time("theory::QuantifiersEngine::time"),
d_qcf_time("theory::QuantifiersEngine::time_qcf"),
void printSynthSolution(std::ostream& out);
/** get list of quantified formulas that were instantiated */
void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
- /** get instantiations */
- void getInstantiations(Node q, std::vector<Node>& insts);
- void getInstantiations(std::map<Node, std::vector<Node> >& insts);
/** get instantiation term vectors */
void getInstantiationTermVectors(Node q,
std::vector<std::vector<Node> >& tvecs);
void getInstantiationTermVectors(
std::map<Node, std::vector<std::vector<Node> > >& insts);
- /** get instantiated conjunction */
- Node getInstantiatedConjunction(Node q);
- /** get unsat core lemmas */
- bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
- /** get explanation for instantiation lemmas */
- void getExplanationForInstLemmas(const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec);
/** get synth solutions
*
}
}
-void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiations( q, insts );
- }else{
- Assert(false);
- }
-}
-
void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
if( d_quantEngine ){
d_quantEngine->getInstantiationTermVectors( q, tvecs );
}
}
-void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiations( insts );
- }else{
- Assert(false);
- }
-}
-
void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
if( d_quantEngine ){
d_quantEngine->getInstantiationTermVectors( insts );
}
}
-Node TheoryEngine::getInstantiatedConjunction( Node q ) {
- if( d_quantEngine ){
- return d_quantEngine->getInstantiatedConjunction( q );
- }else{
- Assert(false);
- return Node::null();
- }
-}
-
TrustNode TheoryEngine::getExplanation(TNode node)
{
Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
/**
* Get instantiation methods
- * first inputs forall x.q[x] and returns ( q[a], ..., q[z] )
- * second inputs forall x.q[x] and returns ( a, ..., z )
- * third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] )
+ * the first given forall x.q[x] returns ( a, ..., z )
+ * the second returns mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] )
* , ... , forall x.qn[x] -> ( qn[a]...qn[z] )
*/
- void getInstantiations( Node q, std::vector< Node >& insts );
void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
- void getInstantiations( std::map< Node, std::vector< Node > >& insts );
void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
- /**
- * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q.
- * Can be used for quantifier elimination when satisfiable and q[t1] ^ ... ^ q[tn] |= q
- */
- Node getInstantiatedConjunction( Node q );
-
/**
* Forwards an entailment check according to the given theoryOfMode.
* See theory.h for documentation on entailmentCheck().
regress1/quantifiers/issue4062-cegqi-aux.smt2
regress1/quantifiers/issue4243-prereg-inc.smt2
regress1/quantifiers/issue4290-cegqi-r.smt2
+ regress1/quantifiers/issue4433-nqe.smt2
regress1/quantifiers/issue4620-erq-witness-unsound.smt2
regress1/quantifiers/issue4685-wrewrite.smt2
+ regress1/quantifiers/issue4849-nqe.smt2
regress1/quantifiers/issue5019-cegqi-i.smt2
+ regress1/quantifiers/issue5279-nqe.smt2
+ regress1/quantifiers/issue5365-nqe.smt2
regress1/quantifiers/issue5469-aext.smt2
regress1/quantifiers/issue5470-aext.smt2
regress1/quantifiers/issue5471-aext.smt2
--- /dev/null
+(set-logic LIA)
+(set-option :cegqi-nested-qe true)
+(set-info :status unsat)
+(assert
+ (forall ((a Int) (b Int))
+ (xor (xor (= a 0) (= b 0))
+ (forall ((c Int))
+ (= (ite (= a 0) 0 1) (ite (= c 0) 0 1))))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --cegqi-nested-qe -q
+; EXPECT: sat
+(set-logic LIA)
+(set-option :cegqi-nested-qe true)
+(set-info :status sat)
+(assert (forall ((a Int)) (exists ((b Int)) (= (ite (= a 0) 0 1) (ite (= b 0) 0 1)))))
+(check-sat)
--- /dev/null
+(set-logic LIA)
+(set-option :cegqi-nested-qe true)
+(set-info :status unsat)
+(assert (forall ((a Int) (b Bool)) (= a (ite b 0 1))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --cegqi-nested-qe -q
+; EXPECT: sat
+(set-logic BV)
+(set-option :cegqi-nested-qe true)
+(set-info :status sat)
+(assert
+ (exists ((a (_ BitVec 32)))
+ (forall ((b (_ BitVec 32)) (c (_ BitVec 32)))
+ (exists ((d (_ BitVec 32)) (e (_ BitVec 32)))
+ (forall ((g (_ BitVec 32)))
+ (exists ((f (_ BitVec 32)))
+ (=> (= (_ bv0 32) a)
+ (= (bvadd e g) (bvand d f) b c))))))))
+(check-sat)
projects / cvc5.git / commitdiff