From 42726171b54b3eb4704cf7a055cb3578d0453033 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 May 2016 11:34:48 -0700 Subject: [PATCH] add limit checks in Grobner. Issue #599 Signed-off-by: Nikolaj Bjorner --- src/math/grobner/grobner.cpp | 17 +++++++++------ src/math/grobner/grobner.h | 2 +- src/model/model_evaluator.cpp | 3 ++- src/qe/qsat.cpp | 39 ++++++++++++++++++++++++++++------- 4 files changed, 45 insertions(+), 16 deletions(-) diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp index 309e0c777..2bf4d5ba3 100644 --- a/src/math/grobner/grobner.cpp +++ b/src/math/grobner/grobner.cpp @@ -670,7 +670,7 @@ grobner::equation * grobner::simplify(equation const * source, equation * target simplify(target); } } - while (simplified); + while (simplified && !m_manager.canceled()); TRACE("grobner", tout << "result: "; display_equation(tout, *target);); return result ? target : 0; } @@ -697,7 +697,10 @@ grobner::equation * grobner::simplify_using_processed(equation * eq) { simplified = true; eq = new_eq; } - } + if (m_manager.canceled()) { + return 0; + } + } } while (simplified); TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq);); @@ -749,13 +752,13 @@ grobner::equation * grobner::pick_next() { /** \brief Use the given equation to simplify processed terms. */ -void grobner::simplify_processed(equation * eq) { +bool grobner::simplify_processed(equation * eq) { ptr_buffer to_insert; ptr_buffer to_remove; ptr_buffer to_delete; equation_set::iterator it = m_processed.begin(); equation_set::iterator end = m_processed.end(); - for (; it != end; ++it) { + for (; it != end && !m_manager.canceled(); ++it) { equation * curr = *it; m_changed_leading_term = false; // if the leading term is simplified, then the equation has to be moved to m_to_process @@ -795,6 +798,7 @@ void grobner::simplify_processed(equation * eq) { end1 = to_delete.end(); for (; it1 != end1; ++it1) del_equation(*it1); + return !m_manager.canceled(); } /** @@ -944,7 +948,8 @@ bool grobner::compute_basis_step() { m_equations_to_unfreeze.push_back(eq); eq = new_eq; } - simplify_processed(eq); + if (m_manager.canceled()) return false; + if (!simplify_processed(eq)) return false; superpose(eq); m_processed.insert(eq); simplify_to_process(eq); @@ -954,7 +959,7 @@ bool grobner::compute_basis_step() { bool grobner::compute_basis(unsigned threshold) { compute_basis_init(); - while (m_num_new_equations < threshold) { + while (m_num_new_equations < threshold && !m_manager.canceled()) { if (compute_basis_step()) return true; } return false; diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h index 6084bf77d..770f0a538 100644 --- a/src/math/grobner/grobner.h +++ b/src/math/grobner/grobner.h @@ -175,7 +175,7 @@ protected: equation * pick_next(); - void simplify_processed(equation * eq); + bool simplify_processed(equation * eq); void simplify_to_process(equation * eq); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index e67e3cb5e..f8c719852 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -114,7 +114,8 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = 0; family_id fid = f->get_family_id(); - if (num == 0 && (fid == null_family_id || m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) { + bool is_uninterp = fid != null_family_id && m().get_plugin(fid)->is_considered_uninterpreted(f); + if (num == 0 && (fid == null_family_id || is_uninterp)) { expr * val = m_model.get_const_interp(f); if (val != 0) { result = val; diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index c7e20b733..e50821256 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -620,7 +620,7 @@ namespace qe { } kernel& get_kernel(unsigned j) { - if (is_exists(j)) { + if (m_kernel_ex || is_exists(j)) { return m_ex; } else { @@ -1073,7 +1073,7 @@ namespace qe { m_mode(mode), m_avars(m), m_free_vars(m), - m_kernel(m) + m_kernel_ex(false) { reset(); } @@ -1240,9 +1240,10 @@ namespace qe { } - kernel m_kernel; + bool m_kernel_ex; lbool max_min(expr_ref_vector const& fmls, svector const& is_max, app_ref_vector const& vars, app* t) { + m_kernel_ex = true; // Assume this is the only call to check. expr_ref_vector defs(m); app_ref_vector free_vars(m), vars1(m); @@ -1250,8 +1251,8 @@ namespace qe { m_pred_abs.get_free_vars(fml, free_vars); m_pred_abs.abstract_atoms(fml, defs); fml = m_pred_abs.mk_abstract(fml); - m_kernel.assert_expr(mk_and(defs)); - m_kernel.assert_expr(fml); + get_kernel(0).k().assert_expr(mk_and(defs)); + get_kernel(0).k().assert_expr(fml); obj_hashtable var_set; for (unsigned i = 0; i < vars.size(); ++i) { var_set.insert(vars[i]); @@ -1278,8 +1279,6 @@ namespace qe { m_vars.push_back(vars1); return max_min(); - - // return l_undef; } lbool max_min() { @@ -1288,15 +1287,39 @@ namespace qe { check_cancel(); expr_ref_vector asms(m_asms); m_pred_abs.get_assumptions(m_model.get(), asms); + // + // TBD: add bound to asms. + // smt::kernel& k = get_kernel(m_level).k(); lbool res = k.check(asms); switch (res) { case l_true: + k.get_model(m_model); + SASSERT(validate_model(asms)); + TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); ); + // + // TBD: compute new bound on objective. + // + push(); break; case l_false: + switch (m_level) { + case 0: return l_false; + case 1: + // TBD + break; + default: + if (m_model.get()) { + project(asms); + } + else { + pop(1); + } + break; + } break; case l_undef: - break; + return res; } } return l_undef;