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
|
#if ! defined _RelBody_h
#define _RelBody_h 1
#include <omega/pres_form.h>
#include <omega/pres_dnf.h>
namespace omega {
typedef enum {under_construction, compressed, uncompressed} Rel_Body_Status;
typedef unsigned char Rel_Unknown_Uses;
const Rel_Unknown_Uses no_u = 1;
const Rel_Unknown_Uses and_u = 2;
const Rel_Unknown_Uses or_u = 4;
//
// Relation body.
// Body and representative are separated to do reference counting.
//
class Rel_Body : public Formula {
public:
bool is_null() const;
inline Node_Type node_type() { return Op_Relation; }
inline bool is_set() const { return number_output == 0; }
int n_inp() const;
int n_out() const;
int n_set() const;
inline Variable_ID_Tuple *global_decls() { return &Symbolic; }
int max_ufs_arity();
int max_shared_ufs_arity();
int max_ufs_arity_of_set();
int max_ufs_arity_of_in();
int max_ufs_arity_of_out();
Variable_ID input_var(int nth);
Variable_ID output_var(int nth);
Variable_ID set_var(int nth);
Variable_ID get_local(const Variable_ID v);
Variable_ID get_local(const Global_Var_ID G);
Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of);
bool has_local(const Global_Var_ID G);
bool has_local(const Global_Var_ID G, Argument_Tuple of);
void name_input_var(int, Const_String);
void name_output_var(int, Const_String);
void name_set_var(int, Const_String);
F_And *and_with_and();
EQ_Handle and_with_EQ();
EQ_Handle and_with_EQ(const Constraint_Handle &c);
GEQ_Handle and_with_GEQ();
GEQ_Handle and_with_GEQ(const Constraint_Handle &c);
void print();
void print(FILE *output_file) { print(output_file, true); }
void print(FILE *output_file, bool printSym);
std::string print_variables_to_string(bool printSym);
void print_with_subs(FILE *output_file, bool printSym, bool newline);
void print_with_subs();
std::string print_with_subs_to_string(bool printSym, bool newline);
std::string print_outputs_with_subs_to_string();
std::string print_outputs_with_subs_to_string(int i);
std::string print_formula_to_string();
void prefix_print();
void prefix_print(FILE *output_file, int debug = 1);
bool is_satisfiable();
bool is_lower_bound_satisfiable();
bool is_upper_bound_satisfiable();
bool is_obvious_tautology();
bool is_definite_tautology();
bool is_unknown();
DNF* query_DNF();
DNF* query_DNF(int rdt_conjs, int rdt_constrs);
void simplify(int rdt_conjs = 0, int rdt_constrs = 0);
void finalize();
inline bool is_finalized() { return finalized; }
inline bool is_shared() { return ref_count > 1; }
void query_difference(Variable_ID v1, Variable_ID v2,
coef_t &lowerBound, coef_t &upperBound,
bool &quaranteed);
void query_variable_bounds(Variable_ID, coef_t &lowerBound, coef_t &upperBound);
coef_t query_variable_mod(Variable_ID v, coef_t factor);
Relation extract_dnf_by_carried_level(int level, int direction);
void make_level_carried_to(int level);
// these are only public to allow the creation of "null_rel"
Rel_Body();
~Rel_Body();
void setup_names();
private:
// These are manipulated primarily as parts of Relations
friend class Relation;
friend_rel_ops;
friend void remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel);
Rel_Unknown_Uses unknown_uses();
inline bool is_simplified() const { return (simplified_DNF!=NULL && get_children().empty()); }
bool is_compressed();
Conjunct *rm_first_conjunct();
Conjunct *single_conjunct();
bool has_single_conjunct();
void beautify();
void rearrange();
friend class EQ_Handle; // these set up names for printing
friend class GEQ_Handle; // and check if simplified
friend class Constraint_Handle; // and update coefficients
void compress();
void uncompress();
void interpret_unknown_as_true();
void interpret_unknown_as_false();
Rel_Body(int n_input, int n_output);
/* Rel_Body(Rel_Body *r); */
Rel_Body(Rel_Body *r, Conjunct *c);
Rel_Body &operator=(Rel_Body &r);
Rel_Body *clone();
inline Formula *formula() { return children().front(); }
inline Formula *rm_formula() { return children().remove_front(); }
bool can_add_child();
void reverse_leading_dir_info();
void invalidate_leading_info(int changed = -1) { Formula::invalidate_leading_info(changed); }
void enforce_leading_info(int guaranteed, int possible, int dir) { Formula::enforce_leading_info(guaranteed, possible, dir); }
// re-declare this so that Relation (a friend) can call it
DNF* DNFize();
void DNF_to_formula();
Conjunct *find_available_conjunct();
F_And *find_available_And();
/* === data === */
private:
int ref_count;
Rel_Body_Status status;
int number_input, number_output;
Tuple<Const_String> In_Names, Out_Names;
Variable_ID_Tuple Symbolic;
DNF* simplified_DNF;
short r_conjs; // are redundant conjuncts eliminated?
bool finalized;
bool _is_set;
};
} // namespace
#endif
|
