mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix #3511

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 11:13:28 -07:00
parent 696a178c08
commit 43e7242e35
2 changed files with 16 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast_ll_pp.cpp
View file

@ -42,11 +42,7 @@ class ll_printer {
}
void display_name(func_decl * decl) {
symbol n = decl->get_name();
if (decl->is_skolem() && n.is_numerical())
m_out << "z3.sk." << n.get_num();
else
m_out << n;
m_out << decl->get_name();
}
bool process_numeral(expr * n) {

23
src/smt/theory_lra.cpp
View file

@ -695,8 +695,10 @@ class theory_lra::imp {
if (!_has_var) {
svector<lpvar> vars;
for (expr* n : *t) {
if (is_app(n)) VERIFY(internalize_term(to_app(n)));
SASSERT(ctx().e_internalized(n));
vars.push_back(register_theory_var_in_lar_solver(mk_var(n)));
theory_var v = mk_var(n);
vars.push_back(register_theory_var_in_lar_solver(v));
}
TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";);
m_solver->register_existing_terms();
@ -769,8 +771,8 @@ class theory_lra::imp {
enode* e = get_enode(n);
theory_var v;
if (!th.is_attached_to_var(e)) {
TRACE("arith", tout << "fresh var: " << mk_pp(n, m) << "\n";);
v = th.mk_var(e);
TRACE("arith", tout << "fresh var: v" << v << " " << mk_pp(n, m) << "\n";);
SASSERT(m_bounds.size() <= static_cast<unsigned>(v) || m_bounds[v].empty());
if (m_bounds.size() <= static_cast<unsigned>(v)) {
m_bounds.push_back(lp_bounds());
@ -875,13 +877,15 @@ class theory_lra::imp {
theory_var z = internalize_linearized_def(term, st);
lpvar vi = register_theory_var_in_lar_solver(z);
add_def_constraint(lp().add_var_bound(vi, lp::LE, rational::zero()));
// if (is_infeasible()) {
if (is_infeasible()) {
IF_VERBOSE(0, verbose_stream() << "infeasible\n";);
// process_conflict(); // exit here?
// }
}
add_def_constraint(lp().add_var_bound(vi, lp::GE, rational::zero()));
// if (is_infeasible()) {
// process_conflict();
// }
if (is_infeasible()) {
IF_VERBOSE(0, verbose_stream() << "infeasible\n";);
// process_conflict(); // exit here?
}
TRACE("arith",
{
expr* o1 = get_enode(v1)->get_owner();
@ -969,7 +973,7 @@ class theory_lra::imp {
}
theory_var v = mk_var(term);
lpvar vi = get_lpvar(v);
TRACE("arith", tout << mk_bounded_pp(term, m) << " v" << v << " vi " << vi << "\n";);
TRACE("arith", tout << mk_bounded_pp(term, m) << " v" << v << " j" << vi << "\n";);
if (vi == UINT_MAX) {
rational const& offset = st.offset();
if (!offset.is_zero()) {
@ -981,6 +985,9 @@ class theory_lra::imp {
TRACE("arith_verbose", tout << "v" << v << " := " << mk_pp(term, m) << " slack: " << vi << " scopes: " << m_scopes.size() << "\n";
lp().print_term(lp().get_term(vi), tout) << "\n";);
}
else {
SASSERT(lp::tv::is_term(vi));
}
rational val;
if (a.is_numeral(term, val)) {
m_fixed_var_table.insert(value_sort_pair(val, is_int(v)), v);