+++ /dev/null
-/********************* */
-/*! \file inst_propagator.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** Propagate mechanism for instantiations
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/inst_propagator.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/rewriter.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-
-EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){
- d_true = NodeManager::currentNM()->mkConst( true );
- d_false = NodeManager::currentNM()->mkConst( false );
-}
-
-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;
-}
-
-/** contains term */
-bool EqualityQueryInstProp::hasTerm( Node a ) {
- if( getEngine()->hasTerm( a ) ){
- return true;
- }else{
- std::vector< Node > exp;
- Node ar = getUfRepresentative( a, exp );
- return !ar.isNull() && getEngine()->hasTerm( ar );
- }
-}
-
-/** get the representative of the equivalence class of a */
-Node EqualityQueryInstProp::getRepresentative( Node a ) {
- if( getEngine()->hasTerm( a ) ){
- a = getEngine()->getRepresentative( a );
- }
- std::vector< Node > exp;
- Node ar = getUfRepresentative( a, exp );
- return ar.isNull() ? a : ar;
-}
-
-/** returns true if a and b are equal in the current context */
-bool EqualityQueryInstProp::areEqual( Node a, Node b ) {
- if( a==b ){
- return true;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- if( ee->areEqual( a, b ) ){
- return true;
- }
- }
- return false;
- }
-}
-
-/** returns true is a and b are disequal in the current context */
-bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {
- if( a==b ){
- return false;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- if( ee->areDisequal( a, b, false ) ){
- return true;
- }
- }
- return false;
- }
-}
-
-/** get the equality engine associated with this query */
-eq::EqualityEngine* EqualityQueryInstProp::getEngine() {
- return d_qe->getActiveEqualityEngine();
-}
-
-/** get the equivalence class of a */
-void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {
- //TODO?
-}
-
-TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {
- TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );
- if( !t.isNull() ){
- return t;
- }else{
- return d_uf_func_map_trie[f].existsTerm( args );
- }
-}
-
-Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {
- bool engine_has_a = getEngine()->hasTerm( a );
- if( engine_has_a ){
- a = getEngine()->getRepresentative( a );
- }
- //get union find representative, if this occurs in the equality engine, return it
- unsigned prev_size = exp.size();
- 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;
- }
- }else{
- if( engine_has_a ){
- return a;
- }
- }
- //retract explanation
- while( exp.size()>prev_size ){
- exp.pop_back();
- }
- return Node::null();
-}
-
-bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {
- if( areEqual( a, b ) ){
- return true;
- }else{
- std::vector< Node > exp_a;
- Node ar = getUfRepresentative( a, exp_a );
- if( !ar.isNull() ){
- std::vector< Node > exp_b;
- if( ar==getUfRepresentative( b, exp_b ) ){
- merge_exp( exp, exp_a );
- merge_exp( exp, exp_b );
- return true;
- }
- }
- return false;
- }
-}
-
-bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {
- if( areDisequal( a, b ) ){
- return true;
- }else{
- //Assert( getRepresentative( a )==a );
- //Assert( getRepresentative( b )==b );
- std::map< Node, std::vector< Node > >::iterator itd = d_diseq_list[a].find( b );
- if( itd!=d_diseq_list[a].end() ){
- exp.insert( exp.end(), itd->second.begin(), itd->second.end() );
- return true;
- }else{
- return false;
- }
- }
-}
-
-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 );
- if( it!=d_uf.end() ){
- if( it->second==a ){
- Assert(d_uf_exp[a].empty());
- return it->second;
- }else{
- Node m = getUfRepresentative( it->second, exp );
- Assert(!m.isNull());
- if( m!=it->second ){
- //update union find
- d_uf[ a ] = m;
- //update explanation : merge the explanation of the parent
- merge_exp( d_uf_exp[ a ], exp );
- Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;
- }
- //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset
- exp.clear();
- exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );
- return m;
- }
- }else{
- return Node::null();
- }
-}
-
-// set a == b with reason, return status, modify a and b to representatives pre-merge
-int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason ) {
- if( a==b ){
- return pol ? STATUS_NONE : STATUS_CONFLICT;
- }
- int status = pol ? STATUS_MERGED_UNKNOWN : STATUS_NONE;
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", pol = " << pol << ", reason size = " << reason.size() << std::endl;
- //get the representative for a
- std::vector< Node > exp_a;
- Node ar = getUfRepresentative( a, exp_a );
- if( ar.isNull() ){
- Assert(exp_a.empty());
- ar = a;
- }
- if( ar==b ){
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
- if( pol ){
- return STATUS_NONE;
- }else{
- merge_exp( reason, exp_a );
- return STATUS_CONFLICT;
- }
- }
- bool swap = false;
- //get the representative for b
- std::vector< Node > exp_b;
- Node br = getUfRepresentative( b, exp_b );
- if( br.isNull() ){
- Assert(exp_b.empty());
- br = b;
- if( !getEngine()->hasTerm( br ) ){
- if( ar!=a || getEngine()->hasTerm( ar ) ){
- swap = true;
- }
- }else{
- if( getEngine()->hasTerm( ar ) ){
- status = STATUS_MERGED_KNOWN;
- }
- }
- }else{
- if( ar==br ){
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
- if( pol ){
- return STATUS_NONE;
- }else{
- merge_exp( reason, exp_a );
- merge_exp( reason, exp_b );
- return STATUS_CONFLICT;
- }
- }else if( getEngine()->hasTerm( ar ) ){
- if( getEngine()->hasTerm( br ) ){
- status = STATUS_MERGED_KNOWN;
- }else{
- swap = true;
- }
- }
- }
-
- if( swap ){
- //swap
- Node temp_r = ar;
- ar = br;
- br = temp_r;
- }
-
- Assert(!getEngine()->hasTerm(ar) || getEngine()->hasTerm(br));
- Assert(ar != br);
-
- std::vector< Node > exp_d;
- if( areDisequalExp( ar, br, exp_d ) ){
- if( pol ){
- merge_exp( reason, exp_b );
- merge_exp( reason, exp_b );
- merge_exp( reason, exp_d );
- return STATUS_CONFLICT;
- }else{
- return STATUS_NONE;
- }
- }else{
- if( pol ){
- //update the union find
- 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() ){
- for( std::map< Node, std::vector< Node > >::iterator itdd = itd->second.begin(); itdd != itd->second.end(); ++itdd ){
- Node d = itdd->first;
- if( d_diseq_list[br].find( d )==d_diseq_list[br].end() ){
- merge_exp( d_diseq_list[br][d], itdd->second );
- merge_exp( d_diseq_list[br][d], d_uf_exp[ar] );
- }
- }
- }
-
- 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;
- }
- }
-}
-
-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::isPropagateLiteral( Node n ) {
- if( n==d_true || n==d_false ){
- return false;
- }else{
- Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
- if( ak==EQUAL ){
- Node atom = n.getKind()==NOT ? n[0] : n;
- return !atom[0].getType().isBoolean();
- }else{
- Assert(ak != NOT);
- return ak!=AND && ak!=OR && 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 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[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;
- }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 ){
- 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( !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==EQUAL && n[0].getType().isBoolean() ) ){
- 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 );
- }
- }
- }
- //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 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{
- watch.push_back( ret );
- }
- }
- 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());
- }
- 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{
- 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 << " [" << polIndex << "], got : " << ret << ", exp size = " << exp.size() << ", watch list size = " << watch_list_out.size() << std::endl;
- visited[polIndex][n] = ret;
- return ret;
- }
-}
-
-void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {
- //TODO : optimize
- if( v.empty() ){
- Assert(up_to_size == -1 || up_to_size == (int)v_to_merge.size());
- v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );
- }else{
- //std::vector< Node >::iterator v_end = v.end();
- up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;
- for( int j=0; j<up_to_size; j++ ){
- if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){
- v.push_back( v_to_merge[j] );
- }
- }
- }
-}
-
-
-void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {
- d_active = true;
- //information about the instance
- d_q = q;
- d_lem = lem;
- Assert(d_terms.empty());
- d_terms.insert( d_terms.end(), terms.begin(), terms.end() );
- //the current lemma
- d_curr = body;
- d_curr_exp.push_back( body );
-}
-
-InstPropagator::InstPropagator(QuantifiersEngine* qe)
- : d_qe(qe),
- d_notify(*this),
- d_qy(qe),
- d_icount(1),
- d_conflict(false),
- d_has_relevant_inst(false) {}
-
-bool InstPropagator::reset( Theory::Effort e ) {
- d_icount = 1;
- d_ii.clear();
- for( unsigned i=0; i<2; i++ ){
- d_conc_to_id[i].clear();
- d_conc_to_id[i][d_qy.d_true] = 0;
- }
- d_conflict = false;
- d_watch_list.clear();
- d_update_list.clear();
- d_relevant_inst.clear();
- d_has_relevant_inst = false;
- return d_qy.reset( e );
-}
-
-bool InstPropagator::notifyInstantiation(QuantifiersModule::QEffort quant_e,
- Node q,
- Node lem,
- std::vector<Node>& terms,
- Node body)
-{
- if( !d_conflict ){
- if( Trace.isOn("qip-prop") ){
- Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;
- for( unsigned i=0; i<terms.size(); i++ ){
- Trace("qip-prop") << " " << terms[i] << std::endl;
- }
- }
- unsigned id = allocateInstantiation( q, lem, terms, body );
- //initialize the information
- if( cacheConclusion( id, body ) ){
- Assert(d_update_list.empty());
- d_update_list.push_back( id );
- bool firstTime = true;
- //update infos in the update list until empty
- do {
- unsigned uid = d_update_list.back();
- d_update_list.pop_back();
- if( d_ii[uid].d_active ){
- update( uid, d_ii[uid], firstTime );
- }
- firstTime = false;
- }while( !d_conflict && !d_update_list.empty() );
- }else{
- d_ii[id].d_active = false;
- Trace("qip-prop") << "...duplicate." << std::endl;
- }
- Trace("qip-prop") << "...finished notify instantiation." << std::endl;
- return !d_conflict;
- }else{
- Assert(false);
- 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->getInstantiate()->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, 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, 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 ){
- 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 << 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( 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++ ){
- Trace("qip-prop") << " " << props[i] << std::endl;
- }
- Trace("qip-prop") << std::endl;
- }
- //determine the status of eval
- if( eval==d_qy.d_false ){
- Assert(props.empty());
- //we have inferred a conflict
- conflict( ii.d_curr_exp );
- return false;
- }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 ){
- propagate( lit[0], lit[1], pol, ii.d_curr_exp );
- }else{
- propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );
- }
- if( d_conflict ){
- return false;
- }
- }
- Trace("qip-prop-debug2") << "Done process propagation " << props[i] << std::endl;
- }
- //if we have not inferred this conclusion yet
- if( cacheConclusion( id, eval ) ){
- 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( 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;
- ii.d_active = false;
- }
- }
- }else{
- Trace("qip-prop-debug") << "...did not update." << std::endl;
- }
- Assert(!d_conflict);
- return true;
-}
-
-void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {
- if( Trace.isOn("qip-propagate") ){
- Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";
- debugPrintExplanation( exp, "qip-propagate" );
- Trace("qip-propagate") << "..." << std::endl;
- }
- //set equal
- int status = d_qy.setEqual( a, b, pol, exp );
- if( status==EqualityQueryInstProp::STATUS_NONE ){
- Trace("qip-prop-debug") << "...already equal/no conflict." << std::endl;
- return;
- }else if( status==EqualityQueryInstProp::STATUS_CONFLICT ){
- Trace("qip-prop-debug") << "...conflict." << std::endl;
- conflict( exp );
- return;
- }
- if( pol ){
- if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
- Trace("qip-rlv-propagate")
- << "Relevant propagation : " << a << " == " << 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++ ){
- //update terms from watched lists
- Node c = i==0 ? a : b;
- std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );
- if( it!=d_watch_list.end() ){
- Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;
- for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){
- unsigned idw = itw->first;
- if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){
- Trace("qip-prop-debug") << "...will update " << idw << std::endl;
- d_update_list.push_back( idw );
- }
- }
- d_watch_list.erase( c );
- }
- }
- }
-}
-
-void InstPropagator::conflict( std::vector< Node >& exp ) {
- Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;
- d_conflict = true;
- d_relevant_inst.clear();
- addRelevantInstances( exp, "qip-propagate" );
- d_has_relevant_inst = true;
-}
-
-bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
- Assert(prop_index == 0 || prop_index == 1);
- //check if the conclusion is non-redundant
- if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){
- d_conc_to_id[prop_index][body] = id;
- return true;
- }else{
- return false;
- }
-}
-
-void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {
- for( unsigned i=0; i<exp.size(); i++ ){
- Assert(d_conc_to_id[0].find(exp[i]) != d_conc_to_id[0].end());
- Trace(c) << " relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;
- d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;
- }
-}
-
-void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {
- for( unsigned i=0; i<exp.size(); i++ ){
- Assert(d_conc_to_id[0].find(exp[i]) != d_conc_to_id[0].end());
- Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";
- }
-}
-
+++ /dev/null
-/********************* */
-/*! \file inst_propagator.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Mathias Preiner, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Propagate mechanism for instantiations
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__QUANTIFIERS_INST_PROPAGATOR_H
-#define CVC4__QUANTIFIERS_INST_PROPAGATOR_H
-
-#include <iostream>
-#include <map>
-#include <string>
-#include <vector>
-#include "expr/node.h"
-#include "expr/node_trie.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_util.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class EqualityQueryInstProp : public EqualityQuery {
-private:
- /** pointer to quantifiers engine */
- QuantifiersEngine* d_qe;
-public:
- EqualityQueryInstProp( QuantifiersEngine* qe );
- ~EqualityQueryInstProp(){};
- /** reset */
- bool reset(Theory::Effort e) override;
- /* Called for new quantifiers */
- void registerQuantifier(Node q) override {}
- /** identify */
- std::string identify() const override { return "EqualityQueryInstProp"; }
- /** extends engine */
- bool extendsEngine() override { return true; }
- /** contains term */
- bool hasTerm(Node a) override;
- /** get the representative of the equivalence class of a */
- Node getRepresentative(Node a) override;
- /** returns true if a and b are equal in the current context */
- bool areEqual(Node a, Node b) override;
- /** returns true is a and b are disequal in the current context */
- bool areDisequal(Node a, Node b) override;
- /** get the equality engine associated with this query */
- eq::EqualityEngine* getEngine() override;
- /** get the equivalence class of a */
- void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
- /** get congruent term */
- TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
-
- public:
- /** get the representative of the equivalence class of a, with explanation */
- Node getRepresentativeExp( Node a, std::vector< Node >& exp );
- /** returns true if a and b are equal in the current context */
- bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
- /** returns true is a and b are disequal in the current context */
- bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
- /** get congruent term */
- TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp );
-private:
- /** term index */
- std::map<Node, TNodeTrie> d_uf_func_map_trie;
- /** union find for terms beyond what is stored in equality engine */
- std::map<Node, Node> d_uf;
- std::map<Node, std::vector<Node> > d_uf_exp;
- Node getUfRepresentative(Node a, std::vector<Node>& exp);
- /** disequality list, stores explanations */
- std::map<Node, std::map<Node, std::vector<Node> > > d_diseq_list;
- /** add arg */
- void addArgument(Node n,
- std::vector<Node>& args,
- std::vector<Node>& watch,
- bool is_watch);
- /** register term */
- void registerUfTerm(TNode n);
-
-public:
- enum {
- STATUS_CONFLICT,
- STATUS_MERGED_KNOWN,
- STATUS_MERGED_UNKNOWN,
- STATUS_NONE,
- };
- /** set equal */
- int setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason );
- Node d_true;
- Node d_false;
-public:
- //for explanations
- static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );
- //for watch list
- static void setWatchList( Node n, std::vector< Node >& watch, std::map< Node, std::vector< Node > >& watch_list_out );
- static void collectWatchList( Node n, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& watch_list );
-
- Node 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 );
- bool isPropagateLiteral( Node n );
-};
-
-class InstPropagator : public QuantifiersUtil {
-private:
- /** pointer to quantifiers engine */
- QuantifiersEngine* d_qe;
- /** notify class */
- class InstantiationNotifyInstPropagator : public InstantiationNotify {
- InstPropagator& d_ip;
- public:
- InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
- bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
- Node q,
- Node lem,
- std::vector<Node>& terms,
- Node body) override
- {
- return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
- }
- void filterInstantiations() override { d_ip.filterInstantiations(); }
- };
- InstantiationNotifyInstPropagator d_notify;
- /** notify instantiation method */
- bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
- Node q,
- Node lem,
- std::vector<Node>& terms,
- Node body);
- /** remove instance ids */
- void filterInstantiations();
- /** allocate instantiation */
- unsigned allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body );
- /** equality query */
- EqualityQueryInstProp d_qy;
- class InstInfo {
- public:
- bool d_active;
- Node d_q;
- Node d_lem;
- std::vector< Node > d_terms;
- // the current entailed body
- Node d_curr;
- //explanation for current entailed body
- std::vector< Node > d_curr_exp;
- void init( Node q, Node lem, std::vector< Node >& terms, Node body );
- };
- /** instantiation count/info */
- unsigned d_icount;
- std::map< unsigned, InstInfo > d_ii;
- std::map< Node, unsigned > d_conc_to_id[2];
- /** are we in conflict */
- bool d_conflict;
- /** watch list */
- std::map< Node, std::map< unsigned, bool > > d_watch_list;
- /** update list */
- std::vector< unsigned > d_update_list;
- /** relevant instances */
- std::map< unsigned, bool > d_relevant_inst;
- bool d_has_relevant_inst;
-private:
- bool update( unsigned id, InstInfo& i, bool firstTime = false );
- void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );
- void conflict( std::vector< Node >& exp );
- bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );
- void addRelevantInstances( std::vector< Node >& exp, const char * c );
- void debugPrintExplanation( std::vector< Node >& exp, const char * c );
-public:
- InstPropagator( QuantifiersEngine* qe );
- ~InstPropagator(){}
- /** reset */
- bool reset(Theory::Effort e) override;
- /* Called for new quantifiers */
- void registerQuantifier(Node q) override {}
- /** identify */
- std::string identify() const override { return "InstPropagator"; }
- /** get the notify mechanism */
- InstantiationNotify* getInstantiationNotify() { return &d_notify; }
-};
-
-}
-}
-}
-
-#endif
projects / cvc5.git / commitdiff