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 | |
parent | 4ff2946e1338d3f500b7e6bababee50fadad68d6 (diff) |
Bug fixes related to parametric datatypes + theory combination + quantifiers. Add regression.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 12 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-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 |
5 files changed, 19 insertions, 12 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 1653ab636..eb8b23973 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -540,8 +540,9 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { if( tst==d_true ){ n_ret = sel; }else{ - mkExpDefSkolem( selector, n[0].getType(), n.getType() ); - Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0] ); + TypeNode ndt = n[0].getType(); + mkExpDefSkolem( selector, ndt, n.getType() ); + Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ndt][ selector ], n[0] ); if( tst==NodeManager::currentNM()->mkConst( false ) ){ n_ret = sk; }else{ @@ -994,10 +995,10 @@ void TheoryDatatypes::getSelectorsForCons( Node r, std::map< int, bool >& sels ) } void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) { - if( d_exp_def_skolem.find( sel )==d_exp_def_skolem.end() ){ + if( d_exp_def_skolem[dt].find( sel )==d_exp_def_skolem[dt].end() ){ std::stringstream ss; ss << sel << "_uf"; - d_exp_def_skolem[ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), + d_exp_def_skolem[dt][ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), NodeManager::currentNM()->mkFunctionType( dt, rt ) ); } } @@ -1299,7 +1300,8 @@ void TheoryDatatypes::computeCareGraph(){ TNode y = f2[k]; Assert(d_equalityEngine.hasTerm(x)); Assert(d_equalityEngine.hasTerm(y)); - if( areDisequal(x, y) ){ + //need to consider types for parametric selectors + if( x.getType()!=y.getType() || areDisequal(x, y) ){ somePairIsDisequal = true; break; }else if( !d_equalityEngine.areEqual( x, y ) ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index b826780fc..4bf04e08c 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -183,7 +183,7 @@ private: /** counter for forcing assignments (ensures fairness) */ unsigned d_dtfCounter; /** expand definition skolem functions */ - std::map< Node, Node > d_exp_def_skolem; + std::map< TypeNode, std::map< Node, Node > > d_exp_def_skolem; /** sygus utilities */ SygusSplit * d_sygus_split; SygusSymBreak * d_sygus_sym_break; 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(); |