mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

move bdd to separate space

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-17 10:03:01 -08:00
parent c560ee54e8
commit 1fdde9e056
7 changed files with 36 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_project.py
View file

@ -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')

1
src/CMakeLists.txt
View file

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

6
src/sat/sat_bdd.cpp → src/math/dd/dd_bdd.cpp
View file

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

8
src/sat/sat_bdd.h → src/math/dd/dd_bdd.h
View file

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

1
src/sat/CMakeLists.txt
View file

@ -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

34
src/sat/sat_elim_vars.cpp
View file

@ -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()]);
}

18
src/sat/sat_elim_vars.h
View file

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