mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-23 04:49:11 +00:00
Code Activity

add reset method

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-19 22:57:59 -07:00
parent a895548b99
commit 1d928663de
3 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/nseq_context_solver.h
View file

@ -68,6 +68,10 @@ namespace smt {
void get_model(model_ref& mdl) override {
m_kernel.get_model(mdl);
}
void reset() override {
m_kernel.reset();
}
};
}

5
src/smt/seq/seq_nielsen.cpp
View file

@ -538,8 +538,6 @@ namespace seq {
m_parikh(alloc(seq_parikh, sg)),
m_seq_regex(alloc(seq::seq_regex, sg)),
m_len_vars(sg.get_manager()) {
m_solver.push(); // we start by resetting the graph which will pop it first
}
nielsen_graph::~nielsen_graph() {
@ -635,8 +633,7 @@ namespace seq {
m_len_var_cache.clear();
m_len_vars.reset();
m_dep_mgr.reset();
m_solver.pop(1);
m_solver.push();
m_solver.reset();
}
std::ostream& nielsen_graph::display(std::ostream& out) const {

1
src/smt/seq/seq_nielsen.h
View file

@ -278,6 +278,7 @@ namespace seq {
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;
virtual void get_model(model_ref& mdl) { mdl = nullptr; }
virtual void reset() = 0;
};
// simplification result for constraint processing