From 1fdde9e05606ce94a4ebad5fd1c0be63d97847e9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 17 Dec 2019 10:03:01 -0800
Subject: [PATCH] move bdd to separate space
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_project.py | 3 +-
src/CMakeLists.txt | 1 +
src/{sat/sat_bdd.cpp => math/dd/dd_bdd.cpp} | 6 ++--
src/{sat/sat_bdd.h => math/dd/dd_bdd.h} | 8 ++---
src/sat/CMakeLists.txt | 1 -
src/sat/sat_elim_vars.cpp | 34 ++++++++++-----------
src/sat/sat_elim_vars.h | 18 +++++------
7 files changed, 36 insertions(+), 35 deletions(-)
rename src/{sat/sat_bdd.cpp => math/dd/dd_bdd.cpp} (99%)
rename src/{sat/sat_bdd.h => math/dd/dd_bdd.h} (99%)
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index ecf40bf21..ad6e3e32b 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -15,7 +15,8 @@ def init_project_def():
init_version()
add_lib('util', [], includes2install = ['z3_version.h'])
add_lib('polynomial', ['util'], 'math/polynomial')
- add_lib('sat', ['util'])
+ add_lib('dd', ['util'], 'math/dd')
+ add_lib('sat', ['util','dd'])
add_lib('nlsat', ['polynomial', 'sat'])
add_lib('lp', ['util','nlsat'], 'util/lp')
add_lib('hilbert', ['util'], 'math/hilbert')
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6d4930ed0..3d50bb21a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -54,6 +54,7 @@ add_subdirectory(ast/substitution)
add_subdirectory(parsers/util)
add_subdirectory(math/grobner)
add_subdirectory(math/euclid)
+add_subdirectory(math/dd)
add_subdirectory(tactic/core)
add_subdirectory(math/subpaving/tactic)
add_subdirectory(tactic/aig)
diff --git a/src/sat/sat_bdd.cpp b/src/math/dd/dd_bdd.cpp
similarity index 99%
rename from src/sat/sat_bdd.cpp
rename to src/math/dd/dd_bdd.cpp
index e7b0632d8..a9a43dd18 100644
--- a/src/sat/sat_bdd.cpp
+++ b/src/math/dd/dd_bdd.cpp
@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation
Module Name:
- sat_bdd.cpp
+ dd_bdd.cpp
Abstract:
@@ -17,11 +17,11 @@ Revision History:
--*/
-#include "sat/sat_bdd.h"
#include "util/trace.h"
#include "util/stopwatch.h"
+#include "math/dd/dd_bdd.h"
-namespace sat {
+namespace dd {
bdd_manager::bdd_manager(unsigned num_vars) {
m_cost_metric = bdd_cost;
diff --git a/src/sat/sat_bdd.h b/src/math/dd/dd_bdd.h
similarity index 99%
rename from src/sat/sat_bdd.h
rename to src/math/dd/dd_bdd.h
index 70f6960fe..9ad69255b 100644
--- a/src/sat/sat_bdd.h
+++ b/src/math/dd/dd_bdd.h
@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation
Module Name:
- sat_bdd
+ dd_bdd
Abstract:
@@ -16,14 +16,14 @@ Author:
Revision History:
--*/
-#ifndef SAT_BDD_H_
-#define SAT_BDD_H_
+#ifndef DD_BDD_H_
+#define DD_BDD_H_
#include "util/vector.h"
#include "util/map.h"
#include "util/small_object_allocator.h"
-namespace sat {
+namespace dd {
class bdd;
diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt
index ee4d19489..e94586854 100644
--- a/src/sat/CMakeLists.txt
+++ b/src/sat/CMakeLists.txt
@@ -3,7 +3,6 @@ z3_add_component(sat
ba_solver.cpp
dimacs.cpp
sat_asymm_branch.cpp
- sat_bdd.cpp
sat_big.cpp
sat_binspr.cpp
sat_clause.cpp
diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
index 1759ec2ad..44a8a979d 100644
--- a/src/sat/sat_elim_vars.cpp
+++ b/src/sat/sat_elim_vars.cpp
@@ -56,7 +56,7 @@ namespace sat{
// associate index with each variable.
sort_marked();
- bdd b1 = elim_var(v);
+ dd::bdd b1 = elim_var(v);
double sz1 = b1.cnf_size();
if (sz1 > 2*clause_size) {
++m_miss;
@@ -76,7 +76,7 @@ namespace sat{
return false;
}
- bool elim_vars::elim_var(bool_var v, bdd const& b) {
+ bool elim_vars::elim_var(bool_var v, dd::bdd const& b) {
literal pos_l(v, false);
literal neg_l(v, true);
clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
@@ -105,7 +105,7 @@ namespace sat{
return true;
}
- bdd elim_vars::elim_var(bool_var v) {
+ dd::bdd elim_vars::elim_var(bool_var v) {
unsigned index = 0;
for (bool_var w : m_vars) {
m_var2index[w] = index++;
@@ -115,12 +115,12 @@ namespace sat{
clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
clause_use_list & neg_occs = simp.m_use_list.get(neg_l);
- bdd b1 = make_clauses(pos_l);
- bdd b2 = make_clauses(neg_l);
- bdd b3 = make_clauses(pos_occs);
- bdd b4 = make_clauses(neg_occs);
- bdd b0 = b1 && b2 && b3 && b4;
- bdd b = m.mk_exists(m_var2index[v], b0);
+ dd::bdd b1 = make_clauses(pos_l);
+ dd::bdd b2 = make_clauses(neg_l);
+ dd::bdd b3 = make_clauses(pos_occs);
+ dd::bdd b4 = make_clauses(neg_occs);
+ dd::bdd b0 = b1 && b2 && b3 && b4;
+ dd::bdd b = m.mk_exists(m_var2index[v], b0);
TRACE("elim_vars",
tout << "eliminate " << v << "\n";
for (watched const& w : simp.get_wlist(~pos_l)) {
@@ -157,7 +157,7 @@ namespace sat{
return b;
}
- void elim_vars::add_clauses(bool_var v0, bdd const& b, literal_vector& lits) {
+ void elim_vars::add_clauses(bool_var v0, dd::bdd const& b, literal_vector& lits) {
if (b.is_true()) {
// no-op
}
@@ -207,7 +207,7 @@ namespace sat{
}
- void elim_vars::get_clauses(bdd const& b, literal_vector & lits, clause_vector& clauses, literal_vector& units) {
+ void elim_vars::get_clauses(dd::bdd const& b, literal_vector & lits, clause_vector& clauses, literal_vector& units) {
if (b.is_true()) {
return;
}
@@ -303,11 +303,11 @@ namespace sat{
return num_vars() <= m_max_literals;
}
- bdd elim_vars::make_clauses(clause_use_list & occs) {
- bdd result = m.mk_true();
+ dd::bdd elim_vars::make_clauses(clause_use_list & occs) {
+ dd::bdd result = m.mk_true();
for (auto it = occs.mk_iterator(); !it.at_end(); it.next()) {
clause const& c = it.curr();
- bdd cl = m.mk_false();
+ dd::bdd cl = m.mk_false();
for (literal l : c) {
cl |= mk_literal(l);
}
@@ -316,8 +316,8 @@ namespace sat{
return result;
}
- bdd elim_vars::make_clauses(literal lit) {
- bdd result = m.mk_true();
+ dd::bdd elim_vars::make_clauses(literal lit) {
+ dd::bdd result = m.mk_true();
watch_list& wl = simp.get_wlist(~lit);
for (watched const& w : wl) {
if (w.is_binary_non_learned_clause()) {
@@ -327,7 +327,7 @@ namespace sat{
return result;
}
- bdd elim_vars::mk_literal(literal l) {
+ dd::bdd elim_vars::mk_literal(literal l) {
return l.sign() ? m.mk_nvar(m_var2index[l.var()]) : m.mk_var(m_var2index[l.var()]);
}
diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h
index b62fdc5db..b3cc6b589 100644
--- a/src/sat/sat_elim_vars.h
+++ b/src/sat/sat_elim_vars.h
@@ -20,7 +20,7 @@ Revision History:
#define SAT_ELIM_VARS_H_
#include "sat/sat_types.h"
-#include "sat/sat_bdd.h"
+#include "math/dd/dd_bdd.h"
namespace sat {
class solver;
@@ -31,7 +31,7 @@ namespace sat {
simplifier& simp;
solver& s;
- bdd_manager m;
+ dd::bdd_manager m;
random_gen m_rand;
@@ -53,13 +53,13 @@ namespace sat {
void shuffle_vars();
bool mark_literals(clause_use_list & occs);
bool mark_literals(literal lit);
- bdd make_clauses(clause_use_list & occs);
- bdd make_clauses(literal lit);
- bdd mk_literal(literal l);
- void get_clauses(bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units);
- void add_clauses(bool_var v, bdd const& b, literal_vector& lits);
- bool elim_var(bool_var v, bdd const& b);
- bdd elim_var(bool_var v);
+ dd::bdd make_clauses(clause_use_list & occs);
+ dd::bdd make_clauses(literal lit);
+ dd::bdd mk_literal(literal l);
+ void get_clauses(dd::bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units);
+ void add_clauses(bool_var v, dd::bdd const& b, literal_vector& lits);
+ bool elim_var(bool_var v, dd::bdd const& b);
+ dd::bdd elim_var(bool_var v);
public:
elim_vars(simplifier& s);