diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 253 |
1 files changed, 181 insertions, 72 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 18ba08ae2..79fdf8791 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -18,6 +18,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "options/datatypes_options.h" +#include "options/uf_options.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fun_def_engine.h" @@ -135,7 +136,7 @@ Node TermDb::getMatchOperator( Node n ) { Kind k = n.getKind(); //datatype operators may be parametric, always assume they are if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || - k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){ + k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO || k==HO_APPLY ){ //since it is parametric, use a particular one as op TypeNode tn = n[0].getType(); Node op = n.getOperator(); @@ -146,6 +147,7 @@ Node TermDb::getMatchOperator( Node n ) { return it->second; } } + Trace("par-op") << "Parametric operator : " << k << ", " << n.getOperator() << ", " << tn << " : " << n << std::endl; d_par_op_map[op][tn] = n; return n; }else if( inst::Trigger::isAtomicTriggerKind( k ) ){ @@ -210,16 +212,27 @@ void TermDb::computeArgReps( TNode n ) { } void TermDb::computeUfEqcTerms( TNode f ) { + Assert( f==getOperatorRepresentative( f ) ); if( d_func_map_eqc_trie.find( f )==d_func_map_eqc_trie.end() ){ d_func_map_eqc_trie[f].clear(); + // get the matchable operators in the equivalence class of f + std::vector< TNode > ops; + ops.push_back( f ); + if( options::ufHo() ){ + ops.insert( ops.end(), d_ho_op_rep_slaves[f].begin(), d_ho_op_rep_slaves[f].end() ); + } eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine(); - for( unsigned i=0; i<d_op_map[f].size(); i++ ){ - TNode n = d_op_map[f][i]; - if( hasTermCurrent( n ) ){ - if( isTermActive( n ) ){ - computeArgReps( n ); - TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n; - d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] ); + for( unsigned j=0; j<ops.size(); j++ ){ + Node ff = ops[j]; + //Assert( !options::ufHo() || ee->areEqual( ff, f ) ); + for( unsigned i=0; i<d_op_map[ff].size(); i++ ){ + TNode n = d_op_map[ff][i]; + if( hasTermCurrent( n ) ){ + if( isTermActive( n ) ){ + computeArgReps( n ); + TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n; + d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] ); + } } } } @@ -227,84 +240,126 @@ void TermDb::computeUfEqcTerms( TNode f ) { } void TermDb::computeUfTerms( TNode f ) { + Assert( f==getOperatorRepresentative( f ) ); if( d_op_nonred_count.find( f )==d_op_nonred_count.end() ){ d_op_nonred_count[ f ] = 0; - std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f ); - if( it!=d_op_map.end() ){ - eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); - Trace("term-db-debug") << "Adding terms for operator " << f << std::endl; - unsigned congruentCount = 0; - unsigned nonCongruentCount = 0; - unsigned alreadyCongruentCount = 0; - unsigned relevantCount = 0; - for( unsigned i=0; i<it->second.size(); i++ ){ - Node n = it->second[i]; - //to be added to term index, term must be relevant, and exist in EE - if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ - relevantCount++; - if( isTermActive( n ) ){ - computeArgReps( n ); - - Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; - for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){ - Trace("term-db-debug") << d_arg_reps[n][i] << " "; - if( std::find( d_func_map_rel_dom[f][i].begin(), - d_func_map_rel_dom[f][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[f][i].end() ){ - d_func_map_rel_dom[f][i].push_back( d_arg_reps[n][i] ); + // get the matchable operators in the equivalence class of f + std::vector< TNode > ops; + ops.push_back( f ); + if( options::ufHo() ){ + ops.insert( ops.end(), d_ho_op_rep_slaves[f].begin(), d_ho_op_rep_slaves[f].end() ); + } + unsigned congruentCount = 0; + unsigned nonCongruentCount = 0; + unsigned alreadyCongruentCount = 0; + unsigned relevantCount = 0; + eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); + for( unsigned j=0; j<ops.size(); j++ ){ + Node ff = ops[j]; + //Assert( !options::ufHo() || ee->areEqual( ff, f ) ); + std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( ff ); + if( it!=d_op_map.end() ){ + Trace("term-db-debug") << "Adding terms for operator " << f << std::endl; + for( unsigned i=0; i<it->second.size(); i++ ){ + Node n = it->second[i]; + //to be added to term index, term must be relevant, and exist in EE + if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ + relevantCount++; + if( isTermActive( n ) ){ + computeArgReps( n ); + + Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; + for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){ + Trace("term-db-debug") << d_arg_reps[n][i] << " "; + if( std::find( d_func_map_rel_dom[f][i].begin(), + d_func_map_rel_dom[f][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[f][i].end() ){ + d_func_map_rel_dom[f][i].push_back( d_arg_reps[n][i] ); + } } - } - Trace("term-db-debug") << std::endl; - Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; - Node at = d_func_map_trie[ f ].addOrGetTerm( n, d_arg_reps[n] ); - Trace("term-db-debug2") << "...add term returned " << at << std::endl; - if( at!=n && ee->areEqual( at, n ) ){ - setTermInactive( n ); - Trace("term-db-debug") << n << " is redundant." << std::endl; - congruentCount++; - }else{ - if( at!=n && ee->areDisequal( at, n, false ) ){ - std::vector< Node > lits; - lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at, n ) ); - for( unsigned i=0; i<at.getNumChildren(); i++ ){ - if( at[i]!=n[i] ){ - lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at[i], n[i] ).negate() ); + Trace("term-db-debug") << std::endl; + Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; + Node at = d_func_map_trie[ f ].addOrGetTerm( n, d_arg_reps[n] ); + Trace("term-db-debug2") << "...add term returned " << at << std::endl; + if( at!=n && ee->areEqual( at, n ) ){ + setTermInactive( n ); + Trace("term-db-debug") << n << " is redundant." << std::endl; + congruentCount++; + }else{ + if( at!=n && ee->areDisequal( at, n, false ) ){ + std::vector< Node > lits; + lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at, n ) ); + bool success = true; + if( options::ufHo() ){ + //operators might be disequal + if( ops.size()>1 ){ + Node atf = getMatchOperator( at ); + Node nf = getMatchOperator( n ); + if( atf!=nf ){ + if( at.getKind()==APPLY_UF && n.getKind()==APPLY_UF ){ + lits.push_back( atf.eqNode( nf ).negate() ); + }else{ + success = false; + Assert( false ); + } + } + } } - } - Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits ); - if( Trace.isOn("term-db-lemma") ){ - Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; - if( !d_quantEngine->getTheoryEngine()->needCheck() ){ - Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; - // we should be a full effort check, prior to theory combination + if( success ){ + for( unsigned k=0; k<at.getNumChildren(); k++ ){ + if( at[k]!=n[k] ){ + lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at[k], n[k] ).negate() ); + } + } + Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits ); + if( Trace.isOn("term-db-lemma") ){ + Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; + if( !d_quantEngine->getTheoryEngine()->needCheck() ){ + Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; + // we should be a full effort check, prior to theory combination + } + Trace("term-db-lemma") << " add lemma : " << lem << std::endl; + } + d_quantEngine->addLemma( lem ); + d_quantEngine->setConflict(); + d_consistent_ee = false; + return; } - Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } - d_quantEngine->addLemma( lem ); - d_quantEngine->setConflict(); - d_consistent_ee = false; - return; + nonCongruentCount++; + d_op_nonred_count[ f ]++; } - nonCongruentCount++; - d_op_nonred_count[ f ]++; + }else{ + Trace("term-db-debug") << n << " is already redundant." << std::endl; + alreadyCongruentCount++; } }else{ - Trace("term-db-debug") << n << " is already redundant." << std::endl; - alreadyCongruentCount++; + Trace("term-db-debug") << n << " is not relevant." << std::endl; } - }else{ - Trace("term-db-debug") << n << " is not relevant." << std::endl; } - } - if( Trace.isOn("tdb") ){ - Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / "; - Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / "; - Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl; + if( Trace.isOn("tdb") ){ + Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / "; + Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / "; + Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl; + } } } } } + +Node TermDb::getOperatorRepresentative( TNode op ) const { + std::map< TNode, TNode >::const_iterator it = d_ho_op_rep.find( op ); + if( it!=d_ho_op_rep.end() ){ + return it->second; + }else{ + return op; + } +} + bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { + if( options::ufHo() ){ + f = getOperatorRepresentative( f ); + } computeUfTerms( f ); Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) || d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r ); @@ -727,6 +782,37 @@ bool TermDb::reset( Theory::Effort effort ){ } } + if( options::ufHo() && options::hoMergeTermDb() ){ + Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl; + // build operator representative map + d_ho_op_rep.clear(); + d_ho_op_rep_slaves.clear(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + TNode r = (*eqcs_i); + if( r.getType().isFunction() ){ + Node first; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + if( d_op_map.find( n )!=d_op_map.end() ){ + if( first.isNull() ){ + first = n; + d_ho_op_rep[n] = n; + }else{ + Trace("quant-ho") << " have : " << n << " == " << first << ", type = " << n.getType() << std::endl; + d_ho_op_rep[n] = first; + d_ho_op_rep_slaves[first].push_back( n ); + } + } + ++eqc_i; + } + } + ++eqcs_i; + } + Trace("quant-ho") << "...finished compute equal functions." << std::endl; + } + /* //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ @@ -740,6 +826,9 @@ bool TermDb::reset( Theory::Effort effort ){ } TermArgTrie * TermDb::getTermArgTrie( Node f ) { + if( options::ufHo() ){ + f = getOperatorRepresentative( f ); + } computeUfTerms( f ); std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); if( itut!=d_func_map_trie.end() ){ @@ -750,6 +839,9 @@ TermArgTrie * TermDb::getTermArgTrie( Node f ) { } TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) { + if( options::ufHo() ){ + f = getOperatorRepresentative( f ); + } computeUfEqcTerms( f ); std::map< Node, TermArgTrie >::iterator itut = d_func_map_eqc_trie.find( f ); if( itut==d_func_map_eqc_trie.end() ){ @@ -769,6 +861,9 @@ TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) { } TNode TermDb::getCongruentTerm( Node f, Node n ) { + if( options::ufHo() ){ + f = getOperatorRepresentative( f ); + } computeUfTerms( f ); std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); if( itut!=d_func_map_trie.end() ){ @@ -780,6 +875,9 @@ TNode TermDb::getCongruentTerm( Node f, Node n ) { } TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { + if( options::ufHo() ){ + f = getOperatorRepresentative( f ); + } computeUfTerms( f ); return d_func_map_trie[f].existsTerm( args ); } @@ -1272,7 +1370,7 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) { if( it==d_typ_closed_enum.end() ){ d_typ_closed_enum[tn] = true; bool ret = true; - if( tn.isArray() || tn.isSort() || tn.isCodatatype() ){ + if( tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction() ){ ret = false; }else if( tn.isSet() ){ ret = isClosedEnumerableType( tn.getSetElementType() ); @@ -1290,9 +1388,8 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) { break; } } - }else{ - //TODO: all subfields must be closed enumerable } + //TODO: other parametric sorts go here d_typ_closed_enum[tn] = ret; return ret; }else{ @@ -1985,6 +2082,18 @@ void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ } } +Node TermDb::getHoTypeMatchPredicate( TypeNode tn ) { + std::map< TypeNode, Node >::iterator ithp = d_ho_type_match_pred.find( tn ); + if( ithp==d_ho_type_match_pred.end() ){ + TypeNode ptn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() ); + Node k = NodeManager::currentNM()->mkSkolem( "U", ptn, "predicate to force higher-order types" ); + d_ho_type_match_pred[tn] = k; + return k; + }else{ + return ithp->second; + } +} + bool TermDb::isInductionTerm( Node n ) { TypeNode tn = n.getType(); if( options::dtStcInduction() && tn.isDatatype() ){ |