diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-01 15:29:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-01 15:29:05 -0500 |
| commit | a8c785aaadae1f5316e8e12455b362c468db4106 (patch) | |
| tree | b20875279c6d698acb7af76121244d07d47ba342 /src | |
| parent | b0fd7761fc36fc53141cb1486e9cb19dd00ae5f3 (diff) | |
Apply preprocessing to counterexample lemmas in CEGQI (#2027)
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 72633e86f..9dd0bdb04 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1475,6 +1475,9 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl; Node rlem = lems[i]; rlem = Rewriter::rewrite( rlem ); + // also must preprocess to ensure that the counterexample atoms we + // collect below are identical to the atoms that we add to the CNF stream + rlem = d_qe->getTheoryEngine()->preprocess(rlem); Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; //record the literals that imply auxiliary variables to be equal to terms if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){ @@ -1498,7 +1501,6 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st }*/ lems[i] = rlem; } - // determine variable order: must do Reals before Ints Trace("cbqi-debug") << "Determine variable order..." << std::endl; if (!d_vars.empty()) @@ -1546,7 +1548,8 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } - //collect atoms from all lemmas: we will only do bounds coming from original body + // collect atoms from all lemmas: we will only solve for literals coming from + // the original body d_is_nested_quant = false; std::map< Node, bool > visited; for( unsigned i=0; i<lems.size(); i++ ){ |