mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

dbg

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-29 10:45:40 -07:00
parent a35d00e4c4
commit e9a4e486ae
6 changed files with 67 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/ba_solver.cpp
View file

@ -1734,6 +1734,7 @@ namespace sat {
: m_solver(nullptr), m_lookahead(nullptr),
m_constraint_id(0), m_ba(*this), m_sort(m_ba) {
TRACE("ba", tout << this << "\n";);
std::cout << "mk " << this << "\n";
m_num_propagations_since_pop = 0;
}

13
src/sat/smt/ba_solver.h
View file

@ -81,8 +81,17 @@ namespace sat {
public:
constraint(extension* e, tag_t t, unsigned id, literal l, unsigned sz, size_t osz):
index_base(e),
m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id), m_pure(false) {}
ext_constraint_idx index() const { return reinterpret_cast<ext_constraint_idx>(this); }
m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id), m_pure(false) {
std::cout << "constraint ext: " << t << " " << e << "\n";
size_t idx = reinterpret_cast<ext_constraint_idx>(this);
std::cout << "index " << idx << "\n";
std::cout << this << " " << index_base::from_index(idx) << "\n";
std::cout << e << " " << index_base::to_extension(idx) << "\n";
std::cout.flush();
}
ext_constraint_idx index() const {
return reinterpret_cast<ext_constraint_idx>(this);
}
unsigned id() const { return m_id; }
tag_t tag() const { return m_tag; }
literal lit() const { return m_lit; }

24
src/sat/smt/euf_solver.cpp
View file

