mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

enable more simplification in case inequality triggers a change.

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-21 19:58:39 -07:00
parent 4e21e126a8
commit 8fac89cdcc
5 changed files with 63 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/tactic/dependent_expr_state_tactic.h
View file

@ -33,6 +33,7 @@ private:
expr_ref_vector m_frozen;
scoped_ptr<dependent_expr_simplifier> m_simp;
scoped_ptr<model_reconstruction_trail> m_model_trail;
bool m_updated = false;
void init() {
if (!m_simp) {
@ -75,6 +76,7 @@ public:
void update(unsigned i, dependent_expr const& j) override {
if (inconsistent())
return;
m_updated = true;
auto [f, p, d] = j();
m_goal->update(i, f, p, d);
}
@ -82,6 +84,7 @@ public:
void add(dependent_expr const& j) override {
if (inconsistent())
return;
m_updated = true;
auto [f, p, d] = j();
m_goal->assert_expr(f, p, d);
}
@ -96,6 +99,10 @@ public:
char const* name() const override { return m_simp ? m_simp->name() : "null"; }
bool updated() override { return m_updated; }
void reset_updated() override { m_updated = false; }
void updt_params(params_ref const& p) override {
m_params.append(p);
init();