mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5605

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-19 12:21:54 -04:00
parent fc3a701888
commit f9dde2e8a4
3 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/opt/maxlex.cpp
View file

@ -135,8 +135,10 @@ namespace opt {
if (mdl) { if (mdl) {
TRACE("opt", tout << *mdl << "\n";); TRACE("opt", tout << *mdl << "\n";);
for (auto & soft : m_soft) { for (auto & soft : m_soft) {
if (!mdl->is_true(soft.s)) if (!mdl->is_true(soft.s)) {
break; update_bounds();
return;
}
soft.set_value(l_true); soft.set_value(l_true);
assert_value(soft); assert_value(soft);
} }
@ -151,9 +153,8 @@ namespace opt {
unsigned sz = m_soft.size(); unsigned sz = m_soft.size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
auto& soft = m_soft[i]; auto& soft = m_soft[i];
if (soft.value != l_undef) { if (soft.value != l_undef)
continue; continue;
}
expr_ref_vector asms(m); expr_ref_vector asms(m);
asms.push_back(soft.s); asms.push_back(soft.s);
lbool is_sat = s().check_sat(asms); lbool is_sat = s().check_sat(asms);

3
src/opt/opt_context.cpp
View file

@ -24,6 +24,7 @@ Notes:
#include "ast/pb_decl_plugin.h" #include "ast/pb_decl_plugin.h"
#include "ast/ast_smt_pp.h" #include "ast/ast_smt_pp.h"
#include "ast/ast_pp_util.h" #include "ast/ast_pp_util.h"
#include "ast/ast_ll_pp.h"
#include "ast/display_dimacs.h" #include "ast/display_dimacs.h"
#include "model/model_smt2_pp.h" #include "model/model_smt2_pp.h"
#include "tactic/goal.h" #include "tactic/goal.h"
@ -1200,7 +1201,7 @@ namespace opt {
app* context::purify(generic_model_converter_ref& fm, expr* term) { app* context::purify(generic_model_converter_ref& fm, expr* term) {
std::ostringstream out; 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()); app* q = m.mk_fresh_const(out.str(), term->get_sort());
if (!fm) fm = alloc(generic_model_converter, m, "opt"); if (!fm) fm = alloc(generic_model_converter, m, "opt");
if (m_arith.is_int_real(term)) { if (m_arith.is_int_real(term)) {

4
src/sat/smt/euf_relevancy.cpp
View file

@ -27,6 +27,7 @@ namespace euf {
return; return;
for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes) for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes)
m_auto_relevant_lim.push_back(m_auto_relevant.size()); 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); m_auto_relevant.push_back(e);
} }
@ -109,6 +110,9 @@ namespace euf {
if (e) if (e)
todo.push_back(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); todo.append(m_auto_relevant);
for (unsigned i = 0; i < todo.size(); ++i) { for (unsigned i = 0; i < todo.size(); ++i) {
expr* e = todo[i]; expr* e = todo[i];