src/theory/sort_inference.h

   1 /*********************                                                        */
   2 /*! \file sort_inference.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Paul Meng, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Pre-process step for performing sort inference
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__SORT_INFERENCE_H
  18 #define __CVC4__SORT_INFERENCE_H
  19
  20 #include <iostream>
  21 #include <string>
  22 #include <vector>
  23 #include <map>
  24 #include "expr/node.h"
  25 #include "expr/type_node.h"
  26
  27 namespace CVC4 {
  28
  29 class SortInference {
  30 private:
  31   //all subsorts
  32   std::vector< int > d_sub_sorts;
  33   std::map< int, bool > d_non_monotonic_sorts;
  34   std::map< TypeNode, std::vector< int > > d_type_sub_sorts;
  35   void recordSubsort( TypeNode tn, int s );
  36 public:
  37   class UnionFind {
  38   public:
  39     UnionFind(){}
  40     UnionFind( UnionFind& c ){
  41       set( c );
  42     }
  43     std::map< int, int > d_eqc;
  44     //pairs that must be disequal
  45     std::vector< std::pair< int, int > > d_deq;
  46     void print(const char * c);
  47     void clear() { d_eqc.clear(); d_deq.clear(); }
  48     void set( UnionFind& c );
  49     int getRepresentative( int t );
  50     void setEqual( int t1, int t2 );
  51     void setDisequal( int t1, int t2 ){ d_deq.push_back( std::pair< int, int >( t1, t2 ) ); }
  52     bool areEqual( int t1, int t2 ) { return getRepresentative( t1 )==getRepresentative( t2 ); }
  53     bool isValid();
  54   };
  55 private:
  56   int sortCount;
  57   int initialSortCount;
  58   UnionFind d_type_union_find;
  59   std::map< int, TypeNode > d_type_types;
  60   std::map< TypeNode, int > d_id_for_types;
  61   //for apply uf operators
  62   std::map< Node, int > d_op_return_types;
  63   std::map< Node, std::vector< int > > d_op_arg_types;
  64   std::map< Node, int > d_equality_types;
  65   //for bound variables
  66   std::map< Node, std::map< Node, int > > d_var_types;
  67   //get representative
  68   void setEqual( int t1, int t2 );
  69   int getIdForType( TypeNode tn );
  70   void printSort( const char* c, int t );
  71   //process
  72   int process( Node n, std::map< Node, Node >& var_bound, std::map< Node, int >& visited );
  73 //for monotonicity inference
  74 private:
  75   void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, std::map< Node, std::map< int, bool > >& visited, bool typeMode = false );
  76
  77 //for rewriting
  78 private:
  79   //mapping from old symbols to new symbols
  80   std::map< Node, Node > d_symbol_map;
  81   //mapping from constants to new symbols
  82   std::map< TypeNode, std::map< Node, Node > > d_const_map;
  83   //helper functions for simplify
  84   TypeNode getOrCreateTypeForId( int t, TypeNode pref );
  85   TypeNode getTypeForId( int t );
  86   Node getNewSymbol( Node old, TypeNode tn );
  87   //simplify
  88   Node simplifyNode( Node n, std::map< Node, Node >& var_bound, TypeNode tnn, std::map< Node, std::map< TypeNode, Node > >& visited );
  89   //make injection
  90   Node mkInjection( TypeNode tn1, TypeNode tn2 );
  91   //reset
  92   void reset();
  93
  94  public:
  95   SortInference() : sortCount(1), initialSortCount() {}
  96   ~SortInference(){}
  97
  98   void simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference );
  99   //get sort id for term n
 100   int getSortId( Node n );
 101   //get sort id for variable of quantified formula f
 102   int getSortId( Node f, Node v );
 103   //set that sk is the skolem variable of v for quantifier f
 104   void setSkolemVar( Node f, Node v, Node sk );
 105 public:
 106   //is well sorted
 107   bool isWellSortedFormula( Node n );
 108   bool isWellSorted( Node n );
 109   //get constraints for being well-typed according to computed sub-types
 110   void getSortConstraints( Node n, SortInference::UnionFind& uf );
 111 public:
 112   //list of all functions and the uninterpreted symbols they were replaced with
 113   std::map< Node, Node > d_model_replace_f;
 114
 115 private:
 116   // store monotonicity for original sorts as well
 117   std::map< TypeNode, bool > d_non_monotonic_sorts_orig;
 118 public:
 119   //is monotonic
 120   bool isMonotonic( TypeNode tn );
 121 };
 122
 123 }
 124
 125 #endif