diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/sort_inference.cpp | 32 | ||||
-rw-r--r-- | src/theory/sort_inference.h | 8 |
2 files changed, 24 insertions, 16 deletions
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 9a90e591d..42364f080 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -29,6 +29,7 @@ #include "theory/quantifiers/quant_util.h" using namespace CVC4; +using namespace CVC4::kind; using namespace std; namespace CVC4 { @@ -434,7 +435,9 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map< } d_equality_types[n] = child_types[0]; retType = getIdForType( n.getType() ); - }else if( n.getKind()==kind::APPLY_UF ){ + } + else if (isHandledApplyUf(n.getKind())) + { Node op = n.getOperator(); TypeNode tn_op = op.getType(); if( d_op_return_types.find( op )==d_op_return_types.end() ){ @@ -663,7 +666,8 @@ Node SortInference::simplifyNode( : i >= 1; } if( processChild ){ - if( n.getKind()==kind::APPLY_UF ){ + if (isHandledApplyUf(n.getKind())) + { Assert(d_op_arg_types.find(op) != d_op_arg_types.end()); tnnc = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() ); Assert(!tnnc.isNull()); @@ -704,7 +708,9 @@ Node SortInference::simplifyNode( Assert(false); } ret = NodeManager::currentNM()->mkNode( kind::EQUAL, children ); - }else if( n.getKind()==kind::APPLY_UF ){ + } + else if (isHandledApplyUf(n.getKind())) + { if( d_symbol_map.find( op )==d_symbol_map.end() ){ //make the new operator if necessary bool opChanged = false; @@ -815,7 +821,8 @@ void SortInference::setSkolemVar( Node f, Node v, Node sk ){ } bool SortInference::isWellSortedFormula( Node n ) { - if( n.getType().isBoolean() && n.getKind()!=kind::APPLY_UF ){ + if (n.getType().isBoolean() && !isHandledApplyUf(n.getKind())) + { for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( !isWellSortedFormula( n[i] ) ){ return false; @@ -831,7 +838,8 @@ bool SortInference::isWellSorted( Node n ) { if( getSortId( n )==0 ){ return false; }else{ - if( n.getKind()==kind::APPLY_UF ){ + if (isHandledApplyUf(n.getKind())) + { for( unsigned i=0; i<n.getNumChildren(); i++ ){ int s1 = getSortId( n[i] ); int s2 = d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ); @@ -847,18 +855,14 @@ bool SortInference::isWellSorted( Node n ) { } } -void SortInference::getSortConstraints( Node n, UnionFind& uf ) { - if( n.getKind()==kind::APPLY_UF ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - getSortConstraints( n[i], uf ); - uf.setEqual( getSortId( n[i] ), d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ) ); - } - } -} - bool SortInference::isMonotonic( TypeNode tn ) { Assert(tn.isSort()); return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end(); } +bool SortInference::isHandledApplyUf(Kind k) const +{ + return k == APPLY_UF && !options::ufHo(); +} + }/* CVC4 namespace */ diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h index 5b28f669d..ecf86376c 100644 --- a/src/theory/sort_inference.h +++ b/src/theory/sort_inference.h @@ -154,11 +154,15 @@ public: //is well sorted bool isWellSortedFormula( Node n ); bool isWellSorted( Node n ); - //get constraints for being well-typed according to computed sub-types - void getSortConstraints( Node n, SortInference::UnionFind& uf ); private: // store monotonicity for original sorts as well std::map<TypeNode, bool> d_non_monotonic_sorts_orig; + /** + * Returns true if k is the APPLY_UF kind and we are not using higher-order + * techniques. This is called in places where we want to know whether to + * treat a term as uninterpreted function. + */ + bool isHandledApplyUf(Kind k) const; }; } |