diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-15 10:40:29 -0500 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-15 10:40:29 -0500 |
commit | 5d660404622a1fa35b228dd691849a64d365d677 (patch) | |
tree | 2b9b3278699d2165cfd3a317c54ad6cda78c4a13 /src | |
parent | bc936567859cf1ebae52ede50a95cdb8e31a999e (diff) |
Fix free variables in cbqi preregister inst. (#1921)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 33 |
1 files changed, 19 insertions, 14 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 2ef2563b3..df51ace2d 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1110,22 +1110,26 @@ bool CegInstantiator::check() { void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) { if( n.getKind()==FORALL || n.getKind()==EXISTS ){ //do nothing - }else{ - if( n.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] ); - if( it!=teq.end() ){ - Node nn = n[ i==0 ? 1 : 0 ]; - if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){ - it->second.push_back( nn ); - Trace("cbqi-presolve") << " - " << n[i] << " = " << nn << std::endl; - } - } + return; + } + if (n.getKind() == EQUAL) + { + for (unsigned i = 0; i < 2; i++) + { + Node nn = n[i == 0 ? 1 : 0]; + std::map<Node, std::vector<Node> >::iterator it = teq.find(n[i]); + if (it != teq.end() && !nn.hasFreeVar() + && std::find(it->second.begin(), it->second.end(), nn) + == it->second.end()) + { + it->second.push_back(nn); + Trace("cbqi-presolve") << " - " << n[i] << " = " << nn << std::endl; } } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - collectPresolveEqTerms( n[i], teq ); - } + } + for (const Node& nc : n) + { + collectPresolveEqTerms(nc, teq); } } @@ -1168,6 +1172,7 @@ void CegInstantiator::presolve( Node q ) { Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); lem = NodeManager::currentNM()->mkNode( OR, g, lem ); Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; + Assert(!lem.hasFreeVar()); d_qe->getOutputChannel().lemma( lem, false, true ); } } |