mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 05:16:08 +00:00
Code Activity

handle more cass with intervals

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-05 11:49:35 -07:00
parent 120b4e4712
commit f40eb62e83
2 changed files with 100 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_derive.h
View file

@ -122,8 +122,8 @@ namespace seq {
expr_ref simplify_ite(expr* d);
expr_ref simplify_ite_rec(path_t& path, intervals_t& intervals, expr* d);
std::pair<expr_ref, expr_ref> simplify_ite_rec(path_t& path, intervals_t& intervals, expr* c, expr* t, expr* e);
void push_path(path_t& path, expr* c, bool sign);
void push_intervals(intervals_t& intervals, expr* c, bool sign);
lbool push_path(path_t& path, expr* c, bool sign);
lbool push_intervals(intervals_t& intervals, expr* c, bool sign);
lbool eval_cond(expr* cond);
lbool eval_range_cond(intervals_t const& intervals, expr* c);
static void intersect_intervals(unsigned lo, unsigned hi, intervals_t& ranges);