From 79ee543d25bab9bd58d76c5ac739d949dd01d789 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 11:59:18 +0200 Subject: [PATCH] Move tbv to util --- src/muz/ddnf/ddnf.cpp | 2 +- src/muz/rel/CMakeLists.txt | 1 - src/muz/rel/doc.cpp | 34 +++++++++++++++++++++++++++++----- src/muz/rel/doc.h | 6 ++++-- src/test/ddnf.cpp | 2 +- src/test/tbv.cpp | 2 +- src/util/CMakeLists.txt | 1 + src/{muz/rel => util}/tbv.cpp | 26 +------------------------- src/{muz/rel => util}/tbv.h | 5 +---- 9 files changed, 39 insertions(+), 40 deletions(-) rename src/{muz/rel => util}/tbv.cpp (91%) rename src/{muz/rel => util}/tbv.h (96%) diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index c0c3d839ccf..cf759c76e93 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -25,7 +25,7 @@ Revision History: #include "muz/base/dl_context.h" #include "ast/scoped_proof.h" #include "ast/bv_decl_plugin.h" -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include namespace datalog { diff --git a/src/muz/rel/CMakeLists.txt b/src/muz/rel/CMakeLists.txt index f03a9040676..1129b6dd9dc 100644 --- a/src/muz/rel/CMakeLists.txt +++ b/src/muz/rel/CMakeLists.txt @@ -23,7 +23,6 @@ z3_add_component(rel doc.cpp karr_relation.cpp rel_context.cpp - tbv.cpp udoc_relation.cpp COMPONENT_DEPENDENCIES muz diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index 0b7800905ad..fbe6b1f61e1 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -695,12 +695,36 @@ void doc_manager::check_equiv(ast_manager& m, expr* fml1, expr* fml2) { SASSERT(res == l_false); } + +expr_ref doc_manager::to_formula(ast_manager & m, tbv const& src) { + expr_ref result(m); + expr_ref_vector conj(m); + for (unsigned i = 0; i < num_tbits(); ++i) { + switch (src[i]) { + case BIT_0: + conj.push_back(m.mk_not(m.mk_const(symbol(i), m.mk_bool_sort()))); + break; + case BIT_1: + conj.push_back(m.mk_const(symbol(i), m.mk_bool_sort())); + break; + default: + break; + } + } + result = mk_and(m, conj.size(), conj.data()); + return result; +} + +expr_ref doc_manager::mk_var(ast_manager & m, unsigned i) { + return expr_ref(m.mk_const(symbol(i), m.mk_bool_sort()), m); +} + expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) { expr_ref result(m); expr_ref_vector conj(m); - conj.push_back(tbvm().to_formula(m, src.pos())); + conj.push_back(to_formula(m, src.pos())); for (unsigned i = 0; i < src.neg().size(); ++i) { - conj.push_back(m.mk_not(tbvm().to_formula(m, src.neg()[i]))); + conj.push_back(m.mk_not(to_formula(m, src.neg()[i]))); } result = mk_and(m, conj.size(), conj.data()); return result; @@ -712,9 +736,9 @@ void doc_manager::project_expand(expr_ref& fml, bit_vector const& to_delete) { for (unsigned i = 0; i < num_tbits(); ++i) { if (to_delete.get(i)) { expr_safe_replace rep1(m), rep2(m); - rep1.insert(tbvm().mk_var(m, i), m.mk_true()); + rep1.insert(mk_var(m, i), m.mk_true()); rep1(fml, tmp1); - rep2.insert(tbvm().mk_var(m, i), m.mk_false()); + rep2.insert(mk_var(m, i), m.mk_false()); rep2(fml, tmp2); if (tmp1 == tmp2) { fml = tmp1; @@ -731,7 +755,7 @@ void doc_manager::project_rename(expr_ref& fml, bit_vector const& to_delete) { expr_safe_replace rep(m); for (unsigned i = 0, j = 0; i < num_tbits(); ++i) { if (!to_delete.get(i)) { - rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i)); + rep.insert(mk_var(m, j), mk_var(m, i)); ++j; } } diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 10120ce8bb4..bae9f64e651 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -22,10 +22,10 @@ Revision History: #pragma once -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include "util/union_find.h" #include "util/buffer.h" - +#include "ast/ast.h" class doc; template class union_bvec; @@ -101,6 +101,8 @@ class doc_manager { void project_rename(expr_ref& fml, bit_vector const& to_delete); void project_expand(expr_ref& fml, bit_vector const& to_delete); expr_ref to_formula(ast_manager& m, doc const& src); + expr_ref to_formula(ast_manager& m, tbv const& src); + expr_ref mk_var(ast_manager& m, unsigned i); void check_equiv(ast_manager& m, expr* fml1, expr* fml2); }; diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index b1bb624a222..c62adb4f927 100644 --- a/src/test/ddnf.cpp +++ b/src/test/ddnf.cpp @@ -4,7 +4,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ #include "muz/ddnf/ddnf.h" -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include #include #include diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp index 6107fad85f9..fe33baba584 100644 --- a/src/test/tbv.cpp +++ b/src/test/tbv.cpp @@ -4,7 +4,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include static void tst1(unsigned num_bits) { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 35727bce2d8..c2a7e8296b2 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -54,6 +54,7 @@ z3_add_component(util state_graph.cpp statistics.cpp symbol.cpp + tbv.cpp timeit.cpp timeout.cpp trace.cpp diff --git a/src/muz/rel/tbv.cpp b/src/util/tbv.cpp similarity index 91% rename from src/muz/rel/tbv.cpp rename to src/util/tbv.cpp index 289e43b4ef6..017ca0eb702 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/util/tbv.cpp @@ -18,9 +18,8 @@ Revision History: --*/ -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include "util/hashtable.h" -#include "ast/ast_util.h" static bool s_debug_alloc = false; @@ -301,26 +300,3 @@ std::ostream& tbv_manager::display(std::ostream& out, tbv const& b) const { if (num_tbits() == 0) return out << "[]"; return display(out, b, num_tbits()-1, 0); } - -expr_ref tbv_manager::to_formula(ast_manager& m, tbv const& src) { - expr_ref result(m); - expr_ref_vector conj(m); - for (unsigned i = 0; i < num_tbits(); ++i) { - switch (src[i]) { - case BIT_0: - conj.push_back(m.mk_not(m.mk_const(symbol(i), m.mk_bool_sort()))); - break; - case BIT_1: - conj.push_back(m.mk_const(symbol(i), m.mk_bool_sort())); - break; - default: - break; - } - } - result = mk_and(m, conj.size(), conj.data()); - return result; -} - -expr_ref tbv_manager::mk_var(ast_manager& m, unsigned i) { - return expr_ref(m.mk_const(symbol(i), m.mk_bool_sort()), m); -} diff --git a/src/muz/rel/tbv.h b/src/util/tbv.h similarity index 96% rename from src/muz/rel/tbv.h rename to src/util/tbv.h index a8aaea23460..2a337be1f3a 100644 --- a/src/muz/rel/tbv.h +++ b/src/util/tbv.h @@ -21,8 +21,8 @@ Revision History: #pragma once #include "util/fixed_bit_vector.h" +#include "util/bit_vector.h" #include "util/rational.h" -#include "ast/ast.h" class tbv; @@ -84,10 +84,7 @@ class tbv_manager { void set(tbv& dst, tbv const& other, unsigned hi, unsigned lo); void set(tbv& dst, unsigned index, tbit value); - static void debug_alloc(); - expr_ref to_formula(ast_manager& m, tbv const& src); - expr_ref mk_var(ast_manager& m, unsigned i); }; class tbv: private fixed_bit_vector {