From f9dde2e8a4709ba37341dc12a9b4a3d543769668 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Oct 2021 12:21:54 -0400
Subject: [PATCH] #5605
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/maxlex.cpp | 9 +++++----
src/opt/opt_context.cpp | 3 ++-
src/sat/smt/euf_relevancy.cpp | 4 ++++
3 files changed, 11 insertions(+), 5 deletions(-)
diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp
index a545aa92e..46c7104d5 100644
--- a/src/opt/maxlex.cpp
+++ b/src/opt/maxlex.cpp
@@ -135,8 +135,10 @@ namespace opt {
if (mdl) {
TRACE("opt", tout << *mdl << "\n";);
for (auto & soft : m_soft) {
- if (!mdl->is_true(soft.s))
- break;
+ if (!mdl->is_true(soft.s)) {
+ update_bounds();
+ return;
+ }
soft.set_value(l_true);
assert_value(soft);
}
@@ -151,9 +153,8 @@ namespace opt {
unsigned sz = m_soft.size();
for (unsigned i = 0; i < sz; ++i) {
auto& soft = m_soft[i];
- if (soft.value != l_undef) {
+ if (soft.value != l_undef)
continue;
- }
expr_ref_vector asms(m);
asms.push_back(soft.s);
lbool is_sat = s().check_sat(asms);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 219b5488d..e78da961b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -24,6 +24,7 @@ Notes:
#include "ast/pb_decl_plugin.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_pp_util.h"
+#include "ast/ast_ll_pp.h"
#include "ast/display_dimacs.h"
#include "model/model_smt2_pp.h"
#include "tactic/goal.h"
@@ -1200,7 +1201,7 @@ namespace opt {
app* context::purify(generic_model_converter_ref& fm, expr* term) {
std::ostringstream out;
- out << mk_pp(term, m);
+ out << mk_bounded_pp(term, m, 3);
app* q = m.mk_fresh_const(out.str(), term->get_sort());
if (!fm) fm = alloc(generic_model_converter, m, "opt");
if (m_arith.is_int_real(term)) {
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index d7f7b9012..06c0469ea 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -27,6 +27,7 @@ namespace euf {
return;
for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes)
m_auto_relevant_lim.push_back(m_auto_relevant.size());
+ std::cout << "add-auto " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
m_auto_relevant.push_back(e);
}
@@ -109,6 +110,9 @@ namespace euf {
if (e)
todo.push_back(e);
}
+ std::cout << "init-relevant\n";
+ for (expr* e : m_auto_relevant)
+ std::cout << "auto-relevant " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
todo.append(m_auto_relevant);
for (unsigned i = 0; i < todo.size(); ++i) {
expr* e = todo[i];