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

remove lattice component

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-02-19 15:49:45 -08:00
parent 5bd7d93b55
commit 38ce0882db
5 changed files with 1 additions and 409 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_finite_set.cpp
View file

@ -28,8 +28,7 @@ namespace smt {
theory(ctx, ctx.get_manager().mk_family_id("finite_set")),
u(m),
m_axioms(m), m_rw(m), m_find(*this),
m_cardinality_solver(*this),
m_lattice_refutation(*this)
m_cardinality_solver(*this)
{
// Setup the add_clause callback for axioms
std::function<void(theory_axiom *)> add_clause_fn =
@ -260,8 +259,6 @@ namespace smt {
ctx.push_trail(push_back_vector(m_eqs));
m_find.merge(v1, v2); // triggers merge_eh, which triggers incremental generation of theory axioms
}
if (ctx.get_fparams().m_finite_set_lattice_refutation)
m_lattice_refutation.add_equality(v1, v2);
// Check if Z3 has a boolean variable for it
TRACE(finite_set, tout << "new_eq_eh_r1: " << n1->get_root() << "r2: "<< n2->get_root() <<"\n";);
@ -288,8 +285,6 @@ namespace smt {
ctx.push_trail(push_back_vector(m_diseqs));
m_axioms.extensionality_axiom(e1, e2);
}
if (ctx.get_fparams().m_finite_set_lattice_refutation)
m_lattice_refutation.add_disequality(v1,v2);
}
//