mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

after rebase

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-06-27 15:20:25 -07:00
parent efa149bed1
commit 7b59e2094d
5 changed files with 17 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_lra.cpp
View file

@ -36,7 +36,7 @@
#include "smt/arith_eq_adapter.h"
#include "util/nat_set.h"
#include "util/lp/nra_solver.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "math/polynomial/algebraic_numbers.h"
#include "math/polynomial/polynomial.h"
#include "ast/ast_pp.h"
@ -2770,7 +2770,7 @@ public:
}
}
expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val) {
expr_ref mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) {
rational r = val.get_rational();
bool is_strict = val.get_infinitesimal().is_pos();
app_ref b(m);
@ -2782,7 +2782,7 @@ public:
b = a.mk_ge(mk_obj(v), a.mk_numeral(r, is_int));
}
if (!ctx().b_internalized(b)) {
fm.insert(b->get_decl());
fm.hide(b->get_decl());
bool_var bv = ctx().mk_bool_var(b);
ctx().set_var_theory(bv, get_id());
// ctx().set_enode_flag(bv, true);
@ -2983,7 +2983,7 @@ theory_lra::inf_eps theory_lra::maximize(theory_var v, expr_ref& blocker, bool&
theory_var theory_lra::add_objective(app* term) {
return m_imp->add_objective(term);
}
expr_ref theory_lra::mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val) {
expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) {
return m_imp->mk_ge(fm, v, val);
}