mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

move to list of clauses

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-01 08:09:33 -07:00 • committed by Arie Gurfinkel
parent 502e323678
commit bfeb15b876
14 changed files with 104 additions and 83 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz/spacer/spacer_iuc_solver.cpp
View file

@ -128,8 +128,8 @@ lbool iuc_solver::check_sat (unsigned num_assumptions, expr * const *assumptions
}
lbool iuc_solver::check_sat_cc(const expr_ref_vector &cube,
const expr_ref_vector &clause) {
if (clause.empty()) {return check_sat(cube.size(), cube.c_ptr());}
vector<expr_ref_vector> const & clauses) {
if (clauses.empty()) {return check_sat(cube.size(), cube.c_ptr());}
// -- remove any old assumptions
if (m_assumptions.size() > m_first_assumption)
@ -144,7 +144,7 @@ lbool iuc_solver::check_sat_cc(const expr_ref_vector &cube,
m_is_proxied = mk_proxies(m_assumptions, m_first_assumption);
lbool res;
res = m_solver.check_sat_cc(m_assumptions, clause);
res = m_solver.check_sat_cc(m_assumptions, clauses);
set_status (res);
return res;
}

2
src/muz/spacer/spacer_iuc_solver.h
View file

@ -126,7 +126,7 @@ public:
{return m_solver.get_scope_level();}
lbool check_sat(unsigned num_assumptions, expr * const *assumptions) override;
lbool check_sat_cc(const expr_ref_vector &cube, const expr_ref_vector &clause) override;
lbool check_sat_cc(const expr_ref_vector &cube, vector<expr_ref_vector> const & clauses) override;
void set_progress_callback(progress_callback *callback) override
{m_solver.set_progress_callback(callback);}
unsigned get_num_assertions() const override

18
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -202,7 +202,7 @@ lbool prop_solver::mss(expr_ref_vector &hard, expr_ref_vector &soft) {
res = m_ctx->check_sat(j+1, hard.c_ptr());
if (res == l_false) {
// -- flip non-true literal to be false
hard[j] = m.mk_not(hard.get(j));
hard[j] = mk_not(m, hard.get(j));
}
else if (res == l_true) {
// -- get the model for the next iteration of the outer loop
@ -218,7 +218,7 @@ lbool prop_solver::mss(expr_ref_vector &hard, expr_ref_vector &soft) {
}
// move sat soft constraints to the output vector
for (unsigned k = i; k < j; ++k) {soft.push_back(hard.get(k));}
for (unsigned k = i; k < j; ++k) { soft.push_back(hard.get(k)); }
// cleanup hard constraints
hard.resize(hard_sz);
return l_true;
@ -228,7 +228,7 @@ lbool prop_solver::mss(expr_ref_vector &hard, expr_ref_vector &soft) {
/// Runs maxsat loop on m_ctx Returns l_false if hard is unsat,
/// otherwise reduces soft such that hard & soft is sat.
lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft,
const expr_ref_vector &clause)
vector<expr_ref_vector> const & clauses)
{
// replace expressions by assumption literals
iuc_solver::scoped_mk_proxy _p_(*m_ctx, hard);
@ -236,7 +236,7 @@ lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft,
// assume soft constraints are propositional literals (no need to proxy)
hard.append(soft);
lbool res = m_ctx->check_sat_cc(hard, clause);
lbool res = m_ctx->check_sat_cc(hard, clauses);
// if hard constraints alone are unsat or there are no soft
// constraints, we are done
if (res != l_false || soft.empty()) { return res; }
@ -270,7 +270,7 @@ lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft,
}
// check that the NEW constraints became sat
res = m_ctx->check_sat_cc(hard, clause);
res = m_ctx->check_sat_cc(hard, clauses);
if (res != l_false) { break; }
// still unsat, update the core and repeat
core.reset();
@ -290,7 +290,7 @@ lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft,
lbool prop_solver::internal_check_assumptions(expr_ref_vector &hard_atoms,
expr_ref_vector &soft_atoms,
const expr_ref_vector &clause)
vector<expr_ref_vector> const & clauses)
{
// XXX Turn model generation if m_model != 0
SASSERT(m_ctx);
@ -302,7 +302,7 @@ lbool prop_solver::internal_check_assumptions(expr_ref_vector &hard_atoms,
}
if (m_in_level) { assert_level_atoms(m_current_level); }
lbool result = maxsmt(hard_atoms, soft_atoms, clause);
lbool result = maxsmt(hard_atoms, soft_atoms, clauses);
if (result != l_false && m_model) { m_ctx->get_model(*m_model); }
SASSERT(result != l_false || soft_atoms.empty());
@ -375,7 +375,9 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
unsigned soft_sz = soft.size();
(void) soft_sz;
lbool res = internal_check_assumptions(hard, soft, clause);
vector<expr_ref_vector> clauses;
clauses.push_back(clause);
lbool res = internal_check_assumptions(hard, soft, clauses);
if (!m_use_push_bg) { m_ctx->pop(1); }
TRACE("psolve_verbose",

4
src/muz/spacer/spacer_prop_solver.h
View file

@ -67,10 +67,10 @@ private:
lbool internal_check_assumptions(expr_ref_vector &hard,
expr_ref_vector &soft,
const expr_ref_vector &clause);
vector<expr_ref_vector> const & clause);
lbool maxsmt(expr_ref_vector &hard, expr_ref_vector &soft,
const expr_ref_vector &clause);
vector<expr_ref_vector> const & clauses);
lbool mss(expr_ref_vector &hard, expr_ref_vector &soft);

91
src/smt/smt_context.cpp
View file

@ -61,7 +61,6 @@ namespace smt {
m_dyn_ack_manager(*this, p),
m_is_diseq_tmp(nullptr),
m_units_to_reassert(m_manager),
m_clause(nullptr),
m_qhead(0),
m_simp_qhead(0),
m_simp_counter(0),
@ -1815,7 +1814,7 @@ namespace smt {
*/
bool context::decide() {
if (at_search_level() && !m_clause_lits.empty()) {
if (at_search_level() && !m_tmp_clauses.empty()) {
switch (decide_clause()) {
case l_true: // already satisfied
break;
@ -2919,8 +2918,7 @@ namespace smt {
del_clauses(m_aux_clauses, 0);
del_clauses(m_lemmas, 0);
del_justifications(m_justifications, 0);
if (m_clause) del_clause(m_clause);
m_clause = nullptr;
reset_tmp_clauses();
if (m_is_diseq_tmp) {
m_is_diseq_tmp->del_eh(m_manager, false);
m_manager.dec_ref(m_is_diseq_tmp->get_owner());
@ -3135,48 +3133,62 @@ namespace smt {
return true;
}
void context::init_clause(expr_ref_vector const& clause) {
if (m_clause) del_clause(m_clause);
m_clause = nullptr;
m_clause_lits.reset();
for (expr* lit : clause) {
void context::init_clause(expr_ref_vector const& _clause) {
literal_vector lits;
for (expr* lit : _clause) {
internalize_formula(lit, true);
mark_as_relevant(lit);
m_clause_lits.push_back(get_literal(lit));
lits.push_back(get_literal(lit));
}
if (m_clause_lits.size() >= 2) {
clause* clausep = nullptr;
if (lits.size() >= 2) {
justification* js = nullptr;
if (m_manager.proofs_enabled()) {
proof * pr = mk_clause_def_axiom(m_clause_lits.size(), m_clause_lits.c_ptr(), nullptr);
proof * pr = mk_clause_def_axiom(lits.size(), lits.c_ptr(), nullptr);
js = mk_justification(justification_proof_wrapper(*this, pr));
}
m_clause = clause::mk(m_manager, m_clause_lits.size(), m_clause_lits.c_ptr(), CLS_AUX, js);
clausep = clause::mk(m_manager, lits.size(), lits.c_ptr(), CLS_AUX, js);
}
m_tmp_clauses.push_back(std::make_pair(clausep, lits));
}
void context::reset_tmp_clauses() {
for (auto& p : m_tmp_clauses) {
if (p.first) del_clause(p.first);
}
m_tmp_clauses.reset();
}
lbool context::decide_clause() {
if (m_clause_lits.empty()) return l_true;
shuffle(m_clause_lits.size(), m_clause_lits.c_ptr(), m_random);
for (literal l : m_clause_lits) {
switch (get_assignment(l)) {
case l_false:
break;
case l_true:
return l_true;
default:
push_scope();
assign(l, b_justification::mk_axiom(), true);
return l_undef;
}
if (m_tmp_clauses.empty()) return l_true;
for (auto & tmp_clause : m_tmp_clauses) {
literal_vector& lits = tmp_clause.second;
for (literal l : lits) {
switch (get_assignment(l)) {
case l_false:
break;
case l_true:
goto next_clause;
default:
shuffle(lits.size(), lits.c_ptr(), m_random);
push_scope();
assign(l, b_justification::mk_axiom(), true);
return l_undef;
}
}
if (lits.size() == 1) {
set_conflict(b_justification(), ~lits[0]);
}
else {
set_conflict(b_justification(tmp_clause.first), null_literal);
}
VERIFY(!resolve_conflict());
return l_false;
next_clause:
;
}
if (m_clause_lits.size() == 1) {
set_conflict(b_justification(), ~m_clause_lits[0]);
}
else {
set_conflict(b_justification(m_clause), null_literal);
}
VERIFY(!resolve_conflict());
return l_false;
return l_true;
}
void context::init_assumptions(expr_ref_vector const& asms) {
@ -3277,10 +3289,7 @@ namespace smt {
m_last_search_failure = MEMOUT;
return false;
}
if (m_clause) del_clause(m_clause);
m_clause = nullptr;
m_clause_lits.reset();
reset_tmp_clauses();
m_unsat_core.reset();
m_stats.m_num_checks++;
pop_to_base_lvl();
@ -3387,17 +3396,17 @@ namespace smt {
return r;
}
lbool context::check(expr_ref_vector const& cube, expr_ref_vector const& clause) {
lbool context::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
if (!check_preamble(true)) return l_undef;
TRACE("before_search", display(tout););
setup_context(false);
expr_ref_vector asms(cube);
add_theory_assumptions(asms);
if (!validate_assumptions(asms)) return l_undef;
if (!validate_assumptions(clause)) return l_undef;
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
internalize_assertions();
init_assumptions(asms);
init_clause(clause);
for (auto const& clause : clauses) init_clause(clause);
lbool r = search();
r = mk_unsat_core(r);
r = check_finalize(r);

8
src/smt/smt_context.h
View file

@ -168,8 +168,8 @@ namespace smt {
expr_ref_vector m_units_to_reassert;
svector<char> m_units_to_reassert_sign;
literal_vector m_assigned_literals;
clause* m_clause;
literal_vector m_clause_lits;
typedef std::pair<clause*, literal_vector> tmp_clause;
vector<tmp_clause> m_tmp_clauses;
unsigned m_qhead;
unsigned m_simp_qhead;
int m_simp_counter; //!< can become negative
@ -1114,6 +1114,8 @@ namespace smt {
lbool decide_clause();
void reset_tmp_clauses();
void reset_assumptions();
void reset_clause();
@ -1505,7 +1507,7 @@ namespace smt {
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true, bool already_did_theory_assumptions = false);
lbool check(expr_ref_vector const& cube, expr_ref_vector const& clause);
lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses);
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);

6
src/smt/smt_kernel.cpp
View file

@ -115,7 +115,7 @@ namespace smt {
return m_kernel.check(num_assumptions, assumptions);
}
lbool check(expr_ref_vector const& cube, expr_ref_vector const& clause) {
lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clause) {
return m_kernel.check(cube, clause);
}
@ -291,8 +291,8 @@ namespace smt {
return r;
}
lbool kernel::check(expr_ref_vector const& cube, expr_ref_vector const& clause) {
return m_imp->check(cube, clause);
lbool kernel::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
return m_imp->check(cube, clauses);
}

2
src/smt/smt_kernel.h
View file

@ -132,7 +132,7 @@ namespace smt {
lbool check(app_ref_vector const& asms) { return check(asms.size(), (expr* const*)asms.c_ptr()); }
lbool check(expr_ref_vector const& cube, expr_ref_vector const& clause);
lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses);
/**
\brief extract consequences among variables.

4
src/smt/smt_solver.cpp
View file

@ -191,8 +191,8 @@ namespace smt {
}
lbool check_sat_cc_core(expr_ref_vector const& cube, expr_ref_vector const& clause) override {
return m_context.check(cube, clause);
lbool check_sat_cc_core(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) override {
return m_context.check(cube, clauses);
}
struct scoped_minimize_core {

4
src/solver/solver.h
View file

@ -152,8 +152,8 @@ public:
The cube corresponds to auxiliary assumptions. The clause as an auxiliary disjunction that is also
assumed for the check.
*/
virtual lbool check_sat_cc(expr_ref_vector const& cube, expr_ref_vector const& clause) {
if (clause.empty()) return check_sat(cube.size(), cube.c_ptr());
virtual lbool check_sat_cc(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
if (clauses.empty()) return check_sat(cube.size(), cube.c_ptr());
NOT_IMPLEMENTED_YET();
}

6
src/solver/solver_na2as.cpp
View file

@ -67,10 +67,10 @@ lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptio
return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr());
}
lbool solver_na2as::check_sat_cc(const expr_ref_vector &assumptions, const expr_ref_vector &clause) {
if (clause.empty()) return check_sat(assumptions.size(), assumptions.c_ptr());
lbool solver_na2as::check_sat_cc(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) {
if (clauses.empty()) return check_sat(assumptions.size(), assumptions.c_ptr());
append_assumptions app(m_assumptions, assumptions.size(), assumptions.c_ptr());
return check_sat_cc_core(m_assumptions, clause);
return check_sat_cc_core(m_assumptions, clauses);
}
lbool solver_na2as::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {

4
src/solver/solver_na2as.h
View file

@ -39,7 +39,7 @@ public:
// Subclasses of solver_na2as should redefine the following *_core methods instead of these ones.
lbool check_sat(unsigned num_assumptions, expr * const * assumptions) override;
lbool check_sat_cc(const expr_ref_vector &assumptions, const expr_ref_vector &clause) override;
lbool check_sat_cc(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) override;
void push() override;
void pop(unsigned n) override;
unsigned get_scope_level() const override;
@ -50,7 +50,7 @@ public:
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override;
protected:
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0;
virtual lbool check_sat_cc_core(const expr_ref_vector &assumptions, const expr_ref_vector &clause) {NOT_IMPLEMENTED_YET();}
virtual lbool check_sat_cc_core(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) { NOT_IMPLEMENTED_YET(); }
virtual void push_core() = 0;
virtual void pop_core(unsigned n) = 0;
};

16
src/solver/solver_pool.cpp
View file

@ -144,14 +144,14 @@ public:
if (m_dump_benchmarks && sw.get_seconds() >= m_dump_threshold) {
expr_ref_vector cube(m, num_assumptions, assumptions);
expr_ref_vector clause(m);
dump_benchmark(cube, clause, res, sw.get_seconds());
vector<expr_ref_vector> clauses;
dump_benchmark(cube, clauses, res, sw.get_seconds());
}
return res;
}
lbool check_sat_cc_core(const expr_ref_vector &cube,
const expr_ref_vector &clause) override {
lbool check_sat_cc_core(expr_ref_vector const & cube,
vector<expr_ref_vector> const & clauses) override {
SASSERT(!m_pushed || get_scope_level() > 0);
m_proof.reset();
scoped_watch _t_(m_pool.m_check_watch);
@ -160,7 +160,7 @@ public:
stopwatch sw;
sw.start();
internalize_assertions();
lbool res = m_base->check_sat_cc(cube, clause);
lbool res = m_base->check_sat_cc(cube, clauses);
sw.stop();
switch (res) {
case l_true:
@ -177,7 +177,7 @@ public:
set_status(res);
if (m_dump_benchmarks && sw.get_seconds() >= m_dump_threshold) {
dump_benchmark(cube, clause, res, sw.get_seconds());
dump_benchmark(cube, clauses, res, sw.get_seconds());
}
return res;
}
@ -265,7 +265,7 @@ public:
private:
void dump_benchmark(const expr_ref_vector &cube, const expr_ref_vector &clause,
void dump_benchmark(const expr_ref_vector &cube, vector<expr_ref_vector> const & clauses,
lbool last_status, double last_time) {
std::string file_name = mk_file_name();
std::ofstream out(file_name);
@ -276,7 +276,7 @@ private:
out << "(set-info :status " << lbool2status(last_status) << ")\n";
m_base->display(out, cube.size(), cube.c_ptr());
if (!clause.empty()) {
for (auto const& clause : clauses) {
out << ";; extra clause\n";
out << "(assert (or ";
for (auto *lit : clause) out << mk_pp(lit, m) << " ";

16
src/test/cube_clause.cpp
View file

@ -35,24 +35,32 @@ void tst_cube_clause() {
r = solver->check_sat(cube);
std::cout << r << "\n";
clause.push_back(b);
r = solver->check_sat(cube, clause);
vector<expr_ref_vector> clauses;
clauses.push_back(clause);
r = solver->check_sat_cc(cube, clauses);
std::cout << r << "\n";
core.reset();
solver->get_unsat_core(core);
std::cout << core << "\n";
clause.push_back(d);
r = solver->check_sat(cube, clause);
clauses.reset();
clauses.push_back(clause);
r = solver->check_sat_cc(cube, clauses);
std::cout << r << "\n";
core.reset();
solver->get_unsat_core(core);
std::cout << core << "\n";
clause.push_back(f);
r = solver->check_sat(cube, clause);
clauses.reset();
clauses.push_back(clause);
r = solver->check_sat_cc(cube, clauses);
std::cout << r << "\n";
core.reset();
solver->get_unsat_core(core);
std::cout << core << "\n";
clause.push_back(g);
r = solver->check_sat(cube, clause);
clauses.reset();
clauses.push_back(clause);
r = solver->check_sat_cc(cube, clauses);
std::cout << r << "\n";
}