@ -64,6 +64,7 @@ namespace euf {
m_internalizers.push_back(bai);
m_decompilers.push_back(alloc(sat::ba_decompile, *ba, s(), m));
ba->push_scopes(s().num_scopes());
std::cout << "extension ba " << ba << "\n";
return ba;
}
}
@ -72,6 +73,7 @@ namespace euf {
bool solver::propagate(literal l, ext_constraint_idx idx) {
auto* ext = sat::index_base::to_extension(idx);
std::cout << "extension " << ext << " " << idx << "\n";
SASSERT(ext != this);
return ext->propagate(l, idx);
}
@ -275,8 +277,12 @@ namespace euf {
sat::extension* solver::copy(sat::solver* s) {
auto* r = copy_core();
r->set_solver(s);
for (auto* e : m_extensions)
r->m_extensions.push_back(e->copy(s));
for (unsigned i = 0; i < m_id2extension.size(); ++i) {
auto* e = m_id2extension[i];
if (e)
r->add_extension(i, e->copy(s));
}
return r;
}
@ -284,8 +290,11 @@ namespace euf {
(void) learned;
auto* r = copy_core();
r->set_lookahead(s);
for (auto* e : m_extensions)
r->m_extensions.push_back(e->copy(s, learned));
for (unsigned i = 0; i < m_id2extension.size(); ++i) {
auto* e = m_id2extension[i];
if (e)
r->add_extension(i, e->copy(s, learned));
}
return r;
}
@ -378,6 +387,7 @@ namespace euf {
m_true = visit(m.mk_true());
m_false = visit(m.mk_false());
}
std::cout << mk_pp(e, m) << "\n";
SASSERT(!si.is_bool_op(e));
sat::scoped_stack _sc(m_stack);
unsigned sz = m_stack.size();
@ -417,6 +427,11 @@ namespace euf {
return n;
if (si.is_bool_op(e)) {
sat::literal lit = si.internalize(e);
enode_bool_pair bp(nullptr, false);
n = m_var2node.get(lit.var(), bp).first;
if (n)
return n;
n = m_egraph.mk(e, 0, nullptr);
attach_bool_var(lit.var(), lit.sign(), n);
if (!m.is_true(e) && !m.is_false(e))
@ -436,6 +451,7 @@ namespace euf {
expr* e = n->get_owner();
if (m.is_bool(e)) {
sat::bool_var v = si.add_bool_var(e);
std::cout << "attach " << v << "\n";
attach_bool_var(v, false, n);
}
}

7
src/sat/smt/sat_smt.h
View file

@ -19,6 +19,7 @@ Author:
#pragma once
#include "ast/ast.h"
#include "ast/ast_pp.h"
#include "sat/sat_solver.h"
namespace sat {
@ -50,9 +51,9 @@ namespace sat {
class index_base {
extension* ex;
public:
index_base(extension* e): ex(e) {}
static extension* to_extension(size_t s) { return from_index(s)->ex; }
index_base(extension* e) : ex(e) { to_index(); }
static extension* to_extension(size_t s) { std::cout << "to_extension: " << from_index(s) << " " << from_index(s)->ex << " " << s << "\n"; return from_index(s)->ex; }
static index_base* from_index(size_t s) { return reinterpret_cast<index_base*>(s); }
size_t to_index() const { return reinterpret_cast<size_t>(this); }
size_t to_index() const { std::cout << "to_index " << this << " " << ex << " " << reinterpret_cast<size_t>(this) << "\n"; return reinterpret_cast<size_t>(this); }
};
}

22
src/sat/smt/sat_th.h
View file

@ -60,5 +60,27 @@ namespace sat {
virtual bool include_func_interp(func_decl* f) const { return false; }
};
class th_solver : public extension, public th_model_builder, public th_decompile, public th_internalizer {
virtual ~th_solver() {}
/**
\brief compute the value for enode \c n and store the value in \c values
for the root of the class of \c n.
*/
virtual void add_value(euf::enode* n, expr_ref_vector& values) = 0;
/**
\brief compute dependencies for node n
*/
virtual void add_dep(euf::enode* n, top_sort<euf::enode>& dep) = 0;
/**
\brief should function be included in model.
*/
virtual bool include_func_interp(func_decl* f) const { return false; }
};
}

14
src/sat/tactic/goal2sat.cpp
View file

@ -95,6 +95,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_xor_solver = p.get_bool("xor_solver", false);
m_euf = false;
m_euf = true;
}
void throw_op_not_handled(std::string const& s) {
@ -194,7 +195,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
bool convert_app(app* t, bool root, bool sign) {
if (pb.is_pb(t)) {
if (!m_euf && pb.is_pb(t)) {
m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
return false;
}
@ -432,7 +433,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
void convert_iff(app * t, bool root, bool sign) {
TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_bounded_pp(t, m, 2) << "\n";);
if (is_xor(t))
if (!m_euf && is_xor(t))
convert_ba(t, root, sign);
else
convert_iff2(t, root, sign);
@ -443,6 +444,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
euf::solver* euf = nullptr;
if (!ext) {
euf = alloc(euf::solver, m, m_map, *this);
std::cout << "set euf\n";
m_solver.set_extension(euf);
for (unsigned i = m_solver.num_scopes(); i-- > 0; )
euf->push();
@ -464,6 +466,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
void convert_ba(app* t, bool root, bool sign) {
SASSERT(!m_euf);
std::cout << "convert ba\n";
sat::extension* ext = m_solver.get_extension();
sat::ba_solver* ba = nullptr;
if (!ext) {
@ -510,7 +514,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
SASSERT(!root || m_result_stack.empty());
}
else if (pb.is_pb(t)) {
else if (!m_euf && pb.is_pb(t)) {
convert_ba(t, root, sign);
}
else {
@ -571,7 +575,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
visit(t->get_arg(0), root, !sign);
continue;
}
if (is_xor(t)) {
if (!m_euf && is_xor(t)) {
convert_ba(t, root, sign);
m_frame_stack.pop_back();
continue;
@ -618,7 +622,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
return false;
}
}
else if (to_app(t)->get_family_id() == pb.get_family_id())
else if (!m_euf && to_app(t)->get_family_id() == pb.get_family_id())
return true;
else
return false;