mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

minor simplification during internalization

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-03 12:43:39 -08:00
parent 36725383d3
commit 1b1ebaa3b0
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/arith_solver.h
View file

@ -292,10 +292,11 @@ namespace arith {
theory_var internalize_linearized_def(expr* term, scoped_internalize_state& st); theory_var internalize_linearized_def(expr* term, scoped_internalize_state& st);
void init_left_side(scoped_internalize_state& st); void init_left_side(scoped_internalize_state& st);
bool internalize_term(expr* term); bool internalize_term(expr* term);
bool internalize_atom(expr* atom); bool internalize_atom(expr* atom);
bool is_unit_var(scoped_internalize_state& st); bool is_unit_var(scoped_internalize_state& st);
bool is_one(scoped_internalize_state& st); bool is_one(scoped_internalize_state& st);
bool is_zero(scoped_internalize_state& st); bool is_zero(scoped_internalize_state& st);
expr* mk_sub(expr* a, expr* b);
enode* mk_enode(expr* e); enode* mk_enode(expr* e);
lpvar register_theory_var_in_lar_solver(theory_var v); lpvar register_theory_var_in_lar_solver(theory_var v);