From 60f1dd27da89be80c172e15e01c49f58e0ceb6c0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 21 Nov 2017 14:02:24 -0600 Subject: [PATCH] Cegqi bv remove extract terms preprocess pass (#1376) * 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 --- src/options/quantifiers_options | 2 + src/theory/quantifiers/ceg_instantiator.cpp | 140 +++++++---- src/theory/quantifiers/ceg_instantiator.h | 94 ++++--- src/theory/quantifiers/ceg_t_instantiator.cpp | 230 +++++++++++++++--- src/theory/quantifiers/ceg_t_instantiator.h | 103 ++++++-- test/regress/regress0/quantifiers/Makefile.am | 1 + test/regress/regress0/sygus/Base16_1.sy | 34 +++ test/regress/regress0/sygus/Makefile.am | 3 +- 8 files changed, 468 insertions(+), 139 deletions(-) create mode 100644 test/regress/regress0/sygus/Base16_1.sy diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index c6dbe60c7..8106c5e5d 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -343,6 +343,8 @@ option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :defaul 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 diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index b41a3cfca..15bfbe9f9 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -33,6 +33,33 @@ namespace CVC4 { 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, @@ -41,9 +68,8 @@ CegInstantiator::CegInstantiator(QuantifiersEngine* 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) + d_effort(CEG_INST_EFFORT_NONE) { } @@ -129,6 +155,7 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index) } d_curr_subs_proc[v].clear(); d_curr_index[v] = index; + d_curr_iphase[v] = CEG_INST_PHASE_NONE; } void CegInstantiator::registerTheoryIds(TypeNode tn, @@ -161,7 +188,10 @@ void CegInstantiator::registerTheoryId(TheoryId tid) 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); } } @@ -192,6 +222,7 @@ void CegInstantiator::deactivateInstantiationVariable(Node v) { d_curr_subs_proc.erase( v ); d_curr_index.erase( v ); + d_curr_iphase.erase(v); } bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) @@ -199,7 +230,7 @@ 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; @@ -268,10 +299,11 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) } // 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; @@ -320,6 +352,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) 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 >::iterator it_reqc = d_curr_eqc.find( r ); @@ -381,6 +414,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) 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++ ){ @@ -426,11 +460,11 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) } //[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 @@ -442,11 +476,12 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) 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)) { @@ -482,13 +517,14 @@ bool CegInstantiator::constructInstantiationInc(Node pv, 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 " << 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 @@ -599,7 +635,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv, } 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; @@ -607,26 +643,28 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector 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::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[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& 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++) { @@ -1143,6 +1183,26 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st registerVariable(ce_vars[i]); } + // preprocess with all relevant instantiator preprocessors + Trace("cbqi-debug") << "Preprocess based on theory-specific methods..." + << std::endl; + std::vector pvars; + pvars.insert(pvars.end(), d_vars.begin(), d_vars.end()); + for (std::pair& 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); @@ -1181,28 +1241,6 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st lems[i] = rlem; } - // preprocess with all relevant instantiator preprocessors - Trace("cbqi-debug") << "Preprocess based on theory-specific methods..." - << std::endl; - std::vector pvars; - pvars.insert(pvars.end(), d_vars.begin(), d_vars.end()); - for (std::map::iterator it = - d_tipp.begin(); - it != d_tipp.end(); - ++it) - { - it->second->registerCounterexampleLemma(lems, pvars); - } - // must register variables generated by preprocessors - Trace("cbqi-debug") << "Register variables from theory-specific methods " - << d_num_input_variables << " " << d_vars.size() << " ..." - << std::endl; - for (unsigned i = d_num_input_variables; i < pvars.size(); i++) - { - Trace("cbqi-reg") << " register theory preprocess variable : " << pvars[i] << std::endl; - registerVariable(pvars[i]); - } - // determine variable order: must do Reals before Ints Trace("cbqi-debug") << "Determine variable order..." << std::endl; if (!d_vars.empty()) @@ -1257,7 +1295,7 @@ bool Instantiator::processEqualTerm(CegInstantiator* ci, Node pv, TermProperties& pv_prop, Node n, - InstEffort effort) + CegInstEffort effort) { pv_prop.d_type = 0; return ci->constructInstantiationInc(pv, n, pv_prop, sf); diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index bf5a37026..ab9c7ea05 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -15,8 +15,8 @@ #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" @@ -143,19 +143,47 @@ public: } }; -/** 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 @@ -357,9 +385,9 @@ class CegInstantiator { //-------------------------------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 d_vars; /** set form of d_vars */ @@ -367,10 +395,11 @@ class CegInstantiator { /** index of variables reported in instantiation */ std::vector d_var_order_index; /** number of input variables - * This is n for quantified formulas with n variables, - * and is at most the size of d_vars. + * + * 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 d_input_vars; /** literals to equalities for aux vars * This stores entries of the form * L -> ( k -> t ) @@ -416,13 +445,15 @@ class CegInstantiator { * 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 d_active_instantiators; /** map from variables to the index in the prefix of the quantified * formula we are processing. */ std::map d_curr_index; + /** map from variables to the phase in which we instantiated them */ + std::map d_curr_iphase; /** cache of current substitutions tried between activate/deactivate */ std::map > > d_curr_subs_proc; /** stack of temporary variables we are solving for, @@ -520,7 +551,7 @@ public: virtual void reset(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { } @@ -538,7 +569,7 @@ public: 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 @@ -551,7 +582,7 @@ public: SolvedForm& sf, Node pv, std::vector& eqc, - InstEffort effort) + CegInstEffort effort) { return false; } @@ -560,7 +591,7 @@ public: virtual bool hasProcessEquality(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { return false; } @@ -581,7 +612,7 @@ public: Node pv, std::vector& term_props, std::vector& terms, - InstEffort effort) + CegInstEffort effort) { return false; } @@ -590,7 +621,7 @@ public: virtual bool hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { return false; } @@ -609,8 +640,11 @@ public: * (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(); } @@ -628,7 +662,7 @@ public: Node pv, Node lit, Node alit, - InstEffort effort) + CegInstEffort effort) { return false; } @@ -643,7 +677,7 @@ public: virtual bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { return false; } @@ -655,7 +689,7 @@ public: virtual bool useModelValue(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { return false; } @@ -663,7 +697,7 @@ public: virtual bool allowModelValue(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { return d_closed_enum_type; } @@ -672,7 +706,7 @@ public: virtual bool needsPostProcessInstantiationForVariable(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { return false; } @@ -684,7 +718,7 @@ public: virtual bool postProcessInstantiationForVariable(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort, + CegInstEffort effort, std::vector& lemmas) { return true; @@ -706,7 +740,7 @@ public: bool useModelValue(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { return true; } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index d58fa2f1e..674f7c17e 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -219,7 +219,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No 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 ); @@ -238,7 +238,7 @@ bool ArithInstantiator::processEquality(CegInstantiator* ci, Node pv, std::vector& term_props, std::vector& terms, - InstEffort effort) + CegInstEffort effort) { Node eq_lhs = terms[0]; Node eq_rhs = terms[1]; @@ -276,8 +276,11 @@ bool ArithInstantiator::processEquality(CegInstantiator* ci, 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; @@ -295,7 +298,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, Node pv, Node lit, Node alit, - InstEffort effort) + CegInstEffort effort) { Node atom = lit.getKind()==NOT ? lit[0] : lit; bool pol = lit.getKind()!=NOT; @@ -415,7 +418,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, 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() ); @@ -637,7 +640,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, } 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(); } @@ -646,7 +649,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable( CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort, + CegInstEffort effort, std::vector& lemmas) { Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end() ); @@ -706,7 +709,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable( void DtInstantiator::reset(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { } @@ -755,10 +758,11 @@ bool DtInstantiator::processEqualTerms(CegInstantiator* ci, SolvedForm& sf, Node pv, std::vector& 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& term_props, std::vector& terms, - InstEffort effort) + CegInstEffort effort) { Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] ); if( !val.isNull() ){ @@ -811,7 +815,7 @@ bool DtInstantiator::processEquality(CegInstantiator* ci, void EprInstantiator::reset(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { d_equal_terms.clear(); } @@ -821,7 +825,7 @@ bool EprInstantiator::processEqualTerm(CegInstantiator* ci, Node pv, TermProperties& pv_prop, Node n, - InstEffort effort) + CegInstEffort effort) { if( options::quantEprMatching() ){ Assert( pv_prop.isBasic() ); @@ -887,7 +891,7 @@ bool EprInstantiator::processEqualTerms(CegInstantiator* ci, SolvedForm& sf, Node pv, std::vector& eqc, - InstEffort effort) + CegInstEffort effort) { if( options::quantEprMatching() ){ //heuristic for best matching constant @@ -945,7 +949,7 @@ BvInstantiator::~BvInstantiator(){ void BvInstantiator::reset(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) + CegInstEffort effort) { d_inst_id_counter = 0; d_var_to_inst_id.clear(); @@ -961,7 +965,7 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, Node pv, Node lit, Node alit, - InstEffort effort) + CegInstEffort effort) { Assert( d_inverter!=NULL ); // find path to pv @@ -991,8 +995,11 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, } } -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; @@ -1088,7 +1095,7 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, 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() ){ @@ -1109,7 +1116,7 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, 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() ){ @@ -1162,18 +1169,6 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, Trace("cegqi-bv") << " ...with slack value : " << curr_slack_val << std::endl; } - // process information about solved status - std::unordered_map::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; } @@ -1325,6 +1320,14 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, 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()); @@ -1362,6 +1365,165 @@ Node BvInstantiator::rewriteTermForSolvePv( 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 je = j.getOperator().getConst(); + 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& lems, std::vector& ce_vars) +{ + // new variables + std::vector vars; + // new lemmas + std::vector 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 > extract_map; + std::unordered_set 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 >& es : extract_map) + { + if (es.second.size() > 1) + { + // sort based on the extract start position + std::vector& 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 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(); + 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 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 >& extract_map, + std::unordered_set& visited) +{ + std::vector 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 */ diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 0242a2994..4fb954d44 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -36,11 +36,11 @@ class ArithInstantiator : public Instantiator { 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; } @@ -49,11 +49,11 @@ class ArithInstantiator : public Instantiator { Node pv, std::vector& term_props, std::vector& terms, - InstEffort effort) override; + CegInstEffort effort) override; virtual bool hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) override + CegInstEffort effort) override { return true; } @@ -61,24 +61,27 @@ class ArithInstantiator : public Instantiator { 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& lemmas) override; virtual std::string identify() const override { return "Arith"; } private: @@ -113,16 +116,16 @@ public: 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& eqc, - InstEffort effort) override; + CegInstEffort effort) override; virtual bool hasProcessEquality(CegInstantiator* ci, SolvedForm& sf, Node pv, - InstEffort effort) override + CegInstEffort effort) override { return true; } @@ -131,7 +134,7 @@ public: Node pv, std::vector& term_props, std::vector& 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); @@ -146,18 +149,18 @@ class EprInstantiator : public Instantiator { 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& eqc, - InstEffort effort) override; + CegInstEffort effort) override; virtual std::string identify() const override { return "Epr"; } private: std::vector d_equal_terms; @@ -188,11 +191,11 @@ class BvInstantiator : public Instantiator { 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; } @@ -200,21 +203,21 @@ class BvInstantiator : public Instantiator { 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; } @@ -262,7 +265,61 @@ class BvInstantiator : public Instantiator { 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& lems, + std::vector& 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 >& extract_map, + std::unordered_set& visited); }; } /* CVC4::theory::quantifiers namespace */ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 274dcaff0..c59570651 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -115,6 +115,7 @@ TESTS = \ 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 \ diff --git a/test/regress/regress0/sygus/Base16_1.sy b/test/regress/regress0/sygus/Base16_1.sy new file mode 100644 index 000000000..5833751cb --- /dev/null +++ b/test/regress/regress0/sygus/Base16_1.sy @@ -0,0 +1,34 @@ +; 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) + + diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index b40ee845f..82c2c2458 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -70,7 +70,8 @@ TESTS = commutative.sy \ 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 -- 2.30.2