From: Andrew Reynolds Date: Tue, 14 Nov 2017 19:42:48 +0000 (-0600) Subject: Clean Ceg Instantiators (#1365) X-Git-Tag: cvc5-1.0.0~5477 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=376d72fd02d7f8822188055355452449b718481f;p=cvc5.git Clean Ceg Instantiators (#1365) * Initial setup for preprocessing counterexample lemmas. * Improve documentation. * Improving documentation, infrastructure. * Extraction -> concatentation as a preprocess step. * Clang format * Minor * Make option, refactor effort levels. * Format * Clean * Format * Rename * Format * More * Format * Splitting changes. * Format * Revert option. * Minor * Format --- diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 36fac5e80..b41a3cfca 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -26,20 +26,35 @@ #include "theory/theory_engine.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta, bool use_vts_inf ) : -d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_vts_inf ){ - d_is_nested_quant = false; +namespace CVC4 { +namespace theory { +namespace quantifiers { + +CegInstantiator::CegInstantiator(QuantifiersEngine* qe, + CegqiOutput* out, + bool use_vts_delta, + bool use_vts_inf) + : d_qe(qe), + d_out(out), + d_use_vts_delta(use_vts_delta), + d_use_vts_inf(use_vts_inf), + d_num_input_variables(0), + d_is_nested_quant(false), + d_effort(INST_EFFORT_NONE) +{ } CegInstantiator::~CegInstantiator() { - for( std::map< Node, Instantiator * >::iterator it = d_instantiator.begin(); it != d_instantiator.end(); ++it ){ - delete it->second; + for (std::pair inst : d_instantiator) + { + delete inst.second; + } + for (std::pair instp : d_tipp) + { + delete instp.second; } } @@ -90,8 +105,8 @@ bool CegInstantiator::hasVariable( Node n, Node pv ) { return d_prog_var[n].find( pv )!=d_prog_var[n].end(); } - -void CegInstantiator::registerInstantiationVariable( Node v, unsigned index ) { +void CegInstantiator::activateInstantiationVariable(Node v, unsigned index) +{ if( d_instantiator.find( v )==d_instantiator.end() ){ TypeNode tn = v.getType(); Instantiator * vinst; @@ -116,21 +131,82 @@ void CegInstantiator::registerInstantiationVariable( Node v, unsigned index ) { d_curr_index[v] = index; } -void CegInstantiator::unregisterInstantiationVariable( Node v ) { +void CegInstantiator::registerTheoryIds(TypeNode tn, + std::map& visited) +{ + if (visited.find(tn) == visited.end()) + { + visited[tn] = true; + TheoryId tid = Theory::theoryOf(tn); + registerTheoryId(tid); + if (tn.isDatatype()) + { + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for (unsigned i = 0; i < dt.getNumConstructors(); i++) + { + for (unsigned j = 0; j < dt[i].getNumArgs(); j++) + { + registerTheoryIds( + TypeNode::fromType( + ((SelectorType)dt[i][j].getType()).getRangeType()), + visited); + } + } + } + } +} + +void CegInstantiator::registerTheoryId(TheoryId tid) +{ + if (std::find(d_tids.begin(), d_tids.end(), tid) == d_tids.end()) + { + // setup any theory-specific preprocessors here + + d_tids.push_back(tid); + } +} + +void CegInstantiator::registerVariable(Node v, bool is_aux) +{ + Assert(std::find(d_vars.begin(), d_vars.end(), v) == d_vars.end()); + Assert(std::find(d_aux_vars.begin(), d_aux_vars.end(), v) + == d_aux_vars.end()); + if (!is_aux) + { + d_vars.push_back(v); + d_vars_set.insert(v); + } + else + { + d_aux_vars.push_back(v); + } + TypeNode vtn = v.getType(); + Trace("cbqi-proc-debug") << "Collect theory ids from type " << vtn << " of " + << v << std::endl; + // collect relevant theories for this variable + std::map visited; + registerTheoryIds(vtn, visited); +} + +void CegInstantiator::deactivateInstantiationVariable(Node v) +{ d_curr_subs_proc.erase( v ); d_curr_index.erase( v ); } -bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){ +bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) +{ if( i==d_vars.size() ){ //solved for all variables, now construct instantiation bool needsPostprocess = - sf.d_vars.size() > d_vars.size() || !d_var_order_index.empty(); + sf.d_vars.size() > d_num_input_variables || !d_var_order_index.empty(); std::vector< Instantiator * > pp_inst; std::map< Instantiator *, Node > pp_inst_to_var; std::vector< Node > lemmas; for( std::map< Node, Instantiator * >::iterator ita = d_active_instantiators.begin(); ita != d_active_instantiators.end(); ++ita ){ - if( ita->second->needsPostProcessInstantiationForVariable( this, sf, ita->first, effort ) ){ + if (ita->second->needsPostProcessInstantiationForVariable( + this, sf, ita->first, d_effort)) + { needsPostprocess = true; pp_inst_to_var[ ita->second ] = ita->first; } @@ -140,7 +216,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e SolvedForm sf_tmp = sf; bool postProcessSuccess = true; for( std::map< Instantiator *, Node >::iterator itp = pp_inst_to_var.begin(); itp != pp_inst_to_var.end(); ++itp ){ - if( !itp->first->postProcessInstantiationForVariable( this, sf_tmp, itp->second, effort, lemmas ) ){ + if (!itp->first->postProcessInstantiationForVariable( + this, sf_tmp, itp->second, d_effort, lemmas)) + { postProcessSuccess = false; break; } @@ -164,7 +242,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e is_cv = true; d_stack_vars.pop_back(); } - registerInstantiationVariable( pv, i ); + activateInstantiationVariable(pv, i); //get the instantiator object Instantiator * vinst = NULL; @@ -174,7 +252,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e } Assert( vinst!=NULL ); d_active_instantiators[pv] = vinst; - vinst->reset( this, sf, pv, effort ); + vinst->reset(this, sf, pv, d_effort); TypeNode pvtn = pv.getType(); TypeNode pvtnb = pvtn.getBaseType(); @@ -189,9 +267,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; } - //if in effort=2, we must choose at least one model value - if( (i+1) >::iterator it_eqc = d_curr_eqc.find( pvr ); @@ -219,24 +297,29 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e proc = true; } if( proc ){ - if( vinst->processEqualTerm( this, sf, pv, pv_prop, ns, effort ) ){ + if (vinst->processEqualTerm( + this, sf, pv, pv_prop, ns, d_effort)) + { return true; } } } } } - if( vinst->processEqualTerms( this, sf, pv, it_eqc->second, effort ) ){ + if (vinst->processEqualTerms(this, sf, pv, it_eqc->second, d_effort)) + { return true; } }else{ Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl; } - //[3] : we can solve an equality for pv - ///iterate over equivalence classes to find cases where we can solve for the variable - if( vinst->hasProcessEquality( this, sf, pv, effort ) ){ - Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << std::endl; + //[2] : we can solve an equality for pv + /// iterate over equivalence classes to find cases where we can solve for + /// the variable + if (vinst->hasProcessEquality(this, sf, pv, d_effort)) + { + Trace("cbqi-inst-debug") << "[2] try based on solving equalities." << std::endl; for( unsigned k=0; k >::iterator it_reqc = d_curr_eqc.find( r ); @@ -272,7 +355,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e Trace("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl; term_props.push_back( lhs_prop[j] ); terms.push_back( lhs[j] ); - if( vinst->processEquality( this, sf, pv, term_props, terms, effort ) ){ + if (vinst->processEquality( + this, sf, pv, term_props, terms, d_effort)) + { return true; } term_props.pop_back(); @@ -292,9 +377,10 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e } } - //[4] directly look at assertions - if( vinst->hasProcessAssertion( this, sf, pv, effort ) ){ - Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl; + //[3] directly look at assertions + if (vinst->hasProcessAssertion(this, sf, pv, d_effort)) + { + Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl; std::unordered_set< Node, NodeHashFunction > lits; //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; for( unsigned r=0; r<2; r++ ){ @@ -307,7 +393,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( lits.find(lit)==lits.end() ){ lits.insert(lit); Node plit = - vinst->hasProcessAssertion(this, sf, pv, lit, effort); + vinst->hasProcessAssertion(this, sf, pv, lit, d_effort); if (!plit.isNull()) { Trace("cbqi-inst-debug2") << " look at " << lit; if (plit != lit) { @@ -320,8 +406,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e Trace("cbqi-inst-debug") << "...try based on literal " << slit << std::endl; // check if contains pv if( hasVariable( slit, pv ) ){ - if (vinst->processAssertion(this, sf, pv, slit, lit, - effort)) { + if (vinst->processAssertion( + this, sf, pv, slit, lit, d_effort)) + { return true; } } @@ -331,16 +418,21 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e } } } - if (vinst->processAssertions(this, sf, pv, effort)) { + if (vinst->processAssertions(this, sf, pv, d_effort)) + { return true; } } } - //[5] resort to using value in model - // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype - bool use_model_value = vinst->useModelValue( this, sf, pv, effort ); - if( ( effort>0 || use_model_value || is_cv ) && vinst->allowModelValue( this, sf, pv, effort ) ){ + //[4] resort to using value in model. We do so if: + // - we are in a higher effort than INST_EFFORT_STANDARD, + // - if the variable is Boolean, or + // - if we are solving for a subfield of a datatype. + bool use_model_value = vinst->useModelValue(this, sf, pv, d_effort); + if ((d_effort > INST_EFFORT_STANDARD || use_model_value || is_cv) + && vinst->allowModelValue(this, sf, pv, d_effort)) + { #ifdef CVC4_ASSERTIONS if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){ Trace("cbqi-warn") << "Had to resort to model value." << std::endl; @@ -349,18 +441,25 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e #endif Node mv = getModelValue( pv ); TermProperties pv_prop_m; - Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl; - int new_effort = use_model_value ? effort : 1; - if( doAddInstantiationInc( pv, mv, pv_prop_m, sf, new_effort ) ){ + Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; + InstEffort prev = d_effort; + if (!use_model_value) + { + // update the effort level to indicate we have used a model value + d_effort = INST_EFFORT_STANDARD_MV; + } + if (constructInstantiationInc(pv, mv, pv_prop_m, sf)) + { return true; } + d_effort = prev; } Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; if( is_cv ){ d_stack_vars.push_back( pv ); } d_active_instantiators.erase( pv ); - unregisterInstantiationVariable( pv ); + deactivateInstantiationVariable(pv); return false; } } @@ -374,12 +473,11 @@ void CegInstantiator::popStackVariable() { d_stack_vars.pop_back(); } -bool CegInstantiator::doAddInstantiationInc(Node pv, - Node n, - TermProperties& pv_prop, - SolvedForm& sf, - unsigned effort, - bool revertOnSuccess) +bool CegInstantiator::constructInstantiationInc(Node pv, + Node n, + TermProperties& pv_prop, + SolvedForm& sf, + bool revertOnSuccess) { Node cnode = pv_prop.getCacheNode(); if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){ @@ -470,7 +568,7 @@ bool CegInstantiator::doAddInstantiationInc(Node pv, sf.push_back( pv, n, pv_prop ); Trace("cbqi-inst-debug2") << "Recurse..." << std::endl; unsigned i = d_curr_index[pv]; - success = doAddInstantiation( sf, d_stack_vars.empty() ? i+1 : i, effort ); + success = constructInstantiation(sf, d_stack_vars.empty() ? i + 1 : i); if (!success || revertOnSuccess) { Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl; @@ -501,14 +599,16 @@ bool CegInstantiator::doAddInstantiationInc(Node pv, } bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) { - if( vars.size()>d_vars.size() ){ + if (vars.size() > d_num_input_variables) + { Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; std::map< Node, Node > subs_map; for( unsigned i=0; i::iterator it = subs_map.find( d_vars[i] ); Assert( it!=subs_map.end() ); Node n = it->second; @@ -516,14 +616,18 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector subs.push_back( n ); } } + Trace("cbqi-inst-debug") << "Sort based on order...." << std::endl; if( !d_var_order_index.empty() ){ std::vector< Node > subs_orig; subs_orig.insert( subs_orig.end(), subs.begin(), subs.end() ); subs.clear(); for( unsigned i=0; idoAddInstantiation( subs ); for( unsigned i=0; iaddLemma( lemmas[i] ); @@ -714,11 +818,13 @@ bool CegInstantiator::check() { } processAssertions(); for( unsigned r=0; r<2; r++ ){ + d_effort = r == 0 ? INST_EFFORT_STANDARD : INST_EFFORT_FULL; SolvedForm sf; d_stack_vars.clear(); d_bound_var_index.clear(); //try to add an instantiation - if( doAddInstantiation( sf, 0, r==0 ? 0 : 2 ) ){ + if (constructInstantiation(sf, 0)) + { return true; } } @@ -792,25 +898,6 @@ void CegInstantiator::presolve( Node q ) { } } -void collectTheoryIds( TypeNode tn, std::map< TypeNode, bool >& visited, std::vector< TheoryId >& tids ){ - std::map< TypeNode, bool >::iterator itt = visited.find( tn ); - if( itt==visited.end() ){ - visited[tn] = true; - TheoryId tid = Theory::theoryOf( tn ); - if( std::find( tids.begin(), tids.end(), tid )==tids.end() ){ - tids.push_back( tid ); - } - if( tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - for( unsigned i=0; i voo; - for( unsigned i=0; i& lems, st d_aux_vars.clear(); d_aux_eq.clear(); for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { - Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl; - d_aux_vars.push_back( i->first ); + Trace("cbqi-reg") << " register aux variable : " << i->first << std::endl; + registerVariable(i->first, true); } for( unsigned i=0; i& lems, st }*/ lems[i] = rlem; } + + // preprocess with all relevant instantiator preprocessors + Trace("cbqi-debug") << "Preprocess based on theory-specific methods..." + << std::endl; + std::vector pvars; + pvars.insert(pvars.end(), d_vars.begin(), d_vars.end()); + for (std::map::iterator it = + d_tipp.begin(); + it != d_tipp.end(); + ++it) + { + it->second->registerCounterexampleLemma(lems, pvars); + } + // must register variables generated by preprocessors + Trace("cbqi-debug") << "Register variables from theory-specific methods " + << d_num_input_variables << " " << d_vars.size() << " ..." + << std::endl; + for (unsigned i = d_num_input_variables; i < pvars.size(); i++) + { + Trace("cbqi-reg") << " register theory preprocess variable : " << pvars[i] << std::endl; + registerVariable(pvars[i]); + } + + // determine variable order: must do Reals before Ints + Trace("cbqi-debug") << "Determine variable order..." << std::endl; + if (!d_vars.empty()) + { + TypeNode tn0 = d_vars[0].getType(); + bool doSort = false; + std::map voo; + for (unsigned i = 0; i < d_vars.size(); i++) + { + voo[d_vars[i]] = i; + d_var_order_index.push_back(0); + if (d_vars[i].getType() != tn0) + { + doSort = true; + } + } + if (doSort) + { + Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl; + sortCegVarOrder scvo; + std::sort(d_vars.begin(), d_vars.end(), scvo); + Trace("cbqi-debug") << "Consider variables in this order : " << std::endl; + for (unsigned i = 0; i < d_vars.size(); i++) + { + d_var_order_index[voo[d_vars[i]]] = i; + Trace("cbqi-debug") << " " << d_vars[i] << " : " << d_vars[i].getType() + << ", index was : " << voo[d_vars[i]] << std::endl; + } + Trace("cbqi-debug") << std::endl; + } + else + { + d_var_order_index.clear(); + } + } + //collect atoms from all lemmas: we will only do bounds coming from original body d_is_nested_quant = false; std::map< Node, bool > visited; for( unsigned i=0; i visited; - collectTheoryIds( pvtn, visited, d_tids ); - } - } } @@ -1142,10 +1252,17 @@ Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ) d_closed_enum_type = qe->getTermEnumeration()->isClosedEnumerableType(tn); } - -bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) { +bool Instantiator::processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + InstEffort effort) +{ pv_prop.d_type = 0; - return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort ); + return ci->constructInstantiationInc(pv, n, pv_prop, sf); } - +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 1e59bfb43..bf5a37026 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -39,10 +39,14 @@ public: }; class Instantiator; +class InstantiatorPreprocess; /** Term Properties - * stores properties for a variable to solve for in CEGQI - * For LIA, this includes the coefficient of the variable, and the bound type + * + * Stores properties for a variable to solve for in counterexample-guided + * instantiation. + * + * For LIA, this includes the coefficient of the variable, and the bound type * for the variable. */ class TermProperties { @@ -53,8 +57,9 @@ public: int d_type; // for arithmetic Node d_coeff; - // get cache node - // we consider terms + TermProperties that are unique up to their cache node (see doAddInstantiationInc) + // get cache node + // we consider terms + TermProperties that are unique up to their cache node + // (see constructInstantiationInc) virtual Node getCacheNode() const { return d_coeff; } // is non-basic virtual bool isBasic() const { return d_coeff.isNull(); } @@ -138,12 +143,126 @@ public: } }; +/** instantiation effort levels */ +enum InstEffort +{ + // uninitialized + INST_EFFORT_NONE, + // standard effort level + INST_EFFORT_STANDARD, + // standard effort level, but we have used model values + INST_EFFORT_STANDARD_MV, + // full effort level + INST_EFFORT_FULL +}; + /** Ceg instantiator * * This class manages counterexample-guided quantifier instantiation * for a single quantified formula. + * + * For details on counterexample-guided quantifier instantiation + * (for linear arithmetic), see Reynolds/King/Kuncak FMSD 2017. */ class CegInstantiator { + public: + CegInstantiator(QuantifiersEngine* qe, + CegqiOutput* out, + bool use_vts_delta = true, + bool use_vts_inf = true); + virtual ~CegInstantiator(); + /** check + * This adds instantiations based on the state of d_vars in current context + * on the output channel d_out of this class. + */ + bool check(); + /** presolve for quantified formula + * + * This initializes formulas that help static learning of the quantifier-free + * solver. It is only called if the option --cbqi-prereg-inst is used. + */ + 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& lems, + std::vector& ce_vars); + /** get the output channel of this class */ + CegqiOutput* getOutput() { return d_out; } + //------------------------------interface for instantiators + /** get quantifiers engine */ + QuantifiersEngine* getQuantifiersEngine() { return d_qe; } + /** push stack variable + * This adds a new variable to solve for in the stack + * of variables we are processing. This stack is only + * used for datatypes, where e.g. the DtInstantiator + * solving for a list x may push the stack "variables" + * head(x) and tail(x). + */ + void pushStackVariable(Node v); + /** pop stack variable */ + void popStackVariable(); + /** construct instantiation increment + * + * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current + * instantiation, specified by sf. + * + * This function returns true if a call to + * QuantifiersEngine::addInstantiation(...) + * was successfully made in a recursive call. + * + * The solved form sf is reverted to its original state if + * this function returns false, or + * revertOnSuccess is true and this function returns true. + */ + bool constructInstantiationInc(Node pv, + Node n, + TermProperties& pv_prop, + SolvedForm& sf, + bool revertOnSuccess = false); + /** get the current model value of term n */ + Node getModelValue(Node n); + /** get bound variable for type + * + * This gets the next (canonical) bound variable of + * type tn. This can be used for instance when + * constructing instantiations that involve choice expressions. + */ + Node getBoundVariable(TypeNode tn); + //------------------------------end interface for instantiators + + /** + * Get the number of atoms in the counterexample lemma of the quantified + * formula we are processing with this class. + */ + unsigned getNumCEAtoms() { return d_ce_atoms.size(); } + /** + * Get the i^th atom of the counterexample lemma of the quantified + * formula we are processing with this class. + */ + Node getCEAtom(unsigned i) { return d_ce_atoms[i]; } + /** is n a term that is eligible for instantiation? */ + bool isEligible(Node n); + /** does n have variable pv? */ + bool hasVariable(Node n, Node pv); + /** are we using delta for LRA virtual term substitution? */ + bool useVtsDelta() { return d_use_vts_delta; } + /** are we using infinity for LRA virtual term substitution? */ + bool useVtsInfinity() { return d_use_vts_inf; } + /** are we processing a nested quantified formula? */ + bool hasNestedQuantification() { return d_is_nested_quant; } private: /** quantified formula associated with this instantiator */ QuantifiersEngine* d_qe; @@ -157,6 +276,8 @@ class CegInstantiator { * (for quantified LRA). */ bool d_use_vts_inf; + + //-------------------------------globally cached /** cache from nodes to the set of variables it contains * (from the quantified formula we are instantiating). */ @@ -168,25 +289,88 @@ class CegInstantiator { * ineligible for instantiation. */ std::unordered_set d_inelig; + /** ensures n is in d_prog_var and d_inelig. */ + void computeProgVars(Node n); + //-------------------------------end globally cached + + //-------------------------------cached per round /** current assertions per theory */ std::map > d_curr_asserts; /** map from representatives to the terms in their equivalence class */ std::map > d_curr_eqc; /** map from types to representatives of that type */ std::map > d_curr_type_eqc; - /** auxiliary variables - * These variables include the result of removing ITE - * terms from the quantified formula we are processing. - * These variables must be eliminated from constraints - * as a preprocess step to check(). + /** process assertions + * This is called once at the beginning of check to + * set up all necessary information for constructing instantiations, + * such as the above data structures. */ - std::vector d_aux_vars; + void processAssertions(); + /** add to auxiliary variable substitution + * This adds the substitution l -> r to the auxiliary + * variable substitution subs_lhs -> subs_rhs, and serializes + * it (applies it to existing substitutions). + */ + void addToAuxVarSubstitution(std::vector& subs_lhs, + std::vector& subs_rhs, + Node l, + Node r); + /** cache bound variables for type returned + * by getBoundVariable(...). + */ + std::unordered_map, TypeNodeHashFunction> + d_bound_var; + /** current index of bound variables for type. + * The next call to getBoundVariable(...) for + * type tn returns the d_bound_var_index[tn]^th + * element of d_bound_var[tn], or a fresh variable + * if not in bounds. + */ + std::unordered_map + d_bound_var_index; + //-------------------------------end cached per round + + //-------------------------------data per theory /** relevant theory ids * A list of theory ids that contain at least one * constraint in the body of the quantified formula we * are processing. */ std::vector d_tids; + /** map from theory ids to instantiator preprocessors */ + std::map d_tipp; + /** registers all theory ids associated with type tn + * + * This recursively calls registerTheoryId for typeOf(tn') for + * all parameters and datatype subfields of type tn. + * visited stores the types we have already visited. + */ + void registerTheoryIds(TypeNode tn, std::map& visited); + /** register theory id tid + * + * This is called when the quantified formula we are processing + * with this class involves theory tid. In this case, we will + * construct instantiations based on the assertion list of this theory. + */ + void registerTheoryId(TheoryId tid); + //-------------------------------end data per theory + + //-------------------------------the variables + /** the variables we are instantiating + * For a quantified formula with n variables, + * the first n terms in d_vars are the instantiation + * constants corresponding to these variables. + */ + std::vector d_vars; + /** set form of d_vars */ + std::unordered_set d_vars_set; + /** index of variables reported in instantiation */ + std::vector d_var_order_index; + /** number of input variables + * This is n for quantified formulas with n variables, + * and is at most the size of d_vars. + */ + unsigned d_num_input_variables; /** literals to equalities for aux vars * This stores entries of the form * L -> ( k -> t ) @@ -207,59 +391,64 @@ class CegInstantiator { * k=t1 and k=t2 respectively. */ std::map > d_aux_eq; - /** the variables we are instantiating - * These are the inst constants of the quantified formula - * we are processing. + /** auxiliary variables + * These variables include the result of removing ITE + * terms from the quantified formula we are processing. + * These variables must be eliminated from constraints + * as a preprocess step to check(). */ - std::vector d_vars; - /** set form of d_vars */ - std::unordered_set d_vars_set; - /** index of variables reported in instantiation */ - std::vector d_var_order_index; - /** are we handled a nested quantified formula? */ + std::vector d_aux_vars; + /** register variable */ + void registerVariable(Node v, bool is_aux = false); + //-------------------------------the variables + + //-------------------------------quantified formula info + /** are we processing a nested quantified formula? */ bool d_is_nested_quant; /** the atoms of the CE lemma */ std::vector d_ce_atoms; - /** cache bound variables for type returned - * by getBoundVariable(...). - */ - std::unordered_map, TypeNodeHashFunction> - d_bound_var; - /** current index of bound variables for type. - * The next call to getBoundVariable(...) for - * type tn returns the d_bound_var_index[tn]^th - * element of d_bound_var[tn], or a fresh variable - * if not in bounds. - */ - std::unordered_map - d_bound_var_index; /** collect atoms */ void collectCeAtoms(Node n, std::map& visited); + //-------------------------------end quantified formula info - private: - //map from variables to their instantiators - std::map< Node, Instantiator * > d_instantiator; - //cache of current substitutions tried between register/unregister - std::map< Node, std::map< Node, std::map< Node, bool > > > d_curr_subs_proc; - std::map< Node, unsigned > d_curr_index; - //stack of temporary variables we are solving (e.g. subfields of datatypes) - std::vector< Node > d_stack_vars; + //-------------------------------current state + /** the current effort level of the instantiator + * This indicates the effort Instantiator objects + * will put into the terms they return. + */ + InstEffort d_effort; /** for each variable, the instantiator used for that variable */ - std::map< Node, Instantiator * > d_active_instantiators; - //register variable - void registerInstantiationVariable( Node v, unsigned index ); - void unregisterInstantiationVariable( Node v ); -private: - //for adding instantiations during check - void computeProgVars( Node n ); - // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ); - // called by the above function after we finalize the variables/substitution and auxiliary lemmas - bool doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ); - //process - void processAssertions(); - void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); -private: + std::map d_active_instantiators; + /** map from variables to the index in the prefix of the quantified + * formula we are processing. + */ + std::map d_curr_index; + /** cache of current substitutions tried between activate/deactivate */ + std::map > > d_curr_subs_proc; + /** stack of temporary variables we are solving for, + * e.g. subfields of datatypes. + */ + std::vector d_stack_vars; + /** activate instantiation variable v at index + * + * This is called when variable (inst constant) v is activated + * for the quantified formula we are processing. + * This method initializes the instantiator class for + * that variable if necessary, where this class is + * determined by the type of v. It also initializes + * the cache of values we have tried substituting for v + * (in d_curr_subs_proc), and stores its index. + */ + void activateInstantiationVariable(Node v, unsigned index); + /** deactivate instantiation variable + * + * This is called when variable (inst constant) v is deactivated + * for the quantified formula we are processing. + */ + void deactivateInstantiationVariable(Node v); + //-------------------------------end current state + + //---------------------------------for applying substitutions /** can use basic substitution */ bool canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ); /** apply substitution @@ -285,170 +474,268 @@ private: /** apply substitution to literal lit, with solved form expanded to subs/prop/non_basic/vars */ Node applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& non_basic ); + //---------------------------------end for applying substitutions + + /** map from variables to their instantiators */ + std::map d_instantiator; + + /** construct instantiation + * This method constructs the current instantiation, where we + * are currently processing the i^th variable in d_vars. + * It returns true if a successful call to the output channel's + * doAddInstantiation was made. + */ + bool constructInstantiation(SolvedForm& sf, unsigned i); + /** do add instantiation + * This method is called by the above function after we finalize the + * variables/substitution and auxiliary lemmas. + * It returns true if a successful call to the output channel's + * doAddInstantiation was made. + */ + bool doAddInstantiation(std::vector& vars, + std::vector& subs, + std::vector& lemmas); +}; + +/** Instantiator class + * + * This is a virtual class that is used for methods for constructing + * substitutions for individual variables in counterexample-guided + * instantiation techniques. + * + * This class contains a set of interface functions below, which are called + * based on a fixed instantiation method implemented by CegInstantiator. + * In these calls, the Instantiator in turn makes calls to methods in + * CegInstanatior (primarily constructInstantiationInc). + */ +class Instantiator { public: - CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); - virtual ~CegInstantiator(); - //check : add instantiations based on valuation of d_vars - bool check(); - //presolve for quantified formula - void presolve( Node q ); - //register the counterexample lemma (stored in lems), modify vector - void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); - //output - CegqiOutput * getOutput() { return d_out; } - //get quantifiers engine - QuantifiersEngine* getQuantifiersEngine() { return d_qe; } - //------------------------------interface for instantiators - /** push stack variable - * This adds a new variable to solve for in the stack - * of variables we are processing. This stack is only - * used for datatypes, where e.g. the DtInstantiator - * solving for a list x may push the stack "variables" - * head(x) and tail(x). + Instantiator( QuantifiersEngine * qe, TypeNode tn ); + virtual ~Instantiator(){} + /** reset + * This is called once, prior to any of the below methods are called. + * This function sets up any initial information necessary for constructing + * instantiations for pv based on the current context. */ - void pushStackVariable( Node v ); - /** pop stack variable */ - void popStackVariable(); - /** do add instantiation increment + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + } + + /** process equal term * - * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current - * instantiation, specified by sf. + * This method is called when the entailment: + * E |= pv_prop.getModifiedTerm(pv) = n + * holds in the current context E, and n is eligible for instantiation. * - * This function returns true if a call to - * QuantifiersEngine::addInstantiation(...) - * was successfully made in a recursive call. - * - * The solved form sf is reverted to its original state if - * this function returns false, or - * revertOnSuccess is true and this function returns true. + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. */ - bool doAddInstantiationInc(Node pv, - Node n, - TermProperties& pv_prop, - SolvedForm& sf, - unsigned effort, - bool revertOnSuccess = false); - /** get the current model value of term n */ - Node getModelValue( Node n ); - /** get bound variable for type + virtual bool processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + InstEffort effort); + /** process equal terms * - * This gets the next (canonical) bound variable of - * type tn. This can be used for instance when - * constructing instantiations that involve choice expressions. + * This method is called after process equal term, where eqc is the list of + * eligible terms in the equivalence class of pv. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. */ - Node getBoundVariable(TypeNode tn); - //------------------------------end interface for instantiators - unsigned getNumCEAtoms() { return d_ce_atoms.size(); } - Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; } - /** is n a term that is eligible for instantiation? */ - bool isEligible( Node n ); - /** does n have variable pv? */ - bool hasVariable( Node n, Node pv ); - /** are we using delta for LRA virtual term substitution? */ - bool useVtsDelta() { return d_use_vts_delta; } - /** are we using infinity for LRA virtual term substitution? */ - bool useVtsInfinity() { return d_use_vts_inf; } - /** are we processing a nested quantified formula? */ - bool hasNestedQuantification() { return d_is_nested_quant; } -}; + virtual bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& eqc, + InstEffort effort) + { + return false; + } + /** whether the instantiator implements processEquality */ + virtual bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return false; + } + /** process equality + * The input is such that term_props.size() = terms.size() = 2 + * This method is called when the entailment: + * E ^ term_props[0].getModifiedTerm(x0) = + * terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1 + * holds in current context E for fresh variables xi, terms[i] are eligible, + * and at least one terms[i] contains pv for i = 0,1. + * Notice in the basic case, E |= terms[0] = terms[1]. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& term_props, + std::vector& terms, + InstEffort effort) + { + return false; + } -// an instantiator for individual variables -// will make calls into CegInstantiator::doAddInstantiationInc -class Instantiator { -protected: - TypeNode d_type; - bool d_closed_enum_type; -public: - Instantiator( QuantifiersEngine * qe, TypeNode tn ); - virtual ~Instantiator(){} - virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {} - - // Called when the entailment: - // E |= pv_prop.getModifiedTerm(pv) = n - // holds in the current context E, and n is eligible for instantiation. - virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ); - // Called about process equal term, where eqc is the list of eligible terms in the equivalence class of pv - virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; } - - // whether the instantiator implements processEquality - virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - // term_props.size() = terms.size() = 2 - // Called when the entailment: - // E ^ term_props[0].getModifiedTerm(x0) = terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1 - // holds in current context E for fresh variables xi, terms[i] are eligible, and at least one terms[i] contains pv for i = 0,1. - // Notice in the basic case, E |= terms[0] = terms[1]. - // Returns true if an instantiation was successfully added via a recursive call - virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { return false; } - - // whether the instantiator implements processAssertion for any literal - virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + /** whether the instantiator implements processAssertion for any literal */ + virtual bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return false; + } /** has process assertion * - * Called when the entailment: + * This method is called when the entailment: * E |= lit * holds in current context E. Typically, lit belongs to the list of current * assertions. * - * This function is used to determine whether the instantiator implements + * This method is used to determine whether the instantiator implements * processAssertion for literal lit. - * If this function returns null, then this intantiator does not handle the - * literal lit - * Otherwise, this function returns a literal lit' with the properties: + * If this method returns null, then this intantiator does not handle the + * literal lit. Otherwise, this method returns a literal lit' such that: * (1) lit' is true in the current model, * (2) lit' implies lit. * where typically lit' = lit. */ - virtual Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, - Node lit, unsigned effort) { + virtual Node hasProcessAssertion( + CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort) + { return Node::null(); } /** process assertion - * Processes the assertion slit for variable pv - * - * lit is the substituted form (under sf) of a literal returned by - * hasProcessAssertion - * alit is the asserted literal, given as input to hasProcessAssertion - * - * Returns true if an instantiation was successfully added via a recursive call - */ - virtual bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, - Node lit, Node alit, unsigned effort) { + * This method processes the assertion slit for variable pv. + * lit : the substituted form (under sf) of a literal returned by + * hasProcessAssertion + * alit : the asserted literal, given as input to hasProcessAssertion + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + InstEffort effort) + { return false; } /** process assertions - * Called after processAssertion is called for each literal asserted to the - * instantiator. - */ - virtual bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, - unsigned effort) { + * + * Called after processAssertion is called for each literal asserted to the + * instantiator. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { return false; } - //do we use the model value as instantiation for pv - virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - //do we allow the model value as instantiation for pv - virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; } + /** do we use the model value as instantiation for pv? + * This method returns true if we use model value instantiations + * at the same effort level as those determined by this instantiator. + */ + virtual bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return false; + } + /** do we allow the model value as instantiation for pv? */ + virtual bool allowModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return d_closed_enum_type; + } - //do we need to postprocess the solved form for pv? - virtual bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - //postprocess the solved form for pv, returns true if we successfully postprocessed, lemmas is a set of lemmas we wish to return along with the instantiation - virtual bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ) { return true; } + /** do we need to postprocess the solved form for pv? */ + virtual bool needsPostProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return false; + } + /** postprocess the solved form for pv + * + * This method returns true if we successfully postprocessed the solved form. + * lemmas is a set of lemmas we wish to return along with the instantiation. + */ + virtual bool postProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort, + std::vector& lemmas) + { + return true; + } /** Identify this module (for debugging) */ virtual std::string identify() const { return "Default"; } + protected: + /** the type of the variable we are instantiating */ + TypeNode d_type; + /** whether d_type is a closed enumerable type */ + bool d_closed_enum_type; }; class ModelValueInstantiator : public Instantiator { public: ModelValueInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~ModelValueInstantiator(){} - bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return true; + } std::string identify() const { return "ModelValue"; } }; -} -} -} +/** instantiator preprocess + * + * This class implements techniques for preprocessing the counterexample lemma + * generated for counterexample-guided quantifier instantiation. + */ +class InstantiatorPreprocess +{ + public: + InstantiatorPreprocess() {} + virtual ~InstantiatorPreprocess() {} + /** register counterexample lemma + * This implements theory-specific preprocessing and registration + * of counterexample lemmas, with the same contract as + * CegInstantiation::registerCounterexampleLemma. + */ + virtual void registerCounterexampleLemma(std::vector& lems, + std::vector& ce_vars) + { + } +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ #endif diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index e16286fa9..7502d42f1 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -31,11 +31,12 @@ #include using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace theory { +namespace quantifiers { Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { Node val = t; @@ -214,7 +215,11 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No return ires; } -void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { +void ArithInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) +{ d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type, false, false ); d_vts_sym[1] = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta( false, false ); for( unsigned i=0; i<2; i++ ){ @@ -227,7 +232,13 @@ void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, un } } -bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { +bool ArithInstantiator::processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& term_props, + std::vector& terms, + InstEffort effort) +{ Node eq_lhs = terms[0]; Node eq_rhs = terms[1]; Node lhs_coeff = term_props[0].d_coeff; @@ -255,7 +266,8 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N int ires = solve_arith( ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta ); if( ires!=0 ){ pv_prop.d_type = 0; - if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){ + if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) + { return true; } } @@ -263,9 +275,9 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N return false; } -Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, - Node pv, Node lit, - unsigned effort) { +Node ArithInstantiator::hasProcessAssertion( + CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort) +{ Node atom = lit.getKind()==NOT ? lit[0] : lit; bool pol = lit.getKind()!=NOT; //arithmetic inequalities and disequalities @@ -277,9 +289,13 @@ Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, } } -bool ArithInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf, - Node pv, Node lit, Node alit, - unsigned effort) { +bool ArithInstantiator::processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + InstEffort effort) +{ Node atom = lit.getKind()==NOT ? lit[0] : lit; bool pol = lit.getKind()!=NOT; //arithmetic inequalities and disequalities @@ -383,7 +399,8 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf, }else{ //try this bound pv_prop.d_type = uires>0 ? 1 : -1; - if( ci->doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){ + if (ci->constructInstantiationInc(pv, uval, pv_prop, sf)) + { return true; } } @@ -394,8 +411,11 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf, return false; } -bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, - Node pv, unsigned effort) { +bool ArithInstantiator::processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) +{ if (options::cbqiModel()) { bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); bool upper_first = false; @@ -422,7 +442,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, val = Rewriter::rewrite( val ); } TermProperties pv_prop_no_bound; - if( ci->doAddInstantiationInc( pv, val, pv_prop_no_bound, sf, effort ) ){ + if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf)) + { return true; } } @@ -519,7 +540,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, TermProperties pv_prop_bound; pv_prop_bound.d_coeff = d_mbp_coeff[rr][best]; pv_prop_bound.d_type = rr==0 ? 1 : -1; - if( ci->doAddInstantiationInc( pv, val, pv_prop_bound, sf, effort ) ){ + if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf)) + { return true; } } @@ -534,7 +556,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, Node theta = sf.getTheta(); val = getModelBasedProjectionValue( ci, pv, val, true, pv_prop_zero.d_coeff, pv_value, zero, sf.getTheta(), Node::null(), Node::null() ); if( !val.isNull() ){ - if( ci->doAddInstantiationInc( pv, val, pv_prop_zero, sf, effort ) ){ + if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf)) + { return true; } } @@ -576,7 +599,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl; if( !val.isNull() ){ TermProperties pv_prop_midpoint; - if( ci->doAddInstantiationInc( pv, val, pv_prop_midpoint, sf, effort ) ){ + if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf)) + { return true; } } @@ -597,7 +621,9 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, TermProperties pv_prop_nopt_bound; pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j]; pv_prop_nopt_bound.d_type = rr==0 ? 1 : -1; - if( ci->doAddInstantiationInc( pv, val, pv_prop_nopt_bound, sf, effort ) ){ + if (ci->constructInstantiationInc( + pv, val, pv_prop_nopt_bound, sf)) + { return true; } } @@ -609,12 +635,19 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, return false; } -bool ArithInstantiator::needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { +bool ArithInstantiator::needsPostProcessInstantiationForVariable( + CegInstantiator* ci, SolvedForm& sf, Node pv, InstEffort effort) +{ return std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end(); } -bool ArithInstantiator::postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, - std::vector< Node >& lemmas ) { +bool ArithInstantiator::postProcessInstantiationForVariable( + CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort, + std::vector& lemmas) +{ Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end() ); Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() ); unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin(); @@ -669,8 +702,11 @@ bool ArithInstantiator::postProcessInstantiationForVariable( CegInstantiator * c return true; } -void DtInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { - +void DtInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) +{ } Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { @@ -714,7 +750,12 @@ Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { return ret; } -bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { +bool DtInstantiator::processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& eqc, + InstEffort effort) +{ Trace("cegqi-dt-debug") << "[2] try based on constructors in equivalence class." << std::endl; //[2] look in equivalence class for a constructor for( unsigned k=0; kmkNode( kind::APPLY_CONSTRUCTOR, children ); TermProperties pv_prop_dt; - if( ci->doAddInstantiationInc( pv, val, pv_prop_dt, sf, effort ) ){ + if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf)) + { return true; }else{ //cleanup @@ -747,29 +789,46 @@ bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, No return false; } -bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { +bool DtInstantiator::processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& term_props, + std::vector& terms, + InstEffort effort) +{ Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] ); if( !val.isNull() ){ TermProperties pv_prop; - if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){ + if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) + { return true; } } return false; } -void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { +void EprInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) +{ d_equal_terms.clear(); } -bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) { +bool EprInstantiator::processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + InstEffort effort) +{ if( options::quantEprMatching() ){ Assert( pv_prop.isBasic() ); d_equal_terms.push_back( n ); return false; }else{ pv_prop.d_type = 0; - return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort ); + return ci->constructInstantiationInc(pv, n, pv_prop, sf); } } @@ -823,8 +882,12 @@ struct sortEqTermsMatch { } }; - -bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { +bool EprInstantiator::processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& eqc, + InstEffort effort) +{ if( options::quantEprMatching() ){ //heuristic for best matching constant sortEqTermsMatch setm; @@ -837,7 +900,8 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N TermProperties pv_prop; pv_prop.d_type = 0; for( unsigned i=0; idoAddInstantiationInc( pv, d_equal_terms[i], pv_prop, sf, effort ) ){ + if (ci->constructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf)) + { return true; } } @@ -877,8 +941,11 @@ BvInstantiator::BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instanti BvInstantiator::~BvInstantiator(){ } - -void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { +void BvInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) +{ d_inst_id_counter = 0; d_var_to_inst_id.clear(); d_inst_id_to_term.clear(); @@ -888,9 +955,13 @@ void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsig d_alit_to_model_slack.clear(); } -void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf, - Node pv, Node lit, Node alit, - unsigned effort) { +void BvInstantiator::processLiteral(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + InstEffort effort) +{ Assert( d_inverter!=NULL ); // find path to pv std::vector< unsigned > path; @@ -919,8 +990,9 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf, } } -Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, - Node pv, Node lit, unsigned effort) { +Node BvInstantiator::hasProcessAssertion( + CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort) +{ Node atom = lit.getKind() == NOT ? lit[0] : lit; bool pol = lit.getKind() != NOT; Kind k = atom.getKind(); @@ -1010,9 +1082,13 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, return Node::null(); } -bool BvInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf, - Node pv, Node lit, Node alit, - unsigned effort) { +bool BvInstantiator::processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + InstEffort effort) +{ // if option enabled, use approach for word-level inversion for BV instantiation if( options::cbqiBv() ){ // get the best rewritten form of lit for solving for pv @@ -1029,8 +1105,11 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf, return false; } -bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, - Node pv, unsigned effort) { +bool BvInstantiator::processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) +{ std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv ); if( iti!=d_var_to_inst_id.end() ){ Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl; @@ -1124,8 +1203,8 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl; d_var_to_curr_inst_id[pv] = inst_id; - if (ci->doAddInstantiationInc( - pv, inst_term, pv_prop_bv, sf, effort, revertOnSuccess)) + if (ci->constructInstantiationInc( + pv, inst_term, pv_prop_bv, sf, revertOnSuccess)) { ret = true; } @@ -1280,3 +1359,7 @@ Node BvInstantiator::rewriteTermForSolvePv( return Node::null(); } + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 30dd1bffa..0242a2994 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -27,65 +27,199 @@ namespace CVC4 { namespace theory { namespace quantifiers { +/** TODO (#1367) : document these classes, also move to separate files. */ + class ArithInstantiator : public Instantiator { -private: - Node d_vts_sym[2]; - std::vector< Node > d_mbp_bounds[2]; - std::vector< Node > d_mbp_coeff[2]; - std::vector< Node > d_mbp_vts_coeff[2][2]; - std::vector< Node > d_mbp_lit[2]; - int solve_arith( CegInstantiator * ci, Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ); - Node getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); -public: + public: ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~ArithInstantiator(){} - void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); - bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ); - bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, - Node lit, unsigned effort); - bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, - Node alit, unsigned effort); - bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, - unsigned effort); - bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); - bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ); - std::string identify() const { return "Arith"; } + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override; + virtual bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override + { + return true; + } + virtual bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& term_props, + std::vector& terms, + InstEffort effort) override; + virtual bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override + { + return true; + } + virtual Node hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + InstEffort effort) override; + virtual bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + InstEffort effort) override; + virtual bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override; + virtual bool needsPostProcessInstantiationForVariable( + CegInstantiator* ci, SolvedForm& sf, Node pv, InstEffort effort) override; + virtual bool postProcessInstantiationForVariable( + CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort, + std::vector& lemmas) override; + virtual std::string identify() const override { return "Arith"; } + private: + Node d_vts_sym[2]; + std::vector d_mbp_bounds[2]; + std::vector d_mbp_coeff[2]; + std::vector d_mbp_vts_coeff[2][2]; + std::vector d_mbp_lit[2]; + int solve_arith(CegInstantiator* ci, + Node v, + Node atom, + Node& veq_c, + Node& val, + Node& vts_coeff_inf, + Node& vts_coeff_delta); + Node getModelBasedProjectionValue(CegInstantiator* ci, + Node e, + Node t, + bool isLower, + Node c, + Node me, + Node mt, + Node theta, + Node inf_coeff, + Node delta_coeff); }; class DtInstantiator : public Instantiator { -private: - Node solve_dt( Node v, Node a, Node b, Node sa, Node sb ); public: DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~DtInstantiator(){} - void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); - bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); - bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ); - std::string identify() const { return "Dt"; } + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override; + virtual bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& eqc, + InstEffort effort) override; + virtual bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override + { + return true; + } + virtual bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& term_props, + std::vector& terms, + InstEffort effort) override; + virtual std::string identify() const override { return "Dt"; } + private: + Node solve_dt(Node v, Node a, Node b, Node sa, Node sb); }; class TermArgTrie; class EprInstantiator : public Instantiator { -private: - std::vector< Node > d_equal_terms; - void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ); - void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ); -public: + public: EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~EprInstantiator(){} - void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); - bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ); - bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); - std::string identify() const { return "Epr"; } + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override; + virtual bool processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + InstEffort effort) override; + virtual bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& eqc, + InstEffort effort) override; + virtual std::string identify() const override { return "Epr"; } + private: + std::vector d_equal_terms; + void computeMatchScore(CegInstantiator* ci, + Node pv, + Node catom, + std::vector& arg_reps, + TermArgTrie* tat, + unsigned index, + std::map& match_score); + void computeMatchScore(CegInstantiator* ci, + Node pv, + Node catom, + Node eqc, + std::map& match_score); }; - +/** Bitvector instantiator + * + * This implements an approach for counterexample-guided instantiation + * for bit-vector variables based on word-level inversions. + * It is enabled by --cbqi-bv. + */ class BvInstantiator : public Instantiator { -private: + public: + BvInstantiator(QuantifiersEngine* qe, TypeNode tn); + virtual ~BvInstantiator(); + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override; + virtual bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override + { + return true; + } + virtual Node hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + InstEffort effort) override; + virtual bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + InstEffort effort) override; + virtual bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override; + virtual bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) override + { + return true; + } + virtual std::string identify() const { return "Bv"; } + private: // point to the bv inverter class BvInverter * d_inverter; unsigned d_inst_id_counter; @@ -123,27 +257,16 @@ private: * internal rules here. * alit is the asserted literal that lit is derived from. */ - void processLiteral(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, - Node alit, unsigned effort); - - public: - BvInstantiator( QuantifiersEngine * qe, TypeNode tn ); - virtual ~BvInstantiator(); - void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); - bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, - Node lit, unsigned effort); - bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, - Node alit, unsigned effort); - bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, - unsigned effort); - bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - std::string identify() const { return "Bv"; } + void processLiteral(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + InstEffort effort); }; - -} -} -} +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ #endif diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 014f06aad..135a2c8d2 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -129,7 +129,7 @@ TESTS = \ # javafe.tc.CheckCompilationUnit.001.smt2 \ # javafe.tc.FlowInsensitiveChecks.682.smt2 \ # clock-10.smt2 -# +# extract-nproc.smt2 # FIXME: I've disabled these since they give different error messages on production and debug # macro-subtype-param.smt2 diff --git a/test/regress/regress0/quantifiers/extract-nproc.smt2 b/test/regress/regress0/quantifiers/extract-nproc.smt2 new file mode 100644 index 000000000..6072776dc --- /dev/null +++ b/test/regress/regress0/quantifiers/extract-nproc.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-rm-extract +; EXPECT: sat +(set-logic BV) +(declare-fun k_3 () (_ BitVec 8)) +(declare-fun k_4 () (_ BitVec 8)) +(declare-fun k_5 () (_ BitVec 8)) +(assert +(forall ((x (_ BitVec 8))) (or (= k_5 x) (not (= k_3 (bvadd (concat #b0000 ((_ extract 7 4) x)) #b01000001))) (not (= k_4 (bvadd (concat #b0000 ((_ extract 3 0) x)) #b01000001)))) )) +(check-sat)