diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-15 10:31:58 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-15 10:31:58 -0500 |
commit | 3344979103bcec622276fca7c2a21cc0945f6c56 (patch) | |
tree | 8cdcd2cec0db34d70a2bbdb0443bbe3d250995cf /src/theory/quantifiers/inst_strategy_cbqi.cpp | |
parent | 8bb55a22b7c0f20305274f8609b9e8404e4bb41c (diff) |
Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cbqi for datatypes with uninterpreted sort subfields. Simplify fmc model construction.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 44 |
1 files changed, 36 insertions, 8 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 88f8e2484..58bebef35 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -496,21 +496,49 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit } return false; } -int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ - int hmin = 1; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - TypeNode tn = q[0][i].getType(); - int handled = -1; + +// -1 : not cbqi sort, 0 : cbqi sort, 1 : cbqi sort regardless of quantifier body +int InstStrategyCbqi::isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited ) { + std::map< TypeNode, int >::iterator itv = visited.find( tn ); + if( itv==visited.end() ){ + visited[tn] = 0; + int ret = -1; if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){ - handled = 0; + ret = 0; }else if( tn.isDatatype() ){ - handled = 0; + ret = 1; + const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ + TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ); + int cret = isCbqiSort( crange, visited ); + if( cret==-1 ){ + visited[tn] = -1; + return -1; + }else if( cret<ret ){ + ret = cret; + } + } + } }else if( tn.isSort() ){ QuantEPR * qepr = d_quantEngine->getQuantEPR(); if( qepr!=NULL ){ - handled = qepr->isEPR( tn ) ? 1 : -1; + ret = qepr->isEPR( tn ) ? 1 : -1; } } + visited[tn] = ret; + return ret; + }else{ + return itv->second; + } +} + +int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ + int hmin = 1; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + TypeNode tn = q[0][i].getType(); + std::map< TypeNode, int > visited; + int handled = isCbqiSort( tn, visited ); if( handled==-1 ){ return -1; }else if( handled<hmin ){ |