From cd7a8260839e83e308753423e41fb757c7c66c41 Mon Sep 17 00:00:00 2001 From: Jamey Sharp Date: Fri, 27 Aug 2021 14:19:12 -0700 Subject: [PATCH] bit_blaster unit tests for adder and multiplier (#5514) These tests cover a mix of constant and non-constant input bits. --- src/test/bit_blaster.cpp | 176 +++++++++++++++++++++++++++++++++------ 1 file changed, 149 insertions(+), 27 deletions(-) diff --git a/src/test/bit_blaster.cpp b/src/test/bit_blaster.cpp index b4c7a8e76fd..8c4cd090337 100644 --- a/src/test/bit_blaster.cpp +++ b/src/test/bit_blaster.cpp @@ -17,9 +17,12 @@ Revision History: --*/ -#include "ast/rewriter/bit_blaster/bit_blaster.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" +#include "ast/reg_decl_plugins.h" +#include "ast/rewriter/bit_blaster/bit_blaster.h" +#include "model/model.h" +#include "model/model_evaluator.h" void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector & r) { sort_ref b(m); @@ -36,38 +39,153 @@ void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector } void display(std::ostream & out, expr_ref_vector & r, bool ll=true) { - ast_mark v; for (unsigned i = 0; i < r.size(); i++) { + out << "bit " << i << ":\n"; if (ll) - ast_ll_pp(out, r.get_manager(), r.get(i), v); + ast_ll_pp(out, r.get_manager(), r.get(i)); else - out << mk_pp(r.get(i), r.get_manager()); - out << "\n"; + out << mk_pp(r.get(i), r.get_manager()) << "\n"; } } -void tst_adder(ast_manager & m, unsigned sz) { -// expr_ref_vector a(m); -// expr_ref_vector b(m); -// expr_ref_vector c(m); -// mk_bits(m, "a", sz, a); -// mk_bits(m, "b", sz, b); -// bool t = true; -// bit_blaster blaster(m, t); -// blaster.mk_adder(sz, a.c_ptr(), b.c_ptr(), c); -// TRACE("bit_blaster", display(tout, c);); +static unsigned to_int(model_core & mdl, expr_ref_vector & out) { + SASSERT(out.size() <= sizeof(unsigned) * 8); + ast_manager & m = mdl.get_manager(); + model_evaluator eval(mdl); + expr_ref bit(m); + unsigned actual = 0; + for (unsigned i = 0; i < out.size(); i++) { + eval(out.get(i), bit); + if (m.is_true(bit)) + actual |= 1 << i; + else + ENSURE(m.is_false(bit)); + } + return actual; } -void tst_multiplier(ast_manager & m, unsigned sz) { -// expr_ref_vector a(m); -// expr_ref_vector b(m); -// expr_ref_vector c(m); -// mk_bits(m, "a", sz, a); -// mk_bits(m, "b", sz, b); -// bool t = true; -// bit_blaster blaster(m, t); -// blaster.mk_multiplier(sz, a.c_ptr(), b.c_ptr(), c); -// TRACE("bit_blaster", display(tout, c);); +#define ENSURE_INT(mdl, out, expected) \ + do { \ + unsigned actual = to_int(mdl, out); \ + TRACE("bit_blaster", \ + display(tout, out); \ + tout << "expected=" << (expected) << ", actual=" << actual << "\n"; \ + ); \ + ENSURE(actual == (expected)); \ + } while (0) + +void tst_adder(ast_manager & m, bit_blaster & blaster) { + model mdl(m); + expr_ref_vector c(m); + app_ref b1(m.mk_const("b1", m.mk_bool_sort()), m); + app_ref b2(m.mk_const("b2", m.mk_bool_sort()), m); + expr_ref not_b1(m.mk_not(b1), m); + + { + expr * const a[] = { b1, b1, b1 }; + expr * const b[] = { m.mk_false(), m.mk_true(), m.mk_true() }; + c.reset(); + blaster.mk_adder(3, a, b, c); + } + + mdl.register_decl(b1->get_decl(), m.mk_false()); + ENSURE_INT(mdl, c, 6); // b000 + b110 + + mdl.register_decl(b1->get_decl(), m.mk_true()); + ENSURE_INT(mdl, c, 5); // b111 + b110 + + { + expr * const a[] = { m.mk_false(), m.mk_true(), m.mk_true() }; + expr * const b[] = { b1, not_b1, m.mk_false() }; + c.reset(); + blaster.mk_adder(3, a, b, c); + } + + mdl.register_decl(b1->get_decl(), m.mk_false()); + ENSURE_INT(mdl, c, 0); // b110 + b010 + + mdl.register_decl(b1->get_decl(), m.mk_true()); + ENSURE_INT(mdl, c, 7); // b110 + b001 + + { + expr * const a[] = { b1, b2, m.mk_true() }; + expr * const b[] = { b1, not_b1, m.mk_false() }; + c.reset(); + blaster.mk_adder(3, a, b, c); + } + + mdl.register_decl(b1->get_decl(), m.mk_false()); + mdl.register_decl(b2->get_decl(), m.mk_false()); + ENSURE_INT(mdl, c, 6); // b100 + b010 + + mdl.register_decl(b1->get_decl(), m.mk_false()); + mdl.register_decl(b2->get_decl(), m.mk_true()); + ENSURE_INT(mdl, c, 0); // b110 + b010 + + mdl.register_decl(b1->get_decl(), m.mk_true()); + mdl.register_decl(b2->get_decl(), m.mk_false()); + ENSURE_INT(mdl, c, 6); // b101 + b001 + + mdl.register_decl(b1->get_decl(), m.mk_true()); + mdl.register_decl(b2->get_decl(), m.mk_true()); + ENSURE_INT(mdl, c, 0); // b111 + b001 +} + +void tst_multiplier(ast_manager & m, bit_blaster & blaster) { + model mdl(m); + expr_ref_vector c(m); + app_ref b1(m.mk_const("b1", m.mk_bool_sort()), m); + app_ref b2(m.mk_const("b2", m.mk_bool_sort()), m); + expr_ref not_b1(m.mk_not(b1), m); + + { + expr * const a[] = { b1, b1, b1 }; + expr * const b[] = { m.mk_false(), m.mk_true(), m.mk_true() }; + c.reset(); + blaster.mk_multiplier(3, a, b, c); + } + + mdl.register_decl(b1->get_decl(), m.mk_false()); + ENSURE_INT(mdl, c, 0); // b000 * b110 + + mdl.register_decl(b1->get_decl(), m.mk_true()); + ENSURE_INT(mdl, c, 2); // b111 * b110 + + { + expr * const a[] = { m.mk_false(), m.mk_true(), m.mk_true() }; + expr * const b[] = { b1, not_b1, m.mk_false() }; + c.reset(); + blaster.mk_multiplier(3, a, b, c); + } + + mdl.register_decl(b1->get_decl(), m.mk_false()); + ENSURE_INT(mdl, c, 4); // b110 * b010 + + mdl.register_decl(b1->get_decl(), m.mk_true()); + ENSURE_INT(mdl, c, 6); // b110 * b001 + + { + expr * const a[] = { b1, b2, m.mk_true() }; + expr * const b[] = { b1, not_b1, m.mk_false() }; + c.reset(); + blaster.mk_multiplier(3, a, b, c); + } + + mdl.register_decl(b1->get_decl(), m.mk_false()); + mdl.register_decl(b2->get_decl(), m.mk_false()); + ENSURE_INT(mdl, c, 0); // b100 * b010 + + mdl.register_decl(b1->get_decl(), m.mk_false()); + mdl.register_decl(b2->get_decl(), m.mk_true()); + ENSURE_INT(mdl, c, 4); // b110 * b010 + + mdl.register_decl(b1->get_decl(), m.mk_true()); + mdl.register_decl(b2->get_decl(), m.mk_false()); + ENSURE_INT(mdl, c, 5); // b101 * b001 + + mdl.register_decl(b1->get_decl(), m.mk_true()); + mdl.register_decl(b2->get_decl(), m.mk_true()); + ENSURE_INT(mdl, c, 7); // b111 * b001 } void tst_le(ast_manager & m, unsigned sz) { @@ -115,8 +233,12 @@ void tst_sh(ast_manager & m, unsigned sz) { void tst_bit_blaster() { ast_manager m; - tst_adder(m, 4); - tst_multiplier(m, 4); + reg_decl_plugins(m); + bit_blaster_params params; + bit_blaster blaster(m, params); + + tst_adder(m, blaster); + tst_multiplier(m, blaster); tst_le(m, 4); tst_eqs(m, 8); tst_sh(m, 4);