diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 18:10:42 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 18:10:42 -0600 |
| commit | 80daa7fd5917526513a510261fd3901f03949dfa (patch) | |
| tree | 7fa74722e30c6e5cc59d96b045273c2bdaf27701 /src/theory/quantifiers | |
| parent | f31163c1f6bb1816365e9f22505d9558a7bc1802 (diff) | |
More simplification to internal implementation of tuples and records.
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; |