diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 3ca0012e7..53f891d28 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -596,7 +596,7 @@ def display_help(exit_code): else: print(" --parallel=num use cl option /MP with 'num' parallel processes") print(" --pypkgdir= Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR) - print(" -b , --build= subdirectory where Z3 will be built (default: build).") + print(" -b , --build= subdirectory where Z3 will be built (default: %s)." % BUILD_DIR) print(" --githash=hash include the given hash in the binaries.") print(" -d, --debug compile Z3 in debug mode.") print(" -t, --trace enable tracing in release mode.") @@ -742,7 +742,8 @@ def extract_c_includes(fname): # Given a path dir1/subdir2/subdir3 returns ../../.. def reverse_path(p): - l = p.split(os.sep) + # Filter out empty components (e.g. will have one if path ends in a slash) + l = list(filter(lambda x: len(x) > 0, p.split(os.sep))) n = len(l) r = '..' for i in range(1, n): diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 8df4234fa..25356a667 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -115,7 +115,7 @@ protected: func_decl * m_i_div_decl; func_decl * m_i_mod_decl; func_decl * m_i_rem_decl; - + func_decl * m_to_real_decl; func_decl * m_to_int_decl; func_decl * m_is_int_decl; @@ -140,7 +140,7 @@ protected: app * m_pi; app * m_e; - + app * m_0_pw_0_int; app * m_0_pw_0_real; func_decl * m_neg_root_decl; @@ -149,7 +149,7 @@ protected: func_decl * m_mod_0_decl; func_decl * m_u_asin_decl; func_decl * m_u_acos_decl; - + ptr_vector m_small_ints; ptr_vector m_small_reals; @@ -175,11 +175,11 @@ public: } virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range); virtual bool is_value(app * e) const; @@ -202,15 +202,34 @@ public: app * mk_numeral(sexpr const * p, unsigned i); app * mk_pi() const { return m_pi; } - + app * mk_e() const { return m_e; } app * mk_0_pw_0_int() const { return m_0_pw_0_int; } - + app * mk_0_pw_0_real() const { return m_0_pw_0_real; } virtual expr * get_some_value(sort * s); + virtual bool is_considered_uninterpreted(func_decl * f) { + if (f->get_family_id() != get_family_id()) + return false; + switch (f->get_decl_kind()) + { + case OP_0_PW_0_INT: + case OP_0_PW_0_REAL: + case OP_NEG_ROOT: + case OP_DIV_0: + case OP_IDIV_0: + case OP_MOD_0: + case OP_U_ASIN: + case OP_U_ACOS: + return true; + default: + return false; + } + return false; + } }; /** @@ -258,7 +277,7 @@ public: bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); } bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); } bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); } - + bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); } bool is_int(expr const * n) const { return is_int(get_sort(n)); } bool is_real(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); } @@ -275,7 +294,7 @@ public: MATCH_BINARY(is_le); MATCH_BINARY(is_ge); MATCH_BINARY(is_lt); - MATCH_BINARY(is_gt); + MATCH_BINARY(is_gt); MATCH_BINARY(is_mod); MATCH_BINARY(is_rem); MATCH_BINARY(is_div); @@ -297,25 +316,25 @@ class arith_util : public arith_recognizers { SASSERT(m_plugin != 0); return *m_plugin; } - + public: arith_util(ast_manager & m); ast_manager & get_manager() const { return m_manager; } - algebraic_numbers::manager & am() { - return plugin().am(); + algebraic_numbers::manager & am() { + return plugin().am(); } bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); } bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val); algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n); - + sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); } sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); } - app * mk_numeral(rational const & val, bool is_int) const { - return plugin().mk_numeral(val, is_int); + app * mk_numeral(rational const & val, bool is_int) const { + return plugin().mk_numeral(val, is_int); } app * mk_numeral(rational const & val, sort const * s) const { SASSERT(is_int(s) || is_real(s)); @@ -379,9 +398,9 @@ public: app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); } app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); } app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); } - + /** - \brief Return the equality (= lhs rhs), but it makes sure that + \brief Return the equality (= lhs rhs), but it makes sure that if one of the arguments is a numeral, then it will be in the right-hand-side; if none of them are numerals, then the left-hand-side has a smaller id than the right hand side. */ diff --git a/src/ast/ast.h b/src/ast/ast.h index 0c058fce8..0dba6039c 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -93,7 +93,7 @@ public: // PARAM_EXTERNAL is not supported by z3 low level input format. This format is legacy, so // this is not a big problem. // Remark: PARAM_EXTERNAL can only be used to decorate theory decls. - PARAM_EXTERNAL + PARAM_EXTERNAL }; private: kind_t m_kind; @@ -123,7 +123,7 @@ public: ~parameter(); parameter& operator=(parameter const& other); - + kind_t get_kind() const { return m_kind; } bool is_int() const { return m_kind == PARAM_INT; } bool is_ast() const { return m_kind == PARAM_AST; } @@ -131,7 +131,7 @@ public: bool is_rational() const { return m_kind == PARAM_RATIONAL; } bool is_double() const { return m_kind == PARAM_DOUBLE; } bool is_external() const { return m_kind == PARAM_EXTERNAL; } - + bool is_int(int & i) const { return is_int() && (i = get_int(), true); } bool is_ast(ast * & a) const { return is_ast() && (a = get_ast(), true); } bool is_symbol(symbol & s) const { return is_symbol() && (s = get_symbol(), true); } @@ -150,7 +150,7 @@ public: deleted. */ void del_eh(ast_manager & m, family_id fid); - + int get_int() const { SASSERT(is_int()); return m_int; } ast * get_ast() const { SASSERT(is_ast()); return m_ast; } symbol const & get_symbol() const { SASSERT(is_symbol()); return *(reinterpret_cast(m_symbol)); } @@ -162,7 +162,7 @@ public: bool operator!=(parameter const & p) const { return !operator==(p); } unsigned hash() const; - + std::ostream& display(std::ostream& out) const; }; @@ -192,7 +192,7 @@ public: /** \brief Return the family_id for s, a new id is created if !has_family(s) - + If has_family(s), then this method is equivalent to get_family_id(s) */ family_id mk_family_id(symbol const & s); @@ -201,11 +201,11 @@ public: \brief Return the family_id for s, return null_family_id if s was not registered in the manager. */ family_id get_family_id(symbol const & s) const; - + bool has_family(symbol const & s) const; void get_dom(svector& dom) const { m_families.get_dom(dom); } - + void get_range(svector & range) const { m_families.get_range(range); } symbol const & get_name(family_id fid) const { return fid >= 0 && fid < static_cast(m_names.size()) ? m_names[fid] : symbol::null; } @@ -220,15 +220,15 @@ public: // ----------------------------------- /** - \brief Each interpreted function declaration or sort has a kind. + \brief Each interpreted function declaration or sort has a kind. Kinds are used to identify interpreted functions and sorts in a family. */ -typedef int decl_kind; +typedef int decl_kind; const decl_kind null_decl_kind = -1; /** - \brief Interpreted function declarations and sorts are associated with - a family id, kind, and parameters. + \brief Interpreted function declarations and sorts are associated with + a family id, kind, and parameters. */ class decl_info { family_id m_family_id; @@ -236,22 +236,22 @@ class decl_info { vector m_parameters; public: bool m_private_parameters; - decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, + decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = 0, bool private_params = false); decl_info(decl_info const& other); ~decl_info() {} - + void init_eh(ast_manager & m); void del_eh(ast_manager & m); - + family_id get_family_id() const { return m_family_id; } decl_kind get_decl_kind() const { return m_kind; } unsigned get_num_parameters() const { return m_parameters.size(); } parameter const & get_parameter(unsigned idx) const { return m_parameters[idx]; } parameter const * get_parameters() const { return m_parameters.begin(); } bool private_parameters() const { return m_private_parameters; } - + unsigned hash() const; bool operator==(decl_info const & info) const; }; @@ -274,7 +274,7 @@ class sort_size { // number of elements precisely (e.g., arrays). In this // cases, we mark the sort as too big. That is, the number // of elements is at least bigger than 2^64. - SS_FINITE_VERY_BIG, + SS_FINITE_VERY_BIG, SS_INFINITE } m_kind; uint64 m_size; // It is only meaningful if m_kind == SS_FINITE @@ -296,13 +296,13 @@ public: static sort_size mk_infinite() { return sort_size(SS_INFINITE, 0); } static sort_size mk_very_big() { return sort_size(SS_FINITE_VERY_BIG, 0); } static sort_size mk_finite(uint64 r) { return sort_size(SS_FINITE, r); } - + bool is_infinite() const { return m_kind == SS_INFINITE; } bool is_very_big() const { return m_kind == SS_FINITE_VERY_BIG; } bool is_finite() const { return m_kind == SS_FINITE; } - + static bool is_very_big_base2(unsigned power) { return power >= 64; } - + uint64 size() const { SASSERT(is_finite()); return m_size; } }; @@ -320,16 +320,16 @@ std::ostream& operator<<(std::ostream& out, sort_size const & ss); class sort_info : public decl_info { sort_size m_num_elements; public: - sort_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, + sort_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = 0, bool private_parameters = false): decl_info(family_id, k, num_parameters, parameters, private_parameters) { } - + sort_info(family_id family_id, decl_kind k, uint64 num_elements, unsigned num_parameters = 0, parameter const * parameters = 0, bool private_parameters = false): decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) { } - + sort_info(family_id family_id, decl_kind k, sort_size const& num_elements, unsigned num_parameters = 0, parameter const * parameters = 0, bool private_parameters = false): decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) { @@ -337,7 +337,7 @@ public: sort_info(sort_info const& other) : decl_info(other), m_num_elements(other.m_num_elements) { } ~sort_info() {} - + bool is_infinite() const { return m_num_elements.is_infinite(); } bool is_very_big() const { return m_num_elements.is_very_big(); } sort_size const & get_num_elements() const { return m_num_elements; } @@ -367,7 +367,7 @@ struct func_decl_info : public decl_info { func_decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = 0); ~func_decl_info() {} - + bool is_associative() const { return m_left_assoc && m_right_assoc; } bool is_left_associative() const { return m_left_assoc; } bool is_right_associative() const { return m_right_assoc; } @@ -394,8 +394,8 @@ struct func_decl_info : public decl_info { // Return true if the func_decl_info is equivalent to the null one (i.e., it does not contain any useful info). bool is_null() const { - return - get_family_id() == null_family_id && !is_left_associative() && !is_right_associative() && !is_commutative() && + return + get_family_id() == null_family_id && !is_left_associative() && !is_right_associative() && !is_commutative() && !is_chainable() && !is_pairwise() && !is_injective() && !is_idempotent() && !is_skolem(); } }; @@ -416,7 +416,7 @@ class shared_occs_mark; class ast { protected: friend class ast_manager; - + unsigned m_id; unsigned m_kind:16; // Warning: the marks should be used carefully, since they are shared. @@ -428,10 +428,10 @@ protected: // So, it is only safe to use mark by "self-contained" code. // They should be viewed as temporary information. // - The functor shared_occs is used by some AST pretty printers. - // - So, a code that uses marks could not use the pretty printer if + // - So, a code that uses marks could not use the pretty printer if // shared_occs used one of the public marks. // - This was a constant source of assertion violations. - unsigned m_mark_shared_occs:1; + unsigned m_mark_shared_occs:1; friend class shared_occs_mark; void mark_so(bool flag) { m_mark_shared_occs = flag; } void reset_mark_so() { m_mark_shared_occs = false; } @@ -442,18 +442,18 @@ protected: // In debug mode, we store who is the owner of the mark. void * m_mark1_owner; void * m_mark2_owner; -#endif +#endif - void inc_ref() { + void inc_ref() { SASSERT(m_ref_count < UINT_MAX); - m_ref_count ++; + m_ref_count ++; } - - void dec_ref() { - SASSERT(m_ref_count > 0); - m_ref_count --; + + void dec_ref() { + SASSERT(m_ref_count > 0); + m_ref_count --; } - + 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) { DEBUG_CODE({ m_mark1_owner = 0; @@ -521,7 +521,7 @@ public: // ----------------------------------- /** - The ids of expressions and declarations are in different ranges. + The ids of expressions and declarations are in different ranges. */ const unsigned c_first_decl_id = (1u << 31u); @@ -556,9 +556,9 @@ public: class sort : public decl { friend class ast_manager; - + static unsigned get_obj_size() { return sizeof(sort); } - + sort(symbol const & name, sort_info * info):decl(AST_SORT, name, info) {} public: sort_info * get_info() const { return static_cast(m_info); } @@ -577,13 +577,13 @@ public: class func_decl : public decl { friend class ast_manager; - + unsigned m_arity; sort * m_range; sort * m_domain[0]; - - static unsigned get_obj_size(unsigned arity) { return sizeof(func_decl) + arity * sizeof(sort *); } - + + static unsigned get_obj_size(unsigned arity) { return sizeof(func_decl) + arity * sizeof(sort *); } + func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, func_decl_info * info); public: func_decl_info * get_info() const { return static_cast(m_info); } @@ -616,7 +616,7 @@ public: class expr : public ast { protected: friend class ast_manager; - + expr(ast_kind k):ast(k) {} public: }; @@ -641,20 +641,20 @@ struct app_flags { class app : public expr { friend class ast_manager; - + func_decl * m_decl; unsigned m_num_args; expr * m_args[0]; - + static app_flags g_constant_flags; - + // remark: store term depth in the end of the app. the depth is only stored if the num_args > 0 - static unsigned get_obj_size(unsigned num_args) { - return num_args == 0 ? sizeof(app) : sizeof(app) + num_args * sizeof(expr *) + sizeof(app_flags); - } + static unsigned get_obj_size(unsigned num_args) { + return num_args == 0 ? sizeof(app) : sizeof(app) + num_args * sizeof(expr *) + sizeof(app_flags); + } friend class tmp_app; - + app_flags * flags() const { return m_num_args == 0 ? &g_constant_flags : reinterpret_cast(const_cast(m_args + m_num_args)); } app(func_decl * decl, unsigned num_args, expr * const * args); @@ -706,11 +706,11 @@ public: expr ** get_args() { return get_app()->m_args; } - + void set_decl(func_decl * d) { get_app()->m_decl = d; } - + void set_num_args(unsigned num_args) { get_app()->m_num_args = num_args; } @@ -746,12 +746,12 @@ public: class var : public expr { friend class ast_manager; - + unsigned m_idx; sort * m_sort; - + static unsigned get_obj_size() { return sizeof(var); } - + var(unsigned idx, sort * s):expr(AST_VAR), m_idx(idx), m_sort(s) {} public: unsigned get_idx() const { return m_idx; } @@ -775,13 +775,13 @@ class quantifier : public expr { int m_weight; bool m_has_unused_vars; bool m_has_labels; - symbol m_qid; - symbol m_skid; + symbol m_qid; + symbol m_skid; unsigned m_num_patterns; unsigned m_num_no_patterns; char m_patterns_decls[0]; - - static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) { + + static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) { return sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*); } @@ -811,7 +811,7 @@ public: expr * get_no_pattern(unsigned idx) const { return get_no_patterns()[idx]; } bool has_patterns() const { return m_num_patterns > 0 || m_num_no_patterns > 0; } unsigned get_size() const { return get_obj_size(m_num_decls, m_num_patterns, m_num_no_patterns); } - + bool may_have_unused_vars() const { return m_has_unused_vars; } void set_no_unused_vars() { m_has_unused_vars = false; } @@ -884,8 +884,8 @@ unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init); // This is the internal comparison functor for hash-consing AST nodes. struct ast_eq_proc { - bool operator()(ast const * n1, ast const * n2) const { - return n1->hash() == n2->hash() && compare_nodes(n1, n2); + bool operator()(ast const * n1, ast const * n2) const { + return n1->hash() == n2->hash() && compare_nodes(n1, n2); } }; @@ -917,18 +917,18 @@ class decl_plugin { protected: ast_manager * m_manager; family_id m_family_id; - + virtual void set_manager(ast_manager * m, family_id id) { SASSERT(m_manager == 0); m_manager = m; m_family_id = id; } - + friend class ast_manager; - + public: decl_plugin():m_manager(0), m_family_id(null_family_id) {} - + virtual ~decl_plugin() {} virtual void finalize() {} @@ -936,24 +936,24 @@ public: virtual decl_plugin * mk_fresh() = 0; family_id get_family_id() const { return m_family_id; } - + virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) = 0; - - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) = 0; - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters, unsigned num_args, expr * const * args, sort * range); /** \brief Return true if the plugin can decide whether two interpreted constants are equal or not. - + For all a, b: If is_value(a) and is_value(b) Then, are_equal(a, b) != are_distinct(a, b) - + The may be much more expensive than checking a pointer. We need this because some plugin values are too expensive too canonize. @@ -963,7 +963,7 @@ public: /** \brief Return true if \c a is a unique plugin value. The following property should hold for unique theory values: - + For all a, b: If is_unique_value(a) and is_unique_value(b) Then, @@ -976,11 +976,11 @@ public: virtual bool is_unique_value(app * a) const { return false; } virtual bool are_equal(app * a, app * b) const { return a == b && is_unique_value(a) && is_unique_value(b); } - + virtual bool are_distinct(app * a, app * b) const { return a != b && is_unique_value(a) && is_unique_value(b); } - + virtual void get_op_names(svector & op_names, symbol const & logic = symbol()) {} - + virtual void get_sort_names(svector & sort_names, symbol const & logic = symbol()) {} virtual expr * get_some_value(sort * s) { return 0; } @@ -989,9 +989,11 @@ public: // This may be the case, for example, for array and datatype sorts. virtual bool is_fully_interp(sort const * s) const { return true; } - // Event handlers for deleting/translating PARAM_EXTERNAL + // Event handlers for deleting/translating PARAM_EXTERNAL virtual void del(parameter const & p) {} virtual parameter translate(parameter const & p, decl_plugin & target) { UNREACHABLE(); return p; } + + virtual bool is_considered_uninterpreted(func_decl * f) { return false; } }; // ----------------------------------- @@ -1009,12 +1011,12 @@ enum basic_op_kind { OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, OP_INTERP, LAST_BASIC_OP, 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_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT, + PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT, PR_PULL_QUANT_STAR, PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST, - + PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM, - PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR, + PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR, PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR }; @@ -1067,7 +1069,7 @@ protected: func_decl * m_lemma_decl; ptr_vector m_unit_resolution_decls; - func_decl * m_def_intro_decl; + func_decl * m_def_intro_decl; func_decl * m_iff_oeq_decl; func_decl * m_skolemize_decl; func_decl * m_mp_oeq_decl; @@ -1083,7 +1085,7 @@ protected: static bool is_proof(decl_kind k) { return k > LAST_BASIC_OP; } bool check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const; bool check_proof_args(basic_op_kind k, unsigned num_args, expr * const * args) const; - func_decl * mk_bool_op_decl(char const * name, basic_op_kind k, unsigned num_args = 0, + func_decl * mk_bool_op_decl(char const * name, basic_op_kind k, unsigned num_args = 0, bool asooc = false, bool comm = false, bool idempotent = false, bool flat_associative = false, bool chainable = false); func_decl * mk_implies_decl(); func_decl * mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents); @@ -1093,10 +1095,10 @@ protected: func_decl * mk_proof_decl(basic_op_kind k, unsigned num_parents); func_decl * mk_proof_decl(basic_op_kind k, unsigned num_parameters, parameter const* params, unsigned num_parents); func_decl * mk_proof_decl( - char const * name, basic_op_kind k, + char const * name, basic_op_kind k, unsigned num_parameters, parameter const* params, unsigned num_parents); - + virtual void set_manager(ast_manager * m, family_id id); func_decl * mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector & cache); func_decl * mk_ite_decl(sort * s); @@ -1105,7 +1107,7 @@ protected: sort* join(unsigned n, expr*const* es); public: basic_decl_plugin(); - + virtual ~basic_decl_plugin() {} virtual void finalize(); @@ -1114,23 +1116,23 @@ public: } virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters); - - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range); - + virtual void get_op_names(svector & op_names, symbol const & logic); - + virtual void get_sort_names(svector & sort_names, symbol const & logic); - virtual bool is_value(app* a) const; + virtual bool is_value(app* a) const; + + virtual bool is_unique_value(app* a) const; - virtual bool is_unique_value(app* a) const; - sort * mk_bool_sort() const { return m_bool_sort; } - sort * mk_proof_sort() const { return m_proof_sort; } + sort * mk_proof_sort() const { return m_proof_sort; } virtual expr * get_some_value(sort * s); }; @@ -1139,7 +1141,7 @@ typedef app proof; /* a proof is just an applicaton */ // ----------------------------------- // -// label_decl_plugin +// label_decl_plugin // // ----------------------------------- @@ -1168,7 +1170,7 @@ public: /** contract: when label - parameter[0] (int): 0 - if the label is negative, 1 - if positive. + parameter[0] (int): 0 - if the label is negative, 1 - if positive. parameter[1] (symbol): label's tag. ... parameter[n-1] (symbol): label's tag. @@ -1178,13 +1180,13 @@ public: ... parameter[n-1] (symbol): label's tag. */ - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); }; // ----------------------------------- // -// pattern_decl_plugin +// pattern_decl_plugin // // ----------------------------------- @@ -1202,7 +1204,7 @@ public: virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); }; @@ -1222,7 +1224,7 @@ enum model_value_op_kind { introduce unsoundess if the sort of a value is finite. Moreover, values should never be internalized in a logical context. - + However, values can be used during evaluation (i.e., simplification). \remark Model values can be viewed as the partion ids in Z3 1.x. @@ -1234,18 +1236,18 @@ public: virtual decl_plugin * mk_fresh() { return alloc(model_value_decl_plugin); } virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - + /** - contract: + contract: parameter[0]: (integer) value idx parameter[1]: (ast) sort of the value. */ - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); virtual bool is_value(app* n) const; - virtual bool is_unique_value(app* a) const; + virtual bool is_unique_value(app* a) const; }; // ----------------------------------- @@ -1261,7 +1263,7 @@ public: user_sort_plugin() {} virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); decl_kind register_name(symbol s); virtual decl_plugin * mk_fresh(); @@ -1321,7 +1323,7 @@ public: bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); } bool is_true(expr const * n) const { return is_app_of(n, m_fid, OP_TRUE); } bool is_false(expr const * n) const { return is_app_of(n, m_fid, OP_FALSE); } - bool is_complement_core(expr const * n1, expr const * n2) const { + bool is_complement_core(expr const * n1, expr const * n2) const { return (is_true(n1) && is_false(n2)) || (is_not(n1) && to_app(n1)->get_arg(0) == n2); } bool is_complement(expr const * n1, expr const * n2) const { return is_complement_core(n1, n2) || is_complement_core(n2, n1); } @@ -1353,7 +1355,7 @@ public: // // Get Some Value functor // -// Functor for returning some value +// Functor for returning some value // of the given sort. // // ----------------------------------- @@ -1394,11 +1396,11 @@ protected: static const unsigned max_trail_sz = 16; static const unsigned factor = 2; }; - + struct expr_array_config : public array_config { typedef expr * value; }; - + typedef parray_manager expr_array_manager; struct expr_dependency_config : public config { @@ -1439,7 +1441,7 @@ protected: family_id m_model_value_family_id; family_id m_user_sort_family_id; family_id m_arith_family_id; - ast_table m_ast_table; + ast_table m_ast_table; id_gen m_expr_id_gen; id_gen m_decl_id_gen; sort * m_bool_sort; @@ -1477,20 +1479,20 @@ public: void enable_int_real_coercions(bool f) { m_int_real_coercions = f; } bool int_real_coercions() const { return m_int_real_coercions; } - + // Return true if s1 and s2 are equal, or coercions are enabled, and s1 and s2 are compatible. bool compatible_sorts(sort * s1, sort * s2) const; // For debugging purposes 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); } - + void compact_memory(); void compress_ids(); // Equivalent to throw ast_exception(msg) void raise_exception(char const * msg); - + bool is_format_manager() const { return m_format_manager == 0; } ast_manager & get_format_manager() { return is_format_manager() ? *this : *m_format_manager; } @@ -1498,7 +1500,7 @@ public: void copy_families_plugins(ast_manager const & from); small_object_allocator & get_allocator() { return m_alloc; } - + family_id mk_family_id(symbol const & s) { return m_family_manager.mk_family_id(s); } family_id mk_family_id(char const * s) { return mk_family_id(symbol(s)); } @@ -1507,70 +1509,70 @@ public: symbol const & get_family_name(family_id fid) const { return m_family_manager.get_name(fid); } - bool is_builtin_family_id(family_id fid) const { - return - fid == null_family_id || - fid == m_basic_family_id || - fid == m_label_family_id || - fid == m_pattern_family_id || + bool is_builtin_family_id(family_id fid) const { + return + fid == null_family_id || + fid == m_basic_family_id || + fid == m_label_family_id || + fid == m_pattern_family_id || fid == m_model_value_family_id || - fid == m_user_sort_family_id; + fid == m_user_sort_family_id; } reslimit& limit() { return m_limit; } bool canceled() { return !limit().inc(); } void register_plugin(symbol const & s, decl_plugin * plugin); - + void register_plugin(family_id id, decl_plugin * plugin); decl_plugin * get_plugin(family_id fid) const; - + bool has_plugin(family_id fid) const { return get_plugin(fid) != 0; } - + bool has_plugin(symbol const & s) const { return m_family_manager.has_family(s) && has_plugin(m_family_manager.get_family_id(s)); } - + void get_dom(svector & dom) const { m_family_manager.get_dom(dom); } - + void get_range(svector & range) const { m_family_manager.get_range(range); } - + family_id get_basic_family_id() const { return m_basic_family_id; } - + basic_decl_plugin * get_basic_decl_plugin() const { return static_cast(get_plugin(m_basic_family_id)); } family_id get_user_sort_family_id() const { return m_user_sort_family_id; } - + user_sort_plugin * get_user_sort_plugin() const { return static_cast(get_plugin(m_user_sort_family_id)); } /** \brief Debugging support method: set the next expression identifier to be the least value id' s.t. - id' >= id - id' is not used by any AST in m_table - - id' is not in the expression m_free_ids + - id' is not in the expression m_free_ids This method should be only used to create small repros that exposes bugs in Z3. */ void set_next_expr_id(unsigned id); - - bool is_value(expr * e) const; - + + bool is_value(expr * e) const; + bool is_unique_value(expr * e) const; bool are_equal(expr * a, expr * b) const; - + bool are_distinct(expr * a, expr * b) const; - + bool contains(ast * a) const { return m_ast_table.contains(a); } - + unsigned get_num_asts() const { return m_ast_table.size(); } void debug_ref_count() { m_debug_ref_count = true; } - - void inc_ref(ast * n) { + + void inc_ref(ast * n) { if (n) n->inc_ref(); } - + void dec_ref(ast * n) { if (n) { n->dec_ref(); @@ -1578,45 +1580,45 @@ public: delete_node(n); } } - + template void inc_array_ref(unsigned sz, T * const * a) { for(unsigned i = 0; i < sz; i++) { inc_ref(a[i]); } } - + template void dec_array_ref(unsigned sz, T * const * a) { for(unsigned i = 0; i < sz; i++) { dec_ref(a[i]); } } - + static unsigned get_node_size(ast const * n); - - size_t get_allocation_size() const { - return m_alloc.get_allocation_size(); + + size_t get_allocation_size() const { + return m_alloc.get_allocation_size(); } - + protected: ast * register_node_core(ast * n); - + template - T * register_node(T * n) { - return static_cast(register_node_core(n)); + T * register_node(T * n) { + return static_cast(register_node_core(n)); } - + void delete_node(ast * n); - - void * allocate_node(unsigned size) { + + void * allocate_node(unsigned size) { return m_alloc.allocate(size); } - + void deallocate_node(ast * n, unsigned sz) { m_alloc.deallocate(sz, n); } - + public: sort * get_sort(expr const * n) const { return ::get_sort(n); } void check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const; @@ -1629,12 +1631,12 @@ public: private: sort * mk_sort(symbol const & name, sort_info * info); - + public: sort * mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters); sort * mk_uninterpreted_sort(symbol const & name) { return mk_uninterpreted_sort(name, 0, 0); } - + sort * mk_sort(symbol const & name, sort_info const & info) { if (info.get_family_id() == null_family_id) { return mk_uninterpreted_sort(name); @@ -1643,45 +1645,45 @@ public: return mk_sort(name, &const_cast(info)); } } - + sort * mk_sort(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = 0); - + sort * mk_bool_sort() const { return m_bool_sort; } - + sort * mk_proof_sort() const { return m_proof_sort; } sort * mk_fresh_sort(char const * prefix = ""); bool is_uninterp(sort const * s) const { return s->get_family_id() == null_family_id || s->get_family_id() == m_user_sort_family_id; } - + /** \brief A sort is "fully" interpreted if it is interpreted, - and doesn't depend on other uninterpreted sorts. + and doesn't depend on other uninterpreted sorts. */ bool is_fully_interp(sort const * s) const; - func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters, + func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range = 0); - func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters, + func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range = 0); - app * mk_app(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = 0, + app * mk_app(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = 0, unsigned num_args = 0, expr * const * args = 0, sort * range = 0); app * mk_app(family_id fid, decl_kind k, unsigned num_args, expr * const * args); app * mk_app(family_id fid, decl_kind k, expr * arg); - + app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2); - + app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2, expr * arg3); app * mk_const(family_id fid, decl_kind k) { return mk_app(fid, k, 0, static_cast(0)); } private: - func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, + func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, func_decl_info * info); - + app * mk_app_core(func_decl * decl, expr * arg1, expr * arg2); app * mk_app_core(func_decl * decl, unsigned num_args, expr * const * args); @@ -1690,8 +1692,8 @@ public: func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range) { return mk_func_decl(name, arity, domain, range, static_cast(0)); } - - func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, + + func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, func_decl_info const & info) { if (info.is_null()) { return mk_func_decl(name, arity, domain, range, static_cast(0)); @@ -1700,69 +1702,69 @@ public: return mk_func_decl(name, arity, domain, range, & const_cast(info)); } } - + func_decl * mk_func_decl(unsigned arity, sort * const * domain, func_decl_info const & info) { - return mk_func_decl(info.get_family_id(), info.get_decl_kind(), info.get_num_parameters(), info.get_parameters(), + return mk_func_decl(info.get_family_id(), info.get_decl_kind(), info.get_num_parameters(), info.get_parameters(), arity, domain); } - + func_decl * mk_const_decl(symbol const & name, sort * s) { return mk_func_decl(name, static_cast(0), 0, s); } - + func_decl * mk_const_decl(symbol const & name, sort * s, func_decl_info const & info) { return mk_func_decl(name, static_cast(0), 0, s, info); } - + func_decl * mk_func_decl(symbol const & name, sort * domain, sort * range, func_decl_info const & info) { return mk_func_decl(name, 1, &domain, range, info); } - + func_decl * mk_func_decl(symbol const & name, sort * domain, sort * range) { return mk_func_decl(name, 1, &domain, range); } - + func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range, func_decl_info const & info) { sort * d[2] = { domain1, domain2 }; return mk_func_decl(name, 2, d, range, info); } - - func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range) { + + func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range) { sort * d[2] = { domain1, domain2 }; return mk_func_decl(name, 2, d, range); } - - func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, + + func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, bool assoc, bool comm = false, bool inj = false); func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range, bool assoc, bool comm = false) { sort * d[2] = { domain1, domain2 }; return mk_func_decl(name, 2, d, range, assoc, comm, false); } - + app * mk_app(func_decl * decl, unsigned num_args, expr * const * args); app * mk_app(func_decl * decl, expr * const * args) { return mk_app(decl, decl->get_arity(), args); } - + app * mk_app(func_decl * decl, expr * arg) { SASSERT(decl->get_arity() == 1); return mk_app(decl, 1, &arg); } - + app * mk_app(func_decl * decl, expr * arg1, expr * arg2) { SASSERT(decl->get_arity() == 2); expr * args[2] = { arg1, arg2 }; return mk_app(decl, 2, args); } - + app * mk_app(func_decl * decl, expr * arg1, expr * arg2, expr * arg3) { SASSERT(decl->get_arity() == 3); expr * args[3] = { arg1, arg2, arg3 }; return mk_app(decl, 3, args); } - + app * mk_const(func_decl * decl) { SASSERT(decl->get_arity() == 0); return mk_app(decl, static_cast(0), static_cast(0)); @@ -1771,21 +1773,21 @@ public: app * mk_const(symbol const & name, sort * s) { return mk_const(mk_const_decl(name, s)); } - + func_decl * mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity, sort * const * domain, sort * range); func_decl * mk_fresh_func_decl(unsigned arity, sort * const * domain, sort * range) { return mk_fresh_func_decl(symbol::null, symbol::null, arity, domain, range); } - - func_decl * mk_fresh_func_decl(char const * prefix, char const * suffix, unsigned arity, + + func_decl * mk_fresh_func_decl(char const * prefix, char const * suffix, unsigned arity, sort * const * domain, sort * range) { return mk_fresh_func_decl(symbol(prefix), symbol(suffix), arity, domain, range); } - + func_decl * mk_fresh_func_decl(char const * prefix, unsigned arity, sort * const * domain, sort * range) { return mk_fresh_func_decl(symbol(prefix), symbol::null, arity, domain, range); } - + app * mk_fresh_const(char const * prefix, sort * s) { return mk_const(mk_fresh_func_decl(prefix, 0, 0, s)); } symbol mk_fresh_var_name(char const * prefix = 0); @@ -1808,7 +1810,7 @@ public: return is_label(n)?(l = to_app(n)->get_arg(0), true):false; } - bool is_label(expr const * n, bool& pos) const { + bool is_label(expr const * n, bool& pos) const { if (is_app_of(n, m_label_family_id, OP_LABEL)) { pos = to_app(n)->get_decl()->get_parameter(0).get_int() != 0; return true; @@ -1832,37 +1834,37 @@ public: app * mk_pattern(app * expr) { return mk_pattern(1, &expr); } - bool is_pattern(expr const * n) const; + bool is_pattern(expr const * n) const; -public: +public: - quantifier * mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, + quantifier * mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null, - unsigned num_patterns = 0, expr * const * patterns = 0, + unsigned num_patterns = 0, expr * const * patterns = 0, unsigned num_no_patterns = 0, expr * const * no_patterns = 0); - quantifier * mk_forall(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, + quantifier * mk_forall(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null, - unsigned num_patterns = 0, expr * const * patterns = 0, + unsigned num_patterns = 0, expr * const * patterns = 0, unsigned num_no_patterns = 0, expr * const * no_patterns = 0) { return mk_quantifier(true, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns, num_no_patterns, no_patterns); } - quantifier * mk_exists(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, + quantifier * mk_exists(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null, - unsigned num_patterns = 0, expr * const * patterns = 0, + unsigned num_patterns = 0, expr * const * patterns = 0, unsigned num_no_patterns = 0, expr * const * no_patterns = 0) { return mk_quantifier(false, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns, num_no_patterns, no_patterns); } - + quantifier * update_quantifier(quantifier * q, unsigned new_num_patterns, expr * const * new_patterns, expr * new_body); 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); - + quantifier * update_quantifier(quantifier * q, expr * new_body); - + quantifier * update_quantifier_weight(quantifier * q, int new_weight); quantifier * update_quantifier(quantifier * q, bool new_is_forall, expr * new_body); @@ -1919,12 +1921,12 @@ public: bool empty(expr_dependency_array const & r) const { return m_expr_dependency_array_manager.empty(r); } expr_dependency * get(expr_dependency_array const & r, unsigned i) const { return m_expr_dependency_array_manager.get(r, i); } void set(expr_dependency_array & r, unsigned i, expr_dependency * v) { m_expr_dependency_array_manager.set(r, i, v); } - void set(expr_dependency_array const & s, unsigned i, expr_dependency * v, expr_dependency_array & r) { - m_expr_dependency_array_manager.set(s, i, v, r); + void set(expr_dependency_array const & s, unsigned i, expr_dependency * v, expr_dependency_array & r) { + m_expr_dependency_array_manager.set(s, i, v, r); } void push_back(expr_dependency_array & r, expr_dependency * v) { m_expr_dependency_array_manager.push_back(r, v); } - void push_back(expr_dependency_array const & s, expr_dependency * v, expr_dependency_array & r) { - m_expr_dependency_array_manager.push_back(s, v, r); + void push_back(expr_dependency_array const & s, expr_dependency * v, expr_dependency_array & r) { + m_expr_dependency_array_manager.push_back(s, v, r); } void pop_back(expr_dependency_array & r) { m_expr_dependency_array_manager.pop_back(r); } void pop_back(expr_dependency_array const & s, expr_dependency_array & r) { m_expr_dependency_array_manager.pop_back(s, r); } @@ -1953,7 +1955,7 @@ public: bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); } bool is_true(expr const * n) const { return n == m_true; } bool is_false(expr const * n) const { return n == m_false; } - bool is_complement_core(expr const * n1, expr const * n2) const { + bool is_complement_core(expr const * n1, expr const * n2) const { return (is_true(n1) && is_false(n2)) || (is_not(n1) && to_app(n1)->get_arg(0) == n2); } bool is_complement(expr const * n1, expr const * n2) const { return is_complement_core(n1, n2) || is_complement_core(n2, n1); } @@ -1981,14 +1983,14 @@ public: MATCH_TERNARY(is_and); MATCH_TERNARY(is_or); - bool is_ite(expr const* n, expr*& t1, expr*& t2, expr*& t3) const { - if (is_ite(n)) { - t1 = to_app(n)->get_arg(0); - t2 = to_app(n)->get_arg(1); + bool is_ite(expr const* n, expr*& t1, expr*& t2, expr*& t3) const { + if (is_ite(n)) { + t1 = to_app(n)->get_arg(0); + t2 = to_app(n)->get_arg(1); t3 = to_app(n)->get_arg(2); - return true; - } - return false; + return true; + } + return false; } public: @@ -2014,14 +2016,14 @@ public: app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); } - func_decl* mk_and_decl() { + func_decl* mk_and_decl() { sort* domain[2] = { m_bool_sort, m_bool_sort }; - return mk_func_decl(m_basic_family_id, OP_AND, 0, 0, 2, domain); + return mk_func_decl(m_basic_family_id, OP_AND, 0, 0, 2, domain); } func_decl* mk_not_decl() { return mk_func_decl(m_basic_family_id, OP_NOT, 0, 0, 1, &m_bool_sort); } func_decl* mk_or_decl() { sort* domain[2] = { m_bool_sort, m_bool_sort }; - return mk_func_decl(m_basic_family_id, OP_OR, 0, 0, 2, domain); + return mk_func_decl(m_basic_family_id, OP_OR, 0, 0, 2, domain); } // ----------------------------------- @@ -2036,7 +2038,7 @@ public: app * mk_model_value(unsigned idx, sort * s); bool is_model_value(expr const * n) const { return is_app_of(n, m_model_value_family_id, OP_MODEL_VALUE); } bool is_model_value(func_decl const * d) const { return is_decl_of(d, m_model_value_family_id, OP_MODEL_VALUE); } - + expr * get_some_value(sort * s, some_value_proc * p); expr * get_some_value(sort * s); @@ -2059,7 +2061,7 @@ public: bool fine_grain_proofs() const { return m_proof_mode == PGM_FINE; } proof_gen_mode proof_mode() const { return m_proof_mode; } void toggle_proof_mode(proof_gen_mode m) { m_proof_mode = m; } // APIs for creating proof objects return [undef] - + proof * mk_undef_proof() const { return m_undef_proof; } bool is_proof(expr const * n) const { return is_app(n) && to_app(n)->get_decl()->get_range() == m_proof_sort; } @@ -2067,7 +2069,7 @@ public: proof* mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl, svector > const& positions, vector > const& substs); - + bool is_undef_proof(expr const * e) const { return e == m_undef_proof; } bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); } @@ -2089,30 +2091,30 @@ public: bool is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector& binding) const; bool is_rewrite(expr const* e, expr*& r1, expr*& r2) const; bool is_hyper_resolve(proof* p) const { return is_app_of(p, m_basic_family_id, PR_HYPER_RESOLVE); } - bool is_hyper_resolve(proof* p, + bool is_hyper_resolve(proof* p, ref_vector& premises, obj_ref& conclusion, svector > & positions, vector >& substs); - + bool is_def_intro(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_DEF_INTRO); } bool is_apply_def(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_APPLY_DEF); } bool is_skolemize(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_SKOLEMIZE); } MATCH_UNARY(is_asserted); - MATCH_UNARY(is_lemma); + MATCH_UNARY(is_lemma); - bool has_fact(proof const * p) const { - SASSERT(is_proof(p)); - unsigned n = p->get_num_args(); - return n > 0 && get_sort(p->get_arg(n - 1)) != m_proof_sort; + bool has_fact(proof const * p) const { + SASSERT(is_proof(p)); + unsigned n = p->get_num_args(); + return n > 0 && get_sort(p->get_arg(n - 1)) != m_proof_sort; } expr * get_fact(proof const * p) const { SASSERT(is_proof(p)); SASSERT(has_fact(p)); return p->get_arg(p->get_num_args() - 1); } - unsigned get_num_parents(proof const * p) const { - SASSERT(is_proof(p)); + unsigned get_num_parents(proof const * p) const { + SASSERT(is_proof(p)); unsigned n = p->get_num_args(); - return !has_fact(p) ? n : n - 1; + return !has_fact(p) ? n : n - 1; } proof * get_parent(proof const * p, unsigned idx) const { SASSERT(is_proof(p)); return to_app(p->get_arg(idx)); } proof * mk_true_proof(); @@ -2147,7 +2149,7 @@ public: proof * mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding); proof * mk_def_axiom(expr * ax); - proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs); + proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs); proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs, expr * new_fact); proof * mk_hypothesis(expr * h); proof * mk_lemma(proof * p, expr * lemma); @@ -2166,7 +2168,7 @@ public: proof * mk_and_elim(proof * p, unsigned i); proof * mk_not_or_elim(proof * p, unsigned i); - proof * mk_th_lemma(family_id tid, + proof * mk_th_lemma(family_id tid, expr * fact, unsigned num_proofs, proof * const * proofs, unsigned num_params = 0, parameter const* params = 0); @@ -2180,7 +2182,7 @@ private: worklist.push_back(n); } } - + template void dec_array_ref(ptr_buffer & worklist, unsigned sz, T * const * a) { for(unsigned i = 0; i < sz; i++) { @@ -2315,7 +2317,7 @@ public: void mark(ast * n, bool flag) { if (flag) mark(n); else reset_mark(n); } - unsigned get_level() { + unsigned get_level() { return m_to_unmark.size(); } @@ -2334,7 +2336,7 @@ typedef ast_fast_mark1 expr_fast_mark1; typedef ast_fast_mark2 expr_fast_mark2; /** - Similar to ast_fast_mark, but increases reference counter. + Similar to ast_fast_mark, but increases reference counter. */ template class ast_ref_fast_mark { @@ -2369,7 +2371,7 @@ public: } m_to_unmark.push_back(n); } - + void reset() { ast * const * it = m_to_unmark.c_ptr(); ast * const * end = it + m_to_unmark.size(); @@ -2378,7 +2380,7 @@ public: } m_to_unmark.reset(); } - + void mark(ast * n, bool flag) { if (flag) mark(n); else reset_mark(n); } }; @@ -2396,7 +2398,7 @@ typedef ast_ref_fast_mark2 expr_ref_fast_mark2; /** \brief A mapping from AST to Boolean - \warning This map does not cleanup the entry associated with a node N, + \warning This map does not cleanup the entry associated with a node N, when N is deleted. */ class ast_mark { @@ -2422,7 +2424,7 @@ public: */ class scoped_mark : public ast_mark { ast_ref_vector m_stack; - unsigned_vector m_lim; + unsigned_vector m_lim; public: scoped_mark(ast_manager& m): m_stack(m) {} virtual ~scoped_mark() {} @@ -2459,4 +2461,4 @@ public: #endif /* AST_H_ */ - + diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index eea4f46d6..563622338 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -33,7 +33,7 @@ enum bv_op_kind { OP_BADD, OP_BSUB, OP_BMUL, - + OP_BSDIV, OP_BUDIV, OP_BSREM, @@ -41,20 +41,20 @@ enum bv_op_kind { OP_BSMOD, // special functions to record the division by 0 cases - // these are internal functions - OP_BSDIV0, + // these are internal functions + OP_BSDIV0, OP_BUDIV0, OP_BSREM0, OP_BUREM0, OP_BSMOD0, // special functions where division by 0 has a fixed interpretation. - OP_BSDIV_I, + OP_BSDIV_I, OP_BUDIV_I, OP_BSREM_I, OP_BUREM_I, OP_BSMOD_I, - + OP_ULEQ, OP_SLEQ, OP_UGEQ, @@ -95,7 +95,7 @@ enum bv_op_kind { OP_BSMUL_NO_UDFL, // no signed multiplication underflow predicate OP_BIT2BOOL, // predicate - OP_MKBV, // bools to bv + OP_MKBV, // bools to bv OP_INT2BV, OP_BV2INT, @@ -176,7 +176,7 @@ protected: ptr_vector m_bv_slt; ptr_vector m_bv_ugt; ptr_vector m_bv_sgt; - + ptr_vector m_bv_and; ptr_vector m_bv_or; ptr_vector m_bv_not; @@ -184,7 +184,7 @@ protected: ptr_vector m_bv_nand; ptr_vector m_bv_nor; ptr_vector m_bv_xnor; - + ptr_vector m_bv_redor; ptr_vector m_bv_redand; ptr_vector m_bv_comp; @@ -203,7 +203,7 @@ protected: ptr_vector m_int2bv; vector > m_bit2bool; ptr_vector m_mkbv; - + virtual void set_manager(ast_manager * m, family_id id); void mk_bv_sort(unsigned bv_size); sort * get_bv_sort(unsigned bv_size); @@ -218,9 +218,9 @@ protected: bool get_bv_size(sort * t, int & result); bool get_bv_size(expr * t, int & result); bool get_concat_size(unsigned arity, sort * const * domain, int & result); - bool get_extend_size(unsigned num_parameters, parameter const * parameters, + bool get_extend_size(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, int & result); - bool get_extract_size(unsigned num_parameters, parameter const * parameters, + bool get_extract_size(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, int & result); func_decl * mk_bv2int(unsigned bv_size, unsigned num_parameters, parameter const * parameters, @@ -229,13 +229,13 @@ protected: func_decl * mk_int2bv(unsigned bv_size, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain); - func_decl * mk_bit2bool(unsigned bv_size, unsigned num_parameters, parameter const * parameters, + func_decl * mk_bit2bool(unsigned bv_size, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain); func_decl * mk_mkbv(unsigned arity, sort * const * domain); bool get_int2bv_size(unsigned num_parameters, parameter const * parameters, int & result); - + func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity); void get_offset_term(app * a, expr * & t, rational & offset) const; @@ -248,24 +248,40 @@ public: virtual decl_plugin * mk_fresh() { return alloc(bv_decl_plugin); } virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range); virtual bool is_value(app * e) const; - + virtual bool is_unique_value(app * e) const { return is_value(e); } virtual void get_op_names(svector & op_names, symbol const & logic); virtual void get_sort_names(svector & sort_names, symbol const & logic); - + virtual bool are_distinct(app* a, app* b) const; - + virtual expr * get_some_value(sort * s); + + virtual bool is_considered_uninterpreted(func_decl * f) { + if (f->get_family_id() != get_family_id()) + return false; + switch (f->get_decl_kind()) { + case OP_BSDIV0: + case OP_BUDIV0: + case OP_BSREM0: + case OP_BUREM0: + case OP_BSMOD0: + return true; + default: + return false; + } + return false; + } }; class bv_recognizers { @@ -282,7 +298,7 @@ public: bool is_zero(expr const * e) const; bool is_bv_sort(sort const * s) const; bool is_bv(expr const* e) const { return is_bv_sort(get_sort(e)); } - + bool is_concat(expr const * e) const { return is_app_of(e, get_fid(), OP_CONCAT); } bool is_extract(func_decl const * f) const { return is_decl_of(f, get_fid(), OP_EXTRACT); } bool is_extract(expr const * e) const { return is_app_of(e, get_fid(), OP_EXTRACT); } @@ -353,7 +369,6 @@ public: rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); } bool has_sign_bit(rational const & n, unsigned bv_size) const; bool mult_inverse(rational const & n, unsigned bv_size, rational & result); - }; class bv_util : public bv_recognizers { @@ -369,8 +384,8 @@ public: app * mk_numeral(rational const & val, unsigned bv_size); app * mk_numeral(uint64 u, unsigned bv_size) { return mk_numeral(rational(u, rational::ui64()), bv_size); } sort * mk_sort(unsigned bv_size); - - unsigned get_bv_size(sort const * s) const { + + unsigned get_bv_size(sort const * s) const { SASSERT(is_bv_sort(s)); return static_cast(s->get_parameter(0).get_int()); } @@ -393,11 +408,11 @@ public: app * mk_bv_add(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); } app * mk_bv_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); } app * mk_bv_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); } - app * mk_zero_extend(unsigned n, expr* e) { + app * mk_zero_extend(unsigned n, expr* e) { parameter p(n); return m_manager.mk_app(get_fid(), OP_ZERO_EXT, 1, &p, 1, &e); } - app * mk_sign_extend(unsigned n, expr* e) { + app * mk_sign_extend(unsigned n, expr* e) { parameter p(n); return m_manager.mk_app(get_fid(), OP_SIGN_EXT, 1, &p, 1, &e); } @@ -413,6 +428,6 @@ public: app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); } }; - + #endif /* BV_DECL_PLUGIN_H_ */ diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index ab78eaf97..fc0e5a807 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -78,91 +78,91 @@ void bv_rewriter::get_param_descrs(param_descrs & r) { poly_rewriter::get_param_descrs(r); bv_rewriter_params::collect_param_descrs(r); #ifndef _EXTERNAL_RELEASE - r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral"); + r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral"); #endif } br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_family_id() == get_fid()); - + switch(f->get_decl_kind()) { case OP_BIT0: SASSERT(num_args == 0); result = m_util.mk_numeral(0, 1); return BR_DONE; case OP_BIT1: SASSERT(num_args == 0); result = m_util.mk_numeral(1, 1); return BR_DONE; - case OP_ULEQ: - SASSERT(num_args == 2); + case OP_ULEQ: + SASSERT(num_args == 2); return mk_ule(args[0], args[1], result); - case OP_UGEQ: - SASSERT(num_args == 2); - return mk_uge(args[0], args[1], result); - case OP_ULT: - SASSERT(num_args == 2); - return mk_ult(args[0], args[1], result); - case OP_UGT: - SASSERT(num_args == 2); - return mk_ult(args[1], args[0], result); - case OP_SLEQ: - SASSERT(num_args == 2); - return mk_sle(args[0], args[1], result); - case OP_SGEQ: - SASSERT(num_args == 2); - return mk_sge(args[0], args[1], result); - case OP_SLT: - SASSERT(num_args == 2); - return mk_slt(args[0], args[1], result); - case OP_SGT: - SASSERT(num_args == 2); - return mk_slt(args[1], args[0], result); - case OP_BADD: - SASSERT(num_args > 0); - return mk_bv_add(num_args, args, result); + case OP_UGEQ: + SASSERT(num_args == 2); + return mk_uge(args[0], args[1], result); + case OP_ULT: + SASSERT(num_args == 2); + return mk_ult(args[0], args[1], result); + case OP_UGT: + SASSERT(num_args == 2); + return mk_ult(args[1], args[0], result); + case OP_SLEQ: + SASSERT(num_args == 2); + return mk_sle(args[0], args[1], result); + case OP_SGEQ: + SASSERT(num_args == 2); + return mk_sge(args[0], args[1], result); + case OP_SLT: + SASSERT(num_args == 2); + return mk_slt(args[0], args[1], result); + case OP_SGT: + SASSERT(num_args == 2); + return mk_slt(args[1], args[0], result); + case OP_BADD: + SASSERT(num_args > 0); + return mk_bv_add(num_args, args, result); case OP_BMUL: - SASSERT(num_args > 0); - return mk_bv_mul(num_args, args, result); - case OP_BSUB: - SASSERT(num_args > 0); - return mk_sub(num_args, args, result); - case OP_BNEG: - SASSERT(num_args == 1); + SASSERT(num_args > 0); + return mk_bv_mul(num_args, args, result); + case OP_BSUB: + SASSERT(num_args > 0); + return mk_sub(num_args, args, result); + case OP_BNEG: + SASSERT(num_args == 1); return mk_uminus(args[0], result); - case OP_BSHL: - SASSERT(num_args == 2); - return mk_bv_shl(args[0], args[1], result); + case OP_BSHL: + SASSERT(num_args == 2); + return mk_bv_shl(args[0], args[1], result); case OP_BLSHR: - SASSERT(num_args == 2); - return mk_bv_lshr(args[0], args[1], result); - case OP_BASHR: - SASSERT(num_args == 2); + SASSERT(num_args == 2); + return mk_bv_lshr(args[0], args[1], result); + case OP_BASHR: + SASSERT(num_args == 2); return mk_bv_ashr(args[0], args[1], result); - case OP_BSDIV: - SASSERT(num_args == 2); + case OP_BSDIV: + SASSERT(num_args == 2); return mk_bv_sdiv(args[0], args[1], result); - case OP_BUDIV: - SASSERT(num_args == 2); - return mk_bv_udiv(args[0], args[1], result); - case OP_BSREM: - SASSERT(num_args == 2); - return mk_bv_srem(args[0], args[1], result); - case OP_BUREM: - SASSERT(num_args == 2); - return mk_bv_urem(args[0], args[1], result); - case OP_BSMOD: - SASSERT(num_args == 2); - return mk_bv_smod(args[0], args[1], result); - case OP_BSDIV_I: - SASSERT(num_args == 2); - return mk_bv_sdiv_i(args[0], args[1], result); - case OP_BUDIV_I: - SASSERT(num_args == 2); + case OP_BUDIV: + SASSERT(num_args == 2); + return mk_bv_udiv(args[0], args[1], result); + case OP_BSREM: + SASSERT(num_args == 2); + return mk_bv_srem(args[0], args[1], result); + case OP_BUREM: + SASSERT(num_args == 2); + return mk_bv_urem(args[0], args[1], result); + case OP_BSMOD: + SASSERT(num_args == 2); + return mk_bv_smod(args[0], args[1], result); + case OP_BSDIV_I: + SASSERT(num_args == 2); + return mk_bv_sdiv_i(args[0], args[1], result); + case OP_BUDIV_I: + SASSERT(num_args == 2); return mk_bv_udiv_i(args[0], args[1], result); - case OP_BSREM_I: - SASSERT(num_args == 2); + case OP_BSREM_I: + SASSERT(num_args == 2); return mk_bv_srem_i(args[0], args[1], result); - case OP_BUREM_I: - SASSERT(num_args == 2); + case OP_BUREM_I: + SASSERT(num_args == 2); return mk_bv_urem_i(args[0], args[1], result); - case OP_BSMOD_I: - SASSERT(num_args == 2); - return mk_bv_smod_i(args[0], args[1], result); + case OP_BSMOD_I: + SASSERT(num_args == 2); + return mk_bv_smod_i(args[0], args[1], result); case OP_CONCAT: return mk_concat(num_args, args, result); case OP_EXTRACT: @@ -193,10 +193,10 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons case OP_BXNOR: return mk_bv_xnor(num_args, args, result); case OP_ROTATE_LEFT: - SASSERT(num_args == 1); - return mk_bv_rotate_left(f->get_parameter(0).get_int(), args[0], result); - case OP_ROTATE_RIGHT: - SASSERT(num_args == 1); + SASSERT(num_args == 1); + return mk_bv_rotate_left(f->get_parameter(0).get_int(), args[0], result); + case OP_ROTATE_RIGHT: + SASSERT(num_args == 1); return mk_bv_rotate_right(f->get_parameter(0).get_int(), args[0], result); case OP_EXT_ROTATE_LEFT: SASSERT(num_args == 2); @@ -210,14 +210,14 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons case OP_INT2BV: SASSERT(num_args == 1); return mk_int2bv(m_util.get_bv_size(f->get_range()), args[0], result); - case OP_BREDOR: - SASSERT(num_args == 1); - return mk_bv_redor(args[0], result); - case OP_BREDAND: - SASSERT(num_args == 1); - return mk_bv_redand(args[0], result); - case OP_BCOMP: - SASSERT(num_args == 2); + case OP_BREDOR: + SASSERT(num_args == 1); + return mk_bv_redor(args[0], result); + case OP_BREDAND: + SASSERT(num_args == 1); + return mk_bv_redand(args[0], result); + case OP_BCOMP: + SASSERT(num_args == 2); return mk_bv_comp(args[0], args[1], result); case OP_MKBV: return mk_mkbv(num_args, args, result); @@ -232,7 +232,7 @@ br_status bv_rewriter::mk_ule(expr * a, expr * b, expr_ref & result) { br_status bv_rewriter::mk_uge(expr * a, expr * b, expr_ref & result) { br_status st = mk_ule(b, a, result); - if (st != BR_FAILED) + if (st != BR_FAILED) return st; result = m_util.mk_ule(b, a); return BR_DONE; @@ -249,7 +249,7 @@ br_status bv_rewriter::mk_sle(expr * a, expr * b, expr_ref & result) { br_status bv_rewriter::mk_sge(expr * a, expr * b, expr_ref & result) { br_status st = mk_sle(b, a, result); - if (st != BR_FAILED) + if (st != BR_FAILED) return st; result = m_util.mk_sle(b, a); return BR_DONE; @@ -272,7 +272,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref return BR_DONE; } - if (is_num1) + if (is_num1) r1 = m_util.norm(r1, sz, is_signed); if (is_num2) r2 = m_util.norm(r2, sz, is_signed); @@ -322,7 +322,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref #if 0 if (!is_signed && m_util.is_concat(b) && to_app(b)->get_num_args() == 2 && m_util.is_zero(to_app(b)->get_arg(0))) { - // + // // a <=_u (concat 0 c) ---> a[h:l] = 0 && a[l-1:0] <=_u c // expr * b_1 = to_app(b)->get_arg(0); @@ -337,9 +337,9 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref if (!is_signed) { // Extended version of the rule above using is_zero_bit. // It also catches examples atoms such as: - // + // // a <=_u #x000f - // + // unsigned bv_sz = m_util.get_bv_size(b); unsigned i = bv_sz; unsigned first_non_zero = UINT_MAX; @@ -350,7 +350,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref break; } } - + if (first_non_zero == UINT_MAX) { // all bits are zero result = m().mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz)); @@ -361,7 +361,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b))); return BR_REWRITE3; } - + } #endif @@ -385,7 +385,7 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ result = arg; return BR_DONE; } - + numeral v; if (is_numeral(arg, v, sz)) { sz = high - low + 1; @@ -420,7 +420,7 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ if (idx > high) continue; // found first argument - if (idx <= low) { + if (idx <= low) { // result is a fragment of this argument if (low == idx && high - idx == curr_sz - 1) { result = curr; @@ -486,13 +486,13 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ m_mk_extract(high, low, to_app(arg)->get_arg(2))); return BR_REWRITE2; } - + return BR_FAILED; } br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { numeral r1, r2; - unsigned bv_size = get_bv_size(arg1); + unsigned bv_size = get_bv_size(arg1); unsigned sz; if (is_numeral(arg2, r2, sz)) { @@ -501,9 +501,9 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { result = arg1; return BR_DONE; } - + if (r2 >= numeral(bv_size)) { - result = mk_numeral(0, bv_size); + result = mk_numeral(0, bv_size); return BR_DONE; } @@ -511,7 +511,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { if (bv_size <= 64) { SASSERT(r1.is_uint64() && r2.is_uint64()); SASSERT(r2.get_uint64() < bv_size); - + uint64 r = shift_left(r1.get_uint64(), r2.get_uint64()); numeral rn(r, numeral::ui64()); rn = m_util.norm(rn, bv_size); @@ -519,7 +519,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } - + SASSERT(r2 < numeral(bv_size)); SASSERT(r2.is_unsigned()); r1 = m_util.norm(r1 * rational::power_of_two(r2.get_unsigned()), bv_size); @@ -539,10 +539,10 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { return BR_FAILED; } - + br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) { numeral r1, r2; - unsigned bv_size = get_bv_size(arg1); + unsigned bv_size = get_bv_size(arg1); unsigned sz; if (is_numeral(arg2, r2, sz)) { @@ -551,15 +551,15 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) { result = arg1; return BR_DONE; } - + if (r2 >= numeral(bv_size)) { result = mk_numeral(0, bv_size); return BR_DONE; } if (is_numeral(arg1, r1, sz)) { - if (bv_size <= 64) { - SASSERT(r1.is_uint64()); + if (bv_size <= 64) { + SASSERT(r1.is_uint64()); SASSERT(r2.is_uint64()); uint64 r = shift_right(r1.get_uint64(), r2.get_uint64()); numeral rn(r, numeral::ui64()); @@ -574,7 +574,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) { result = mk_numeral(r1, bv_size); return BR_DONE; } - + SASSERT(r2.is_pos()); SASSERT(r2 < numeral(bv_size)); // (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x)) @@ -652,13 +652,13 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) { result = mk_numeral(r1, bv_size); return BR_DONE; } - + // (bvashr (bvashr x r1) r2) --> (bvashr x r1+r2) if (is_num2 && m_util.is_bv_ashr(arg1) && is_numeral(to_app(arg1)->get_arg(1), r1, bv_size)) { r1 += r2; if (r1 > numeral(bv_size)) r1 = numeral(bv_size); - result = m().mk_app(get_fid(), OP_BASHR, + result = m().mk_app(get_fid(), OP_BASHR, to_app(arg1)->get_arg(0), mk_numeral(r1, bv_size)); return BR_REWRITE1; // not really needed at this time. @@ -694,7 +694,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e if (r2.is_zero()) { if (!hi_div0) { result = m().mk_app(get_fid(), OP_BSDIV0, arg1); - return BR_DONE; + return BR_REWRITE1; } else { // The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff) @@ -709,13 +709,13 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e result = arg1; return BR_DONE; } - + if (!r2.is_zero() && is_numeral(arg1, r1, bv_size)) { r1 = m_util.norm(r1, bv_size, true); result = mk_numeral(machine_div(r1, r2), bv_size); return BR_DONE; } - + result = m().mk_app(get_fid(), OP_BSDIV_I, arg1, arg2); return BR_DONE; } @@ -735,9 +735,9 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result) { numeral r1, r2; unsigned bv_size; - + TRACE("bv_udiv", tout << "hi_div0: " << hi_div0 << "\n";); - + TRACE("udiv2mul", tout << mk_ismt2_pp(arg2, m()) << " udiv2mul: " << m_udiv2mul << "\n";); if (is_numeral(arg2, r2, bv_size)) { @@ -745,13 +745,13 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e if (r2.is_zero()) { if (!hi_div0) { result = m().mk_app(get_fid(), OP_BUDIV0, arg1); - return BR_DONE; + return BR_REWRITE1; } else { // The "hardware interpretation" for (bvudiv x 0) is #xffff result = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size); return BR_DONE; - + } } @@ -765,7 +765,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e result = mk_numeral(machine_div(r1, r2), bv_size); return BR_DONE; } - + unsigned shift; if (r2.is_power_of_two(shift)) { result = m().mk_app(get_fid(), OP_BLSHR, arg1, mk_numeral(shift, bv_size)); @@ -808,7 +808,7 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e if (r2.is_zero()) { if (!hi_div0) { result = m().mk_app(get_fid(), OP_BSREM0, arg1); - return BR_DONE; + return BR_REWRITE1; } else { // The "hardware interpretation" for (bvsrem x 0) is x @@ -821,13 +821,13 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e result = mk_numeral(0, bv_size); return BR_DONE; } - + if (!r2.is_zero() && is_numeral(arg1, r1, bv_size)) { r1 = m_util.norm(r1, bv_size, true); result = mk_numeral(r1 % r2, bv_size); return BR_DONE; } - + result = m().mk_app(get_fid(), OP_BSREM_I, arg1, arg2); return BR_DONE; } @@ -890,7 +890,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e result = mk_numeral(0, bv_size); return BR_DONE; } - + if (!r2.is_zero() && is_num1) { r1 = m_util.norm(r1, bv_size); r1 %= r2; @@ -907,7 +907,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e result = m_util.mk_concat(2, args); return BR_REWRITE2; } - + result = m().mk_app(get_fid(), OP_BUREM_I, arg1, arg2); return BR_DONE; } @@ -921,7 +921,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e zero); return BR_REWRITE2; } - + // urem(x - 1, x) ==> ite(x = 0, urem0(x-1), x - 1) ==> ite(x = 0, urem0(-1), x - 1) expr * x; if (is_x_minus_one(arg1, x) && x == arg2) { @@ -942,7 +942,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e result = zero; return BR_DONE; } - + // urem(x - 1, x) --> x - 1 expr * x; if (is_x_minus_one(arg1, x) && x == arg2) { @@ -986,7 +986,7 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e result = arg1; return BR_DONE; } - + if (is_num1) { numeral abs_r1 = m_util.norm(abs(r1), bv_size); numeral abs_r2 = m_util.norm(abs(r2), bv_size); @@ -1012,7 +1012,7 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e return BR_REWRITE2; } } - + if (hi_div0) { result = m().mk_app(get_fid(), OP_BSMOD_I, arg1, arg2); return BR_DONE; @@ -1028,13 +1028,13 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e br_status bv_rewriter::mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result) { numeral val; bool is_int; - + if (m_autil.is_numeral(arg, val, is_int)) { val = m_util.norm(val, bv_size); result = mk_numeral(val, bv_size); return BR_DONE; } - + // (int2bv (bv2int x)) --> x if (m_util.is_bv2int(arg) && bv_size == get_bv_size(to_app(arg)->get_arg(0))) { result = to_app(arg)->get_arg(0); @@ -1051,7 +1051,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) { result = m_autil.mk_numeral(v, true); return BR_DONE; } - + // TODO: add other simplifications return BR_FAILED; @@ -1068,7 +1068,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re for (unsigned i = 0; i < num_args; i++) { expr * arg = args[i]; expr * prev = 0; - if (i > 0) + if (i > 0) prev = new_args.back(); if (is_numeral(arg, v1, sz1) && prev != 0 && is_numeral(prev, v2, sz2)) { v2 *= rational::power_of_two(sz1); @@ -1084,7 +1084,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re } expanded = true; } - else if (m_util.is_extract(arg) && + else if (m_util.is_extract(arg) && prev != 0 && m_util.is_extract(prev) && to_app(arg)->get_arg(0) == to_app(prev)->get_arg(0) && @@ -1101,7 +1101,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re new_args.push_back(arg); } } - if (!fused_numeral && !expanded && !fused_extract) + if (!fused_numeral && !expanded && !fused_extract) return BR_FAILED; SASSERT(!new_args.empty()); if (new_args.size() == 1) { @@ -1144,18 +1144,18 @@ br_status bv_rewriter::mk_sign_extend(unsigned n, expr * arg, expr_ref & result) result = mk_numeral(r, result_bv_size); return BR_DONE; } - + if (m_elim_sign_ext) { unsigned sz = get_bv_size(arg); expr * sign = m_mk_extract(sz-1, sz-1, arg); ptr_buffer args; - for (unsigned i = 0; i < n; i++) + for (unsigned i = 0; i < n; i++) args.push_back(sign); args.push_back(arg); result = m_util.mk_concat(args.size(), args.c_ptr()); return BR_REWRITE2; } - + return BR_FAILED; } @@ -1185,7 +1185,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re expr * arg = args[i]; if (m_util.is_bv_or(arg)) { unsigned num2 = to_app(arg)->get_num_args(); - for (unsigned j = 0; j < num2; j++) + for (unsigned j = 0; j < num2; j++) flat_args.push_back(to_app(arg)->get_arg(j)); } else { @@ -1244,12 +1244,12 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re result = mk_numeral(v1, sz); return BR_DONE; } - + // Simplifications of the form: // (bvor (concat x #x00) (concat #x00 y)) --> (concat x y) - if (new_args.size() == 2 && - num_coeffs == 0 && - m_util.is_concat(new_args[0]) && + if (new_args.size() == 2 && + num_coeffs == 0 && + m_util.is_concat(new_args[0]) && m_util.is_concat(new_args[1])) { app * concat1 = to_app(new_args[0]); app * concat2 = to_app(new_args[1]); @@ -1311,8 +1311,8 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re } std::reverse(exs.begin(), exs.end()); result = m_util.mk_concat(exs.size(), exs.c_ptr()); - TRACE("mask_bug", - tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_ismt2_pp(t, m()) << ")\n"; + TRACE("mask_bug", + tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_ismt2_pp(t, m()) << ")\n"; tout << mk_ismt2_pp(result, m()) << "))\n";); return BR_REWRITE2; } @@ -1324,7 +1324,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re if (!v1.is_zero()) { new_args.push_back(mk_numeral(v1, sz)); } - + switch (new_args.size()) { case 0: result = mk_numeral(0, sz); @@ -1354,7 +1354,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r expr * arg = args[i]; if (m_util.is_bv_xor(arg)) { unsigned num2 = to_app(arg)->get_num_args(); - for (unsigned j = 0; j < num2; j++) + for (unsigned j = 0; j < num2; j++) flat_args.push_back(to_app(arg)->get_arg(j)); } else { @@ -1367,7 +1367,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r args = flat_args.c_ptr(); } } - + expr_fast_mark1 pos_args; expr_fast_mark2 neg_args; bool merged = false; @@ -1380,7 +1380,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r num_coeffs++; continue; } - + if (m_util.is_bv_not(arg)) { expr * atom = to_app(arg)->get_arg(0); if (neg_args.is_marked(atom)) { @@ -1411,14 +1411,14 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r } } } - + // XOR is a mask // All arguments but one is a numeral. - // + // // Apply a transformation of the form: // // (bvxor a 0011) --> (concat ((_ extract 3 2) a) ((_ extract 1 0) (bvnot a))) - // + // if (!v1.is_zero() && num_coeffs == num - 1) { // find argument that is not a numeral expr * t = 0; @@ -1453,12 +1453,12 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r } } std::reverse(exs.c_ptr(), exs.c_ptr() + exs.size()); - if (exs.size() == 1) + if (exs.size() == 1) result = exs[0]; else result = m_util.mk_concat(exs.size(), exs.c_ptr()); return BR_REWRITE3; - } + } if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1)))) && (!m_bv_sort_ac || is_sorted(num, args))) @@ -1487,7 +1487,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r pos_args.mark(arg, false); } } - + switch (new_args.size()) { case 0: result = mk_numeral(0, sz); @@ -1653,7 +1653,7 @@ br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) { br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result) { br_status st = mk_add_core(num_args, args, result); - if (st != BR_FAILED && st != BR_DONE) + if (st != BR_FAILED && st != BR_DONE) return st; #if 0 expr * x; @@ -1673,14 +1673,14 @@ br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_re return st; if (!m_util.is_concat(y) && !is_numeral(y)) return st; - + unsigned sz = get_bv_size(x); - + for (unsigned i = 0; i < sz; i++) { if (!is_zero_bit(x,i) && !is_zero_bit(y,i)) return st; } - + result = m().mk_app(get_fid(), OP_BOR, x, y); return BR_REWRITE1; #else @@ -1747,7 +1747,7 @@ bool bv_rewriter::is_zero_bit(expr * x, unsigned idx) { br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result) { br_status st = mk_mul_core(num_args, args, result); - if (st != BR_FAILED && st != BR_DONE) + if (st != BR_FAILED && st != BR_DONE) return st; expr * x; expr * y; @@ -1761,7 +1761,7 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re else { return st; } - + if (m_mul2concat) { numeral v; unsigned bv_size; @@ -1810,12 +1810,12 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { result = m().mk_eq(to_app(lhs)->get_arg(0), mk_numeral(numeral(1) - v, 1)); return BR_REWRITE1; } - + bool is_one = v.is_one(); expr_ref bit1(m()); bit1 = is_one ? rhs : mk_numeral(numeral(1), 1); - + if (m_util.is_bv_or(lhs)) { ptr_buffer new_args; unsigned num = to_app(lhs)->get_num_args(); @@ -1831,8 +1831,8 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { return BR_REWRITE3; } } - - + + if (m_util.is_bv_xor(lhs)) { ptr_buffer new_args; unsigned num = to_app(lhs)->get_num_args(); @@ -1849,7 +1849,7 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { return BR_REWRITE3; } } - + return BR_FAILED; } @@ -1861,14 +1861,14 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu TRACE("blast_eq_value", tout << "sz: " << sz << "\n" << mk_ismt2_pp(lhs, m()) << "\n";); if (is_numeral(lhs)) std::swap(lhs, rhs); - + numeral v; if (!is_numeral(rhs, v, sz)) return BR_FAILED; if (!m_util.is_bv_or(lhs) && !m_util.is_bv_xor(lhs) && !m_util.is_bv_not(lhs)) return BR_FAILED; - + numeral two(2); ptr_buffer new_args; for (unsigned i = 0; i < sz; i++) { @@ -1888,7 +1888,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { if (m_util.is_concat(lhs)) { num1 = to_app(lhs)->get_num_args(); - args1 = to_app(lhs)->get_args(); + args1 = to_app(lhs)->get_args(); } else { num1 = 1; @@ -1897,7 +1897,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { if (m_util.is_concat(rhs)) { num2 = to_app(rhs)->get_num_args(); - args2 = to_app(rhs)->get_args(); + args2 = to_app(rhs)->get_args(); } else { num2 = 1; @@ -1930,7 +1930,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { new_eqs.push_back(m().mk_eq(m_mk_extract(sz1 - 1, low1, arg1), m_mk_extract(rsz1 + low2 - 1, low2, arg2))); low1 = 0; - low2 += rsz1; + low2 += rsz1; --i1; } else { @@ -1948,8 +1948,8 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { } bool bv_rewriter::is_concat_split_target(expr * t) const { - return - m_split_concat_eq || + return + m_split_concat_eq || m_util.is_concat(t) || m_util.is_numeral(t) || m_util.is_bv_or(t); @@ -1964,7 +1964,7 @@ void bv_rewriter::mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & r SASSERT(is_numeral(c)); if (is_minus_one_times_t(t1)) result = m().mk_eq(t2, m_util.mk_bv_sub(c, t1)); - else + else result = m().mk_eq(t1, m_util.mk_bv_sub(c, t2)); } @@ -2024,14 +2024,14 @@ bool bv_rewriter::has_numeral(app* a) const { } br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) { - + expr * c, * x; numeral c_val, c_inv_val; unsigned sz; - if (m_util.is_bv_mul(lhs, c, x) && - m_util.is_numeral(c, c_val, sz) && + if (m_util.is_bv_mul(lhs, c, x) && + m_util.is_numeral(c, c_val, sz) && m_util.mult_inverse(c_val, sz, c_inv_val)) { - + SASSERT(m_util.norm(c_val * c_inv_val, sz).is_one()); numeral rhs_val; @@ -2048,7 +2048,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) { if (m_util.is_bv_mul(rhs, c2, x2) && m_util.is_numeral(c2, c2_val, sz)) { // x = c_inv * c2 * x2 numeral new_c2 = m_util.norm(c_inv_val * c2_val, sz); - if (new_c2.is_one()) + if (new_c2.is_one()) result = m().mk_eq(x, x2); else result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val * c2_val, sz), x2)); @@ -2077,7 +2077,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) { } } if (found) { - result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz), + result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz), m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs)); return BR_REWRITE3; } @@ -2095,7 +2095,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { result = m().mk_false(); return BR_DONE; } - + bool swapped = false; if (is_numeral(lhs)) { swapped = true; @@ -2120,7 +2120,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";); return st; } - + if (m_blast_eq_value) { st = mk_blast_eq_value(lhs, rhs, result); if (st != BR_FAILED) @@ -2142,10 +2142,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { new_lhs = lhs; new_rhs = rhs; } - + lhs = new_lhs; rhs = new_rhs; - // Try to rewrite t1 + t2 = c --> t1 = c - t2 + // Try to rewrite t1 + t2 = c --> t1 = c - t2 // Reason: it is much cheaper to bit-blast. if (isolate_term(lhs, rhs, result)) { return BR_REWRITE2; @@ -2155,7 +2155,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { } if (st != BR_FAILED) { - result = m().mk_eq(lhs, rhs); + result = m().mk_eq(lhs, rhs); return BR_DONE; } } diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 78d3fb4f1..f01743ca9 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -155,7 +155,7 @@ public: void updt_params(params_ref const & p); static void get_param_descrs(param_descrs & r); - + void set_mkbv2num(bool f) { m_mkbv2num = f; } unsigned get_bv_size(expr * t) const {return m_util.get_bv_size(t); } @@ -164,7 +164,7 @@ public: bool is_bv(expr * t) const { return m_util.is_bv(t); } expr * mk_numeral(numeral const & v, unsigned sz) { return m_util.mk_numeral(v, sz); } expr * mk_numeral(unsigned v, unsigned sz) { return m_util.mk_numeral(numeral(v), sz); } - + br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { if (mk_app_core(f, num_args, args, result) == BR_FAILED) @@ -174,6 +174,8 @@ public: br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); bool hi_div0() const { return m_hi_div0; } + + bv_util & get_util() { return m_util; } }; #endif diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 7488e6b18..1697b74ed 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -49,9 +49,9 @@ struct evaluator_cfg : public default_rewriter_cfg { evaluator_cfg(ast_manager & m, model & md, params_ref const & p): m_model(md), m_b_rw(m), - // We must allow customers to set parameters for arithmetic rewriter/evaluator. + // We must allow customers to set parameters for arithmetic rewriter/evaluator. // In particular, the maximum degree of algebraic numbers that will be evaluated. - m_a_rw(m, p), + m_a_rw(m, p), m_bv_rw(m), // See comment above. We want to allow customers to set :sort-store m_ar_rw(m, p), @@ -73,7 +73,7 @@ struct evaluator_cfg : public default_rewriter_cfg { m_model_completion = p.completion(); m_cache = p.cache(); } - + ast_manager & m() const { return m_model.get_manager(); } bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) { @@ -89,11 +89,11 @@ struct evaluator_cfg : public default_rewriter_cfg { SASSERT(fi->get_arity() == num); bool actuals_are_values = true; - + for (unsigned i = 0; actuals_are_values && i < num; i++) { actuals_are_values = m().is_value(args[i]); } - + if (!actuals_are_values) return false; // let get_macro handle it @@ -115,7 +115,7 @@ struct evaluator_cfg : public default_rewriter_cfg { result = val; return BR_DONE; } - + if (m_model_completion) { sort * s = f->get_range(); expr * val = m_model.get_some_value(s); @@ -154,7 +154,7 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_a_rw.mk_app_core(f, num, args, result); else if (fid == m_bv_rw.get_fid()) st = m_bv_rw.mk_app_core(f, num, args, result); - else if (fid == m_ar_rw.get_fid()) + else if (fid == m_ar_rw.get_fid()) st = m_ar_rw.mk_app_core(f, num, args, result); else if (fid == m_dt_rw.get_fid()) st = m_dt_rw.mk_app_core(f, num, args, result); @@ -180,9 +180,10 @@ struct evaluator_cfg : public default_rewriter_cfg { return st; } - bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { + bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { + TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";); - func_interp * fi = m_model.get_func_interp(f); + func_interp * fi = m_model.get_func_interp(f); if (fi != 0) { if (fi->is_partial()) { if (m_model_completion) { @@ -193,13 +194,16 @@ struct evaluator_cfg : public default_rewriter_cfg { else { return false; } - } + } def = fi->get_interp(); SASSERT(def != 0); return true; } - if (f->get_family_id() == null_family_id && m_model_completion) { + if (m_model_completion && + (f->get_family_id() == null_family_id || + m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) + { sort * s = f->get_range(); expr * val = m_model.get_some_value(s); func_interp * new_fi = alloc(func_interp, m(), f->get_arity()); @@ -211,8 +215,8 @@ struct evaluator_cfg : public default_rewriter_cfg { return false; } - - bool max_steps_exceeded(unsigned num_steps) const { + + bool max_steps_exceeded(unsigned num_steps) const { cooperate("model evaluator"); if (memory::get_allocation_size() > m_max_memory) throw rewriter_exception(Z3_MAX_MEMORY_MSG); @@ -228,7 +232,7 @@ template class rewriter_tpl; struct model_evaluator::imp : public rewriter_tpl { evaluator_cfg m_cfg; imp(model & md, params_ref const & p): - rewriter_tpl(md.get_manager(), + rewriter_tpl(md.get_manager(), false, // no proofs for evaluator m_cfg), m_cfg(md.get_manager(), md, p) { diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 54c67feca..66676c619 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -76,7 +76,7 @@ void invoke_gdb() { for (;;) { std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n"; char result; - bool ok = (std::cin >> result); + bool ok = bool(std::cin >> result); if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached. switch(result) { case 'C':