* Preprocess extract -> concat pass for cegqi bv.
* Add sygus bench
* Fixes, infrastructure.
* Minor fixes.
* Try
* Minor
* Minor
* Document
* Format
* Improving debug messages.
* Address
* Format
* Overlapping extracts.
* Format
* Minor
* Address review.
* Format
* Comment
* Format
interleave model value instantiation with word-level inversion approach
option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode
choose mode for handling bit-vector inequalities with counterexample-guided instantiation
+option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default false
+ replaces extract terms with variables for counterexample-guided instantiation for bit-vectors
### local theory extensions options
namespace theory {
namespace quantifiers {
+std::ostream& operator<<(std::ostream& os, CegInstEffort e)
+{
+ switch (e)
+ {
+ case CEG_INST_EFFORT_NONE: os << "?"; break;
+ case CEG_INST_EFFORT_STANDARD: os << "STANDARD"; break;
+ case CEG_INST_EFFORT_STANDARD_MV: os << "STANDARD_MV"; break;
+ case CEG_INST_EFFORT_FULL: os << "FULL"; break;
+ default: Unreachable();
+ }
+ return os;
+}
+
+std::ostream& operator<<(std::ostream& os, CegInstPhase phase)
+{
+ switch (phase)
+ {
+ case CEG_INST_PHASE_NONE: os << "?"; break;
+ case CEG_INST_PHASE_EQC: os << "eqc"; break;
+ case CEG_INST_PHASE_EQUAL: os << "eq"; break;
+ case CEG_INST_PHASE_ASSERTION: os << "as"; break;
+ case CEG_INST_PHASE_MVALUE: os << "mv"; break;
+ default: Unreachable();
+ }
+ return os;
+}
+
CegInstantiator::CegInstantiator(QuantifiersEngine* qe,
CegqiOutput* out,
bool use_vts_delta,
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)
+ d_effort(CEG_INST_EFFORT_NONE)
{
}
}
d_curr_subs_proc[v].clear();
d_curr_index[v] = index;
+ d_curr_iphase[v] = CEG_INST_PHASE_NONE;
}
void CegInstantiator::registerTheoryIds(TypeNode tn,
if (std::find(d_tids.begin(), d_tids.end(), tid) == d_tids.end())
{
// setup any theory-specific preprocessors here
-
+ if (tid == THEORY_BV)
+ {
+ d_tipp[tid] = new BvInstantiatorPreprocess;
+ }
d_tids.push_back(tid);
}
}
{
d_curr_subs_proc.erase( v );
d_curr_index.erase( v );
+ d_curr_iphase.erase(v);
}
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_num_input_variables || !d_var_order_index.empty();
+ sf.d_vars.size() > d_input_vars.size() || !d_var_order_index.empty();
std::vector< Instantiator * > pp_inst;
std::map< Instantiator *, Node > pp_inst_to_var;
std::vector< Node > lemmas;
}
// if d_effort is full, we must choose at least one model value
- if ((i + 1) < d_vars.size() || d_effort != INST_EFFORT_FULL)
+ if ((i + 1) < d_vars.size() || d_effort != CEG_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;
+ d_curr_iphase[pv] = CEG_INST_PHASE_EQC;
std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
if( it_eqc!=d_curr_eqc.end() ){
//std::vector< Node > eq_candidates;
if (vinst->hasProcessEquality(this, sf, pv, d_effort))
{
Trace("cbqi-inst-debug") << "[2] try based on solving equalities." << std::endl;
+ d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL;
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 );
if (vinst->hasProcessAssertion(this, sf, pv, d_effort))
{
Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
+ d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION;
std::unordered_set< Node, NodeHashFunction > lits;
//unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
for( unsigned r=0; r<2; r++ ){
}
//[4] resort to using value in model. We do so if:
- // - we are in a higher effort than INST_EFFORT_STANDARD,
+ // - we are in a higher effort than CEG_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)
+ if ((d_effort > CEG_INST_EFFORT_STANDARD || use_model_value || is_cv)
&& vinst->allowModelValue(this, sf, pv, d_effort))
{
#ifdef CVC4_ASSERTIONS
Node mv = getModelValue( pv );
TermProperties pv_prop_m;
Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
- InstEffort prev = d_effort;
+ d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE;
+ CegInstEffort 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;
+ d_effort = CEG_INST_EFFORT_STANDARD_MV;
}
if (constructInstantiationInc(pv, mv, pv_prop_m, sf))
{
Node cnode = pv_prop.getCacheNode();
if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
d_curr_subs_proc[pv][n][cnode] = true;
- if( Trace.isOn("cbqi-inst") ){
+ if( Trace.isOn("cbqi-inst-debug") ){
for( unsigned j=0; j<sf.d_subs.size(); j++ ){
- Trace("cbqi-inst") << " ";
+ Trace("cbqi-inst-debug") << " ";
}
- Trace("cbqi-inst") << sf.d_subs.size() << ": ";
+ Trace("cbqi-inst-debug") << sf.d_subs.size() << ": (" << d_curr_iphase[pv]
+ << ") ";
Node mod_pv = pv_prop.getModifiedTerm( pv );
- Trace("cbqi-inst") << mod_pv << " -> " << n << std::endl;
+ Trace("cbqi-inst-debug") << mod_pv << " -> " << n << std::endl;
Assert( n.getType().isSubtypeOf( pv.getType() ) );
}
//must ensure variables have been computed for n
}
bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) {
- if (vars.size() > d_num_input_variables)
+ if (vars.size() > d_input_vars.size() || !d_var_order_index.empty())
{
Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
std::map< Node, Node > subs_map;
subs_map[vars[i]] = subs[i];
}
subs.clear();
- for (unsigned i = 0; i < d_vars.size(); i++)
+ for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
{
- std::map< Node, Node >::iterator it = subs_map.find( d_vars[i] );
+ std::map<Node, Node>::iterator it = subs_map.find(d_input_vars[i]);
Assert( it!=subs_map.end() );
Node n = it->second;
- Trace("cbqi-inst-debug") << " " << d_vars[i] << " -> " << n << std::endl;
+ Trace("cbqi-inst-debug") << " " << d_input_vars[i] << " -> " << n
+ << std::endl;
+ Assert(n.getType().isSubtypeOf(d_input_vars[i].getType()));
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]] );
+ if (Trace.isOn("cbqi-inst"))
+ {
+ Trace("cbqi-inst") << "Ceg Instantiator produced : " << std::endl;
+ for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
+ {
+ Node v = d_input_vars[i];
+ Trace("cbqi-inst") << i << " (" << d_curr_iphase[v] << ") : "
+ << v << " -> " << subs[i] << std::endl;
+ Assert(subs[i].getType().isSubtypeOf(v.getType()));
}
}
- 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++ ){
}
processAssertions();
for( unsigned r=0; r<2; r++ ){
- d_effort = r == 0 ? INST_EFFORT_STANDARD : INST_EFFORT_FULL;
+ d_effort = r == 0 ? CEG_INST_EFFORT_STANDARD : CEG_INST_EFFORT_FULL;
SolvedForm sf;
d_stack_vars.clear();
d_bound_var_index.clear();
void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl;
+ d_input_vars.clear();
+ d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end());
+
//Assert( d_vars.empty() );
d_vars.clear();
- d_num_input_variables = ce_vars.size();
registerTheoryId(THEORY_UF);
for (unsigned i = 0; i < ce_vars.size(); i++)
{
registerVariable(ce_vars[i]);
}
+ // 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::pair<const TheoryId, InstantiatorPreprocess*>& p : d_tipp)
+ {
+ p.second->registerCounterexampleLemma(lems, pvars);
+ }
+ // must register variables generated by preprocessors
+ Trace("cbqi-debug") << "Register variables from theory-specific methods "
+ << d_input_vars.size() << " " << pvars.size() << " ..."
+ << std::endl;
+ for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i)
+ {
+ Trace("cbqi-reg") << " register theory preprocess variable : " << pvars[i]
+ << std::endl;
+ registerVariable(pvars[i]);
+ }
+
//remove ITEs
IteSkolemMap iteSkolemMap;
d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
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())
Node pv,
TermProperties& pv_prop,
Node n,
- InstEffort effort)
+ CegInstEffort effort)
{
pv_prop.d_type = 0;
return ci->constructInstantiationInc(pv, n, pv_prop, sf);
#include "cvc4_private.h"
-#ifndef __CVC4__CEG_INSTANTIATOR_H
-#define __CVC4__CEG_INSTANTIATOR_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
#include "theory/quantifiers_engine.h"
#include "util/statistics_registry.h"
}
};
-/** instantiation effort levels */
-enum InstEffort
+/** instantiation effort levels
+ *
+ * This effort is used to stratify the construction of
+ * instantiations for some theories that may result to
+ * using model value instantiations.
+ */
+enum CegInstEffort
{
// uninitialized
- INST_EFFORT_NONE,
+ CEG_INST_EFFORT_NONE,
// standard effort level
- INST_EFFORT_STANDARD,
+ CEG_INST_EFFORT_STANDARD,
// standard effort level, but we have used model values
- INST_EFFORT_STANDARD_MV,
+ CEG_INST_EFFORT_STANDARD_MV,
// full effort level
- INST_EFFORT_FULL
+ CEG_INST_EFFORT_FULL
+};
+
+std::ostream& operator<<(std::ostream& os, CegInstEffort e);
+
+/** instantiation phase for variables
+ *
+ * This indicates the phase in which we constructed
+ * a substitution for individual variables.
+ */
+enum CegInstPhase
+{
+ // uninitialized
+ CEG_INST_PHASE_NONE,
+ // instantiation constructed during traversal of equivalence classes
+ CEG_INST_PHASE_EQC,
+ // instantiation constructed during solving equalities
+ CEG_INST_PHASE_EQUAL,
+ // instantiation constructed by looking at theory assertions
+ CEG_INST_PHASE_ASSERTION,
+ // instantiation constructed by querying model value
+ CEG_INST_PHASE_MVALUE,
};
+std::ostream& operator<<(std::ostream& os, CegInstPhase phase);
+
/** Ceg instantiator
*
* This class manages counterexample-guided quantifier instantiation
//-------------------------------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.
+ *
+ * This is a superset of the variables for the instantiations we are
+ * generating and sending on the output channel of this class.
*/
std::vector<Node> d_vars;
/** set form of d_vars */
/** 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.
+ *
+ * These are the variables, in order, for the instantiations we are generating
+ * and sending on the output channel of this class.
*/
- unsigned d_num_input_variables;
+ std::vector<Node> d_input_vars;
/** literals to equalities for aux vars
* This stores entries of the form
* L -> ( k -> t )
* This indicates the effort Instantiator objects
* will put into the terms they return.
*/
- InstEffort d_effort;
+ CegInstEffort d_effort;
/** for each variable, the instantiator used for that variable */
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;
+ /** map from variables to the phase in which we instantiated them */
+ std::map<Node, CegInstPhase> d_curr_iphase;
/** 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,
virtual void reset(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
}
Node pv,
TermProperties& pv_prop,
Node n,
- InstEffort effort);
+ CegInstEffort effort);
/** process equal terms
*
* This method is called after process equal term, where eqc is the list of
SolvedForm& sf,
Node pv,
std::vector<Node>& eqc,
- InstEffort effort)
+ CegInstEffort effort)
{
return false;
}
virtual bool hasProcessEquality(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
return false;
}
Node pv,
std::vector<TermProperties>& term_props,
std::vector<Node>& terms,
- InstEffort effort)
+ CegInstEffort effort)
{
return false;
}
virtual bool hasProcessAssertion(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
return false;
}
* (2) lit' implies lit.
* where typically lit' = lit.
*/
- virtual Node hasProcessAssertion(
- CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort)
+ virtual Node hasProcessAssertion(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ Node lit,
+ CegInstEffort effort)
{
return Node::null();
}
Node pv,
Node lit,
Node alit,
- InstEffort effort)
+ CegInstEffort effort)
{
return false;
}
virtual bool processAssertions(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
return false;
}
virtual bool useModelValue(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
return false;
}
virtual bool allowModelValue(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
return d_closed_enum_type;
}
virtual bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
return false;
}
virtual bool postProcessInstantiationForVariable(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort,
+ CegInstEffort effort,
std::vector<Node>& lemmas)
{
return true;
bool useModelValue(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
return true;
}
void ArithInstantiator::reset(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type, false, false );
d_vts_sym[1] = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta( false, false );
Node pv,
std::vector<TermProperties>& term_props,
std::vector<Node>& terms,
- InstEffort effort)
+ CegInstEffort effort)
{
Node eq_lhs = terms[0];
Node eq_rhs = terms[1];
return false;
}
-Node ArithInstantiator::hasProcessAssertion(
- CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort)
+Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ Node lit,
+ CegInstEffort effort)
{
Node atom = lit.getKind()==NOT ? lit[0] : lit;
bool pol = lit.getKind()!=NOT;
Node pv,
Node lit,
Node alit,
- InstEffort effort)
+ CegInstEffort effort)
{
Node atom = lit.getKind()==NOT ? lit[0] : lit;
bool pol = lit.getKind()!=NOT;
bool ArithInstantiator::processAssertions(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
if (options::cbqiModel()) {
bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() );
}
bool ArithInstantiator::needsPostProcessInstantiationForVariable(
- CegInstantiator* ci, SolvedForm& sf, Node pv, InstEffort effort)
+ CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort)
{
return std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end();
}
CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort,
+ CegInstEffort effort,
std::vector<Node>& lemmas)
{
Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end() );
void DtInstantiator::reset(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
}
SolvedForm& sf,
Node pv,
std::vector<Node>& eqc,
- InstEffort effort)
+ CegInstEffort effort)
{
- Trace("cegqi-dt-debug") << "[2] try based on constructors in equivalence class." << std::endl;
- //[2] look in equivalence class for a constructor
+ Trace("cegqi-dt-debug") << "try based on constructors in equivalence class."
+ << std::endl;
+ // look in equivalence class for a constructor
for( unsigned k=0; k<eqc.size(); k++ ){
Node n = eqc[k];
if( n.getKind()==APPLY_CONSTRUCTOR ){
Node pv,
std::vector<TermProperties>& term_props,
std::vector<Node>& terms,
- InstEffort effort)
+ CegInstEffort effort)
{
Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] );
if( !val.isNull() ){
void EprInstantiator::reset(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
d_equal_terms.clear();
}
Node pv,
TermProperties& pv_prop,
Node n,
- InstEffort effort)
+ CegInstEffort effort)
{
if( options::quantEprMatching() ){
Assert( pv_prop.isBasic() );
SolvedForm& sf,
Node pv,
std::vector<Node>& eqc,
- InstEffort effort)
+ CegInstEffort effort)
{
if( options::quantEprMatching() ){
//heuristic for best matching constant
void BvInstantiator::reset(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort effort)
{
d_inst_id_counter = 0;
d_var_to_inst_id.clear();
Node pv,
Node lit,
Node alit,
- InstEffort effort)
+ CegInstEffort effort)
{
Assert( d_inverter!=NULL );
// find path to pv
}
}
-Node BvInstantiator::hasProcessAssertion(
- CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort)
+Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ Node lit,
+ CegInstEffort effort)
{
Node atom = lit.getKind() == NOT ? lit[0] : lit;
bool pol = lit.getKind() != NOT;
Node pv,
Node lit,
Node alit,
- InstEffort effort)
+ CegInstEffort effort)
{
// if option enabled, use approach for word-level inversion for BV instantiation
if( options::cbqiBv() ){
bool BvInstantiator::processAssertions(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort)
+ CegInstEffort 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") << " ...with slack value : " << curr_slack_val
<< std::endl;
}
- // process information about solved status
- std::unordered_map<unsigned, BvInverterStatus>::iterator its =
- d_inst_id_to_status.find(inst_id);
- Assert(its != d_inst_id_to_status.end());
- if (!its->second.d_conds.empty()) {
- Trace("cegqi-bv") << " ...with " << its->second.d_conds.size()
- << " side conditions : " << std::endl;
- for (unsigned k = 0; k < its->second.d_conds.size(); k++) {
- Node cond = its->second.d_conds[k];
- Trace("cegqi-bv") << " " << cond << std::endl;
- }
- }
Trace("cegqi-bv") << std::endl;
}
visited.top()[cur] = ret;
}
+ else if (Trace.isOn("cegqi-bv-nl"))
+ {
+ if (cur == pv)
+ {
+ Trace("cegqi-bv-nl") << "NONLINEAR LITERAL for " << pv << " : " << lit
+ << std::endl;
+ }
+ }
} while (!visit.top().empty());
Assert(visited.size() == 1);
Assert(visited.top().find(lit) != visited.top().end());
return Node::null();
}
+/** sort bv extract interval
+ *
+ * This sorts lists of bitvector extract terms where
+ * ((_ extract i1 i2) t) < ((_ extract j1 j2) t)
+ * if i1>j1 or i1=j1 and i2>j2.
+ */
+struct SortBvExtractInterval
+{
+ bool operator()(Node i, Node j)
+ {
+ Assert(i.getKind() == BITVECTOR_EXTRACT);
+ Assert(j.getKind() == BITVECTOR_EXTRACT);
+ BitVectorExtract ie = i.getOperator().getConst<BitVectorExtract>();
+ BitVectorExtract je = j.getOperator().getConst<BitVectorExtract>();
+ if (ie.high > je.high)
+ {
+ return true;
+ }
+ else if (ie.high == je.high)
+ {
+ Assert(ie.low != je.low);
+ return ie.low > je.low;
+ }
+ return false;
+ }
+};
+
+void BvInstantiatorPreprocess::registerCounterexampleLemma(
+ std::vector<Node>& lems, std::vector<Node>& ce_vars)
+{
+ // new variables
+ std::vector<Node> vars;
+ // new lemmas
+ std::vector<Node> new_lems;
+
+ if (options::cbqiBvRmExtract())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
+ // map from terms to bitvector extracts applied to that term
+ std::map<Node, std::vector<Node> > extract_map;
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ for (unsigned i = 0, size = lems.size(); i < size; i++)
+ {
+ Trace("cegqi-bv-pp-debug2") << "Register ce lemma # " << i << " : "
+ << lems[i] << std::endl;
+ collectExtracts(lems[i], extract_map, visited);
+ }
+ for (std::pair<const Node, std::vector<Node> >& es : extract_map)
+ {
+ if (es.second.size() > 1)
+ {
+ // sort based on the extract start position
+ std::vector<Node>& curr_vec = es.second;
+
+ SortBvExtractInterval sbei;
+ std::sort(curr_vec.begin(), curr_vec.end(), sbei);
+
+ unsigned width = es.first.getType().getBitVectorSize();
+
+ // list of points b such that:
+ // b>0 and we must start a segment at (b-1) or b==0
+ std::vector<unsigned> boundaries;
+ boundaries.push_back(width);
+ boundaries.push_back(0);
+
+ Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl;
+ for (unsigned i = 0, size = curr_vec.size(); i < size; i++)
+ {
+ Trace("cegqi-bv-pp") << " " << i << " : " << curr_vec[i]
+ << std::endl;
+ BitVectorExtract e =
+ curr_vec[i].getOperator().getConst<BitVectorExtract>();
+ if (std::find(boundaries.begin(), boundaries.end(), e.high + 1)
+ == boundaries.end())
+ {
+ boundaries.push_back(e.high + 1);
+ }
+ if (std::find(boundaries.begin(), boundaries.end(), e.low)
+ == boundaries.end())
+ {
+ boundaries.push_back(e.low);
+ }
+ }
+ std::sort(boundaries.rbegin(), boundaries.rend());
+
+ // make the extract variables
+ std::vector<Node> children;
+ for (unsigned i = 1; i < boundaries.size(); i++)
+ {
+ Assert(boundaries[i - 1] > 0);
+ Node ex = bv::utils::mkExtract(
+ es.first, boundaries[i - 1] - 1, boundaries[i]);
+ Node var =
+ nm->mkSkolem("ek",
+ ex.getType(),
+ "variable to represent disjoint extract region");
+ Node ceq_lem = var.eqNode(ex);
+ Trace("cegqi-bv-pp") << "Introduced : " << ceq_lem << std::endl;
+ new_lems.push_back(ceq_lem);
+ children.push_back(var);
+ vars.push_back(var);
+ }
+
+ Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children);
+ Assert(conc.getType() == es.first.getType());
+ Node eq_lem = conc.eqNode(es.first);
+ Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl;
+ new_lems.push_back(eq_lem);
+ }
+ Trace("cegqi-bv-pp") << "...finished processing extracts for term "
+ << es.first << std::endl;
+ }
+ Trace("cegqi-bv-pp") << "-----done remove extracts" << std::endl;
+ }
+
+ if (!vars.empty())
+ {
+ // could try applying subs -> vars here
+ // in practice, this led to worse performance
+
+ Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..."
+ << std::endl;
+ lems.insert(lems.end(), new_lems.begin(), new_lems.end());
+ Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..."
+ << std::endl;
+ ce_vars.insert(ce_vars.end(), vars.begin(), vars.end());
+ }
+}
+
+void BvInstantiatorPreprocess::collectExtracts(
+ Node lem,
+ std::map<Node, std::vector<Node> >& extract_map,
+ std::unordered_set<TNode, TNodeHashFunction>& visited)
+{
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(lem);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ if (visited.find(cur) == visited.end())
+ {
+ visited.insert(cur);
+
+ if (cur.getKind() == BITVECTOR_EXTRACT)
+ {
+ extract_map[cur[0]].push_back(cur);
+ }
+
+ for (const Node& nc : cur)
+ {
+ visit.push_back(nc);
+ }
+ }
+ } while (!visit.empty());
+}
+
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
virtual void reset(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool hasProcessEquality(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override
+ CegInstEffort effort) override
{
return true;
}
Node pv,
std::vector<TermProperties>& term_props,
std::vector<Node>& terms,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool hasProcessAssertion(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override
+ CegInstEffort effort) override
{
return true;
}
SolvedForm& sf,
Node pv,
Node lit,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool processAssertion(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
Node lit,
Node alit,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool processAssertions(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool needsPostProcessInstantiationForVariable(
- CegInstantiator* ci, SolvedForm& sf, Node pv, InstEffort effort) override;
+ CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override;
virtual bool postProcessInstantiationForVariable(
CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort,
+ CegInstEffort effort,
std::vector<Node>& lemmas) override;
virtual std::string identify() const override { return "Arith"; }
private:
virtual void reset(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool processEqualTerms(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
std::vector<Node>& eqc,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool hasProcessEquality(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override
+ CegInstEffort effort) override
{
return true;
}
Node pv,
std::vector<TermProperties>& term_props,
std::vector<Node>& terms,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual std::string identify() const override { return "Dt"; }
private:
Node solve_dt(Node v, Node a, Node b, Node sa, Node sb);
virtual void reset(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool processEqualTerm(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
TermProperties& pv_prop,
Node n,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool processEqualTerms(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
std::vector<Node>& eqc,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual std::string identify() const override { return "Epr"; }
private:
std::vector<Node> d_equal_terms;
virtual void reset(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool hasProcessAssertion(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override
+ CegInstEffort effort) override
{
return true;
}
SolvedForm& sf,
Node pv,
Node lit,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool processAssertion(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
Node lit,
Node alit,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool processAssertions(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override;
+ CegInstEffort effort) override;
virtual bool useModelValue(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- InstEffort effort) override
+ CegInstEffort effort) override
{
return true;
}
Node pv,
Node lit,
Node alit,
- InstEffort effort);
+ CegInstEffort effort);
+};
+
+/** Bitvector instantiator preprocess
+ *
+ * This class implements preprocess techniques that are helpful for
+ * counterexample-guided instantiation, such as introducing variables
+ * that refer to disjoint bit-vector extracts.
+ */
+class BvInstantiatorPreprocess : public InstantiatorPreprocess
+{
+ public:
+ BvInstantiatorPreprocess() {}
+ virtual ~BvInstantiatorPreprocess() {}
+ /** register counterexample lemma
+ *
+ * This method modifies the contents of lems based on removing extract terms
+ * when the option --cbqi-bv-rm-extract is enabled.
+ *
+ * For example:
+ * P[ ((extract 7 4) t), ((extract 3 0) t)]
+ * becomes:
+ * P[((extract 7 4) t), ((extract 3 0) t)] ^
+ * t = concat( x74, x30 ) ^
+ * x74 = ((extract 7 4) t) ^
+ * x30 = ((extract 3 0) t)
+ * where x74 and x30 are fresh variables.
+ *
+ * Another example:
+ * P[ ((extract 7 3) t), ((extract 4 0) t)]
+ * becomes:
+ * P[((extract 7 4) t), ((extract 3 0) t)] ^
+ * t = concat( x75, x44, x30 ) ^
+ * x75 = ((extract 7 5) t) ^
+ * x44 = ((extract 4 4) t) ^
+ * x30 = ((extract 3 0) t)
+ * where x75, x44 and x30 are fresh variables.
+ *
+ * Notice we leave the original conjecture alone. This is done for performance
+ * since the added equalities ensure we are able to construct the proper
+ * solved forms for variables in t and for the intermediate variables above.
+ */
+ virtual void registerCounterexampleLemma(std::vector<Node>& lems,
+ std::vector<Node>& ce_vars) override;
+
+ private:
+ /** collect extracts
+ *
+ * This method collects all extract terms in lem
+ * and stores them in d_extract_map.
+ * visited is the terms we've already visited.
+ */
+ void collectExtracts(Node lem,
+ std::map<Node, std::vector<Node> >& extract_map,
+ std::unordered_set<TNode, TNodeHashFunction>& visited);
};
} /* CVC4::theory::quantifiers namespace */
NUM878.smt2 \
psyco-107-bv.smt2 \
ari118-bv-2occ-x.smt2 \
+ extract-nproc.smt2 \
javafe.ast.StandardPrettyPrint.319.smt2 \
javafe.ast.StmtVec.009.smt2 \
javafe.ast.WhileStmt.447.smt2 \
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-qe-preproc --cbqi-bv-rm-extract --sygus-out=status --cbqi-bv --cegqi-si=all
+(set-logic BV)
+
+(define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l))))
+
+(define-fun E ((x (BitVec 8))) (BitVec 8) (bvadd x #x41))
+
+(define-fun f ((x (BitVec 8))) (BitVec 8) (bvsub x #x41))
+
+(define-fun d ((x (BitVec 8))) Bool (bvule x #x3f))
+
+(synth-fun D ((x (BitVec 8)) (y (BitVec 8)) ) (BitVec 8)
+ ((Start (BitVec 8) (
+ (f Start) x y Const
+ (bvshl Start Start) (bvnot Start)
+ (bvand Start Start)
+ (bvxor Start Start)
+ (bvor Start Start)
+ (bvneg Start)
+ (bvadd Start Start)
+ (bvlshr Start Start)
+ (bvsub Start Start)
+ ))
+ (Const (BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00))
+))
+
+(declare-var x (BitVec 8))
+(constraint (= x (D (E (B #x07 #x04 x) ) (E (B #x03 #x00 x)) )) )
+
+; notice we don't have solution reconstruction for this
+(check-synth)
+
+
process-10-vars.sy \
process-10-vars-2fun.sy \
inv-unused.sy \
- ccp16.lus.sy
+ ccp16.lus.sy \
+ Base16_1.sy
# sygus tests currently taking too long for make regress
projects / cvc5.git / commitdiff