Skip to content

Commit

Permalink
fix output
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Nov 7, 2019
1 parent 0a8b924 commit 1fec4bb
Show file tree
Hide file tree
Showing 3 changed files with 34 additions and 31 deletions.
2 changes: 1 addition & 1 deletion src/smt/smt_context.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ namespace smt {

std::ostream& display_last_failure(std::ostream& out) const;
std::string last_failure_as_string() const;
void set_reason_unknown(char const* msg) { m_unknown = msg; std::cout << m_unknown << "\n"; }
void set_reason_unknown(char const* msg) { m_unknown = msg; }
void set_progress_callback(progress_callback *callback);


Expand Down
2 changes: 1 addition & 1 deletion src/smt/smt_model_generator.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -489,7 +489,7 @@ namespace smt {

proto_model * model_generator::mk_model() {
SASSERT(!m_model);
TRACE("model", m_context->display(tout););
TRACE("model_verbose", m_context->display(tout););
init_model();
register_existing_model_values();
mk_bool_model();
Expand Down
61 changes: 32 additions & 29 deletions src/smt/theory_arith_core.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,13 +39,35 @@ namespace smt {

template<typename Ext>
void theory_arith<Ext>::found_underspecified_op(app * n) {
context& ctx = get_context();
m_underspecified_ops.push_back(n);
get_context().push_trail(push_back_vector<context, ptr_vector<app>>(m_underspecified_ops));
ctx.push_trail(push_back_vector<context, ptr_vector<app>>(m_underspecified_ops));
if (!m_found_underspecified_op) {
TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, get_manager()) << "\n";);
get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
ctx.push_trail(value_trail<context, bool>(m_found_underspecified_op));
m_found_underspecified_op = true;
}

expr* e = nullptr;
if (m_util.is_div(n)) {
e = m_util.mk_div0(n->get_arg(0), n->get_arg(1));
}
else if (m_util.is_idiv(n)) {
e = m_util.mk_idiv0(n->get_arg(0), n->get_arg(1));
}
else if (m_util.is_rem(n)) {
e = m_util.mk_rem0(n->get_arg(0), n->get_arg(1));
}
else if (m_util.is_mod(n)) {
e = m_util.mk_mod0(n->get_arg(0), n->get_arg(1));
}
else if (m_util.is_power(n)) {
e = m_util.mk_power0(n->get_arg(0), n->get_arg(1));
}
if (e) {
ctx.assign(mk_eq(e, n, false), nullptr);
}

}

template<typename Ext>
Expand Down Expand Up @@ -389,9 +411,9 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_div(app * n) {
rational r(1);
if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
if (!ctx.relevancy())
mk_div_axiom(n->get_arg(0), n->get_arg(1));
return s;
Expand All @@ -400,9 +422,9 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_idiv(app * n) {
rational r;
if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
app * mod = m_util.mk_mod(n->get_arg(0), n->get_arg(1));
ctx.internalize(mod, false);
if (ctx.relevancy())
Expand All @@ -414,9 +436,9 @@ namespace smt {
theory_var theory_arith<Ext>::internalize_mod(app * n) {
TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
rational r(1);
if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
if (!ctx.relevancy())
mk_idiv_mod_axioms(n->get_arg(0), n->get_arg(1));
return s;
Expand All @@ -425,9 +447,9 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_rem(app * n) {
rational r(1);
if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
if (!ctx.relevancy()) {
mk_rem_axiom(n->get_arg(0), n->get_arg(1));
}
Expand Down Expand Up @@ -3265,36 +3287,17 @@ namespace smt {

template<typename Ext>
void theory_arith<Ext>::init_model(model_generator & m) {
TRACE("theory_arith", tout << "init model invoked...\n";);
TRACE("theory_arith", tout << "init model invoked...\n";
for (app* n : m_underspecified_ops) {
tout << mk_pp(n, get_manager()) << "\n";
});
context& ctx = get_context();
m_factory = alloc(arith_factory, get_manager());
m.register_factory(m_factory);
compute_epsilon();
if (!m_model_depends_on_computed_epsilon) {
refine_epsilon();
}
for (app* n : m_underspecified_ops) {
enode* e = nullptr;
if (m_util.is_div(n)) {
e = mk_enode(m_util.mk_div0(n->get_arg(0), n->get_arg(1)));
}
else if (m_util.is_idiv(n)) {
e = mk_enode(m_util.mk_idiv0(n->get_arg(0), n->get_arg(1)));
}
else if (m_util.is_rem(n)) {
e = mk_enode(m_util.mk_rem0(n->get_arg(0), n->get_arg(1)));
}
else if (m_util.is_mod(n)) {
e = mk_enode(m_util.mk_mod0(n->get_arg(0), n->get_arg(1)));
}
else if (m_util.is_power(n)) {
e = mk_enode(m_util.mk_power0(n->get_arg(0), n->get_arg(1)));
}
if (e) {
ctx.mark_as_relevant(e);
ctx.add_eq(e, ctx.get_enode(n), eq_justification());
}
}
}

template<typename Ext>
Expand Down

0 comments on commit 1fec4bb

Please sign in to comment.