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/api/z3_api.h b/src/api/z3_api.h index b37c963b4..d31d958f7 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5642,6 +5642,9 @@ extern "C" { if the result is \c Z3_L_UNDEF, but the returned model is not guaranteed to satisfy quantified assertions. + \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. + Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc. + def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),)) */ Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c); @@ -5662,6 +5665,9 @@ extern "C" { The solver supports the commands #Z3_solver_push and #Z3_solver_pop, but it will always solve each #Z3_solver_check from scratch. + \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. + Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc. + def_API('Z3_mk_solver_from_tactic', SOLVER, (_in(CONTEXT), _in(TACTIC))) */ Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t); 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/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 1d66b793d..40bb7efe8 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -419,11 +419,16 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, dbg_decouple("fpa2bv_add_exp_delta", exp_delta); - // cap the delta - expr_ref cap(m), cap_le_delta(m); - cap = m_bv_util.mk_numeral(sbits+2, ebits); - cap_le_delta = m_bv_util.mk_ule(cap, exp_delta); - m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta); + if (log2(sbits + 2) < ebits + 2) + { + // cap the delta + expr_ref cap(m), cap_le_delta(m); + cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2); + cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta)); + m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta); + exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta); + dbg_decouple("fpa2bv_add_exp_cap", cap); + } dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.cpp b/src/ast/rewriter/bit_blaster/bit_blaster.cpp index 153066711..1055ceb58 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster.cpp @@ -21,10 +21,10 @@ Revision History: #include"ast_pp.h" #include"bv_decl_plugin.h" -bit_blaster_cfg::bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, basic_simplifier_plugin & _s): +bit_blaster_cfg::bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool_rewriter& rw): m_util(u), m_params(p), - s(_s) { + m_rw(rw) { } static void sort_args(expr * & l1, expr * & l2, expr * & l3) { @@ -47,30 +47,30 @@ void bit_blaster_cfg::mk_xor3(expr * l1, expr * l2, expr * l3, expr_ref & r) { else if (l2 == l3) r = l1; else if (m().is_complement(l1, l2)) - s.mk_not(l3, r); + m_rw.mk_not(l3, r); else if (m().is_complement(l1, l3)) - s.mk_not(l2, r); + m_rw.mk_not(l2, r); else if (m().is_complement(l2, l3)) - s.mk_not(l1, r); + m_rw.mk_not(l1, r); else if (m().is_true(l1)) - s.mk_iff(l2, l3, r); + m_rw.mk_iff(l2, l3, r); else if (m().is_false(l1)) - s.mk_xor(l2, l3, r); + m_rw.mk_xor(l2, l3, r); else if (m().is_true(l2)) - s.mk_iff(l1, l3, r); + m_rw.mk_iff(l1, l3, r); else if (m().is_false(l2)) - s.mk_xor(l1, l3, r); + m_rw.mk_xor(l1, l3, r); else if (m().is_true(l3)) - s.mk_iff(l1, l2, r); + m_rw.mk_iff(l1, l2, r); else if (m().is_false(l3)) - s.mk_xor(l1, l2, r); + m_rw.mk_xor(l1, l2, r); else r = m().mk_app(m_util.get_family_id(), OP_XOR3, l1, l2, l3); } else { expr_ref t(m()); - s.mk_xor(l1, l2, t); - s.mk_xor(t, l3, r); + m_rw.mk_xor(l1, l2, t); + m_rw.mk_xor(t, l3, r); } } @@ -90,17 +90,17 @@ void bit_blaster_cfg::mk_carry(expr * l1, expr * l2, expr * l3, expr_ref & r) { else if (l1 == l2 && l1 == l3) r = l1; else if (m().is_false(l1)) - s.mk_and(l2, l3, r); + m_rw.mk_and(l2, l3, r); else if (m().is_false(l2)) - s.mk_and(l1, l3, r); + m_rw.mk_and(l1, l3, r); else if (m().is_false(l3)) - s.mk_and(l1, l2, r); + m_rw.mk_and(l1, l2, r); else if (m().is_true(l1)) - s.mk_or(l2, l3, r); + m_rw.mk_or(l2, l3, r); else if (m().is_true(l2)) - s.mk_or(l1, l3, r); + m_rw.mk_or(l1, l3, r); else if (m().is_true(l3)) - s.mk_or(l1, l2, r); + m_rw.mk_or(l1, l2, r); else if (m().is_complement(l1, l2)) r = l3; else if (m().is_complement(l1, l3)) @@ -112,17 +112,17 @@ void bit_blaster_cfg::mk_carry(expr * l1, expr * l2, expr * l3, expr_ref & r) { } else { expr_ref t1(m()), t2(m()), t3(m()); - s.mk_and(l1, l2, t1); - s.mk_and(l1, l3, t2); - s.mk_and(l2, l3, t3); - s.mk_or(t1, t2, t3, r); + m_rw.mk_and(l1, l2, t1); + m_rw.mk_and(l1, l3, t2); + m_rw.mk_and(l2, l3, t3); + m_rw.mk_or(t1, t2, t3, r); } } template class bit_blaster_tpl; bit_blaster::bit_blaster(ast_manager & m, bit_blaster_params const & params): - bit_blaster_tpl(bit_blaster_cfg(m_util, params, m_simp)), + bit_blaster_tpl(bit_blaster_cfg(m_util, params, m_rw)), m_util(m), - m_simp(m) { + m_rw(m) { } diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h index 958c79b4d..6221eeaf9 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster.h @@ -19,7 +19,7 @@ Revision History: #ifndef BIT_BLASTER_H_ #define BIT_BLASTER_H_ -#include"basic_simplifier_plugin.h" +#include"bool_rewriter.h" #include"bit_blaster_params.h" #include"bit_blaster_tpl.h" #include"bv_decl_plugin.h" @@ -31,31 +31,31 @@ public: protected: bv_util & m_util; bit_blaster_params const & m_params; - basic_simplifier_plugin & s; + bool_rewriter & m_rw; public: - bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, basic_simplifier_plugin & _s); + bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool_rewriter& rw); ast_manager & m() const { return m_util.get_manager(); } numeral power(unsigned n) const { return rational::power_of_two(n); } - void mk_xor(expr * a, expr * b, expr_ref & r) { s.mk_xor(a, b, r); } + void mk_xor(expr * a, expr * b, expr_ref & r) { m_rw.mk_xor(a, b, r); } void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r); void mk_carry(expr * a, expr * b, expr * c, expr_ref & r); - void mk_iff(expr * a, expr * b, expr_ref & r) { s.mk_iff(a, b, r); } - void mk_and(expr * a, expr * b, expr_ref & r) { s.mk_and(a, b, r); } - void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { s.mk_and(a, b, c, r); } - void mk_and(unsigned sz, expr * const * args, expr_ref & r) { s.mk_and(sz, args, r); } - void mk_or(expr * a, expr * b, expr_ref & r) { s.mk_or(a, b, r); } - void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { s.mk_or(a, b, c, r); } - void mk_or(unsigned sz, expr * const * args, expr_ref & r) { s.mk_or(sz, args, r); } - void mk_not(expr * a, expr_ref & r) { s.mk_not(a, r); } - void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { s.mk_ite(c, t, e, r); } - void mk_nand(expr * a, expr * b, expr_ref & r) { s.mk_nand(a, b, r); } - void mk_nor(expr * a, expr * b, expr_ref & r) { s.mk_nor(a, b, r); } + void mk_iff(expr * a, expr * b, expr_ref & r) { m_rw.mk_iff(a, b, r); } + void mk_and(expr * a, expr * b, expr_ref & r) { m_rw.mk_and(a, b, r); } + void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_and(a, b, c, r); } + void mk_and(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_and(sz, args, r); } + void mk_or(expr * a, expr * b, expr_ref & r) { m_rw.mk_or(a, b, r); } + void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_or(a, b, c, r); } + void mk_or(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_or(sz, args, r); } + void mk_not(expr * a, expr_ref & r) { m_rw.mk_not(a, r); } + void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rw.mk_ite(c, t, e, r); } + void mk_nand(expr * a, expr * b, expr_ref & r) { m_rw.mk_nand(a, b, r); } + void mk_nor(expr * a, expr * b, expr_ref & r) { m_rw.mk_nor(a, b, r); } }; class bit_blaster : public bit_blaster_tpl { bv_util m_util; - basic_simplifier_plugin m_simp; + bool_rewriter m_rw; public: bit_blaster(ast_manager & m, bit_blaster_params const & params); bit_blaster_params const & get_params() const { return this->m_params; } diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index bf9e7f394..49c68fedf 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -362,6 +362,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); return BR_FAILED; } + if (m().is_ite(f)) { SASSERT(num == 3); if (butil().is_bv(args[1])) { diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 53f058fb4..15b87697f 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -23,6 +23,7 @@ Revision History: #include"common_msgs.h" #include"rewriter_types.h" + template void bit_blaster_tpl::checkpoint() { if (memory::get_allocation_size() > m_max_memory) @@ -173,7 +174,7 @@ void bit_blaster_tpl::mk_multiplier(unsigned sz, expr * const * a_bits, exp SASSERT(sz == out_bits.size()); return; } - + if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) { SASSERT(sz == out_bits.size()); return; diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 6a652c2f7..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)); } @@ -2010,8 +2010,8 @@ bool bv_rewriter::is_add_mul_const(expr* e) const { bool bv_rewriter::is_concat_target(expr* lhs, expr* rhs) const { return - (m_util.is_concat(lhs) && (is_concat_split_target(rhs) || has_numeral(to_app(lhs)))) || - (m_util.is_concat(rhs) && (is_concat_split_target(lhs) || has_numeral(to_app(rhs)))); + (m_util.is_concat(lhs) && is_concat_split_target(rhs)) || + (m_util.is_concat(rhs) && is_concat_split_target(lhs)); } bool bv_rewriter::has_numeral(app* a) const { @@ -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/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 89b9bb90f..c65f51144 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -875,6 +875,10 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { if (m().is_false(cond)) { continue; } + if (m().is_true(cond)) { + add_next(next, trail, mv.dst(), acc); + continue; + } expr* args[2] = { cond, acc }; cond = mk_and(m(), 2, args); add_next(next, trail, mv.dst(), cond); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 0eac9d316..05edb35c8 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -3,11 +3,11 @@ Copyright (c) 2011 Microsoft Corporation Module Name: - dl_decl_plugin.h + seq_decl_plugin.h Abstract: - + decl_plugin for the theory of sequences Author: @@ -43,7 +43,7 @@ static bool is_escape_char(char const *& s, unsigned& result) { if (*s != '\\' || *(s + 1) == 0) { return false; } - if (*(s + 1) == 'x' && + if (*(s + 1) == 'x' && is_hex_digit(*(s + 2), d1) && is_hex_digit(*(s + 3), d2)) { result = d1*16 + d2; s += 4; @@ -100,7 +100,7 @@ zstring::zstring(char const* s, encoding enc): m_encoding(enc) { if (is_escape_char(s, ch)) { m_buffer.push_back(ch); } - else { + else { m_buffer.push_back(*s); ++s; } @@ -115,7 +115,7 @@ zstring::zstring(zstring const& other) { zstring::zstring(unsigned num_bits, bool const* ch) { SASSERT(num_bits == 8 || num_bits == 16); m_encoding = (num_bits == 8)?ascii:unicode; - unsigned n = 0; + unsigned n = 0; for (unsigned i = 0; i < num_bits; ++i) { n |= (((unsigned)ch[i]) << i); } @@ -161,10 +161,10 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const { } static const char esc_table[32][6] = - { "\\x00", "\\x01", "\\x02", "\\x03", "\\x04", "\\x05", "\\x06", "\\x07", "\\x08", "\\x09", "\\n", "\\v", "\\f", "\\r", "\\x0E", "\\x0F", + { "\\x00", "\\x01", "\\x02", "\\x03", "\\x04", "\\x05", "\\x06", "\\x07", "\\x08", "\\x09", "\\n", "\\v", "\\f", "\\r", "\\x0E", "\\x0F", "\\x10", "\\x11", "\\x12", "\\x13", "\\x14", "\\x15", "\\x16", "\\x17", "\\x18", "\\x19", "\\x1A", "\\x1B", "\\x1C", "\\x1D", "\\x1E", "\\x1F" }; - + std::string zstring::encode() const { SASSERT(m_encoding == ascii); std::ostringstream strm; @@ -173,6 +173,9 @@ std::string zstring::encode() const { if (0 <= ch && ch < 32) { strm << esc_table[ch]; } + else if (ch == '\\') { + strm << "\\\\"; + } else { strm << (char)(ch); } @@ -220,7 +223,7 @@ int zstring::indexof(zstring const& other, int offset) const { bool prefix = true; for (unsigned j = 0; prefix && j < other.length(); ++j) { prefix = m_buffer[i + j] == other[j]; - } + } if (prefix) { return static_cast(i); } @@ -250,7 +253,7 @@ std::ostream& zstring::operator<<(std::ostream& out) const { } -seq_decl_plugin::seq_decl_plugin(): m_init(false), +seq_decl_plugin::seq_decl_plugin(): m_init(false), m_stringc_sym("String"), m_charc_sym("Char"), m_string(0), @@ -258,7 +261,7 @@ seq_decl_plugin::seq_decl_plugin(): m_init(false), m_re(0) {} void seq_decl_plugin::finalize() { - for (unsigned i = 0; i < m_sigs.size(); ++i) + for (unsigned i = 0; i < m_sigs.size(); ++i) dealloc(m_sigs[i]); m_manager->dec_ref(m_string); m_manager->dec_ref(m_char); @@ -266,7 +269,7 @@ void seq_decl_plugin::finalize() { } bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) { - return + return s->get_name().is_numerical() && (idx = s->get_name().get_num(), true); } @@ -283,7 +286,7 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { return true; } - + if (s->get_family_id() == sP->get_family_id() && s->get_decl_kind() == sP->get_decl_kind() && s->get_num_parameters() == sP->get_num_parameters()) { @@ -308,7 +311,7 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { ptr_vector binding; ast_manager& m = *m_manager; - TRACE("seq_verbose", + TRACE("seq_verbose", tout << sig.m_name << ": "; for (unsigned i = 0; i < dsz; ++i) tout << mk_pp(dom[i], m) << " "; if (range) tout << " range: " << mk_pp(range, m); @@ -375,7 +378,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran for (unsigned i = 0; i < dsz; ++i) { strm << mk_pp(sig.m_dom[i].get(), m) << " "; } - + m.raise_exception(strm.str().c_str()); } if (!range && dsz == 0) { @@ -438,7 +441,7 @@ void seq_decl_plugin::init() { m_sigs.resize(LAST_SEQ_OP); // TBD: have (par ..) construct and load parameterized signature from premable. m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA); - m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq.empty", 1, 0, 0, seqA); + m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq.empty", 1, 0, 0, seqA); m_sigs[OP_SEQ_CONCAT] = alloc(psig, m, "seq.++", 1, 2, seqAseqA, seqA); m_sigs[OP_SEQ_PREFIX] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_SUFFIX] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT); @@ -548,10 +551,10 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons match_right_assoc(*m_sigs[k], arity, domain, range, rng); func_decl_info info(m_family_id, k_seq); info.set_right_associative(); - return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info); + return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info); } -func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { init(); ast_manager& m = *m_manager; @@ -568,7 +571,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, func_decl_info info(m_family_id, k, 1, ¶m); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, info); } - + case OP_SEQ_UNIT: case OP_RE_PLUS: case OP_RE_STAR: @@ -593,7 +596,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, } match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET)); - + case OP_RE_LOOP: switch (arity) { case 1: @@ -601,7 +604,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, if (num_parameters == 0 || num_parameters > 2 || !parameters[0].is_int() || (num_parameters == 2 && !parameters[1].is_int())) { m.raise_exception("Expecting two numeral parameters to function re-loop"); } - return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); + return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); case 2: if (m_re != domain[0] || !arith_util(m).is_int(domain[1])) { m.raise_exception("Incorrect type of arguments passed to re.loop. Expecting regular expression and two integer parameters"); @@ -613,26 +616,26 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, domain[0], func_decl_info(m_family_id, k, num_parameters, parameters)); default: - m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters"); + m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters"); } - + case OP_STRING_CONST: if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) { m.raise_exception("invalid string declaration"); - } + } return m.mk_const_decl(m_stringc_sym, m_string, func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters)); - + case OP_RE_UNION: - case OP_RE_CONCAT: - case OP_RE_INTERSECT: + case OP_RE_CONCAT: + case OP_RE_INTERSECT: return mk_assoc_fun(k, arity, domain, range, k, k); - case OP_SEQ_CONCAT: + case OP_SEQ_CONCAT: return mk_assoc_fun(k, arity, domain, range, k, _OP_STRING_CONCAT); - case _OP_STRING_CONCAT: + case _OP_STRING_CONCAT: return mk_assoc_fun(k, arity, domain, range, OP_SEQ_CONCAT, k); case OP_SEQ_REPLACE: @@ -743,8 +746,8 @@ app* seq_decl_plugin::mk_string(zstring const& s) { bool seq_decl_plugin::is_value(app* e) const { - return - is_app_of(e, m_family_id, OP_SEQ_EMPTY) || + return + is_app_of(e, m_family_id, OP_SEQ_EMPTY) || (is_app_of(e, m_family_id, OP_SEQ_UNIT) && m_manager->is_value(e->get_arg(0))); } @@ -782,7 +785,7 @@ app* seq_util::str::mk_char(char ch) { zstring s(ch, zstring::ascii); return mk_char(s, 0); } - + bool seq_util::str::is_char(expr* n, zstring& c) const { if (u.is_char(n)) { c = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str()); @@ -809,7 +812,7 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const { while (is_concat(e, e1, e2)) { get_concat(e1, es); e = e2; - } + } if (!is_empty(e)) { es.push_back(e); } @@ -835,7 +838,7 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& h return true; } } - return false; + return false; } bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) { @@ -847,5 +850,5 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) { return true; } } - return false; + return false; } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index a83878b0e..4739af84b 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -7,7 +7,7 @@ Module Name: Abstract: - + decl_plugin for the theory of sequences Author: @@ -41,7 +41,7 @@ enum seq_op_kind { OP_SEQ_EXTRACT, OP_SEQ_REPLACE, OP_SEQ_AT, - OP_SEQ_LENGTH, + OP_SEQ_LENGTH, OP_SEQ_INDEX, OP_SEQ_TO_RE, OP_SEQ_IN_RE, @@ -61,19 +61,19 @@ enum seq_op_kind { // string specific operators. OP_STRING_CONST, - OP_STRING_ITOS, - OP_STRING_STOI, + OP_STRING_ITOS, + OP_STRING_STOI, // internal only operators. Converted to SEQ variants. - _OP_STRING_STRREPL, - _OP_STRING_CONCAT, - _OP_STRING_LENGTH, + _OP_STRING_STRREPL, + _OP_STRING_CONCAT, + _OP_STRING_LENGTH, _OP_STRING_STRCTN, - _OP_STRING_PREFIX, - _OP_STRING_SUFFIX, - _OP_STRING_IN_REGEXP, - _OP_STRING_TO_REGEXP, - _OP_STRING_CHARAT, - _OP_STRING_SUBSTR, + _OP_STRING_PREFIX, + _OP_STRING_SUFFIX, + _OP_STRING_IN_REGEXP, + _OP_STRING_TO_REGEXP, + _OP_STRING_CHARAT, + _OP_STRING_SUBSTR, _OP_STRING_STRIDOF, _OP_REGEXP_EMPTY, _OP_REGEXP_FULL, @@ -85,10 +85,10 @@ enum seq_op_kind { class zstring { public: enum encoding { - ascii, + ascii, unicode }; -private: +private: buffer m_buffer; encoding m_encoding; public: @@ -101,7 +101,7 @@ public: zstring replace(zstring const& src, zstring const& dst) const; unsigned num_bits() const { return (m_encoding==ascii)?8:16; } encoding get_encoding() const { return m_encoding; } - std::string encode() const; + std::string encode() const; unsigned length() const { return m_buffer.size(); } unsigned operator[](unsigned i) const { return m_buffer[i]; } bool empty() const { return m_buffer.empty(); } @@ -113,7 +113,7 @@ public: zstring operator+(zstring const& other) const; std::ostream& operator<<(std::ostream& out) const; }; - + class seq_decl_plugin : public decl_plugin { struct psig { symbol m_name; @@ -161,18 +161,18 @@ public: virtual ~seq_decl_plugin() {} virtual void finalize(); - + virtual decl_plugin * mk_fresh() { return alloc(seq_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 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 * e) const; virtual bool is_unique_value(app * e) const { return is_value(e); } @@ -181,8 +181,8 @@ public: bool is_char(ast* a) const { return a == m_char; } - app* mk_string(symbol const& s); - app* mk_string(zstring const& s); + app* mk_string(symbol const& s); + app* mk_string(zstring const& s); }; @@ -244,12 +244,12 @@ public: bool is_string(expr const* n, symbol& s) const { return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true); } - + bool is_string(expr const* n, zstring& s) const; bool is_char(expr* n, zstring& s) const; - bool is_empty(expr const* n) const { symbol s; - return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); + bool is_empty(expr const* n) const { symbol s; + return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); } bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); } @@ -265,7 +265,7 @@ public: bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } - + MATCH_BINARY(is_concat); MATCH_UNARY(is_length); MATCH_TERNARY(is_extract); @@ -278,7 +278,7 @@ public: MATCH_BINARY(is_suffix); MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); - MATCH_BINARY(is_in_re); + MATCH_BINARY(is_in_re); MATCH_UNARY(is_unit); void get_concat(expr* e, expr_ref_vector& es) const; @@ -301,7 +301,7 @@ public: app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); } app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); } app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); } - app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); } + app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); } app* mk_loop(expr* r, unsigned lo); app* mk_loop(expr* r, unsigned lo, unsigned hi); @@ -325,23 +325,23 @@ public: MATCH_UNARY(is_plus); MATCH_UNARY(is_opt); bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi); - bool is_loop(expr const* n, expr*& body, unsigned& lo); + bool is_loop(expr const* n, expr*& body, unsigned& lo); }; str str; re re; - seq_util(ast_manager& m): - m(m), + seq_util(ast_manager& m): + m(m), seq(*static_cast(m.get_plugin(m.mk_family_id("seq")))), m_fid(seq.get_family_id()), str(*this), - re(*this) { + re(*this) { } ~seq_util() {} family_id get_family_id() const { return m_fid; } - + }; #endif /* SEQ_DECL_PLUGIN_H_ */ diff --git a/src/ast/simplifier/fpa_simplifier_plugin.cpp b/src/ast/simplifier/fpa_simplifier_plugin.cpp index 4aba9c76c..5775f1af0 100644 --- a/src/ast/simplifier/fpa_simplifier_plugin.cpp +++ b/src/ast/simplifier/fpa_simplifier_plugin.cpp @@ -24,16 +24,16 @@ m_rw(m) {} fpa_simplifier_plugin::~fpa_simplifier_plugin() {} bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); + set_reduce_invoked(); SASSERT(f->get_family_id() == get_family_id()); - return m_rw.mk_app_core(f, num_args, args, result) == BR_DONE; + return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED; } bool fpa_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { set_reduce_invoked(); - return m_rw.mk_eq_core(lhs, rhs, result) == BR_DONE; + return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED; } diff --git a/src/ast/simplifier/seq_simplifier_plugin.cpp b/src/ast/simplifier/seq_simplifier_plugin.cpp new file mode 100644 index 000000000..0b7bddf0a --- /dev/null +++ b/src/ast/simplifier/seq_simplifier_plugin.cpp @@ -0,0 +1,39 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + seq_simplifier_plugin.cpp + +Abstract: + + Simplifier for the theory of sequences + +Author: + + Nikolaj Bjorner (nbjorner) 2016-02-05 + +--*/ +#include"seq_simplifier_plugin.h" + +seq_simplifier_plugin::seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b) : +simplifier_plugin(symbol("seq"), m), +m_util(m), +m_rw(m) {} + +seq_simplifier_plugin::~seq_simplifier_plugin() {} + +bool seq_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { + set_reduce_invoked(); + + SASSERT(f->get_family_id() == get_family_id()); + + return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED; +} + +bool seq_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { + set_reduce_invoked(); + + return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED; +} + diff --git a/src/ast/simplifier/seq_simplifier_plugin.h b/src/ast/simplifier/seq_simplifier_plugin.h new file mode 100644 index 000000000..45668678c --- /dev/null +++ b/src/ast/simplifier/seq_simplifier_plugin.h @@ -0,0 +1,39 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + seq_simplifier_plugin.h + +Abstract: + + Simplifier for the sequence theory + +Author: + + Nikolaj Bjorner (nbjorner) 2016-02-05 + +--*/ +#ifndef SEQ_SIMPLIFIER_PLUGIN_H_ +#define SEQ_SIMPLIFIER_PLUGIN_H_ + +#include"basic_simplifier_plugin.h" +#include"seq_decl_plugin.h" +#include"seq_rewriter.h" + +class seq_simplifier_plugin : public simplifier_plugin { + seq_util m_util; + seq_rewriter m_rw; + +public: + seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b); + ~seq_simplifier_plugin(); + + + virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + + virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result); + +}; + +#endif /* SEQ_SIMPLIFIER_PLUGIN_H_ */ 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/opt/opt_context.cpp b/src/opt/opt_context.cpp index 97b8c999d..3c305723b 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -883,11 +883,11 @@ namespace opt { bool neg; if (is_maxsat(fml, terms, weights, offset, neg, id, index)) { objective& obj = m_objectives[index]; + if (obj.m_type != O_MAXSMT) { // change from maximize/minimize. obj.m_id = id; obj.m_type = O_MAXSMT; - obj.m_weights.append(weights); SASSERT(!m_maxsmts.contains(id)); add_maxsmt(id); } @@ -895,10 +895,13 @@ namespace opt { SASSERT(obj.m_id == id); obj.m_terms.reset(); obj.m_terms.append(terms); + obj.m_weights.reset(); + obj.m_weights.append(weights); obj.m_adjust_value.set_offset(offset); obj.m_adjust_value.set_negate(neg); m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value); - TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";); + TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n"; + tout << terms << "\n";); } else if (is_maximize(fml, tr, orig_term, index)) { purify(tr); diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6543bddad..df4b528fd 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -23,6 +23,7 @@ Revision History: #include"array_simplifier_plugin.h" #include"datatype_simplifier_plugin.h" #include"fpa_simplifier_plugin.h" +#include"seq_simplifier_plugin.h" #include"bv_simplifier_plugin.h" #include"for_each_expr.h" #include"well_sorted.h" @@ -98,6 +99,7 @@ void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifie s.register_plugin(bvsimp); s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp)); s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp)); + s.register_plugin(alloc(seq_simplifier_plugin, m_manager, *bsimp)); } void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) { diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index e4f698914..94566c52b 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -471,12 +471,12 @@ namespace smt { if (get_enode(v)->get_root() != get_enode(v2)->get_root()) { SASSERT(get_bv_size(v) == get_bv_size(v2)); context & ctx = get_context(); - justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2)); TRACE("fixed_var_eh", tout << "detected equality: v" << v << " = v" << v2 << "\n"; display_var(tout, v); display_var(tout, v2);); m_stats.m_num_th2core_eq++; add_fixed_eq(v, v2); + justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2)); ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js)); m_fixed_var_table.insert(key, v2); } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index a06ee723c..16f883548 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -30,12 +30,13 @@ namespace smt { expr * m_e; public: fpa2bv_conversion_trail_elem(ast_manager & m, obj_map & c, expr * e) : - m(m), m_conversions(c), m_e(e) {} + m(m), m_conversions(c), m_e(e) { m.inc_ref(e); } virtual ~fpa2bv_conversion_trail_elem() {} virtual void undo(theory_fpa & th) { expr * v = m_conversions.find(m_e); m_conversions.remove(m_e); m.dec_ref(v); + m.dec_ref(m_e); } }; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 0a9c48f18..df96f9c20 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -823,6 +823,23 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& } bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) { + + rational val1, val2; + if (has_length(l) && has_length(r) && + get_length(l, val1) && get_length(r, val2) && val1 == val2) { + context& ctx = get_context(); + expr_ref len1(m_util.str.mk_length(l), m); + expr_ref len2(m_util.str.mk_length(r), m); + literal lit = mk_eq(len1, len2, false); + if (ctx.get_assignment(lit) == l_true) { + lits.push_back(lit); + return true; + } + else { + TRACE("seq", tout << "Assignment: " << len1 << " = " << len2 << " " << ctx.get_assignment(lit) << "\n";); + return false; + } + } expr_ref len1(m), len2(m); lits.reset(); if (get_length(l, len1, lits) && @@ -2431,6 +2448,7 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) { literal l_le_s = mk_literal(m_autil.mk_le(mk_sub(l, ls), zero)); add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey)); add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false)); + add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, m_util.str.mk_length(y), false)); } /* diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index e436d19c4..f23d874a6 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -106,9 +106,14 @@ class solve_eqs_tactic : public tactic { } } bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) { - return - trivial_solve1(lhs, rhs, var, def, pr) || - trivial_solve1(rhs, lhs, var, def, pr); + if (trivial_solve1(lhs, rhs, var, def, pr)) return true; + if (trivial_solve1(rhs, lhs, var, def, pr)) { + if (m_produce_proofs) { + pr = m().mk_commutativity(m().mk_eq(lhs, rhs)); + } + return true; + } + return false; } // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2)) 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':