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

abstract solver API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-06 19:42:01 +01:00
parent 9cf99e26a6
commit d04e72819a
11 changed files with 237 additions and 110 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/CMakeLists.txt
View file

@ -19,6 +19,7 @@ z3_add_component(rewriter
factor_equivs.cpp factor_equivs.cpp
factor_rewriter.cpp factor_rewriter.cpp
fpa_rewriter.cpp fpa_rewriter.cpp
hoist_rewriter.cpp
inj_axiom.cpp inj_axiom.cpp
label_rewriter.cpp label_rewriter.cpp
maximize_ac_sharing.cpp maximize_ac_sharing.cpp

6
src/sat/sat_solver.cpp
View file

@ -34,7 +34,7 @@ Revision History:
namespace sat { namespace sat {
solver::solver(params_ref const & p, reslimit& l): solver::solver(params_ref const & p, reslimit& l):
m_rlimit(l), solver_core(l),
m_checkpoint_enabled(true), m_checkpoint_enabled(true),
m_config(p), m_config(p),
m_par(nullptr), m_par(nullptr),
@ -3328,7 +3328,7 @@ namespace sat {
bool_var solver::max_var(bool learned, bool_var v) { bool_var solver::max_var(bool learned, bool_var v) {
m_user_bin_clauses.reset(); m_user_bin_clauses.reset();
collect_bin_clauses(m_user_bin_clauses, learned); collect_bin_clauses(m_user_bin_clauses, learned, false);
for (unsigned i = 0; i < m_user_bin_clauses.size(); ++i) { for (unsigned i = 0; i < m_user_bin_clauses.size(); ++i) {
literal l1 = m_user_bin_clauses[i].first; literal l1 = m_user_bin_clauses[i].first;
literal l2 = m_user_bin_clauses[i].second; literal l2 = m_user_bin_clauses[i].second;
@ -3827,7 +3827,7 @@ namespace sat {
max_cliques<neg_literal> mc; max_cliques<neg_literal> mc;
m_user_bin_clauses.reset(); m_user_bin_clauses.reset();
m_binary_clause_graph.reset(); m_binary_clause_graph.reset();
collect_bin_clauses(m_user_bin_clauses, true); collect_bin_clauses(m_user_bin_clauses, true, false);
hashtable<literal_pair, pair_hash<literal_hash, literal_hash>, default_eq<literal_pair> > seen_bc; hashtable<literal_pair, pair_hash<literal_hash, literal_hash>, default_eq<literal_pair> > seen_bc;
for (auto const& b : m_user_bin_clauses) { for (auto const& b : m_user_bin_clauses) {
literal l1 = b.first; literal l1 = b.first;

63
src/sat/sat_solver.h
View file

@ -37,6 +37,7 @@ Revision History:
#include "sat/sat_drat.h" #include "sat/sat_drat.h"
#include "sat/sat_parallel.h" #include "sat/sat_parallel.h"
#include "sat/sat_local_search.h" #include "sat/sat_local_search.h"
#include "sat/sat_solver_core.h"
#include "util/params.h" #include "util/params.h"
#include "util/statistics.h" #include "util/statistics.h"
#include "util/stopwatch.h" #include "util/stopwatch.h"
@ -75,11 +76,10 @@ namespace sat {
void collect_statistics(statistics & st) const; void collect_statistics(statistics & st) const;
}; };
class solver { class solver : public solver_core {
public: public:
struct abort_solver {}; struct abort_solver {};
protected: protected:
reslimit& m_rlimit;
bool m_checkpoint_enabled; bool m_checkpoint_enabled;
config m_config; config m_config;
stats m_stats; stats m_stats;
@ -197,12 +197,12 @@ namespace sat {
// Misc // Misc
// //
// ----------------------- // -----------------------
void updt_params(params_ref const & p); void updt_params(params_ref const & p) override;
static void collect_param_descrs(param_descrs & d); static void collect_param_descrs(param_descrs & d);
void collect_statistics(statistics & st) const; void collect_statistics(statistics & st) const override;
void reset_statistics(); void reset_statistics();
void display_status(std::ostream & out) const; void display_status(std::ostream & out) const override;
/** /**
\brief Copy (non learned) clauses from src to this solver. \brief Copy (non learned) clauses from src to this solver.
@ -217,6 +217,9 @@ namespace sat {
// Variable & Clause creation // Variable & Clause creation
// //
// ----------------------- // -----------------------
void add_clause(unsigned num_lits, literal * lits, bool learned) override { mk_clause(num_lits, lits, learned); }
bool_var add_var(bool ext) override { return mk_var(ext, true); }
bool_var mk_var(bool ext = false, bool dvar = true); bool_var mk_var(bool ext = false, bool dvar = true);
void mk_clause(literal_vector const& lits, bool learned = false) { mk_clause(lits.size(), lits.c_ptr(), learned); } void mk_clause(literal_vector const& lits, bool learned = false) { mk_clause(lits.size(), lits.c_ptr(), learned); }
void mk_clause(unsigned num_lits, literal * lits, bool learned = false); void mk_clause(unsigned num_lits, literal * lits, bool learned = false);
@ -279,29 +282,28 @@ namespace sat {
// //
// ----------------------- // -----------------------
public: public:
bool inconsistent() const { return m_inconsistent; } bool inconsistent() const override { return m_inconsistent; }
unsigned num_vars() const { return m_level.size(); } unsigned num_vars() const override { return m_level.size(); }
unsigned num_clauses() const; unsigned num_clauses() const override;
void num_binary(unsigned& given, unsigned& learned) const; void num_binary(unsigned& given, unsigned& learned) const;
unsigned num_restarts() const { return m_restarts; } unsigned num_restarts() const { return m_restarts; }
bool is_external(bool_var v) const { return m_external[v] != 0; } bool is_external(bool_var v) const override { return m_external[v] != 0; }
bool is_external(literal l) const { return is_external(l.var()); } void set_external(bool_var v) override;
void set_external(bool_var v); void set_non_external(bool_var v) override;
void set_non_external(bool_var v);
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
void set_eliminated(bool_var v, bool f) { m_eliminated[v] = f; } void set_eliminated(bool_var v, bool f) override { m_eliminated[v] = f; }
bool was_eliminated(literal l) const { return was_eliminated(l.var()); } bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
unsigned scope_lvl() const { return m_scope_lvl; } unsigned scope_lvl() const { return m_scope_lvl; }
unsigned search_lvl() const { return m_search_lvl; } unsigned search_lvl() const { return m_search_lvl; }
bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
bool at_base_lvl() const { return m_scope_lvl == 0; } bool at_base_lvl() const override { return m_scope_lvl == 0; }
lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); } lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }
lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); } lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
unsigned lvl(bool_var v) const { return m_level[v]; } unsigned lvl(bool_var v) const { return m_level[v]; }
unsigned lvl(literal l) const { return m_level[l.var()]; } unsigned lvl(literal l) const { return m_level[l.var()]; }
unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
unsigned trail_size() const { return m_trail.size(); } unsigned trail_size() const { return m_trail.size(); }
literal trail_literal(unsigned i) const { return m_trail[i]; } literal trail_literal(unsigned i) const override { return m_trail[i]; }
literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; } literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; }
void assign(literal l, justification j) { void assign(literal l, justification j) {
TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";); TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
@ -333,8 +335,8 @@ namespace sat {
config const& get_config() const { return m_config; } config const& get_config() const { return m_config; }
void set_incremental(bool b) { m_config.m_incremental = b; } void set_incremental(bool b) { m_config.m_incremental = b; }
bool is_incremental() const { return m_config.m_incremental; } bool is_incremental() const { return m_config.m_incremental; }
extension* get_extension() const { return m_ext.get(); } extension* get_extension() const override { return m_ext.get(); }
void set_extension(extension* e); void set_extension(extension* e) override;
bool set_root(literal l, literal r); bool set_root(literal l, literal r);
void flush_roots(); void flush_roots();
typedef std::pair<literal, literal> bin_clause; typedef std::pair<literal, literal> bin_clause;
@ -369,13 +371,13 @@ namespace sat {
// //
// ----------------------- // -----------------------
public: public:
lbool check(unsigned num_lits = 0, literal const* lits = nullptr); lbool check(unsigned num_lits = 0, literal const* lits = nullptr) override;
model const & get_model() const { return m_model; } model const & get_model() const override { return m_model; }
bool model_is_current() const { return m_model_is_current; } bool model_is_current() const { return m_model_is_current; }
literal_vector const& get_core() const { return m_core; } literal_vector const& get_core() const override { return m_core; }
model_converter const & get_model_converter() const { return m_mc; } model_converter const & get_model_converter() const { return m_mc; }
void flush(model_converter& mc) { mc.flush(m_mc); } void flush(model_converter& mc) override { mc.flush(m_mc); }
void set_model(model const& mdl); void set_model(model const& mdl);
char const* get_reason_unknown() const { return m_reason_unknown.c_str(); } char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
bool check_clauses(model const& m) const; bool check_clauses(model const& m) const;
@ -545,10 +547,10 @@ namespace sat {
bool_var max_var(bool learned, bool_var v); bool_var max_var(bool learned, bool_var v);
public: public:
void user_push(); void user_push() override;
void user_pop(unsigned num_scopes); void user_pop(unsigned num_scopes) override;
void pop_to_base_level(); void pop_to_base_level() override;
unsigned num_user_scopes() const { return m_user_scope_literals.size(); } unsigned num_user_scopes() const override { return m_user_scope_literals.size(); }
reslimit& rlimit() { return m_rlimit; } reslimit& rlimit() { return m_rlimit; }
// ----------------------- // -----------------------
// //
@ -645,8 +647,9 @@ namespace sat {
clause * const * begin_learned() const { return m_learned.begin(); } clause * const * begin_learned() const { return m_learned.begin(); }
clause * const * end_learned() const { return m_learned.end(); } clause * const * end_learned() const { return m_learned.end(); }
clause_vector const& learned() const { return m_learned; } clause_vector const& learned() const { return m_learned; }
clause_vector const& clauses() const { return m_clauses; } clause_vector const& clauses() const override { return m_clauses; }
void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only = false) const; void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const override;
// ----------------------- // -----------------------
// //
@ -654,11 +657,11 @@ namespace sat {
// //
// ----------------------- // -----------------------
public: public:
bool check_invariant() const; bool check_invariant() const override;
void display(std::ostream & out) const; void display(std::ostream & out) const;
void display_watches(std::ostream & out) const; void display_watches(std::ostream & out) const;
void display_watches(std::ostream & out, literal lit) const; void display_watches(std::ostream & out, literal lit) const;
void display_dimacs(std::ostream & out) const; void display_dimacs(std::ostream & out) const override;
void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const; void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const;
void display_assignment(std::ostream & out) const; void display_assignment(std::ostream & out) const;
std::ostream& display_justification(std::ostream & out, justification const& j) const; std::ostream& display_justification(std::ostream & out, justification const& j) const;

116
src/sat/sat_solver_core.h Normal file
View file

@ -0,0 +1,116 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
sat_solver_core.h
Abstract:
SAT solver API class.
Author:
Nikolaj Bjorner (nbjorner) 2019-02-06
Revision History:
--*/
#ifndef SAT_SOLVER_CORE_H_
#define SAT_SOLVER_CORE_H_
#include "sat/sat_types.h"
namespace sat {
class solver_core {
protected:
reslimit& m_rlimit;
public:
solver_core(reslimit& l) : m_rlimit(l) {}
~solver_core() {}
virtual void pop_to_base_level() {}
virtual bool at_base_lvl() const { return true; }
// retrieve model if solver return sat
virtual model const & get_model() const = 0;
// retrieve core from assumptions
virtual literal_vector const& get_core() const = 0;
// is the state inconsistent?
virtual bool inconsistent() const = 0;
// number of variables and clauses
virtual unsigned num_vars() const = 0;
virtual unsigned num_clauses() const = 0;
// check satisfiability
virtual lbool check(unsigned num_lits = 0, literal const* lits = nullptr) = 0;
// add clauses
virtual void add_clause(unsigned n, literal* lits, bool is_redundant) = 0;
void add_clause(literal l1, literal l2, bool is_redundant) {
literal lits[2] = {l1, l2};
add_clause(2, lits, is_redundant);
}
void add_clause(literal l1, literal l2, literal l3, bool is_redundant) {
literal lits[3] = {l1, l2, l3};
add_clause(3, lits, is_redundant);
}
// create boolean variable, tagged as external (= true) or internal (can be eliminated).
virtual bool_var add_var(bool ext) = 0;
// update parameters
virtual void updt_params(params_ref const& p) {}
virtual bool check_invariant() const { return true; }
virtual void display_status(std::ostream& out) const {}
virtual void display_dimacs(std::ostream& out) const {}
virtual bool is_external(bool_var v) const { return true; }
bool is_external(literal l) const { return is_external(l.var()); }
virtual void set_external(bool_var v) {}
virtual void set_non_external(bool_var v) {}
virtual void set_eliminated(bool_var v, bool f) {}
// optional support for user-scopes. Not relevant for sat_tactic integration.
// it is only relevant for incremental mode SAT, which isn't wrapped (yet)
virtual void user_push() { throw default_exception("optional API not supported"); }
virtual void user_pop(unsigned num_scopes) {};
virtual unsigned num_user_scopes() const { return 0;}
// hooks for extension solver. really just ba_solver atm.
virtual extension* get_extension() const { return nullptr; }
virtual void set_extension(extension* e) { if (e) throw default_exception("optional API not supported"); }
// The following methods are used when converting the state from the SAT solver back
// to a set of assertions.
// retrieve model converter that handles variable elimination and other transformations
virtual void flush(model_converter& mc) {}
// size of initial trail containing unit clauses
virtual unsigned init_trail_size() const = 0;
// literal at trail index i
virtual literal trail_literal(unsigned i) const = 0;
// collect n-ary clauses
virtual clause_vector const& clauses() const = 0;
// collect binary clauses
typedef std::pair<literal, literal> bin_clause;
virtual void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const = 0;
// collect statistics from sat solver
virtual void collect_statistics(statistics & st) const {}
};
};
#endif

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

@ -57,7 +57,7 @@ struct goal2sat::imp {
svector<sat::literal> m_result_stack; svector<sat::literal> m_result_stack;
obj_map<app, sat::literal> m_cache; obj_map<app, sat::literal> m_cache;
obj_hashtable<expr> m_interface_vars; obj_hashtable<expr> m_interface_vars;
sat::solver & m_solver; sat::solver_core & m_solver;
atom2bool_var & m_map; atom2bool_var & m_map;
dep2asm_map & m_dep2asm; dep2asm_map & m_dep2asm;
sat::bool_var m_true; sat::bool_var m_true;
@ -69,7 +69,7 @@ struct goal2sat::imp {
bool m_xor_solver; bool m_xor_solver;
bool m_is_lemma; bool m_is_lemma;
imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external): imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
m(_m), m(_m),
pb(m), pb(m),
m_ext(nullptr), m_ext(nullptr),
@ -97,30 +97,30 @@ struct goal2sat::imp {
void mk_clause(sat::literal l) { void mk_clause(sat::literal l) {
TRACE("goal2sat", tout << "mk_clause: " << l << "\n";); TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
m_solver.mk_clause(1, &l); m_solver.add_clause(1, &l, false);
} }
void set_lemma_mode(bool f) { m_is_lemma = f; } void set_lemma_mode(bool f) { m_is_lemma = f; }
void mk_clause(sat::literal l1, sat::literal l2) { void mk_clause(sat::literal l1, sat::literal l2) {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";); TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
m_solver.mk_clause(l1, l2, m_is_lemma); m_solver.add_clause(l1, l2, m_is_lemma);
} }
void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) { void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";); TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
m_solver.mk_clause(l1, l2, l3, m_is_lemma); m_solver.add_clause(l1, l2, l3, m_is_lemma);
} }
void mk_clause(unsigned num, sat::literal * lits) { void mk_clause(unsigned num, sat::literal * lits) {
TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";); TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
m_solver.mk_clause(num, lits, m_is_lemma); m_solver.add_clause(num, lits, m_is_lemma);
} }
sat::bool_var mk_true() { sat::bool_var mk_true() {
if (m_true == sat::null_bool_var) { if (m_true == sat::null_bool_var) {
// create fake variable to represent true; // create fake variable to represent true;
m_true = m_solver.mk_var(false); m_true = m_solver.add_var(false);
mk_clause(sat::literal(m_true, false)); // v is true mk_clause(sat::literal(m_true, false)); // v is true
} }
return m_true; return m_true;
@ -139,7 +139,7 @@ struct goal2sat::imp {
} }
else { else {
bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t); bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
sat::bool_var v = m_solver.mk_var(ext); sat::bool_var v = m_solver.add_var(ext);
m_map.insert(t, v); m_map.insert(t, v);
l = sat::literal(v, sign); l = sat::literal(v, sign);
TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";); TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";);
@ -247,7 +247,7 @@ struct goal2sat::imp {
} }
else { else {
SASSERT(num <= m_result_stack.size()); SASSERT(num <= m_result_stack.size());
sat::bool_var k = m_solver.mk_var(); sat::bool_var k = m_solver.add_var(false);
sat::literal l(k, false); sat::literal l(k, false);
m_cache.insert(t, l); m_cache.insert(t, l);
sat::literal * lits = m_result_stack.end() - num; sat::literal * lits = m_result_stack.end() - num;
@ -286,7 +286,7 @@ struct goal2sat::imp {
} }
else { else {
SASSERT(num <= m_result_stack.size()); SASSERT(num <= m_result_stack.size());
sat::bool_var k = m_solver.mk_var(); sat::bool_var k = m_solver.add_var(false);
sat::literal l(k, false); sat::literal l(k, false);
m_cache.insert(t, l); m_cache.insert(t, l);
// l => /\ lits // l => /\ lits
@ -329,7 +329,7 @@ struct goal2sat::imp {
m_result_stack.reset(); m_result_stack.reset();
} }
else { else {
sat::bool_var k = m_solver.mk_var(); sat::bool_var k = m_solver.add_var(false);
sat::literal l(k, false); sat::literal l(k, false);
m_cache.insert(n, l); m_cache.insert(n, l);
mk_clause(~l, ~c, t); mk_clause(~l, ~c, t);
@ -366,7 +366,7 @@ struct goal2sat::imp {
m_result_stack.reset(); m_result_stack.reset();
} }
else { else {
sat::bool_var k = m_solver.mk_var(); sat::bool_var k = m_solver.add_var(false);
sat::literal l(k, false); sat::literal l(k, false);
m_cache.insert(t, l); m_cache.insert(t, l);
mk_clause(~l, l1, ~l2); mk_clause(~l, l1, ~l2);
@ -390,7 +390,7 @@ struct goal2sat::imp {
return; return;
} }
sat::literal_vector lits; sat::literal_vector lits;
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = m_solver.add_var(true);
lits.push_back(sat::literal(v, true)); lits.push_back(sat::literal(v, true));
convert_pb_args(num, lits); convert_pb_args(num, lits);
// ensure that = is converted to xor // ensure that = is converted to xor
@ -472,7 +472,7 @@ struct goal2sat::imp {
m_ext->add_pb_ge(sat::null_bool_var, wlits, k1); m_ext->add_pb_ge(sat::null_bool_var, wlits, k1);
} }
else { else {
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = m_solver.add_var(true);
sat::literal lit(v, sign); sat::literal lit(v, sign);
m_ext->add_pb_ge(v, wlits, k.get_unsigned()); m_ext->add_pb_ge(v, wlits, k.get_unsigned());
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
@ -503,7 +503,7 @@ struct goal2sat::imp {
m_ext->add_pb_ge(sat::null_bool_var, wlits, k1); m_ext->add_pb_ge(sat::null_bool_var, wlits, k1);
} }
else { else {
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = m_solver.add_var(true);
sat::literal lit(v, sign); sat::literal lit(v, sign);
m_ext->add_pb_ge(v, wlits, k.get_unsigned()); m_ext->add_pb_ge(v, wlits, k.get_unsigned());
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
@ -518,8 +518,8 @@ struct goal2sat::imp {
svector<wliteral> wlits; svector<wliteral> wlits;
convert_pb_args(t, wlits); convert_pb_args(t, wlits);
bool base_assert = (root && !sign && m_solver.num_user_scopes() == 0); bool base_assert = (root && !sign && m_solver.num_user_scopes() == 0);
sat::bool_var v1 = base_assert ? sat::null_bool_var : m_solver.mk_var(true); 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.mk_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()); m_ext->add_pb_ge(v1, wlits, k.get_unsigned());
k.neg(); k.neg();
for (wliteral& wl : wlits) { for (wliteral& wl : wlits) {
@ -533,7 +533,7 @@ struct goal2sat::imp {
} }
else { else {
sat::literal l1(v1, false), l2(v2, false); sat::literal l1(v1, false), l2(v2, false);
sat::bool_var v = m_solver.mk_var(); sat::bool_var v = m_solver.add_var(false);
sat::literal l(v, false); sat::literal l(v, false);
mk_clause(~l, l1); mk_clause(~l, l1);
mk_clause(~l, l2); mk_clause(~l, l2);
@ -553,7 +553,7 @@ struct goal2sat::imp {
m_ext->add_at_least(sat::null_bool_var, lits, k.get_unsigned()); m_ext->add_at_least(sat::null_bool_var, lits, k.get_unsigned());
} }
else { else {
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = m_solver.add_var(true);
sat::literal lit(v, false); sat::literal lit(v, false);
m_ext->add_at_least(v, lits, k.get_unsigned()); m_ext->add_at_least(v, lits, k.get_unsigned());
m_cache.insert(t, lit); m_cache.insert(t, lit);
@ -575,7 +575,7 @@ struct goal2sat::imp {
m_ext->add_at_least(sat::null_bool_var, lits, lits.size() - k.get_unsigned()); m_ext->add_at_least(sat::null_bool_var, lits, lits.size() - k.get_unsigned());
} }
else { else {
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = m_solver.add_var(true);
sat::literal lit(v, false); sat::literal lit(v, false);
m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned()); m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned());
m_cache.insert(t, lit); m_cache.insert(t, lit);
@ -588,8 +588,8 @@ struct goal2sat::imp {
SASSERT(k.is_unsigned()); SASSERT(k.is_unsigned());
sat::literal_vector lits; sat::literal_vector lits;
convert_pb_args(t->get_num_args(), lits); convert_pb_args(t->get_num_args(), lits);
sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true); 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.mk_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()); m_ext->add_at_least(v1, lits, k.get_unsigned());
for (sat::literal& l : lits) { for (sat::literal& l : lits) {
l.neg(); l.neg();
@ -602,7 +602,7 @@ struct goal2sat::imp {
} }
else { else {
sat::literal l1(v1, false), l2(v2, false); sat::literal l1(v1, false), l2(v2, false);
sat::bool_var v = m_solver.mk_var(); sat::bool_var v = m_solver.add_var(false);
sat::literal l(v, false); sat::literal l(v, false);
mk_clause(~l, l1); mk_clause(~l, l1);
mk_clause(~l, l2); mk_clause(~l, l2);
@ -897,7 +897,7 @@ struct goal2sat::scoped_set_imp {
}; };
void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external, bool is_lemma) { void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external, bool is_lemma) {
imp proc(g.m(), p, t, m, dep2asm, default_external); imp proc(g.m(), p, t, m, dep2asm, default_external);
scoped_set_imp set(this, &proc); scoped_set_imp set(this, &proc);
proc.set_lemma_mode(is_lemma); proc.set_lemma_mode(is_lemma);
@ -916,7 +916,7 @@ void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) {
sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {} sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {}
void sat2goal::mc::flush_smc(sat::solver& s, atom2bool_var const& map) { void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) {
s.flush(m_smc); s.flush(m_smc);
m_var2expr.resize(s.num_vars()); m_var2expr.resize(s.num_vars());
map.mk_var_inv(m_var2expr); map.mk_var_inv(m_var2expr);
@ -1157,13 +1157,14 @@ struct sat2goal::imp {
r.assert_expr(fml); r.assert_expr(fml);
} }
void assert_clauses(ref<mc>& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { void assert_clauses(ref<mc>& mc, sat::solver_core const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
ptr_buffer<expr> lits; ptr_buffer<expr> lits;
unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd;
for (sat::clause* cp : clauses) { for (sat::clause* cp : clauses) {
checkpoint(); checkpoint();
lits.reset(); lits.reset();
sat::clause const & c = *cp; sat::clause const & c = *cp;
if (asserted || m_learned || c.glue() <= s.get_config().m_gc_small_lbd) { if (asserted || m_learned || c.glue() <= small_lbd) {
for (sat::literal l : c) { for (sat::literal l : c) {
lits.push_back(lit2expr(mc, l)); lits.push_back(lit2expr(mc, l));
} }
@ -1172,11 +1173,11 @@ struct sat2goal::imp {
} }
} }
sat::ba_solver* get_ba_solver(sat::solver const& s) { sat::ba_solver* get_ba_solver(sat::solver_core const& s) {
return dynamic_cast<sat::ba_solver*>(s.get_extension()); return dynamic_cast<sat::ba_solver*>(s.get_extension());
} }
void operator()(sat::solver & s, atom2bool_var const & map, goal & r, ref<mc> & mc) { void operator()(sat::solver_core & s, atom2bool_var const & map, goal & r, ref<mc> & mc) {
if (s.at_base_lvl() && s.inconsistent()) { if (s.at_base_lvl() && s.inconsistent()) {
r.assert_expr(m.mk_false()); r.assert_expr(m.mk_false());
return; return;
@ -1196,7 +1197,7 @@ struct sat2goal::imp {
// collect binary clauses // collect binary clauses
svector<sat::solver::bin_clause> bin_clauses; svector<sat::solver::bin_clause> bin_clauses;
s.collect_bin_clauses(bin_clauses, m_learned); s.collect_bin_clauses(bin_clauses, m_learned, false);
for (sat::solver::bin_clause const& bc : bin_clauses) { for (sat::solver::bin_clause const& bc : bin_clauses) {
checkpoint(); checkpoint();
r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second))); r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second)));
@ -1262,7 +1263,7 @@ struct sat2goal::scoped_set_imp {
} }
}; };
void sat2goal::operator()(sat::solver & t, atom2bool_var const & m, params_ref const & p, void sat2goal::operator()(sat::solver_core & t, atom2bool_var const & m, params_ref const & p,
goal & g, ref<mc> & mc) { goal & g, ref<mc> & mc) {
imp proc(g.m(), p); imp proc(g.m(), p);
scoped_set_imp set(this, &proc); scoped_set_imp set(this, &proc);

6
src/sat/tactic/goal2sat.h
View file

@ -62,7 +62,7 @@ public:
\warning conversion throws a tactic_exception, if it is interrupted (by set_cancel), \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory). an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory).
*/ */
void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false, bool is_lemma = false); void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false, bool is_lemma = false);
void get_interpreted_atoms(expr_ref_vector& atoms); void get_interpreted_atoms(expr_ref_vector& atoms);
@ -88,7 +88,7 @@ public:
mc(ast_manager& m); mc(ast_manager& m);
~mc() override {} ~mc() override {}
// flush model converter from SAT solver to this structure. // flush model converter from SAT solver to this structure.
void flush_smc(sat::solver& s, atom2bool_var const& map); void flush_smc(sat::solver_core& s, atom2bool_var const& map);
void operator()(model_ref& md) override; void operator()(model_ref& md) override;
void operator()(expr_ref& fml) override; void operator()(expr_ref& fml) override;
model_converter* translate(ast_translation& translator) override; model_converter* translate(ast_translation& translator) override;
@ -113,7 +113,7 @@ public:
\warning conversion throws a tactic_exception, if it is interrupted (by set_cancel), \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
or memory consumption limit is reached (set with param :max-memory). or memory consumption limit is reached (set with param :max-memory).
*/ */
void operator()(sat::solver & t, atom2bool_var const & m, params_ref const & p, goal & s, ref<mc> & mc); void operator()(sat::solver_core & t, atom2bool_var const & m, params_ref const & p, goal & s, ref<mc> & mc);
}; };

28
src/sat/tactic/sat_tactic.cpp
View file

@ -29,12 +29,12 @@ class sat_tactic : public tactic {
ast_manager & m; ast_manager & m;
goal2sat m_goal2sat; goal2sat m_goal2sat;
sat2goal m_sat2goal; sat2goal m_sat2goal;
sat::solver m_solver; scoped_ptr<sat::solver_core> m_solver;
params_ref m_params; params_ref m_params;
imp(ast_manager & _m, params_ref const & p): imp(ast_manager & _m, params_ref const & p):
m(_m), m(_m),
m_solver(p, m.limit()), m_solver(alloc(sat::solver, p, m.limit())),
m_params(p) { m_params(p) {
SASSERT(!m.proofs_enabled()); SASSERT(!m.proofs_enabled());
updt_params(p); updt_params(p);
@ -51,7 +51,7 @@ class sat_tactic : public tactic {
atom2bool_var map(m); atom2bool_var map(m);
obj_map<expr, sat::literal> dep2asm; obj_map<expr, sat::literal> dep2asm;
sat::literal_vector assumptions; sat::literal_vector assumptions;
m_goal2sat(*g, m_params, m_solver, map, dep2asm); m_goal2sat(*g, m_params, *m_solver, map, dep2asm);
TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n"; TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n";
for (auto const& kv : map) { for (auto const& kv : map) {
if (!is_uninterp_const(kv.m_key)) if (!is_uninterp_const(kv.m_key))
@ -60,15 +60,15 @@ class sat_tactic : public tactic {
g->reset(); g->reset();
g->m().compact_memory(); g->m().compact_memory();
CASSERT("sat_solver", m_solver.check_invariant()); CASSERT("sat_solver", m_solver->check_invariant());
IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream());); IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver->display_status(verbose_stream()););
TRACE("sat_dimacs", m_solver.display_dimacs(tout);); TRACE("sat_dimacs", m_solver->display_dimacs(tout););
dep2assumptions(dep2asm, assumptions); dep2assumptions(dep2asm, assumptions);
lbool r = m_solver.check(assumptions.size(), assumptions.c_ptr()); lbool r = m_solver->check(assumptions.size(), assumptions.c_ptr());
if (r == l_false) { if (r == l_false) {
expr_dependency * lcore = nullptr; expr_dependency * lcore = nullptr;
if (produce_core) { if (produce_core) {
sat::literal_vector const& ucore = m_solver.get_core(); sat::literal_vector const& ucore = m_solver->get_core();
u_map<expr*> asm2dep; u_map<expr*> asm2dep;
mk_asm2dep(dep2asm, asm2dep); mk_asm2dep(dep2asm, asm2dep);
for (unsigned i = 0; i < ucore.size(); ++i) { for (unsigned i = 0; i < ucore.size(); ++i) {
@ -83,7 +83,7 @@ class sat_tactic : public tactic {
// register model // register model
if (produce_models) { if (produce_models) {
model_ref md = alloc(model, m); model_ref md = alloc(model, m);
sat::model const & ll_m = m_solver.get_model(); sat::model const & ll_m = m_solver->get_model();
TRACE("sat_tactic", for (unsigned i = 0; i < ll_m.size(); i++) tout << i << ":" << ll_m[i] << " "; tout << "\n";); TRACE("sat_tactic", for (unsigned i = 0; i < ll_m.size(); i++) tout << i << ":" << ll_m[i] << " "; tout << "\n";);
for (auto const& kv : map) { for (auto const& kv : map) {
expr * n = kv.m_key; expr * n = kv.m_key;
@ -109,9 +109,9 @@ class sat_tactic : public tactic {
#if 0 #if 0
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constrains interpreted atoms, recovering formula from sat solver...\"\n";); IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constrains interpreted atoms, recovering formula from sat solver...\"\n";);
#endif #endif
m_solver.pop_to_base_level(); m_solver->pop_to_base_level();
ref<sat2goal::mc> mc; ref<sat2goal::mc> mc;
m_sat2goal(m_solver, map, m_params, *(g.get()), mc); m_sat2goal(*m_solver, map, m_params, *(g.get()), mc);
g->add(mc.get()); g->add(mc.get());
} }
g->inc_depth(); g->inc_depth();
@ -134,7 +134,7 @@ class sat_tactic : public tactic {
} }
void updt_params(params_ref const& p) { void updt_params(params_ref const& p) {
m_solver.updt_params(p); m_solver->updt_params(p);
} }
}; };
@ -192,10 +192,10 @@ public:
scoped_set_imp set(this, &proc); scoped_set_imp set(this, &proc);
try { try {
proc(g, result); proc(g, result);
proc.m_solver.collect_statistics(m_stats); proc.m_solver->collect_statistics(m_stats);
} }
catch (sat::solver_exception & ex) { catch (sat::solver_exception & ex) {
proc.m_solver.collect_statistics(m_stats); proc.m_solver->collect_statistics(m_stats);
throw tactic_exception(ex.msg()); throw tactic_exception(ex.msg());
} }
TRACE("sat_stats", m_stats.display_smt2(tout);); TRACE("sat_stats", m_stats.display_smt2(tout););

2
src/shell/dimacs_frontend.cpp
View file

@ -113,7 +113,7 @@ static void track_clauses(sat::solver const& src,
sat::clause * const * it = src.begin_clauses(); sat::clause * const * it = src.begin_clauses();
sat::clause * const * end = src.end_clauses(); sat::clause * const * end = src.end_clauses();
svector<sat::solver::bin_clause> bin_clauses; svector<sat::solver::bin_clause> bin_clauses;
src.collect_bin_clauses(bin_clauses, false); src.collect_bin_clauses(bin_clauses, false, false);
tracking_clauses.reserve(2*src.num_vars() + static_cast<unsigned>(end - it) + bin_clauses.size()); tracking_clauses.reserve(2*src.num_vars() + static_cast<unsigned>(end - it) + bin_clauses.size());
for (sat::bool_var v = 1; v < src.num_vars(); ++v) { for (sat::bool_var v = 1; v < src.num_vars(); ++v) {

31
src/smt/smt_cg_table.cpp
View file

@ -71,10 +71,7 @@ namespace smt {
void cg_table::display(std::ostream & out) const { void cg_table::display(std::ostream & out) const {
out << "congruence table:\n"; out << "congruence table:\n";
table::iterator it = m_table.begin(); for (enode * n : m_table) {
table::iterator end = m_table.end();
for (; it != end; ++it) {
enode * n = *it;
out << mk_pp(n->get_owner(), m_manager) << "\n"; out << mk_pp(n->get_owner(), m_manager) << "\n";
} }
} }
@ -82,10 +79,7 @@ namespace smt {
void cg_table::display_compact(std::ostream & out) const { void cg_table::display_compact(std::ostream & out) const {
if (!m_table.empty()) { if (!m_table.empty()) {
out << "congruence table:\n"; out << "congruence table:\n";
table::iterator it = m_table.begin(); for (enode * n : m_table) {
table::iterator end = m_table.end();
for (; it != end; ++it) {
enode * n = *it;
out << "#" << n->get_owner()->get_id() << " "; out << "#" << n->get_owner()->get_id() << " ";
} }
out << "\n"; out << "\n";
@ -94,10 +88,7 @@ namespace smt {
#ifdef Z3DEBUG #ifdef Z3DEBUG
bool cg_table::check_invariant() const { bool cg_table::check_invariant() const {
table::iterator it = m_table.begin(); for (enode * n : m_table) {
table::iterator end = m_table.end();
for (; it != end; ++it) {
enode * n = *it;
CTRACE("cg_table", !contains_ptr(n), tout << "#" << n->get_owner_id() << "\n";); CTRACE("cg_table", !contains_ptr(n), tout << "#" << n->get_owner_id() << "\n";);
SASSERT(contains_ptr(n)); SASSERT(contains_ptr(n));
} }
@ -136,9 +127,11 @@ namespace smt {
} }
bool cg_table::cg_eq::operator()(enode * n1, enode * n2) const { bool cg_table::cg_eq::operator()(enode * n1, enode * n2) const {
SASSERT(n1->get_num_args() == n2->get_num_args());
SASSERT(n1->get_decl() == n2->get_decl()); SASSERT(n1->get_decl() == n2->get_decl());
unsigned num = n1->get_num_args(); unsigned num = n1->get_num_args();
if (num != n2->get_num_args()) {
return false;
}
for (unsigned i = 0; i < num; i++) for (unsigned i = 0; i < num; i++)
if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root()) if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root())
return false; return false;
@ -205,10 +198,7 @@ namespace smt {
} }
void cg_table::reset() { void cg_table::reset() {
ptr_vector<void>::iterator it = m_tables.begin(); for (void* t : m_tables) {
ptr_vector<void>::iterator end = m_tables.end();
for (; it != end; ++it) {
void * t = *it;
switch (GET_TAG(t)) { switch (GET_TAG(t)) {
case UNARY: case UNARY:
dealloc(UNTAG(unary_table*, t)); dealloc(UNTAG(unary_table*, t));
@ -225,10 +215,9 @@ namespace smt {
} }
} }
m_tables.reset(); m_tables.reset();
obj_map<func_decl, unsigned>::iterator it2 = m_func_decl2id.begin(); for (auto const& kv : m_func_decl2id) {
obj_map<func_decl, unsigned>::iterator end2 = m_func_decl2id.end(); m_manager.dec_ref(kv.m_key);
for (; it2 != end2; ++it2) }
m_manager.dec_ref(it2->m_key);
m_func_decl2id.reset(); m_func_decl2id.reset();
} }

2
src/smt/smt_cg_table.h
View file

@ -252,6 +252,8 @@ namespace smt {
enode_bool_pair insert(enode * n) { enode_bool_pair insert(enode * n) {
// it doesn't make sense to insert a constant. // it doesn't make sense to insert a constant.
SASSERT(n->get_num_args() > 0); SASSERT(n->get_num_args() > 0);
SASSERT(!m_manager.is_and(n->get_owner()));
SASSERT(!m_manager.is_or(n->get_owner()));
enode * n_prime; enode * n_prime;
void * t = get_table(n); void * t = get_table(n);
switch (static_cast<table_kind>(GET_TAG(t))) { switch (static_cast<table_kind>(GET_TAG(t))) {

29
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -22,6 +22,9 @@ Revision History:
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/pb_decl_plugin.h" #include "ast/pb_decl_plugin.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/hoist_rewriter.h"
#include "tactic/goal_shared_occs.h" #include "tactic/goal_shared_occs.h"
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
@ -574,27 +577,36 @@ class solve_eqs_tactic : public tactic {
} }
else if (m().is_or(f)) { else if (m().is_or(f)) {
flatten_or(f, args); flatten_or(f, args);
//std::cout << "hoist or " << args.size() << "\n";
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
path.push_back(nnf_context(false, args, i)); path.push_back(nnf_context(false, args, i));
hoist_nnf(g, args.get(i), path, idx, depth + 1); hoist_nnf(g, args.get(i), path, idx, depth + 1);
path.pop_back(); path.pop_back();
} }
} }
else {
// std::cout << "no hoist " << mk_pp(f, m()) << "\n";
}
} }
bool collect_hoist(goal const& g) { void collect_hoist(goal const& g) {
bool change = false;
unsigned size = g.size(); unsigned size = g.size();
vector<nnf_context> path; vector<nnf_context> path;
for (unsigned idx = 0; idx < size; idx++) { for (unsigned idx = 0; idx < size; idx++) {
checkpoint(); checkpoint();
hoist_nnf(g, g.form(idx), path, idx, 0); hoist_nnf(g, g.form(idx), path, idx, 0);
} }
return change; }
void distribute_and_or(goal & g) {
unsigned size = g.size();
hoist_rewriter_star rw(m());
th_rewriter thrw(m());
expr_ref tmp(m()), tmp2(m());
for (unsigned idx = 0; idx < size; idx++) {
checkpoint();
expr* f = g.form(idx);
thrw(f, tmp);
rw(tmp, tmp2);
g.update(idx, tmp2);
}
} }
void sort_vars() { void sort_vars() {
@ -918,6 +930,9 @@ class solve_eqs_tactic : public tactic {
m_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs); m_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
m_norm_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs); m_norm_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
while (true) { while (true) {
if (m_context_solve) {
distribute_and_or(*(g.get()));
}
collect_num_occs(*g); collect_num_occs(*g);
collect(*g); collect(*g);
if (m_context_solve) { if (m_context_solve) {