mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
bit_blaster unit tests for adder and multiplier (#5514)
These tests cover a mix of constant and non-constant input bits.
This commit is contained in:
Jamey Sharp
GitHub
parent
8f306c6a8f
commit
cd7a826083
|
|
@ -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);
|
||||
|
|
|
|||
Loading…
Reference in a new issue