From ece5ad90e04cdf09634d7356154828a91928ed17 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 20 Jan 2018 17:09:43 -0800
Subject: [PATCH] fix model conversion bugs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/cmd_context/cmd_context.cpp | 20 ++++-----
src/cmd_context/cmd_context.h | 2 +-
src/cmd_context/pdecl.cpp | 4 +-
src/sat/sat_model_converter.cpp | 40 +++++++++---------
src/sat/sat_model_converter.h | 2 +
src/sat/sat_simplifier.cpp | 15 ++++---
src/sat/sat_solver/inc_sat_solver.cpp | 42 +++++++------------
src/tactic/generic_model_converter.cpp | 1 +
.../portfolio/bounded_int2bv_solver.cpp | 8 ++--
src/tactic/portfolio/enum2bv_solver.cpp | 6 +--
src/tactic/portfolio/pb2bv_solver.cpp | 16 +++----
11 files changed, 68 insertions(+), 88 deletions(-)
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 0b2decec8..f82f8868d 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1419,7 +1419,9 @@ void cmd_context::restore_assertions(unsigned old_sz) {
SASSERT(m_assertions.empty());
return;
}
- SASSERT(old_sz <= m_assertions.size());
+ if (old_sz == m_assertions.size())
+ return;
+ SASSERT(old_sz < m_assertions.size());
SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
restore(m(), m_assertions, old_sz);
if (produce_unsat_cores())
@@ -1520,7 +1522,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
}
display_sat_result(r);
if (r == l_true) {
- complete_model();
validate_model();
}
validate_check_sat_result(r);
@@ -1528,9 +1529,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
// get_opt()->display_assignment(regular_stream());
}
- if (r == l_true && m_params.m_dump_models) {
- model_ref md;
- get_check_sat_result()->get_model(md);
+ model_ref md;
+ if (r == l_true && m_params.m_dump_models && is_model_available(md)) {
display_model(md);
}
}
@@ -1695,14 +1695,10 @@ struct contains_underspecified_op_proc {
/**
\brief Complete the model if necessary.
*/
-void cmd_context::complete_model() {
- model_ref md;
- if (!is_model_available(md) ||
- gparams::get_value("model.completion") != "true")
+void cmd_context::complete_model(model_ref& md) const {
+ if (gparams::get_value("model.completion") != "true" || !md.get())
return;
- get_check_sat_result()->get_model(md);
- SASSERT(md.get() != 0);
params_ref p;
p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
p.set_uint("sort_store", true);
@@ -1770,7 +1766,6 @@ void cmd_context::validate_model() {
return;
if (!is_model_available(md))
return;
- get_check_sat_result()->get_model(md);
SASSERT(md.get() != 0);
params_ref p;
p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
@@ -1902,6 +1897,7 @@ bool cmd_context::is_model_available(model_ref& md) const {
has_manager() &&
(cs_state() == css_sat || cs_state() == css_unknown)) {
get_check_sat_result()->get_model(md);
+ complete_model(md);
return md.get() != 0;
}
return false;
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index dc85ad2e0..253384f35 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -365,7 +365,7 @@ public:
void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
check_sat_state cs_state() const;
- void complete_model();
+ void complete_model(model_ref& mdl) const;
void validate_model();
void display_model(model_ref& mdl);
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 7a85e87a2..51220b1d0 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -18,6 +18,7 @@ Revision History:
--*/
#include "cmd_context/pdecl.h"
#include "ast/datatype_decl_plugin.h"
+#include <sstream>
using namespace format_ns;
class psort_inst_cache {
@@ -866,8 +867,6 @@ psort * pdecl_manager::mk_psort_cnst(sort * s) {
}
psort * pdecl_manager::register_psort(psort * n) {
- enable_trace("register_psort");
- TRACE("register_psort", tout << "registering psort...\n"; n->display(tout); tout << "\n";);
psort * r = m_table.insert_if_not_there(n);
if (r != n) {
del_decl_core(n);
@@ -947,7 +946,6 @@ void pdecl_manager::del_decl_core(pdecl * p) {
}
void pdecl_manager::del_decl(pdecl * p) {
-enable_trace("register_psort");
TRACE("register_psort", tout << "del psort "; p->display(tout); tout << "\n";);
if (p->is_psort()) {
psort * _p = static_cast<psort*>(p);
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index ce059a07b..7a2b4f5f4 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -347,6 +347,17 @@ namespace sat {
return result;
}
+ void model_converter::swap(bool_var v, unsigned sz, literal_vector& clause) {
+ for (unsigned j = 0; j < sz; ++j) {
+ if (v == clause[j].var()) {
+ std::swap(clause[0], clause[j]);
+ return;
+ }
+ }
+ IF_VERBOSE(0, verbose_stream() << "not found: v" << v << " " << clause << "\n";);
+ UNREACHABLE();
+ }
+
void model_converter::expand(literal_vector& update_stack) {
sat::literal_vector clause;
for (entry const& e : m_entries) {
@@ -357,34 +368,23 @@ namespace sat {
if (l == null_literal) {
elim_stack* st = e.m_elim_stack[index];
if (st) {
- // clause sizes increase
- elim_stackv const& stack = st->stack();
- unsigned sz = stack.size();
- for (unsigned i = 0; i < sz; ++i) {
- unsigned csz = stack[i].first;
- literal lit = stack[i].second;
- BOOL found = false;
- unsigned j = 0;
- for (j = 0; j < csz; ++j) {
- if (clause[j] == lit) {
- std::swap(clause[j], clause[0]);
- found = true;
- break;
- }
- }
- SASSERT(found);
+ // clause sizes increase, so we can always swap
+ // the blocked literal to the front from the prefix.
+ for (auto const& p : st->stack()) {
+ unsigned csz = p.first;
+ literal lit = p.second;
+ swap(lit.var(), csz, clause);
update_stack.append(csz, clause.c_ptr());
update_stack.push_back(null_literal);
}
}
+ swap(e.var(), clause.size(), clause);
update_stack.append(clause);
update_stack.push_back(null_literal);
clause.reset();
- continue;
}
- clause.push_back(l);
- if (l.var() == e.var()) {
- std::swap(clause[0], clause.back());
+ else {
+ clause.push_back(l);
}
}
}
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index 88fdfe5b7..be7d03188 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -94,6 +94,8 @@ namespace sat {
bool legal_to_flip(bool_var v) const;
+ void swap(bool_var v, unsigned sz, literal_vector& clause);
+
public:
model_converter();
~model_converter();
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index b983a0da3..66e0baa89 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -231,7 +231,7 @@ namespace sat {
if (bce_enabled() || abce_enabled() || bca_enabled()) {
elim_blocked_clauses();
}
- si.check_watches();
+ if (!m_need_cleanup) si.check_watches();
if (!learned) {
m_num_calls++;
@@ -680,7 +680,7 @@ namespace sat {
}
void simplifier::elim_lit(clause & c, literal l) {
- TRACE("elim_lit", tout << "processing: " << c << "\n";);
+ TRACE("elim_lit", tout << "processing: " << l << " @ " << c << "\n";);
m_need_cleanup = true;
m_num_elim_lits++;
insert_elim_todo(l.var());
@@ -979,23 +979,23 @@ namespace sat {
void operator()() {
integrity_checker si(s.s);
- si.check_watches();
+ //si.check_watches();
if (s.bce_enabled()) {
block_clauses();
}
- si.check_watches();
+ //si.check_watches();
if (s.abce_enabled()) {
cce<false>();
}
- si.check_watches();
+ //si.check_watches();
if (s.cce_enabled()) {
cce<true>();
}
- si.check_watches();
+ //si.check_watches();
if (s.bca_enabled()) {
bca();
}
- si.check_watches();
+ //si.check_watches();
}
void block_clauses() {
@@ -1829,7 +1829,6 @@ namespace sat {
return true;
}
}
-
return true;
}
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 0ad665c5e..03f6e6d0b 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -54,7 +54,6 @@ class inc_sat_solver : public solver {
unsigned m_fmls_head;
expr_ref_vector m_core;
atom2bool_var m_map;
- model_ref m_model;
scoped_ptr<bit_blaster_rewriter> m_bb_rewriter;
tactic_ref m_preprocess;
unsigned m_num_scopes;
@@ -183,7 +182,6 @@ public:
TRACE("sat", tout << _assumptions << "\n";);
dep2asm_t dep2asm;
- m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return r;
r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm);
@@ -289,12 +287,6 @@ public:
r.reset();
r.append(m_core.size(), m_core.c_ptr());
}
- virtual void get_model_core(model_ref & mdl) {
- if (!m_model.get()) {
- extract_model();
- }
- mdl = m_model;
- }
virtual proof * get_proof() {
UNREACHABLE();
return 0;
@@ -302,7 +294,6 @@ public:
virtual expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) {
if (!is_internalized()) {
- m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return expr_ref_vector(m);
}
@@ -789,14 +780,14 @@ private:
}
}
- void extract_model() {
+ virtual void get_model_core(model_ref & mdl) {
TRACE("sat", tout << "retrieve model " << (m_solver.model_is_current()?"present":"absent") << "\n";);
if (!m_solver.model_is_current()) {
- m_model = 0;
+ mdl = nullptr;
return;
}
sat::model const & ll_m = m_solver.get_model();
- model_ref md = alloc(model, m);
+ mdl = alloc(model, m);
for (auto const& kv : m_map) {
expr * n = kv.m_key;
if (is_app(n) && to_app(n)->get_num_args() > 0) {
@@ -805,40 +796,39 @@ private:
sat::bool_var v = kv.m_value;
switch (sat::value_at(v, ll_m)) {
case l_true:
- md->register_decl(to_app(n)->get_decl(), m.mk_true());
+ mdl->register_decl(to_app(n)->get_decl(), m.mk_true());
break;
case l_false:
- md->register_decl(to_app(n)->get_decl(), m.mk_false());
+ mdl->register_decl(to_app(n)->get_decl(), m.mk_false());
break;
default:
break;
}
}
- m_model = md;
- //IF_VERBOSE(0, model_v2_pp(verbose_stream(), *m_model, true););
+ //IF_VERBOSE(0, model_v2_pp(verbose_stream(), *mdl, true););
if (m_sat_mc) {
- // IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n"););
- (*m_sat_mc)(m_model);
+ //IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n"););
+ (*m_sat_mc)(mdl);
}
insert_const2bits();
if (m_mc0) {
- // IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n"););
- (*m_mc0)(m_model);
+ //IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n"););
+ (*m_mc0)(mdl);
}
- TRACE("sat", model_smt2_pp(tout, m, *m_model, 0););
+ TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););
+
+ // IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
- // IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "after\n"););
-
-#if 1
+#if 0
IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
- model_evaluator eval(*m_model);
+ model_evaluator eval(*mdl);
for (expr * f : m_fmls) {
expr_ref tmp(m);
eval(f, tmp);
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << mk_pp(f, m) << "\n";
- model_smt2_pp(tout, m, *(m_model.get()), 0););
+ model_smt2_pp(tout, m, *(mdl.get()), 0););
if (!m.is_true(tmp)) {
IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n";);
IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index 139355d5f..485682858 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -38,6 +38,7 @@ void generic_model_converter::add(func_decl * d, expr* e) {
void generic_model_converter::operator()(model_ref & md) {
TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout););
+ // IF_VERBOSE(0, verbose_stream() << "Apply converter " << m_orig << "\n";);
model_evaluator ev(*(md.get()));
ev.set_model_completion(true);
ev.set_expand_array_equalities(false);
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index ee6630fd3..7d198468c 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -152,14 +152,14 @@ public:
virtual void get_model_core(model_ref & mdl) {
m_solver->get_model(mdl);
if (mdl) {
- model_converter_ref mc = bounded_model_converter();
+ model_converter_ref mc = local_model_converter();
if (mc) (*mc)(mdl);
}
}
model_converter* external_model_converter() const {
- return concat(mc0(), bounded_model_converter());
+ return concat(mc0(), local_model_converter());
}
- model_converter* bounded_model_converter() const {
+ model_converter* local_model_converter() const {
if (m_int2bv.empty() && m_bv_fns.empty()) return nullptr;
generic_model_converter* mc = alloc(generic_model_converter, m, "bounded_int2bv");
for (func_decl* f : m_bv_fns)
@@ -178,7 +178,7 @@ public:
}
virtual model_converter_ref get_model_converter() const {
- model_converter_ref mc = concat(mc0(), bounded_model_converter());
+ model_converter_ref mc = external_model_converter();
mc = concat(mc.get(), m_solver->get_model_converter().get());
return mc;
}
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 9567f369f..527d9aeb3 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -92,11 +92,11 @@ public:
virtual void get_model_core(model_ref & mdl) {
m_solver->get_model(mdl);
if (mdl) {
- model_converter_ref mc = enum_model_converter();
+ model_converter_ref mc = local_model_converter();
if (mc) (*mc)(mdl);
}
}
- model_converter* enum_model_converter() const {
+ model_converter* local_model_converter() const {
if (m_rewriter.enum2def().empty() &&
m_rewriter.enum2bv().empty()) {
return nullptr;
@@ -110,7 +110,7 @@ public:
}
model_converter* external_model_converter() const {
- return concat(mc0(), enum_model_converter());
+ return concat(mc0(), local_model_converter());
}
virtual model_converter_ref get_model_converter() const {
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index 6660e1bb4..14e58a637 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -91,14 +91,15 @@ public:
virtual void get_model_core(model_ref & mdl) {
m_solver->get_model(mdl);
if (mdl) {
- filter_model(mdl);
+ model_converter_ref mc = local_model_converter();
+ if (mc) (*mc)(mdl);
}
}
model_converter* external_model_converter() const {
- return concat(mc0(), filter_model_converter());
+ return concat(mc0(), local_model_converter());
}
virtual model_converter_ref get_model_converter() const {
- model_converter_ref mc = concat(mc0(), filter_model_converter());
+ model_converter_ref mc = external_model_converter();
mc = concat(mc.get(), m_solver->get_model_converter().get());
return mc;
}
@@ -113,7 +114,7 @@ public:
flush_assertions();
return m_solver->get_consequences(asms, vars, consequences); }
- model_converter* filter_model_converter() const {
+ model_converter* local_model_converter() const {
if (m_rewriter.fresh_constants().empty()) {
return nullptr;
}
@@ -125,13 +126,6 @@ public:
return filter;
}
- void filter_model(model_ref& mdl) {
- model_converter_ref mc = filter_model_converter();
- if (mc.get()) {
- (*mc)(mdl);
- }
- }
-
virtual unsigned get_num_assertions() const {
flush_assertions();
return m_solver->get_num_assertions();