mirror of
https://github.com/Z3Prover/z3
synced 2025-11-03 21:09:11 +00:00
use variable id as level, separate cut-set updates, add missing reset in pdd
This commit is contained in:
Nikolaj Bjorner
parent
55554215ac
commit
57846e50fa
8 changed files with 158 additions and 126 deletions
|
|
@ -49,8 +49,9 @@ namespace dd {
|
|||
m_nodes.reset();
|
||||
m_free_nodes.reset();
|
||||
m_pdd_stack.reset();
|
||||
m_mpq_table.reset();
|
||||
m_values.reset();
|
||||
m_free_values.reset();
|
||||
m_mpq_table.reset();
|
||||
init_nodes(level2var);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -83,12 +83,12 @@ namespace sat {
|
|||
std::function<void (literal_vector const&)> on_xor =
|
||||
[&,this](literal_vector const& xors) {
|
||||
SASSERT(xors.size() > 1);
|
||||
unsigned max_level = s.def_level(xors.back().var());
|
||||
unsigned max_level = xors.back().var();
|
||||
unsigned index = xors.size() - 1;
|
||||
for (unsigned i = index; i-- > 0; ) {
|
||||
literal l = xors[i];
|
||||
if (s.def_level(l.var()) > max_level) {
|
||||
max_level = s.def_level(l.var());
|
||||
if (l.var() > max_level) {
|
||||
max_level = l.var();
|
||||
index = i;
|
||||
}
|
||||
}
|
||||
|
|
@ -227,109 +227,138 @@ namespace sat {
|
|||
|
||||
vector<cut_set> aig_cuts::get_cuts(unsigned max_cut_size, unsigned max_cutset_size) {
|
||||
unsigned_vector sorted = top_sort();
|
||||
vector<cut_set> cuts;
|
||||
cuts.resize(m_aig.size());
|
||||
max_cut_size = std::min(cut().max_cut_size, max_cut_size);
|
||||
cut_set cut_set2;
|
||||
cut_set2.init(m_region, max_cutset_size + 1);
|
||||
vector<cut_set> cuts(m_aig.size());
|
||||
m_max_cut_size = std::min(cut().max_cut_size, max_cut_size);
|
||||
m_max_cutset_size = max_cutset_size;
|
||||
m_cut_set1.init(m_region, m_max_cutset_size + 1);
|
||||
m_cut_set2.init(m_region, m_max_cutset_size + 1);
|
||||
|
||||
unsigned j = 0;
|
||||
for (unsigned id : sorted) {
|
||||
node const& n = m_aig[id];
|
||||
if (!n.is_valid()) {
|
||||
continue;
|
||||
if (n.is_valid()) {
|
||||
auto& cut_set = cuts[id];
|
||||
cut_set.init(m_region, m_max_cutset_size + 1);
|
||||
cut_set.push_back(cut(id));
|
||||
sorted[j++] = id;
|
||||
}
|
||||
}
|
||||
sorted.shrink(j);
|
||||
augment(sorted, cuts);
|
||||
return cuts;
|
||||
}
|
||||
|
||||
void aig_cuts::augment(unsigned_vector const& ids, vector<cut_set>& cuts) {
|
||||
for (unsigned id : ids) {
|
||||
node const& n = m_aig[id];
|
||||
SASSERT(n.is_valid());
|
||||
auto& cut_set = cuts[id];
|
||||
cut_set.init(m_region, max_cutset_size + 1);
|
||||
if (n.is_var()) {
|
||||
SASSERT(!n.sign());
|
||||
}
|
||||
else if (n.is_ite()) {
|
||||
literal l1 = child(n, 0);
|
||||
literal l2 = child(n, 1);
|
||||
literal l3 = child(n, 2);
|
||||
for (auto const& a : cuts[l1.var()]) {
|
||||
for (auto const& b : cuts[l2.var()]) {
|
||||
cut ab;
|
||||
if (!ab.merge(a, b, max_cut_size)) {
|
||||
continue;
|
||||
}
|
||||
for (auto const& c : cuts[l3.var()]) {
|
||||
cut abc;
|
||||
if (!abc.merge(ab, c, max_cut_size)) {
|
||||
continue;
|
||||
}
|
||||
if (cut_set.size() >= max_cutset_size) break;
|
||||
uint64_t t1 = a.shift_table(abc);
|
||||
uint64_t t2 = b.shift_table(abc);
|
||||
uint64_t t3 = c.shift_table(abc);
|
||||
if (l1.sign()) t1 = ~t1;
|
||||
if (l2.sign()) t2 = ~t2;
|
||||
if (l3.sign()) t3 = ~t3;
|
||||
abc.set_table((t1 & t2) | (~t1 & t3));
|
||||
if (n.sign()) abc.negate();
|
||||
// extract tree size: abc.m_tree_size = a.m_tree_size + b.m_tree_size + c.m_tree_size + 1;
|
||||
cut_set.insert(abc);
|
||||
}
|
||||
}
|
||||
}
|
||||
augment_ite(n, cut_set, cuts);
|
||||
}
|
||||
else if (n.num_children() == 2) {
|
||||
SASSERT(n.is_and() || n.is_xor());
|
||||
literal l1 = child(n, 0);
|
||||
literal l2 = child(n, 1);
|
||||
for (auto const& a : cuts[l1.var()]) {
|
||||
for (auto const& b : cuts[l2.var()]) {
|
||||
if (cut_set.size() >= max_cutset_size) break;
|
||||
cut c;
|
||||
if (c.merge(a, b, max_cut_size)) {
|
||||
uint64_t t1 = a.shift_table(c);
|
||||
uint64_t t2 = b.shift_table(c);
|
||||
if (l1.sign()) t1 = ~t1;
|
||||
if (l2.sign()) t2 = ~t2;
|
||||
uint64_t t3 = n.is_and() ? t1 & t2 : t1 ^ t2;
|
||||
c.set_table(t3);
|
||||
if (n.sign()) c.negate();
|
||||
cut_set.insert(c);
|
||||
}
|
||||
}
|
||||
if (cut_set.size() >= max_cutset_size) break;
|
||||
}
|
||||
augment_aig2(n, cut_set, cuts);
|
||||
}
|
||||
else if (n.num_children() < max_cut_size) {
|
||||
SASSERT(n.is_and() || n.is_xor());
|
||||
literal lit = child(n, 0);
|
||||
for (auto const& a : cuts[lit.var()]) {
|
||||
cut_set.push_back(a);
|
||||
if (lit.sign()) {
|
||||
cut_set.back().negate();
|
||||
}
|
||||
}
|
||||
for (unsigned i = 1; i < n.num_children(); ++i) {
|
||||
cut_set2.reset();
|
||||
literal lit = child(n, i);
|
||||
for (auto const& a : cut_set) {
|
||||
for (auto const& b : cuts[lit.var()]) {
|
||||
cut c;
|
||||
if (cut_set2.size() >= max_cutset_size)
|
||||
break;
|
||||
if (c.merge(a, b, max_cut_size)) {
|
||||
uint64_t t1 = a.shift_table(c);
|
||||
uint64_t t2 = b.shift_table(c);
|
||||
if (lit.sign()) t2 = ~t2;
|
||||
uint64_t t3 = n.is_and() ? t1 & t2 : t1 ^ t2;
|
||||
c.set_table(t3);
|
||||
if (i + 1 == n.num_children() && n.sign()) c.negate();
|
||||
cut_set2.insert(c);
|
||||
}
|
||||
}
|
||||
if (cut_set2.size() >= max_cutset_size)
|
||||
break;
|
||||
}
|
||||
cut_set.swap(cut_set2);
|
||||
}
|
||||
else if (n.num_children() < m_max_cut_size && cut_set.size() < m_max_cutset_size) {
|
||||
augment_aigN(n, cut_set, cuts);
|
||||
}
|
||||
cut_set.push_back(cut(id));
|
||||
}
|
||||
return cuts;
|
||||
}
|
||||
|
||||
void aig_cuts::augment_ite(node const& n, cut_set& cs, vector<cut_set>& cuts) {
|
||||
literal l1 = child(n, 0);
|
||||
literal l2 = child(n, 1);
|
||||
literal l3 = child(n, 2);
|
||||
for (auto const& a : cuts[l1.var()]) {
|
||||
for (auto const& b : cuts[l2.var()]) {
|
||||
cut ab;
|
||||
if (!ab.merge(a, b, m_max_cut_size)) {
|
||||
continue;
|
||||
}
|
||||
for (auto const& c : cuts[l3.var()]) {
|
||||
cut abc;
|
||||
if (!abc.merge(ab, c, m_max_cut_size)) {
|
||||
continue;
|
||||
}
|
||||
if (cs.size() >= m_max_cutset_size) break;
|
||||
uint64_t t1 = a.shift_table(abc);
|
||||
uint64_t t2 = b.shift_table(abc);
|
||||
uint64_t t3 = c.shift_table(abc);
|
||||
if (l1.sign()) t1 = ~t1;
|
||||
if (l2.sign()) t2 = ~t2;
|
||||
if (l3.sign()) t3 = ~t3;
|
||||
abc.set_table((t1 & t2) | (~t1 & t3));
|
||||
if (n.sign()) abc.negate();
|
||||
// extract tree size: abc.m_tree_size = a.m_tree_size + b.m_tree_size + c.m_tree_size + 1;
|
||||
cs.insert(abc);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig2(node const& n, cut_set& cs, vector<cut_set>& cuts) {
|
||||
SASSERT(n.is_and() || n.is_xor());
|
||||
literal l1 = child(n, 0);
|
||||
literal l2 = child(n, 1);
|
||||
for (auto const& a : cuts[l1.var()]) {
|
||||
for (auto const& b : cuts[l2.var()]) {
|
||||
if (cs.size() >= m_max_cutset_size) break;
|
||||
cut c;
|
||||
if (c.merge(a, b, m_max_cut_size)) {
|
||||
uint64_t t1 = a.shift_table(c);
|
||||
uint64_t t2 = b.shift_table(c);
|
||||
if (l1.sign()) t1 = ~t1;
|
||||
if (l2.sign()) t2 = ~t2;
|
||||
uint64_t t3 = n.is_and() ? t1 & t2 : t1 ^ t2;
|
||||
c.set_table(t3);
|
||||
if (n.sign()) c.negate();
|
||||
cs.insert(c);
|
||||
}
|
||||
}
|
||||
if (cs.size() >= m_max_cutset_size)
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aigN(node const& n, cut_set& cs, vector<cut_set>& cuts) {
|
||||
m_cut_set1.reset();
|
||||
SASSERT(n.is_and() || n.is_xor());
|
||||
literal lit = child(n, 0);
|
||||
for (auto const& a : cuts[lit.var()]) {
|
||||
m_cut_set1.push_back(a);
|
||||
if (lit.sign()) {
|
||||
m_cut_set1.back().negate();
|
||||
}
|
||||
}
|
||||
for (unsigned i = 1; i < n.num_children(); ++i) {
|
||||
m_cut_set2.reset();
|
||||
literal lit = child(n, i);
|
||||
for (auto const& a : m_cut_set1) {
|
||||
for (auto const& b : cuts[lit.var()]) {
|
||||
cut c;
|
||||
if (m_cut_set2.size() + cs.size() >= m_max_cutset_size)
|
||||
break;
|
||||
if (c.merge(a, b, m_max_cut_size)) {
|
||||
uint64_t t1 = a.shift_table(c);
|
||||
uint64_t t2 = b.shift_table(c);
|
||||
if (lit.sign()) t2 = ~t2;
|
||||
uint64_t t3 = n.is_and() ? t1 & t2 : t1 ^ t2;
|
||||
c.set_table(t3);
|
||||
if (i + 1 == n.num_children() && n.sign()) c.negate();
|
||||
m_cut_set2.insert(c);
|
||||
}
|
||||
}
|
||||
if (m_cut_set2.size() + cs.size() >= m_max_cutset_size)
|
||||
break;
|
||||
}
|
||||
m_cut_set1.swap(m_cut_set2);
|
||||
}
|
||||
for (auto & cut : m_cut_set1) {
|
||||
cs.insert(cut);
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::add_var(unsigned v) {
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ namespace sat {
|
|||
};
|
||||
|
||||
class aig_cuts {
|
||||
// encodes one of var, n1 & n2 & .. & nk, !(n1 & n2 & .. & nk)
|
||||
// encodes one of var, and, !and, xor, !xor, ite, !ite.
|
||||
class node {
|
||||
bool m_sign;
|
||||
bool_op m_op;
|
||||
|
|
@ -54,11 +54,20 @@ namespace sat {
|
|||
unsigned num_children() const { SASSERT(!is_var()); return m_num_children; }
|
||||
unsigned offset() const { return m_offset; }
|
||||
};
|
||||
svector<node> m_aig; // vector of aig nodes.
|
||||
svector<node> m_aig; // vector of main aig nodes.
|
||||
vector<svector<node>> m_aux_aig; // vector of auxiliary aig nodes.
|
||||
literal_vector m_literals;
|
||||
region m_region;
|
||||
unsigned m_max_cut_size;
|
||||
unsigned m_max_cutset_size;
|
||||
cut_set m_cut_set1, m_cut_set2;
|
||||
|
||||
unsigned_vector top_sort();
|
||||
void augment(unsigned_vector const& ids, vector<cut_set>& cuts);
|
||||
void augment_ite(node const& n, cut_set& cs, vector<cut_set>& cuts);
|
||||
void augment_aig2(node const& n, cut_set& cs, vector<cut_set>& cuts);
|
||||
void augment_aigN(node const& n, cut_set& cs, vector<cut_set>& cuts);
|
||||
|
||||
public:
|
||||
void add_var(unsigned v);
|
||||
void add_node(literal head, bool_op op, unsigned sz, literal const* args);
|
||||
|
|
|
|||
|
|
@ -353,7 +353,7 @@ namespace sat {
|
|||
|
||||
/**
|
||||
assign levels to variables.
|
||||
use s.def_level as a primary source for the level of a variable.
|
||||
use variable id as a primary source for the level of a variable.
|
||||
secondarily, sort variables randomly (each variable is assigned
|
||||
a random, unique, id).
|
||||
*/
|
||||
|
|
@ -365,7 +365,7 @@ namespace sat {
|
|||
for (unsigned i = 0; i < nv; ++i) var2id[i] = i;
|
||||
shuffle(var2id.size(), var2id.c_ptr(), s.rand());
|
||||
for (unsigned i = 0; i < nv; ++i) id2var[var2id[i]] = i;
|
||||
for (unsigned i = 0; i < nv; ++i) vl[i] = std::make_pair(s.def_level(i), var2id[i]);
|
||||
for (unsigned i = 0; i < nv; ++i) vl[i] = std::make_pair(i, var2id[i]);
|
||||
std::sort(vl.begin(), vl.end());
|
||||
for (unsigned i = 0; i < nv; ++i) l2v[i] = id2var[vl[i].second];
|
||||
|
||||
|
|
|
|||
|
|
@ -151,7 +151,6 @@ namespace sat {
|
|||
m_phase[v] = src.m_phase[v];
|
||||
m_best_phase[v] = src.m_best_phase[v];
|
||||
m_prev_phase[v] = src.m_prev_phase[v];
|
||||
m_level[v] = src.m_level[v];
|
||||
|
||||
// inherit activity:
|
||||
m_activity[v] = src.m_activity[v];
|
||||
|
|
@ -239,7 +238,7 @@ namespace sat {
|
|||
//
|
||||
// -----------------------
|
||||
|
||||
bool_var solver::mk_var(bool ext, bool dvar, unsigned level) {
|
||||
bool_var solver::mk_var(bool ext, bool dvar) {
|
||||
m_model_is_current = false;
|
||||
m_stats.m_mk_var++;
|
||||
bool_var v = m_justification.size();
|
||||
|
|
@ -251,7 +250,6 @@ namespace sat {
|
|||
m_decision.push_back(dvar);
|
||||
m_eliminated.push_back(false);
|
||||
m_external.push_back(ext);
|
||||
m_level.push_back(level);
|
||||
m_touched.push_back(0);
|
||||
m_activity.push_back(0);
|
||||
m_mark.push_back(false);
|
||||
|
|
@ -3859,7 +3857,6 @@ namespace sat {
|
|||
m_decision.shrink(v);
|
||||
m_eliminated.shrink(v);
|
||||
m_external.shrink(v);
|
||||
m_level.shrink(v);
|
||||
m_touched.shrink(v);
|
||||
m_activity.shrink(v);
|
||||
m_mark.shrink(v);
|
||||
|
|
|
|||
|
|
@ -122,7 +122,6 @@ namespace sat {
|
|||
svector<bool> m_lit_mark;
|
||||
svector<bool> m_eliminated;
|
||||
svector<bool> m_external;
|
||||
unsigned_vector m_level;
|
||||
unsigned_vector m_touched;
|
||||
unsigned m_touch_index;
|
||||
literal_vector m_replay_assign;
|
||||
|
|
@ -248,9 +247,9 @@ namespace sat {
|
|||
//
|
||||
// -----------------------
|
||||
void add_clause(unsigned num_lits, literal * lits, bool learned) override { mk_clause(num_lits, lits, learned); }
|
||||
bool_var add_var(bool ext, unsigned level = 0) override { return mk_var(ext, true, level); }
|
||||
bool_var add_var(bool ext) override { return mk_var(ext, true); }
|
||||
|
||||
bool_var mk_var(bool ext = false, bool dvar = true, unsigned level = 0);
|
||||
bool_var mk_var(bool ext = false, bool dvar = true);
|
||||
|
||||
clause* mk_clause(literal_vector const& lits, bool learned = false) { return mk_clause(lits.size(), lits.c_ptr(), learned); }
|
||||
clause* mk_clause(unsigned num_lits, literal * lits, bool learned = false);
|
||||
|
|
@ -335,7 +334,6 @@ namespace sat {
|
|||
bool was_eliminated(bool_var v) const { return m_eliminated[v]; }
|
||||
void set_eliminated(bool_var v, bool f) override;
|
||||
bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
|
||||
unsigned def_level(bool_var v) const { return m_level[v]; }
|
||||
unsigned scope_lvl() const { return m_scope_lvl; }
|
||||
unsigned search_lvl() const { return m_search_lvl; }
|
||||
bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
|
||||
|
|
|
|||
|
|
@ -63,9 +63,7 @@ namespace sat {
|
|||
add_clause(3, lits, is_redundant);
|
||||
}
|
||||
// create boolean variable, tagged as external (= true) or internal (can be eliminated).
|
||||
// the level indicates the depth in an ast the variable comes from.
|
||||
// variables of higher levels are outputs gates relative to lower levels
|
||||
virtual bool_var add_var(bool ext, unsigned level = 0) = 0;
|
||||
virtual bool_var add_var(bool ext) = 0;
|
||||
|
||||
// update parameters
|
||||
virtual void updt_params(params_ref const& p) {}
|
||||
|
|
|
|||
|
|
@ -121,7 +121,7 @@ struct goal2sat::imp {
|
|||
sat::literal mk_true() {
|
||||
if (m_true == sat::null_literal) {
|
||||
// create fake variable to represent true;
|
||||
m_true = sat::literal(m_solver.add_var(false, 0), false);
|
||||
m_true = sat::literal(m_solver.add_var(false), false);
|
||||
mk_clause(m_true); // v is true
|
||||
}
|
||||
return m_true;
|
||||
|
|
@ -140,7 +140,7 @@ struct goal2sat::imp {
|
|||
}
|
||||
else {
|
||||
bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
|
||||
sat::bool_var v = m_solver.add_var(ext, get_depth(t));
|
||||
sat::bool_var v = m_solver.add_var(ext);
|
||||
m_map.insert(t, v);
|
||||
l = sat::literal(v, sign);
|
||||
TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << "\n";);
|
||||
|
|
@ -248,7 +248,7 @@ struct goal2sat::imp {
|
|||
}
|
||||
else {
|
||||
SASSERT(num <= m_result_stack.size());
|
||||
sat::bool_var k = m_solver.add_var(false, get_depth(t));
|
||||
sat::bool_var k = m_solver.add_var(false);
|
||||
sat::literal l(k, false);
|
||||
m_cache.insert(t, l);
|
||||
sat::literal * lits = m_result_stack.end() - num;
|
||||
|
|
@ -287,7 +287,7 @@ struct goal2sat::imp {
|
|||
}
|
||||
else {
|
||||
SASSERT(num <= m_result_stack.size());
|
||||
sat::bool_var k = m_solver.add_var(false, get_depth(t));
|
||||
sat::bool_var k = m_solver.add_var(false);
|
||||
sat::literal l(k, false);
|
||||
m_cache.insert(t, l);
|
||||
// l => /\ lits
|
||||
|
|
@ -330,7 +330,7 @@ struct goal2sat::imp {
|
|||
m_result_stack.reset();
|
||||
}
|
||||
else {
|
||||
sat::bool_var k = m_solver.add_var(false, get_depth(n));
|
||||
sat::bool_var k = m_solver.add_var(false);
|
||||
sat::literal l(k, false);
|
||||
m_cache.insert(n, l);
|
||||
mk_clause(~l, ~c, t);
|
||||
|
|
@ -367,7 +367,7 @@ struct goal2sat::imp {
|
|||
m_result_stack.reset();
|
||||
}
|
||||
else {
|
||||
sat::bool_var k = m_solver.add_var(false, get_depth(t));
|
||||
sat::bool_var k = m_solver.add_var(false);
|
||||
sat::literal l(k, false);
|
||||
m_cache.insert(t, l);
|
||||
mk_clause(~l, l1, ~l2);
|
||||
|
|
@ -391,7 +391,7 @@ struct goal2sat::imp {
|
|||
return;
|
||||
}
|
||||
sat::literal_vector lits;
|
||||
sat::bool_var v = m_solver.add_var(true, get_depth(t));
|
||||
sat::bool_var v = m_solver.add_var(true);
|
||||
lits.push_back(sat::literal(v, true));
|
||||
convert_pb_args(num, lits);
|
||||
// ensure that = is converted to xor
|
||||
|
|
@ -473,7 +473,7 @@ struct goal2sat::imp {
|
|||
m_ext->add_pb_ge(sat::null_bool_var, wlits, k1);
|
||||
}
|
||||
else {
|
||||
sat::bool_var v = m_solver.add_var(true, get_depth(t));
|
||||
sat::bool_var v = m_solver.add_var(true);
|
||||
sat::literal lit(v, sign);
|
||||
m_ext->add_pb_ge(v, wlits, k.get_unsigned());
|
||||
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
|
||||
|
|
@ -504,7 +504,7 @@ struct goal2sat::imp {
|
|||
m_ext->add_pb_ge(sat::null_bool_var, wlits, k1);
|
||||
}
|
||||
else {
|
||||
sat::bool_var v = m_solver.add_var(true, get_depth(t));
|
||||
sat::bool_var v = m_solver.add_var(true);
|
||||
sat::literal lit(v, sign);
|
||||
m_ext->add_pb_ge(v, wlits, k.get_unsigned());
|
||||
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
|
||||
|
|
@ -518,8 +518,8 @@ struct goal2sat::imp {
|
|||
svector<wliteral> wlits;
|
||||
convert_pb_args(t, wlits);
|
||||
bool base_assert = (root && !sign && m_solver.num_user_scopes() == 0);
|
||||
sat::bool_var v1 = base_assert ? sat::null_bool_var : m_solver.add_var(true, get_depth(t));
|
||||
sat::bool_var v2 = base_assert ? sat::null_bool_var : m_solver.add_var(true, get_depth(t));
|
||||
sat::bool_var v1 = base_assert ? sat::null_bool_var : m_solver.add_var(true);
|
||||
sat::bool_var v2 = base_assert ? sat::null_bool_var : m_solver.add_var(true);
|
||||
m_ext->add_pb_ge(v1, wlits, k.get_unsigned());
|
||||
k.neg();
|
||||
for (wliteral& wl : wlits) {
|
||||
|
|
@ -533,7 +533,7 @@ struct goal2sat::imp {
|
|||
}
|
||||
else {
|
||||
sat::literal l1(v1, false), l2(v2, false);
|
||||
sat::bool_var v = m_solver.add_var(false, get_depth(t));
|
||||
sat::bool_var v = m_solver.add_var(false);
|
||||
sat::literal l(v, false);
|
||||
mk_clause(~l, l1);
|
||||
mk_clause(~l, l2);
|
||||
|
|
@ -558,7 +558,7 @@ struct goal2sat::imp {
|
|||
m_ext->add_at_least(sat::null_bool_var, lits, k2);
|
||||
}
|
||||
else {
|
||||
sat::bool_var v = m_solver.add_var(true, get_depth(t));
|
||||
sat::bool_var v = m_solver.add_var(true);
|
||||
sat::literal lit(v, false);
|
||||
m_ext->add_at_least(v, lits, k.get_unsigned());
|
||||
m_cache.insert(t, lit);
|
||||
|
|
@ -585,7 +585,7 @@ struct goal2sat::imp {
|
|||
m_ext->add_at_least(sat::null_bool_var, lits, k2);
|
||||
}
|
||||
else {
|
||||
sat::bool_var v = m_solver.add_var(true, get_depth(t));
|
||||
sat::bool_var v = m_solver.add_var(true);
|
||||
sat::literal lit(v, false);
|
||||
m_ext->add_at_least(v, lits, k2);
|
||||
m_cache.insert(t, lit);
|
||||
|
|
@ -598,8 +598,8 @@ struct goal2sat::imp {
|
|||
SASSERT(k.is_unsigned());
|
||||
sat::literal_vector lits;
|
||||
convert_pb_args(t->get_num_args(), lits);
|
||||
sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.add_var(true, get_depth(t));
|
||||
sat::bool_var v2 = (root && !sign) ? sat::null_bool_var : m_solver.add_var(true, get_depth(t));
|
||||
sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.add_var(true);
|
||||
sat::bool_var v2 = (root && !sign) ? sat::null_bool_var : m_solver.add_var(true);
|
||||
m_ext->add_at_least(v1, lits, k.get_unsigned());
|
||||
for (sat::literal& l : lits) {
|
||||
l.neg();
|
||||
|
|
@ -612,7 +612,7 @@ struct goal2sat::imp {
|
|||
}
|
||||
else {
|
||||
sat::literal l1(v1, false), l2(v2, false);
|
||||
sat::bool_var v = m_solver.add_var(false, get_depth(t));
|
||||
sat::bool_var v = m_solver.add_var(false);
|
||||
sat::literal l(v, false);
|
||||
mk_clause(~l, l1);
|
||||
mk_clause(~l, l2);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue