From 6a3ba64afe51b841fdf8ceb5b3f82df2f5a13566 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Aug 2021 16:48:28 -0700
Subject: [PATCH] #5454
@wintersteiger: added code review comment to theory_fpa. The bug seen in #5454 doesn't surface with theory_fpa, though.
---
src/ast/fpa/fpa2bv_converter.cpp | 3 ++-
src/sat/smt/fpa_solver.cpp | 16 ++++++++++++++--
src/sat/smt/fpa_solver.h | 2 +-
src/smt/theory_fpa.cpp | 5 +++++
4 files changed, 22 insertions(+), 4 deletions(-)
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index a654e6070..3167f2305 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -19,6 +19,7 @@ Notes:
#include<math.h>
#include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
#include "ast/well_sorted.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/used_vars.h"
@@ -4430,7 +4431,7 @@ expr* fpa2bv_converter_wrapped::bv2fpa_value(sort* s, expr* a, expr* b, expr* c)
mpfm.set(f, ebits, sbits, mpzm.is_one(sgn_z), mpzm.get_int64(exp_u), sig_z);
result = m_util.mk_value(f);
- TRACE("t_fpa", tout << "result: [" <<
+ TRACE("t_fpa", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << " result: [" <<
mpzm.to_string(sgn_z) << "," <<
mpzm.to_string(exp_z) << "," <<
mpzm.to_string(sig_z) << "] --> " <<
diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
index bdf224328..4adc81b32 100644
--- a/src/sat/smt/fpa_solver.cpp
+++ b/src/sat/smt/fpa_solver.cpp
@@ -83,6 +83,12 @@ namespace fpa {
return conds;
}
+ sat::check_result solver::check() {
+ SASSERT(m_converter.m_extra_assertions.empty());
+ SASSERT(m_nodes.size() <= m_nodes_qhead);
+ return sat::check_result::CR_DONE;
+ }
+
void solver::attach_new_th_var(enode* n) {
theory_var v = mk_var(n);
ctx.attach_th_var(n, this, v);
@@ -183,7 +189,7 @@ namespace fpa {
add_unit(atom);
}
}
- else {
+ else {
switch (a->get_decl_kind()) {
case OP_FPA_TO_FP:
case OP_FPA_TO_UBV:
@@ -199,7 +205,7 @@ namespace fpa {
break;
}
}
-
+ activate(e);
}
void solver::activate(expr* n) {
@@ -223,7 +229,11 @@ namespace fpa {
VERIFY(m_fpa_util.is_fp(bv_val_e, a, b, c));
expr* args[] = { a, b, c };
expr_ref cc_args(m_bv_util.mk_concat(3, args), m);
+ // Require
+ // wrap(n) = bvK
+ // fp(extract(wrap(n)) = n
add_unit(eq_internalize(wrapped, cc_args));
+ add_unit(eq_internalize(bv_val_e, n));
add_units(mk_side_conditions());
}
else if (m.is_ite(n)) {
@@ -313,6 +323,7 @@ namespace fpa {
expr* e = n->get_expr();
app_ref wrapped(m);
expr_ref value(m);
+
auto is_wrapped = [&]() {
if (!wrapped) wrapped = m_converter.wrap(e);
return expr2enode(wrapped) != nullptr;
@@ -345,6 +356,7 @@ namespace fpa {
value = m_fpa_util.mk_pzero(ebits, sbits);
}
values.set(n->get_root_id(), value);
+ TRACE("t_fpa", tout << ctx.bpp(n) << " := " << value << "\n";);
}
bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h
index 795abdfdd..38abb399d 100644
--- a/src/sat/smt/fpa_solver.h
+++ b/src/sat/smt/fpa_solver.h
@@ -72,7 +72,7 @@ namespace fpa {
bool unit_propagate() override;
void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); }
- sat::check_result check() override { return sat::check_result::CR_DONE; }
+ sat::check_result check() override;
euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 5f8e35394..1543ac2c2 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -454,6 +454,11 @@ namespace smt {
expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) };
cc_args = m_bv_util.mk_concat(3, args);
c = m.mk_eq(wrapped, cc_args);
+ // NB code review: #5454 exposes a bug in fpa_solver that
+ // could be latent here as well. It needs also the equality
+ // n == bv_val_e to be asserted such that whenever something is assigned th
+ // bit-vector value cc_args it is equated with n
+ // I don't see another way this constraint would be enforced.
assert_cnstr(c);
assert_cnstr(mk_side_conditions());
}