mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 06:07:46 +00:00
Code Activity

Expose timestamp method in sls_context (#8347)

Browse source 
* Initial plan

* Expose timestamp method in sls_context

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-26 11:27:27 -08:00 • committed by GitHub
parent 4a29326eaa
commit 0a68837ef2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sls_context.h
View file

@ -86,6 +86,7 @@ namespace sls {
virtual void force_restart() = 0; virtual void force_restart() = 0;
virtual std::ostream& display(std::ostream& out) = 0; virtual std::ostream& display(std::ostream& out) = 0;
virtual reslimit& rlimit() = 0; virtual reslimit& rlimit() = 0;
virtual unsigned timestamp(sat::bool_var v) = 0;
}; };
class context { class context {
@ -195,6 +196,7 @@ namespace sls {
void shift_weights() { s.shift_weights(); } void shift_weights() { s.shift_weights(); }
bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); } bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); }
double reward(sat::bool_var v) { return s.reward(v); } double reward(sat::bool_var v) { return s.reward(v); }
unsigned timestamp(sat::bool_var v) { return s.timestamp(v); }
indexed_uint_set const& unsat() const { return s.unsat(); } indexed_uint_set const& unsat() const { return s.unsat(); }
indexed_uint_set const& unsat_vars() const { return s.unsat_vars(); } indexed_uint_set const& unsat_vars() const { return s.unsat_vars(); }
unsigned num_external_in_unsat_vars() const { return s.num_external_in_unsat_vars(); } unsigned num_external_in_unsat_vars() const { return s.num_external_in_unsat_vars(); }

1
src/ast/sls/sls_smt_plugin.h
View file

@ -186,5 +186,6 @@ namespace sls {
m_new_clause_added = true; m_new_clause_added = true;
} }
void force_restart() override { m_ddfw->force_restart(); } void force_restart() override { m_ddfw->force_restart(); }
unsigned timestamp(sat::bool_var v) override { return m_ddfw->timestamp(v); }
}; };
} }

1
src/ast/sls/sls_smt_solver.cpp
View file

@ -102,6 +102,7 @@ namespace sls {
void add_input_assertion(expr* f) { m_context.add_input_assertion(f); } void add_input_assertion(expr* f) { m_context.add_input_assertion(f); }
reslimit& rlimit() override { return m_ddfw.rlimit(); } reslimit& rlimit() override { return m_ddfw.rlimit(); }
void shift_weights() override { m_ddfw.shift_weights(); } void shift_weights() override { m_ddfw.shift_weights(); }
unsigned timestamp(sat::bool_var v) override { return m_ddfw.timestamp(v); }
void force_restart() override { m_ddfw.force_restart(); } void force_restart() override { m_ddfw.force_restart(); }

1
src/test/sls_test.cpp
View file

@ -37,6 +37,7 @@ namespace bv {
void force_restart() override {} void force_restart() override {}
std::ostream& display(std::ostream& out) override { return out; } std::ostream& display(std::ostream& out) override { return out; }
reslimit& rlimit() override { return m_limit; } reslimit& rlimit() override { return m_limit; }
unsigned timestamp(sat::bool_var v) override { return 0; }
}; };
class sls_test { class sls_test {