diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 4 |
2 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index afe8cd598..881210d78 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -932,8 +932,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto newChildren.push_back( Node::fromExpr( c.getConstructor() ) ); std::vector< Node > newVars; for( unsigned j=0; j<c.getNumArgs(); j++ ){ - TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() ); - tn = tn[1]; + TypeNode tn = TypeNode::fromType( c[j].getRangeType() ); Node v = NodeManager::currentNM()->mkBoundVar( tn ); newChildren.push_back( v ); newVars.push_back( v ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 560f68810..a679ccfa8 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -855,7 +855,7 @@ Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) { void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){ for( unsigned j=0; j<dc.getNumArgs(); j++ ){ - TypeNode tn = TypeNode::fromType( ((SelectorType)dc[j].getSelector().getType()).getRangeType() ); + TypeNode tn = TypeNode::fromType( dc[j].getRangeType() ); std::vector< Node > ssc; if( tn==ntn ){ ssc.push_back( n ); @@ -1050,7 +1050,7 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) { 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 ctn = TypeNode::fromType( ((SelectorType)dt[i][j].getSelector().getType()).getRangeType() ); + TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() ); if( tn!=ctn && !isClosedEnumerableType( ctn ) ){ ret = false; break; |