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