From daa40de3db744393e25ecd558ba3cc7b008e0e59 Mon Sep 17 00:00:00 2001
From: jurajsic <juraj.sic@outlook.com>
Date: Fri, 26 May 2023 14:03:07 +0200
Subject: [PATCH] remove set_instance() from decision procedure

---
 .../theory_str_noodler/decision_procedure.cpp    | 16 +---------------
 src/smt/theory_str_noodler/decision_procedure.h  | 13 -------------
 2 files changed, 1 insertion(+), 28 deletions(-)

diff --git a/src/smt/theory_str_noodler/decision_procedure.cpp b/src/smt/theory_str_noodler/decision_procedure.cpp
index cbea985d966..03399333c3d 100644
--- a/src/smt/theory_str_noodler/decision_procedure.cpp
+++ b/src/smt/theory_str_noodler/decision_procedure.cpp
@@ -853,21 +853,7 @@ namespace smt::noodler {
         res = expr_ref(this->m.mk_and(res, this->m_util_a.mk_ge(var, this->m_util_a.mk_int(0))), this->m);
         return res;
     }
-
-    /**
-     * @brief Set new instance for the decision procedure.
-     * 
-     * @param equalities Equalities
-     * @param init_aut_ass Initial automata assignment
-     * @param init_length_sensitive_vars Length sensitive vars
-     */
-    void DecisionProcedure::set_instance(const Formula &equalities, AutAssignment &init_aut_ass, const std::unordered_set<BasicTerm>& init_length_sensitive_vars) {
-        this->init_length_sensitive_vars = init_length_sensitive_vars;
-        this->formula = equalities;
-        this->init_aut_ass = init_aut_ass;
-        this->prep_handler = FormulaPreprocess(equalities, init_aut_ass, init_length_sensitive_vars, m_params);
-    }
-
+    
     void DecisionProcedure::add_str_lits_to_init_aut_ass() {
         size_t counter{ 0 };
         std::map<zstring, zstring> str_literals{};
diff --git a/src/smt/theory_str_noodler/decision_procedure.h b/src/smt/theory_str_noodler/decision_procedure.h
index 35e71378f69..5924defff18 100644
--- a/src/smt/theory_str_noodler/decision_procedure.h
+++ b/src/smt/theory_str_noodler/decision_procedure.h
@@ -380,19 +380,6 @@ namespace smt::noodler {
             init_aut_ass(init_aut_ass),
             m_params(par),
             len_eq_vars(len_eq_vars) { }
-        /**
-         * @brief Set new instance for the decision procedure.
-         * 
-         * @param equalities Equalities
-         * @param init_aut_ass Initial automata assignment
-         * @param init_length_sensitive_vars Length sensitive vars
-         */
-        void set_instance(Formula equalities, AutAssignment init_aut_ass, std::unordered_set<BasicTerm> init_length_sensitive_vars) {
-            this->init_length_sensitive_vars = init_length_sensitive_vars;
-            this->formula = equalities;
-            this->init_aut_ass = init_aut_ass;
-            this->prep_handler = FormulaPreprocess(equalities, init_aut_ass, init_length_sensitive_vars, m_params);
-        }
         
         bool compute_next_solution() override;