summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/quantifiers_options10
-rw-r--r--src/theory/quantifiers/term_database.cpp253
-rw-r--r--src/theory/quantifiers/term_database.h30
-rw-r--r--src/theory/quantifiers/theory_quantifiers_type_rules.h3
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.");
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback