Skip to content

Commit

Permalink
remove set_instance() from decision procedure
Browse files Browse the repository at this point in the history
  • Loading branch information
jurajsic committed May 26, 2023
1 parent 791c346 commit daa40de
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 28 deletions.
16 changes: 1 addition & 15 deletions src/smt/theory_str_noodler/decision_procedure.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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{};
Expand Down
13 changes: 0 additions & 13 deletions src/smt/theory_str_noodler/decision_procedure.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down

0 comments on commit daa40de

Please sign in to comment.