add virtual function requirement to dependent_expr_state

Z3Prover · Nov 19, 2022 · a81a5ec · a81a5ec
1 parent dcc995f
commit a81a5ec
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
@@ -46,6 +46,7 @@ class dependent_expr_state {
     virtual unsigned size() const = 0;
     virtual dependent_expr const& operator[](unsigned i) = 0;
     virtual void update(unsigned i, dependent_expr const& j) = 0;
+    virtual void add(dependent_expr const& j) = 0;
     virtual bool inconsistent() = 0;
     virtual model_reconstruction_trail& model_trail() = 0;
 

diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
@@ -60,10 +60,16 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         m_dep = dependent_expr(m, m_goal->form(i), m_goal->dep(i));
         return m_dep;
     }
+
     void update(unsigned i, dependent_expr const& j) override {
         auto [f, d] = j();
         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 {
         return m_goal->inconsistent();