From b663c658c80cee918afe37222e62dd1e5db33f5c Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Oct 2013 14:22:36 -0500
Subject: Added support for converting unsorted problems to multi-sorted
 problems via sort inference and monotonicity.  Minor cleanup.

---
 src/util/sort_inference.cpp | 234 +++++++++++++++++++++++++++++++-------------
 src/util/sort_inference.h   |  12 ++-
 2 files changed, 174 insertions(+), 72 deletions(-)

(limited to 'src/util')

diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index b66d1cbe4..682e1e1e7 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -21,6 +21,7 @@
 
 #include "util/sort_inference.h"
 #include "theory/uf/options.h"
+#include "smt/options.h"
 //#include "theory/rewriter.h"
 
 using namespace CVC4;
@@ -75,10 +76,11 @@ bool SortInference::UnionFind::isValid() {
 }
 
 
-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 );
   }
 }
 
@@ -91,7 +93,25 @@ void SortInference::printSort( const char* c, int t ){
   }
 }
 
-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;
@@ -100,53 +120,62 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
   }
   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 ){
@@ -154,33 +183,79 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
       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 ){
@@ -234,7 +309,7 @@ int SortInference::getIdForType( TypeNode tn ){
 }
 
 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() ){
@@ -284,9 +359,14 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
   }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++ ){
@@ -306,7 +386,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
       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
@@ -333,13 +413,14 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
       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;
@@ -351,25 +432,24 @@ void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< 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 );
   }
 }
 
@@ -384,15 +464,14 @@ TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode 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]++;
+      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;
@@ -419,6 +498,10 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){
       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;
@@ -473,7 +556,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
         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() ){
@@ -519,7 +602,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
     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 );
@@ -534,6 +617,22 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
   }
 
 }
+
+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() ){
@@ -554,6 +653,7 @@ int SortInference::getSortId( Node f, Node v ) {
 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 );
   }
diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h
index 8f0fc5e9f..cd80f57d8 100644
--- a/src/util/sort_inference.h
+++ b/src/util/sort_inference.h
@@ -31,7 +31,8 @@ private:
   //all subsorts
   std::vector< int > d_sub_sorts;
   std::map< int, bool > d_non_monotonic_sorts;
-  void recordSubsort( int s );
+  std::map< TypeNode, std::vector< int > > d_type_sub_sorts;
+  void recordSubsort( TypeNode tn, int s );
 public:
   class UnionFind {
   public:
@@ -79,20 +80,21 @@ private:
   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 );
-
+  //make injection
+  Node mkInjection( TypeNode tn1, TypeNode tn2 );
+  //reset
+  void reset();
 public:
   SortInference() : sortCount( 1 ){}
   ~SortInference(){}
 
-  void simplify( std::vector< Node >& assertions, bool doRewrite = false );
+  bool simplify( std::vector< Node >& assertions );
   //get sort id for term n
   int getSortId( Node n );
   //get sort id for variable of quantified formula f
-- 
cgit v1.2.3