diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 732a89099..6fa4e809e 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -707,7 +707,7 @@ void tactic_example7() {
std::cout << s.check() << "\n";
model m = s.get_model();
std::cout << "model for subgoal:\n" << m << "\n";
- std::cout << "model for original goal:\n" << r.convert_model(m) << "\n";
+ std::cout << "model for original goal:\n" << subgoal.convert_model(m) << "\n";
}
void tactic_example8() {
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 2805e7e2d..48ce6d22d 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -553,11 +553,19 @@ extern "C" {
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
- Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, unsigned cutoff) {
+ Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vs, unsigned cutoff) {
Z3_TRY;
- LOG_Z3_solver_cube(c, s, cutoff);
+ LOG_Z3_solver_cube(c, s, vs, cutoff);
ast_manager& m = mk_c(c)->m();
- expr_ref_vector result(m);
+ expr_ref_vector result(m), vars(m);
+ for (ast* a : to_ast_vector_ref(vs)) {
+ if (!is_expr(a)) {
+ SET_ERROR_CODE(Z3_INVALID_USAGE);
+ }
+ else {
+ vars.push_back(to_expr(a));
+ }
+ }
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false);
@@ -568,7 +576,7 @@ extern "C" {
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
- result.append(to_solver_ref(s)->cube(cutoff));
+ result.append(to_solver_ref(s)->cube(vars, cutoff));
}
catch (z3_exception & ex) {
mk_c(c)->handle_exception(ex);
@@ -580,6 +588,10 @@ extern "C" {
for (expr* e : result) {
v->m_ast_vector.push_back(e);
}
+ to_ast_vector_ref(vs).reset();
+ for (expr* a : vars) {
+ to_ast_vector_ref(vs).push_back(a);
+ }
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);
}
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 428f210ee..270a98ca9 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1999,18 +1999,23 @@ namespace z3 {
param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
- expr_vector cube(unsigned cutoff) { Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, cutoff); check_error(); return expr_vector(ctx(), r); }
+ expr_vector cube(expr_vector& vars, unsigned cutoff) {
+ Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
+ check_error();
+ return expr_vector(ctx(), r);
+ }
class cube_iterator {
- solver& m_solver;
- unsigned& m_cutoff;
- expr_vector m_cube;
- bool m_end;
- bool m_empty;
+ solver& m_solver;
+ unsigned& m_cutoff;
+ expr_vector& m_vars;
+ expr_vector m_cube;
+ bool m_end;
+ bool m_empty;
void inc() {
assert(!m_end && !m_empty);
- m_cube = m_solver.cube(m_cutoff);
+ m_cube = m_solver.cube(m_vars, m_cutoff);
m_cutoff = 0xFFFFFFFF;
if (m_cube.size() == 1 && m_cube[0].is_false()) {
m_cube = z3::expr_vector(m_solver.ctx());
@@ -2021,9 +2026,10 @@ namespace z3 {
}
}
public:
- cube_iterator(solver& s, unsigned& cutoff, bool end):
+ cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
m_solver(s),
m_cutoff(cutoff),
+ m_vars(vars),
m_cube(s.ctx()),
m_end(end),
m_empty(false) {
@@ -2056,20 +2062,32 @@ namespace z3 {
};
class cube_generator {
- solver& m_solver;
- unsigned m_cutoff;
+ solver& m_solver;
+ unsigned m_cutoff;
+ expr_vector m_default_vars;
+ expr_vector& m_vars;
public:
cube_generator(solver& s):
m_solver(s),
- m_cutoff(0xFFFFFFFF)
+ m_cutoff(0xFFFFFFFF),
+ m_default_vars(s.ctx()),
+ m_vars(m_default_vars)
{}
- cube_iterator begin() { return cube_iterator(m_solver, m_cutoff, false); }
- cube_iterator end() { return cube_iterator(m_solver, m_cutoff, true); }
+ cube_generator(solver& s, expr_vector& vars):
+ m_solver(s),
+ m_cutoff(0xFFFFFFFF),
+ m_default_vars(s.ctx()),
+ m_vars(vars)
+ {}
+
+ cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
+ cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
void set_cutoff(unsigned c) { m_cutoff = c; }
};
cube_generator cubes() { return cube_generator(*this); }
+ cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
};
inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index e136516e4..f67a298bb 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -404,6 +404,11 @@ namespace Microsoft.Z3
/// Backtrack level that can be adjusted by conquer process
///
public uint BacktrackLevel { get; set; }
+
+ ///
+ /// Variables available and returned by the cuber.
+ ///
+ public BoolExpr[] CubeVariables { get; set; }
///
@@ -411,16 +416,21 @@ namespace Microsoft.Z3
///
public IEnumerable Cube()
{
+ ASTVector cv = new ASTVector(Context);
+ if (CubeVariables != null)
+ foreach (var b in CubeVariables) cv.Push(b);
+
while (true) {
var lvl = BacktrackLevel;
BacktrackLevel = uint.MaxValue;
- ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl));
+ ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl));
var v = r.ToBoolExprArray();
+ CubeVariables = cv.ToBoolExprArray();
if (v.Length == 1 && v[0].IsFalse) {
break;
}
yield return v;
- if (v.Length == 0) {
+ if (v.Length == 0) {
break;
}
}
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index f15386a93..e16459fda 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6313,18 +6313,25 @@ class Solver(Z3PPObject):
consequences = [ consequences[i] for i in range(sz) ]
return CheckSatResult(r), consequences
- def cube(self):
+ def cube(self, vars = None):
"""Get set of cubes"""
+ self.cube_vs = AstVector(None, self.ctx)
+ if vars is not None:
+ for v in vars:
+ self.cube_vs.push(v)
while True:
lvl = self.backtrack_level
self.backtrack_level = 4000000000
- r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, lvl), self.ctx)
+ r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
if (len(r) == 1 and is_false(r[0])):
- return
- yield r
+ return
+ yield r
if (len(r) == 0):
return
+ def cube_vars(self):
+ return self.cube_vs
+
def proof(self):
"""Return a proof for the last `check()`. Proof construction must be enabled."""
return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index b212912b9..99d6021ef 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6230,13 +6230,20 @@ extern "C" {
The number of (non-constant) cubes is by default 1. For the sat solver cubing is controlled
using parameters sat.lookahead.cube.cutoff and sat.lookahead.cube.fraction.
+ The third argument is a vector of variables that may be used for cubing.
+ The contents of the vector is only used in the first call. The initial list of variables
+ is used in subsequent calls until it returns the unsatisfiable cube.
+ The vector is modified to contain a set of Autarky variables that occor in clauses that
+ are affected by the (last literal in the) cube. These variables could be used by a different
+ cuber (on a different solver object) for further recursive cubing.
+
The last argument is a backtracking level. It instructs the cube process to backtrack below
the indicated level for the next cube.
- def_API('Z3_solver_cube', AST_VECTOR, (_in(CONTEXT), _in(SOLVER), _in(UINT)))
+ def_API('Z3_solver_cube', AST_VECTOR, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(UINT)))
*/
- Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, unsigned backtrack_level);
+ Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level);
/**
\brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions
diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h
index 84469f490..55c1711c3 100644
--- a/src/muz/spacer/spacer_itp_solver.h
+++ b/src/muz/spacer/spacer_itp_solver.h
@@ -119,7 +119,7 @@ public:
{NOT_IMPLEMENTED_YET();}
virtual void assert_lemma(expr* e) { NOT_IMPLEMENTED_YET(); }
virtual expr_ref lookahead(const expr_ref_vector &,const expr_ref_vector &) { return expr_ref(m.mk_true(), m); }
- virtual expr_ref_vector cube(unsigned) { return expr_ref_vector(m); }
+ virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { return expr_ref_vector(m); }
virtual void push();
diff --git a/src/muz/spacer/spacer_virtual_solver.h b/src/muz/spacer/spacer_virtual_solver.h
index 946df95ad..c7dfd3c11 100644
--- a/src/muz/spacer/spacer_virtual_solver.h
+++ b/src/muz/spacer/spacer_virtual_solver.h
@@ -94,7 +94,7 @@ public:
virtual void reset();
virtual void set_progress_callback(progress_callback *callback) {UNREACHABLE();}
- virtual expr_ref_vector cube(unsigned) { return expr_ref_vector(m); }
+ virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { return expr_ref_vector(m); }
virtual solver *translate(ast_manager &m, params_ref const &p);
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 117b65c5a..5fa87b3ba 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -285,10 +285,12 @@ public:
m_last_index = 0;
bool first = index > 0;
SASSERT(index < asms.size() || asms.empty());
+ IF_VERBOSE(1, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);
while (index < asms.size() && is_sat == l_true) {
while (!first && asms.size() > 20*(index - m_last_index) && index < asms.size()) {
index = next_index(asms, index);
}
+ IF_VERBOSE(1, verbose_stream() << "hill climb " << index << "\n";);
first = false;
// IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";);
m_last_index = index;
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 9d1eccb38..4d2f39416 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -108,7 +108,7 @@ namespace opt {
virtual ast_manager& get_manager() const { return m; }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes);
virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores);
- virtual expr_ref_vector cube(unsigned) { return expr_ref_vector(m); }
+ virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { return expr_ref_vector(m); }
void set_logic(symbol const& logic);
smt::theory_var add_objective(app* term);
diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 6d06a3a2e..8211c4760 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -72,7 +72,7 @@ namespace sat {
unsigned elim = m_elim_literals;
if (big) big->init_big(s, true);
process(big, s.m_clauses);
- process(big, s.m_learned);
+ if (big) process(big, s.m_learned);
s.propagate(false);
if (s.m_inconsistent)
break;
diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h
index b18c549ac..6790bd963 100644
--- a/src/sat/sat_asymm_branch.h
+++ b/src/sat/sat_asymm_branch.h
@@ -42,7 +42,6 @@ namespace sat {
unsigned m_asymm_branch_rounds;
unsigned m_asymm_branch_delay;
bool m_asymm_branch_sampled;
- bool m_asymm_branch_propagate;
bool m_asymm_branch_all;
int64 m_asymm_branch_limit;
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 361e15d91..09610a3a7 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -136,6 +136,7 @@ namespace sat {
m_gc_increment = p.gc_increment();
m_gc_small_lbd = p.gc_small_lbd();
m_gc_k = std::min(255u, p.gc_k());
+ m_gc_burst = p.gc_burst();
m_minimize_lemmas = p.minimize_lemmas();
m_core_minimize = p.core_minimize();
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index a8eb09278..270ae9d04 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -181,9 +181,9 @@ namespace sat {
for (bool_var v : to_elim) {
literal l(v, false);
literal r = roots[v];
- SASSERT(v != r.var());
- if (m_solver.is_external(v)) {
- m_solver.set_root(l, r);
+ SASSERT(v != r.var());
+ bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r);
+ if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) {
// cannot really eliminate v, since we have to notify extension of future assignments
m_solver.mk_bin_clause(~l, r, false);
m_solver.mk_bin_clause(l, ~r, false);
diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
index f9f06f222..f04318a5d 100644
--- a/src/sat/sat_elim_vars.cpp
+++ b/src/sat/sat_elim_vars.cpp
@@ -122,17 +122,17 @@ namespace sat{
bdd b = m.mk_exists(m_var2index[v], b0);
TRACE("elim_vars",
tout << "eliminate " << v << "\n";
- /*for (watched const& w : simp.get_wlist(~pos_l)) {
- if (w.is_binary_unblocked_clause()) {
+ for (watched const& w : simp.get_wlist(~pos_l)) {
+ if (w.is_binary_non_learned_clause()) {
tout << pos_l << " " << w.get_literal() << "\n";
}
- }*/
+ }
m.display(tout, b1);
- /*for (watched const& w : simp.get_wlist(~neg_l)) {
- if (w.is_binary_unblocked_clause()) {
+ for (watched const& w : simp.get_wlist(~neg_l)) {
+ if (w.is_binary_non_learned_clause()) {
tout << neg_l << " " << w.get_literal() << "\n";
}
- }*/
+ }
m.display(tout, b2);
clause_use_list::iterator itp = pos_occs.mk_iterator();
while (!itp.at_end()) {
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 31a9f12e9..f3d4a3125 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -338,7 +338,7 @@ namespace sat {
}
TRACE("sat", display_candidates(tout << "sum: " << sum << "\n"););
if (skip_candidates > 0) {
- IF_VERBOSE(0, verbose_stream() << "candidates: " << m_candidates.size() << " skip: " << skip_candidates << "\n";);
+ IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :candidates " << m_candidates.size() << " :skipped " << skip_candidates << ")\n";);
}
return sum;
}
@@ -2050,15 +2050,15 @@ namespace sat {
return h;
}
- lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
+ lbool lookahead::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
scoped_ext _scoped_ext(*this);
lits.reset();
- m_select_lookahead_vars.reset();
- for (auto v : vars) {
- m_select_lookahead_vars.insert(v);
- }
bool is_first = m_cube_state.m_first;
if (is_first) {
+ m_select_lookahead_vars.reset();
+ for (auto v : vars) {
+ m_select_lookahead_vars.insert(v);
+ }
init_search();
m_model.reset();
m_cube_state.m_first = false;
@@ -2111,6 +2111,8 @@ namespace sat {
#else
lits.append(m_cube_state.m_cube);
#endif
+ vars.reset();
+ for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
return l_undef;
}
@@ -2126,6 +2128,8 @@ namespace sat {
continue;
}
if (lit == null_literal) {
+ vars.reset();
+ for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
return l_true;
}
TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";);
@@ -2248,40 +2252,6 @@ namespace sat {
return l;
}
-
- literal lookahead::select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars) {
- IF_VERBOSE(1, verbose_stream() << "(sat-select " << vars.size() << ")\n";);
- scoped_ext _sext(*this);
- m_search_mode = lookahead_mode::searching;
- scoped_level _sl(*this, c_fixed_truth);
- init();
- if (inconsistent()) return null_literal;
- inc_istamp();
- for (auto v : vars) {
- m_select_lookahead_vars.insert(v);
- }
-
- scoped_assumptions _sa(*this, assumptions);
- literal l = choose();
- m_select_lookahead_vars.reset();
- if (inconsistent()) l = null_literal;
-
-#if 0
- // assign unit literals that were found during search for lookahead.
- if (assumptions.empty()) {
- unsigned num_assigned = 0;
- for (literal lit : m_trail) {
- if (!m_s.was_eliminated(lit.var()) && m_s.value(lit) != l_true) {
- m_s.assign(lit, justification());
- ++num_assigned;
- }
- }
- IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_assigned << ")\n";);
- }
-#endif
- return l;
- }
-
/**
\brief simplify set of clauses by extracting units from a lookahead at base level.
*/
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 6a7bb7449..3ebbfb7a5 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -587,15 +587,14 @@ namespace sat {
/**
\brief create cubes to std-out in DIMACS form.
The cubes are controlled using cut-depth and cut-fraction parameters.
- If cut-depth != 0, then it is used to control the depth of cuts.
+ If cut-depth != 0, then it is used to control thedepth of cuts.
Otherwise, cut-fraction gives an adaptive threshold for creating cuts.
*/
- lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
+ lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level);
void update_cube_statistics(statistics& st);
- literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
/**
\brief simplify set of clauses by extracting units from a lookahead at base level.
*/
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 2c0a0973a..a52ab4c8d 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -60,6 +60,7 @@ namespace sat {
m_next_simplify = 0;
m_num_checkpoints = 0;
m_simplifications = 0;
+ m_ext = 0;
m_cuber = nullptr;
m_mc.set_solver(this);
}
@@ -861,12 +862,7 @@ namespace sat {
return r;
}
- literal solver::select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars) {
- lookahead lh(*this);
- return lh.select_lookahead(assumptions, vars);
- }
-
- lbool solver::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
+ lbool solver::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
if (!m_cuber) {
m_cuber = alloc(lookahead, *this);
}
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 8f70086ba..bac9c4bb3 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -355,10 +355,10 @@ namespace sat {
bool check_clauses(model const& m) const;
bool is_assumption(bool_var v) const;
- literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
- lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
+ lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level);
protected:
+
unsigned m_conflicts_since_init;
unsigned m_restarts;
unsigned m_conflicts_since_restart;
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 6802b7373..d731c246c 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -67,12 +67,12 @@ class inc_sat_solver : public solver {
std::string m_unknown;
// access formulas after they have been pre-processed and handled by the sat solver.
// this allows to access the internal state of the SAT solver and carry on partial results.
- bool m_internalized; // are formulas internalized?
bool m_internalized_converted; // have internalized formulas been converted back
expr_ref_vector m_internalized_fmls; // formulas in internalized format
-
typedef obj_map dep2asm_t;
+
+ bool is_internalized() const { return m_fmls_head == m_fmls.size(); }
public:
inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode):
m(m),
@@ -84,7 +84,6 @@ public:
m_map(m),
m_num_scopes(0),
m_unknown("no reason given"),
- m_internalized(false),
m_internalized_converted(false),
m_internalized_fmls(m) {
updt_params(p);
@@ -94,7 +93,6 @@ public:
bool override_incremental() const {
sat_simplifier_params p(m_params);
- //std::cout << "override: " << p.override_incremental() << "\n";
return p.override_incremental();
}
@@ -124,7 +122,6 @@ public:
if (m_mc0) result->m_mc0 = m_mc0->translate(tr);
//if (m_sat_mc) result->m_sat_mc = m_sat_mc->translate(tr); MN: commenting this line removes bloat
// copy m_bb_rewriter?
- result->m_internalized = m_internalized;
result->m_internalized_converted = m_internalized_converted;
return result;
}
@@ -188,8 +185,6 @@ public:
if (r != l_true) return r;
r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm);
if (r != l_true) return r;
- m_internalized = true;
- m_internalized_converted = false;
init_reason_unknown();
try {
@@ -226,11 +221,8 @@ public:
m_fmls_head_lim.push_back(m_fmls_head);
if (m_bb_rewriter) m_bb_rewriter->push();
m_map.push();
- m_internalized = true;
- m_internalized_converted = false;
}
virtual void pop(unsigned n) {
- m_internalized = false;
if (n > m_num_scopes) { // allow inc_sat_solver to
n = m_num_scopes; // take over for another solver.
}
@@ -264,7 +256,6 @@ public:
virtual ast_manager& get_manager() const { return m; }
virtual void assert_expr_core(expr * t) {
- m_internalized = false;
TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
m_fmls.push_back(t);
}
@@ -305,18 +296,19 @@ public:
return 0;
}
- virtual expr_ref_vector cube(unsigned backtrack_level) {
- if (!m_internalized) {
- dep2asm_t dep2asm;
+ virtual expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) {
+ if (!is_internalized()) {
m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return expr_ref_vector(m);
- m_internalized = true;
}
convert_internalized();
+ obj_hashtable _vs;
+ for (expr* v : vs) _vs.insert(v);
sat::bool_var_vector vars;
for (auto& kv : m_map) {
- vars.push_back(kv.m_value);
+ if (_vs.empty() || _vs.contains(kv.m_key))
+ vars.push_back(kv.m_value);
}
sat::literal_vector lits;
lbool result = m_solver.cube(vars, lits, backtrack_level);
@@ -327,7 +319,7 @@ public:
}
if (result == l_true) {
return expr_ref_vector(m);
- }
+ }
expr_ref_vector fmls(m);
expr_ref_vector lit2expr(m);
lit2expr.resize(m_solver.num_vars() * 2);
@@ -335,6 +327,13 @@ public:
for (sat::literal l : lits) {
fmls.push_back(lit2expr[l.index()].get());
}
+ vs.reset();
+ for (sat::bool_var v : vars) {
+ expr* x = lit2expr[sat::literal(v, false).index()].get();
+ if (x) {
+ vs.push_back(x);
+ }
+ }
return fmls;
}
@@ -419,7 +418,7 @@ public:
}
virtual unsigned get_num_assertions() const {
const_cast(this)->convert_internalized();
- if (m_internalized && m_internalized_converted) {
+ if (is_internalized() && m_internalized_converted) {
return m_internalized_fmls.size();
}
else {
@@ -427,7 +426,7 @@ public:
}
}
virtual expr * get_assertion(unsigned idx) const {
- if (m_internalized && m_internalized_converted) {
+ if (is_internalized() && m_internalized_converted) {
return m_internalized_fmls[idx];
}
return m_fmls[idx];
@@ -443,7 +442,7 @@ public:
const_cast(this)->convert_internalized();
if (m_cached_mc)
return m_cached_mc;
- if (m_internalized && m_internalized_converted) {
+ if (is_internalized() && m_internalized_converted) {
m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
@@ -455,7 +454,10 @@ public:
}
void convert_internalized() {
- if (!m_internalized || m_internalized_converted) return;
+ if (!is_internalized() && m_fmls_head > 0) {
+ internalize_formulas();
+ }
+ if (!is_internalized() || m_internalized_converted) return;
sat2goal s2g;
m_cached_mc = nullptr;
goal g(m, false, true, false);
@@ -679,6 +681,7 @@ private:
if (res != l_undef) {
m_fmls_head = m_fmls.size();
}
+ m_internalized_converted = false;
return res;
}
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 01ea61fd9..3449ad480 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -222,7 +222,7 @@ namespace smt {
return expr_ref(m.mk_true(), m);
}
- virtual expr_ref_vector cube(unsigned) {
+ virtual expr_ref_vector cube(expr_ref_vector&, unsigned) {
return expr_ref_vector(get_manager());
}
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 29f6a32f1..713009cd6 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -275,8 +275,8 @@ public:
return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions();
}
- virtual expr_ref_vector cube(unsigned backtrack_level) {
- return m_solver1->cube(backtrack_level);
+ virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) {
+ return m_solver1->cube(vars, backtrack_level);
}
virtual expr * get_assumption(unsigned idx) const {
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 7a51725a2..bc6ffb0e0 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -47,7 +47,7 @@ class solver : public check_sat_result {
params_ref m_params;
bool m_enforce_model_conversion;
public:
- solver(): m_enforce_model_conversion(true) {}
+ solver(): m_enforce_model_conversion(false) {}
virtual ~solver() {}
/**
@@ -190,7 +190,7 @@ public:
\brief extract a lookahead candidates for branching.
*/
- virtual expr_ref_vector cube(unsigned backtrack_level) = 0;
+ virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) = 0;
/**
\brief Display the content of this solver.
diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp
index 1b7203351..2f6a22580 100644
--- a/src/solver/solver_pool.cpp
+++ b/src/solver/solver_pool.cpp
@@ -223,7 +223,7 @@ public:
virtual void get_labels(svector & r) { return m_base->get_labels(r); }
virtual void set_progress_callback(progress_callback * callback) { m_base->set_progress_callback(callback); }
- virtual expr_ref_vector cube(unsigned ) { return expr_ref_vector(m); }
+ virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned ) { return expr_ref_vector(m); }
virtual ast_manager& get_manager() const { return m_base->get_manager(); }
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 4585af65e..cbe6b34a9 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -77,7 +77,7 @@ public:
virtual ast_manager& get_manager() const;
- virtual expr_ref_vector cube(unsigned ) {
+ virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned ) {
return expr_ref_vector(get_manager());
}
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index b8a8f6704..c81d413b8 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -162,7 +162,7 @@ public:
virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
virtual void get_labels(svector & r) { m_solver->get_labels(r); }
virtual ast_manager& get_manager() const { return m; }
- virtual expr_ref_vector cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); }
+ virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { flush_assertions(); return m_solver->cube(vars, backtrack_level); }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
flush_assertions();
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index ffb51fe2e..bfe057f82 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -103,7 +103,7 @@ public:
virtual void get_labels(svector & r) { m_solver->get_labels(r); }
virtual ast_manager& get_manager() const { return m; }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
- virtual expr_ref_vector cube(unsigned backtrack_level) { return m_solver->cube(backtrack_level); }
+ virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { return m_solver->cube(vars, backtrack_level); }
virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
datatype_util dt(m);
diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp
index 8e14d77e2..f4982c2c2 100644
--- a/src/tactic/portfolio/parallel_tactic.cpp
+++ b/src/tactic/portfolio/parallel_tactic.cpp
@@ -414,7 +414,8 @@ private:
cubes.reset();
s.set_cube_params();
while (true) {
- expr_ref_vector c = s.get_solver().cube(UINT_MAX); // TBD tune this
+ 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);
return;
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index cb5327443..eba10cbd1 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -100,7 +100,7 @@ public:
virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
virtual void get_labels(svector & r) { m_solver->get_labels(r); }
virtual ast_manager& get_manager() const { return m; }
- virtual expr_ref_vector cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); }
+ virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { flush_assertions(); return m_solver->cube(vars, backtrack_level); }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
flush_assertions();