src/theory/sort_inference.h

   1 /*********************                                                        */
   2 /*! \file sort_inference.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Paul Meng
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 /** sort inference
  30  *
  31  * This class implements sort inference techniques, which rewrites a
  32  * formula F into an equisatisfiable formula F', where the symbols g in F are
  33  * replaced by others g', possibly of different types. For details, see e.g.:
  34  *   "Sort it out with Monotonicity" Claessen 2011
  35  *   "Non-Cyclic Sorts for First-Order Satisfiability" Korovin 2013.
  36  */
  37 class SortInference {
  38 private:
  39   //all subsorts
  40   std::vector< int > d_sub_sorts;
  41   std::map< int, bool > d_non_monotonic_sorts;
  42   std::map< TypeNode, std::vector< int > > d_type_sub_sorts;
  43   void recordSubsort( TypeNode tn, int s );
  44 public:
  45   class UnionFind {
  46   public:
  47     UnionFind(){}
  48     UnionFind( UnionFind& c ){
  49       set( c );
  50     }
  51     std::map< int, int > d_eqc;
  52     //pairs that must be disequal
  53     std::vector< std::pair< int, int > > d_deq;
  54     void print(const char * c);
  55     void clear() { d_eqc.clear(); d_deq.clear(); }
  56     void set( UnionFind& c );
  57     int getRepresentative( int t );
  58     void setEqual( int t1, int t2 );
  59     void setDisequal( int t1, int t2 ){ d_deq.push_back( std::pair< int, int >( t1, t2 ) ); }
  60     bool areEqual( int t1, int t2 ) { return getRepresentative( t1 )==getRepresentative( t2 ); }
  61     bool isValid();
  62   };
  63
  64  private:
  65   /** the id count for all subsorts we have allocated */
  66   int d_sortCount;
  67   UnionFind d_type_union_find;
  68   std::map< int, TypeNode > d_type_types;
  69   std::map< TypeNode, int > d_id_for_types;
  70   //for apply uf operators
  71   std::map< Node, int > d_op_return_types;
  72   std::map< Node, std::vector< int > > d_op_arg_types;
  73   std::map< Node, int > d_equality_types;
  74   //for bound variables
  75   std::map< Node, std::map< Node, int > > d_var_types;
  76   //get representative
  77   void setEqual( int t1, int t2 );
  78   int getIdForType( TypeNode tn );
  79   void printSort( const char* c, int t );
  80   //process
  81   int process( Node n, std::map< Node, Node >& var_bound, std::map< Node, int >& visited );
  82   // for monotonicity inference
  83  private:
  84   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 );
  85
  86 //for rewriting
  87 private:
  88   //mapping from old symbols to new symbols
  89   std::map< Node, Node > d_symbol_map;
  90   //mapping from constants to new symbols
  91   std::map< TypeNode, std::map< Node, Node > > d_const_map;
  92   //helper functions for simplify
  93   TypeNode getOrCreateTypeForId( int t, TypeNode pref );
  94   TypeNode getTypeForId( int t );
  95   Node getNewSymbol( Node old, TypeNode tn );
  96   //simplify
  97   Node simplifyNode(Node n,
  98                     std::map<Node, Node>& var_bound,
  99                     TypeNode tnn,
 100                     std::map<Node, Node>& model_replace_f,
 101                     std::map<Node, std::map<TypeNode, Node> >& visited);
 102   //make injection
 103   Node mkInjection( TypeNode tn1, TypeNode tn2 );
 104   //reset
 105   void reset();
 106
 107  public:
 108   SortInference() : d_sortCount(1) {}
 109   ~SortInference(){}
 110
 111   /** initialize
 112    *
 113    * This initializes this class. The input formula is indicated by assertions.
 114    */
 115   void initialize(const std::vector<Node>& assertions);
 116   /** simplify
 117    *
 118    * This returns the simplified form of formula n, based on the information
 119    * computed during initialization. The argument model_replace_f stores the
 120    * mapping between functions and their analog in the sort-inferred signature.
 121    * The argument visited is a cache of the internal results of simplifying
 122    * previous nodes with this class.
 123    *
 124    * Must call initialize() before this function.
 125    */
 126   Node simplify(Node n,
 127                 std::map<Node, Node>& model_replace_f,
 128                 std::map<Node, std::map<TypeNode, Node> >& visited);
 129   /** get new constraints
 130    *
 131    * This adds constraints to new_asserts that ensure the following.
 132    * Let F be the conjunction of assertions from the input. Let F' be the
 133    * conjunction of the simplified form of each conjunct in F. Let C be the
 134    * conjunction of formulas adding to new_asserts. Then, F and F' ^ C are
 135    * equisatisfiable.
 136    */
 137   void getNewAssertions(std::vector<Node>& new_asserts);
 138   /** compute monotonicity
 139    *
 140    * This computes whether sorts are monotonic (see e.g. Claessen 2011). If
 141    * this function is called, then calls to isMonotonic() can subsequently be
 142    * used to query whether sorts are monotonic.
 143    */
 144   void computeMonotonicity(const std::vector<Node>& assertions);
 145   /** return true if tn was inferred to be monotonic */
 146   bool isMonotonic(TypeNode tn);
 147   //get sort id for term n
 148   int getSortId( Node n );
 149   //get sort id for variable of quantified formula f
 150   int getSortId( Node f, Node v );
 151   //set that sk is the skolem variable of v for quantifier f
 152   void setSkolemVar( Node f, Node v, Node sk );
 153 public:
 154   //is well sorted
 155   bool isWellSortedFormula( Node n );
 156   bool isWellSorted( Node n );
 157   //get constraints for being well-typed according to computed sub-types
 158   void getSortConstraints( Node n, SortInference::UnionFind& uf );
 159 private:
 160   // store monotonicity for original sorts as well
 161  std::map<TypeNode, bool> d_non_monotonic_sorts_orig;
 162 };
 163
 164 }
 165
 166 #endif