mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add virtual function requirement to dependent_expr_state

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-19 18:46:31 +07:00
parent dcc995f0e5
commit a81a5ec68c
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/simplifiers/dependent_expr_state.h
View file

@ -46,6 +46,7 @@ public:
virtual unsigned size() const = 0; virtual unsigned size() const = 0;
virtual dependent_expr const& operator[](unsigned i) = 0; virtual dependent_expr const& operator[](unsigned i) = 0;
virtual void update(unsigned i, dependent_expr const& j) = 0; virtual void update(unsigned i, dependent_expr const& j) = 0;
virtual void add(dependent_expr const& j) = 0;
virtual bool inconsistent() = 0; virtual bool inconsistent() = 0;
virtual model_reconstruction_trail& model_trail() = 0; virtual model_reconstruction_trail& model_trail() = 0;

6
src/tactic/dependent_expr_state_tactic.h
View file

@ -60,10 +60,16 @@ public:
m_dep = dependent_expr(m, m_goal->form(i), m_goal->dep(i)); m_dep = dependent_expr(m, m_goal->form(i), m_goal->dep(i));
return m_dep; return m_dep;
} }
void update(unsigned i, dependent_expr const& j) override { void update(unsigned i, dependent_expr const& j) override {
auto [f, d] = j(); auto [f, d] = j();
m_goal->update(i, f, nullptr, d); m_goal->update(i, f, nullptr, d);
} }
void add(dependent_expr const& j) override {
auto [f, d] = j();
m_goal->assert_expr(f, nullptr, d);
}
bool inconsistent() override { bool inconsistent() override {
return m_goal->inconsistent(); return m_goal->inconsistent();