1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 ast.h
7
8 Abstract:
9
10 Expression DAG
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2006-09-18.
15
16 Revision History:
17
18 --*/
19 #pragma once
20
21
22 #include "util/vector.h"
23 #include "util/hashtable.h"
24 #include "util/buffer.h"
25 #include "util/symbol.h"
26 #include "util/rational.h"
27 #include "util/hash.h"
28 #include "util/optional.h"
29 #include "util/trace.h"
30 #include "util/bit_vector.h"
31 #include "util/symbol_table.h"
32 #include "util/tptr.h"
33 #include "util/memory_manager.h"
34 #include "util/small_object_allocator.h"
35 #include "util/obj_ref.h"
36 #include "util/ref_vector.h"
37 #include "util/ref_pair_vector.h"
38 #include "util/ref_buffer.h"
39 #include "util/obj_mark.h"
40 #include "util/obj_hashtable.h"
41 #include "util/id_gen.h"
42 #include "util/map.h"
43 #include "util/parray.h"
44 #include "util/dictionary.h"
45 #include "util/chashtable.h"
46 #include "util/z3_exception.h"
47 #include "util/dependency.h"
48 #include "util/rlimit.h"
49
50 #define RECYCLE_FREE_AST_INDICES
51
52 #ifdef _MSC_VER
53 #pragma warning(disable : 4200)
54 #pragma warning(disable : 4355)
55 #endif
56
57 #ifdef _MSC_VER
58 # define Z3_NORETURN __declspec(noreturn)
59 #else
60 # define Z3_NORETURN [[noreturn]]
61 #endif
62
63 class ast;
64 class ast_manager;
65
66 /**
67 \brief Generic exception for AST related errors.
68
69 We used to use fatal_error_msg to report errors inside plugins.
70 */
71 class ast_exception : public default_exception {
72 public:
ast_exception(std::string && msg)73 ast_exception(std::string && msg) : default_exception(std::move(msg)) {}
74 };
75
76 typedef int family_id;
77 const family_id null_family_id = -1;
78
79 // -----------------------------------
80 //
81 // parameter
82 //
83 // -----------------------------------
84
85 /**
86 \brief Interpreted function declarations and sorts may have parameters that are used
87 to encode extra information associated with them.
88 */
89 class parameter {
90 public:
91 enum kind_t {
92 PARAM_INT,
93 PARAM_AST,
94 PARAM_SYMBOL,
95 PARAM_RATIONAL,
96 PARAM_DOUBLE,
97 // PARAM_EXTERNAL is used for handling decl_plugin specific parameters.
98 // For example, it is used for handling mpf numbers in float_decl_plugin,
99 // and irrational algebraic numbers in arith_decl_plugin.
100 // PARAM_EXTERNAL is not supported by z3 low level input format. This format is legacy, so
101 // this is not a big problem.
102 // Remark: PARAM_EXTERNAL can only be used to decorate theory decls.
103 PARAM_EXTERNAL
104 };
105 private:
106 kind_t m_kind;
107
108 // It is not possible to use tag pointers, since symbols are already tagged.
109 union {
110 int m_int; // for PARAM_INT
111 ast* m_ast; // for PARAM_AST
112 symbol m_symbol; // for PARAM_SYMBOL
113 rational* m_rational; // for PARAM_RATIONAL
114 double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
115 unsigned m_ext_id; // for PARAM_EXTERNAL
116 };
117
118 public:
119
parameter()120 parameter(): m_kind(PARAM_INT), m_int(0) {}
parameter(int val)121 explicit parameter(int val): m_kind(PARAM_INT), m_int(val) {}
parameter(unsigned val)122 explicit parameter(unsigned val): m_kind(PARAM_INT), m_int(val) {}
parameter(ast * p)123 explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {}
parameter(symbol const & s)124 explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s) {}
parameter(rational const & r)125 explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {}
parameter(rational && r)126 explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {}
parameter(double d)127 explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
parameter(const char * s)128 explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {}
parameter(const std::string & s)129 explicit parameter(const std::string &s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {}
parameter(unsigned ext_id,bool)130 explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
131 parameter(parameter const&);
132
parameter(parameter && other)133 parameter(parameter && other) noexcept : m_kind(other.m_kind) {
134 switch (other.m_kind) {
135 case PARAM_INT: m_int = other.get_int(); break;
136 case PARAM_AST: m_ast = other.get_ast(); break;
137 case PARAM_SYMBOL: m_symbol = other.m_symbol; break;
138 case PARAM_RATIONAL: m_rational = nullptr; std::swap(m_rational, other.m_rational); break;
139 case PARAM_DOUBLE: m_dval = other.m_dval; break;
140 case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
141 default:
142 UNREACHABLE();
143 break;
144 }
145 }
146
147 ~parameter();
148
149 parameter& operator=(parameter const& other);
150
get_kind()151 kind_t get_kind() const { return m_kind; }
is_int()152 bool is_int() const { return m_kind == PARAM_INT; }
is_ast()153 bool is_ast() const { return m_kind == PARAM_AST; }
is_symbol()154 bool is_symbol() const { return m_kind == PARAM_SYMBOL; }
is_rational()155 bool is_rational() const { return m_kind == PARAM_RATIONAL; }
is_double()156 bool is_double() const { return m_kind == PARAM_DOUBLE; }
is_external()157 bool is_external() const { return m_kind == PARAM_EXTERNAL; }
158
is_int(int & i)159 bool is_int(int & i) const { return is_int() && (i = get_int(), true); }
is_ast(ast * & a)160 bool is_ast(ast * & a) const { return is_ast() && (a = get_ast(), true); }
is_symbol(symbol & s)161 bool is_symbol(symbol & s) const { return is_symbol() && (s = get_symbol(), true); }
is_rational(rational & r)162 bool is_rational(rational & r) const { return is_rational() && (r = get_rational(), true); }
is_double(double & d)163 bool is_double(double & d) const { return is_double() && (d = get_double(), true); }
is_external(unsigned & id)164 bool is_external(unsigned & id) const { return is_external() && (id = get_ext_id(), true); }
165
166 /**
167 \brief This method is invoked when the parameter is
168 attached to a function declaration or sort.
169 */
170 void init_eh(ast_manager & m);
171 /**
172 \brief This method is invoked before the function
173 declaration or sort associated with the parameter is
174 deleted.
175 */
176 void del_eh(ast_manager & m, family_id fid);
177
get_int()178 int get_int() const { SASSERT(is_int()); return m_int; }
get_ast()179 ast * get_ast() const { SASSERT(is_ast()); return m_ast; }
get_symbol()180 symbol get_symbol() const { SASSERT(is_symbol()); return m_symbol; }
get_rational()181 rational const & get_rational() const { SASSERT(is_rational()); return *m_rational; }
get_double()182 double get_double() const { SASSERT(is_double()); return m_dval; }
get_ext_id()183 unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; }
184
185 bool operator==(parameter const & p) const;
186 bool operator!=(parameter const & p) const { return !operator==(p); }
187
188 unsigned hash() const;
189
190 std::ostream& display(std::ostream& out) const;
191 };
192
193 inline std::ostream& operator<<(std::ostream& out, parameter const & p) {
194 return p.display(out);
195 }
196
197 void display_parameters(std::ostream & out, unsigned n, parameter const * p);
198
199 // -----------------------------------
200 //
201 // family_manager
202 //
203 // -----------------------------------
204
205 /**
206 \brief Interpreted functions and sorts are grouped in families.
207 Each family has an unique ID. This class models the mapping
208 between symbols (family names) and the unique IDs.
209 */
210 class family_manager {
211 family_id m_next_id;
212 symbol_table<family_id> m_families;
213 svector<symbol> m_names;
214 public:
family_manager()215 family_manager():m_next_id(0) {}
216
217 /**
218 \brief Return the family_id for s, a new id is created if !has_family(s)
219
220 If has_family(s), then this method is equivalent to get_family_id(s)
221 */
222 family_id mk_family_id(symbol const & s);
223
224 /**
225 \brief Return the family_id for s, return null_family_id if s was not registered in the manager.
226 */
227 family_id get_family_id(symbol const & s) const;
228
229 bool has_family(symbol const & s) const;
230
get_dom(svector<symbol> & dom)231 void get_dom(svector<symbol>& dom) const { m_families.get_dom(dom); }
232
get_range(svector<family_id> & range)233 void get_range(svector<family_id> & range) const { m_families.get_range(range); }
234
get_name(family_id fid)235 symbol const & get_name(family_id fid) const { return fid >= 0 && fid < static_cast<int>(m_names.size()) ? m_names[fid] : symbol::null; }
236
has_family(family_id fid)237 bool has_family(family_id fid) const { return fid >= 0 && fid < static_cast<int>(m_names.size()); }
238 };
239
240 // -----------------------------------
241 //
242 // decl_info
243 //
244 // -----------------------------------
245
246 /**
247 \brief Each interpreted function declaration or sort has a kind.
248 Kinds are used to identify interpreted functions and sorts in a family.
249 */
250 typedef int decl_kind;
251 const decl_kind null_decl_kind = -1;
252
253 /**
254 \brief Interpreted function declarations and sorts are associated with
255 a family id, kind, and parameters.
256 */
257 class decl_info {
258 family_id m_family_id;
259 decl_kind m_kind;
260 vector<parameter> m_parameters;
261 public:
262 bool m_private_parameters;
263 decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind,
264 unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_params = false);
265
266 decl_info(decl_info const& other);
267
268 void init_eh(ast_manager & m);
269 void del_eh(ast_manager & m);
270
get_family_id()271 family_id get_family_id() const { return m_family_id; }
get_decl_kind()272 decl_kind get_decl_kind() const { return m_kind; }
get_num_parameters()273 unsigned get_num_parameters() const { return m_parameters.size(); }
get_parameter(unsigned idx)274 parameter const & get_parameter(unsigned idx) const { return m_parameters[idx]; }
get_parameters()275 parameter const * get_parameters() const { return m_parameters.begin(); }
private_parameters()276 bool private_parameters() const { return m_private_parameters; }
277
278 struct iterator {
279 decl_info const& d;
iteratoriterator280 iterator(decl_info const& d) : d(d) {}
beginiterator281 parameter const* begin() const { return d.get_parameters(); }
enditerator282 parameter const* end() const { return begin() + d.get_num_parameters(); }
283 };
parameters()284 iterator parameters() const { return iterator(*this); }
285
286 unsigned hash() const;
287 bool operator==(decl_info const & info) const;
288 };
289
290 std::ostream & operator<<(std::ostream & out, decl_info const & info);
291
292 // -----------------------------------
293 //
294 // sort_size
295 //
296 // -----------------------------------
297
298 /**
299 \brief Models the number of elements of a sort.
300 */
301 class sort_size {
302 enum kind_t {
303 SS_FINITE,
304 // For some sorts it may be too expensive to compute the
305 // number of elements precisely (e.g., arrays). In this
306 // cases, we mark the sort as too big. That is, the number
307 // of elements is at least bigger than 2^64.
308 SS_FINITE_VERY_BIG,
309 SS_INFINITE
310 } m_kind;
311 uint64_t m_size; // It is only meaningful if m_kind == SS_FINITE
sort_size(kind_t k,uint64_t r)312 sort_size(kind_t k, uint64_t r):m_kind(k), m_size(r) {}
313 public:
sort_size()314 sort_size():m_kind(SS_INFINITE), m_size(0) {}
sort_size(uint64_t const & sz)315 sort_size(uint64_t const & sz):m_kind(SS_FINITE), m_size(sz) {}
sort_size(rational const & r)316 explicit sort_size(rational const& r) {
317 if (r.is_uint64()) {
318 m_kind = SS_FINITE;
319 m_size = r.get_uint64();
320 }
321 else {
322 m_kind = SS_FINITE_VERY_BIG;
323 m_size = 0;
324 }
325 }
mk_infinite()326 static sort_size mk_infinite() { return sort_size(SS_INFINITE, 0); }
mk_very_big()327 static sort_size mk_very_big() { return sort_size(SS_FINITE_VERY_BIG, 0); }
mk_finite(uint64_t r)328 static sort_size mk_finite(uint64_t r) { return sort_size(SS_FINITE, r); }
329
is_infinite()330 bool is_infinite() const { return m_kind == SS_INFINITE; }
is_very_big()331 bool is_very_big() const { return m_kind == SS_FINITE_VERY_BIG; }
is_finite()332 bool is_finite() const { return m_kind == SS_FINITE; }
333
is_very_big_base2(unsigned power)334 static bool is_very_big_base2(unsigned power) { return power >= 64; }
335
size()336 uint64_t size() const { SASSERT(is_finite()); return m_size; }
337 };
338
339 std::ostream& operator<<(std::ostream& out, sort_size const & ss);
340
341 // -----------------------------------
342 //
343 // sort_info
344 //
345 // -----------------------------------
346
347 /**
348 \brief Extra information that may be attached to interpreted sorts.
349 */
350 class sort_info : public decl_info {
351 sort_size m_num_elements;
352 public:
353 sort_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind,
354 unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_parameters = false):
decl_info(family_id,k,num_parameters,parameters,private_parameters)355 decl_info(family_id, k, num_parameters, parameters, private_parameters) {
356 }
357
358 sort_info(family_id family_id, decl_kind k, uint64_t num_elements,
359 unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_parameters = false):
decl_info(family_id,k,num_parameters,parameters,private_parameters)360 decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) {
361 }
362
363 sort_info(family_id family_id, decl_kind k, sort_size const& num_elements,
364 unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_parameters = false):
decl_info(family_id,k,num_parameters,parameters,private_parameters)365 decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) {
366 }
sort_info(sort_info const & other)367 sort_info(sort_info const& other) : decl_info(other), m_num_elements(other.m_num_elements) {
368 }
sort_info(decl_info const & di,sort_size const & num_elements)369 sort_info(decl_info const& di, sort_size const& num_elements) :
370 decl_info(di), m_num_elements(num_elements) {}
371
is_infinite()372 bool is_infinite() const { return m_num_elements.is_infinite(); }
is_very_big()373 bool is_very_big() const { return m_num_elements.is_very_big(); }
get_num_elements()374 sort_size const & get_num_elements() const { return m_num_elements; }
set_num_elements(sort_size const & s)375 void set_num_elements(sort_size const& s) { m_num_elements = s; }
376 };
377
378 std::ostream & operator<<(std::ostream & out, sort_info const & info);
379
380 // -----------------------------------
381 //
382 // func_decl_info
383 //
384 // -----------------------------------
385
386 /**
387 \brief Extra information that may be attached to interpreted function decls.
388 */
389 struct func_decl_info : public decl_info {
390 bool m_left_assoc:1;
391 bool m_right_assoc:1;
392 bool m_flat_associative:1;
393 bool m_commutative:1;
394 bool m_chainable:1;
395 bool m_pairwise:1;
396 bool m_injective:1;
397 bool m_idempotent:1;
398 bool m_skolem:1;
399 bool m_lambda:1;
400
401 func_decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = nullptr);
402
is_associativefunc_decl_info403 bool is_associative() const { return m_left_assoc && m_right_assoc; }
is_left_associativefunc_decl_info404 bool is_left_associative() const { return m_left_assoc; }
is_right_associativefunc_decl_info405 bool is_right_associative() const { return m_right_assoc; }
is_flat_associativefunc_decl_info406 bool is_flat_associative() const { return m_flat_associative; }
is_commutativefunc_decl_info407 bool is_commutative() const { return m_commutative; }
is_chainablefunc_decl_info408 bool is_chainable() const { return m_chainable; }
is_pairwisefunc_decl_info409 bool is_pairwise() const { return m_pairwise; }
is_injectivefunc_decl_info410 bool is_injective() const { return m_injective; }
is_idempotentfunc_decl_info411 bool is_idempotent() const { return m_idempotent; }
is_skolemfunc_decl_info412 bool is_skolem() const { return m_skolem; }
is_lambdafunc_decl_info413 bool is_lambda() const { return m_lambda; }
414
415 void set_associative(bool flag = true) { m_left_assoc = flag; m_right_assoc = flag; }
416 void set_left_associative(bool flag = true) { m_left_assoc = flag; }
417 void set_right_associative(bool flag = true) { m_right_assoc = flag; }
418 void set_flat_associative(bool flag = true) { m_flat_associative = flag; }
419 void set_commutative(bool flag = true) { m_commutative = flag; }
420 void set_chainable(bool flag = true) { m_chainable = flag; }
421 void set_pairwise(bool flag = true) { m_pairwise = flag; }
422 void set_injective(bool flag = true) { m_injective = flag; }
423 void set_idempotent(bool flag = true) { m_idempotent = flag; }
424 void set_skolem(bool flag = true) { m_skolem = flag; }
425 void set_lambda(bool flag = true) { m_lambda = flag; }
426
427 bool operator==(func_decl_info const & info) const;
428
429 // Return true if the func_decl_info is equivalent to the null one (i.e., it does not contain any useful info).
is_nullfunc_decl_info430 bool is_null() const {
431 return
432 get_family_id() == null_family_id && !is_left_associative() && !is_right_associative() && !is_commutative() &&
433 !is_chainable() && !is_pairwise() && !is_injective() && !is_idempotent() && !is_skolem();
434 }
435 };
436
437 std::ostream & operator<<(std::ostream & out, func_decl_info const & info);
438
439 // -----------------------------------
440 //
441 // ast
442 //
443 // -----------------------------------
444
445 typedef enum { AST_APP, AST_VAR, AST_QUANTIFIER, AST_SORT, AST_FUNC_DECL } ast_kind;
446 char const * get_ast_kind_name(ast_kind k);
447
448 class shared_occs_mark;
449
450 class ast {
451 protected:
452 friend class ast_manager;
453
454 unsigned m_id;
455 unsigned m_kind:16;
456 // Warning: the marks should be used carefully, since they are shared.
457 unsigned m_mark1:1;
458 unsigned m_mark2:1;
459 // Private mark used by shared_occs functor
460 // Motivation for this field:
461 // - A mark cannot be used by more than one owner.
462 // So, it is only safe to use mark by "self-contained" code.
463 // They should be viewed as temporary information.
464 // - The functor shared_occs is used by some AST pretty printers.
465 // - So, a code that uses marks could not use the pretty printer if
466 // shared_occs used one of the public marks.
467 // - This was a constant source of assertion violations.
468 unsigned m_mark_shared_occs:1;
469 friend class shared_occs_mark;
mark_so(bool flag)470 void mark_so(bool flag) { m_mark_shared_occs = flag; }
reset_mark_so()471 void reset_mark_so() { m_mark_shared_occs = false; }
is_marked_so()472 bool is_marked_so() const { return m_mark_shared_occs; }
473 unsigned m_ref_count;
474 unsigned m_hash;
475 #ifdef Z3DEBUG
476 // In debug mode, we store who is the owner of the mark.
477 void * m_mark1_owner;
478 void * m_mark2_owner;
479 #endif
480
inc_ref()481 void inc_ref() {
482 SASSERT(m_ref_count < UINT_MAX);
483 m_ref_count ++;
484 }
485
dec_ref()486 void dec_ref() {
487 SASSERT(m_ref_count > 0);
488 --m_ref_count;
489 }
490
ast(ast_kind k)491 ast(ast_kind k):m_id(UINT_MAX), m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false), m_ref_count(0) {
492 DEBUG_CODE({
493 m_mark1_owner = 0;
494 m_mark2_owner = 0;
495 });
496 }
497 public:
get_id()498 unsigned get_id() const { return m_id; }
get_ref_count()499 unsigned get_ref_count() const { return m_ref_count; }
get_kind()500 ast_kind get_kind() const { return static_cast<ast_kind>(m_kind); }
hash()501 unsigned hash() const { return m_hash; }
502
503 #ifdef Z3DEBUG
mark1(bool flag,void * owner)504 void mark1(bool flag, void * owner) { SASSERT(m_mark1_owner == 0 || m_mark1_owner == owner); m_mark1 = flag; m_mark1_owner = owner; }
mark2(bool flag,void * owner)505 void mark2(bool flag, void * owner) { SASSERT(m_mark2_owner == 0 || m_mark2_owner == owner); m_mark2 = flag; m_mark2_owner = owner; }
reset_mark1(void * owner)506 void reset_mark1(void * owner) { SASSERT(m_mark1_owner == 0 || m_mark1_owner == owner); m_mark1 = false; m_mark1_owner = 0; }
reset_mark2(void * owner)507 void reset_mark2(void * owner) { SASSERT(m_mark2_owner == 0 || m_mark2_owner == owner); m_mark2 = false; m_mark2_owner = 0; }
is_marked1(void * owner)508 bool is_marked1(void * owner) const { SASSERT(m_mark1_owner == 0 || m_mark1_owner == owner); return m_mark1; }
is_marked2(void * owner)509 bool is_marked2(void * owner) const { SASSERT(m_mark2_owner == 0 || m_mark2_owner == owner); return m_mark2; }
510 #define AST_MARK1(A,F,O) A->mark1(F, O)
511 #define AST_MARK2(A,F,O) A->mark2(F, O)
512 #define AST_RESET_MARK1(A,O) A->reset_mark1(O)
513 #define AST_RESET_MARK2(A,O) A->reset_mark2(O)
514 #define AST_IS_MARKED1(A,O) A->is_marked1(O)
515 #define AST_IS_MARKED2(A,O) A->is_marked2(O)
516 #else
mark1(bool flag)517 void mark1(bool flag) { m_mark1 = flag; }
mark2(bool flag)518 void mark2(bool flag) { m_mark2 = flag; }
reset_mark1()519 void reset_mark1() { m_mark1 = false; }
reset_mark2()520 void reset_mark2() { m_mark2 = false; }
is_marked1()521 bool is_marked1() const { return m_mark1; }
is_marked2()522 bool is_marked2() const { return m_mark2; }
523 #define AST_MARK1(A,F,O) A->mark1(F)
524 #define AST_MARK2(A,F,O) A->mark2(F)
525 #define AST_RESET_MARK1(A,O) A->reset_mark1()
526 #define AST_RESET_MARK2(A,O) A->reset_mark2()
527 #define AST_IS_MARKED1(A,O) A->is_marked1()
528 #define AST_IS_MARKED2(A,O) A->is_marked2()
529 #endif
530 };
531
532 #define MATCH_TERNARY(_MATCHER_) \
533 bool _MATCHER_(expr const* n, expr*& a1, expr*& a2, expr *& a3) const { \
534 if (_MATCHER_(n) && to_app(n)->get_num_args() == 3) { \
535 a1 = to_app(n)->get_arg(0); a2 = to_app(n)->get_arg(1); a3 = to_app(n)->get_arg(2); return true; } \
536 return false; \
537 }
538
539 #define MATCH_BINARY(_MATCHER_) \
540 bool _MATCHER_(expr const* n, expr*& s, expr*& t) const { \
541 if (_MATCHER_(n) && to_app(n)->get_num_args() == 2) { s = to_app(n)->get_arg(0); t = to_app(n)->get_arg(1); return true; } \
542 return false; \
543 }
544
545 #define MATCH_UNARY(_MATCHER_) \
546 bool _MATCHER_(expr const* n, expr*& s) const { \
547 if (_MATCHER_(n) && to_app(n)->get_num_args() == 1) { s = to_app(n)->get_arg(0); return true; } \
548 return false; \
549 }
550
551 // -----------------------------------
552 //
553 // decl
554 //
555 // -----------------------------------
556
557 /**
558 The ids of expressions and declarations are in different ranges.
559 */
560 const unsigned c_first_decl_id = (1u << 31u);
561
562 /**
563 \brief Superclass for function declarations and sorts.
564 */
565 class decl : public ast {
566 protected:
567 friend class ast_manager;
568
569 symbol m_name;
570 decl_info * m_info;
571
decl(ast_kind k,symbol const & name,decl_info * info)572 decl(ast_kind k, symbol const & name, decl_info * info):ast(k), m_name(name), m_info(info) {}
573 public:
get_decl_id()574 unsigned get_decl_id() const { SASSERT(get_id() >= c_first_decl_id); return get_id() - c_first_decl_id; }
get_name()575 symbol const & get_name() const { return m_name; }
get_info()576 decl_info * get_info() const { return m_info; }
get_family_id()577 family_id get_family_id() const { return m_info == nullptr ? null_family_id : m_info->get_family_id(); }
get_decl_kind()578 decl_kind get_decl_kind() const { return m_info == nullptr ? null_decl_kind : m_info->get_decl_kind(); }
get_num_parameters()579 unsigned get_num_parameters() const { return m_info == nullptr ? 0 : m_info->get_num_parameters(); }
get_parameter(unsigned idx)580 parameter const & get_parameter(unsigned idx) const { return m_info->get_parameter(idx); }
get_parameters()581 parameter const * get_parameters() const { return m_info == nullptr ? nullptr : m_info->get_parameters(); }
private_parameters()582 bool private_parameters() const { return m_info != nullptr && m_info->private_parameters(); }
583
584 struct iterator {
585 decl const& d;
iteratoriterator586 iterator(decl const& d) : d(d) {}
beginiterator587 parameter const* begin() const { return d.get_parameters(); }
enditerator588 parameter const* end() const { return begin() + d.get_num_parameters(); }
589 };
parameters()590 iterator parameters() const { return iterator(*this); }
591
592
593 };
594
595 // -----------------------------------
596 //
597 // sort
598 //
599 // -----------------------------------
600
601 class sort : public decl {
602 friend class ast_manager;
603
get_obj_size()604 static unsigned get_obj_size() { return sizeof(sort); }
605
sort(symbol const & name,sort_info * info)606 sort(symbol const & name, sort_info * info):decl(AST_SORT, name, info) {}
607 public:
get_info()608 sort_info * get_info() const { return static_cast<sort_info*>(m_info); }
is_infinite()609 bool is_infinite() const { return get_info() == nullptr || get_info()->is_infinite(); }
is_very_big()610 bool is_very_big() const { return get_info() == nullptr || get_info()->is_very_big(); }
is_sort_of(family_id fid,decl_kind k)611 bool is_sort_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; }
get_num_elements()612 sort_size const & get_num_elements() const { return get_info()->get_num_elements(); }
set_num_elements(sort_size const & s)613 void set_num_elements(sort_size const& s) { get_info()->set_num_elements(s); }
get_size()614 unsigned get_size() const { return get_obj_size(); }
615 };
616
617 // -----------------------------------
618 //
619 // func_decl
620 //
621 // -----------------------------------
622
623 class func_decl : public decl {
624 friend class ast_manager;
625
626 unsigned m_arity;
627 sort * m_range;
628 sort * m_domain[0];
629
get_obj_size(unsigned arity)630 static unsigned get_obj_size(unsigned arity) { return sizeof(func_decl) + arity * sizeof(sort *); }
631
632 func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, func_decl_info * info);
633 public:
get_info()634 func_decl_info * get_info() const { return static_cast<func_decl_info*>(m_info); }
is_associative()635 bool is_associative() const { return get_info() != nullptr && get_info()->is_associative(); }
is_left_associative()636 bool is_left_associative() const { return get_info() != nullptr && get_info()->is_left_associative(); }
is_right_associative()637 bool is_right_associative() const { return get_info() != nullptr && get_info()->is_right_associative(); }
is_flat_associative()638 bool is_flat_associative() const { return get_info() != nullptr && get_info()->is_flat_associative(); }
is_commutative()639 bool is_commutative() const { return get_info() != nullptr && get_info()->is_commutative(); }
is_chainable()640 bool is_chainable() const { return get_info() != nullptr && get_info()->is_chainable(); }
is_pairwise()641 bool is_pairwise() const { return get_info() != nullptr && get_info()->is_pairwise(); }
is_injective()642 bool is_injective() const { return get_info() != nullptr && get_info()->is_injective(); }
is_skolem()643 bool is_skolem() const { return get_info() != nullptr && get_info()->is_skolem(); }
is_lambda()644 bool is_lambda() const { return get_info() != nullptr && get_info()->is_lambda(); }
is_idempotent()645 bool is_idempotent() const { return get_info() != nullptr && get_info()->is_idempotent(); }
get_arity()646 unsigned get_arity() const { return m_arity; }
get_domain(unsigned idx)647 sort * get_domain(unsigned idx) const { SASSERT(idx < get_arity()); return m_domain[idx]; }
get_domain()648 sort * const * get_domain() const { return m_domain; }
get_range()649 sort * get_range() const { return m_range; }
get_size()650 unsigned get_size() const { return get_obj_size(m_arity); }
begin()651 sort * const * begin() const { return get_domain(); }
end()652 sort * const * end() const { return get_domain() + get_arity(); }
653
654 };
655
656 // -----------------------------------
657 //
658 // expression
659 //
660 // -----------------------------------
661
662 /**
663 \brief Superclass for applications, variables and quantifiers.
664 */
665 class expr : public ast {
666 protected:
667 friend class ast_manager;
668
expr(ast_kind k)669 expr(ast_kind k):ast(k) {}
670 public:
671 };
672
673 // -----------------------------------
674 //
675 // application
676 //
677 // -----------------------------------
678
679 #define APP_DEPTH_NUM_BITS 16
680 const unsigned c_max_depth = ((1 << APP_DEPTH_NUM_BITS) - 1);
681 struct app_flags {
682 unsigned m_depth:APP_DEPTH_NUM_BITS; // if app is to deep, it doesn't matter.
683 unsigned m_ground:1; // application does not have free variables or nested quantifiers.
684 unsigned m_has_quantifiers:1; // application has nested quantifiers.
685 unsigned m_has_labels:1; // application has nested labels.
686 };
687
688 class app : public expr {
689 friend class ast_manager;
690
691 func_decl * m_decl;
692 unsigned m_num_args;
693 expr * m_args[0];
694
695 static app_flags g_constant_flags;
696
697 // remark: store term depth in the end of the app. the depth is only stored if the num_args > 0
get_obj_size(unsigned num_args)698 static unsigned get_obj_size(unsigned num_args) {
699 return num_args == 0 ? sizeof(app) : sizeof(app) + num_args * sizeof(expr *) + sizeof(app_flags);
700 }
701
702 friend class tmp_app;
703
flags()704 app_flags * flags() const { return m_num_args == 0 ? &g_constant_flags : reinterpret_cast<app_flags*>(const_cast<expr**>(m_args + m_num_args)); }
705
706 app(func_decl * decl, unsigned num_args, expr * const * args);
707 public:
get_decl()708 func_decl * get_decl() const { return m_decl; }
get_family_id()709 family_id get_family_id() const { return get_decl()->get_family_id(); }
get_decl_kind()710 decl_kind get_decl_kind() const { return get_decl()->get_decl_kind(); }
get_name()711 symbol const& get_name() const { return get_decl()->get_name(); }
get_num_parameters()712 unsigned get_num_parameters() const { return get_decl()->get_num_parameters(); }
get_parameter(unsigned idx)713 parameter const& get_parameter(unsigned idx) const { return get_decl()->get_parameter(idx); }
get_parameters()714 parameter const* get_parameters() const { return get_decl()->get_parameters(); }
is_app_of(family_id fid,decl_kind k)715 bool is_app_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; }
get_num_args()716 unsigned get_num_args() const { return m_num_args; }
get_arg(unsigned idx)717 expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
get_args()718 expr * const * get_args() const { return m_args; }
get_size()719 unsigned get_size() const { return get_obj_size(get_num_args()); }
begin()720 expr * const * begin() const { return m_args; }
end()721 expr * const * end() const { return m_args + m_num_args; }
722
get_depth()723 unsigned get_depth() const { return flags()->m_depth; }
is_ground()724 bool is_ground() const { return flags()->m_ground; }
has_quantifiers()725 bool has_quantifiers() const { return flags()->m_has_quantifiers; }
has_labels()726 bool has_labels() const { return flags()->m_has_labels; }
727 };
728
729 // -----------------------------------
730 //
731 // temporary application: little hack to avoid
732 // the creation of temporary expressions to just
733 // check the presence of the expression in
734 // some container/index.
735 //
736 // -----------------------------------
737
738 class tmp_app {
739 unsigned m_num_args;
740 char * m_data;
741 public:
tmp_app(unsigned num_args)742 tmp_app(unsigned num_args):
743 m_num_args(num_args) {
744 unsigned sz = app::get_obj_size(num_args);
745 m_data = alloc_svect(char, sz);
746 memset(m_data, 0, sz);
747 get_app()->m_num_args = m_num_args;
748 }
749
~tmp_app()750 ~tmp_app() {
751 dealloc_svect(m_data);
752 }
753
get_app()754 app * get_app() {
755 return reinterpret_cast<app*>(m_data);
756 }
757
get_args()758 expr ** get_args() {
759 return get_app()->m_args;
760 }
761
set_decl(func_decl * d)762 void set_decl(func_decl * d) {
763 get_app()->m_decl = d;
764 }
765
set_num_args(unsigned num_args)766 void set_num_args(unsigned num_args) {
767 get_app()->m_num_args = num_args;
768 }
769
set_arg(unsigned idx,expr * arg)770 void set_arg(unsigned idx, expr * arg) {
771 get_args()[idx] = arg;
772 SASSERT(get_app()->get_arg(idx) == arg);
773 }
774
copy(app * source)775 void copy(app * source) {
776 SASSERT(source->get_num_args() <= m_num_args);
777 new (m_data) app(source->get_decl(), source->get_num_args(), source->get_args());
778 SASSERT(get_app()->get_decl() == source->get_decl());
779 SASSERT(get_app()->get_arg(0) == source->get_arg(0));
780 SASSERT(get_app()->get_arg(1) == source->get_arg(1));
781 }
782
copy_swapping_args(app * source)783 void copy_swapping_args(app * source) {
784 SASSERT(source->get_num_args() == 2 && m_num_args >= 2);
785 expr * args[2] = { source->get_arg(1), source->get_arg(0) };
786 new (m_data) app(source->get_decl(), 2, args);
787 SASSERT(get_app()->get_decl() == source->get_decl());
788 SASSERT(get_app()->get_arg(0) == source->get_arg(1));
789 SASSERT(get_app()->get_arg(1) == source->get_arg(0));
790 }
791 };
792
793 // -----------------------------------
794 //
795 // variables
796 //
797 // -----------------------------------
798
799 class var : public expr {
800 friend class ast_manager;
801
802 unsigned m_idx;
803 sort * m_sort;
804
get_obj_size()805 static unsigned get_obj_size() { return sizeof(var); }
806
var(unsigned idx,sort * s)807 var(unsigned idx, sort * s):expr(AST_VAR), m_idx(idx), m_sort(s) {}
808 public:
get_idx()809 unsigned get_idx() const { return m_idx; }
get_sort()810 sort * get_sort() const { return m_sort; }
get_size()811 unsigned get_size() const { return get_obj_size(); }
812 };
813
814 // -----------------------------------
815 //
816 // quantifier
817 //
818 // -----------------------------------
819
820 enum quantifier_kind {
821 forall_k,
822 exists_k,
823 lambda_k
824 };
825
826 class quantifier : public expr {
827 friend class ast_manager;
828 quantifier_kind m_kind;
829 unsigned m_num_decls;
830 expr * m_expr;
831 sort * m_sort;
832 unsigned m_depth;
833 // extra fields
834 int m_weight;
835 bool m_has_unused_vars;
836 bool m_has_labels;
837 symbol m_qid;
838 symbol m_skid;
839 unsigned m_num_patterns;
840 unsigned m_num_no_patterns;
841 char m_patterns_decls[0];
842
get_obj_size(unsigned num_decls,unsigned num_patterns,unsigned num_no_patterns)843 static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) {
844 return sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*);
845 }
846
847 quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, sort* s,
848 int weight, symbol const & qid, symbol const & skid, unsigned num_patterns, expr * const * patterns,
849 unsigned num_no_patterns, expr * const * no_patterns);
850
851 quantifier(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, sort* sort);
852
853 public:
get_kind()854 quantifier_kind get_kind() const { return m_kind; }
855 // bool is_forall() const { return m_kind == forall_k; }
856 // bool is_exists() const { return m_kind == exists_k; }
857 // bool is_lambda() const { return m_kind == lambda_k; }
858
get_num_decls()859 unsigned get_num_decls() const { return m_num_decls; }
get_decl_sorts()860 sort * const * get_decl_sorts() const { return reinterpret_cast<sort * const *>(m_patterns_decls); }
get_decl_names()861 symbol const * get_decl_names() const { return reinterpret_cast<symbol const *>(get_decl_sorts() + m_num_decls); }
get_decl_sort(unsigned idx)862 sort * get_decl_sort(unsigned idx) const { return get_decl_sorts()[idx]; }
get_decl_name(unsigned idx)863 symbol const & get_decl_name(unsigned idx) const { return get_decl_names()[idx]; }
get_expr()864 expr * get_expr() const { return m_expr; }
865
get_sort()866 sort * get_sort() const { return m_sort; }
867
get_depth()868 unsigned get_depth() const { return m_depth; }
869
get_weight()870 int get_weight() const { return m_weight; }
get_qid()871 symbol const & get_qid() const { return m_qid; }
get_skid()872 symbol const & get_skid() const { return m_skid; }
get_num_patterns()873 unsigned get_num_patterns() const { return m_num_patterns; }
get_patterns()874 expr * const * get_patterns() const { return reinterpret_cast<expr * const *>(get_decl_names() + m_num_decls); }
get_pattern(unsigned idx)875 expr * get_pattern(unsigned idx) const { return get_patterns()[idx]; }
get_num_no_patterns()876 unsigned get_num_no_patterns() const { return m_num_no_patterns; }
get_no_patterns()877 expr * const * get_no_patterns() const { return reinterpret_cast<expr * const *>(get_decl_names() + m_num_decls); }
get_no_pattern(unsigned idx)878 expr * get_no_pattern(unsigned idx) const { return get_no_patterns()[idx]; }
has_patterns()879 bool has_patterns() const { return m_num_patterns > 0 || m_num_no_patterns > 0; }
get_size()880 unsigned get_size() const { return get_obj_size(m_num_decls, m_num_patterns, m_num_no_patterns); }
881
may_have_unused_vars()882 bool may_have_unused_vars() const { return m_has_unused_vars; }
set_no_unused_vars()883 void set_no_unused_vars() { m_has_unused_vars = false; }
884
has_labels()885 bool has_labels() const { return m_has_labels; }
886
887
get_num_children()888 unsigned get_num_children() const { return 1 + get_num_patterns() + get_num_no_patterns(); }
get_child(unsigned idx)889 expr * get_child(unsigned idx) const {
890 SASSERT(idx < get_num_children());
891 if (idx == 0)
892 return get_expr();
893 else if (idx <= get_num_patterns())
894 return get_pattern(idx - 1);
895 else
896 return get_no_pattern(idx - get_num_patterns() - 1);
897 }
898 };
899
900 // -----------------------------------
901 //
902 // AST recognisers
903 //
904 // -----------------------------------
905
is_decl(ast const * n)906 inline bool is_decl(ast const * n) { ast_kind k = n->get_kind(); return k == AST_FUNC_DECL || k == AST_SORT; }
is_sort(ast const * n)907 inline bool is_sort(ast const * n) { return n->get_kind() == AST_SORT; }
is_func_decl(ast const * n)908 inline bool is_func_decl(ast const * n) { return n->get_kind() == AST_FUNC_DECL; }
is_expr(ast const * n)909 inline bool is_expr(ast const * n) { return !is_decl(n); }
is_app(ast const * n)910 inline bool is_app(ast const * n) { return n->get_kind() == AST_APP; }
is_var(ast const * n)911 inline bool is_var(ast const * n) { return n->get_kind() == AST_VAR; }
is_var(ast const * n,unsigned & idx)912 inline bool is_var(ast const * n, unsigned& idx) { return is_var(n) && (idx = static_cast<var const*>(n)->get_idx(), true); }
is_quantifier(ast const * n)913 inline bool is_quantifier(ast const * n) { return n->get_kind() == AST_QUANTIFIER; }
is_forall(ast const * n)914 inline bool is_forall(ast const * n) { return is_quantifier(n) && static_cast<quantifier const *>(n)->get_kind() == forall_k; }
is_exists(ast const * n)915 inline bool is_exists(ast const * n) { return is_quantifier(n) && static_cast<quantifier const *>(n)->get_kind() == exists_k; }
is_lambda(ast const * n)916 inline bool is_lambda(ast const * n) { return is_quantifier(n) && static_cast<quantifier const *>(n)->get_kind() == lambda_k; }
917
918 // -----------------------------------
919 //
920 // AST coercions
921 //
922 // -----------------------------------
923
to_decl(ast * n)924 inline decl * to_decl(ast * n) { SASSERT(is_decl(n)); return static_cast<decl *>(n); }
to_sort(ast * n)925 inline sort * to_sort(ast * n) { SASSERT(is_sort(n)); return static_cast<sort *>(n); }
to_func_decl(ast * n)926 inline func_decl * to_func_decl(ast * n) { SASSERT(is_func_decl(n)); return static_cast<func_decl *>(n); }
to_expr(ast * n)927 inline expr * to_expr(ast * n) { SASSERT(is_expr(n)); return static_cast<expr *>(n); }
to_app(ast * n)928 inline app * to_app(ast * n) { SASSERT(is_app(n)); return static_cast<app *>(n); }
to_var(ast * n)929 inline var * to_var(ast * n) { SASSERT(is_var(n)); return static_cast<var *>(n); }
to_quantifier(ast * n)930 inline quantifier * to_quantifier(ast * n) { SASSERT(is_quantifier(n)); return static_cast<quantifier *>(n); }
931
to_decl(ast const * n)932 inline decl const * to_decl(ast const * n) { SASSERT(is_decl(n)); return static_cast<decl const *>(n); }
to_sort(ast const * n)933 inline sort const * to_sort(ast const * n) { SASSERT(is_sort(n)); return static_cast<sort const *>(n); }
to_func_decl(ast const * n)934 inline func_decl const * to_func_decl(ast const * n) { SASSERT(is_func_decl(n)); return static_cast<func_decl const *>(n); }
to_expr(ast const * n)935 inline expr const * to_expr(ast const * n) { SASSERT(is_expr(n)); return static_cast<expr const *>(n); }
to_app(ast const * n)936 inline app const * to_app(ast const * n) { SASSERT(is_app(n)); return static_cast<app const *>(n); }
to_var(ast const * n)937 inline var const * to_var(ast const * n) { SASSERT(is_var(n)); return static_cast<var const *>(n); }
to_quantifier(ast const * n)938 inline quantifier const * to_quantifier(ast const * n) { SASSERT(is_quantifier(n)); return static_cast<quantifier const *>(n); }
939
940 // -----------------------------------
941 //
942 // AST hash-consing
943 //
944 // -----------------------------------
945
946 unsigned get_node_hash(ast const * n);
947 bool compare_nodes(ast const * n1, ast const * n2);
948 unsigned get_node_size(ast const * n);
949 unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init);
950 unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init);
951 unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init);
952 unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init);
953 unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init);
954
955 // This is the internal comparison functor for hash-consing AST nodes.
956 struct ast_eq_proc {
operatorast_eq_proc957 bool operator()(ast const * n1, ast const * n2) const {
958 return n1->hash() == n2->hash() && compare_nodes(n1, n2);
959 }
960 };
961
962 class ast_translation;
963
964 class ast_table : public chashtable<ast*, obj_ptr_hash<ast>, ast_eq_proc> {
965 public:
966 void push_erase(ast * n);
967 ast* pop_erase();
968 };
969
970 // -----------------------------------
971 //
972 // decl_plugin
973 //
974 // -----------------------------------
975
976 /**
977 \brief Auxiliary data-structure used to initialize the parser symbol tables.
978 */
979 struct builtin_name {
980 decl_kind m_kind;
981 symbol m_name;
builtin_namebuiltin_name982 builtin_name(char const * name, decl_kind k) : m_kind(k), m_name(name) {}
builtin_namebuiltin_name983 builtin_name(const std::string &name, decl_kind k) : m_kind(k), m_name(name) {}
984 };
985
986 /**
987 \brief Each family of interpreted function declarations and sorts must provide a plugin
988 to build sorts and decls of the family.
989 */
990 class decl_plugin {
991 protected:
992 ast_manager * m_manager;
993 family_id m_family_id;
994
set_manager(ast_manager * m,family_id id)995 virtual void set_manager(ast_manager * m, family_id id) {
996 SASSERT(m_manager == nullptr);
997 m_manager = m;
998 m_family_id = id;
999 }
1000
inherit(decl_plugin * other_p,ast_translation &)1001 virtual void inherit(decl_plugin* other_p, ast_translation& ) { }
1002
1003 /**
1004 \brief Checks whether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line
1005 to that log. The theory solver should add some description of the meaning of the term in terms of the theory's
1006 internal reasoning to the end of the line and insert a line break.
1007
1008 \param a the term that should be described.
1009
1010 \return true if a log is being generated, false otherwise.
1011 */
1012 bool log_constant_meaning_prelude(app * a);
1013
1014 friend class ast_manager;
1015
1016 public:
decl_plugin()1017 decl_plugin():m_manager(nullptr), m_family_id(null_family_id) {}
1018
~decl_plugin()1019 virtual ~decl_plugin() {}
finalize()1020 virtual void finalize() {}
1021
1022
1023 virtual decl_plugin * mk_fresh() = 0;
1024
get_family_id()1025 family_id get_family_id() const { return m_family_id; }
1026
1027 virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) = 0;
1028
1029 virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
1030 unsigned arity, sort * const * domain, sort * range) = 0;
1031
1032 virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters,
1033 unsigned num_args, expr * const * args, sort * range);
1034
1035 /**
1036 \brief Return true if the plugin can decide whether two
1037 interpreted constants are equal or not.
1038
1039 For all a, b:
1040 If is_value(a) and is_value(b)
1041 Then,
1042 are_equal(a, b) != are_distinct(a, b)
1043
1044 The may be much more expensive than checking a pointer.
1045
1046 We need this because some plugin values are too expensive too canonize.
1047 */
is_value(app * a)1048 virtual bool is_value(app * a) const { return false; }
1049
1050 /**
1051 \brief Return true if \c a is a unique plugin value.
1052 The following property should hold for unique theory values:
1053
1054 For all a, b:
1055 If is_unique_value(a) and is_unique_value(b)
1056 Then,
1057 a == b (pointer equality)
1058 IFF
1059 the interpretations of these theory terms are equal.
1060
1061 \remark This is a stronger version of is_value.
1062 */
is_unique_value(app * a)1063 virtual bool is_unique_value(app * a) const { return false; }
1064
are_equal(app * a,app * b)1065 virtual bool are_equal(app * a, app * b) const { return a == b; }
1066
are_distinct(app * a,app * b)1067 virtual bool are_distinct(app * a, app * b) const { return a != b && is_unique_value(a) && is_unique_value(b); }
1068
1069 virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic = symbol()) {}
1070
1071 virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic = symbol()) {}
1072
get_some_value(sort * s)1073 virtual expr * get_some_value(sort * s) { return nullptr; }
1074
1075 // Return true if the interpreted sort s does not depend on uninterpreted sorts.
1076 // This may be the case, for example, for array and datatype sorts.
is_fully_interp(sort * s)1077 virtual bool is_fully_interp(sort * s) const { return true; }
1078
1079 // Event handlers for deleting/translating PARAM_EXTERNAL
del(parameter const & p)1080 virtual void del(parameter const & p) {}
translate(parameter const & p,decl_plugin & target)1081 virtual parameter translate(parameter const & p, decl_plugin & target) { UNREACHABLE(); return p; }
1082
is_considered_uninterpreted(func_decl * f)1083 virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
1084 };
1085
1086 // -----------------------------------
1087 //
1088 // basic_decl_plugin (i.e., builtin plugin)
1089 //
1090 // -----------------------------------
1091
1092 enum basic_sort_kind {
1093 BOOL_SORT,
1094 PROOF_SORT
1095 };
1096
1097 enum basic_op_kind {
1098 OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, LAST_BASIC_OP,
1099
1100 PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO, PR_BIND,
1101 PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
1102 PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
1103
1104 PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM,
1105
1106 PR_ASSUMPTION_ADD, PR_TH_ASSUMPTION_ADD, PR_LEMMA_ADD, PR_TH_LEMMA_ADD, PR_REDUNDANT_DEL, PR_CLAUSE_TRAIL,
1107
1108 PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_SKOLEMIZE,
1109 PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR
1110 };
1111
1112 class basic_decl_plugin : public decl_plugin {
1113 protected:
1114 sort * m_bool_sort;
1115 func_decl * m_true_decl;
1116 func_decl * m_false_decl;
1117 func_decl * m_and_decl;
1118 func_decl * m_or_decl;
1119 func_decl * m_xor_decl;
1120 func_decl * m_not_decl;
1121 func_decl * m_implies_decl;
1122 ptr_vector<func_decl> m_eq_decls; // cached eqs
1123 ptr_vector<func_decl> m_ite_decls; // cached ites
1124
1125 ptr_vector<func_decl> m_oeq_decls; // cached observational eqs
1126 sort * m_proof_sort;
1127 func_decl * m_undef_decl;
1128 func_decl * m_true_pr_decl;
1129 func_decl * m_asserted_decl;
1130 func_decl * m_goal_decl;
1131 func_decl * m_modus_ponens_decl;
1132 func_decl * m_reflexivity_decl;
1133 func_decl * m_symmetry_decl;
1134 func_decl * m_transitivity_decl;
1135 func_decl * m_quant_intro_decl;
1136 func_decl * m_and_elim_decl;
1137 func_decl * m_not_or_elim_decl;
1138 func_decl * m_rewrite_decl;
1139 func_decl * m_pull_quant_decl;
1140 func_decl * m_push_quant_decl;
1141 func_decl * m_elim_unused_vars_decl;
1142 func_decl * m_der_decl;
1143 func_decl * m_quant_inst_decl;
1144 ptr_vector<func_decl> m_monotonicity_decls;
1145 ptr_vector<func_decl> m_transitivity_star_decls;
1146 ptr_vector<func_decl> m_distributivity_decls;
1147 ptr_vector<func_decl> m_assoc_flat_decls;
1148 ptr_vector<func_decl> m_rewrite_star_decls;
1149
1150 func_decl * m_hypothesis_decl;
1151 func_decl * m_iff_true_decl;
1152 func_decl * m_iff_false_decl;
1153 func_decl * m_commutativity_decl;
1154 func_decl * m_def_axiom_decl;
1155 func_decl * m_lemma_decl;
1156 ptr_vector<func_decl> m_unit_resolution_decls;
1157
1158 func_decl * m_def_intro_decl;
1159 func_decl * m_iff_oeq_decl;
1160 func_decl * m_skolemize_decl;
1161 func_decl * m_mp_oeq_decl;
1162 func_decl * m_assumption_add_decl;
1163 func_decl * m_lemma_add_decl;
1164 func_decl * m_th_assumption_add_decl;
1165 func_decl * m_th_lemma_add_decl;
1166 func_decl * m_redundant_del_decl;
1167 ptr_vector<func_decl> m_apply_def_decls;
1168 ptr_vector<func_decl> m_nnf_pos_decls;
1169 ptr_vector<func_decl> m_nnf_neg_decls;
1170
1171 ptr_vector<func_decl> m_th_lemma_decls;
1172 func_decl * m_hyper_res_decl0;
1173
is_proof(decl_kind k)1174 static bool is_proof(decl_kind k) { return k > LAST_BASIC_OP; }
1175 bool check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const;
1176 bool check_proof_args(basic_op_kind k, unsigned num_args, expr * const * args) const;
1177 func_decl * mk_bool_op_decl(char const * name, basic_op_kind k, unsigned num_args = 0,
1178 bool asooc = false, bool comm = false, bool idempotent = false, bool flat_associative = false, bool chainable = false);
1179 func_decl * mk_implies_decl();
1180 func_decl * mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, bool inc_ref);
1181 func_decl * mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, func_decl*& fn);
1182 func_decl * mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, ptr_vector<func_decl> & cache);
1183 func_decl * mk_compressed_proof_decl(char const * name, basic_op_kind k, unsigned num_parents);
1184 func_decl * mk_proof_decl(basic_op_kind k, unsigned num_parents);
1185 func_decl * mk_proof_decl(basic_op_kind k, unsigned num_parameters, parameter const* params, unsigned num_parents);
1186 func_decl * mk_proof_decl(
1187 char const * name, basic_op_kind k,
1188 unsigned num_parameters, parameter const* params, unsigned num_parents);
1189
1190
1191 void set_manager(ast_manager * m, family_id id) override;
1192 func_decl * mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector<func_decl> & cache);
1193 func_decl * mk_ite_decl(sort * s);
1194 sort* join(sort* s1, sort* s2);
1195 sort* join(unsigned n, sort*const* srts);
1196 sort* join(unsigned n, expr*const* es);
1197 public:
1198 basic_decl_plugin();
1199
~basic_decl_plugin()1200 ~basic_decl_plugin() override {}
1201 void finalize() override;
1202
mk_fresh()1203 decl_plugin * mk_fresh() override {
1204 return alloc(basic_decl_plugin);
1205 }
1206
1207 sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) override;
1208
1209 func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
1210 unsigned arity, sort * const * domain, sort * range) override;
1211
1212 func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
1213 unsigned num_args, expr * const * args, sort * range) override;
1214
1215 void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
1216
1217 void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;
1218
1219 bool is_value(app* a) const override;
1220
1221 bool is_unique_value(app* a) const override;
1222
mk_bool_sort()1223 sort * mk_bool_sort() const { return m_bool_sort; }
mk_proof_sort()1224 sort * mk_proof_sort() const { return m_proof_sort; }
1225
1226 expr * get_some_value(sort * s) override;
1227 };
1228
1229 typedef app proof; /* a proof is just an application */
1230
1231 // -----------------------------------
1232 //
1233 // label_decl_plugin
1234 //
1235 // -----------------------------------
1236
1237 enum label_op_kind {
1238 OP_LABEL,
1239 OP_LABEL_LIT
1240 };
1241
1242 /**
1243 \brief Labels are identity functions used to mark sub-expressions.
1244 */
1245 class label_decl_plugin : public decl_plugin {
1246 symbol m_lblpos;
1247 symbol m_lblneg;
1248 symbol m_lbllit;
1249
1250 void set_manager(ast_manager * m, family_id id) override;
1251
1252 public:
1253 label_decl_plugin();
1254 ~label_decl_plugin() override;
1255
mk_fresh()1256 decl_plugin * mk_fresh() override { return alloc(label_decl_plugin); }
1257
1258 sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
1259
1260 /**
1261 contract: when label
1262 parameter[0] (int): 0 - if the label is negative, 1 - if positive.
1263 parameter[1] (symbol): label's tag.
1264 ...
1265 parameter[n-1] (symbol): label's tag.
1266
1267 contract: when label literal (they are always positive)
1268 parameter[0] (symbol): label's tag
1269 ...
1270 parameter[n-1] (symbol): label's tag.
1271 */
1272 func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
1273 unsigned arity, sort * const * domain, sort * range) override;
1274 };
1275
1276 // -----------------------------------
1277 //
1278 // pattern_decl_plugin
1279 //
1280 // -----------------------------------
1281
1282 enum pattern_op_kind {
1283 OP_PATTERN
1284 };
1285
1286 /**
1287 \brief Patterns are used to group expressions. These expressions are using during E-matching for
1288 heuristic quantifier instantiation.
1289 */
1290 class pattern_decl_plugin : public decl_plugin {
1291 public:
mk_fresh()1292 decl_plugin * mk_fresh() override { return alloc(pattern_decl_plugin); }
1293
1294 sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
1295
1296 func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
1297 unsigned arity, sort * const * domain, sort * range) override;
1298 };
1299
1300 // -----------------------------------
1301 //
1302 // model_value_plugin
1303 //
1304 // -----------------------------------
1305
1306 enum model_value_op_kind {
1307 OP_MODEL_VALUE
1308 };
1309
1310 /**
1311 \brief Values are used during model construction. All values are
1312 assumed to be different. Users should not use them, since they may
1313 introduce unsoundness if the sort of a value is finite.
1314
1315 Moreover, values should never be internalized in a logical context.
1316
1317 However, values can be used during evaluation (i.e., simplification).
1318
1319 \remark Model values can be viewed as the partition ids in Z3 1.x.
1320 */
1321 class model_value_decl_plugin : public decl_plugin {
1322 public:
model_value_decl_plugin()1323 model_value_decl_plugin() {}
1324
mk_fresh()1325 decl_plugin * mk_fresh() override { return alloc(model_value_decl_plugin); }
1326
1327 sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
1328
1329 /**
1330 contract:
1331 parameter[0]: (integer) value idx
1332 parameter[1]: (ast) sort of the value.
1333 */
1334 func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
1335 unsigned arity, sort * const * domain, sort * range) override;
1336
1337 bool is_value(app* n) const override;
1338
1339 bool is_unique_value(app* a) const override;
1340 };
1341
1342 // -----------------------------------
1343 //
1344 // user_sort_plugin for supporting user declared sorts in SMT2
1345 //
1346 // -----------------------------------
1347
1348 class user_sort_plugin : public decl_plugin {
1349 svector<symbol> m_sort_names;
1350 dictionary<int> m_name2decl_kind;
1351 public:
user_sort_plugin()1352 user_sort_plugin() {}
1353
1354 sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
1355 func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
1356 unsigned arity, sort * const * domain, sort * range) override;
1357 decl_kind register_name(symbol s);
1358 decl_plugin * mk_fresh() override;
1359 };
1360
1361
1362 // -----------------------------------
1363 //
1364 // Auxiliary functions
1365 //
1366 // -----------------------------------
1367
1368 // Return true if n is an application of d.
is_app_of(expr const * n,func_decl const * d)1369 inline bool is_app_of(expr const * n, func_decl const * d) { return n->get_kind() == AST_APP && to_app(n)->get_decl() == d; }
is_app_of(expr const * n,family_id fid,decl_kind k)1370 inline bool is_app_of(expr const * n, family_id fid, decl_kind k) { return n->get_kind() == AST_APP && to_app(n)->is_app_of(fid, k); }
is_sort_of(sort const * s,family_id fid,decl_kind k)1371 inline bool is_sort_of(sort const * s, family_id fid, decl_kind k) { return s->is_sort_of(fid, k); }
is_uninterp_const(expr const * n)1372 inline bool is_uninterp_const(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id; }
is_uninterp(expr const * n)1373 inline bool is_uninterp(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_family_id() == null_family_id; }
is_decl_of(func_decl const * d,family_id fid,decl_kind k)1374 inline bool is_decl_of(func_decl const * d, family_id fid, decl_kind k) { return d->get_family_id() == fid && d->get_decl_kind() == k; }
is_ground(expr const * n)1375 inline bool is_ground(expr const * n) { return is_app(n) && to_app(n)->is_ground(); }
is_non_ground(expr const * n)1376 inline bool is_non_ground(expr const * n) { return ( ! is_ground(n)); }
1377
get_depth(expr const * n)1378 inline unsigned get_depth(expr const * n) {
1379 if (is_app(n)) return to_app(n)->get_depth();
1380 else if (is_quantifier(n)) return to_quantifier(n)->get_depth();
1381 else return 1;
1382 }
1383
has_quantifiers(expr const * n)1384 inline bool has_quantifiers(expr const * n) {
1385 return is_app(n) ? to_app(n)->has_quantifiers() : is_quantifier(n);
1386 }
1387
has_labels(expr const * n)1388 inline bool has_labels(expr const * n) {
1389 if (is_app(n)) return to_app(n)->has_labels();
1390 else if (is_quantifier(n)) return to_quantifier(n)->has_labels();
1391 else return false;
1392 }
1393
1394 sort * get_sort(expr const * n);
1395
1396 class basic_recognizers {
1397 family_id m_fid;
1398 public:
basic_recognizers(family_id fid)1399 basic_recognizers(family_id fid):m_fid(fid) {}
is_bool(sort const * s)1400 bool is_bool(sort const * s) const { return is_sort_of(s, m_fid, BOOL_SORT); }
is_bool(expr const * n)1401 bool is_bool(expr const * n) const { return is_bool(get_sort(n)); }
is_or(expr const * n)1402 bool is_or(expr const * n) const { return is_app_of(n, m_fid, OP_OR); }
is_implies(expr const * n)1403 bool is_implies(expr const * n) const { return is_app_of(n, m_fid, OP_IMPLIES); }
is_and(expr const * n)1404 bool is_and(expr const * n) const { return is_app_of(n, m_fid, OP_AND); }
is_not(expr const * n)1405 bool is_not(expr const * n) const { return is_app_of(n, m_fid, OP_NOT); }
is_eq(expr const * n)1406 bool is_eq(expr const * n) const { return is_app_of(n, m_fid, OP_EQ); }
is_iff(expr const * n)1407 bool is_iff(expr const* n) const { return is_eq(n) && is_bool(to_app(n)->get_arg(0)); }
is_oeq(expr const * n)1408 bool is_oeq(expr const * n) const { return is_app_of(n, m_fid, OP_OEQ); }
is_distinct(expr const * n)1409 bool is_distinct(expr const * n) const { return is_app_of(n, m_fid, OP_DISTINCT); }
is_xor(expr const * n)1410 bool is_xor(expr const * n) const { return is_app_of(n, m_fid, OP_XOR); }
is_ite(expr const * n)1411 bool is_ite(expr const * n) const { return is_app_of(n, m_fid, OP_ITE); }
is_term_ite(expr const * n)1412 bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); }
is_true(expr const * n)1413 bool is_true(expr const * n) const { return is_app_of(n, m_fid, OP_TRUE); }
is_false(expr const * n)1414 bool is_false(expr const * n) const { return is_app_of(n, m_fid, OP_FALSE); }
is_complement_core(expr const * n1,expr const * n2)1415 bool is_complement_core(expr const * n1, expr const * n2) const {
1416 return (is_true(n1) && is_false(n2)) || (is_not(n1) && to_app(n1)->get_arg(0) == n2);
1417 }
is_complement(expr const * n1,expr const * n2)1418 bool is_complement(expr const * n1, expr const * n2) const { return is_complement_core(n1, n2) || is_complement_core(n2, n1); }
is_or(func_decl const * d)1419 bool is_or(func_decl const * d) const { return is_decl_of(d, m_fid, OP_OR); }
is_implies(func_decl const * d)1420 bool is_implies(func_decl const * d) const { return is_decl_of(d, m_fid, OP_IMPLIES); }
is_and(func_decl const * d)1421 bool is_and(func_decl const * d) const { return is_decl_of(d, m_fid, OP_AND); }
is_not(func_decl const * d)1422 bool is_not(func_decl const * d) const { return is_decl_of(d, m_fid, OP_NOT); }
is_eq(func_decl const * d)1423 bool is_eq(func_decl const * d) const { return is_decl_of(d, m_fid, OP_EQ); }
is_xor(func_decl const * d)1424 bool is_xor(func_decl const * d) const { return is_decl_of(d, m_fid, OP_XOR); }
is_ite(func_decl const * d)1425 bool is_ite(func_decl const * d) const { return is_decl_of(d, m_fid, OP_ITE); }
is_term_ite(func_decl const * d)1426 bool is_term_ite(func_decl const * d) const { return is_ite(d) && !is_bool(d->get_range()); }
is_distinct(func_decl const * d)1427 bool is_distinct(func_decl const * d) const { return is_decl_of(d, m_fid, OP_DISTINCT); }
1428
1429 MATCH_UNARY(is_not);
1430 MATCH_BINARY(is_eq);
1431 MATCH_BINARY(is_implies);
1432 MATCH_BINARY(is_and);
1433 MATCH_BINARY(is_or);
1434 MATCH_BINARY(is_xor);
1435 MATCH_TERNARY(is_and);
1436 MATCH_TERNARY(is_or);
is_iff(expr const * n,expr * & lhs,expr * & rhs)1437 bool is_iff(expr const* n, expr*& lhs, expr*& rhs) const { return is_eq(n, lhs, rhs) && is_bool(lhs); }
1438
1439 bool is_ite(expr const * n, expr * & t1, expr * & t2, expr * & t3) const;
1440 };
1441
1442 // -----------------------------------
1443 //
1444 // Get Some Value functor
1445 //
1446 // Functor for returning some value
1447 // of the given sort.
1448 //
1449 // -----------------------------------
1450 class some_value_proc {
1451 public:
1452 virtual expr * operator()(sort * s) = 0;
1453 };
1454
1455 // -----------------------------------
1456 //
1457 // Proof generation mode
1458 //
1459 // -----------------------------------
1460
1461 enum proof_gen_mode {
1462 PGM_DISABLED,
1463 PGM_ENABLED
1464 };
1465
1466 // -----------------------------------
1467 //
1468 // ast_manager
1469 //
1470 // -----------------------------------
1471
1472 class ast_manager {
1473 friend class basic_decl_plugin;
1474 protected:
1475 struct config {
1476 typedef ast_manager value_manager;
1477 typedef small_object_allocator allocator;
1478 static const bool ref_count = true;
1479 };
1480
1481 struct array_config : public config {
1482 static const bool preserve_roots = true;
1483 static const unsigned max_trail_sz = 16;
1484 static const unsigned factor = 2;
1485 };
1486
1487 struct expr_array_config : public array_config {
1488 typedef expr * value;
1489 };
1490
1491 typedef parray_manager<expr_array_config> expr_array_manager;
1492
1493 struct expr_dependency_config : public config {
1494 typedef expr * value;
1495 };
1496
1497 typedef dependency_manager<expr_dependency_config> expr_dependency_manager;
1498
1499 public:
1500 typedef expr_array_manager::ref expr_array;
1501 typedef expr_dependency_manager::dependency expr_dependency;
1502
1503 protected:
1504 struct expr_dependency_array_config : public array_config {
1505 typedef expr_dependency * value;
1506 };
1507
1508 typedef parray_manager<expr_dependency_array_config> expr_dependency_array_manager;
1509
1510 public:
1511 typedef expr_dependency_array_manager::ref expr_dependency_array;
1512
1513 void show_id_gen();
1514
1515 void update_fresh_id(ast_manager const& other);
1516
mk_fresh_id()1517 unsigned mk_fresh_id() { return ++m_fresh_id; }
1518
1519 protected:
1520 reslimit m_limit;
1521 small_object_allocator m_alloc;
1522 family_manager m_family_manager;
1523 expr_array_manager m_expr_array_manager;
1524 expr_dependency_manager m_expr_dependency_manager;
1525 expr_dependency_array_manager m_expr_dependency_array_manager;
1526 ptr_vector<decl_plugin> m_plugins;
1527 proof_gen_mode m_proof_mode;
1528 bool m_int_real_coercions; // If true, use hack that automatically introduces to_int/to_real when needed.
1529 family_id m_basic_family_id;
1530 family_id m_label_family_id;
1531 family_id m_pattern_family_id;
1532 family_id m_model_value_family_id;
1533 family_id m_user_sort_family_id;
1534 family_id m_arith_family_id;
1535 ast_table m_ast_table;
1536 obj_map<func_decl, quantifier*> m_lambda_defs;
1537 id_gen m_expr_id_gen;
1538 id_gen m_decl_id_gen;
1539 sort * m_bool_sort;
1540 sort * m_proof_sort;
1541 app * m_true;
1542 app * m_false;
1543 proof * m_undef_proof;
1544 unsigned m_fresh_id;
1545 bool m_debug_ref_count;
1546 u_map<unsigned> m_debug_free_indices;
1547 std::fstream* m_trace_stream;
1548 bool m_trace_stream_owner;
1549 #ifdef Z3DEBUG
1550 bool slow_not_contains(ast const * n);
1551 #endif
1552 ast_manager * m_format_manager; // hack for isolating format objects in a different manager.
1553 symbol m_lambda_def;
1554
1555 void init();
1556
1557 bool coercion_needed(func_decl * decl, unsigned num_args, expr * const * args);
1558
1559 void check_args(func_decl* f, unsigned n, expr* const* es);
1560
1561
1562 public:
1563 ast_manager(proof_gen_mode = PGM_DISABLED, char const * trace_file = nullptr, bool is_format_manager = false);
1564 ast_manager(proof_gen_mode, std::fstream * trace_stream, bool is_format_manager = false);
1565 ast_manager(ast_manager const & src, bool disable_proofs = false);
1566 ~ast_manager();
1567
1568 // propagate cancellation signal to decl_plugins
1569
has_trace_stream()1570 bool has_trace_stream() const { return m_trace_stream != nullptr; }
trace_stream()1571 std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }
1572 struct suspend_trace {
1573 ast_manager& m;
1574 std::fstream* m_tr;
suspend_tracesuspend_trace1575 suspend_trace(ast_manager& m): m(m), m_tr(m.m_trace_stream) { m.m_trace_stream = nullptr; }
~suspend_tracesuspend_trace1576 ~suspend_trace() { m.m_trace_stream = m_tr; }
1577 };
1578
enable_int_real_coercions(bool f)1579 void enable_int_real_coercions(bool f) { m_int_real_coercions = f; }
int_real_coercions()1580 bool int_real_coercions() const { return m_int_real_coercions; }
1581
1582 // Return true if s1 and s2 are equal, or coercions are enabled, and s1 and s2 are compatible.
1583 bool compatible_sorts(sort * s1, sort * s2) const;
1584 expr* coerce_to(expr* e, sort* s);
1585
1586 // For debugging purposes
display_free_ids(std::ostream & out)1587 void display_free_ids(std::ostream & out) { m_expr_id_gen.display_free_ids(out); out << "\n"; m_decl_id_gen.display_free_ids(out); }
1588
1589 void compact_memory();
1590
1591 void compress_ids();
1592
1593 // Equivalent to throw ast_exception(msg)
1594 Z3_NORETURN void raise_exception(char const * msg);
1595 Z3_NORETURN void raise_exception(std::string && s);
1596
1597 std::ostream& display(std::ostream& out, parameter const& p);
1598
is_format_manager()1599 bool is_format_manager() const { return m_format_manager == nullptr; }
1600
get_format_manager()1601 ast_manager & get_format_manager() { return is_format_manager() ? *this : *m_format_manager; }
1602
1603 void copy_families_plugins(ast_manager const & from);
1604
get_allocator()1605 small_object_allocator & get_allocator() { return m_alloc; }
1606
mk_family_id(symbol const & s)1607 family_id mk_family_id(symbol const & s) { return m_family_manager.mk_family_id(s); }
mk_family_id(char const * s)1608 family_id mk_family_id(char const * s) { return mk_family_id(symbol(s)); }
1609
get_family_id(symbol const & s)1610 family_id get_family_id(symbol const & s) const { return m_family_manager.get_family_id(s); }
get_family_id(char const * s)1611 family_id get_family_id(char const * s) const { return get_family_id(symbol(s)); }
1612
get_family_name(family_id fid)1613 symbol const & get_family_name(family_id fid) const { return m_family_manager.get_name(fid); }
1614
is_builtin_family_id(family_id fid)1615 bool is_builtin_family_id(family_id fid) const {
1616 return
1617 fid == null_family_id ||
1618 fid == m_basic_family_id ||
1619 fid == m_label_family_id ||
1620 fid == m_pattern_family_id ||
1621 fid == m_model_value_family_id ||
1622 fid == m_user_sort_family_id;
1623 }
1624
limit()1625 reslimit& limit() { return m_limit; }
1626 // bool canceled() { return !limit().inc(); }
inc()1627 bool inc() { return limit().inc(); }
1628
1629 void register_plugin(symbol const & s, decl_plugin * plugin);
1630
1631 void register_plugin(family_id id, decl_plugin * plugin);
1632
1633 decl_plugin * get_plugin(family_id fid) const;
1634
has_plugin(family_id fid)1635 bool has_plugin(family_id fid) const { return get_plugin(fid) != nullptr; }
1636
has_plugin(symbol const & s)1637 bool has_plugin(symbol const & s) const { return m_family_manager.has_family(s) && has_plugin(m_family_manager.get_family_id(s)); }
1638
get_dom(svector<symbol> & dom)1639 void get_dom(svector<symbol> & dom) const { m_family_manager.get_dom(dom); }
1640
get_range(svector<family_id> & range)1641 void get_range(svector<family_id> & range) const { m_family_manager.get_range(range); }
1642
get_basic_family_id()1643 family_id get_basic_family_id() const { return m_basic_family_id; }
1644
get_basic_decl_plugin()1645 basic_decl_plugin * get_basic_decl_plugin() const { return static_cast<basic_decl_plugin*>(get_plugin(m_basic_family_id)); }
1646
get_user_sort_family_id()1647 family_id get_user_sort_family_id() const { return m_user_sort_family_id; }
1648
get_user_sort_plugin()1649 user_sort_plugin * get_user_sort_plugin() const { return static_cast<user_sort_plugin*>(get_plugin(m_user_sort_family_id)); }
1650
1651 /**
1652 \brief Debugging support method: set the next expression identifier to be the least value id' s.t.
1653 - id' >= id
1654 - id' is not used by any AST in m_table
1655 - id' is not in the expression m_free_ids
1656
1657 This method should be only used to create small repros that exposes bugs in Z3.
1658 */
1659 void set_next_expr_id(unsigned id);
1660
1661 bool is_value(expr * e) const;
1662
1663 bool is_unique_value(expr * e) const;
1664
1665 bool are_equal(expr * a, expr * b) const;
1666
1667 bool are_distinct(expr * a, expr * b) const;
1668
contains(ast * a)1669 bool contains(ast * a) const { return m_ast_table.contains(a); }
1670
is_lambda_def(quantifier * q)1671 bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; }
1672 void add_lambda_def(func_decl* f, quantifier* q);
1673 quantifier* is_lambda_def(func_decl* f);
1674
1675
lambda_def_qid()1676 symbol const& lambda_def_qid() const { return m_lambda_def; }
1677
get_num_asts()1678 unsigned get_num_asts() const { return m_ast_table.size(); }
1679
debug_ref_count()1680 void debug_ref_count() { m_debug_ref_count = true; }
1681
inc_ref(ast * n)1682 void inc_ref(ast* n) {
1683 if (n)
1684 n->inc_ref();
1685 }
1686
dec_ref(ast * n)1687 void dec_ref(ast* n) {
1688 if (n) {
1689 n->dec_ref();
1690 if (n->get_ref_count() == 0)
1691 delete_node(n);
1692 }
1693 }
1694
1695 template<typename T>
inc_array_ref(unsigned sz,T * const * a)1696 void inc_array_ref(unsigned sz, T * const * a) {
1697 for(unsigned i = 0; i < sz; i++) {
1698 inc_ref(a[i]);
1699 }
1700 }
1701
1702 template<typename T>
dec_array_ref(unsigned sz,T * const * a)1703 void dec_array_ref(unsigned sz, T * const * a) {
1704 for(unsigned i = 0; i < sz; i++) {
1705 dec_ref(a[i]);
1706 }
1707 }
1708
1709 static unsigned get_node_size(ast const * n);
1710
get_allocation_size()1711 size_t get_allocation_size() const {
1712 return m_alloc.get_allocation_size();
1713 }
1714
1715 std::ostream& display(std::ostream& out) const;
1716
1717 protected:
1718 ast * register_node_core(ast * n);
1719
1720 template<typename T>
register_node(T * n)1721 T * register_node(T * n) {
1722 return static_cast<T *>(register_node_core(n));
1723 }
1724
1725 void delete_node(ast * n);
1726
allocate_node(unsigned size)1727 void * allocate_node(unsigned size) {
1728 return m_alloc.allocate(size);
1729 }
1730
deallocate_node(ast * n,unsigned sz)1731 void deallocate_node(ast * n, unsigned sz) {
1732 m_alloc.deallocate(sz, n);
1733 }
1734
1735 public:
get_sort(expr const * n)1736 sort * get_sort(expr const * n) const { return ::get_sort(n); }
1737 void check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const;
1738 void check_sorts_core(ast const * n) const;
1739 bool check_sorts(ast const * n) const;
1740
1741 bool is_bool(expr const * n) const;
is_bool(sort const * s)1742 bool is_bool(sort const * s) const { return s == m_bool_sort; }
get_eq_op(expr const * n)1743 decl_kind get_eq_op(expr const * n) const { return OP_EQ; }
1744
1745 private:
1746 sort * mk_sort(symbol const & name, sort_info * info);
1747
1748 public:
1749 sort * mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters);
1750
mk_uninterpreted_sort(symbol const & name)1751 sort * mk_uninterpreted_sort(symbol const & name) { return mk_uninterpreted_sort(name, 0, nullptr); }
1752
mk_sort(symbol const & name,sort_info const & info)1753 sort * mk_sort(symbol const & name, sort_info const & info) {
1754 if (info.get_family_id() == null_family_id) {
1755 return mk_uninterpreted_sort(name);
1756 }
1757 else {
1758 return mk_sort(name, &const_cast<sort_info &>(info));
1759 }
1760 }
1761
1762 sort * mk_sort(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = nullptr);
1763
1764 sort * substitute(sort* s, unsigned n, sort * const * src, sort * const * dst);
1765
mk_bool_sort()1766 sort * mk_bool_sort() const { return m_bool_sort; }
1767
mk_proof_sort()1768 sort * mk_proof_sort() const { return m_proof_sort; }
1769
1770 sort * mk_fresh_sort(char const * prefix = "");
1771
is_uninterp(sort const * s)1772 bool is_uninterp(sort const * s) const { return s->get_family_id() == null_family_id || s->get_family_id() == m_user_sort_family_id; }
1773
1774 /**
1775 \brief A sort is "fully" interpreted if it is interpreted,
1776 and doesn't depend on other uninterpreted sorts.
1777 */
1778 bool is_fully_interp(sort * s) const;
1779
1780 func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
1781 unsigned arity, sort * const * domain, sort * range = nullptr);
1782
1783 func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
1784 unsigned num_args, expr * const * args, sort * range = nullptr);
1785
1786 app * mk_app(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = nullptr,
1787 unsigned num_args = 0, expr * const * args = nullptr, sort * range = nullptr);
1788
1789 app * mk_app(family_id fid, decl_kind k, unsigned num_args, expr * const * args);
1790
1791 app * mk_app(family_id fid, decl_kind k, expr * arg);
1792
1793 app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2);
1794
1795 app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2, expr * arg3);
1796
mk_const(family_id fid,decl_kind k)1797 app * mk_const(family_id fid, decl_kind k) { return mk_app(fid, k, 0, static_cast<expr * const *>(nullptr)); }
1798 private:
1799 func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
1800 func_decl_info * info);
1801
1802 app * mk_app_core(func_decl * decl, expr * arg1, expr * arg2);
1803
1804 app * mk_app_core(func_decl * decl, unsigned num_args, expr * const * args);
1805
1806 public:
mk_func_decl(symbol const & name,unsigned arity,sort * const * domain,sort * range)1807 func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range) {
1808 return mk_func_decl(name, arity, domain, range, static_cast<func_decl_info *>(nullptr));
1809 }
1810
mk_func_decl(symbol const & name,unsigned arity,sort * const * domain,sort * range,func_decl_info const & info)1811 func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
1812 func_decl_info const & info) {
1813 if (info.is_null()) {
1814 return mk_func_decl(name, arity, domain, range, static_cast<func_decl_info *>(nullptr));
1815 }
1816 else {
1817 return mk_func_decl(name, arity, domain, range, & const_cast<func_decl_info&>(info));
1818 }
1819 }
1820
mk_func_decl(unsigned arity,sort * const * domain,func_decl_info const & info)1821 func_decl * mk_func_decl(unsigned arity, sort * const * domain, func_decl_info const & info) {
1822 return mk_func_decl(info.get_family_id(), info.get_decl_kind(), info.get_num_parameters(), info.get_parameters(),
1823 arity, domain);
1824 }
1825
mk_skolem_const_decl(symbol const & name,sort * s)1826 func_decl * mk_skolem_const_decl(symbol const& name, sort* s) {
1827 func_decl_info info;
1828 info.set_skolem(true);
1829 return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s, info);
1830 }
1831
mk_const_decl(const char * name,sort * s)1832 func_decl * mk_const_decl(const char* name, sort * s) {
1833 return mk_func_decl(symbol(name), static_cast<unsigned>(0), nullptr, s);
1834 }
1835
mk_const_decl(std::string const & name,sort * s)1836 func_decl * mk_const_decl(std::string const& name, sort * s) {
1837 return mk_func_decl(symbol(name.c_str()), static_cast<unsigned>(0), nullptr, s);
1838 }
1839
mk_const_decl(symbol const & name,sort * s)1840 func_decl * mk_const_decl(symbol const & name, sort * s) {
1841 return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s);
1842 }
1843
mk_const_decl(symbol const & name,sort * s,func_decl_info const & info)1844 func_decl * mk_const_decl(symbol const & name, sort * s, func_decl_info const & info) {
1845 return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s, info);
1846 }
1847
mk_func_decl(symbol const & name,sort * domain,sort * range,func_decl_info const & info)1848 func_decl * mk_func_decl(symbol const & name, sort * domain, sort * range, func_decl_info const & info) {
1849 return mk_func_decl(name, 1, &domain, range, info);
1850 }
1851
mk_func_decl(symbol const & name,sort * domain,sort * range)1852 func_decl * mk_func_decl(symbol const & name, sort * domain, sort * range) {
1853 return mk_func_decl(name, 1, &domain, range);
1854 }
1855
mk_func_decl(symbol const & name,sort * domain1,sort * domain2,sort * range,func_decl_info const & info)1856 func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range, func_decl_info const & info) {
1857 sort * d[2] = { domain1, domain2 };
1858 return mk_func_decl(name, 2, d, range, info);
1859 }
1860
mk_func_decl(symbol const & name,sort * domain1,sort * domain2,sort * range)1861 func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range) {
1862 sort * d[2] = { domain1, domain2 };
1863 return mk_func_decl(name, 2, d, range);
1864 }
1865
1866 func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
1867 bool assoc, bool comm = false, bool inj = false);
1868
1869 func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range, bool assoc, bool comm = false) {
1870 sort * d[2] = { domain1, domain2 };
1871 return mk_func_decl(name, 2, d, range, assoc, comm, false);
1872 }
1873
is_considered_uninterpreted(func_decl * f)1874 bool is_considered_uninterpreted(func_decl* f) {
1875 if (f->get_family_id() == null_family_id) {
1876 return true;
1877 }
1878 decl_plugin* p = get_plugin(f->get_family_id());
1879 return !p || p->is_considered_uninterpreted(f);
1880 }
1881
1882 app * mk_app(func_decl * decl, unsigned num_args, expr * const * args);
1883
mk_app(func_decl * decl,ref_vector<expr,ast_manager> const & args)1884 app* mk_app(func_decl* decl, ref_vector<expr, ast_manager> const& args) {
1885 return mk_app(decl, args.size(), args.c_ptr());
1886 }
1887
mk_app(func_decl * decl,ref_buffer<expr,ast_manager> const & args)1888 app* mk_app(func_decl* decl, ref_buffer<expr, ast_manager> const& args) {
1889 return mk_app(decl, args.size(), args.c_ptr());
1890 }
1891
mk_app(func_decl * decl,ref_vector<app,ast_manager> const & args)1892 app* mk_app(func_decl* decl, ref_vector<app, ast_manager> const& args) {
1893 return mk_app(decl, args.size(), (expr*const*)args.c_ptr());
1894 }
1895
mk_app(func_decl * decl,ptr_vector<expr> const & args)1896 app * mk_app(func_decl * decl, ptr_vector<expr> const& args) {
1897 return mk_app(decl, args.size(), args.c_ptr());
1898 }
1899
mk_app(func_decl * decl,ptr_buffer<expr> const & args)1900 app * mk_app(func_decl * decl, ptr_buffer<expr> const& args) {
1901 return mk_app(decl, args.size(), args.c_ptr());
1902 }
1903
mk_app(func_decl * decl,ptr_vector<app> const & args)1904 app * mk_app(func_decl * decl, ptr_vector<app> const& args) {
1905 return mk_app(decl, args.size(), (expr*const*)args.c_ptr());
1906 }
1907
mk_app(func_decl * decl,expr * const * args)1908 app * mk_app(func_decl * decl, expr * const * args) {
1909 return mk_app(decl, decl->get_arity(), args);
1910 }
1911
mk_app(func_decl * decl,expr * arg)1912 app * mk_app(func_decl * decl, expr * arg) {
1913 SASSERT(decl->get_arity() == 1);
1914 return mk_app(decl, 1, &arg);
1915 }
1916
mk_app(func_decl * decl,expr * arg1,expr * arg2)1917 app * mk_app(func_decl * decl, expr * arg1, expr * arg2) {
1918 SASSERT(decl->get_arity() == 2);
1919 expr * args[2] = { arg1, arg2 };
1920 return mk_app(decl, 2, args);
1921 }
1922
mk_app(func_decl * decl,expr * arg1,expr * arg2,expr * arg3)1923 app * mk_app(func_decl * decl, expr * arg1, expr * arg2, expr * arg3) {
1924 SASSERT(decl->get_arity() == 3);
1925 expr * args[3] = { arg1, arg2, arg3 };
1926 return mk_app(decl, 3, args);
1927 }
1928
mk_const(func_decl * decl)1929 app * mk_const(func_decl * decl) {
1930 SASSERT(decl->get_arity() == 0);
1931 return mk_app(decl, static_cast<unsigned>(0), static_cast<expr**>(nullptr));
1932 }
1933
mk_skolem_const(symbol const & name,sort * s)1934 app * mk_skolem_const(symbol const & name, sort * s) {
1935 return mk_const(mk_skolem_const_decl(name, s));
1936 }
1937
mk_const(symbol const & name,sort * s)1938 app * mk_const(symbol const & name, sort * s) {
1939 return mk_const(mk_const_decl(name, s));
1940 }
1941
mk_const(std::string const & name,sort * s)1942 app * mk_const(std::string const & name, sort * s) {
1943 return mk_const(mk_const_decl(name, s));
1944 }
1945
mk_const(char const * name,sort * s)1946 app * mk_const(char const* name, sort * s) {
1947 return mk_const(mk_const_decl(name, s));
1948 }
1949
1950 func_decl * mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity,
1951 sort * const * domain, sort * range, bool skolem = true);
1952
1953 func_decl * mk_fresh_func_decl(unsigned arity, sort * const * domain, sort * range, bool skolem = true) {
1954 return mk_fresh_func_decl(symbol::null, symbol::null, arity, domain, range, skolem);
1955 }
1956
1957 func_decl * mk_fresh_func_decl(char const * prefix, char const * suffix, unsigned arity,
1958 sort * const * domain, sort * range, bool skolem = true) {
1959 return mk_fresh_func_decl(symbol(prefix), symbol(suffix), arity, domain, range, skolem);
1960 }
1961
1962 func_decl * mk_fresh_func_decl(char const * prefix, unsigned arity, sort * const * domain, sort * range, bool skolem = true) {
1963 return mk_fresh_func_decl(symbol(prefix), symbol::null, arity, domain, range, skolem);
1964 }
1965
1966 app * mk_fresh_const(char const * prefix, sort * s, bool skolem = true) {
1967 return mk_const(mk_fresh_func_decl(prefix, 0, nullptr, s, skolem));
1968 }
1969
1970 app * mk_fresh_const(std::string const& prefix, sort * s, bool skolem = true) {
1971 return mk_fresh_const(prefix.c_str(), s, skolem);
1972 }
1973
1974 app * mk_fresh_const(symbol const& prefix, sort * s, bool skolem = true) {
1975 auto str = prefix.str();
1976 return mk_fresh_const(str.c_str(), s, skolem);
1977 }
1978
1979 symbol mk_fresh_var_name(char const * prefix = nullptr);
1980
1981 var * mk_var(unsigned idx, sort * ty);
1982
1983 app * mk_label(bool pos, unsigned num_names, symbol const * names, expr * n);
1984
1985 app * mk_label(bool pos, symbol const & name, expr * n);
1986
1987 bool is_label(expr const * n, bool & pos, buffer<symbol> & names) const;
1988
is_label(expr const * n,bool & pos,buffer<symbol> & names,expr * & l)1989 bool is_label(expr const * n, bool & pos, buffer<symbol> & names, expr*& l) const {
1990 return is_label(n, pos, names)?(l = to_app(n)->get_arg(0), true):false;
1991 }
1992
is_label(expr const * n)1993 bool is_label(expr const * n) const { return is_app_of(n, m_label_family_id, OP_LABEL); }
1994
is_label(expr const * n,expr * & l)1995 bool is_label(expr const * n, expr*& l) const {
1996 return is_label(n)?(l = to_app(n)->get_arg(0), true):false;
1997 }
1998
is_label(expr const * n,bool & pos)1999 bool is_label(expr const * n, bool& pos) const {
2000 if (is_app_of(n, m_label_family_id, OP_LABEL)) {
2001 pos = to_app(n)->get_decl()->get_parameter(0).get_int() != 0;
2002 return true;
2003 }
2004 else {
2005 return false;
2006 }
2007 }
2008
2009 app * mk_label_lit(unsigned num_names, symbol const * names);
2010
2011 app * mk_label_lit(symbol const & name);
2012
2013 bool is_label_lit(expr const * n, buffer<symbol> & names) const;
2014
is_label_lit(expr const * n)2015 bool is_label_lit(expr const * n) const { return is_app_of(n, m_label_family_id, OP_LABEL_LIT); }
2016
get_label_family_id()2017 family_id get_label_family_id() const { return m_label_family_id; }
2018
2019 app * mk_pattern(unsigned num_exprs, app * const * exprs);
2020
mk_pattern(app * expr)2021 app * mk_pattern(app * expr) { return mk_pattern(1, &expr); }
2022
2023 bool is_pattern(expr const * n) const;
2024
2025 bool is_pattern(expr const *n, ptr_vector<expr> &args);
2026
2027 public:
2028
2029 quantifier * mk_quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
2030 int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
2031 unsigned num_patterns = 0, expr * const * patterns = nullptr,
2032 unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr);
2033
2034 quantifier * mk_forall(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
2035 int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
2036 unsigned num_patterns = 0, expr * const * patterns = nullptr,
2037 unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
2038 return mk_quantifier(forall_k, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns,
2039 num_no_patterns, no_patterns);
2040 }
2041
2042 quantifier * mk_exists(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
2043 int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
2044 unsigned num_patterns = 0, expr * const * patterns = nullptr,
2045 unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
2046 return mk_quantifier(exists_k, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns,
2047 num_no_patterns, no_patterns);
2048 }
2049
2050 quantifier * mk_lambda(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body);
2051
2052 quantifier * update_quantifier(quantifier * q, unsigned new_num_patterns, expr * const * new_patterns, expr * new_body);
2053
2054 quantifier * update_quantifier(quantifier * q, unsigned new_num_patterns, expr * const * new_patterns, unsigned new_num_no_patterns, expr * const * new_no_patterns, expr * new_body);
2055
2056 quantifier * update_quantifier(quantifier * q, expr * new_body);
2057
2058 quantifier * update_quantifier_weight(quantifier * q, int new_weight);
2059
2060 quantifier * update_quantifier(quantifier * q, quantifier_kind new_kind, expr * new_body);
2061
2062 quantifier * update_quantifier(quantifier * q, quantifier_kind new_kind, unsigned new_num_patterns, expr * const * new_patterns, expr * new_body);
2063
2064 // -----------------------------------
2065 //
2066 // expr_array
2067 //
2068 // -----------------------------------
2069 public:
mk(expr_array & r)2070 void mk(expr_array & r) { m_expr_array_manager.mk(r); }
del(expr_array & r)2071 void del(expr_array & r) { m_expr_array_manager.del(r); }
copy(expr_array const & s,expr_array & r)2072 void copy(expr_array const & s, expr_array & r) { m_expr_array_manager.copy(s, r); }
size(expr_array const & r)2073 unsigned size(expr_array const & r) const { return m_expr_array_manager.size(r); }
empty(expr_array const & r)2074 bool empty(expr_array const & r) const { return m_expr_array_manager.empty(r); }
get(expr_array const & r,unsigned i)2075 expr * get(expr_array const & r, unsigned i) const { return m_expr_array_manager.get(r, i); }
set(expr_array & r,unsigned i,expr * v)2076 void set(expr_array & r, unsigned i, expr * v) { m_expr_array_manager.set(r, i, v); }
set(expr_array const & s,unsigned i,expr * v,expr_array & r)2077 void set(expr_array const & s, unsigned i, expr * v, expr_array & r) { m_expr_array_manager.set(s, i, v, r); }
push_back(expr_array & r,expr * v)2078 void push_back(expr_array & r, expr * v) { m_expr_array_manager.push_back(r, v); }
push_back(expr_array const & s,expr * v,expr_array & r)2079 void push_back(expr_array const & s, expr * v, expr_array & r) { m_expr_array_manager.push_back(s, v, r); }
pop_back(expr_array & r)2080 void pop_back(expr_array & r) { m_expr_array_manager.pop_back(r); }
pop_back(expr_array const & s,expr_array & r)2081 void pop_back(expr_array const & s, expr_array & r) { m_expr_array_manager.pop_back(s, r); }
unshare(expr_array & r)2082 void unshare(expr_array & r) { m_expr_array_manager.unshare(r); }
unfold(expr_array & r)2083 void unfold(expr_array & r) { m_expr_array_manager.unfold(r); }
reroot(expr_array & r)2084 void reroot(expr_array & r) { m_expr_array_manager.reroot(r); }
2085
2086 // -----------------------------------
2087 //
2088 // expr_dependency
2089 //
2090 // -----------------------------------
2091 public:
mk_empty_dependencies()2092 expr_dependency * mk_empty_dependencies() { return m_expr_dependency_manager.mk_empty(); }
2093 expr_dependency * mk_leaf(expr * t);
2094 expr_dependency * mk_join(unsigned n, expr * const * ts);
mk_join(expr_dependency * d1,expr_dependency * d2)2095 expr_dependency * mk_join(expr_dependency * d1, expr_dependency * d2) { return m_expr_dependency_manager.mk_join(d1, d2); }
inc_ref(expr_dependency * d)2096 void inc_ref(expr_dependency * d) { if (d) m_expr_dependency_manager.inc_ref(d); }
dec_ref(expr_dependency * d)2097 void dec_ref(expr_dependency * d) { if (d) m_expr_dependency_manager.dec_ref(d); }
2098 void linearize(expr_dependency * d, ptr_vector<expr> & ts);
contains(expr_dependency * d,expr * t)2099 bool contains(expr_dependency * d, expr * t) { return m_expr_dependency_manager.contains(d, t); }
2100
2101 // -----------------------------------
2102 //
2103 // expr_dependency_array
2104 //
2105 // -----------------------------------
2106 public:
mk(expr_dependency_array & r)2107 void mk(expr_dependency_array & r) { m_expr_dependency_array_manager.mk(r); }
del(expr_dependency_array & r)2108 void del(expr_dependency_array & r) { m_expr_dependency_array_manager.del(r); }
copy(expr_dependency_array const & s,expr_dependency_array & r)2109 void copy(expr_dependency_array const & s, expr_dependency_array & r) { m_expr_dependency_array_manager.copy(s, r); }
size(expr_dependency_array const & r)2110 unsigned size(expr_dependency_array const & r) const { return m_expr_dependency_array_manager.size(r); }
empty(expr_dependency_array const & r)2111 bool empty(expr_dependency_array const & r) const { return m_expr_dependency_array_manager.empty(r); }
get(expr_dependency_array const & r,unsigned i)2112 expr_dependency * get(expr_dependency_array const & r, unsigned i) const { return m_expr_dependency_array_manager.get(r, i); }
set(expr_dependency_array & r,unsigned i,expr_dependency * v)2113 void set(expr_dependency_array & r, unsigned i, expr_dependency * v) { m_expr_dependency_array_manager.set(r, i, v); }
set(expr_dependency_array const & s,unsigned i,expr_dependency * v,expr_dependency_array & r)2114 void set(expr_dependency_array const & s, unsigned i, expr_dependency * v, expr_dependency_array & r) {
2115 m_expr_dependency_array_manager.set(s, i, v, r);
2116 }
push_back(expr_dependency_array & r,expr_dependency * v)2117 void push_back(expr_dependency_array & r, expr_dependency * v) { m_expr_dependency_array_manager.push_back(r, v); }
push_back(expr_dependency_array const & s,expr_dependency * v,expr_dependency_array & r)2118 void push_back(expr_dependency_array const & s, expr_dependency * v, expr_dependency_array & r) {
2119 m_expr_dependency_array_manager.push_back(s, v, r);
2120 }
pop_back(expr_dependency_array & r)2121 void pop_back(expr_dependency_array & r) { m_expr_dependency_array_manager.pop_back(r); }
pop_back(expr_dependency_array const & s,expr_dependency_array & r)2122 void pop_back(expr_dependency_array const & s, expr_dependency_array & r) { m_expr_dependency_array_manager.pop_back(s, r); }
unshare(expr_dependency_array & r)2123 void unshare(expr_dependency_array & r) { m_expr_dependency_array_manager.unshare(r); }
unfold(expr_dependency_array & r)2124 void unfold(expr_dependency_array & r) { m_expr_dependency_array_manager.unfold(r); }
reroot(expr_dependency_array & r)2125 void reroot(expr_dependency_array & r) { m_expr_dependency_array_manager.reroot(r); }
2126
2127 // -----------------------------------
2128 //
2129 // Builtin operators
2130 //
2131 // -----------------------------------
2132
2133 public:
2134
is_or(expr const * n)2135 bool is_or(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_OR); }
is_implies(expr const * n)2136 bool is_implies(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_IMPLIES); }
is_and(expr const * n)2137 bool is_and(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_AND); }
is_not(expr const * n)2138 bool is_not(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_NOT); }
is_eq(expr const * n)2139 bool is_eq(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_EQ); }
is_iff(expr const * n)2140 bool is_iff(expr const * n) const { return is_eq(n) && is_bool(to_app(n)->get_arg(0)); }
is_oeq(expr const * n)2141 bool is_oeq(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_OEQ); }
is_distinct(expr const * n)2142 bool is_distinct(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_DISTINCT); }
is_xor(expr const * n)2143 bool is_xor(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_XOR); }
is_ite(expr const * n)2144 bool is_ite(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_ITE); }
is_term_ite(expr const * n)2145 bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); }
is_true(expr const * n)2146 bool is_true(expr const * n) const { return n == m_true; }
is_false(expr const * n)2147 bool is_false(expr const * n) const { return n == m_false; }
is_complement_core(expr const * n1,expr const * n2)2148 bool is_complement_core(expr const * n1, expr const * n2) const {
2149 return (is_true(n1) && is_false(n2)) || (is_not(n1) && to_app(n1)->get_arg(0) == n2);
2150 }
is_complement(expr const * n1,expr const * n2)2151 bool is_complement(expr const * n1, expr const * n2) const { return is_complement_core(n1, n2) || is_complement_core(n2, n1); }
2152
is_or(func_decl const * d)2153 bool is_or(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_OR); }
is_implies(func_decl const * d)2154