summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp12
-rw-r--r--src/theory/datatypes/theory_datatypes.h2
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp3
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp4
-rw-r--r--src/theory/quantifiers/term_database.cpp10
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback