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:
UnionFind()47     UnionFind(){}
UnionFind(UnionFind & c)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);
clear()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 );
setDisequal(int t1,int t2)59     void setDisequal( int t1, int t2 ){ d_deq.push_back( std::pair< int, int >( t1, t2 ) ); }
areEqual(int t1,int 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:
SortInference()108   SortInference() : d_sortCount(1) {}
~SortInference()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
167