mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-24 21:26:59 +00:00
Code Activity

updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-27 20:49:37 -08:00
parent 1c7cb87900
commit 475101e932
2 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/sat/sat_local_search.cpp
View file

@ -74,7 +74,7 @@ namespace sat {
constraint & cn = m_constraints[c]; constraint & cn = m_constraints[c];
for (unsigned i = 0; i < cn.size(); ++i) { for (unsigned i = 0; i < cn.size(); ++i) {
bool_var v = cn[i].var(); bool_var v = cn[i].var();
if (cur_solution[v] == is_pos(cn[i])) if (is_true(cn[i]))
--cn.m_slack; --cn.m_slack;
} }
// constraint_slack[c] = constraint_k[c] - true_terms_count[c]; // constraint_slack[c] = constraint_k[c] - true_terms_count[c];
@ -340,9 +340,9 @@ namespace sat {
int org_flipvar_score = score(flipvar); int org_flipvar_score = score(flipvar);
int org_flipvar_slack_score = slack_score(flipvar); int org_flipvar_slack_score = slack_score(flipvar);
bool is_true = cur_solution[flipvar]; bool flip_is_true = cur_solution[flipvar];
int_vector& truep = m_vars[flipvar].m_watch[is_true]; int_vector& truep = m_vars[flipvar].m_watch[flip_is_true];
int_vector& falsep = m_vars[flipvar].m_watch[!is_true]; int_vector& falsep = m_vars[flipvar].m_watch[!flip_is_true];
// update related clauses and neighbor vars // update related clauses and neighbor vars
for (unsigned i = 0; i < truep.size(); ++i) { for (unsigned i = 0; i < truep.size(); ++i) {
@ -354,7 +354,7 @@ namespace sat {
for (unsigned j = 0; j < c.size(); ++j) { for (unsigned j = 0; j < c.size(); ++j) {
v = c[j].var(); v = c[j].var();
// flipping the slack increasing var will no long sat this constraint // flipping the slack increasing var will no long sat this constraint
if (cur_solution[v] == is_pos(c[j])) { if (is_true(c[j])) {
//score[v] -= constraint_weight[c]; //score[v] -= constraint_weight[c];
dec_score(v); dec_score(v);
} }
@ -367,7 +367,7 @@ namespace sat {
//score[v] += constraint_weight[c]; //score[v] += constraint_weight[c];
inc_score(v); inc_score(v);
// slack increasing var // slack increasing var
if (cur_solution[v] == is_pos(c[j])) if (is_true(c[j]))
inc_slack_score(v); inc_slack_score(v);
} }
unsat(truep[i]); unsat(truep[i]);
@ -376,7 +376,7 @@ namespace sat {
for (unsigned j = 0; j < c.size(); ++j) { for (unsigned j = 0; j < c.size(); ++j) {
v = c[j].var(); v = c[j].var();
// flip the slack decreasing var will falsify this constraint // flip the slack decreasing var will falsify this constraint
if (cur_solution[v] != is_pos(c[j])) { if (is_false(c[j])) {
//score[v] -= constraint_weight[c]; //score[v] -= constraint_weight[c];
dec_score(v); dec_score(v);
dec_slack_score(v); dec_slack_score(v);
@ -396,7 +396,7 @@ namespace sat {
for (unsigned j = 0; j < c.size(); ++j) { for (unsigned j = 0; j < c.size(); ++j) {
v = c[j].var(); v = c[j].var();
// flip the slack decreasing var will no long falsify this constraint // flip the slack decreasing var will no long falsify this constraint
if (cur_solution[v] != is_pos(c[j])) { if (is_false(c[j])) {
//score[v] += constraint_weight[c]; //score[v] += constraint_weight[c];
inc_score(v); inc_score(v);
inc_slack_score(v); inc_slack_score(v);
@ -410,7 +410,7 @@ namespace sat {
//score[v] -= constraint_weight[c]; //score[v] -= constraint_weight[c];
dec_score(v); dec_score(v);
// slack increasing var no longer sat this var // slack increasing var no longer sat this var
if (cur_solution[v] == is_pos(c[j])) if (is_true(c[j]))
dec_slack_score(v); dec_slack_score(v);
} }
sat(falsep[i]); sat(falsep[i]);
@ -419,7 +419,7 @@ namespace sat {
for (unsigned j = 0; j < c.size(); ++j) { for (unsigned j = 0; j < c.size(); ++j) {
v = c[j].var(); v = c[j].var();
// flip the slack increasing var will satisfy this constraint // flip the slack increasing var will satisfy this constraint
if (cur_solution[v] == is_pos(c[j])) { if (is_true(c[j])) {
//score[v] += constraint_weight[c]; //score[v] += constraint_weight[c];
inc_score(v); inc_score(v);
} }
@ -526,7 +526,7 @@ namespace sat {
unsigned c_size = c.size(); unsigned c_size = c.size();
for (unsigned i = 0; i < c_size; ++i) { for (unsigned i = 0; i < c_size; ++i) {
v = c[i].var(); v = c[i].var();
if (cur_solution[v] == is_pos(c[i]) && time_stamp(v) < time_stamp(best_var)) if (is_true(c[i]) && time_stamp(v) < time_stamp(best_var))
best_var = v; best_var = v;
} }
return best_var; return best_var;

8
src/sat/sat_local_search.h
View file

@ -113,9 +113,9 @@ namespace sat {
/* TBD: other scores */ /* TBD: other scores */
struct constraint { struct constraint {
unsigned m_k; unsigned m_k;
int m_slack; int m_slack;
svector<literal> m_literals; literal_vector m_literals;
constraint(unsigned k) : m_k(k), m_slack(0) {} constraint(unsigned k) : m_k(k), m_slack(0) {}
unsigned size() const { return m_literals.size(); } unsigned size() const { return m_literals.size(); }
literal const& operator[](unsigned idx) const { return m_literals[idx]; } literal const& operator[](unsigned idx) const { return m_literals[idx]; }
@ -127,6 +127,8 @@ namespace sat {
// vector<svector<term> > constraint_term; // constraint_term[i][j] means the j'th term of constraint i // vector<svector<term> > constraint_term; // constraint_term[i][j] means the j'th term of constraint i
inline bool is_pos(literal t) const { return !t.sign(); } inline bool is_pos(literal t) const { return !t.sign(); }
inline bool is_true(literal l) const { return cur_solution[l.var()] != l.sign(); }
inline bool is_false(literal l) const { return cur_solution[l.var()] == l.sign(); }
// parameters of the instance // parameters of the instance
unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint