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);