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