diff options
author | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
---|---|---|
committer | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
commit | 36a0d1d948f201471596e092136c5a00103f78af (patch) | |
tree | 7a9b0d79074da1cb0c1cbed986584d50792a30e9 /src/theory/quantifiers/inst_propagator.cpp | |
parent | 66525e81928d0d025dbcc197ab3ef772eac31103 (diff) | |
parent | a58abbe71fb1fc07129ff9c7568ac544145fb57c (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4.git
Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy
Diffstat (limited to 'src/theory/quantifiers/inst_propagator.cpp')
-rwxr-xr-x[-rw-r--r--] | src/theory/quantifiers/inst_propagator.cpp | 476 |
1 files changed, 280 insertions, 196 deletions
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index d4be58636..41c9c40c8 100644..100755 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -34,6 +34,7 @@ bool EqualityQueryInstProp::reset( Theory::Effort e ) { d_uf.clear(); d_uf_exp.clear(); d_diseq_list.clear(); + d_uf_func_map_trie.clear(); return true; } @@ -103,8 +104,7 @@ TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& arg if( !t.isNull() ){ return t; }else{ - //TODO? - return TNode::null(); + return d_uf_func_map_trie[f].existsTerm( args ); } } @@ -118,6 +118,7 @@ Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& e Node ar = getUfRepresentative( a, exp ); if( !ar.isNull() ){ if( engine_has_a || getEngine()->hasTerm( ar ) ){ + Trace("qip-eq") << "getRepresentativeExp " << a << " returns " << ar << std::endl; Assert( getEngine()->hasTerm( ar ) ); Assert( getEngine()->getRepresentative( ar )==ar ); return ar; @@ -168,6 +169,21 @@ bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& } } +TNode EqualityQueryInstProp::getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp ) { + TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args ); + if( !t.isNull() ){ + return t; + }else{ + TNode tt = d_uf_func_map_trie[f].existsTerm( args ); + if( !tt.isNull() ){ + //TODO? + return tt; + }else{ + return tt; + } + } +} + Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) { Assert( exp.empty() ); std::map< Node, Node >::iterator it = d_uf.find( a ); @@ -252,7 +268,7 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No } } } - + if( swap ){ //swap Node temp_r = ar; @@ -262,7 +278,7 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) ); Assert( ar!=br ); - + std::vector< Node > exp_d; if( areDisequalExp( ar, br, exp_d ) ){ if( pol ){ @@ -279,18 +295,20 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No Assert( d_uf_exp[ar].empty() ); Assert( d_uf_exp[br].empty() ); + //registerUfTerm( ar ); d_uf[ar] = br; merge_exp( d_uf_exp[ar], exp_a ); merge_exp( d_uf_exp[ar], exp_b ); merge_exp( d_uf_exp[ar], reason ); + //registerUfTerm( br ); d_uf[br] = br; d_uf_exp[br].clear(); Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl; a = ar; b = br; - + //carry disequality list std::map< Node, std::map< Node, std::vector< Node > > >::iterator itd = d_diseq_list.find( ar ); if( itd!=d_diseq_list.end() ){ @@ -302,13 +320,13 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No } } } - + return status; }else{ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : disequal " << ar << " <> " << br << std::endl; Assert( d_diseq_list[ar].find( br )==d_diseq_list[ar].end() ); Assert( d_diseq_list[br].find( ar )==d_diseq_list[br].end() ); - + merge_exp( d_diseq_list[ar][br], reason ); merge_exp( d_diseq_list[br][ar], reason ); return STATUS_NONE; @@ -316,187 +334,234 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No } } -void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) { - if( is_prop ){ - if( isLiteral( n ) ){ - props.push_back( pol ? n : n.negate() ); - return; +void EqualityQueryInstProp::registerUfTerm( TNode n ) { + if( d_uf.find( n )==d_uf.end() ){ + if( !getEngine()->hasTerm( n ) ){ + TNode f = d_qe->getTermDatabase()->getMatchOperator( n ); + if( !f.isNull() ){ + std::vector< TNode > args; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( !getEngine()->hasTerm( n[i] ) ){ + return; + }else{ + args.push_back( n[i] ); + } + } + d_uf_func_map_trie[f].addTerm( n, args ); + } } } +} + +//void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) { +void EqualityQueryInstProp::addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch ) { + if( is_watch ){ + watch.push_back( n ); + } args.push_back( n ); } -bool EqualityQueryInstProp::isLiteral( Node n ) { - Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind(); - Assert( ak!=NOT ); - return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE; +bool EqualityQueryInstProp::isPropagateLiteral( Node n ) { + if( n==d_true || n==d_false ){ + return false; + }else{ + Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind(); + Assert( ak!=NOT ); + return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE; + } +} + +void EqualityQueryInstProp::setWatchList( Node n, std::vector< Node >& watch, std::map< Node, std::vector< Node > >& watch_list_out ) { + if( watch.empty() ){ + watch.push_back( n ); + } + for( unsigned j=0; j<watch.size(); j++ ){ + Trace("qip-eval") << "Watch : " << n << " -> " << watch[j] << std::endl; + watch_list_out[n].push_back( watch[j] ); + } +} + +void EqualityQueryInstProp::collectWatchList( Node n, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& watch_list ) { + std::map< Node, std::vector< Node > >::iterator it = watch_list_out.find( n ); + if( it!=watch_list_out.end() && std::find( watch_list.begin(), watch_list.end(), n )==watch_list.end() ){ + watch_list.push_back( n ); + for( unsigned j=0; j<it->second.size(); j++ ){ + collectWatchList( it->second[j], watch_list_out, watch_list ); + } + } } -//this is identical to TermDb::evaluateTerm2, but tracks more information -Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol, - std::map< Node, bool >& watch_list_out, std::vector< Node >& props ) { - std::map< Node, Node >::iterator itv = visited.find( n ); - if( itv != visited.end() ){ +//this is similar to TermDb::evaluateTerm2, but tracks more information +Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, std::map< int, std::map< Node, Node > >& visited, + bool hasPol, bool pol, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& props ) { + int polIndex = hasPol ? ( pol ? 1 : -1 ) : 0; + std::map< Node, Node >::iterator itv = visited[polIndex].find( n ); + if( itv!=visited[polIndex].end() ){ return itv->second; }else{ - visited[n] = n; - Trace("qip-eval") << "evaluate term : " << n << std::endl; - std::vector< Node > exp_n; - Node ret = getRepresentativeExp( n, exp_n ); - if( ret.isNull() ){ - //term is not known to be equal to a representative in equality engine, evaluate it - Kind k = n.getKind(); - if( k==FORALL ){ - ret = Node::null(); - }else{ - std::map< Node, bool > watch_list_out_curr; - TNode f = d_qe->getTermDatabase()->getMatchOperator( n ); - std::vector< Node > args; - bool ret_set = false; - bool childChanged = false; - int abort_i = -1; - //get the child entailed polarity - Assert( n.getKind()!=IMPLIES ); - bool newHasPol, newPol; - QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol ); - //for each child - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props ); - if( c.isNull() ){ - ret = Node::null(); - ret_set = true; - break; - }else if( c==d_true || c==d_false ){ - //short-circuiting - if( k==kind::AND || k==kind::OR ){ - if( (k==kind::AND)==(c==d_false) ){ - ret = c; - ret_set = true; - break; - }else{ - //redundant - c = Node::null(); - childChanged = true; - } - }else if( k==kind::ITE && i==0 ){ - Assert( watch_list_out_curr.empty() ); - ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props ); - ret_set = true; - break; - }else if( k==kind::NOT ){ - ret = c==d_true ? d_false : d_true; + visited[polIndex][n] = n; + Node ret; + //check if it should be propagated in this context + if( hasPol && isPropagateLiteral( n ) ){ + Assert( n.getType().isBoolean() ); + //must be Boolean + ret = evaluateTermExp( n, exp, visited, false, pol, watch_list_out, props ); + if( isPropagateLiteral( ret ) ){ + Trace("qip-eval") << "-----> propagate : " << ret << std::endl; + props.push_back( pol ? ret : ret.negate() ); + ret = pol ? d_true : d_false; + } + }else{ + Trace("qip-eval") << "evaluate term : " << n << " [" << polIndex << "]" << std::endl; + std::vector< Node > exp_n; + ret = getRepresentativeExp( n, exp_n ); + if( ret.isNull() ){ + //term is not known to be equal to a representative in equality engine, evaluate it + Kind k = n.getKind(); + if( k!=FORALL ){ + TNode f = d_qe->getTermDatabase()->getMatchOperator( n ); + std::vector< Node > args; + bool ret_set = false; + bool childChanged = false; + int abort_i = -1; + //get the child entailed polarity + Assert( n.getKind()!=IMPLIES ); + bool newHasPol, newPol; + QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol ); + std::vector< Node > watch; + //for each child + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out, props ); + if( c.isNull() ){ + ret = Node::null(); ret_set = true; break; - } - } - if( !c.isNull() ){ - childChanged = childChanged || n[i]!=c; - if( !f.isNull() && !watch_list_out_curr.empty() ){ - // we are done if this is an UF application and an argument is unevaluated - args.push_back( c ); - abort_i = i; - break; - }else if( ( k==kind::AND || k==kind::OR ) ){ - if( c.getKind()==k ){ - //flatten - for( unsigned j=0; j<c.getNumChildren(); j++ ){ - addArgument( args, props, c[j], newHasPol, newPol ); + }else if( c==d_true || c==d_false ){ + //short-circuiting + if( k==kind::AND || k==kind::OR ){ + if( (k==kind::AND)==(c==d_false) ){ + ret = c; + ret_set = true; + break; + }else{ + //redundant + c = Node::null(); + childChanged = true; } - }else{ - addArgument( args, props, c, newHasPol, newPol ); + }else if( k==kind::ITE && i==0 ){ + ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out, props ); + ret_set = true; + break; + }else if( k==kind::NOT ){ + ret = c==d_true ? d_false : d_true; + ret_set = true; + break; } - //if we are in a branching position - if( hasPol && !newHasPol && args.size()>=2 ){ - //we are done if at least two args are unevaluated + } + if( !c.isNull() ){ + childChanged = childChanged || n[i]!=c; + bool is_watch = watch_list_out.find( c )!=watch_list_out.end(); + if( !f.isNull() && is_watch ){ + // we are done if this is an UF application and an argument is unevaluated + addArgument( c, args, watch, is_watch ); abort_i = i; break; + }else if( k==kind::AND || k==kind::OR || k==kind::ITE || k==IFF ){ + Trace("qip-eval-debug") << "Adding argument " << c << " to " << k << ", isProp = " << newHasPol << std::endl; + if( ( k==kind::AND || k==kind::OR ) && c.getKind()==k ){ + //flatten + for( unsigned j=0; j<c.getNumChildren(); j++ ){ + addArgument( c[j], args, watch, is_watch ); + } + }else{ + addArgument( c, args, watch, is_watch ); + } + Trace("qip-eval-debug") << "props/args = " << props.size() << "/" << args.size() << std::endl; + //if we are in a branching position + if( hasPol && !newHasPol && args.size()>=2 ){ + //we are done if at least two args are unevaluated + abort_i = i; + break; + } + }else{ + addArgument( c, args, watch, is_watch ); } - }else if( k==kind::ITE ){ - //we are done if we are ITE and condition is unevaluated - Assert( i==0 ); - args.push_back( c ); - abort_i = i; - break; - }else{ - args.push_back( c ); } } - } - //add remaining children if we aborted - if( abort_i!=-1 ){ - for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){ - args.push_back( n[i] ); - } - } - //copy over the watch list - for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){ - watch_list_out[itc->first] = itc->second; - } - - //if we have not short-circuited evaluation - if( !ret_set ){ - //if it is an indexed term, return the congruent term - if( !f.isNull() && watch_list_out.empty() ){ - std::vector< TNode > t_args; - for( unsigned i=0; i<args.size(); i++ ) { - t_args.push_back( args[i] ); - } - Assert( args.size()==n.getNumChildren() ); - //args contains terms known by the equality engine - TNode nn = getCongruentTerm( f, t_args ); - Trace("qip-eval") << " got congruent term " << nn << " from DB for " << n << std::endl; - if( !nn.isNull() ){ - //successfully constructed representative in EE - Assert( exp_n.empty() ); - ret = getRepresentativeExp( nn, exp_n ); - Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl; - merge_exp( exp, exp_n ); - ret_set = true; - Assert( !ret.isNull() ); + //add remaining children if we aborted + if( abort_i!=-1 ){ + Trace("qip-eval-debug") << "..." << n << " aborted at " << abort_i << std::endl; + for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){ + args.push_back( n[i] ); } } + //if we have not short-circuited evaluation if( !ret_set ){ - if( childChanged ){ - Trace("qip-eval") << "return rewrite" << std::endl; - if( ( k==kind::AND || k==kind::OR ) ){ - if( args.empty() ){ - ret = k==kind::AND ? d_true : d_false; - ret_set = true; - }else if( args.size()==1 ){ - ret = args[0]; - ret_set = true; - } + //if it is an indexed term, return the congruent term + if( !f.isNull() && watch.empty() ){ + std::vector< TNode > t_args; + for( unsigned i=0; i<args.size(); i++ ) { + Trace("qip-eval") << "arg " << i << " : " << args[i] << std::endl; + t_args.push_back( args[i] ); + } + Assert( args.size()==n.getNumChildren() ); + //args contains terms known by the equality engine + TNode nn = getCongruentTerm( f, t_args ); + Trace("qip-eval") << " got congruent term " << nn << " for " << n << std::endl; + if( !nn.isNull() ){ + //successfully constructed representative in EE + Assert( exp_n.empty() ); + ret = getRepresentativeExp( nn, exp_n ); + Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl; + merge_exp( exp, exp_n ); + ret_set = true; + Assert( !ret.isNull() ); + Assert( ret!=n ); + // we have that n == ret, check if the union find should be updated TODO? }else{ - Assert( args.size()==n.getNumChildren() ); + watch.push_back( ret ); } - if( !ret_set ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - args.insert( args.begin(), n.getOperator() ); + } + if( !ret_set ){ + if( childChanged || args.size()!=n.getNumChildren() ){ + Trace("qip-eval") << "return rewrite" << std::endl; + if( k==kind::AND || k==kind::OR ){ + if( args.empty() ){ + ret = k==kind::AND ? d_true : d_false; + ret_set = true; + }else if( args.size()==1 ){ + //need to re-evaluate (may be new propagations) + ret = evaluateTermExp( args[0], exp, visited, hasPol, pol, watch_list_out, props ); + ret_set = true; + } + }else{ + Assert( args.size()==n.getNumChildren() ); } - ret = NodeManager::currentNM()->mkNode( k, args ); - ret = Rewriter::rewrite( ret ); - //re-evaluate - Node ret_eval = getRepresentativeExp( ret, exp_n ); - if( !ret_eval.isNull() ){ - ret = ret_eval; - watch_list_out.clear(); - }else{ - watch_list_out[ret] = true; + if( !ret_set ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + args.insert( args.begin(), n.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( k, args ); + setWatchList( ret, watch, watch_list_out ); + ret = Rewriter::rewrite( ret ); + //need to re-evaluate + ret = evaluateTermExp( ret, exp, visited, hasPol, pol, watch_list_out, props ); } + }else{ + ret = n; + setWatchList( ret, watch, watch_list_out ); } - }else{ - ret = n; - watch_list_out[ret] = true; } } } + }else{ + Trace("qip-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl; + merge_exp( exp, exp_n ); } - }else{ - Trace("qip-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl; - merge_exp( exp, exp_n ); } - Trace("qip-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl; - visited[n] = ret; + + Trace("qip-eval") << "evaluated term : " << n << " [" << polIndex << "], got : " << ret << ", exp size = " << exp.size() << ", watch list size = " << watch_list_out.size() << std::endl; + visited[polIndex][n] = ret; return ret; } } @@ -545,6 +610,7 @@ bool InstPropagator::reset( Theory::Effort e ) { d_watch_list.clear(); d_update_list.clear(); d_relevant_inst.clear(); + d_has_relevant_inst = false; return d_qy.reset( e ); } @@ -556,10 +622,7 @@ bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, st Trace("qip-prop") << " " << terms[i] << std::endl; } } - unsigned id = d_icount; - d_icount++; - Trace("qip-prop") << "...assign id=" << id << std::endl; - d_ii[id].init( q, lem, terms, body ); + unsigned id = allocateInstantiation( q, lem, terms, body ); //initialize the information if( cacheConclusion( id, body ) ){ Assert( d_update_list.empty() ); @@ -582,35 +645,67 @@ bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, st return !d_conflict; }else{ Assert( false ); - return true; + return false; + } +} + +void InstPropagator::filterInstantiations() { + if( d_has_relevant_inst ){ + //now, inform quantifiers engine which instances should be retracted + Trace("qip-prop-debug") << "...remove instantiation ids : "; + for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){ + if( !it->second.d_q.isNull() ){ + if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){ + if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){ + Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl; + Assert( false ); + }else{ + Trace("qip-prop-debug") << it->first << " "; + } + }else{ + //mark the quantified formula as relevant + d_qe->markRelevant( it->second.d_q ); + } + } + } + Trace("qip-prop-debug") << std::endl; + Trace("quant-engine-conflict") << "-----> InstPropagator::" << ( d_conflict ? "conflict" : "propagate" ) << " with " << d_relevant_inst.size() << " instances." << std::endl; } } +unsigned InstPropagator::allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ) { + unsigned id = d_icount; + d_icount++; + Trace("qip-prop") << "...assign id=" << id << std::endl; + d_ii[id].init( q, lem, terms, body ); + return id; +} + bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) { Assert( !d_conflict ); Assert( ii.d_active ); Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl; //update the evaluation of the current lemma - std::map< Node, Node > visited; - std::map< Node, bool > watch_list; + std::map< Node, std::vector< Node > > watch_list_out; + std::map< int, std::map< Node, Node > > visited; + std::vector< Node > exp; std::vector< Node > props; - Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props ); + Node eval = d_qy.evaluateTermExp( ii.d_curr, exp, visited, true, true, watch_list_out, props ); + EqualityQueryInstProp::merge_exp( ii.d_curr_exp, exp ); if( eval.isNull() ){ ii.d_active = false; }else if( firstTime || eval!=ii.d_curr ){ - if( EqualityQueryInstProp::isLiteral( eval ) ){ - props.push_back( eval ); - eval = d_qy.d_true; - watch_list.clear(); - } + std::vector< Node > watch_list; + d_qy.collectWatchList( eval, watch_list_out, watch_list ); if( Trace.isOn("qip-prop") ){ Trace("qip-prop") << "Update info [" << id << "]..." << std::endl; - Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = "; + Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << std::endl; + Trace("qip-prop") << "...explanation = "; debugPrintExplanation( ii.d_curr_exp, "qip-prop" ); Trace("qip-prop") << std::endl; Trace("qip-prop") << "...watch list: " << std::endl; - for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){ - Trace("qip-prop") << " " << itw->first << std::endl; + for( unsigned i=0; i<watch_list.size(); i++ ){ + Trace("qip-prop") << " " << watch_list[i] << std::endl; } Trace("qip-prop") << "...new propagations: " << std::endl; for( unsigned i=0; i<props.size(); i++ ){ @@ -627,8 +722,13 @@ bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) { }else{ for( unsigned i=0; i<props.size(); i++ ){ Trace("qip-prop-debug2") << "Process propagation " << props[i] << std::endl; + Assert( d_qy.isPropagateLiteral( props[i] ) ); //if we haven't propagated this literal yet if( cacheConclusion( id, props[i], 1 ) ){ + //watch list for propagated literal: may not yet be purely EE representatives + std::vector< Node > prop_watch_list; + d_qy.collectWatchList( props[i], watch_list_out, prop_watch_list ); + Node lit = props[i].getKind()==NOT ? props[i][0] : props[i]; bool pol = props[i].getKind()!=NOT; if( lit.getKind()==EQUAL ){ @@ -647,10 +747,10 @@ bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) { ii.d_curr = eval; //update the watch list Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl; - //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations. - // Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms. - for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){ - d_watch_list[ itw->first ][ id ] = true; + //Here, we need to be notified of enough terms such that if we are not notified, then update( id, ii ) will return no propagations. + // Similar to two-watched literals, but since we are taking into account UF, we need to watch all terms on a complete path of two terms. + for( unsigned i=0; i<watch_list.size(); i++ ){ + d_watch_list[ watch_list[i] ][ id ] = true; } }else{ Trace("qip-prop-debug") << "...conclusion " << eval << " is duplicate." << std::endl; @@ -682,10 +782,12 @@ void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& e } if( pol ){ if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){ + Trace("qip-rlv-propagate") << "Relevant propagation : " << a << ( pol ? " == " : " != " ) << b << std::endl; Assert( d_qy.getEngine()->hasTerm( a ) ); Assert( d_qy.getEngine()->hasTerm( b ) ); Trace("qip-prop-debug") << "...equality between known terms." << std::endl; addRelevantInstances( exp, "qip-propagate" ); + //d_has_relevant_inst = true; } Trace("qip-prop-debug") << "...merged representatives " << a << " and " << b << std::endl; for( unsigned i=0; i<2; i++ ){ @@ -712,25 +814,7 @@ void InstPropagator::conflict( std::vector< Node >& exp ) { d_conflict = true; d_relevant_inst.clear(); addRelevantInstances( exp, "qip-propagate" ); - - //now, inform quantifiers engine which instances should be retracted - Trace("qip-prop-debug") << "...remove instantiation ids : "; - for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){ - if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){ - if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){ - Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl; - Assert( false ); - }else{ - Trace("qip-prop-debug") << it->first << " "; - } - }else{ - //mark the quantified formula as relevant - d_qe->markRelevant( it->second.d_q ); - } - } - Trace("qip-prop-debug") << std::endl; - //will interupt the quantifiers engine - Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl; + d_has_relevant_inst = true; } bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) { |