mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-10 10:43:55 +08:00
parent 00685ff04f
commit d57bca8f8c
8 changed files with 78 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_lookahead.cpp
View file

@ -1832,7 +1832,7 @@ namespace sat {
unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations;
scoped_level _sl(*this, dl_truth);
//SASSERT(get_level(m_trail.back()) == dl_truth);
IF_VERBOSE(2, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";);
IF_VERBOSE(3, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";);
lookahead_backtrack();
assign(l);
propagate();

2
src/sat/sat_model_converter.cpp
View file

@ -75,7 +75,7 @@ namespace sat {
void model_converter::operator()(model & m) const {
vector<entry>::const_iterator begin = m_entries.begin();
vector<entry>::const_iterator it = m_entries.end();
bool first = false; // true; // false; // // true;
bool first = false; // true; // false; // // true;
//SASSERT(!m_solver || m_solver->check_clauses(m));
while (it != begin) {
--it;

9
src/sat/sat_simplifier.cpp
View file

@ -1129,7 +1129,8 @@ namespace sat {
}
}
}
if (m_intersection.empty()) {
// remove tautology literals if literal has no resolution intersection
if (m_intersection.empty() && !first) {
m_tautology.shrink(tsz);
}
// if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";);
@ -1202,7 +1203,7 @@ namespace sat {
if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit);
if (s.is_marked(lit)) idx = i;
}
if (false) {
if (false && _blocked.var() == 8074) {
IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n";
verbose_stream() << "tautology: " << m_tautology << "\n";
verbose_stream() << "index: " << idx << "\n";
@ -1212,8 +1213,8 @@ namespace sat {
}
for (unsigned i = idx; i > 0; --i) {
literal lit = m_covered_clause[i];
s.mark_visited(lit);
continue;
//s.mark_visited(lit);
//continue;
if (!s.is_marked(lit)) continue;
clause_ante const& ante = m_covered_antecedent[i];
if (ante.cls()) {

33
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -552,7 +552,7 @@ class elim_uncnstr_tactic : public tactic {
// The result of bv_le is not just introducing a new fresh name,
// we need a side condition.
// TODO: the correct proof step
return 0;
return nullptr;
}
if (uncnstr(arg1)) {
// v <= t
@ -804,20 +804,17 @@ class elim_uncnstr_tactic : public tactic {
ast_manager & m() { return m_manager; }
void init_mc(bool produce_models) {
if (!produce_models) {
m_mc = 0;
return;
m_mc = nullptr;
if (produce_models) {
m_mc = alloc(mc, m(), "elim_uncstr");
}
m_mc = alloc(mc, m(), "elim_uncstr");
}
void init_rw(bool produce_proofs) {
m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);
}
void operator()(goal_ref const & g,
goal_ref_buffer & result) {
bool produce_models = g->models_enabled();
void operator()(goal_ref const & g, goal_ref_buffer & result) {
bool produce_proofs = g->proofs_enabled();
TRACE("elim_uncnstr_bug", g->display(tout););
@ -832,14 +829,9 @@ class elim_uncnstr_tactic : public tactic {
}
bool modified = true;
TRACE("elim_uncnstr", tout << "unconstrained variables...\n";
obj_hashtable<expr>::iterator it = m_vars.begin();
obj_hashtable<expr>::iterator end = m_vars.end();
for (; it != end; ++it) {
expr * v = *it;
tout << mk_ismt2_pp(v, m()) << " ";
}
for (expr * v : m_vars) tout << mk_ismt2_pp(v, m()) << " ";
tout << "\n";);
init_mc(produce_models);
init_mc(g->models_enabled());
init_rw(produce_proofs);
expr_ref new_f(m());
@ -866,14 +858,9 @@ class elim_uncnstr_tactic : public tactic {
else {
app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars;
m_num_elim_apps = fresh_vars.size();
if (produce_models && !fresh_vars.empty()) {
generic_model_converter * fmc = alloc(generic_model_converter, m(), "elim_uncnstr");
for (app * f : fresh_vars)
fmc->hide(f);
g->add(concat(fmc, m_mc.get()));
}
else {
g->set((model_converter*)nullptr);
if (m_mc.get()) {
for (app * f : fresh_vars) m_mc->hide(f);
g->add(m_mc.get());
}
}
m_mc = 0;

2
src/tactic/portfolio/CMakeLists.txt
View file

@ -18,8 +18,6 @@ z3_add_component(portfolio
smtlogic_tactics
subpaving_tactic
ufbv_tactic
PYG_FILES
parallel_params.pyg
TACTIC_HEADERS
default_tactic.h
fd_solver.h

88
src/tactic/portfolio/parallel_tactic.cpp
View file

@ -42,6 +42,7 @@ Notes:
#include "solver/solver2tactic.h"
#include "tactic/tactic.h"
#include "tactic/portfolio/fd_solver.h"
#include "tactic/smtlogics/parallel_params.hpp"
class parallel_tactic : public tactic {
@ -150,10 +151,27 @@ class parallel_tactic : public tactic {
};
class cube_var {
expr_ref_vector m_vars;
expr_ref m_cube;
public:
cube_var(expr* c, expr_ref_vector& vs):
m_vars(vs), m_cube(c, vs.get_manager()) {}
cube_var operator()(ast_translation& tr) {
expr_ref_vector vars(tr.to());
for (expr* v : m_vars) vars.push_back(tr(v));
return cube_var(tr(m_cube.get()), vars);
}
expr* cube() const { return m_cube; }
expr_ref_vector const& vars() { return m_vars; }
};
class solver_state {
task_type m_type; // current work role of the task
scoped_ptr<ast_manager> m_manager; // ownership handle to ast_manager
expr_ref_vector m_cubes; // set of cubes to process by task
vector<cube_var> m_cubes; // set of cubes to process by task
expr_ref_vector m_asserted_cubes; // set of cubes asserted on the current solver
params_ref m_params; // configuration parameters
ref<solver> m_solver; // solver state
@ -176,14 +194,14 @@ class parallel_tactic : public tactic {
solver_state(ast_manager* m, solver* s, params_ref const& p, task_type t):
m_type(t),
m_manager(m),
m_cubes(s->get_manager()),
m_asserted_cubes(s->get_manager()),
m_params(p),
m_solver(s),
m_depth(0),
m_width(1.0)
{
m_restart_max = p.get_uint("sat.restart.max", 10);
parallel_params pp(p);
m_restart_max = pp.restart_max();
}
ast_manager& m() { return m_solver->get_manager(); }
@ -199,7 +217,7 @@ class parallel_tactic : public tactic {
ast_translation tr(m, *new_m);
solver* s = m_solver->translate(*new_m, m_params);
solver_state* st = alloc(solver_state, new_m, s, m_params, m_type);
for (expr* c : m_cubes) st->m_cubes.push_back(tr(c));
for (auto & c : m_cubes) st->m_cubes.push_back(c(tr));
for (expr* c : m_asserted_cubes) st->m_asserted_cubes.push_back(tr(c));
st->m_depth = m_depth;
st->m_width = m_width;
@ -210,11 +228,11 @@ class parallel_tactic : public tactic {
void set_type(task_type t) { m_type = t; }
expr_ref_vector const& cubes() const { SASSERT(m_type == conquer_task); return m_cubes; }
vector<cube_var> const& cubes() const { SASSERT(m_type == conquer_task); return m_cubes; }
// remove up to n cubes from list of cubes.
expr_ref_vector split_cubes(unsigned n) {
expr_ref_vector result(m());
vector<cube_var> split_cubes(unsigned n) {
vector<cube_var> result;
while (n-- > 0 && !m_cubes.empty()) {
result.push_back(m_cubes.back());
m_cubes.pop_back();
@ -222,7 +240,7 @@ class parallel_tactic : public tactic {
return result;
}
void set_cubes(expr_ref_vector const& c) {
void set_cubes(vector<cube_var>& c) {
m_cubes.reset();
m_cubes.append(c);
}
@ -280,16 +298,18 @@ class parallel_tactic : public tactic {
}
void set_conquer_params() {
m_params.set_bool("gc.initial", true);
m_params.set_bool("lookahead_simplify", false);
m_params.set_uint("restart.max", m_restart_max);
get_solver().updt_params(m_params);
}
void set_simplify_params(bool pb_simp, bool retain_blocked) {
parallel_params pp(m_params);
m_params.set_bool("cardinality.solver", pb_simp);
m_params.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit"));
if (m_params.get_uint("inprocess.max", UINT_MAX) == UINT_MAX)
m_params.set_uint("inprocess.max", 2);
m_params.set_uint("inprocess.max", pp.inprocess_max());
m_params.set_bool("lookahead_simplify", true);
m_params.set_uint("restart.max", UINT_MAX);
m_params.set_bool("retain_blocked_clauses", retain_blocked);
@ -350,7 +370,7 @@ private:
IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% ";
if (status == l_true) verbose_stream() << ":status sat ";
if (status == l_undef) verbose_stream() << ":status unknown ";
verbose_stream() << ":unsat " << m_num_unsat << " :branches " << m_branches << ")\n";);
verbose_stream() << ":unsat " << m_num_unsat << " :open-branches " << m_branches << ")\n";);
}
void report_sat(solver_state& s) {
@ -371,9 +391,11 @@ private:
}
void report_unsat(solver_state& s) {
{
std::lock_guard<std::mutex> lock(m_mutex);
++m_num_unsat;
}
close_branch(s, l_false);
std::lock_guard<std::mutex> lock(m_mutex);
++m_num_unsat;
}
void report_undef(solver_state& s) {
@ -383,7 +405,11 @@ private:
void cube_and_conquer(solver_state& s) {
ast_manager& m = s.m();
expr_ref_vector cubes(m), cube(m), hard_cubes(m);
// expr_ref_vector cube(m), hard_cubes(m);
vector<cube_var> cube, hard_cubes, cubes;
expr_ref_vector vars(m);
add_branches(1);
switch (s.type()) {
case cube_task: goto cube;
@ -399,7 +425,11 @@ private:
SASSERT(cube.size() <= 1);
IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";);
if (!s.cubes().empty()) m_queue.add_task(s.clone());
if (!cube.empty()) s.assert_cube(cube.get(0));
if (!cube.empty()) {
s.assert_cube(cube.get(0).cube());
vars.reset();
vars.append(cube.get(0).vars());
}
s.inc_depth(1);
// simplify
@ -414,7 +444,6 @@ private:
cubes.reset();
s.set_cube_params();
while (true) {
expr_ref_vector vars(m);
expr_ref_vector c = s.get_solver().cube(vars, UINT_MAX); // TBD tune this
if (c.empty()) {
report_undef(s);
@ -423,11 +452,11 @@ private:
if (m.is_false(c.back())) {
break;
}
cubes.push_back(mk_and(c));
cubes.push_back(cube_var(mk_and(c), vars));
IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :cube " << cubes.size() << " :vars " << vars.size() << ")\n");
}
IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << ")\n";);
IF_VERBOSE(12, verbose_stream() << "(tactic.parallel :cubes " << cubes << ")\n";);
if (cubes.empty()) {
report_unsat(s);
@ -435,7 +464,7 @@ private:
}
else {
s.inc_width(cubes.size());
add_branches(cubes.size());
add_branches(cubes.size() - 1);
s.set_cubes(cubes);
s.set_type(conquer_task);
goto conquer;
@ -451,9 +480,9 @@ private:
s.set_conquer_params();
hard_cubes.reset();
for (expr * c : cubes) {
switch (s.solve(c)) {
case l_undef: hard_cubes.push_back(c); break;
for (cube_var& cv : cubes) {
switch (s.solve(cv.cube())) {
case l_undef: hard_cubes.push_back(cv); break;
case l_true: report_sat(s); break;
case l_false: report_unsat(s); break;
}
@ -580,6 +609,15 @@ public:
result.push_back(g.get());
}
virtual void collect_param_descrs(param_descrs & r) {
r.insert("conquer_batch_size", CPK_UINT, "(default: 1000) batch size of cubes to conquer");
}
unsigned conquer_batch_size() const {
parallel_params pp(m_params);
return pp.conquer_batch_size();
}
void cleanup() {
m_queue.reset();
init();
@ -593,14 +631,6 @@ public:
m_params.copy(p);
}
virtual void collect_param_descrs(param_descrs & r) {
r.insert("conquer_batch_size", CPK_UINT, "(default: 1000) batch size of cubes to conquer");
}
unsigned conquer_batch_size() const {
return m_params.get_uint("conquer_batch_size", 1000);
}
virtual void collect_statistics(statistics & st) const {
st.copy(m_stats);
st.update("par unsat", m_num_unsat);

1
src/tactic/smtlogics/CMakeLists.txt
View file

@ -26,6 +26,7 @@ z3_add_component(smtlogic_tactics
smt_tactic
PYG_FILES
qfufbv_tactic_params.pyg
parallel_params.pyg
TACTIC_HEADERS
nra_tactic.h
qfaufbv_tactic.h

2
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -29,7 +29,7 @@ Notes:
#include "tactic/aig/aig_tactic.h"
#include "sat/tactic/sat_tactic.h"
#include "tactic/portfolio/parallel_tactic.h"
#include "tactic/portfolio/parallel_params.hpp"
#include "tactic/smtlogics/parallel_params.hpp"
#include "ackermannization/ackermannize_bv_tactic.h"
#define MEMLIMIT 300