diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/sort_inference.cpp | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index c4c0a8b47..74f2e4803 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -367,12 +367,21 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map< if( d_var_types.find( n )!=d_var_types.end() ){ return getIdForType( n.getType() ); }else{ + //apply sort inference to quantified variables for( size_t i=0; i<n[0].getNumChildren(); i++ ){ - //apply sort inference to quantified variables - d_var_types[n][n[0][i]] = d_sortCount; - d_sortCount++; - - //type of the quantified variable must be the same + TypeNode nitn = n[0][i].getType(); + if( !nitn.isSort() ) + { + // If the variable is of an interpreted sort, we assume the + // the sort of the variable will stay the same sort. + d_var_types[n][n[0][i]] = getIdForType( nitn ); + } + else + { + // If it is of an uninterpreted sort, infer subsorts. + d_var_types[n][n[0][i]] = d_sortCount; + d_sortCount++; + } var_bound[ n[0][i] ] = n; } } |