#include "util/sort_inference.h"
#include "theory/uf/options.h"
+#include "smt/options.h"
//#include "theory/rewriter.h"
using namespace CVC4;
}
-void SortInference::recordSubsort( int s ){
+void SortInference::recordSubsort( TypeNode tn, int s ){
s = d_type_union_find.getRepresentative( s );
if( std::find( d_sub_sorts.begin(), d_sub_sorts.end(), s )==d_sub_sorts.end() ){
d_sub_sorts.push_back( s );
+ d_type_sub_sorts[tn].push_back( s );
}
}
}
}
-void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
+void SortInference::reset() {
+ d_sub_sorts.clear();
+ d_non_monotonic_sorts.clear();
+ d_type_sub_sorts.clear();
+ //reset info
+ sortCount = 1;
+ d_type_union_find.clear();
+ d_type_types.clear();
+ d_id_for_types.clear();
+ d_op_return_types.clear();
+ d_op_arg_types.clear();
+ d_var_types.clear();
+ //for rewriting
+ d_symbol_map.clear();
+ d_const_map.clear();
+}
+
+bool SortInference::simplify( std::vector< Node >& assertions ){
+ Trace("sort-inference") << "Calculating sort inference..." << std::endl;
//process all assertions
for( unsigned i=0; i<assertions.size(); i++ ){
Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
}
for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
Trace("sort-inference") << it->first << " : ";
+ TypeNode retTn = it->first.getType();
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++ ){
- recordSubsort( d_op_arg_types[ it->first ][i] );
+ recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] );
printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
Trace("sort-inference") << " ";
}
Trace("sort-inference") << ") -> ";
+ retTn = retTn[(int)retTn.getNumChildren()-1];
}
- recordSubsort( it->second );
+ recordSubsort( retTn, it->second );
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 );
+ for( unsigned i=0; i<it->first[0].getNumChildren(); i++ ){
+ recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] );
+ printSort( "sort-inference", it->second[it->first[0][i]] );
Trace("sort-inference") << std::endl;
}
Trace("sort-inference") << std::endl;
}
- //determine monotonicity of sorts
- for( unsigned i=0; i<assertions.size(); i++ ){
- Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
- std::map< Node, Node > var_bound;
- processMonotonic( assertions[i], true, true, var_bound );
- }
+ if( !options::ufssSymBreak() ){
+ bool rewritten = false;
+ //determine monotonicity of sorts
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
+ std::map< Node, Node > var_bound;
+ processMonotonic( assertions[i], true, true, var_bound );
+ }
- Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
- for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
- printSort( "sort-inference", d_sub_sorts[i] );
- if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
- Trace("sort-inference") << " is interpreted." << std::endl;
- }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
- Trace("sort-inference") << " is monotonic." << std::endl;
- }else{
- Trace("sort-inference") << " is not monotonic." << std::endl;
+ Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
+ for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
+ printSort( "sort-inference", d_sub_sorts[i] );
+ if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
+ Trace("sort-inference") << " is interpreted." << std::endl;
+ }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
+ Trace("sort-inference") << " is monotonic." << std::endl;
+ }else{
+ Trace("sort-inference") << " is not monotonic." << std::endl;
+ }
}
- }
- if( doRewrite ){
- //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)
+ //simplify all assertions by introducing new symbols wherever necessary
for( unsigned i=0; i<assertions.size(); i++ ){
+ Node prev = assertions[i];
std::map< Node, Node > var_bound;
assertions[i] = simplify( assertions[i], var_bound );
- Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl;
+ if( prev!=assertions[i] ){
+ rewritten = true;
+ Trace("sort-inference-rewrite") << prev << std::endl;
+ 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 ){
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?
+ //TODO: add lemma enforcing introduced constants to be distinct
}
- }else if( !options::ufssSymBreak() ){
- std::map< int, Node > constants;
- //just add a bunch of unit lemmas
+
+ //enforce constraints based on monotonicity
+ for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){
+ int nmonSort = -1;
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
+ nmonSort = it->second[i];
+ break;
+ }
+ }
+ if( nmonSort!=-1 ){
+ std::vector< Node > injections;
+ TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first );
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ if( it->second[i]!=nmonSort ){
+ TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first );
+ //make injection to nmonSort
+ Node a1 = mkInjection( new_tn, base_tn );
+ injections.push_back( a1 );
+ if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
+ //also must make injection from nmonSort to this
+ Node a2 = mkInjection( base_tn, new_tn );
+ injections.push_back( a2 );
+ }
+ }
+ }
+ Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl;
+ for( unsigned j=0; j<injections.size(); j++ ){
+ Trace("sort-inference-rewrite") << " " << injections[j] << std::endl;
+ }
+ assertions.insert( assertions.end(), injections.begin(), injections.end() );
+ if( !injections.empty() ){
+ rewritten = true;
+ }
+ }
+ }
+ //no sub-sort information is stored
+ reset();
+ return rewritten;
+ }
+ /*
+ else if( !options::ufssSymBreak() ){
+ //just add the unit lemmas between constants
+ std::map< TypeNode, std::map< int, Node > > constants;
for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
int rt = d_type_union_find.getRepresentative( it->second );
- if( d_op_arg_types[ it->first ].empty() && constants.find( rt )==constants.end() ){
- constants[ rt ] = it->first;
+ if( d_op_arg_types[ it->first ].empty() ){
+ TypeNode tn = it->first.getType();
+ if( constants[ tn ].find( rt )==constants[ tn ].end() ){
+ constants[ tn ][ rt ] = it->first;
+ }
}
}
//add unit lemmas for each constant
- Node first_const;
- for( std::map< int, Node >::iterator it = constants.begin(); it != constants.end(); ++it ){
- if( first_const.isNull() ){
- first_const = it->second;
- }else{
- Node eq = first_const.eqNode( it->second );
- //eq = Rewriter::rewrite( eq );
- Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
- assertions.push_back( eq );
+ for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){
+ Node first_const;
+ for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ if( first_const.isNull() ){
+ first_const = it2->second;
+ }else{
+ Node eq = first_const.eqNode( it2->second );
+ //eq = Rewriter::rewrite( eq );
+ Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
+ assertions.push_back( eq );
+ }
}
}
-
-
}
+ */
initialSortCount = sortCount;
+ return false;
}
void SortInference::setEqual( int t1, int t2 ){
}
int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
- Trace("sort-inference-debug") << "Process " << n << std::endl;
+ Trace("sort-inference-debug") << "...Process " << n << std::endl;
//add to variable bindings
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
if( d_var_types.find( n )!=d_var_types.end() ){
}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++;
+ if( n.getType().isBoolean() ){
+ //use booleans
+ d_op_return_types[op] = getIdForType( n.getType() );
+ }else{
+ //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++ ){
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 ){
+ }else if( n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM ){
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
retType = getIdForType( n.getType() );
}
}
- Trace("sort-inference-debug") << "Type( " << n << " ) = ";
+ Trace("sort-inference-debug") << "...Type( " << n << " ) = ";
printSort("sort-inference-debug", retType );
Trace("sort-inference-debug") << std::endl;
return retType;
}
void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ) {
+ Trace("sort-inference-debug") << "...Process monotonic " << pol << " " << hasPol << " " << n << std::endl;
if( n.getKind()==kind::FORALL ){
for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
var_bound[n[0][i]] = n;
}else if( n.getKind()==kind::EQUAL ){
if( !hasPol || pol ){
for( unsigned i=0; i<2; i++ ){
- if( var_bound.find( n[i] )==var_bound.end() ){
+ if( var_bound.find( n[i] )!=var_bound.end() ){
int sid = getSortId( var_bound[n[i]], n[i] );
d_non_monotonic_sorts[sid] = true;
break;
}
}
}
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bool npol = pol;
- bool nhasPol = hasPol;
- if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){
- npol = !npol;
- }
- if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){
- nhasPol = false;
- }
- processMonotonic( n[i], npol, nhasPol, var_bound );
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ bool npol = pol;
+ bool nhasPol = hasPol;
+ if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){
+ npol = !npol;
}
+ if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){
+ nhasPol = false;
+ }
+ processMonotonic( n[i], npol, nhasPol, var_bound );
}
}
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]++;
+ ss << "it_" << t << "_" << pref;
retType = NodeManager::currentNM()->mkSort( ss.str() );
}
+ Trace("sort-inference") << "-> Make type " << retType << " to correspond to ";
+ printSort("sort-inference", t );
+ Trace("sort-inference") << std::endl;
d_id_for_types[ retType ] = rt;
d_type_types[ rt ] = retType;
return retType;
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 if( old.getKind()==kind::BOUND_VARIABLE ){
+ std::stringstream ss;
+ ss << "b_" << old;
+ return NodeManager::currentNM()->mkBoundVar( ss.str(), tn );
}else{
std::stringstream ss;
ss << "i_$$_" << old;
Assert( false );
}
}
- return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
+ return NodeManager::currentNM()->mkNode( kind::EQUAL, children );
}else if( n.getKind()==kind::APPLY_UF ){
Node op = n.getOperator();
if( d_symbol_map.find( op )==d_symbol_map.end() ){
std::map< Node, Node >::iterator it = var_bound.find( n );
if( it!=var_bound.end() ){
return it->second;
- }else if( n.getKind() == kind::VARIABLE ){
+ }else if( n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM ){
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 );
}
}
+
+Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) {
+ std::vector< TypeNode > tns;
+ tns.push_back( tn1 );
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 );
+ Node f = NodeManager::currentNM()->mkSkolem( "inj_$$", typ, "injection for monotonicity constraint" );
+ Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl;
+ Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 );
+ Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 );
+ return NodeManager::currentNM()->mkNode( kind::FORALL,
+ NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ),
+ NodeManager::currentNM()->mkNode( kind::IMPLIES,
+ NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ),
+ v1.eqNode( v2 ) ) );
+}
+
int SortInference::getSortId( Node n ) {
Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n;
if( d_op_return_types.find( op )!=d_op_return_types.end() ){
void SortInference::setSkolemVar( Node f, Node v, Node sk ){
Trace("sort-inference-temp") << "Set skolem var for " << f << ", variable " << v << std::endl;
if( isWellSortedFormula( f ) && d_var_types.find( f )==d_var_types.end() ){
+ //calculate the sort for variables if not done so already
std::map< Node, Node > var_bound;
process( f, var_bound );
}
projects / cvc5.git / commitdiff