Skip to content

Commit

Permalink
na
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Sep 2, 2020
1 parent e4b7b7b commit d83d0a8
Show file tree
Hide file tree
Showing 14 changed files with 274 additions and 59 deletions.
2 changes: 1 addition & 1 deletion src/ast/euf/euf_egraph.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -245,7 +245,7 @@ namespace euf {
std::swap(n1, n2);
}
if ((m.is_true(r2->get_owner()) || m.is_false(r2->get_owner())) && j.is_congruence()) {
m_new_lits.push_back(enode_pair(n1, false));
m_new_lits.push_back(enode_bool_pair(n1, false));
++m_stats.m_num_lits;
}
for (enode* p : enode_parents(n1))
Expand Down
32 changes: 11 additions & 21 deletions src/sat/sat_drat.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,18 +68,16 @@ namespace sat {
m_activity = s.get_config().m_drat_activity;
}

std::ostream& operator<<(std::ostream& out, status st) {
std::ostream& drat::pp(std::ostream& out, status st) const {
if (st.is_redundant())
out << "l";
else if (st.is_deleted())
out << "d";
else if (st.is_asserted())
out << "a";

if (st.is_ba())
out << " ba";
else if (st.is_euf())
out << " euf";
if (!st.is_sat())
out << " " << m_theory[st.get_th()];
return out;
}

Expand All @@ -103,15 +101,9 @@ namespace sat {
buffer[len++] = ' ';
}

if (st.is_euf()) {
buffer[len++] = 'e';
buffer[len++] = 'u';
buffer[len++] = 'f';
buffer[len++] = ' ';
}
else if (st.is_ba()) {
buffer[len++] = 'b';
buffer[len++] = 'a';
if (!st.is_sat()) {
for (char ch : m_theory[st.get_th()])
buffer[len++] = ch;
buffer[len++] = ' ';
}
for (unsigned i = 0; i < n; ++i) {
Expand Down Expand Up @@ -139,8 +131,6 @@ namespace sat {
buffer[len++] = '\n';
m_out->write(buffer, len);

m_out->flush();

}

void drat::dump_activity() {
Expand Down Expand Up @@ -192,7 +182,7 @@ namespace sat {
}

void drat::trace(std::ostream& out, unsigned n, literal const* c, status st) {
out << st << " ";
pp(out, st) << " ";
literal last = null_literal;
for (unsigned i = 0; i < n; ++i) {
if (c[i] != last) {
Expand All @@ -204,7 +194,7 @@ namespace sat {
}

void drat::append(literal l, status st) {
TRACE("sat_drat", tout << st << " " << l << "\n";);
TRACE("sat_drat", pp(tout, st) << " " << l << "\n";);

declare(l);
IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st););
Expand All @@ -222,7 +212,7 @@ namespace sat {
}

void drat::append(literal l1, literal l2, status st) {
TRACE("sat_drat", tout << st << " " << l1 << " " << l2 << "\n";);
TRACE("sat_drat", pp(tout, st) << " " << l1 << " " << l2 << "\n";);
declare(l1);
declare(l2);
literal lits[2] = { l1, l2 };
Expand Down Expand Up @@ -305,7 +295,7 @@ namespace sat {
#endif

void drat::append(clause& c, status st) {
TRACE("sat_drat", tout << st << " " << c << "\n";);
TRACE("sat_drat", pp(tout, st) << " " << c << "\n";);
for (literal lit : c) declare(lit);
unsigned n = c.size();
IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st););
Expand Down Expand Up @@ -609,7 +599,7 @@ namespace sat {
if (num_true == 0 && num_undef == 1) {
out << "Unit ";
}
out << m_status[i] << " " << i << ": " << *c << "\n";
pp(out, m_status[i]) << " " << i << ": " << *c << "\n";
}
}
for (unsigned i = 0; i < m_assignment.size(); ++i) {
Expand Down
5 changes: 4 additions & 1 deletion src/sat/sat_drat.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ namespace sat {
literal_vector m_units;
vector<watch> m_watches;
svector<lbool> m_assignment;
svector<std::string> m_theory;
bool m_inconsistent;
unsigned m_num_add, m_num_del;
bool m_check_unsat, m_check_sat, m_check, m_activity;
Expand All @@ -77,7 +78,7 @@ namespace sat {

bool is_clause(clause& c, literal l1, literal l2, literal l3, status st1, status st2);

friend std::ostream& operator<<(std::ostream & out, status st);
std::ostream& pp(std::ostream & out, status st) const;
status get_status(bool learned) const;

void declare(literal l);
Expand All @@ -99,6 +100,8 @@ namespace sat {
~drat();

void updt_config();

void add_theory(int id, symbol const& s) { m_theory.setx(id, s.str(), std::string()); }
void add();
void add(literal l, bool learned);
void add(literal l1, literal l2, status st);
Expand Down
24 changes: 9 additions & 15 deletions src/sat/sat_types.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -255,30 +255,24 @@ namespace sat {
class status {
public:
enum class st { asserted, redundant, deleted };
enum class orig { sat, ba, euf };
int m_orig;
st m_st;
orig m_orig;
public:
status(enum st s, enum orig o) : m_st(s), m_orig(o) {};
status(enum st s, int o) : m_st(s), m_orig(o) {};
status(status const& s) : m_st(s.m_st), m_orig(s.m_orig) {}
status(status&& s) noexcept { m_st = st::asserted; m_orig = orig::sat; std::swap(m_st, s.m_st); std::swap(m_orig, s.m_orig); }
static status redundant() { return status(status::st::redundant, status::orig::sat); }
static status asserted() { return status(status::st::asserted, status::orig::sat); }
static status deleted() { return status(status::st::deleted, status::orig::sat); }
status(status&& s) noexcept { m_st = st::asserted; m_orig = -1; std::swap(m_st, s.m_st); std::swap(m_orig, s.m_orig); }
static status redundant() { return status(status::st::redundant, -1); }
static status asserted() { return status(status::st::asserted, -1); }
static status deleted() { return status(status::st::deleted, -1); }

static status euf(bool redundant) { return status(redundant ? st::redundant : st::asserted, orig::euf); }

static status ba(bool redundant) { return redundant ? ba_redundant() : ba_asserted(); }
static status ba_redundant() { return status(status::st::redundant, status::orig::ba); }
static status ba_asserted() { return status(status::st::asserted, status::orig::ba); }
static status th(bool redundant, int id) { return status(redundant ? st::redundant : st::asserted, id); }

bool is_redundant() const { return st::redundant == m_st; }
bool is_asserted() const { return st::asserted == m_st; }
bool is_deleted() const { return st::deleted == m_st; }

bool is_sat() const { return orig::sat == m_orig; }
bool is_ba() const { return orig::ba == m_orig; }
bool is_euf() const { return orig::euf == m_orig; }
bool is_sat() const { return -1 == m_orig; }
int get_th() const { return m_orig; }
};


Expand Down
1 change: 1 addition & 0 deletions src/sat/smt/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ z3_add_component(sat_smt
atom2bool_var.cpp
ba_internalize.cpp
ba_solver.cpp
bv_internalize.cpp
xor_solver.cpp
euf_ackerman.cpp
euf_internalize.cpp
Expand Down
24 changes: 12 additions & 12 deletions src/sat/smt/ba_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -360,7 +360,7 @@ namespace sat {
}
if (p.k() == 1 && p.lit() == null_literal) {
literal_vector lits(p.literals());
s().mk_clause(lits.size(), lits.c_ptr(), status::ba(p.learned()));
s().mk_clause(lits.size(), lits.c_ptr(), status::th(p.learned(), get_id()));
IF_VERBOSE(100, display(verbose_stream() << "add clause: " << lits << "\n", p, true););
remove_constraint(p, "implies clause");
}
Expand Down Expand Up @@ -412,7 +412,7 @@ namespace sat {

if (k == 1 && p.lit() == null_literal) {
literal_vector lits(sz, p.literals().c_ptr());
s().mk_clause(sz, lits.c_ptr(), status::ba(p.learned()));
s().mk_clause(sz, lits.c_ptr(), status::th(p.learned(), get_id()));
remove_constraint(p, "is clause");
return;
}
Expand Down Expand Up @@ -795,7 +795,7 @@ namespace sat {

else if (k == 1 && p.lit() == null_literal) {
literal_vector lits(sz, p.literals().c_ptr());
s().mk_clause(sz, lits.c_ptr(), status::ba(p.learned()));
s().mk_clause(sz, lits.c_ptr(), status::th(p.learned(), get_id()));
remove_constraint(p, "recompiled to clause");
return;
}
Expand Down Expand Up @@ -1598,7 +1598,7 @@ namespace sat {
TRACE("ba", tout << m_lemma << "\n";);

if (get_config().m_drat && m_solver) {
s().m_drat.add(m_lemma, sat::status::ba(true));
s().m_drat.add(m_lemma, sat::status::th(true, get_id()));
}

s().m_lemma.reset();
Expand Down Expand Up @@ -1750,7 +1750,7 @@ namespace sat {
ba_solver::constraint* ba_solver::add_at_least(literal lit, literal_vector const& lits, unsigned k, bool learned) {
if (k == 1 && lit == null_literal) {
literal_vector _lits(lits);
s().mk_clause(_lits.size(), _lits.c_ptr(), status::ba(learned));
s().mk_clause(_lits.size(), _lits.c_ptr(), status::th(learned, get_id()));
return nullptr;
}
if (!learned && clausify(lit, lits.size(), lits.c_ptr(), k)) {
Expand Down Expand Up @@ -2140,7 +2140,7 @@ namespace sat {
for (literal lit : r)
lits.push_back(~lit);
lits.push_back(l);
s().m_drat.add(lits, sat::status::ba(true));
s().m_drat.add(lits, sat::status::th(true, get_id()));
}
}

Expand Down Expand Up @@ -2899,35 +2899,35 @@ namespace sat {

if (k == 1 && c.lit() == null_literal) {
literal_vector lits(sz, c.literals().c_ptr());
s().mk_clause(sz, lits.c_ptr(), sat::status::ba(c.learned()));
s().mk_clause(sz, lits.c_ptr(), sat::status::th(c.learned(), get_id()));
remove_constraint(c, "recompiled to clause");
return;
}

if (sz == 0) {
if (c.lit() == null_literal) {
if (k > 0) {
s().mk_clause(0, nullptr, status::ba_asserted());
s().mk_clause(0, nullptr, status::th(false, get_id()));
}
}
else if (k > 0) {
literal lit = ~c.lit();
s().mk_clause(1, &lit, status::ba(c.learned()));
s().mk_clause(1, &lit, status::th(c.learned(), get_id()));
}
else {
literal lit = c.lit();
s().mk_clause(1, &lit, status::ba(c.learned()));
s().mk_clause(1, &lit, status::th(c.learned(), get_id()));
}
remove_constraint(c, "recompiled to clause");
return;
}
if (all_units && sz < k) {
if (c.lit() == null_literal) {
s().mk_clause(0, nullptr, status::ba(c.learned()));
s().mk_clause(0, nullptr, status::th(c.learned(), get_id()));
}
else {
literal lit = ~c.lit();
s().mk_clause(1, &lit, status::ba(c.learned()));
s().mk_clause(1, &lit, status::th(c.learned(), get_id()));
}
remove_constraint(c, "recompiled to clause");
return;
Expand Down
75 changes: 75 additions & 0 deletions src/sat/smt/bv_internalize.cpp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
bv_internalize.cpp
Abstract:
Internalize utilities for bit-vector solver plugin.
Author:
Nikolaj Bjorner (nbjorner) 2020-08-30
--*/

#include "sat/smt/bv_solver.h"
#include "sat/smt/euf_solver.h"
#include "sat/smt/sat_th.h"
#include "tactic/tactic_exception.h"

namespace bv {

euf::theory_var solver::mk_var(euf::enode* n) {
theory_var r = euf::th_euf_solver::mk_var(n);
m_find.mk_var();
m_bits.push_back(sat::literal_vector());
m_wpos.push_back(0);
m_zero_one_bits.push_back(zero_one_bits());
ctx.attach_th_var(n, this, r);
return r;
}

sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
flet<bool> _is_learned(m_is_redundant, learned);
sat::scoped_stack _sc(m_stack);
unsigned sz = m_stack.size();
visit(e);
while (m_stack.size() > sz) {
loop:
if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
sat::eframe & fr = m_stack.back();
expr* e = fr.m_e;
if (visited(e)) {
m_stack.pop_back();
continue;
}
unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;

while (fr.m_idx < num) {
expr* arg = to_app(e)->get_arg(fr.m_idx);
fr.m_idx++;
visit(arg);
if (!visited(arg))
goto loop;
}
visit(e);
SASSERT(visited(e));
m_stack.pop_back();
}
SASSERT(visited(e));
return sat::null_literal;
}

bool solver::visit(expr* e) {
return false;
}

bool solver::visited(expr* e) {
return false;
}

}
Loading

0 comments on commit d83d0a8

Please sign in to comment.