* 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
#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<Node, Instantiator*> inst : d_instantiator)
+ {
+ delete inst.second;
+ }
+ for (std::pair<TheoryId, InstantiatorPreprocess*> instp : d_tipp)
+ {
+ delete instp.second;
}
}
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;
d_curr_index[v] = index;
}
-void CegInstantiator::unregisterInstantiationVariable( Node v ) {
+void CegInstantiator::registerTheoryIds(TypeNode tn,
+ std::map<TypeNode, bool>& 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<TypeNode, bool> 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;
}
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;
}
is_cv = true;
d_stack_vars.pop_back();
}
- registerInstantiationVariable( pv, i );
+ activateInstantiationVariable(pv, i);
//get the instantiator object
Instantiator * vinst = NULL;
}
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();
Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
}
- //if in effort=2, we must choose at least one model value
- if( (i+1)<d_vars.size() || effort!=2 ){
-
+ // if d_effort is full, we must choose at least one model value
+ if ((i + 1) < d_vars.size() || d_effort != INST_EFFORT_FULL)
+ {
//[1] easy case : pv is in the equivalence class as another term not containing pv
Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
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<d_curr_type_eqc[pvtnb].size(); k++ ){
Node r = d_curr_type_eqc[pvtnb][k];
std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
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();
}
}
- //[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++ ){
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) {
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;
}
}
}
}
}
- 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;
#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;
}
}
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() ){
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;
}
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<subs.size(); i++ ){
subs_map[vars[i]] = subs[i];
}
subs.clear();
- for( unsigned i=0; i<d_vars.size(); i++ ){
+ for (unsigned i = 0; i < d_vars.size(); i++)
+ {
std::map< Node, Node >::iterator it = subs_map.find( d_vars[i] );
Assert( it!=subs_map.end() );
Node n = it->second;
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; i<subs_orig.size(); i++ ){
+ Assert(d_var_order_index[i]<subs_orig.size());
subs.push_back( subs_orig[d_var_order_index[i]] );
}
}
+ subs.resize(d_num_input_variables);
+ Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl;
bool ret = d_out->doAddInstantiation( subs );
for( unsigned i=0; i<lemmas.size(); i++ ){
d_out->addLemma( lemmas[i] );
}
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;
}
}
}
}
-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<dt.getNumConstructors(); i++ ){
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- collectTheoryIds( TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ), visited, tids );
- }
- }
- }
- }
-}
-
void CegInstantiator::processAssertions() {
Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl;
d_curr_asserts.clear();
void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
+ Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl;
//Assert( d_vars.empty() );
d_vars.clear();
- d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
- d_vars_set.insert(ce_vars.begin(), ce_vars.end());
-
- //determine variable order: must do Reals before Ints
- if( !d_vars.empty() ){
- TypeNode tn0 = d_vars[0].getType();
- bool doSort = false;
- std::map< Node, unsigned > 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();
- }
+ d_num_input_variables = ce_vars.size();
+ registerTheoryId(THEORY_UF);
+ for (unsigned i = 0; i < ce_vars.size(); i++)
+ {
+ Trace("cbqi-reg") << " register input variable : " << ce_vars[i] << std::endl;
+ registerVariable(ce_vars[i]);
}
//remove ITEs
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.size(); i++ ){
Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl;
}*/
lems[i] = rlem;
}
+
+ // preprocess with all relevant instantiator preprocessors
+ Trace("cbqi-debug") << "Preprocess based on theory-specific methods..."
+ << std::endl;
+ std::vector<Node> pvars;
+ pvars.insert(pvars.end(), d_vars.begin(), d_vars.end());
+ for (std::map<TheoryId, InstantiatorPreprocess*>::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<Node, unsigned> 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<lems.size(); i++ ){
collectCeAtoms( lems[i], visited );
}
-
- //compute the theory ids
- d_tids.clear();
- d_tids.push_back(THEORY_UF);
- for( unsigned r=0; r<2; r++ ){
- unsigned sz = r==0 ? d_vars.size() : d_aux_vars.size();
- for( unsigned i=0; i<sz; i++ ){
- Node pv = r==0 ? d_vars[i] : d_aux_vars[i];
- TypeNode pvtn = pv.getType();
- Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
- //collect relevant theories
- std::map< TypeNode, bool > visited;
- collectTheoryIds( pvtn, visited, d_tids );
- }
- }
}
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 */
};
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 {
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(); }
}
};
+/** 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<Node>& lems,
+ std::vector<Node>& 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;
* (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).
*/
* ineligible for instantiation.
*/
std::unordered_set<Node, NodeHashFunction> 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<TheoryId, std::vector<Node> > d_curr_asserts;
/** map from representatives to the terms in their equivalence class */
std::map<Node, std::vector<Node> > d_curr_eqc;
/** map from types to representatives of that type */
std::map<TypeNode, std::vector<Node> > 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<Node> 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<Node>& subs_lhs,
+ std::vector<Node>& subs_rhs,
+ Node l,
+ Node r);
+ /** cache bound variables for type returned
+ * by getBoundVariable(...).
+ */
+ std::unordered_map<TypeNode, std::vector<Node>, 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<TypeNode, unsigned, TypeNodeHashFunction>
+ 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<TheoryId> d_tids;
+ /** map from theory ids to instantiator preprocessors */
+ std::map<TheoryId, InstantiatorPreprocess*> 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<TypeNode, bool>& 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<Node> d_vars;
+ /** set form of d_vars */
+ std::unordered_set<Node, NodeHashFunction> d_vars_set;
+ /** index of variables reported in instantiation */
+ std::vector<unsigned> 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 )
* k=t1 and k=t2 respectively.
*/
std::map<Node, std::map<Node, Node> > 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<Node> d_vars;
- /** set form of d_vars */
- std::unordered_set<Node, NodeHashFunction> d_vars_set;
- /** index of variables reported in instantiation */
- std::vector<unsigned> d_var_order_index;
- /** are we handled a nested quantified formula? */
+ std::vector<Node> 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<Node> d_ce_atoms;
- /** cache bound variables for type returned
- * by getBoundVariable(...).
- */
- std::unordered_map<TypeNode, std::vector<Node>, 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<TypeNode, unsigned, TypeNodeHashFunction>
- d_bound_var_index;
/** collect atoms */
void collectCeAtoms(Node n, std::map<Node, bool>& 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<Node, Instantiator*> d_active_instantiators;
+ /** map from variables to the index in the prefix of the quantified
+ * formula we are processing.
+ */
+ std::map<Node, unsigned> d_curr_index;
+ /** cache of current substitutions tried between activate/deactivate */
+ std::map<Node, std::map<Node, std::map<Node, bool> > > d_curr_subs_proc;
+ /** stack of temporary variables we are solving for,
+ * e.g. subfields of datatypes.
+ */
+ std::vector<Node> 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
/** 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<Node, Instantiator*> 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<Node>& vars,
+ std::vector<Node>& subs,
+ std::vector<Node>& 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<Node>& 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<TermProperties>& term_props,
+ std::vector<Node>& 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<Node>& 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<Node>& lems,
+ std::vector<Node>& ce_vars)
+ {
+ }
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
#endif
#include <stack>
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;
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++ ){
}
}
-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<TermProperties>& term_props,
+ std::vector<Node>& terms,
+ InstEffort effort)
+{
Node eq_lhs = terms[0];
Node eq_rhs = terms[1];
Node lhs_coeff = term_props[0].d_coeff;
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;
}
}
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
}
}
-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
}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;
}
}
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;
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;
}
}
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;
}
}
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;
}
}
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;
}
}
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;
}
}
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<Node>& 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();
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 ) {
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<Node>& 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; k<eqc.size(); k++ ){
}
Node val = NodeManager::currentNM()->mkNode( 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
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<TermProperties>& term_props,
+ std::vector<Node>& 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);
}
}
}
};
-
-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<Node>& eqc,
+ InstEffort effort)
+{
if( options::quantEprMatching() ){
//heuristic for best matching constant
sortEqTermsMatch setm;
TermProperties pv_prop;
pv_prop.d_type = 0;
for( unsigned i=0; i<d_equal_terms.size(); i++ ){
- if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_prop, sf, effort ) ){
+ if (ci->constructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf))
+ {
return true;
}
}
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();
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;
}
}
-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();
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
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;
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;
}
return Node::null();
}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
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<TermProperties>& term_props,
+ std::vector<Node>& 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<Node>& lemmas) override;
+ virtual std::string identify() const override { return "Arith"; }
+ 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);
};
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<Node>& 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<TermProperties>& term_props,
+ std::vector<Node>& 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<Node>& eqc,
+ InstEffort effort) override;
+ virtual std::string identify() const override { return "Epr"; }
+ 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);
};
-
+/** 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;
* 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
# 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
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff