mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-28 00:33:56 -07:00
parent c561563a47
commit 6c4cadd223
6 changed files with 70 additions and 124 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/sat/sat_lookahead.cpp
View file

@ -463,10 +463,8 @@ namespace sat {
}
}
static unsigned counter = 0;
void lookahead::heule_schur_scores() {
if (counter % 10 != 0) return;
++counter;
if (m_rating_throttle++ % 10 != 0) return;
for (bool_var x : m_freevars) {
literal l(x, false);
m_rating[l.var()] = heule_schur_score(l) * heule_schur_score(~l);
@ -536,8 +534,7 @@ namespace sat {
}
void lookahead::heule_unit_scores() {
if (counter % 10 != 0) return;
++counter;
if (m_rating_throttle++ % 10 != 0) return;
for (bool_var x : m_freevars) {
literal l(x, false);
m_rating[l.var()] = heule_unit_score(l) * heule_unit_score(~l);
@ -614,7 +611,6 @@ namespace sat {
double neg = l_score(~l, h, factor, sqfactor, afactor);
hp[l.index()] = pos;
hp[(~l).index()] = neg;
// std::cout << "h_scores: " << pos << " " << neg << "\n";
m_rating[l.var()] = pos * neg;
}
}
@ -930,8 +926,6 @@ namespace sat {
return out;
}
static unsigned last_prefix_length = 0;
void lookahead::display_search_string() {
printf("\r");
uint64 q = m_prefix;
@ -945,10 +939,10 @@ namespace sat {
printf(" d: %d", depth);
new_prefix_length += 10;
}
for (unsigned i = new_prefix_length; i < last_prefix_length; ++i) {
for (unsigned i = new_prefix_length; i < m_last_prefix_length; ++i) {
printf(" ");
}
last_prefix_length = new_prefix_length;
m_last_prefix_length = new_prefix_length;
fflush(stdout);
}
@ -2105,7 +2099,6 @@ namespace sat {
l = diff1 < diff2 ? lit : ~lit;
}
}
// if (count > 1) std::cout << count << "\n";
TRACE("sat", tout << "selected: " << l << "\n";);
return l;
}
@ -2276,8 +2269,8 @@ namespace sat {
if (m_search_mode == lookahead_mode::searching) {
m_stats.m_propagations++;
TRACE("sat", tout << "removing free var v" << l.var() << "\n";);
if (l.var() > m_freevars.max_var()) std::cout << "bigger than max-var: " << l << " " << " " << m_freevars.max_var() << "\n";
if (!m_freevars.contains(l.var())) std::cout << "does not contain: " << l << " eliminated: " << m_s.was_eliminated(l.var()) << "\n";
if (l.var() > m_freevars.max_var()) IF_VERBOSE(0, verbose_stream() << "bigger than max-var: " << l << " " << " " << m_freevars.max_var() << "\n";);
if (!m_freevars.contains(l.var())) IF_VERBOSE(0, verbose_stream() << "does not contain: " << l << " eliminated: " << m_s.was_eliminated(l.var()) << "\n";);
if (m_freevars.contains(l.var())) { m_freevars.remove(l.var()); }
validate_assign(l);
}

6
src/sat/sat_lookahead.h
View file

@ -194,8 +194,10 @@ namespace sat {
#endif
double m_lookahead_reward; // metric associated with current lookahead1 literal.
literal_vector m_wstack; // windofall stack that is populated in lookahead1 mode
unsigned m_last_prefix_length;
uint64 m_prefix; // where we are in search tree
svector<prefix> m_vprefix; // var: prefix where variable participates in propagation
unsigned m_rating_throttle; // throttle to recompute rating
indexed_uint_set m_freevars;
lookahead_mode m_search_mode; // mode of search
stats m_stats;
@ -507,7 +509,9 @@ namespace sat {
m_drat(s),
m_num_tc1(0),
m_level(2),
m_prefix(0) {
m_last_prefix_length(0),
m_prefix(0),
m_rating_throttle(0) {
m_s.rlimit().push_child(&m_rlimit);
init_config();
}

1
src/sat/sat_solver.h
View file

@ -597,6 +597,7 @@ namespace sat {
clause * const * begin_learned() const { return m_learned.begin(); }
clause * const * end_learned() const { return m_learned.end(); }
clause_vector const& learned() const { return m_learned; }
clause_vector const& clauses() const { return m_clauses; }
void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only = false) const;
// -----------------------

53
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -17,27 +17,6 @@ Notes:
--*/
/*
#include "solver.h"
#include "tactical.h"
#include "sat_solver.h"
#include "ba_solver.h"
#include "tactic2solver.h"
#include "aig_tactic.h"
#include "propagate_values_tactic.h"
#include "max_bv_sharing_tactic.h"
#include "card2bv_tactic.h"
#include "bit_blaster_tactic.h"
#include "simplify_tactic.h"
#include "goal2sat.h"
#include "ast_pp.h"
#include "model_smt2_pp.h"
#include "filter_model_converter.h"
#include "bit_blaster_model_converter.h"
#include "ast_translation.h"
#include "ast_util.h"
#include "propagate_values_tactic.h"
*/
#include "solver/solver.h"
#include "tactic/tactical.h"
@ -133,17 +112,6 @@ public:
if (m_mc0.get()) result->m_mc0 = m_mc0->translate(tr);
result->m_internalized = m_internalized;
result->m_internalized_converted = m_internalized_converted;
#if 0
static unsigned file_no = 0;
#pragma omp critical (print_sat)
{
++file_no;
std::ostringstream ostrm;
ostrm << "s" << file_no << ".txt";
std::ofstream ous(ostrm.str());
result->m_solver.display(ous);
}
#endif
return result;
}
@ -660,9 +628,9 @@ private:
}
sat::literal_vector value;
sat::literal_set premises;
for (unsigned i = 0; i < bvars.size(); ++i) {
for (sat::bool_var bv : bvars) {
unsigned index;
if (bool_var2conseq.find(bvars[i], index)) {
if (bool_var2conseq.find(bv, index)) {
value.push_back(lconseq[index][0]);
for (unsigned j = 1; j < lconseq[index].size(); ++j) {
premises.insert(lconseq[index][j]);
@ -754,10 +722,8 @@ private:
}
void extract_asm2dep(dep2asm_t const& dep2asm, u_map<expr*>& asm2dep) {
dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
expr* e = it->m_key;
asm2dep.insert(it->m_value.index(), e);
for (auto const& kv : dep2asm) {
asm2dep.insert(kv.m_value.index(), kv.m_key);
}
}
@ -777,9 +743,9 @@ private:
);
m_core.reset();
for (unsigned i = 0; i < core.size(); ++i) {
for (sat::literal c : core) {
expr* e = 0;
VERIFY(asm2dep.find(core[i].index(), e));
VERIFY(asm2dep.find(c.index(), e));
if (asm2fml.contains(e)) {
e = asm2fml.find(e);
}
@ -789,11 +755,10 @@ private:
void check_assumptions(dep2asm_t& dep2asm) {
sat::model const & ll_m = m_solver.get_model();
dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
sat::literal lit = it->m_value;
for (auto const& kv : dep2asm) {
sat::literal lit = kv.m_value;
if (sat::value_at(lit, ll_m) != l_true) {
IF_VERBOSE(0, verbose_stream() << mk_pp(it->m_key, m) << " does not evaluate to true\n";
IF_VERBOSE(0, verbose_stream() << mk_pp(kv.m_key, m) << " does not evaluate to true\n";
verbose_stream() << m_asms << "\n";
m_solver.display_assignment(verbose_stream());
m_solver.display(verbose_stream()););

15
src/sat/tactic/atom2bool_var.cpp
View file

@ -16,19 +16,18 @@ Author:
Notes:
--*/
#include "sat/tactic/atom2bool_var.h"
#include "ast/ast_smt2_pp.h"
#include "util/ref_util.h"
#include "ast/ast_smt2_pp.h"
#include "tactic/goal.h"
#include "sat/tactic/atom2bool_var.h"
void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const {
obj_map<expr, var>::iterator it = m_mapping.begin();
obj_map<expr, var>::iterator end = m_mapping.end();
for (; it != end; ++it) {
sat::literal l(static_cast<sat::bool_var>(it->m_value), false);
lit2expr.set(l.index(), it->m_key);
for (auto const& kv : m_mapping) {
sat::literal l(static_cast<sat::bool_var>(kv.m_value), false);
lit2expr.set(l.index(), kv.m_key);
l.neg();
lit2expr.set(l.index(), m().mk_not(it->m_key));
lit2expr.set(l.index(), m().mk_not(kv.m_key));
}
}

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

@ -26,19 +26,19 @@ Author:
Notes:
--*/
#include "sat/tactic/goal2sat.h"
#include "ast/ast_smt2_pp.h"
#include "util/ref_util.h"
#include "util/cooperate.h"
#include "tactic/filter_model_converter.h"
#include "model/model_evaluator.h"
#include "ast/for_each_expr.h"
#include "model/model_v2_pp.h"
#include "tactic/tactic.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"
#include "sat/ba_solver.h"
#include "ast/pb_decl_plugin.h"
#include "ast/ast_util.h"
#include "ast/for_each_expr.h"
#include "sat/tactic/goal2sat.h"
#include "sat/ba_solver.h"
#include "model/model_evaluator.h"
#include "model/model_v2_pp.h"
#include "tactic/tactic.h"
#include "tactic/filter_model_converter.h"
#include<sstream>
struct goal2sat::imp {
@ -412,15 +412,7 @@ struct goal2sat::imp {
for (unsigned i = 0; i < num_args; ++i) {
sat::literal lit(m_result_stack[sz - num_args + i]);
if (!m_solver.is_external(lit.var())) {
#if 1
m_solver.set_external(lit.var());
#else
sat::bool_var w = m_solver.mk_var(true);
sat::literal lit2(w, false);
mk_clause(lit, ~lit2);
mk_clause(~lit, lit2);
lit = lit2;
#endif
}
lits.push_back(lit);
}
@ -473,9 +465,9 @@ struct goal2sat::imp {
k.neg();
svector<wliteral> wlits;
convert_pb_args(t, wlits);
for (unsigned i = 0; i < wlits.size(); ++i) {
wlits[i].second.neg();
k += rational(wlits[i].first);
for (wliteral& wl : wlits) {
wl.second.neg();
k += rational(wl.first);
}
check_unsigned(k);
unsigned sz = m_result_stack.size();
@ -502,9 +494,9 @@ struct goal2sat::imp {
sat::bool_var v2 = root ? sat::null_bool_var : m_solver.mk_var(true);
m_ext->add_pb_ge(v1, wlits, k.get_unsigned());
k.neg();
for (unsigned i = 0; i < wlits.size(); ++i) {
wlits[i].second.neg();
k += rational(wlits[i].first);
for (wliteral& wl : wlits) {
wl.second.neg();
k += rational(wl.first);
}
check_unsigned(k);
m_ext->add_pb_ge(v2, wlits, k.get_unsigned());
@ -547,8 +539,8 @@ struct goal2sat::imp {
sat::literal_vector lits;
unsigned sz = m_result_stack.size();
convert_pb_args(t->get_num_args(), lits);
for (unsigned i = 0; i < lits.size(); ++i) {
lits[i].neg();
for (sat::literal& l : lits) {
l.neg();
}
if (root) {
m_result_stack.reset();
@ -570,8 +562,8 @@ struct goal2sat::imp {
sat::bool_var v1 = root ? sat::null_bool_var : m_solver.mk_var(true);
sat::bool_var v2 = root ? sat::null_bool_var : m_solver.mk_var(true);
m_ext->add_at_least(v1, lits, k.get_unsigned());
for (unsigned i = 0; i < lits.size(); ++i) {
lits[i].neg();
for (sat::literal& l : lits) {
l.neg();
}
m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned());
if (root) {
@ -782,8 +774,7 @@ struct goal2sat::imp {
fmls.reset();
m.linearize(g.dep(idx), deps);
fmls.push_back(f);
for (unsigned i = 0; i < deps.size(); ++i) {
expr * d = deps[i];
for (expr * d : deps) {
expr * d1 = d;
SASSERT(m.is_bool(d));
bool sign = m.is_not(d, d1);
@ -935,10 +926,8 @@ struct sat2goal::imp {
// create a SAT model using md
sat::model sat_md;
unsigned sz = m_var2expr.size();
expr_ref val(m());
for (sat::bool_var v = 0; v < sz; v++) {
expr * atom = m_var2expr.get(v);
for (expr * atom : m_var2expr) {
ev(atom, val);
if (m().is_true(val))
sat_md.push_back(l_true);
@ -952,7 +941,7 @@ struct sat2goal::imp {
m_mc(sat_md);
// register value of non-auxiliary boolean variables back into md
sz = m_var2expr.size();
unsigned sz = m_var2expr.size();
for (sat::bool_var v = 0; v < sz; v++) {
expr * atom = m_var2expr.get(v);
if (is_uninterp_const(atom)) {
@ -973,9 +962,8 @@ struct sat2goal::imp {
virtual model_converter * translate(ast_translation & translator) {
sat_model_converter * res = alloc(sat_model_converter, translator.to());
res->m_fmc = static_cast<filter_model_converter*>(m_fmc->translate(translator));
unsigned sz = m_var2expr.size();
for (unsigned i = 0; i < sz; i++)
res->m_var2expr.push_back(translator(m_var2expr.get(i)));
for (expr* e : m_var2expr)
res->m_var2expr.push_back(translator(e));
return res;
}
@ -1056,9 +1044,9 @@ struct sat2goal::imp {
pb_util pb(m);
ptr_buffer<expr> lits;
vector<rational> coeffs;
for (unsigned i = 0; i < p.size(); ++i) {
lits.push_back(lit2expr(p[i].second));
coeffs.push_back(rational(p[i].first));
for (auto const& wl : p) {
lits.push_back(lit2expr(wl.second));
coeffs.push_back(rational(wl.first));
}
rational k(p.k());
expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m);
@ -1072,8 +1060,8 @@ struct sat2goal::imp {
void assert_card(goal& r, sat::ba_solver::card const& c) {
pb_util pb(m);
ptr_buffer<expr> lits;
for (unsigned i = 0; i < c.size(); ++i) {
lits.push_back(lit2expr(c[i]));
for (sat::literal l : c) {
lits.push_back(lit2expr(l));
}
expr_ref fml(pb.mk_at_most_k(c.size(), lits.c_ptr(), c.k()), m);
@ -1085,8 +1073,8 @@ struct sat2goal::imp {
void assert_xor(goal & r, sat::ba_solver::xor const& x) {
ptr_buffer<expr> lits;
for (unsigned i = 0; i < x.size(); ++i) {
lits.push_back(lit2expr(x[i]));
for (sat::literal l : x) {
lits.push_back(lit2expr(l));
}
expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m);
@ -1096,16 +1084,16 @@ struct sat2goal::imp {
r.assert_expr(fml);
}
void assert_clauses(sat::solver const & s, sat::clause * const * begin, sat::clause * const * end, goal & r, bool asserted) {
void assert_clauses(sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
ptr_buffer<expr> lits;
for (sat::clause * const * it = begin; it != end; it++) {
for (sat::clause* cp : clauses) {
checkpoint();
lits.reset();
sat::clause const & c = *(*it);
sat::clause const & c = *cp;
unsigned sz = c.size();
if (asserted || m_learned || c.glue() <= s.get_config().m_gc_small_lbd) {
for (unsigned i = 0; i < sz; i++) {
lits.push_back(lit2expr(c[i]));
for (sat::literal l : c) {
lits.push_back(lit2expr(l));
}
r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
}
@ -1141,15 +1129,13 @@ struct sat2goal::imp {
// collect binary clauses
svector<sat::solver::bin_clause> bin_clauses;
s.collect_bin_clauses(bin_clauses, m_learned);
svector<sat::solver::bin_clause>::iterator it = bin_clauses.begin();
svector<sat::solver::bin_clause>::iterator end = bin_clauses.end();
for (; it != end; ++it) {
for (sat::solver::bin_clause const& bc : bin_clauses) {
checkpoint();
r.assert_expr(m.mk_or(lit2expr(it->first), lit2expr(it->second)));
r.assert_expr(m.mk_or(lit2expr(bc.first), lit2expr(bc.second)));
}
// collect clauses
assert_clauses(s, s.begin_clauses(), s.end_clauses(), r, true);
assert_clauses(s, s.begin_learned(), s.end_learned(), r, false);
assert_clauses(s, s.clauses(), r, true);
assert_clauses(s, s.learned(), r, false);
sat::ba_solver* ext = get_ba_solver(s);
if (ext) {
@ -1220,13 +1206,11 @@ struct sat2goal::imp {
// collect learned binary clauses
svector<sat::solver::bin_clause> bin_clauses;
s.collect_bin_clauses(bin_clauses, true, true);
svector<sat::solver::bin_clause>::iterator it = bin_clauses.begin();
svector<sat::solver::bin_clause>::iterator end = bin_clauses.end();
for (; it != end; ++it) {
for (sat::solver::bin_clause const& bc : bin_clauses) {
checkpoint();
lits.reset();
lits.push_back(it->first);
lits.push_back(it->second);
lits.push_back(bc.first);
lits.push_back(bc.second);
add_clause(lits, lemmas);
}
// collect clauses