mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-22 23:15:51 +00:00
Code Activity

update

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-03 11:58:22 -07:00
parent 1c11526d64
commit 4a52f32c6b
2 changed files with 6 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/seq_regex.h
View file

@ -225,10 +225,9 @@ namespace smt {
seq_regex(theory_seq& th); seq_regex(theory_seq& th);
void push_scope() {} bool final_check() {
void pop_scope(unsigned num_scopes) {} return true;
bool can_propagate() const { return false; } }
bool propagate() const { return false; }
void propagate_in_re(literal lit); void propagate_in_re(literal lit);

10
src/smt/theory_seq.cpp
View file

@ -341,8 +341,8 @@ final_check_status theory_seq::final_check_eh(unsigned level) {
TRACEFIN("solve_nqs"); TRACEFIN("solve_nqs");
return FC_CONTINUE; return FC_CONTINUE;
} }
if (m_regex.propagate()) { if (!m_regex.final_check()) {
TRACEFIN("regex propagate"); TRACEFIN("regex final check");
return FC_CONTINUE; return FC_CONTINUE;
} }
if (check_fixed_length(true, false)) { if (check_fixed_length(true, false)) {
@ -2473,7 +2473,7 @@ theory_var theory_seq::mk_var(enode* n) {
} }
bool theory_seq::can_propagate() { bool theory_seq::can_propagate() {
return m_axioms_head < m_axioms.size() || !m_replay.empty() || m_new_solution || m_regex.can_propagate(); return m_axioms_head < m_axioms.size() || !m_replay.empty() || m_new_solution;
} }
bool theory_seq::canonize(expr* e, dependency*& eqs, expr_ref& result) { bool theory_seq::canonize(expr* e, dependency*& eqs, expr_ref& result) {
@ -2689,8 +2689,6 @@ void theory_seq::add_dependency(dependency*& dep, enode* a, enode* b) {
void theory_seq::propagate() { void theory_seq::propagate() {
if (m_regex.can_propagate())
m_regex.propagate();
while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) { while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
expr_ref e(m); expr_ref e(m);
e = m_axioms.get(m_axioms_head); e = m_axioms.get(m_axioms_head);
@ -3261,7 +3259,6 @@ void theory_seq::push_scope_eh() {
m_ncs.push_scope(); m_ncs.push_scope();
m_lts.push_scope(); m_lts.push_scope();
m_recfuns.push_scope(); m_recfuns.push_scope();
m_regex.push_scope();
} }
void theory_seq::pop_scope_eh(unsigned num_scopes) { void theory_seq::pop_scope_eh(unsigned num_scopes) {
@ -3275,7 +3272,6 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
m_ncs.pop_scope(num_scopes); m_ncs.pop_scope(num_scopes);
m_lts.pop_scope(num_scopes); m_lts.pop_scope(num_scopes);
m_recfuns.pop_scope(num_scopes); m_recfuns.pop_scope(num_scopes);
m_regex.pop_scope(num_scopes);
m_rewrite.reset(); m_rewrite.reset();
if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) { if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) {
m_replay.reset(); m_replay.reset();