diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/options/quantifiers_options | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 253 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 30 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_type_rules.h | 3 |
4 files changed, 219 insertions, 77 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 44fbc4ee7..2e765ce6b 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -368,6 +368,16 @@ option quantAntiSkolem --quant-anti-skolem bool :read-write :default false option quantEqualityEngine --quant-ee bool :default false maintain congrunce closure over universal equalities +### higher-order options + +option hoMatching --ho-matching bool :default true + do higher-order matching algorithm for triggers with variable operators +option hoMatchingVarArgPriority --ho-matching-var-priority bool :default true + give priority to variable arguments over constant arguments + +option hoMergeTermDb --ho-merge-term-db bool :default true + merge term indices modulo equality + ### proof options option trackInstLemmas --track-inst-lemmas bool :read-write :default false 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() ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9df9da957..852d94fde 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -132,6 +132,7 @@ class QuantifiersEngine; namespace inst{ class Trigger; + class HigherOrderTrigger; } namespace quantifiers { @@ -188,6 +189,7 @@ class TermDb : public QuantifiersUtil { friend class ::CVC4::theory::QuantifiersEngine; //TODO: eliminate most of these friend class ::CVC4::theory::inst::Trigger; + friend class ::CVC4::theory::inst::HigherOrderTrigger; friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; friend class ::CVC4::theory::quantifiers::QuantConflictFind; friend class ::CVC4::theory::quantifiers::RelevantDomain; @@ -251,6 +253,17 @@ private: Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ); TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); + /** compute uf eqc terms */ + void computeUfEqcTerms( TNode f ); + /** compute uf terms */ + void computeUfTerms( TNode f ); +private: // for higher-order term indexing + /** a map from matchable operators to their representative */ + std::map< TNode, TNode > d_ho_op_rep; + /** for each representative matchable operator, the list of other matchable operators in their equivalence class */ + std::map< TNode, std::vector< TNode > > d_ho_op_rep_slaves; + /** get operator representative */ + Node getOperatorRepresentative( TNode op ) const; public: /** ground terms for operator */ unsigned getNumGroundTerms( Node f ); @@ -272,10 +285,6 @@ public: TNode getCongruentTerm( Node f, std::vector< TNode >& args ); /** compute arg reps */ void computeArgReps( TNode n ); - /** compute uf eqc terms */ - void computeUfEqcTerms( TNode f ); - /** compute uf terms */ - void computeUfTerms( TNode f ); /** in relevant domain */ bool inRelevantDomain( TNode f, unsigned i, TNode r ); /** evaluate a term under a substitution. Return representative in EE if possible. @@ -520,6 +529,19 @@ public: /** is bool connective term */ static bool isBoolConnectiveTerm( TNode n ); +//for higher-order +private: + /** dummy predicate that states terms should be considered first-class members of equality engine */ + std::map< TypeNode, Node > d_ho_type_match_pred; +public: + /** get higher-order type match predicate + * This predicate is used to force certain functions f of type tn to appear as first-class representatives in the + * quantifier-free UF solver. For a typical use case, we call getHoTypeMatchPredicate which returns a fresh + * predicate P of type (tn -> Bool). Then, we add P( f ) as a lemma. + * TODO: we may eliminate this depending on how github issue #1115 is resolved. + */ + Node getHoTypeMatchPredicate( TypeNode tn ); + //for sygus private: TermDbSygus * d_sygus_tdb; diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index f3e68b9f9..2ea7e9b72 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -86,7 +86,8 @@ struct QuantifierInstPatternTypeRule { Assert(n.getKind() == kind::INST_PATTERN ); if( check ){ TypeNode tn = n[0].getType(check); - if( tn.isFunction() ){ + // this check catches the common mistake writing :pattern (f x) instead of :pattern ((f x)) + if( n[0].isVar() && n[0].getKind()!=kind::BOUND_VARIABLE && tn.isFunction() ){ throw TypeCheckingExceptionPrivate(n[0], "Pattern must be a list of fully-applied terms."); } } |