diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-04 17:30:18 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-04 17:30:18 -0500 |
commit | aed7130284c04f7ada79db1ed3d4a8ddb08d3543 (patch) | |
tree | 5388d8ef1af23934fe381d0f1b5da796d5176a19 /src/util | |
parent | 9c0b2f6abd82564df0686cca826015f4eb9095fa (diff) |
fixed files with DOS newlines; fixed contrib/ scripts to use git
Diffstat (limited to 'src/util')
-rw-r--r--[-rwxr-xr-x] | src/util/sort_inference.cpp | 854 | ||||
-rw-r--r--[-rwxr-xr-x] | src/util/sort_inference.h | 152 |
2 files changed, 503 insertions, 503 deletions
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index cab5dac42..0304a8e35 100755..100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -1,428 +1,428 @@ -/********************* */
-/*! \file sort_inference.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Sort inference module
- **
- ** This class implements sort inference, based on a simple algorithm:
- ** First, we assume all functions and predicates have distinct uninterpreted types.
- ** One pass is made through the input assertions, while a union-find data structure
- ** maintains necessary information regarding constraints on these types.
- **/
-
-#include <vector>
-
-#include "util/sort_inference.h"
-
-using namespace CVC4;
-using namespace std;
-
-namespace CVC4 {
-
-
-void SortInference::printSort( const char* c, int t ){
- int rt = getRepresentative( t );
- if( d_type_types.find( rt )!=d_type_types.end() ){
- Trace(c) << d_type_types[rt];
- }else{
- Trace(c) << "s_" << rt;
- }
-}
-
-void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
- //process all assertions
- for( unsigned i=0; i<assertions.size(); i++ ){
- Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
- std::map< Node, Node > var_bound;
- process( assertions[i], var_bound );
- }
- //print debug
- if( Trace.isOn("sort-inference") ){
- for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
- Trace("sort-inference") << it->first << " : ";
- if( !d_op_arg_types[ it->first ].empty() ){
- Trace("sort-inference") << "( ";
- for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
- printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
- Trace("sort-inference") << " ";
- }
- Trace("sort-inference") << ") -> ";
- }
- printSort( "sort-inference", it->second );
- Trace("sort-inference") << std::endl;
- }
- for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
- Trace("sort-inference") << "Quantified formula " << it->first << " : " << std::endl;
- for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- printSort( "sort-inference", it2->second );
- Trace("sort-inference") << std::endl;
- }
- Trace("sort-inference") << std::endl;
- }
- }
- if( doRewrite ){
- //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)
- for( unsigned i=0; i<assertions.size(); i++ ){
- std::map< Node, Node > var_bound;
- assertions[i] = simplify( assertions[i], var_bound );
- Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl;
- }
- //now, ensure constants are distinct
- for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){
- std::vector< Node > consts;
- for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- consts.push_back( it2->second );
- }
- //add lemma enforcing introduced constants to be distinct?
- }
- }
-}
-
-int SortInference::getRepresentative( int t ){
- std::map< int, int >::iterator it = d_type_union_find.find( t );
- if( it!=d_type_union_find.end() ){
- if( it->second==t ){
- return t;
- }else{
- int rt = getRepresentative( it->second );
- d_type_union_find[t] = rt;
- return rt;
- }
- }else{
- return t;
- }
-}
-
-void SortInference::setEqual( int t1, int t2 ){
- if( t1!=t2 ){
- int rt1 = getRepresentative( t1 );
- int rt2 = getRepresentative( t2 );
- if( rt1!=rt2 ){
- Trace("sort-inference-debug") << "Set equal : ";
- printSort( "sort-inference-debug", rt1 );
- Trace("sort-inference-debug") << " ";
- printSort( "sort-inference-debug", rt2 );
- Trace("sort-inference-debug") << std::endl;
- //check if they must be a type
- std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 );
- std::map< int, TypeNode >::iterator it2 = d_type_types.find( rt2 );
- if( it2!=d_type_types.end() ){
- if( it1==d_type_types.end() ){
- //swap sides
- int swap = rt1;
- rt1 = rt2;
- rt2 = swap;
- }else{
- Assert( rt1==rt2 );
- }
- }
- /*
- d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() );
- d_type_eq_class[rt2].clear();
- Trace("sort-inference-debug") << "EqClass : { ";
- for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){
- Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", ";
- }
- Trace("sort-inference-debug") << "}" << std::endl;
- */
- d_type_union_find[rt2] = rt1;
- }
- }
-}
-
-int SortInference::getIdForType( TypeNode tn ){
- //register the return type
- std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn );
- if( it==d_id_for_types.end() ){
- int sc = sortCount;
- d_type_types[ sortCount ] = tn;
- d_id_for_types[ tn ] = sortCount;
- sortCount++;
- return sc;
- }else{
- return it->second;
- }
-}
-
-int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
- Trace("sort-inference-debug") << "Process " << n << std::endl;
- //add to variable bindings
- if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
- for( size_t i=0; i<n[0].getNumChildren(); i++ ){
- //TODO: try applying sort inference to quantified variables
- d_var_types[n][ n[0][i] ] = sortCount;
- sortCount++;
-
- //type of the quantified variable must be the same
- //d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );
- var_bound[ n[0][i] ] = n;
- }
- }
-
- //process children
- std::vector< Node > children;
- std::vector< int > child_types;
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- bool processChild = true;
- if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
- processChild = i==1;
- }
- if( processChild ){
- children.push_back( n[i] );
- child_types.push_back( process( n[i], var_bound ) );
- }
- }
-
- //remove from variable bindings
- if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
- //erase from variable bound
- for( size_t i=0; i<n[0].getNumChildren(); i++ ){
- var_bound.erase( n[0][i] );
- }
- }
-
- int retType;
- if( n.getKind()==kind::EQUAL ){
- //we only require that the left and right hand side must be equal
- setEqual( child_types[0], child_types[1] );
- retType = getIdForType( n.getType() );
- }else if( n.getKind()==kind::APPLY_UF ){
- Node op = n.getOperator();
- if( d_op_return_types.find( op )==d_op_return_types.end() ){
- //assign arbitrary sort for return type
- d_op_return_types[op] = sortCount;
- sortCount++;
- //d_type_eq_class[sortCount].push_back( op );
- //assign arbitrary sort for argument types
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- d_op_arg_types[op].push_back( sortCount );
- sortCount++;
- }
- }
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- //the argument of the operator must match the return type of the subterm
- setEqual( child_types[i], d_op_arg_types[op][i] );
- }
- //return type is the return type
- retType = d_op_return_types[op];
- }else{
- std::map< Node, Node >::iterator it = var_bound.find( n );
- if( it!=var_bound.end() ){
- Trace("sort-inference-debug") << n << " is a bound variable." << std::endl;
- //the return type was specified while binding
- retType = d_var_types[it->second][n];
- }else if( n.getKind() == kind::VARIABLE ){
- Trace("sort-inference-debug") << n << " is a variable." << std::endl;
- if( d_op_return_types.find( n )==d_op_return_types.end() ){
- //assign arbitrary sort
- d_op_return_types[n] = sortCount;
- sortCount++;
- //d_type_eq_class[sortCount].push_back( n );
- }
- retType = d_op_return_types[n];
- }else if( n.isConst() ){
- Trace("sort-inference-debug") << n << " is a constant." << std::endl;
- //can be any type we want
- retType = sortCount;
- sortCount++;
- }else{
- Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl;
- //it is an interpretted term
- for( size_t i=0; i<children.size(); i++ ){
- Trace("sort-inference-debug") << children[i] << " forced to have " << children[i].getType() << std::endl;
- //must enforce the actual type of the operator on the children
- int ct = getIdForType( children[i].getType() );
- setEqual( child_types[i], ct );
- }
- //return type must be the actual return type
- retType = getIdForType( n.getType() );
- }
- }
- Trace("sort-inference-debug") << "Type( " << n << " ) = ";
- printSort("sort-inference-debug", retType );
- Trace("sort-inference-debug") << std::endl;
- return retType;
-}
-
-
-TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
- int rt = getRepresentative( t );
- if( d_type_types.find( rt )!=d_type_types.end() ){
- return d_type_types[rt];
- }else{
- TypeNode retType;
- //see if we can assign pref
- if( !pref.isNull() && d_id_for_types.find( pref )==d_id_for_types.end() ){
- retType = pref;
- }else{
- if( d_subtype_count.find( pref )==d_subtype_count.end() ){
- d_subtype_count[pref] = 0;
- }
- //must create new type
- std::stringstream ss;
- ss << "it_" << d_subtype_count[pref] << "_" << pref;
- d_subtype_count[pref]++;
- retType = NodeManager::currentNM()->mkSort( ss.str() );
- }
- d_id_for_types[ retType ] = rt;
- d_type_types[ rt ] = retType;
- return retType;
- }
-}
-
-TypeNode SortInference::getTypeForId( int t ){
- int rt = getRepresentative( t );
- if( d_type_types.find( rt )!=d_type_types.end() ){
- return d_type_types[rt];
- }else{
- return TypeNode::null();
- }
-}
-
-Node SortInference::getNewSymbol( Node old, TypeNode tn ){
- if( tn==old.getType() ){
- return old;
- }else if( old.isConst() ){
- //must make constant of type tn
- if( d_const_map[tn].find( old )==d_const_map[tn].end() ){
- std::stringstream ss;
- ss << "ic_" << tn << "_" << old;
- d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" ); //use mkConst???
- }
- return d_const_map[tn][ old ];
- }else{
- std::stringstream ss;
- ss << "i_$$_" << old;
- return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" );
- }
-}
-
-Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
- std::vector< Node > children;
- if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
- //recreate based on types of variables
- std::vector< Node > new_children;
- for( size_t i=0; i<n[0].getNumChildren(); i++ ){
- TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() );
- Node v = getNewSymbol( n[0][i], tn );
- new_children.push_back( v );
- var_bound[ n[0][i] ] = v;
- }
- children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) );
- }
-
- //process children
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- bool processChild = true;
- if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
- processChild = i>=1;
- }
- if( processChild ){
- children.push_back( simplify( n[i], var_bound ) );
- }
- }
-
- //remove from variable bindings
- if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
- //erase from variable bound
- for( size_t i=0; i<n[0].getNumChildren(); i++ ){
- var_bound.erase( n[0][i] );
- }
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }else if( n.getKind()==kind::EQUAL ){
- if( children[0].getType()!=children[1].getType() ){
- if( children[0].isConst() ){
- children[0] = getNewSymbol( children[0], children[1].getType() );
- }else if( children[1].isConst() ){
- children[1] = getNewSymbol( children[1], children[0].getType() );
- }else{
- Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl;
- Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl;
- Assert( false );
- }
- }
- return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
- }else if( n.getKind()==kind::APPLY_UF ){
- Node op = n.getOperator();
- if( d_symbol_map.find( op )==d_symbol_map.end() ){
- //make the new operator if necessary
- bool opChanged = false;
- std::vector< TypeNode > argTypes;
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- TypeNode tn = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );
- argTypes.push_back( tn );
- if( tn!=n[i].getType() ){
- opChanged = true;
- }
- }
- TypeNode retType = getOrCreateTypeForId( d_op_return_types[op], n.getType() );
- if( retType!=n.getType() ){
- opChanged = true;
- }
- if( opChanged ){
- std::stringstream ss;
- ss << "io_$$_" << op;
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType );
- d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" );
- }else{
- d_symbol_map[op] = op;
- }
- }
- children[0] = d_symbol_map[op];
- //make sure all children have been taken care of
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- TypeNode tn = children[i+1].getType();
- TypeNode tna = getTypeForId( d_op_arg_types[op][i] );
- if( tn!=tna ){
- if( n[i].isConst() ){
- children[i+1] = getNewSymbol( n[i], tna );
- }else{
- Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl;
- Assert( false );
- }
- }
- }
- return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
- }else{
- std::map< Node, Node >::iterator it = var_bound.find( n );
- if( it!=var_bound.end() ){
- return it->second;
- }else if( n.getKind() == kind::VARIABLE ){
- if( d_symbol_map.find( n )==d_symbol_map.end() ){
- TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() );
- d_symbol_map[n] = getNewSymbol( n, tn );
- }
- return d_symbol_map[n];
- }else if( n.isConst() ){
- //just return n, we will fix at higher scope
- return n;
- }else{
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
- }
-
-}
-int SortInference::getSortId( Node n ) {
- Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n;
- return getRepresentative( d_op_return_types[op] );
-}
-
-int SortInference::getSortId( Node f, Node v ) {
- return getRepresentative( d_var_types[f][v] );
-}
-
-void SortInference::setSkolemVar( Node f, Node v, Node sk ){
- d_op_return_types[sk] = getSortId( f, v );
-}
-
+/********************* */ +/*! \file sort_inference.cpp + ** \verbatim + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sort inference module + ** + ** This class implements sort inference, based on a simple algorithm: + ** First, we assume all functions and predicates have distinct uninterpreted types. + ** One pass is made through the input assertions, while a union-find data structure + ** maintains necessary information regarding constraints on these types. + **/ + +#include <vector> + +#include "util/sort_inference.h" + +using namespace CVC4; +using namespace std; + +namespace CVC4 { + + +void SortInference::printSort( const char* c, int t ){ + int rt = getRepresentative( t ); + if( d_type_types.find( rt )!=d_type_types.end() ){ + Trace(c) << d_type_types[rt]; + }else{ + Trace(c) << "s_" << rt; + } +} + +void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){ + //process all assertions + for( unsigned i=0; i<assertions.size(); i++ ){ + Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl; + std::map< Node, Node > var_bound; + process( assertions[i], var_bound ); + } + //print debug + if( Trace.isOn("sort-inference") ){ + for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ + Trace("sort-inference") << it->first << " : "; + if( !d_op_arg_types[ it->first ].empty() ){ + Trace("sort-inference") << "( "; + for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){ + printSort( "sort-inference", d_op_arg_types[ it->first ][i] ); + Trace("sort-inference") << " "; + } + Trace("sort-inference") << ") -> "; + } + printSort( "sort-inference", it->second ); + Trace("sort-inference") << std::endl; + } + for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){ + Trace("sort-inference") << "Quantified formula " << it->first << " : " << std::endl; + for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + printSort( "sort-inference", it2->second ); + Trace("sort-inference") << std::endl; + } + Trace("sort-inference") << std::endl; + } + } + if( doRewrite ){ + //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers) + for( unsigned i=0; i<assertions.size(); i++ ){ + std::map< Node, Node > var_bound; + assertions[i] = simplify( assertions[i], var_bound ); + Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl; + } + //now, ensure constants are distinct + for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){ + std::vector< Node > consts; + for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + consts.push_back( it2->second ); + } + //add lemma enforcing introduced constants to be distinct? + } + } +} + +int SortInference::getRepresentative( int t ){ + std::map< int, int >::iterator it = d_type_union_find.find( t ); + if( it!=d_type_union_find.end() ){ + if( it->second==t ){ + return t; + }else{ + int rt = getRepresentative( it->second ); + d_type_union_find[t] = rt; + return rt; + } + }else{ + return t; + } +} + +void SortInference::setEqual( int t1, int t2 ){ + if( t1!=t2 ){ + int rt1 = getRepresentative( t1 ); + int rt2 = getRepresentative( t2 ); + if( rt1!=rt2 ){ + Trace("sort-inference-debug") << "Set equal : "; + printSort( "sort-inference-debug", rt1 ); + Trace("sort-inference-debug") << " "; + printSort( "sort-inference-debug", rt2 ); + Trace("sort-inference-debug") << std::endl; + //check if they must be a type + std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 ); + std::map< int, TypeNode >::iterator it2 = d_type_types.find( rt2 ); + if( it2!=d_type_types.end() ){ + if( it1==d_type_types.end() ){ + //swap sides + int swap = rt1; + rt1 = rt2; + rt2 = swap; + }else{ + Assert( rt1==rt2 ); + } + } + /* + d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() ); + d_type_eq_class[rt2].clear(); + Trace("sort-inference-debug") << "EqClass : { "; + for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){ + Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", "; + } + Trace("sort-inference-debug") << "}" << std::endl; + */ + d_type_union_find[rt2] = rt1; + } + } +} + +int SortInference::getIdForType( TypeNode tn ){ + //register the return type + std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn ); + if( it==d_id_for_types.end() ){ + int sc = sortCount; + d_type_types[ sortCount ] = tn; + d_id_for_types[ tn ] = sortCount; + sortCount++; + return sc; + }else{ + return it->second; + } +} + +int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ + Trace("sort-inference-debug") << "Process " << n << std::endl; + //add to variable bindings + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + for( size_t i=0; i<n[0].getNumChildren(); i++ ){ + //TODO: try applying sort inference to quantified variables + d_var_types[n][ n[0][i] ] = sortCount; + sortCount++; + + //type of the quantified variable must be the same + //d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() ); + var_bound[ n[0][i] ] = n; + } + } + + //process children + std::vector< Node > children; + std::vector< int > child_types; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + bool processChild = true; + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + processChild = i==1; + } + if( processChild ){ + children.push_back( n[i] ); + child_types.push_back( process( n[i], var_bound ) ); + } + } + + //remove from variable bindings + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + //erase from variable bound + for( size_t i=0; i<n[0].getNumChildren(); i++ ){ + var_bound.erase( n[0][i] ); + } + } + + int retType; + if( n.getKind()==kind::EQUAL ){ + //we only require that the left and right hand side must be equal + setEqual( child_types[0], child_types[1] ); + retType = getIdForType( n.getType() ); + }else if( n.getKind()==kind::APPLY_UF ){ + Node op = n.getOperator(); + if( d_op_return_types.find( op )==d_op_return_types.end() ){ + //assign arbitrary sort for return type + d_op_return_types[op] = sortCount; + sortCount++; + //d_type_eq_class[sortCount].push_back( op ); + //assign arbitrary sort for argument types + for( size_t i=0; i<n.getNumChildren(); i++ ){ + d_op_arg_types[op].push_back( sortCount ); + sortCount++; + } + } + for( size_t i=0; i<n.getNumChildren(); i++ ){ + //the argument of the operator must match the return type of the subterm + setEqual( child_types[i], d_op_arg_types[op][i] ); + } + //return type is the return type + retType = d_op_return_types[op]; + }else{ + std::map< Node, Node >::iterator it = var_bound.find( n ); + if( it!=var_bound.end() ){ + Trace("sort-inference-debug") << n << " is a bound variable." << std::endl; + //the return type was specified while binding + retType = d_var_types[it->second][n]; + }else if( n.getKind() == kind::VARIABLE ){ + Trace("sort-inference-debug") << n << " is a variable." << std::endl; + if( d_op_return_types.find( n )==d_op_return_types.end() ){ + //assign arbitrary sort + d_op_return_types[n] = sortCount; + sortCount++; + //d_type_eq_class[sortCount].push_back( n ); + } + retType = d_op_return_types[n]; + }else if( n.isConst() ){ + Trace("sort-inference-debug") << n << " is a constant." << std::endl; + //can be any type we want + retType = sortCount; + sortCount++; + }else{ + Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl; + //it is an interpretted term + for( size_t i=0; i<children.size(); i++ ){ + Trace("sort-inference-debug") << children[i] << " forced to have " << children[i].getType() << std::endl; + //must enforce the actual type of the operator on the children + int ct = getIdForType( children[i].getType() ); + setEqual( child_types[i], ct ); + } + //return type must be the actual return type + retType = getIdForType( n.getType() ); + } + } + Trace("sort-inference-debug") << "Type( " << n << " ) = "; + printSort("sort-inference-debug", retType ); + Trace("sort-inference-debug") << std::endl; + return retType; +} + + +TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){ + int rt = getRepresentative( t ); + if( d_type_types.find( rt )!=d_type_types.end() ){ + return d_type_types[rt]; + }else{ + TypeNode retType; + //see if we can assign pref + if( !pref.isNull() && d_id_for_types.find( pref )==d_id_for_types.end() ){ + retType = pref; + }else{ + if( d_subtype_count.find( pref )==d_subtype_count.end() ){ + d_subtype_count[pref] = 0; + } + //must create new type + std::stringstream ss; + ss << "it_" << d_subtype_count[pref] << "_" << pref; + d_subtype_count[pref]++; + retType = NodeManager::currentNM()->mkSort( ss.str() ); + } + d_id_for_types[ retType ] = rt; + d_type_types[ rt ] = retType; + return retType; + } +} + +TypeNode SortInference::getTypeForId( int t ){ + int rt = getRepresentative( t ); + if( d_type_types.find( rt )!=d_type_types.end() ){ + return d_type_types[rt]; + }else{ + return TypeNode::null(); + } +} + +Node SortInference::getNewSymbol( Node old, TypeNode tn ){ + if( tn==old.getType() ){ + return old; + }else if( old.isConst() ){ + //must make constant of type tn + if( d_const_map[tn].find( old )==d_const_map[tn].end() ){ + std::stringstream ss; + ss << "ic_" << tn << "_" << old; + d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" ); //use mkConst??? + } + return d_const_map[tn][ old ]; + }else{ + std::stringstream ss; + ss << "i_$$_" << old; + return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" ); + } +} + +Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ + std::vector< Node > children; + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + //recreate based on types of variables + std::vector< Node > new_children; + for( size_t i=0; i<n[0].getNumChildren(); i++ ){ + TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() ); + Node v = getNewSymbol( n[0][i], tn ); + new_children.push_back( v ); + var_bound[ n[0][i] ] = v; + } + children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) ); + } + + //process children + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for( size_t i=0; i<n.getNumChildren(); i++ ){ + bool processChild = true; + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + processChild = i>=1; + } + if( processChild ){ + children.push_back( simplify( n[i], var_bound ) ); + } + } + + //remove from variable bindings + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + //erase from variable bound + for( size_t i=0; i<n[0].getNumChildren(); i++ ){ + var_bound.erase( n[0][i] ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else if( n.getKind()==kind::EQUAL ){ + if( children[0].getType()!=children[1].getType() ){ + if( children[0].isConst() ){ + children[0] = getNewSymbol( children[0], children[1].getType() ); + }else if( children[1].isConst() ){ + children[1] = getNewSymbol( children[1], children[0].getType() ); + }else{ + Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl; + Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl; + Assert( false ); + } + } + return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children ); + }else if( n.getKind()==kind::APPLY_UF ){ + Node op = n.getOperator(); + if( d_symbol_map.find( op )==d_symbol_map.end() ){ + //make the new operator if necessary + bool opChanged = false; + std::vector< TypeNode > argTypes; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + TypeNode tn = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() ); + argTypes.push_back( tn ); + if( tn!=n[i].getType() ){ + opChanged = true; + } + } + TypeNode retType = getOrCreateTypeForId( d_op_return_types[op], n.getType() ); + if( retType!=n.getType() ){ + opChanged = true; + } + if( opChanged ){ + std::stringstream ss; + ss << "io_$$_" << op; + TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType ); + d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" ); + }else{ + d_symbol_map[op] = op; + } + } + children[0] = d_symbol_map[op]; + //make sure all children have been taken care of + for( size_t i=0; i<n.getNumChildren(); i++ ){ + TypeNode tn = children[i+1].getType(); + TypeNode tna = getTypeForId( d_op_arg_types[op][i] ); + if( tn!=tna ){ + if( n[i].isConst() ){ + children[i+1] = getNewSymbol( n[i], tna ); + }else{ + Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl; + Assert( false ); + } + } + } + return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children ); + }else{ + std::map< Node, Node >::iterator it = var_bound.find( n ); + if( it!=var_bound.end() ){ + return it->second; + }else if( n.getKind() == kind::VARIABLE ){ + if( d_symbol_map.find( n )==d_symbol_map.end() ){ + TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() ); + d_symbol_map[n] = getNewSymbol( n, tn ); + } + return d_symbol_map[n]; + }else if( n.isConst() ){ + //just return n, we will fix at higher scope + return n; + }else{ + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + +} +int SortInference::getSortId( Node n ) { + Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n; + return getRepresentative( d_op_return_types[op] ); +} + +int SortInference::getSortId( Node f, Node v ) { + return getRepresentative( d_var_types[f][v] ); +} + +void SortInference::setSkolemVar( Node f, Node v, Node sk ){ + d_op_return_types[sk] = getSortId( f, v ); +} + }
\ No newline at end of file diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h index 1378a266c..0b1f96f85 100755..100644 --- a/src/util/sort_inference.h +++ b/src/util/sort_inference.h @@ -1,76 +1,76 @@ -/********************* */
-/*! \file sort_inference.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Pre-process step for performing sort inference
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__SORT_INFERENCE_H
-#define __CVC4__SORT_INFERENCE_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-
-namespace CVC4 {
-
-class SortInference{
-private:
- //for debugging
- //std::map< int, std::vector< Node > > d_type_eq_class;
-private:
- int sortCount;
- std::map< int, int > d_type_union_find;
- std::map< int, TypeNode > d_type_types;
- std::map< TypeNode, int > d_id_for_types;
- //for apply uf operators
- std::map< Node, int > d_op_return_types;
- std::map< Node, std::vector< int > > d_op_arg_types;
- //for bound variables
- std::map< Node, std::map< Node, int > > d_var_types;
- //get representative
- int getRepresentative( int t );
- void setEqual( int t1, int t2 );
- int getIdForType( TypeNode tn );
- void printSort( const char* c, int t );
- //process
- int process( Node n, std::map< Node, Node >& var_bound );
-private:
- //mapping from old symbols to new symbols
- std::map< Node, Node > d_symbol_map;
- //mapping from constants to new symbols
- std::map< TypeNode, std::map< Node, Node > > d_const_map;
- //number of subtypes generated
- std::map< TypeNode, int > d_subtype_count;
- //helper functions for simplify
- TypeNode getOrCreateTypeForId( int t, TypeNode pref );
- TypeNode getTypeForId( int t );
- Node getNewSymbol( Node old, TypeNode tn );
- //simplify
- Node simplify( Node n, std::map< Node, Node >& var_bound );
-public:
- SortInference() : sortCount( 0 ){}
- ~SortInference(){}
-
- void simplify( std::vector< Node >& assertions, bool doRewrite = false );
- int getSortId( Node n );
- int getSortId( Node f, Node v );
- //set that sk is the skolem variable of v for quantifier f
- void setSkolemVar( Node f, Node v, Node sk );
-};
-
-}
-
-#endif
+/********************* */ +/*! \file sort_inference.h + ** \verbatim + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Pre-process step for performing sort inference + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SORT_INFERENCE_H +#define __CVC4__SORT_INFERENCE_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class SortInference{ +private: + //for debugging + //std::map< int, std::vector< Node > > d_type_eq_class; +private: + int sortCount; + std::map< int, int > d_type_union_find; + std::map< int, TypeNode > d_type_types; + std::map< TypeNode, int > d_id_for_types; + //for apply uf operators + std::map< Node, int > d_op_return_types; + std::map< Node, std::vector< int > > d_op_arg_types; + //for bound variables + std::map< Node, std::map< Node, int > > d_var_types; + //get representative + int getRepresentative( int t ); + void setEqual( int t1, int t2 ); + int getIdForType( TypeNode tn ); + void printSort( const char* c, int t ); + //process + int process( Node n, std::map< Node, Node >& var_bound ); +private: + //mapping from old symbols to new symbols + std::map< Node, Node > d_symbol_map; + //mapping from constants to new symbols + std::map< TypeNode, std::map< Node, Node > > d_const_map; + //number of subtypes generated + std::map< TypeNode, int > d_subtype_count; + //helper functions for simplify + TypeNode getOrCreateTypeForId( int t, TypeNode pref ); + TypeNode getTypeForId( int t ); + Node getNewSymbol( Node old, TypeNode tn ); + //simplify + Node simplify( Node n, std::map< Node, Node >& var_bound ); +public: + SortInference() : sortCount( 0 ){} + ~SortInference(){} + + void simplify( std::vector< Node >& assertions, bool doRewrite = false ); + int getSortId( Node n ); + int getSortId( Node f, Node v ); + //set that sk is the skolem variable of v for quantifier f + void setSkolemVar( Node f, Node v, Node sk ); +}; + +} + +#endif |