mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-27 22:33:35 +00:00
Code Activity

Added unit (not char) case in apply_const_nielsen

Browse source
This commit is contained in:
CEisenhofer 2026-03-24 13:34:39 +01:00
parent b74f0bbb00
commit 538fbc1b8d
2 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2011,7 +2011,7 @@ namespace seq {
// char vs var: branch 1: var -> ε, branch 2: var -> char·var (depending on direction) // char vs var: branch 1: var -> ε, branch 2: var -> char·var (depending on direction)
// NSB review: add also case var -> unit·var // NSB review: add also case var -> unit·var
euf::snode* char_head = lhead->is_char() ? lhead : (rhead->is_char() ? rhead : nullptr); euf::snode* char_head = (lhead->is_char() || lhead->is_unit()) ? lhead : ((rhead->is_char() || rhead->is_unit()) ? rhead : nullptr);
euf::snode* var_head = lhead->is_var() ? lhead : (rhead->is_var() ? rhead : nullptr); euf::snode* var_head = lhead->is_var() ? lhead : (rhead->is_var() ? rhead : nullptr);
if (char_head && var_head) { if (char_head && var_head) {
nielsen_node* child = mk_child(node); nielsen_node* child = mk_child(node);

4
src/smt/theory_nseq.cpp
View file

@ -185,9 +185,7 @@ namespace smt {
if (s1 && s2) { if (s1 && s2) {
seq::dep_tracker dep = nullptr; seq::dep_tracker dep = nullptr;
ctx.push_trail(restore_vector(m_prop_queue)); ctx.push_trail(restore_vector(m_prop_queue));
m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep));}
std::cout << "Enqueuing equation " << seq::snode_label_html(s1, m) << " = " << seq::snode_label_html(s2, m) << std::endl;
}
} }
void theory_nseq::new_diseq_eh(theory_var v1, theory_var v2) { void theory_nseq::new_diseq_eh(theory_var v1, theory_var v2) {