From bc19992543c4793ae90f286d4834c782e9b23548 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Dec 2022 12:02:08 -0800 Subject: [PATCH] add doc for ackermannize Signed-off-by: Nikolaj Bjorner --- src/ackermannization/ackermannize_bv_tactic.h | 32 ++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/src/ackermannization/ackermannize_bv_tactic.h b/src/ackermannization/ackermannize_bv_tactic.h index 073a680bf..b99ae00e4 100644 --- a/src/ackermannization/ackermannize_bv_tactic.h +++ b/src/ackermannization/ackermannize_bv_tactic.h @@ -11,7 +11,37 @@ Author: Mikolas Janota -Revision History: +Tactic Documentation: + +## Tactic ackernannize_bv + +### Short Description + +A tactic for performing Ackermann reduction for bit-vector formulas + +### Long Description + +The Ackermann reduction replaces uninterpreted functions $f(t_1), f(t_2)$ +by fresh variables $f_1, f_2$ and addes axioms $t_1 \simeq t_2 \implies f_1 \simeq f_2$. +The reduction has the effect of eliminating uninterpreted functions. When the reduction +produces a pure bit-vector benchmark, it allows Z3 to use a specialized SAT solver. + +### Example + +```z3 +(declare-const x (_ BitVec 32)) +(declare-const y (_ BitVec 32)) +(declare-fun f ((_ BitVec 32)) (_ BitVec 8)) + +(assert (not (= (f x) (f y)))) +(apply ackermannize_bv) +``` + +### Notes + +* does not support proofs, does not support unsatisfiable cores + + --*/ #pragma once