mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 22:36:10 +00:00
Code Activity

classical

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-03 10:33:28 -07:00
parent cdccd389e9
commit b60a44c66b
3 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/euf/euf_sgraph.cpp
View file

@ -132,6 +132,7 @@ namespace euf {
n->m_nullable = false; n->m_nullable = false;
n->m_level = 1; n->m_level = 1;
n->m_length = 1; n->m_length = 1;
n->m_is_classical = false;
break; break;
case snode_kind::s_unit: case snode_kind::s_unit:
@ -286,6 +287,7 @@ namespace euf {
default: default:
// NSB review: is this the correct defaults for unclassified nodes? // NSB review: is this the correct defaults for unclassified nodes?
// Is this UNREACHABLE()?
n->m_ground = true; n->m_ground = true;
n->m_regex_free = true; n->m_regex_free = true;
n->m_nullable = false; n->m_nullable = false;

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

@ -162,7 +162,7 @@ namespace seq {
// ----------------------------------------------- // -----------------------------------------------
bool str_mem::is_primitive() const { bool str_mem::is_primitive() const {
return m_str && m_str->length() == 1 && m_str->is_var(); return m_str && m_str->length() == 1 && m_str->is_var() && m_regex->is_ground();
} }
bool str_mem::is_trivial() const { bool str_mem::is_trivial() const {
@ -2241,12 +2241,12 @@ namespace seq {
// Priority 7: GPowerIntr - ground power introduction // Priority 7: GPowerIntr - ground power introduction
if (apply_gpower_intr(node)) if (apply_gpower_intr(node))
return ++m_stats.m_mod_gpower_intr, true; return ++m_stats.m_mod_gpower_intr, true;
// Priority 7b: Regex Factorization (Boolean Closure) // Priority 8: Regex Factorization (Boolean Closure)
if (apply_regex_factorization(node)) if (apply_regex_factorization(node))
return ++m_stats.m_mod_regex_factorization, true; return ++m_stats.m_mod_regex_factorization, true;
// Priority 8: ConstNielsen - char vs var (2 children) // Priority 8b: ConstNielsen - char vs var (2 children)
if (apply_const_nielsen(node)) if (apply_const_nielsen(node))
return ++m_stats.m_mod_const_nielsen, true; return ++m_stats.m_mod_const_nielsen, true;

3
src/smt/seq_model.cpp
View file

@ -30,6 +30,8 @@ namespace smt {
{} {}
void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen) { void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen) {
TRACE(seq, nielsen.display(tout << nielsen.to_dot() << "\n"));
m_var_values.reset(); m_var_values.reset();
m_var_regex.reset(); m_var_regex.reset();
m_trail.reset(); m_trail.reset();
@ -50,6 +52,7 @@ namespace smt {
// extract variable assignments from the satisfying leaf's substitution path // extract variable assignments from the satisfying leaf's substitution path
extract_assignments(nielsen.sat_path()); extract_assignments(nielsen.sat_path());
} }
model_value_proc* seq_model::mk_value(enode* n, model_generator& mg) { model_value_proc* seq_model::mk_value(enode* n, model_generator& mg) {