diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 13:35:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 13:35:07 -0500 |
commit | 13e452be03bef09e2f54f42e2bc42383505ffcea (patch) | |
tree | 39695fe22d387bc84bc49d20831a19648d55011f /src/theory/quantifiers/ceg_instantiator.cpp | |
parent | be11fae39055f213586058ec9129d1276f724b0e (diff) |
CBQI BV choice expressions (#1296)
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.
* Minor
* Make unique bound variables for choice functions in BvInstantor, clean up.
* Incorporate missing optimizations
* Clang format
* Unused field.
* Minor
* Fix, add regression.
* Fix regression.
* Fix bug that led to incorrect cleanup of instantiations.
* Add missing regression
* Improve handling of choice rewriting.
* Fix
* Clang format
* Use canonical variables for choice functions in cbqi bv.
* Add regression
* Clang format.
* Address review.
* Clang format
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.cpp')
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 67 |
1 files changed, 53 insertions, 14 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 57bfb2d14..e7749cd92 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -46,24 +46,35 @@ CegInstantiator::~CegInstantiator() { void CegInstantiator::computeProgVars( Node n ){ if( d_prog_var.find( n )==d_prog_var.end() ){ d_prog_var[n].clear(); - if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){ - d_prog_var[n][n] = true; + if (n.getKind() == kind::CHOICE) + { + Assert(d_prog_var.find(n[0][0]) == d_prog_var.end()); + d_prog_var[n[0][0]].clear(); + } + if (d_vars_set.find(n) != d_vars_set.end()) + { + d_prog_var[n].insert(n); }else if( !d_out->isEligibleForInstantiation( n ) ){ - d_inelig[n] = true; + d_inelig.insert(n); return; } for( unsigned i=0; i<n.getNumChildren(); i++ ){ computeProgVars( n[i] ); if( d_inelig.find( n[i] )!=d_inelig.end() ){ - d_inelig[n] = true; - } - for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){ - d_prog_var[n][it->first] = true; - } - //selectors applied to program variables are also variables - if( n.getKind()==APPLY_SELECTOR_TOTAL && d_prog_var[n].find( n[0] )!=d_prog_var[n].end() ){ - d_prog_var[n][n] = true; + d_inelig.insert(n); } + // all variables in child are contained in this + d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end()); + } + // selectors applied to program variables are also variables + if (n.getKind() == APPLY_SELECTOR_TOTAL + && d_prog_var[n].find(n[0]) != d_prog_var[n].end()) + { + d_prog_var[n].insert(n); + } + if (n.getKind() == kind::CHOICE) + { + d_prog_var.erase(n[0][0]); } } } @@ -113,7 +124,8 @@ void CegInstantiator::unregisterInstantiationVariable( Node v ) { bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){ if( i==d_vars.size() ){ //solved for all variables, now construct instantiation - bool needsPostprocess = false; + bool needsPostprocess = + sf.d_vars.size() > d_vars.size() || !d_var_order_index.empty(); std::vector< Instantiator * > pp_inst; std::map< Instantiator *, Node > pp_inst_to_var; std::vector< Node > lemmas; @@ -522,8 +534,13 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){ Assert( d_prog_var.find( n )!=d_prog_var.end() ); if( !non_basic.empty() ){ - for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){ - if( std::find( non_basic.begin(), non_basic.end(), it->first )!=non_basic.end() ){ + for (std::unordered_set<Node, NodeHashFunction>::iterator it = + d_prog_var[n].begin(); + it != d_prog_var[n].end(); + ++it) + { + if (std::find(non_basic.begin(), non_basic.end(), *it) != non_basic.end()) + { return false; } } @@ -699,6 +716,7 @@ bool CegInstantiator::check() { for( unsigned r=0; r<2; r++ ){ SolvedForm sf; d_stack_vars.clear(); + d_bound_var_index.clear(); //try to add an instantiation if( doAddInstantiation( sf, 0, r==0 ? 0 : 2 ) ){ return true; @@ -979,6 +997,26 @@ Node CegInstantiator::getModelValue( Node n ) { return d_qe->getModel()->getValue( n ); } +Node CegInstantiator::getBoundVariable(TypeNode tn) +{ + unsigned index = 0; + std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>::iterator itb = + d_bound_var_index.find(tn); + if (itb != d_bound_var_index.end()) + { + index = itb->second; + } + d_bound_var_index[tn] = index + 1; + while (index >= d_bound_var[tn].size()) + { + std::stringstream ss; + ss << "x" << index; + Node x = NodeManager::currentNM()->mkBoundVar(ss.str(), tn); + d_bound_var[tn].push_back(x); + } + return d_bound_var[tn][index]; +} + void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { if( n.getKind()==FORALL ){ d_is_nested_quant = true; @@ -1010,6 +1048,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st //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() ){ |