From d5316e017e9c0c9f44e4aa2453f908fde7ff4324 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Dec 2022 20:38:28 -0800 Subject: [PATCH 1/4] add tactic descriptions --- src/muz/spacer/spacer_sym_mux.cpp | 4 +- src/tactic/arith/pb2bv_tactic.h | 27 ++++++++++- src/tactic/arith/propagate_ineqs_tactic.h | 55 +++++++++++++++-------- src/tactic/arith/purify_arith_tactic.h | 23 +++++++++- 4 files changed, 88 insertions(+), 21 deletions(-) diff --git a/src/muz/spacer/spacer_sym_mux.cpp b/src/muz/spacer/spacer_sym_mux.cpp index cfe0908d698..451a2b3dcf8 100644 --- a/src/muz/spacer/spacer_sym_mux.cpp +++ b/src/muz/spacer/spacer_sym_mux.cpp @@ -144,10 +144,12 @@ struct conv_rewriter_cfg : public default_rewriter_cfg { bool get_subst(expr * s, expr * & t, proof * & t_pr) { - if (!is_app(s)) { return false; } + if (!is_app(s)) + return false; app * a = to_app(s); func_decl * sym = a->get_decl(); if (!m_parent.has_index(sym, m_from_idx)) { + CTRACE("spacer", m_homogenous && m_parent.is_muxed(sym), tout << "not found " << mk_pp(a, m) << "\n"); SASSERT(!m_homogenous || !m_parent.is_muxed(sym)); return false; } diff --git a/src/tactic/arith/pb2bv_tactic.h b/src/tactic/arith/pb2bv_tactic.h index e23c54d8350..b1c94a6ba98 100644 --- a/src/tactic/arith/pb2bv_tactic.h +++ b/src/tactic/arith/pb2bv_tactic.h @@ -13,7 +13,32 @@ Module Name: Christoph (cwinter) 2012-02-15 -Notes: +Tactic Documentation: + +## Tactic pb2bv + +### Short Description + +Convert pseudo-boolean constraints to bit-vectors + +### Example + +```z3 +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) +(declare-const u Int) +(assert (<= 0 x)) +(assert (<= 0 y)) +(assert (<= 0 z)) +(assert (<= 0 u)) +(assert (<= x 1)) +(assert (<= y 1)) +(assert (<= z 1)) +(assert (<= u 1)) +(assert (>= (+ (* 3 x) (* 2 y) (* 2 z) (* 2 u)) 4)) +(apply pb2bv) +``` --*/ #pragma once diff --git a/src/tactic/arith/propagate_ineqs_tactic.h b/src/tactic/arith/propagate_ineqs_tactic.h index 47806a34192..6341bf28165 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.h +++ b/src/tactic/arith/propagate_ineqs_tactic.h @@ -4,30 +4,49 @@ Copyright (c) 2012 Microsoft Corporation Module Name: propagate_ineqs_tactic.h + +Author: -Abstract: + Leonardo (leonardo) 2012-02-19 - This tactic performs the following tasks: +Tactic Documentation: - - Propagate bounds using the bound_propagator. - - Eliminate subsumed inequalities. - For example: - x - y >= 3 - can be replaced with true if we know that - x >= 3 and y <= 0 - - - Convert inequalities of the form p <= k and p >= k into p = k, - where p is a polynomial and k is a constant. +## Tactic propagate-ineqs - This strategy assumes the input is in arith LHS mode. - This can be achieved by using option :arith-lhs true in the - simplifier. - -Author: +### Short Description - Leonardo (leonardo) 2012-02-19 +Propagate ineqs/bounds, remove subsumed inequalities + +### Long Description + +This tactic performs the following tasks: + +- Propagate bounds using the bound_propagator. +- Eliminate subsumed inequalities. + - For example: + `x - y >= 3` can be replaced with true if we know that `x >= 3` and `y <= 0` + + - Convert inequalities of the form `p <= k` and `p >= k` into `p = k`, + where `p` is a polynomial and `k` is a constant. + +This strategy assumes the input is in arith LHS mode. +This can be achieved by using option :arith-lhs true in the simplifier. -Notes: +### Example +```z3 +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) +(declare-const u Int) +(declare-const v Int) +(declare-const w Int) +(assert (>= x 3)) +(assert (<= y 0)) +(assert (>= (- x y) 3)) +(assert (>= (* u v w) 2)) +(assert (<= (* v u w) 2)) +(apply (and-then simplify propagate-ineqs)) +``` --*/ #pragma once diff --git a/src/tactic/arith/purify_arith_tactic.h b/src/tactic/arith/purify_arith_tactic.h index ef5f08b6180..4f3aa847a51 100644 --- a/src/tactic/arith/purify_arith_tactic.h +++ b/src/tactic/arith/purify_arith_tactic.h @@ -42,7 +42,28 @@ Module Name: Leonardo de Moura (leonardo) 2011-12-30. -Revision History: +Tactic Documentation: + +## Tactic purify-arith + +### Short Description + +Eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects. +These operators can be replaced by introcing fresh variables and using multiplication and addition. + +### Example +```z3 +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) +(declare-const u Int) +(declare-const v Int) +(declare-const w Int) +(assert (= (div x 3) y)) +(assert (= (mod z 4) u)) +(assert (> (mod v w) u)) +(apply purify-arith) +``` --*/ #pragma once From 13920c4772683d179932507230755a7a19dc8b24 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Dec 2022 11:42:02 -0800 Subject: [PATCH 2/4] more doc Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/nla2bv_tactic.cpp | 6 ++-- src/tactic/arith/normalize_bounds_tactic.cpp | 2 +- src/tactic/arith/purify_arith_tactic.cpp | 6 ++-- src/tactic/arith/recover_01_tactic.cpp | 2 +- src/tactic/bv/bit_blaster_tactic.cpp | 8 +++--- src/tactic/bv/bit_blaster_tactic.h | 30 ++++++++++++++------ 6 files changed, 33 insertions(+), 21 deletions(-) diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index bdcf5795380..cd37db40292 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -442,9 +442,9 @@ class nla2bv_tactic : public tactic { void collect_param_descrs(param_descrs & r) override { r.insert("nla2bv_max_bv_size", CPK_UINT, "(default: inf) maximum bit-vector size used by nla2bv tactic"); - r.insert("nla2bv_bv_size", CPK_UINT, "(default: 4) default bit-vector size used by nla2bv tactic."); - r.insert("nla2bv_root", CPK_UINT, "(default: 2) nla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding."); - r.insert("nla2bv_divisor", CPK_UINT, "(default: 2) nla2bv tactic parameter."); + r.insert("nla2bv_bv_size", CPK_UINT, "default bit-vector size used by nla2bv tactic.", "4"); + r.insert("nla2bv_root", CPK_UINT, "nla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding.", "2"); + r.insert("nla2bv_divisor", CPK_UINT, "nla2bv tactic parameter.", "2"); } /** diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index cba791ee16b..b20eaf53a3d 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -161,7 +161,7 @@ class normalize_bounds_tactic : public tactic { void collect_param_descrs(param_descrs & r) override { insert_produce_models(r); - r.insert("norm_int_only", CPK_BOOL, "(default: true) normalize only the bounds of integer constants."); + r.insert("norm_int_only", CPK_BOOL, "normalize only the bounds of integer constants.", "true"); } void operator()(goal_ref const & in, diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 7c69ef12e82..db19863987a 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -911,11 +911,11 @@ class purify_arith_tactic : public tactic { void collect_param_descrs(param_descrs & r) override { r.insert("complete", CPK_BOOL, - "(default: true) add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root"); + "add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root", "true"); r.insert("elim_root_objects", CPK_BOOL, - "(default: true) eliminate root objects."); + "eliminate root objects.", "true"); r.insert("elim_inverses", CPK_BOOL, - "(default: true) eliminate inverse trigonometric functions (asin, acos, atan)."); + "eliminate inverse trigonometric functions (asin, acos, atan).", "true"); th_rewriter::get_param_descrs(r); } diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index d97f9b80fc6..623f82cf9d6 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -407,7 +407,7 @@ class recover_01_tactic : public tactic { void collect_param_descrs(param_descrs & r) override { th_rewriter::get_param_descrs(r); - r.insert("recover_01_max_bits", CPK_UINT, "(default: 10) maximum number of bits to consider in a clause."); + r.insert("recover_01_max_bits", CPK_UINT, "maximum number of bits to consider in a clause.", "10"); } void operator()(goal_ref const & g, diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 978a0a9a6f6..5e35d7d9ad0 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -129,10 +129,10 @@ class bit_blaster_tactic : public tactic { void collect_param_descrs(param_descrs & r) override { insert_max_memory(r); insert_max_steps(r); - r.insert("blast_mul", CPK_BOOL, "(default: true) bit-blast multipliers (and dividers, remainders)."); - r.insert("blast_add", CPK_BOOL, "(default: true) bit-blast adders."); - r.insert("blast_quant", CPK_BOOL, "(default: false) bit-blast quantified variables."); - r.insert("blast_full", CPK_BOOL, "(default: false) bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms."); + r.insert("blast_mul", CPK_BOOL, "bit-blast multipliers (and dividers, remainders).", "true"); + r.insert("blast_add", CPK_BOOL, "bit-blast adders.", "true"); + r.insert("blast_quant", CPK_BOOL, "bit-blast quantified variables.", "false"); + r.insert("blast_full", CPK_BOOL, "bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms.", "false"); } void operator()(goal_ref const & g, diff --git a/src/tactic/bv/bit_blaster_tactic.h b/src/tactic/bv/bit_blaster_tactic.h index e90a675aa24..07d85d9c6a0 100644 --- a/src/tactic/bv/bit_blaster_tactic.h +++ b/src/tactic/bv/bit_blaster_tactic.h @@ -1,21 +1,33 @@ /*++ Copyright (c) 2011 Microsoft Corporation - Module Name: +Module Name: bit_blaster_tactic.h - Abstract: +Author: - Apply bit-blasting to a given goal. - - Author: - - Leonardo (leonardo) 2011-10-25 - - Notes: + Leonardo (leonardo) 2011-10-25 +Tactic Documentation: + +## Tactic bit-blast + +### Short Description + +Apply bit-blasting to a given goal. + +### Example + +```z3 +(declare-const x (_ BitVec 8)) +(declare-const y (_ BitVec 8)) +(assert (bvule x y)) +(apply bit-blast) +``` + --*/ + #pragma once #include "util/params.h" From 0768a2ead15d162e0e39c5791441cd16ccd73dd0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Dec 2022 19:23:32 -0800 Subject: [PATCH 3/4] updated doc --- src/tactic/bv/bv1_blaster_tactic.h | 36 +++++++++++++++------ src/tactic/bv/bv_bound_chk_tactic.cpp | 1 - src/tactic/bv/bv_bound_chk_tactic.h | 14 ++++---- src/tactic/bv/bv_size_reduction_tactic.h | 41 ++++++++++++++++++++---- 4 files changed, 68 insertions(+), 24 deletions(-) diff --git a/src/tactic/bv/bv1_blaster_tactic.h b/src/tactic/bv/bv1_blaster_tactic.h index c150778fd8a..9cc7f90d530 100644 --- a/src/tactic/bv/bv1_blaster_tactic.h +++ b/src/tactic/bv/bv1_blaster_tactic.h @@ -5,21 +5,37 @@ Module Name: bv1_blaster_tactic.h -Abstract: +Author: - Rewriter for "blasting" bit-vectors of size n into bit-vectors of size 1. - This rewriter only supports concat and extract operators. - This transformation is useful for handling benchmarks that contain - many BV equalities. + Leonardo (leonardo) 2011-10-25 - Remark: other operators can be mapped into concat/extract by using - the simplifiers. +Tactic Documentation: -Author: +## Tactic bv1-blast - Leonardo (leonardo) 2011-10-25 +### Short Description + +Reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported). + +### Long Description + +Rewriter for "blasting" bit-vectors of size n into bit-vectors of size 1. +This rewriter only supports concat and extract operators. +This transformation is useful for handling benchmarks that contain +many BV equalities. + +_Remark_: other operators can be mapped into concat/extract by using +the simplifiers. + +### Example -Notes: +```z3 +(declare-const x (_ BitVec 8)) +(declare-const y (_ BitVec 4)) +(declare-const z (_ BitVec 4)) +(assert (= (concat y z) x)) + (apply bv1-blast) +``` --*/ #pragma once diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index 3a2f8583125..f6db3c30e46 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -48,7 +48,6 @@ struct bv_bound_chk_rewriter_cfg : public default_rewriter_cfg { m_bv_ineq_consistency_test_max = p.bv_ineq_consistency_test_max(); m_max_memory = p.max_memory(); m_max_steps = p.max_steps(); - } ast_manager & m() const { return m_m; } diff --git a/src/tactic/bv/bv_bound_chk_tactic.h b/src/tactic/bv/bv_bound_chk_tactic.h index 60411e69353..bafd2ec5131 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.h +++ b/src/tactic/bv/bv_bound_chk_tactic.h @@ -1,18 +1,18 @@ /*++ - Copyright (c) 2016 Microsoft Corporation +Copyright (c) 2016 Microsoft Corporation - Module Name: +Module Name: - bv_bound_chk_tactic.h + bv_bound_chk_tactic.h - Abstract: +Author: + Mikolas Janota - Author: +### Notes - Mikolas Janota +* does not support proofs, does not support cores - Revision History: --*/ #pragma once diff --git a/src/tactic/bv/bv_size_reduction_tactic.h b/src/tactic/bv/bv_size_reduction_tactic.h index 1bb512f3fc2..a55c66e73a0 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.h +++ b/src/tactic/bv/bv_size_reduction_tactic.h @@ -7,12 +7,6 @@ Module Name: Abstract: - Reduce the number of bits used to encode constants, by using signed bounds. - Example: suppose x is a bit-vector of size 8, and we have - signed bounds for x such that: - -2 <= x <= 2 - Then, x can be replaced by ((sign-extend 5) k) - where k is a fresh bit-vector constant of size 3. Author: @@ -20,6 +14,41 @@ Module Name: Notes: +Tactic Documentation: + +## Tactic reduce-bv-size + +### Short Description + +Rry to reduce bit-vector sizes using inequalities. + +### Long Description + +Reduce the number of bits used to encode constants, by using signed bounds. +Example: suppose $x$ is a bit-vector of size 8, and we have +signed bounds for $x$ such that: + +``` + -2 <= x <= 2 +``` + +Then, $x$ can be replaced by `((sign-extend 5) k)` +where `k` is a fresh bit-vector constant of size 3. + +### Example + +```z3 +(declare-const x (_ BitVec 32)) +(assert (bvsle (bvneg (_ bv2 32)) x)) +(assert (bvsle x (_ bv2 32))) +(assert (= (bvmul x x) (_ bv9 32))) +(apply (and-then simplify reduce-bv-size)) +``` + +### Notes + +* does not support proofs, nor unsat cores + --*/ #pragma once From e423fabf6a8808c36d906cdd62dda9c90773992d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Dec 2022 20:35:36 -0800 Subject: [PATCH 4/4] tactic Signed-off-by: Nikolaj Bjorner --- doc/mk_tactic_doc.py | 10 +- src/tactic/bv/bv_bounds_tactic.cpp | 165 +++++++++++--------------- src/tactic/bv/bv_bounds_tactic.h | 27 ++++- src/tactic/bv/bvarray2uf_tactic.h | 26 ++-- src/tactic/bv/dt2bv_tactic.h | 23 +++- src/tactic/bv/elim_small_bv_tactic.h | 16 +++ src/tactic/bv/max_bv_sharing_tactic.h | 20 +++- 7 files changed, 170 insertions(+), 117 deletions(-) diff --git a/doc/mk_tactic_doc.py b/doc/mk_tactic_doc.py index e4c71341a88..6f4837cddb6 100644 --- a/doc/mk_tactic_doc.py +++ b/doc/mk_tactic_doc.py @@ -53,13 +53,21 @@ def extract_tactic_doc(ous, f): if is_doc.search(line): generate_tactic_doc(ous, f, ins) +def find_tactic_name(path): + with open(path) as ins: + for line in ins: + m = is_tac_name.search(line) + if m: + return m.group(1) + return "" + def presort_files(): tac_files = [] for root, dirs, files in os.walk(doc_path("../src")): for f in files: if f.endswith("tactic.h"): tac_files += [(f, os.path.join(root, f))] - tac_files = sorted(tac_files, key = lambda x: x[0]) + tac_files = sorted(tac_files, key = lambda x: find_tactic_name(x[1])) return tac_files def help(ous): diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 72f0266c1cd..58183287d5c 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -35,11 +35,12 @@ namespace { struct interval { // l < h: [l, h] // l > h: [0, h] U [l, UMAX_INT] - uint64_t l, h; - unsigned sz; - bool tight; + uint64_t l = 0, h = 0; + unsigned sz = 0; + bool tight = true; interval() {} + interval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { // canonicalize full set if (is_wrapped() && l == h + 1) { @@ -50,8 +51,7 @@ namespace { } bool invariant() const { - return l <= uMaxInt(sz) && h <= uMaxInt(sz) && - (!is_wrapped() || l != h+1); + return l <= uMaxInt(sz) && h <= uMaxInt(sz) && (!is_wrapped() || l != h+1); } bool is_full() const { return l == 0 && h == uMaxInt(sz); } @@ -67,22 +67,17 @@ namespace { bool implies(const interval& b) const { if (b.is_full()) return true; - if (is_full()) + else if (is_full()) return false; - - if (is_wrapped()) { + else if (is_wrapped()) // l >= b.l >= b.h >= h - return b.is_wrapped() && h <= b.h && l >= b.l; - } - else if (b.is_wrapped()) { + return b.is_wrapped() && h <= b.h && l >= b.l; + else if (b.is_wrapped()) // b.l > b.h >= h >= l // h >= l >= b.l > b.h - return h <= b.h || l >= b.l; - } - else { - // - return l >= b.l && h <= b.h; - } + return h <= b.h || l >= b.l; + else + return l >= b.l && h <= b.h; } /// return false if intersection is unsat @@ -98,28 +93,26 @@ namespace { if (is_wrapped()) { if (b.is_wrapped()) { - if (h >= b.l) { + if (h >= b.l) result = b; - } else if (b.h >= l) { + else if (b.h >= l) result = *this; - } else { + else result = interval(std::max(l, b.l), std::min(h, b.h), sz); - } - } else { - return b.intersect(*this, result); } + else + return b.intersect(*this, result); } else if (b.is_wrapped()) { // ... b.h ... l ... h ... b.l .. - if (h < b.l && l > b.h) { - return false; - } + if (h < b.l && l > b.h) + return false; // ... l ... b.l ... h ... - if (h >= b.l && l <= b.h) { + if (h >= b.l && l <= b.h) result = b; - } else if (h >= b.l) { + else if (h >= b.l) result = interval(b.l, h, sz); - } else { + else { // ... l .. b.h .. h .. b.l ... SASSERT(l <= b.h); result = interval(l, std::min(h, b.h), sz); @@ -136,20 +129,16 @@ namespace { /// return false if negation is empty bool negate(interval& result) const { - if (!tight) { + if (!tight) result = interval(0, uMaxInt(sz), true); - return true; - } - - if (is_full()) + else if (is_full()) return false; - if (l == 0) { + else if (l == 0) result = interval(h + 1, uMaxInt(sz), sz); - } else if (uMaxInt(sz) == h) { + else if (uMaxInt(sz) == h) result = interval(0, l - 1, sz); - } else { - result = interval(h + 1, l - 1, sz); - } + else + result = interval(h + 1, l - 1, sz); return true; } }; @@ -163,9 +152,9 @@ namespace { struct undo_bound { - expr* e { nullptr }; + expr* e = nullptr; interval b; - bool fresh { false }; + bool fresh = false; undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} }; @@ -176,7 +165,7 @@ namespace { ast_manager& m; params_ref m_params; - bool m_propagate_eq; + bool m_propagate_eq = false; bv_util m_bv; vector m_scopes; map m_bound; @@ -224,7 +213,8 @@ namespace { v = lhs; return true; } - } else if (m.is_eq(e, lhs, rhs)) { + } + else if (m.is_eq(e, lhs, rhs)) { if (is_number(lhs, n, sz)) { if (m_bv.is_numeral(rhs)) return false; @@ -252,7 +242,7 @@ namespace { } static void get_param_descrs(param_descrs& r) { - r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); + r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false"); } ~bv_bounds_simplifier() override { @@ -546,22 +536,19 @@ namespace { } static void get_param_descrs(param_descrs& r) { - r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); + r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false"); } ~dom_bv_bounds_simplifier() override { - for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { - dealloc(m_expr_vars[i]); - } - for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { - dealloc(m_bound_exprs[i]); - } + for (auto* e : m_expr_vars) + dealloc(e); + for (auto* b : m_bound_exprs) + dealloc(b); } bool assert_expr(expr * t, bool sign) override { - while (m.is_not(t, t)) { - sign = !sign; - } + while (m.is_not(t, t)) + sign = !sign; interval b; expr* t1; @@ -581,7 +568,8 @@ namespace { return true; m_scopes.push_back(undo_bound(t1, old, false)); old = intr; - } else { + } + else { m_bound.insert(t1, b); m_scopes.push_back(undo_bound(t1, interval(), true)); } @@ -602,9 +590,8 @@ namespace { return; bool sign = false; - while (m.is_not(t, t)) { - sign = !sign; - } + while (m.is_not(t, t)) + sign = !sign; if (!is_bound(t, t1, b)) return; @@ -619,27 +606,21 @@ namespace { interval ctx, intr; bool was_updated = true; - if (b.is_full() && b.tight) { - r = m.mk_true(); - } + if (b.is_full() && b.tight) + r = m.mk_true(); else if (m_bound.find(t1, ctx)) { - if (ctx.implies(b)) { - r = m.mk_true(); - } - else if (!b.intersect(ctx, intr)) { - r = m.mk_false(); - } - else if (m_propagate_eq && intr.is_singleton()) { + if (ctx.implies(b)) + r = m.mk_true(); + else if (!b.intersect(ctx, intr)) + r = m.mk_false(); + else if (m_propagate_eq && intr.is_singleton()) r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), - t1->get_sort())); - } - else { - was_updated = false; - } - } - else { - was_updated = false; + t1->get_sort())); + else + was_updated = false; } + else + was_updated = false; TRACE("bv", tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";); if (sign && was_updated) @@ -654,18 +635,16 @@ namespace { while (!todo.empty()) { t = todo.back(); todo.pop_back(); - if (mark.is_marked(t)) { - continue; - } + if (mark.is_marked(t)) + continue; if (t == v) { todo.reset(); return true; } mark.mark(t); - if (!is_app(t)) { - continue; - } + if (!is_app(t)) + continue; app* a = to_app(t); todo.append(a->get_num_args(), a->get_args()); } @@ -680,14 +659,11 @@ namespace { while (!todo.empty()) { t = todo.back(); todo.pop_back(); - if (mark1.is_marked(t)) { - continue; - } - mark1.mark(t); - - if (!is_app(t)) { - continue; - } + if (mark1.is_marked(t)) + continue; + mark1.mark(t); + if (!is_app(t)) + continue; interval b; expr* e; if (is_bound(t, e, b)) { @@ -718,14 +694,13 @@ namespace { m_scopes.reset(); return; } - for (unsigned i = m_scopes.size()-1; i >= target; --i) { + for (unsigned i = m_scopes.size(); i-- > target; ) { undo_bound& undo = m_scopes[i]; SASSERT(m_bound.contains(undo.e)); - if (undo.fresh) { + if (undo.fresh) m_bound.erase(undo.e); - } else { - m_bound.insert(undo.e, undo.b); - } + else + m_bound.insert(undo.e, undo.b); } m_scopes.shrink(target); } diff --git a/src/tactic/bv/bv_bounds_tactic.h b/src/tactic/bv/bv_bounds_tactic.h index 58de42199bf..325cca89e2b 100644 --- a/src/tactic/bv/bv_bounds_tactic.h +++ b/src/tactic/bv/bv_bounds_tactic.h @@ -5,15 +5,34 @@ Module Name: bv_bounds_tactic.h -Abstract: - - Contextual bounds simplification tactic. - Author: Nuno Lopes (nlopes) 2016-2-12 Nikolaj Bjorner (nbjorner) +Tactic Documentation: + +## Tactic propagate-bv-bounds + +### Short Description + +Contextual bounds simplification tactic. + +### Example + +```z3 +(declare-const x (_ BitVec 32)) +(declare-const y (_ BitVec 32)) +(declare-const z (_ BitVec 32)) +(assert (bvule (_ bv4 32) x)) +(assert (bvule x (_ bv24 32))) +(assert (or (bvule x (_ bv100 32)) (bvule (_ bv32 32) x))) +(apply propagate-bv-bounds) +``` + +### Notes + +* assumes that bit-vector inequalities have been simplified to use bvule/bvsle --*/ #pragma once diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h index a22a78f86aa..393ab164c5d 100644 --- a/src/tactic/bv/bvarray2uf_tactic.h +++ b/src/tactic/bv/bvarray2uf_tactic.h @@ -3,18 +3,30 @@ Copyright (c) 2015 Microsoft Corporation Module Name: - bvarray2ufbvarray2uf_tactic.h - -Abstract: - - Tactic that rewrites bit-vector arrays into bit-vector - (uninterpreted) functions. + bvarray2uf_tactic.h Author: Christoph (cwinter) 2015-11-04 -Notes: +Tactic Documentation: + +## Tactic bvarray2uf + +### Short Description + +Tactic that rewrites bit-vector arrays into bit-vector +(uninterpreted) functions. + +### Example + +```z3 +(declare-const a (Array (_ BitVec 32) (_ BitVec 32))) +(declare-const b (_ BitVec 32)) +(declare-const c (_ BitVec 32)) +(assert (= (select a b) c)) +(apply bvarray2uf) +``` --*/ #pragma once diff --git a/src/tactic/bv/dt2bv_tactic.h b/src/tactic/bv/dt2bv_tactic.h index 906386ed4ed..05713dfd6b0 100644 --- a/src/tactic/bv/dt2bv_tactic.h +++ b/src/tactic/bv/dt2bv_tactic.h @@ -5,15 +5,28 @@ Module Name: dt2bv_tactic.h -Abstract: - - Tactic that eliminates finite domain data-types. - Author: nbjorner 2016-07-22 -Revision History: +Tactic Documentation + +## Tactic dt2bv + +### Short Description + +Tactic that eliminates finite domain data-types. + +### Example + +```z3 +(declare-datatypes ((Color 0)) (((Red) (Blue) (Green) (DarkBlue) (MetallicBlack) (MetallicSilver) (Silver) (Black)))) +(declare-const x Color) +(declare-const y Color) +(assert (not (= x y))) +(assert (not (= x Red))) +(apply dt2bv) +``` --*/ #pragma once diff --git a/src/tactic/bv/elim_small_bv_tactic.h b/src/tactic/bv/elim_small_bv_tactic.h index e4a91f70fe4..46e6dca3938 100644 --- a/src/tactic/bv/elim_small_bv_tactic.h +++ b/src/tactic/bv/elim_small_bv_tactic.h @@ -15,6 +15,22 @@ Module Name: Revision History: +Tactic Documentation + +## Tactic elim-small-bv + +### Short Description + +Eliminate small, quantified bit-vectors by expansion + +### Example + +```z3 +(declare-fun p ((_ BitVec 2)) Bool) +(assert (forall ((x (_ BitVec 2))) (p x))) +(apply elim-small-bv) +``` + --*/ #pragma once diff --git a/src/tactic/bv/max_bv_sharing_tactic.h b/src/tactic/bv/max_bv_sharing_tactic.h index bf14e9f14e7..2f21ee4b9e8 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.h +++ b/src/tactic/bv/max_bv_sharing_tactic.h @@ -7,16 +7,26 @@ Module Name: Abstract: - Rewriter for "maximing" the number of shared terms. - The idea is to rewrite AC terms to maximize sharing. - This rewriter is particularly useful for reducing - the number of Adders and Multipliers before "bit-blasting". + Author: Leonardo de Moura (leonardo) 2011-12-29. -Revision History: +Tactic Documentation + +## Tactic max-bv-sharing + +### Short Description + +Use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers + +### Long Description + +Rewriter for "maximing" the number of shared terms. +The idea is to rewrite AC terms to maximize sharing. +This rewriter is particularly useful for reducing +the number of Adders and Multipliers before "bit-blasting". --*/ #pragma once