From 1a5449c3d445c2a5b980cb69681c5b4cb7cf7836 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Mar 2016 12:35:29 -0700 Subject: [PATCH 1/6] enable new NRA solver for nra benchmarks Signed-off-by: Nikolaj Bjorner --- src/qe/nlqsat.cpp | 122 +++++++++++++++++++++++++++- src/qe/qe_lite.cpp | 4 - src/tactic/smtlogics/nra_tactic.cpp | 6 +- 3 files changed, 122 insertions(+), 10 deletions(-) diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 2846fd03e..e05bed9a7 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -31,6 +31,10 @@ Revision History: #include "tseitin_cnf_tactic.h" #include "expr_safe_replace.h" #include "ast_pp.h" +#include "for_each_expr.h" +#include "rewriter.h" +#include "rewriter_def.h" + namespace qe { @@ -76,6 +80,7 @@ namespace qe { stats m_stats; statistics m_st; obj_hashtable m_free_vars; + obj_hashtable m_aux_vars; expr_ref_vector m_answer; expr_safe_replace m_answer_simplify; nlsat::literal_vector m_assumptions; @@ -423,6 +428,115 @@ namespace qe { } } + struct div { + expr_ref num, den, name; + div(ast_manager& m, expr* n, expr* d, expr* nm): + num(n, m), den(d, m), name(nm, m) {} + }; + + class div_rewriter_cfg : public default_rewriter_cfg { + nlqsat& s; + ast_manager& m; + arith_util a; + vector
m_divs; + public: + div_rewriter_cfg(nlqsat& s): s(s), m(s.m), a(s.m) {} + ~div_rewriter_cfg() {} + br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) { + if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1]) && is_ground(args[0]) && is_ground(args[1])) { + result = m.mk_fresh_const("div", a.mk_real()); + m_divs.push_back(div(m, args[0], args[1], result)); + return BR_DONE; + } + return BR_FAILED; + } + vector
const& divs() const { return m_divs; } + }; + + //template class rewriter_tpl; + + + class div_rewriter_star : public rewriter_tpl { + div_rewriter_cfg m_cfg; + public: + div_rewriter_star(nlqsat& s): + rewriter_tpl(s.m, false, m_cfg), + m_cfg(s) + {} + vector
const& divs() const { return m_cfg.divs(); } + }; + + class is_pure_proc { + nlqsat& s; + arith_util a; + bool m_has_divs; + public: + is_pure_proc(nlqsat& s): s(s), a(s.m), m_has_divs(false) {} + + void operator()(::var * n) { + if (!a.is_real(n) && !s.m.is_bool(n)) { + throw tactic_exception("not NRA"); + } + } + void operator()(app * n) { + if (n->get_family_id() == s.m.get_basic_family_id()) { + return; + } + if (is_uninterp_const(n) && (a.is_real(n) || s.m.is_bool(n))) { + return; + } + if (a.is_mul(n) || a.is_add(n) || a.is_sub(n) || a.is_uminus(n) || a.is_numeral(n) || + a.is_le(n) || a.is_ge(n) || a.is_lt(n) || a.is_gt(n)) { + return; + } + expr* n1, *n2; + if (a.is_div(n, n1, n2) && a.is_numeral(n2)) { + return; + } + rational r; + if (a.is_power(n, n1, n2) && a.is_numeral(n2, r) && r.is_unsigned()) { + return; + } + if (a.is_div(n, n1, n2) && is_ground(n1) && is_ground(n2) && s.m_mode == qsat_t) { + m_has_divs = true; + return; + } + TRACE("qe", tout << "not NRA: " << mk_pp(n, s.m) << "\n";); + throw tactic_exception("not NRA"); + } + void operator()(quantifier * n) {} + + bool has_divs() const { return m_has_divs; } + }; + + void purify(expr_ref& fml) { + is_pure_proc is_pure(*this); + { + expr_fast_mark1 visited; + quick_for_each_expr(is_pure, visited, fml); + } + if (is_pure.has_divs()) { + arith_util arith(m); + div_rewriter_star rw(*this); + proof_ref pr(m); + rw(fml, fml, pr); + vector
const& divs = rw.divs(); + expr_ref_vector axioms(m); + for (unsigned i = 0; i < divs.size(); ++i) { + axioms.push_back( + m.mk_or(m.mk_eq(divs[i].den, arith.mk_numeral(rational(0), false)), + m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name)))); + for (unsigned j = i + 1; j < divs.size(); ++j) { + axioms.push_back(m.mk_or(m.mk_not(m.mk_eq(divs[i].den, divs[j].den)), + m.mk_not(m.mk_eq(divs[i].num, divs[j].num)), + m.mk_eq(divs[i].name, divs[j].name))); + } + } + axioms.push_back(fml); + fml = mk_and(axioms); + } + } + void reset() { //m_solver.reset(); m_asms.reset(); @@ -444,6 +558,7 @@ namespace qe { m_st.reset(); m_solver.collect_statistics(m_st); m_free_vars.reset(); + m_aux_vars.reset(); m_answer.reset(); m_answer_simplify.reset(); m_assumptions.reset(); @@ -488,10 +603,11 @@ namespace qe { app_ref_vector vars(m); bool is_forall = false; pred_abs abs(m); + purify(fml); abs.get_free_vars(fml, vars); insert_set(m_free_vars, vars); qvars.push_back(vars); - vars.reset(); + vars.reset(); if (m_mode == elim_t) { is_forall = true; hoist.pull_quantifier(is_forall, fml, vars); @@ -607,7 +723,7 @@ namespace qe { for (; it != end; ++it) { nlsat::var x = it->m_value; expr * t = it->m_key; - if (!is_uninterp_const(t) || !m_free_vars.contains(t)) + if (!is_uninterp_const(t) || !m_free_vars.contains(t) || m_aux_vars.contains(t)) continue; expr * v; try { @@ -626,7 +742,7 @@ namespace qe { for (; it != end; ++it) { expr * a = it->m_key; nlsat::bool_var b = it->m_value; - if (a == 0 || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a)) + if (a == 0 || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a) || m_aux_vars.contains(a)) continue; lbool val = m_bmodel0.get(b, l_undef); if (val == l_undef) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index aad802a2a..5039e4c3d 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -21,7 +21,6 @@ Revision History: #include "expr_abstract.h" #include "used_vars.h" #include "occurs.h" -#include "for_each_expr.h" #include "rewriter_def.h" #include "ast_pp.h" #include "ast_ll_pp.h" @@ -2423,9 +2422,6 @@ public: TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) { tout << mk_pp(fmls[i].get(), m) << "\n"; }); - IF_VERBOSE(3, for (unsigned i = 0; i < fmls.size(); ++i) { - verbose_stream() << mk_pp(fmls[i].get(), m) << "\n"; - }); is_variable_test is_var(index_set, index_of_bound); m_der.set_is_variable_proc(is_var); m_fm.set_is_variable_proc(is_var); diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp index 75fbcc3f4..4098cd6c1 100644 --- a/src/tactic/smtlogics/nra_tactic.cpp +++ b/src/tactic/smtlogics/nra_tactic.cpp @@ -38,13 +38,13 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) { return and_then(mk_simplify_tactic(m, p), mk_nnf_tactic(m, p), mk_propagate_values_tactic(m, p), - //mk_qe_lite_tactic(m), - mk_qe_tactic(m, p), + mk_qe_lite_tactic(m), + //mk_qe_tactic(m, p), cond(mk_is_qfnra_probe(), or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000), try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), mk_qfnra_nlsat_tactic(m, p2)), -#if 0 +#if 1 or_else(mk_nlqsat_tactic(m, p), mk_smt_tactic(p)) #else From 680c28d083e46425ef5603214ece86529487cac1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Mar 2016 16:34:04 -0700 Subject: [PATCH 2/6] remove nnf conversion which breaks NRA property Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 2 +- src/tactic/smtlogics/nra_tactic.cpp | 27 +++++++++++---------------- 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 40177bb08..ae3f1252b 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -460,7 +460,7 @@ namespace nlsat { void del(bool_var b) { SASSERT(m_bwatches[b].empty()); - SASSERT(m_bvalues[b] == l_undef); + //SASSERT(m_bvalues[b] == l_undef); m_num_bool_vars--; m_dead[b] = true; m_atoms[b] = 0; diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp index 4098cd6c1..063e0775a 100644 --- a/src/tactic/smtlogics/nra_tactic.cpp +++ b/src/tactic/smtlogics/nra_tactic.cpp @@ -35,22 +35,17 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) { p2.set_uint("seed", 13); p2.set_bool("factor", false); - return and_then(mk_simplify_tactic(m, p), - mk_nnf_tactic(m, p), - mk_propagate_values_tactic(m, p), - mk_qe_lite_tactic(m), - //mk_qe_tactic(m, p), - cond(mk_is_qfnra_probe(), - or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000), - try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), - mk_qfnra_nlsat_tactic(m, p2)), -#if 1 - or_else(mk_nlqsat_tactic(m, p), - mk_smt_tactic(p)) -#else - mk_smt_tactic(p) -#endif - )); + return and_then( + mk_simplify_tactic(m, p), + mk_propagate_values_tactic(m, p), + mk_qe_lite_tactic(m), + cond(mk_is_qfnra_probe(), + or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000), + try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), + mk_qfnra_nlsat_tactic(m, p2)), + or_else(mk_nlqsat_tactic(m, p), + mk_smt_tactic(p)) + )); } From 3dc2028925e6936b07682e342b8a644b7551fb20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Mar 2016 09:20:57 -0700 Subject: [PATCH 3/6] adding min/max Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 4 +-- src/qe/qsat.cpp | 82 +++++++++++++++++++++++++++++++++++++++++-------- src/qe/qsat.h | 11 +++++++ 3 files changed, 83 insertions(+), 14 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d33f352e1..c169be14d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -294,10 +294,10 @@ if (ENABLE_TRACING) list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_TRACE") endif() # Should we always enable tracing when doing a debug build? -#list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_TRACE>) +list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_TRACE>) ################################################################################ -# Postion indepdent code +# Postion independent code ################################################################################ # This is required because code built in the components will end up in a shared # library. If not building a shared library ``-fPIC`` isn't needed and would add diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index b080b71a2..0a5c40dbd 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -499,15 +499,7 @@ namespace qe { } } } - - class qsat : public tactic { - - struct stats { - unsigned m_num_rounds; - stats() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - }; - + class kernel { ast_manager& m; smt_params m_smtp; @@ -542,6 +534,15 @@ namespace qe { ); } }; + + class qsat : public tactic { + + struct stats { + unsigned m_num_rounds; + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + ast_manager& m; params_ref m_params; @@ -1155,10 +1156,67 @@ namespace qe { tactic * translate(ast_manager & m) { return alloc(qsat, m, m_params, m_qelim, m_force_elim); - } - - + } }; + + + + + struct min_max_opt::imp { + ast_manager& m; + expr_ref_vector m_fmls; + pred_abs m_pred_abs; + qe::mbp m_mbp; + kernel m_kernel; + + imp(ast_manager& m): + m(m), + m_fmls(m), + m_pred_abs(m), + m_mbp(m), + m_kernel(m) {} + + void add(expr* e) { + m_fmls.push_back(e); + } + + lbool check(svector const& is_max, func_decl_ref_vector const& vars, app* t) { + // Assume this is the only call to check. + expr_ref_vector defs(m); + expr_ref fml = mk_and(m_fmls); + 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); + // TBD + + return l_undef; + } + }; + + min_max_opt::min_max_opt(ast_manager& m) { + m_imp = alloc(imp, m); + } + + min_max_opt::~min_max_opt() { + dealloc(m_imp); + } + + void min_max_opt::add(expr* e) { + m_imp->add(e); + } + + void min_max_opt::add(expr_ref_vector const& fmls) { + for (unsigned i = 0; i < fmls.size(); ++i) { + add(fmls[i]); + } + } + + lbool min_max_opt::check(svector const& is_max, func_decl_ref_vector const& vars, app* t) { + return m_imp->check(is_max, vars, t); + } + + }; diff --git a/src/qe/qsat.h b/src/qe/qsat.h index ee9f9e6ad..91b370294 100644 --- a/src/qe/qsat.h +++ b/src/qe/qsat.h @@ -113,6 +113,17 @@ namespace qe { void collect_statistics(statistics& st) const; }; + class min_max_opt { + struct imp; + imp* m_imp; + public: + min_max_opt(ast_manager& m); + ~min_max_opt(); + void add(expr* e); + void add(expr_ref_vector const& fmls); + lbool check(svector const& is_max, func_decl_ref_vector const& vars, app* t); + }; + } From 701f32471e362a5d5e3d30bb77ad33fb235e067f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Mar 2016 15:04:20 -0700 Subject: [PATCH 4/6] hardening model checker code against cancellations' Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/rewriter_def.h | 3 +++ src/smt/smt_context_inv.cpp | 4 ++-- src/smt/smt_model_finder.cpp | 4 +++- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 6fff9aff4..4d55632d3 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -595,6 +595,9 @@ void rewriter_tpl::set_inv_bindings(unsigned num_bindings, expr * const template template void rewriter_tpl::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) { + if (m().canceled()) { + throw rewriter_exception(m().limit().get_cancel_msg()); + } SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size()); SASSERT(not_rewriting()); m_root = t; diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index 50814b686..6b626c2de 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -420,14 +420,14 @@ namespace smt { case l_undef: break; case l_true: - m_proto_model->eval(n, res, false); + if (!m_proto_model->eval(n, res, false)) return true; CTRACE("mbqi_bug", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); if (m.is_false(res)) { return false; } break; case l_false: - m_proto_model->eval(n, res, false); + if (!m_proto_model->eval(n, res, false)) return true; CTRACE("mbqi_bug", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); if (m.is_true(res)) { return false; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index a425475c2..f166125ba 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -149,6 +149,7 @@ namespace smt { SASSERT(!contains_model_value(t)); unsigned gen = (*it).m_value; expr * t_val = ev.eval(t, true); + if (!t_val) break; TRACE("model_finder", tout << mk_pp(t, m_manager) << " " << mk_pp(t_val, m_manager) << "\n";); expr * old_t = 0; @@ -828,7 +829,7 @@ namespace smt { for (; it != end; ++it) { expr * t = (*it).m_key; expr * t_val = eval(t, true); - if (!already_found.contains(t_val)) { + if (t_val && !already_found.contains(t_val)) { values.push_back(t_val); already_found.insert(t_val); } @@ -891,6 +892,7 @@ namespace smt { add_mono_exceptions(n); ptr_buffer values; get_instantiation_set_values(n, values); + if (values.empty()) return; sort_values(n, values); sort * s = n->get_sort(); arith_simplifier_plugin * as = get_arith_simp(); From 5e737641b754ca1aa0e75ffcbdfdeac6cb8a0cdf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Mar 2016 16:57:30 -0700 Subject: [PATCH 5/6] remove qe-lite pass in quant_tatics Signed-off-by: Nikolaj Bjorner --- src/qe/qe_lite.cpp | 49 ++++++++++++++++++++++++-- src/smt/proto_model/proto_model.cpp | 1 + src/tactic/smtlogics/quant_tactics.cpp | 3 -- 3 files changed, 47 insertions(+), 6 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 5039e4c3d..86a3fbec8 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -491,6 +491,10 @@ namespace eq { m_new_args.push_back(args[i]); } } + if (m_new_args.size() == num_args) { + r = q; + return; + } expr_ref t(m); if (q->is_forall()) { @@ -771,7 +775,7 @@ namespace eq { proof_ref curr_pr(m); q = to_quantifier(r); reduce_quantifier1(q, r, curr_pr); - if (m.proofs_enabled()) { + if (m.proofs_enabled() && r != q) { pr = m.mk_transitivity(pr, curr_pr); } } while (q != r && is_quantifier(r)); @@ -2297,7 +2301,7 @@ public: } m_imp(indices, true, result); if (is_forall(q)) { - result = m.mk_not(result); + result = push_not(result); } result = m.update_quantifier( q, @@ -2476,6 +2480,41 @@ class qe_lite_tactic : public tactic { cooperate("qe-lite"); } + void debug_diff(expr* a, expr* b) { + ptr_vector as, bs; + as.push_back(a); + bs.push_back(b); + expr* a1, *a2, *b1, *b2; + while (!as.empty()) { + a = as.back(); + b = bs.back(); + as.pop_back(); + bs.pop_back(); + if (a == b) { + continue; + } + else if (is_forall(a) && is_forall(b)) { + as.push_back(to_quantifier(a)->get_expr()); + bs.push_back(to_quantifier(b)->get_expr()); + } + else if (m.is_and(a, a1, a2) && m.is_and(b, b1, b2)) { + as.push_back(a1); + as.push_back(a2); + bs.push_back(b1); + bs.push_back(b2); + } + else if (m.is_eq(a, a1, a2) && m.is_eq(b, b1, b2)) { + as.push_back(a1); + as.push_back(a2); + bs.push_back(b1); + bs.push_back(b2); + } + else { + TRACE("qe", tout << mk_pp(a, m) << " != " << mk_pp(b, m) << "\n";); + } + } + } + void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, @@ -2507,7 +2546,11 @@ class qe_lite_tactic : public tactic { new_pr = g->pr(i); } } - g->update(i, new_f, new_pr, g->dep(i)); + if (f != new_f) { + TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n";); + debug_diff(f, new_f); + g->update(i, new_f, new_pr, g->dep(i)); + } } g->inc_depth(); result.push_back(g.get()); diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index cfc037a68..c4f38cc3a 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -105,6 +105,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { m_eval.set_model_completion(model_completion); try { m_eval(e, result); + std::cout << result << "\n"; return true; } catch (model_evaluator_exception & ex) { diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 8760d255e..13a790e93 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -22,8 +22,6 @@ Revision History: #include"solve_eqs_tactic.h" #include"elim_uncnstr_tactic.h" #include"qe_tactic.h" -#include"qe_sat_tactic.h" -#include"qe_lite.h" #include"qsat.h" #include"nlqsat.h" #include"ctx_simplify_tactic.h" @@ -54,7 +52,6 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f using_params(mk_simplify_tactic(m), pull_ite_p), solve_eqs, mk_elim_uncnstr_tactic(m), - mk_qe_lite_tactic(m), mk_simplify_tactic(m)); } From 72ec6dc8e1ecec52d894b45d852c2fdec055d30b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Mar 2016 16:58:48 -0700 Subject: [PATCH 6/6] remove debug code Signed-off-by: Nikolaj Bjorner --- src/qe/qe_lite.cpp | 1 - src/smt/proto_model/proto_model.cpp | 1 - 2 files changed, 2 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 86a3fbec8..f28a93753 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2548,7 +2548,6 @@ class qe_lite_tactic : public tactic { } if (f != new_f) { TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n";); - debug_diff(f, new_f); g->update(i, new_f, new_pr, g->dep(i)); } } diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index c4f38cc3a..cfc037a68 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -105,7 +105,6 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { m_eval.set_model_completion(model_completion); try { m_eval(e, result); - std::cout << result << "\n"; return true; } catch (model_evaluator_exception & ex) {