1 /********************* */
2 /*! \file sort_inference.h
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
12 ** \brief Pre-process step for performing sort inference
15 #include "cvc4_private.h"
17 #ifndef CVC4__SORT_INFERENCE_H
18 #define CVC4__SORT_INFERENCE_H
24 #include "expr/node.h"
25 #include "expr/type_node.h"
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.
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
);
48 UnionFind( UnionFind
& c
){
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
); }
65 /** the id count for all subsorts we have allocated */
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
;
75 std::map
< Node
, std::map
< Node
, int > > d_var_types
;
77 void setEqual( int t1
, int t2
);
78 int getIdForType( TypeNode tn
);
79 void printSort( const char* c
, int t
);
81 int process( Node n
, std::map
< Node
, Node
>& var_bound
, std::map
< Node
, int >& visited
);
82 // for monotonicity inference
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 );
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
);
97 Node
simplifyNode(Node n
,
98 std::map
<Node
, Node
>& var_bound
,
100 std::map
<Node
, Node
>& model_replace_f
,
101 std::map
<Node
, std::map
<TypeNode
, Node
> >& visited
);
103 Node
mkInjection( TypeNode tn1
, TypeNode tn2
);
108 SortInference() : d_sortCount(1) {}
113 * This initializes this class. The input formula is indicated by assertions.
115 void initialize(const std::vector
<Node
>& assertions
);
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.
124 * Must call initialize() before this function.
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
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
137 void getNewAssertions(std::vector
<Node
>& new_asserts
);
138 /** compute monotonicity
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.
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
);
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
);
160 // store monotonicity for original sorts as well
161 std::map
<TypeNode
, bool> d_non_monotonic_sorts_orig
;