mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-01 12:58:54 +00:00
Code Activity

sort constraint

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-30 09:50:41 -07:00
parent b3143e759b
commit c85e2ee2bd
2 changed files with 3 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.h
View file

@ -880,9 +880,7 @@ namespace smt {
void undo_mk_enode();
void apply_sort_cnstr(app * term, enode * e);
void apply_sort_cnstr(quantifier *term, enode *e);
void apply_sort_cnstr(expr * term, enode * e);
bool simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits);

12
src/smt/smt_internalizer.cpp
View file

@ -1085,22 +1085,14 @@ namespace smt {
/**
\brief Apply sort constraints on e.
*/
void context::apply_sort_cnstr(app * term, enode * e) {
sort * s = term->get_decl()->get_range();
void context::apply_sort_cnstr(expr * term, enode * e) {
sort * s = term->get_sort();
theory * th = m_theories.get_plugin(s->get_family_id());
if (th) {
th->apply_sort_cnstr(e, s);
}
}
void context::apply_sort_cnstr(quantifier *lambda_term, enode *e) {
sort *s = lambda_term->get_sort();
theory *th = m_theories.get_plugin(s->get_family_id());
if (th) {
th->apply_sort_cnstr(e, s);
}
}
/**
\brief Return the literal associated with n.
*/