1 /********************* */
2 /*! \file sort_inference.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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"
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
);
40 UnionFind( UnionFind
& c
){
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
); }
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
;
66 std::map
< Node
, std::map
< Node
, int > > d_var_types
;
68 void setEqual( int t1
, int t2
);
69 int getIdForType( TypeNode tn
);
70 void printSort( const char* c
, int t
);
72 int process( Node n
, std::map
< Node
, Node
>& var_bound
, std::map
< Node
, int >& visited
);
73 //for monotonicity inference
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 );
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
);
88 Node
simplifyNode( Node n
, std::map
< Node
, Node
>& var_bound
, TypeNode tnn
, std::map
< Node
, std::map
< TypeNode
, Node
> >& visited
);
90 Node
mkInjection( TypeNode tn1
, TypeNode tn2
);
94 SortInference() : sortCount( 1 ){}
97 void simplify( std::vector
< Node
>& assertions
, bool doSortInference
, bool doMonotonicyInference
);
98 //get sort id for term n
99 int getSortId( Node n
);
100 //get sort id for variable of quantified formula f
101 int getSortId( Node f
, Node v
);
102 //set that sk is the skolem variable of v for quantifier f
103 void setSkolemVar( Node f
, Node v
, Node sk
);
106 bool isWellSortedFormula( Node n
);
107 bool isWellSorted( Node n
);
108 //get constraints for being well-typed according to computed sub-types
109 void getSortConstraints( Node n
, SortInference::UnionFind
& uf
);
111 //list of all functions and the uninterpreted symbols they were replaced with
112 std::map
< Node
, Node
> d_model_replace_f
;
115 // store monotonicity for original sorts as well
116 std::map
< TypeNode
, bool > d_non_monotonic_sorts_orig
;
119 bool isMonotonic( TypeNode tn
);