mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

save memory in the sat solver to tentatively speed things up.

Browse source 
I get a slight speedup on my benchmarks. There's still one extra sign extend, which will be removed in a follow-up patch

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-03-02 09:50:35 +00:00
parent e64760abbd
commit 89c43676d5
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_solver.h
View file

@ -89,7 +89,7 @@ namespace sat {
clause_vector m_learned; clause_vector m_learned;
unsigned m_num_frozen; unsigned m_num_frozen;
vector<watch_list> m_watches; vector<watch_list> m_watches;
svector<lbool> m_assignment; char_vector m_assignment;
svector<justification> m_justification; svector<justification> m_justification;
svector<char> m_decision; svector<char> m_decision;
svector<char> m_mark; svector<char> m_mark;
@ -200,8 +200,8 @@ namespace sat {
bool is_external(bool_var v) const { return m_external[v] != 0; } bool is_external(bool_var v) const { return m_external[v] != 0; }
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; } unsigned scope_lvl() const { return m_scope_lvl; }
lbool value(literal l) const { return m_assignment[l.index()]; } lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }
lbool value(bool_var v) const { return 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()]; }
void assign(literal l, justification j) { void assign(literal l, justification j) {