diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-12 18:48:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-12 18:48:27 -0500 |
| commit | 51cab64a53daee8e6f2693f12911c71827013f15 (patch) | |
| tree | db037aaeee3d2c7d15b6395394e5df7ae47af4b7 /src/theory/quantifiers/ceg_instantiator.cpp | |
| parent | b0d151fc69779c9e214d89683e005756a9834c2e (diff) | |
Initial infrastructure for BV instantiation via word-level inversions. (#1056)
* Initial infrastructure for BV instantiation via word-level inversions.
* Minor clean up.
* Change visited to unordered set.
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.cpp')
| -rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 05e86c9e8..db283ccfc 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -11,7 +11,7 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation **/ - + #include "theory/quantifiers/ceg_instantiator.h" #include "theory/quantifiers/ceg_t_instantiator.h" @@ -131,7 +131,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e postProcessSuccess = false; break; } - } + } if( postProcessSuccess ){ return doAddInstantiation( sf_tmp.d_subs, sf_tmp.d_vars ); }else{ @@ -294,9 +294,13 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e Node lit = ita->second[j]; if( std::find( lits.begin(), lits.end(), lit )==lits.end() ){ lits.push_back( lit ); - if( vinst->processAssertion( this, sf, pv, lit, effort ) ){ - return true; - } + //if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){ + // apply substitutions check if eligible and contains pv + // TODO + if( vinst->processAssertion( this, sf, pv, lit, effort ) ){ + return true; + } + //} } } } @@ -326,7 +330,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e } } Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; - if( is_cv ){ + if( is_cv ){ d_stack_vars.push_back( pv ); } d_active_instantiators.erase( pv ); @@ -509,7 +513,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) ); } } - + if( !req_coeff ){ Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); if( n!=nret ){ @@ -995,7 +999,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st Node v = lems[i][0]; d_aux_eq[rlem][v] = lems[i][1]; Trace("cbqi-debug") << " " << rlem << " implies " << v << " = " << lems[i][1] << std::endl; - } + } }*/ lems[i] = rlem; } |