mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
working on SLS
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2909e8cd9e
commit
e3a854743b
2 changed files with 1 additions and 5 deletions
|
@ -54,7 +54,6 @@ namespace opt {
|
|||
unsigned m_upper;
|
||||
unsigned m_lower;
|
||||
model_ref m_model;
|
||||
unsigned m_num_steps;
|
||||
|
||||
imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft):
|
||||
m(m),
|
||||
|
@ -64,8 +63,7 @@ namespace opt {
|
|||
m_orig_soft(soft),
|
||||
m_aux(m),
|
||||
m_upper(0),
|
||||
m_lower(0),
|
||||
m_num_steps(0)
|
||||
m_lower(0)
|
||||
{
|
||||
m_upper = m_soft.size() + 1;
|
||||
m_assignment.resize(m_soft.size(), false);
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue