diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 16:29:20 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 16:29:20 -0500 |
commit | dd01099518aab8d42d788dfadadbe11763ec9d18 (patch) | |
tree | ab3accd00c5e4ee3f2035349b9387bf8b9d85e90 /src/theory/quantifiers | |
parent | 4ff2946e1338d3f500b7e6bababee50fadad68d6 (diff) |
Bug fixes related to parametric datatypes + theory combination + quantifiers. Add regression.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 10 |
3 files changed, 11 insertions, 6 deletions
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index bb514f41b..8c67eb95e 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -691,10 +691,13 @@ bool FullSaturation::process( Node f, bool fullEffort ){ if( max_zero[i] ){ //no terms available, will report incomplete instantiation terms.push_back( Node::null() ); + Trace("inst-alg-rd") << " null" << std::endl; }else if( r==0 ){ terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] ); + Trace("inst-alg-rd") << " " << rd->getRDomain( f, i )->d_terms[childIndex[i]] << std::endl; }else{ terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) ); + Trace("inst-alg-rd") << " " << d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) << std::endl; } } if( d_quantEngine->addInstantiation( f, terms, false ) ){ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 1cbfbd99b..c796333b3 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -508,9 +508,9 @@ bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRe if( it!=d_var_rel_dom.end() ){ for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ for( unsigned j=0; j<it2->second.size(); j++ ){ - Debug("qcf-match-debug2") << n << " in relevant domain " << it2->second << "." << it2->second[j] << "?" << std::endl; + Debug("qcf-match-debug2") << n << " in relevant domain " << it2->first << "." << it2->second[j] << "?" << std::endl; if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){ - Debug("qcf-match-debug") << " -> fail, since " << n << " is not in relevant domain of " << it2->second << "." << it2->second[j] << std::endl; + Debug("qcf-match-debug") << " -> fail, since " << n << " is not in relevant domain of " << it2->first << "." << it2->second[j] << std::endl; return false; } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ef301c2cf..51c72d7bb 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -126,9 +126,10 @@ Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) { } Node TermDb::getMatchOperator( Node n ) { - //return n.getOperator(); Kind k = n.getKind(); - if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ){ + //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 ){ //since it is parametric, use a particular one as op TypeNode tn = n[0].getType(); Node op = n.getOperator(); @@ -241,10 +242,11 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ if( itv != visited.end() ){ return itv->second; } - Assert( n.getKind()!=BOUND_VARIABLE ); Trace("term-db-eval") << "evaluate term : " << n << std::endl; Node ret; - if( !qy->hasTerm( n ) ){ + if( n.getKind()==BOUND_VARIABLE ){ + return n; + }else if( !qy->hasTerm( n ) ){ //term is not known to be equal to a representative in equality engine, evaluate it if( n.getKind()==FORALL ){ ret = Node::null(); |