From 28c03ed1de3410bb9d62cae11860db58c79bb286 Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Thu, 21 Feb 2019 19:29:35 +0100
Subject: [PATCH] logging support for theory axioms
---
src/ast/ast.cpp | 2 +-
src/ast/bv_decl_plugin.cpp | 2 +-
src/ast/datatype_decl_plugin.cpp | 41 +++++++
src/ast/datatype_decl_plugin.h | 5 +-
src/ast/rewriter/th_rewriter.cpp | 23 ++++
src/smt/smt_internalizer.cpp | 8 --
src/smt/smt_quantifier.cpp | 186 +++++++++++++++----------------
src/smt/smt_quantifier.h | 5 +
src/smt/smt_theory.h | 62 +++++++++++
src/smt/theory_arith_aux.h | 4 +
src/smt/theory_arith_core.h | 5 +
src/smt/theory_arith_int.h | 13 ++-
src/smt/theory_arith_nl.h | 3 +
src/smt/theory_array_base.cpp | 6 +
src/smt/theory_array_full.cpp | 2 +
src/smt/theory_bv.cpp | 26 ++++-
src/smt/theory_datatype.cpp | 26 +++++
src/smt/theory_diff_logic_def.h | 5 +
src/smt/theory_dl.cpp | 4 +
src/smt/theory_fpa.cpp | 2 +
src/smt/theory_jobscheduler.cpp | 51 ++++++++-
src/smt/theory_lra.cpp | 68 ++++++++++-
src/smt/theory_recfun.cpp | 17 ++-
src/smt/theory_seq.cpp | 62 +++++++++--
src/smt/theory_seq.h | 1 +
src/smt/theory_str.cpp | 6 +
26 files changed, 508 insertions(+), 127 deletions(-)
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index ba5ee5d5a..0f6a81a59 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2486,7 +2486,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s
trace_quant(*m_trace_stream, r);
*m_trace_stream << "[attach-var-names] #" << r->get_id();
for (unsigned i = 0; i < num_decls; ++i) {
- *m_trace_stream << " (" << decl_names[num_decls - i - 1].str() << " ; " << decl_sorts[num_decls - i -1]->get_name().str() << ")";
+ *m_trace_stream << " (|" << decl_names[num_decls - i - 1].str() << "| ; |" << decl_sorts[num_decls - i -1]->get_name().str() << "|)";
}
*m_trace_stream << "\n";
}
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index ce75cd90e..c4bada552 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -981,7 +981,7 @@ app * bv_util::mk_bv(unsigned n, expr* const* es) {
uint8_t hexDigit = 0;
unsigned curLength = (4 - n % 4) % 4;
for (unsigned i = 0; i < n; ++i) {
- hexDigit << 1;
+ hexDigit <<= 1;
++curLength;
if (m_manager.is_true(es[i])) {
hexDigit |= 1;
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 9cb685ccc..db3c0e2a0 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -400,6 +400,47 @@ namespace datatype {
sort_ref_vector ps(*m_manager);
for (symbol const& s : m_def_block) {
new_sorts.push_back(m_defs[s]->instantiate(ps));
+ if (m_manager->has_trace_stream()) {
+ symbol const& family_name = m_manager->get_family_name(get_family_id());
+ for (constructor const* c : *m_defs[s]) {
+ func_decl_ref f = c->instantiate(new_sorts.back());
+ const unsigned num_args = f->get_arity();
+ if (num_args == 0) continue;
+ for (unsigned i = 0; i < num_args; ++i) {
+ m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n";
+ ++m_id_counter;
+ }
+ const unsigned constructor_id = m_id_counter;
+ m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name();
+ for (unsigned i = 0; i < num_args; ++i) {
+ m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i;
+ }
+ m_manager->trace_stream() << "\n";
+ ++m_id_counter;
+ m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n";
+ ++m_id_counter;
+ m_axiom_bases.insert(f->get_name(), constructor_id + 4);
+ std::ostringstream var_sorts;
+ for (accessor const* a : *c) {
+ var_sorts << " (;" << a->range()->get_name() << ")";
+ }
+ std::string var_description = var_sorts.str();
+ unsigned i = 0;
+ for (accessor const* a : *c) {
+ func_decl_ref acc = a->instantiate(new_sorts.back());
+ m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n";
+ ++m_id_counter;
+ m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i
+ << " " << family_name << "#" << m_id_counter - 1 << "\n";
+ ++m_id_counter;
+ m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1
+ << " " << family_name << "#" << m_id_counter - 1 << "\n";
+ m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n";
+ ++m_id_counter;
+ ++i;
+ }
+ }
+ }
}
return true;
}
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index fc98c97e7..736cc0875 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -249,13 +249,15 @@ namespace datatype {
class plugin : public decl_plugin {
mutable scoped_ptr<util> m_util;
map<symbol, def*, symbol_hash_proc, symbol_eq_proc> m_defs;
+ map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> m_axiom_bases;
+ unsigned m_id_counter;
svector<symbol> m_def_block;
unsigned m_class_id;
void inherit(decl_plugin* other_p, ast_translation& tr) override;
public:
- plugin(): m_class_id(0) {}
+ plugin(): m_id_counter(0), m_class_id(0) {}
~plugin() override;
void finalize() override;
@@ -290,6 +292,7 @@ namespace datatype {
def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); }
def& get_def(symbol const& s) { return *(m_defs[s]); }
bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); }
+ unsigned get_axiom_base_id(symbol const& s) { return m_axiom_bases[s]; }
util & u() const;
private:
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index eb819c988..4fa8c4074 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -562,6 +562,29 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = nullptr;
br_status st = reduce_app_core(f, num, args, result);
+
+ if (st != BR_FAILED && m().has_trace_stream()) {
+ family_id fid = f->get_family_id();
+ if (fid == m_b_rw.get_fid()) {
+ decl_kind k = f->get_decl_kind();
+ if (k == OP_EQ) {
+ SASSERT(num == 2);
+ fid = m().get_sort(args[0])->get_family_id();
+ }
+ else if (k == OP_ITE) {
+ SASSERT(num == 3);
+ fid = m().get_sort(args[1])->get_family_id();
+ }
+ }
+ app_ref tmp(m());
+ tmp = m().mk_app(f, num, args);
+ m().trace_stream() << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n";
+ tmp = m().mk_eq(tmp, result);
+ m().trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << tmp->get_id() << "\n";
+ m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n";
+ m().trace_stream() << "[end-of-instance]\n";
+ }
+
if (st != BR_DONE && st != BR_FAILED) {
CTRACE("th_rewriter_step", st != BR_FAILED,
tout << f->get_name() << "\n";
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 4a6cd086c..5f9e031e5 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1019,15 +1019,7 @@ namespace smt {
sort * s = term->get_decl()->get_range();
theory * th = m_theories.get_plugin(s->get_family_id());
if (th) {
- if (m_manager.has_trace_stream()) {
- m_manager.trace_stream() << "[theory-constraints] " << m_manager.get_family_name(s->get_family_id()) << "\n";
- }
-
th->apply_sort_cnstr(e, s);
-
- if (m_manager.has_trace_stream()) {
- m_manager.trace_stream() << "[end-theory-constraints]\n";
- }
}
}
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 65a6db875..01a9353f7 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -32,6 +32,96 @@ namespace smt {
quantifier_manager_plugin * mk_default_plugin();
+ /**
+ \brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its
+ equivalence class are in the log and up-to-date.
+ */
+ void quantifier_manager::log_justification_to_root(std::ostream & log, enode *en, obj_hashtable<enode> &already_visited, context &ctx, ast_manager &m) {
+ enode *root = en->get_root();
+ for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
+ if (already_visited.find(it) == already_visited.end()) already_visited.insert(it);
+ else break;
+
+ if (!it->m_proof_is_logged) {
+ log_single_justification(log, it, already_visited, ctx, m);
+ it->m_proof_is_logged = true;
+ } else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
+
+ // When the justification of an argument changes m_proof_is_logged is not reset => We need to check if the proofs of all arguments are logged.
+ const unsigned num_args = it->get_num_args();
+ enode *target = it->get_trans_justification().m_target;
+
+ for (unsigned i = 0; i < num_args; ++i) {
+ log_justification_to_root(log, it->get_arg(i), already_visited, ctx, m);
+ log_justification_to_root(log, target->get_arg(i), already_visited, ctx, m);
+ }
+ it->m_proof_is_logged = true;
+ }
+ }
+ if (!root->m_proof_is_logged) {
+ log << "[eq-expl] #" << root->get_owner_id() << " root\n";
+ root->m_proof_is_logged = true;
+ }
+ }
+
+ /**
+ \brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log
+ equalities needed by the step (e.g. argument equalities for congruence steps).
+ */
+ void quantifier_manager::log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &already_visited, context &ctx, ast_manager &m) {
+ smt::literal lit;
+ unsigned num_args;
+ enode *target = en->get_trans_justification().m_target;
+ theory_id th_id;
+
+ switch (en->get_trans_justification().m_justification.get_kind()) {
+ case smt::eq_justification::kind::EQUATION:
+ lit = en->get_trans_justification().m_justification.get_literal();
+ out << "[eq-expl] #" << en->get_owner_id() << " lit #" << ctx.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n";
+ break;
+ case smt::eq_justification::kind::AXIOM:
+ out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n";
+ break;
+ case smt::eq_justification::kind::CONGRUENCE:
+ if (!en->get_trans_justification().m_justification.used_commutativity()) {
+ num_args = en->get_num_args();
+
+ for (unsigned i = 0; i < num_args; ++i) {
+ log_justification_to_root(out, en->get_arg(i), already_visited, ctx, m);
+ log_justification_to_root(out, target->get_arg(i), already_visited, ctx, m);
+ }
+
+ out << "[eq-expl] #" << en->get_owner_id() << " cg";
+ for (unsigned i = 0; i < num_args; ++i) {
+ out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
+ }
+ out << " ; #" << target->get_owner_id() << "\n";
+
+ break;
+ } else {
+
+ // The e-graph only supports commutativity for binary functions
+ out << "[eq-expl] #" << en->get_owner_id()
+ << " cg (#" << en->get_arg(0)->get_owner_id() << " #" << target->get_arg(1)->get_owner_id()
+ << ") (#" << en->get_arg(1)->get_owner_id() << " #" << target->get_arg(0)->get_owner_id()
+ << ") ; #" << target->get_owner_id() << "\n";
+ break;
+ }
+ case smt::eq_justification::kind::JUSTIFICATION:
+ th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory();
+ if (th_id != null_theory_id) {
+ symbol const theory = m.get_family_name(th_id);
+ out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n";
+ } else {
+ out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
+ }
+ break;
+ default:
+ out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
+ break;
+ }
+ }
+
struct quantifier_manager::imp {
quantifier_manager & m_wrapper;
context & m_context;
@@ -105,96 +195,6 @@ namespace smt {
return m_plugin->is_shared(n);
}
- /**
- \brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its
- equivalence class are in the log and up-to-date.
- */
- void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable<enode> &already_visited) {
- enode *root = en->get_root();
- for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
- if (already_visited.find(it) == already_visited.end()) already_visited.insert(it);
- else break;
-
- if (!it->m_proof_is_logged) {
- log_single_justification(log, it, already_visited);
- it->m_proof_is_logged = true;
- } else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
-
- // When the justification of an argument changes m_proof_is_logged is not reset => We need to check if the proofs of all arguments are logged.
- const unsigned num_args = it->get_num_args();
- enode *target = it->get_trans_justification().m_target;
-
- for (unsigned i = 0; i < num_args; ++i) {
- log_justification_to_root(log, it->get_arg(i), already_visited);
- log_justification_to_root(log, target->get_arg(i), already_visited);
- }
- it->m_proof_is_logged = true;
- }
- }
- if (!root->m_proof_is_logged) {
- log << "[eq-expl] #" << root->get_owner_id() << " root\n";
- root->m_proof_is_logged = true;
- }
- }
-
- /**
- \brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log
- equalities needed by the step (e.g. argument equalities for congruence steps).
- */
- void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &already_visited) {
- smt::literal lit;
- unsigned num_args;
- enode *target = en->get_trans_justification().m_target;
- theory_id th_id;
-
- switch (en->get_trans_justification().m_justification.get_kind()) {
- case smt::eq_justification::kind::EQUATION:
- lit = en->get_trans_justification().m_justification.get_literal();
- out << "[eq-expl] #" << en->get_owner_id() << " lit #" << m_context.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n";
- break;
- case smt::eq_justification::kind::AXIOM:
- out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n";
- break;
- case smt::eq_justification::kind::CONGRUENCE:
- if (!en->get_trans_justification().m_justification.used_commutativity()) {
- num_args = en->get_num_args();
-
- for (unsigned i = 0; i < num_args; ++i) {
- log_justification_to_root(out, en->get_arg(i), already_visited);
- log_justification_to_root(out, target->get_arg(i), already_visited);
- }
-
- out << "[eq-expl] #" << en->get_owner_id() << " cg";
- for (unsigned i = 0; i < num_args; ++i) {
- out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
- }
- out << " ; #" << target->get_owner_id() << "\n";
-
- break;
- } else {
-
- // The e-graph only supports commutativity for binary functions
- out << "[eq-expl] #" << en->get_owner_id()
- << " cg (#" << en->get_arg(0)->get_owner_id() << " #" << target->get_arg(1)->get_owner_id()
- << ") (#" << en->get_arg(1)->get_owner_id() << " #" << target->get_arg(0)->get_owner_id()
- << ") ; #" << target->get_owner_id() << "\n";
- break;
- }
- case smt::eq_justification::kind::JUSTIFICATION:
- th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory();
- if (th_id != null_theory_id) {
- symbol const theory = m().get_family_name(th_id);
- out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n";
- } else {
- out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
- }
- break;
- default:
- out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
- break;
- }
- }
-
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
@@ -225,15 +225,15 @@ namespace smt {
// In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
// is used. We need to make sure that all of these equalities appear in the log.
for (unsigned i = 0; i < num_bindings; ++i) {
- log_justification_to_root(out, bindings[i], already_visited);
+ log_justification_to_root(out, bindings[i], already_visited, m_context, m());
}
for (auto n : used_enodes) {
enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n);
if (orig != nullptr) {
- log_justification_to_root(out, orig, already_visited);
- log_justification_to_root(out, substituted, already_visited);
+ log_justification_to_root(out, orig, already_visited, m_context, m());
+ log_justification_to_root(out, substituted, already_visited, m_context, m());
}
}
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index 4f14c6853..a126407d7 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -52,6 +52,11 @@ namespace smt {
quantifier_stat * get_stat(quantifier * q) const;
unsigned get_generation(quantifier * q) const;
+ static void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable<enode> &already_visited, context &ctx, ast_manager &m);
+ private:
+ static void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &already_visited, context &ctx, ast_manager &m);
+ public:
+
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index 66bb3e14b..ebce8df6f 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -20,6 +20,7 @@ Revision History:
#define SMT_THEORY_H_
#include "smt/smt_enode.h"
+#include "smt/smt_quantifier.h"
#include "util/obj_hashtable.h"
#include "util/statistics.h"
#include<typeinfo>
@@ -358,6 +359,67 @@ namespace smt {
std::ostream& display_var_flat_def(std::ostream & out, theory_var v) const { return display_flat_app(out, get_enode(v)->get_owner()); }
+ protected:
+ void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) {
+ ast_manager & m = get_manager();
+ symbol const & family_name = m.get_family_name(get_family_id());
+ if (pattern_id == UINT_MAX) {
+ m.trace_stream() << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << family_name << "#";
+ if (axiom_id != UINT_MAX)
+ m.trace_stream() << axiom_id;
+ for (unsigned i = 0; i < num_bindings; ++i) {
+ m.trace_stream() << " #" << bindings[i]->get_id();
+ }
+ if (used_enodes.size() > 0) {
+ m.trace_stream() << " ;";
+ for (auto n : used_enodes) {
+ enode *orig = std::get<0>(n);
+ enode *substituted = std::get<1>(n);
+ SASSERT(orig == nullptr);
+ m.trace_stream() << " #" << substituted->get_owner_id();
+ }
+ }
+ } else {
+ SASSERT(axiom_id != UINT_MAX);
+ obj_hashtable<enode> already_visited;
+ for (auto n : used_enodes) {
+ enode *orig = std::get<0>(n);
+ enode *substituted = std::get<1>(n);
+ if (orig != nullptr) {
+ quantifier_manager::log_justification_to_root(m.trace_stream(), orig, already_visited, get_context(), get_manager());
+ quantifier_manager::log_justification_to_root(m.trace_stream(), substituted, already_visited, get_context(), get_manager());
+ }
+ }
+ m.trace_stream() << "[new-match] " << static_cast<void *>(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id;
+ for (unsigned i = 0; i < num_bindings; ++i) {
+ m.trace_stream() << " #" << bindings[i]->get_id();
+ }
+ m.trace_stream() << " ;";
+ for (auto n : used_enodes) {
+ enode *orig = std::get<0>(n);
+ enode *substituted = std::get<1>(n);
+ if (orig == nullptr) {
+ m.trace_stream() << " #" << substituted->get_owner_id();
+ } else {
+ m.trace_stream() << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
+ }
+ }
+ }
+ m.trace_stream() << "\n";
+ m.trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << r->get_id() << "\n";
+ }
+
+ void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) { log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); }
+
+ void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) {
+ vector<std::tuple<enode *, enode *>> used_enodes;
+ for (unsigned i = 0; i < num_blamed_enodes; ++i) {
+ used_enodes.push_back(std::make_tuple(nullptr, blamed_enodes[i]));
+ }
+ log_axiom_instantiation(r, UINT_MAX, 0, nullptr, UINT_MAX, used_enodes);
+ }
+
+ public:
/**
\brief Assume eqs between variable that are equal with respect to the given table.
Table is a hashtable indexed by the variable value.
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index f70e50ece..bac82b083 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1239,6 +1239,10 @@ namespace smt {
farkas.add(abs(pa.get_rational()), to_app(tmp));
}
tmp = farkas.get();
+ if (m.has_trace_stream()) {
+ log_axiom_instantiation(tmp);
+ m.trace_stream() << "[end-of-instance]\n";
+ }
// IF_VERBOSE(1, verbose_stream() << "Farkas result: " << tmp << "\n";);
atom* a = get_bv2a(m_bound_watch);
SASSERT(a);
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index f3a3e9238..72bb263d0 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -447,7 +447,10 @@ namespace smt {
tout << l_ante << "\n" << l_conseq << "\n";);
// literal lits[2] = {l_ante, l_conseq};
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ante, conseq));
mk_clause(l_ante, l_conseq, 0, nullptr);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+
if (ctx.relevancy()) {
if (l_ante == false_literal) {
ctx.mark_as_relevant(l_conseq);
@@ -517,7 +520,9 @@ namespace smt {
expr_ref mod_j(m);
while(j < k) {
mod_j = m.mk_eq(mod, m_util.mk_numeral(j, true));
+ if (m.has_trace_stream()) log_axiom_instantiation(mod_j);
ctx.internalize(mod_j, false);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
literal lit(ctx.get_literal(mod_j));
lits.push_back(lit);
ctx.mark_as_relevant(lit);
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index afe527a98..f4e901de4 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -199,6 +199,7 @@ namespace smt {
void theory_arith<Ext>::branch_infeasible_int_var(theory_var v) {
SASSERT(is_int(v));
SASSERT(!get_value(v).is_int());
+ ast_manager & m = get_manager();
m_stats.m_branches++;
numeral k = ceil(get_value(v));
rational _k = k.to_rational();
@@ -206,13 +207,15 @@ namespace smt {
display_var(tout, v);
tout << "k = " << k << ", _k = "<< _k << std::endl;
);
- expr_ref bound(get_manager());
+ expr_ref bound(m);
expr* e = get_enode(v)->get_owner();
bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));
- TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(to_app(bound), m.mk_not(to_app(bound))));
+ TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";);
context & ctx = get_context();
ctx.internalize(bound, true);
ctx.mark_as_relevant(bound.get());
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
@@ -365,6 +368,7 @@ namespace smt {
mk_polynomial_ge(pol.size(), pol.c_ptr(), unsat_row[0]+rational(1), p2);
context& ctx = get_context();
+ if (get_manager().has_trace_stream()) log_axiom_instantiation(get_manager().mk_or(p1, p2));
ctx.internalize(p1, false);
ctx.internalize(p2, false);
literal l1(ctx.get_literal(p1)), l2(ctx.get_literal(p2));
@@ -372,6 +376,7 @@ namespace smt {
ctx.mark_as_relevant(p2.get());
ctx.mk_th_axiom(get_id(), l1, l2);
+ if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
TRACE("arith_int",
tout << "cut: (or " << mk_pp(p1, get_manager()) << " " << mk_pp(p2, get_manager()) << ")\n";
@@ -400,7 +405,9 @@ namespace smt {
bool _is_int = m_util.is_int(e);
expr * bound = m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int));
context & ctx = get_context();
+ if (get_manager().has_trace_stream()) log_axiom_instantiation(bound);
ctx.internalize(bound, true);
+ if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
ctx.mark_as_relevant(bound);
result = true;
}
@@ -646,7 +653,9 @@ namespace smt {
TRACE("gomory_cut", tout << "new cut:\n" << bound << "\n"; ante.display(tout););
literal l = null_literal;
context & ctx = get_context();
+ if (get_manager().has_trace_stream()) log_axiom_instantiation(bound);
ctx.internalize(bound, true);
+ if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
l = ctx.get_literal(bound);
ctx.mark_as_relevant(l);
dump_lemmas(l, ante);
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 24e1020fd..457c6e068 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -789,7 +789,10 @@ namespace smt {
bound = m_util.mk_eq(var2expr(v), m_util.mk_numeral(rational(0), true));
TRACE("non_linear", tout << "new bound:\n" << mk_pp(bound, get_manager()) << "\n";);
context & ctx = get_context();
+ ast_manager & m = get_manager();
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(bound, m.mk_not(bound)));
ctx.internalize(bound, true);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
ctx.mark_as_relevant(bound);
literal l = ctx.get_literal(bound);
SASSERT(!l.sign());
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index c024c0da0..9ba520c9d 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -111,7 +111,9 @@ namespace smt {
if (m.proofs_enabled()) {
literal l(mk_eq(sel, val, true));
ctx.mark_as_relevant(l);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
assert_axiom(l);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
else {
TRACE("mk_var_bug", tout << "mk_sel: " << sel->get_id() << "\n";);
@@ -189,7 +191,9 @@ namespace smt {
TRACE("array_map_bug", tout << "axiom2:\n";
tout << mk_ismt2_pp(idx1->get_owner(), m) << "\n=\n" << mk_ismt2_pp(idx2->get_owner(), m);
tout << "\nimplies\n" << mk_ismt2_pp(conseq_expr, m) << "\n";);
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(ante.var()), conseq_expr));
assert_axiom(ante, conseq);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}
@@ -331,7 +335,9 @@ namespace smt {
literal sel1_eq_sel2 = mk_eq(sel1, sel2, true);
ctx.mark_as_relevant(n1_eq_n2);
ctx.mark_as_relevant(sel1_eq_sel2);
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var()))));
assert_axiom(n1_eq_n2, ~sel1_eq_sel2);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
bool theory_array_base::can_propagate() {
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index d0a37175d..20aba9436 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -777,8 +777,10 @@ namespace smt {
else {
m_eqs.insert(v1, v2, true);
literal eq(mk_eq(v1, v2, true));
+ if (get_manager().has_trace_stream()) log_axiom_instantiation(get_context().bool_var2expr(eq.var()));
get_context().mark_as_relevant(eq);
assert_axiom(eq);
+ if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
// m_eqsv.push_back(eq);
return true;
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 33207d15a..36cddb1cc 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -229,9 +229,12 @@ namespace smt {
enode * e2 = get_enode(v2);
literal l = ~(mk_eq(e1->get_owner(), e2->get_owner(), true));
context & ctx = get_context();
+ ast_manager & m = get_manager();
+ expr * eq = ctx.bool_var2expr(l.var());
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq)));
ctx.mk_th_axiom(get_id(), 1, &l);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (ctx.relevancy()) {
- expr * eq = ctx.bool_var2expr(l.var());
relevancy_eh * eh = ctx.mk_relevancy_eh(pair_relevancy_eh(e1->get_owner(), e2->get_owner(), eq));
ctx.add_relevancy_eh(e1->get_owner(), eh);
ctx.add_relevancy_eh(e2->get_owner(), eh);
@@ -440,11 +443,13 @@ namespace smt {
e1 = mk_bit2bool(o1, i);
e2 = mk_bit2bool(o2, i);
literal eq = mk_eq(e1, e2, true);
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var()))));
ctx.mk_th_axiom(get_id(), l1, ~l2, ~eq);
ctx.mk_th_axiom(get_id(), ~l1, l2, ~eq);
ctx.mk_th_axiom(get_id(), l1, l2, eq);
ctx.mk_th_axiom(get_id(), ~l1, ~l2, eq);
ctx.mk_th_axiom(get_id(), eq, ~oeq);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
eqs.push_back(~eq);
}
eqs.push_back(oeq);
@@ -612,7 +617,9 @@ namespace smt {
);
ctx.mark_as_relevant(l);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
ctx.mk_th_axiom(get_id(), 1, &l);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
void theory_bv::internalize_int2bv(app* n) {
@@ -653,7 +660,9 @@ namespace smt {
literal l(mk_eq(lhs, rhs, false));
ctx.mark_as_relevant(l);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
ctx.mk_th_axiom(get_id(), 1, &l);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
TRACE("bv",
tout << mk_pp(lhs, m) << " == \n";
@@ -674,7 +683,9 @@ namespace smt {
TRACE("bv", tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";);
l = literal(mk_eq(lhs, rhs, false));
ctx.mark_as_relevant(l);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
ctx.mk_th_axiom(get_id(), 1, &l);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}
@@ -1126,8 +1137,10 @@ namespace smt {
unsigned num_bool_vars = ctx.get_num_bool_vars();
#endif
literal_vector & lits = m_tmp_literals;
+ ptr_vector<expr> exprs;
lits.reset();
- lits.push_back(mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true));
+ literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true);
+ lits.push_back(eq);
literal_vector const & bits1 = m_bits[v1];
literal_vector::const_iterator it1 = bits1.begin();
literal_vector::const_iterator end1 = bits1.end();
@@ -1147,9 +1160,12 @@ namespace smt {
ctx.internalize(diff, true);
literal arg = ctx.get_literal(diff);
lits.push_back(arg);
+ exprs.push_back(diff);
}
m_stats.m_num_diseq_dynamic++;
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_or(exprs.size(), exprs.c_ptr())));
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
TRACE_CODE({
static unsigned num = 0;
static unsigned new_bool_vars = 0;
@@ -1237,6 +1253,7 @@ namespace smt {
m_stats.m_num_bit2core++;
context & ctx = get_context();
+ ast_manager & m = get_manager();
SASSERT(ctx.get_assignment(antecedent) == l_true);
SASSERT(m_bits[v2][idx].var() == consequent.var());
SASSERT(consequent.var() != antecedent.var());
@@ -1253,8 +1270,11 @@ namespace smt {
literal_vector lits;
lits.push_back(~consequent);
lits.push_back(antecedent);
- lits.push_back(~mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false));
+ literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false);
+ lits.push_back(~eq);
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_implies(ctx.bool_var2expr(consequent.var()), ctx.bool_var2expr(antecedent.var()))));
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m_wpos[v2] == idx)
find_wpos(v2);
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 6aa49efae..9209d8b5d 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -140,7 +140,14 @@ namespace smt {
args.push_back(acc);
}
expr * mk = m.mk_app(c, args.size(), args.c_ptr());
+ app_ref ax(m);
+ ax = m.mk_eq(n->get_owner(), mk);
+ if (antecedent != null_literal) {
+ ax = m.mk_implies(get_context().bool_var2expr(antecedent.var()), ax);
+ }
+ if (m.has_trace_stream()) log_axiom_instantiation(ax, 1, &n);
assert_eq_axiom(n, mk, antecedent);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
/**
@@ -157,11 +164,22 @@ namespace smt {
func_decl * d = n->get_decl();
ptr_vector<func_decl> const & accessors = *m_util.get_constructor_accessors(d);
SASSERT(n->get_num_args() == accessors.size());
+ ptr_vector<app> bindings;
+ vector<std::tuple<enode *, enode *>> used_enodes;
+ used_enodes.push_back(std::make_tuple(nullptr, n));
+ for (unsigned i = 0; i < n->get_num_args(); ++i) {
+ bindings.push_back(n->get_arg(i)->get_owner());
+ }
+ unsigned base_id = get_manager().has_trace_stream() && accessors.size() > 0 ? m_util.get_plugin()->get_axiom_base_id(d->get_name()) : 0;
unsigned i = 0;
for (func_decl * acc : accessors) {
app * acc_app = m.mk_app(acc, n->get_owner());
enode * arg = n->get_arg(i);
+ app_ref eq(m);
+ eq = m.mk_eq(arg->get_owner(), acc_app);
+ if (m.has_trace_stream()) log_axiom_instantiation(eq, base_id + 3*i, bindings.size(), bindings.c_ptr(), base_id - 3, used_enodes);
assert_eq_axiom(arg, acc_app, null_literal);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
++i;
}
}
@@ -218,10 +236,18 @@ namespace smt {
arg = ctx.get_enode(acc_app);
}
app * acc_own = m.mk_app(acc1, own);
+ app_ref imp(m);
+ imp = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own));
+ if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n);
assert_eq_axiom(arg, acc_own, is_con);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
// update_field is identity if 'n' is not created by a matching constructor.
+ app_ref imp(m);
+ imp = m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_owner(), arg1));
+ if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n);
assert_eq_axiom(n, arg1, ~is_con);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
theory_var theory_datatype::mk_var(enode * n) {
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 48991da8e..b7bd9adf1 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -598,7 +598,9 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
le = m_util.mk_le(m_util.mk_add(n2,n1), n3);
le = get_manager().mk_not(le);
}
+ if (get_manager().has_trace_stream())log_axiom_instantiation(le);
ctx.internalize(le, false);
+ if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
ctx.mark_as_relevant(le.get());
literal lit(ctx.get_literal(le));
bool_var bv = lit.var();
@@ -1007,6 +1009,7 @@ void theory_diff_logic<Ext>::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v
t2 = m_util.mk_numeral(k, m.get_sort(s2.get()));
// t1 - s1 = k
eq = m.mk_eq(s2.get(), t2.get());
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_eq(m.mk_eq(m_util.mk_add(s1, t2), t1), eq));
TRACE("diff_logic",
tout << v1 << " .. " << v2 << "\n";
@@ -1015,6 +1018,8 @@ void theory_diff_logic<Ext>::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v
if (!internalize_atom(eq.get(), false)) {
UNREACHABLE();
}
+
+ if (m.has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
literal l(ctx.get_literal(eq.get()));
if (!is_eq) {
diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp
index 824bd1d9e..be99b1234 100644
--- a/src/smt/theory_dl.cpp
+++ b/src/smt/theory_dl.cpp
@@ -256,6 +256,7 @@ namespace smt {
lt = u().mk_lt(x,y);
le = b().mk_ule(m().mk_app(r,y),m().mk_app(r,x));
context& ctx = get_context();
+ if (m().has_trace_stream()) log_axiom_instantiation(m().mk_eq(lt, le));
ctx.internalize(lt, false);
ctx.internalize(le, false);
literal lit1(ctx.get_literal(lt));
@@ -266,12 +267,15 @@ namespace smt {
literal lits2[2] = { ~lit1, ~lit2 };
ctx.mk_th_axiom(get_id(), 2, lits1);
ctx.mk_th_axiom(get_id(), 2, lits2);
+ if (m().has_trace_stream()) m().trace_stream() << "[end-of-instance]\n";
}
void assert_cnstr(expr* e) {
TRACE("theory_dl", tout << mk_pp(e, m()) << "\n";);
context& ctx = get_context();
+ if (m().has_trace_stream()) log_axiom_instantiation(e);
ctx.internalize(e, false);
+ if (m().has_trace_stream()) m().trace_stream() << "[end-of-instance]\n";
literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 42d90c242..559615340 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -409,7 +409,9 @@ namespace smt {
if (get_manager().is_true(e)) return;
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
context & ctx = get_context();
+ if (get_manager().has_trace_stream()) log_axiom_instantiation(e);
ctx.internalize(e, false);
+ if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp
index 3b218f56d..802455683 100644
--- a/src/smt/theory_jobscheduler.cpp
+++ b/src/smt/theory_jobscheduler.cpp
@@ -306,6 +306,9 @@ namespace smt {
literal end_ge_lo = mk_ge(ji.m_end, clb);
// Initialization ensures that satisfiable states have completion time below end.
VERIFY(clb <= get_job_resource(j, r).m_end);
+ ast_manager& m = get_manager();
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var())));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
region& r = ctx.get_region();
ctx.assign(end_ge_lo,
ctx.mk_justification(
@@ -376,6 +379,9 @@ namespace smt {
lits.push_back(mk_eq_lit(end_e->get_owner(), rhs));
context& ctx = get_context();
ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr);
+ ast_manager& m = get_manager();
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var())));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
return true;
}
@@ -707,7 +713,9 @@ namespace smt {
// start(j) <= end(j)
lit = mk_le(ji.m_start, ji.m_end);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var()));
ctx.mk_th_axiom(get_id(), 1, &lit);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
time_t start_lb = std::numeric_limits<time_t>::max();
time_t runtime_lb = std::numeric_limits<time_t>::max();
@@ -735,11 +743,15 @@ namespace smt {
// start(j) >= start_lb
lit = mk_ge(ji.m_start, start_lb);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var()));
ctx.mk_th_axiom(get_id(), 1, &lit);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
// end(j) <= end_ub
lit = mk_le(ji.m_end, end_ub);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var()));
ctx.mk_th_axiom(get_id(), 1, &lit);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
// start(j) + runtime_lb <= end(j)
// end(j) <= start(j) + runtime_ub
@@ -754,7 +766,10 @@ namespace smt {
void theory_jobscheduler::assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq) {
job_info const& ji = m_jobs[j];
literal l2 = mk_le(ji.m_end, jr.m_end);
- get_context().mk_th_axiom(get_id(), ~eq, l2);
+ context& ctx = get_context();
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var())));
+ ctx.mk_th_axiom(get_id(), ~eq, l2);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
// resource(j) = r => start(j) <= lst(j, r, end(j, r))
@@ -762,11 +777,16 @@ namespace smt {
context& ctx = get_context();
time_t t;
if (lst(j, r, t)) {
- ctx.mk_th_axiom(get_id(), ~eq, mk_le(m_jobs[j].m_start, t));
+ literal le = mk_le(m_jobs[j].m_start, t);
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(le.var())));
+ ctx.mk_th_axiom(get_id(), ~eq, le);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
else {
eq.neg();
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_not(ctx.bool_var2expr(eq.var())));
ctx.mk_th_axiom(get_id(), 1, &eq);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}
@@ -777,7 +797,10 @@ namespace smt {
if (!first_available(jr, m_resources[r], idx)) return;
vector<res_available>& available = m_resources[r].m_available;
literal l2 = mk_ge(m_jobs[j].m_start, available[idx].m_start);
- get_context().mk_th_axiom(get_id(), ~eq, l2);
+ context& ctx = get_context();
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var())));
+ ctx.mk_th_axiom(get_id(), ~eq, l2);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
// resource(j) = r => start(j) <= end[idx] || start[idx+1] <= start(j);
@@ -788,7 +811,11 @@ namespace smt {
SASSERT(resource_available(jr, available[idx]));
literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
literal l3 = mk_le(m_jobs[j].m_start, available[idx].m_end);
- get_context().mk_th_axiom(get_id(), ~eq, l2, l3);
+ context& ctx = get_context();
+ ast_manager& m = get_manager();
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var()))));
+ ctx.mk_th_axiom(get_id(), ~eq, l2, l3);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
// resource(j) = r => end(j) <= end[idx] || start[idx+1] <= start(j);
@@ -799,7 +826,11 @@ namespace smt {
SASSERT(resource_available(jr, available[idx]));
literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end);
literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
- get_context().mk_th_axiom(get_id(), ~eq, l2, l3);
+ context& ctx = get_context();
+ ast_manager& m = get_manager();
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var()))));
+ ctx.mk_th_axiom(get_id(), ~eq, l2, l3);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
/**
@@ -808,6 +839,7 @@ namespace smt {
bool theory_jobscheduler::split_job2resource(unsigned j) {
job_info const& ji = m_jobs[j];
context& ctx = get_context();
+ ast_manager& m = get_manager();
if (ji.m_is_bound) return false;
auto const& jrs = ji.m_resources;
for (job_resource const& jr : jrs) {
@@ -818,6 +850,8 @@ namespace smt {
if (ctx.is_diseq(e1, e2))
continue;
literal eq = mk_eq_lit(e1, e2);
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var()))));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (ctx.get_assignment(eq) != l_false) {
ctx.mark_as_relevant(eq);
if (assume_eq(e1, e2)) {
@@ -826,14 +860,19 @@ namespace smt {
}
}
literal_vector lits;
+ ptr_vector<expr> exprs;
for (job_resource const& jr : jrs) {
unsigned r = jr.m_resource_id;
res_info const& ri = m_resources[r];
enode* e1 = ji.m_job2resource;
enode* e2 = ri.m_resource;
- lits.push_back(mk_eq_lit(e1, e2));
+ literal eq = mk_eq_lit(e1, e2);
+ lits.push_back(eq);
+ exprs.push_back(ctx.bool_var2expr(eq.var()));
}
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(exprs.size(), exprs.c_ptr()));
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
return true;
}
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 0b25aa626..2fad2f97b 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1038,9 +1038,14 @@ public:
expr_ref rem(a.mk_rem(dividend, divisor), m);
expr_ref mod(a.mk_mod(dividend, divisor), m);
expr_ref mmod(a.mk_uminus(mod), m);
- literal dgez = mk_literal(a.mk_ge(divisor, zero));
- mk_axiom(~dgez, th.mk_eq(rem, mod, false));
- mk_axiom( dgez, th.mk_eq(rem, mmod, false));
+ expr_ref degz_expr(a.mk_ge(divisor, zero), m);
+ literal dgez = mk_literal(degz_expr);
+ literal pos = th.mk_eq(rem, mod, false);
+ literal neg = th.mk_eq(rem, mmod, false);
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_ite(degz_expr, ctx().bool_var2expr(pos.var()), ctx().bool_var2expr(neg.var())));
+ mk_axiom(~dgez, pos);
+ mk_axiom( dgez, neg);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
// q = 0 or q * (p div q) = p
@@ -1048,7 +1053,9 @@ public:
if (a.is_zero(q)) return;
literal eqz = th.mk_eq(q, a.mk_real(0), false);
literal eq = th.mk_eq(a.mk_mul(q, a.mk_div(p, q)), p, false);
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(ctx().bool_var2expr(eqz.var())), ctx().bool_var2expr(eq.var())));
mk_axiom(eqz, eq);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
// to_int (to_real x) = x
@@ -1057,14 +1064,20 @@ public:
expr* x = nullptr, *y = nullptr;
VERIFY (a.is_to_int(n, x));
if (a.is_to_real(x, y)) {
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_eq(n, y));
mk_axiom(th.mk_eq(y, n, false));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
else {
expr_ref to_r(a.mk_to_real(n), m);
expr_ref lo(a.mk_le(a.mk_sub(to_r, x), a.mk_real(0)), m);
expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m);
+ if (m.has_trace_stream()) th.log_axiom_instantiation(lo);
mk_axiom(mk_literal(lo));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_not(hi));
mk_axiom(~mk_literal(hi));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}
@@ -1074,8 +1087,10 @@ public:
VERIFY(a.is_is_int(n, x));
literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
literal is_int = ctx().get_literal(n);
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_iff(n, ctx().bool_var2expr(eq.var())));
mk_axiom(~is_int, eq);
mk_axiom(is_int, ~eq);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
// create axiom for
@@ -1127,17 +1142,32 @@ public:
k = rational::zero();
}
+ context& c = ctx();
if (!k.is_zero()) {
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
mk_axiom(eq);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
mk_axiom(mod_ge_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper)));
mk_axiom(mk_literal(a.mk_le(mod, upper)));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (k.is_pos()) {
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
mk_axiom(~p_ge_0, div_ge_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
mk_axiom(~p_le_0, div_le_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
else {
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
mk_axiom(~p_ge_0, div_le_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
mk_axiom(~p_le_0, div_ge_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}
else {
@@ -1149,26 +1179,46 @@ public:
// q >= 0 or (p mod q) < -q
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
literal q_le_0 = mk_literal(a.mk_le(q, zero));
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
mk_axiom(q_ge_0, eq);
mk_axiom(q_le_0, eq);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
mk_axiom(q_ge_0, mod_ge_0);
mk_axiom(q_le_0, mod_ge_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero)));
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)));
mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
mk_axiom(q_le_0, ~p_ge_0, div_ge_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
mk_axiom(q_le_0, ~p_le_0, div_le_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
mk_axiom(q_ge_0, ~p_ge_0, div_le_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
mk_axiom(q_ge_0, ~p_le_0, div_ge_0);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
unsigned _k = k.get_unsigned();
literal_buffer lits;
+ ptr_vector<expr> exprs;
for (unsigned j = 0; j < _k; ++j) {
literal mod_j = th.mk_eq(mod, a.mk_int(j), false);
lits.push_back(mod_j);
+ exprs.push_back(c.bool_var2expr(mod_j.var()));
ctx().mark_as_relevant(mod_j);
}
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_or(exprs.size(), exprs.c_ptr()));
ctx().mk_th_axiom(get_id(), lits.size(), lits.begin());
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}
@@ -1603,8 +1653,12 @@ public:
literal p_ge_r1 = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true)));
literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true)));
literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true)));
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var())));
mk_axiom(~p_le_r1, n_le_div);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var())));
mk_axiom(~p_ge_r1, n_ge_div);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
all_divs_valid = false;
@@ -1643,8 +1697,12 @@ public:
literal pq_rhs = ~mk_literal(a.mk_ge(pqr, zero));
literal n_le_div = mk_literal(a.mk_le(n, divc));
literal n_ge_div = mk_literal(a.mk_ge(n, divc));
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(pq_lhs.var()), ctx().bool_var2expr(n_le_div.var())));
mk_axiom(pq_lhs, n_le_div);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(pq_rhs.var()), ctx().bool_var2expr(n_ge_div.var())));
mk_axiom(pq_rhs, n_ge_div);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
TRACE("arith",
literal_vector lits;
lits.push_back(pq_lhs);
@@ -1759,6 +1817,8 @@ public:
case lp::lia_move::branch: {
TRACE("arith", tout << "branch\n";);
app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
+ if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_or(b, m.mk_not(b)));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";);
// branch on term >= k + 1
// branch on term <= k
@@ -1772,6 +1832,8 @@ public:
++m_stats.m_gomory_cuts;
// m_explanation implies term <= k
app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
+ if (m.has_trace_stream()) th.log_axiom_instantiation(b);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n");
TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper()););
m_eqs.reset();
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 303bf5155..08434b0d0 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -308,7 +308,9 @@ namespace smt {
unsigned depth = get_depth(e.m_lhs);
expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
literal lit = mk_eq_lit(lhs, rhs);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx().bool_var2expr(lit.var()));
ctx().mk_th_axiom(get_id(), 1, &lit);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
TRACEFN("macro expansion yields " << mk_pp(rhs, m) << "\n" <<
"literal " << pp_lit(ctx(), lit));
}
@@ -327,6 +329,7 @@ namespace smt {
// add case-axioms for all case-paths
auto & vars = e.m_def->get_vars();
literal_vector preds;
+ ptr_vector<expr> pred_exprs;
for (recfun::case_def const & c : e.m_def->get_cases()) {
// applied predicate to `args`
app_ref pred_applied = c.apply_case_predicate(e.m_args);
@@ -337,6 +340,7 @@ namespace smt {
SASSERT(u().owns_app(pred_applied));
literal concl = mk_literal(pred_applied);
preds.push_back(concl);
+ pred_exprs.push_back(pred_applied);
if (c.is_immediate()) {
body_expansion be(pred_applied, c, e.m_args);
@@ -348,20 +352,27 @@ namespace smt {
}
literal_vector guards;
+ ptr_vector<expr> exprs;
guards.push_back(concl);
for (auto & g : c.get_guards()) {
expr_ref ga = apply_args(depth, vars, e.m_args, g);
literal guard = mk_literal(ga);
guards.push_back(~guard);
+ exprs.push_back(m.mk_not(ga));
literal c[2] = {~concl, guard};
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(pred_applied, ga));
ctx().mk_th_axiom(get_id(), 2, c);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(pred_applied), m.mk_or(exprs.size(), exprs.c_ptr())));
ctx().mk_th_axiom(get_id(), guards);
-
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
// the disjunction of branches is asserted
// to close the available cases.
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(pred_exprs.size(), pred_exprs.c_ptr()));
ctx().mk_th_axiom(get_id(), preds);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
/**
@@ -382,9 +393,11 @@ namespace smt {
expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
literal_vector clause;
+ ptr_vector<expr> exprs;
for (auto & g : e.m_cdef->get_guards()) {
expr_ref guard = apply_args(depth, vars, args, g);
clause.push_back(~mk_literal(guard));
+ exprs.push_back(guard);
if (clause.back() == true_literal) {
TRACEFN("body " << pp_body_expansion(e,m) << "\n" << clause << "\n" << guard);
return;
@@ -394,7 +407,9 @@ namespace smt {
}
}
clause.push_back(mk_eq_lit(lhs, rhs));
+ if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(exprs.size(), exprs.c_ptr()), m.mk_eq(lhs, rhs)));
ctx().mk_th_axiom(get_id(), clause);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
TRACEFN("body " << pp_body_expansion(e,m));
TRACEFN(pp_lits(ctx(), clause));
}
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 2bce6cf56..98192f3ae 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2169,6 +2169,12 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
m_new_propagation = true;
ctx.assign(lit, js);
+ if (m.has_trace_stream()) {
+ expr* expr = ctx.bool_var2expr(lit.var());
+ if (lit.sign()) expr = get_manager().mk_not(expr);
+ log_axiom_instantiation(expr);
+ m.trace_stream() << "[end-of-instance]\n";
+ }
}
void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) {
@@ -2202,7 +2208,9 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
justification* js = ctx.mk_justification(
ext_theory_eq_propagation_justification(
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_eq(n1->get_owner(), n2->get_owner()));
ctx.assign_eq(n1, n2, eq_justification(js));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
m_new_propagation = true;
enforce_length_coherence(n1, n2);
@@ -3165,6 +3173,16 @@ bool theory_seq::solve_nc(unsigned idx) {
}
TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()) << "\n";);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+ if (m.has_trace_stream()) {
+ ptr_vector<expr> exprs;
+ for (literal l : lits) {
+ expr* e = ctx.bool_var2expr(l.var());
+ if (l.sign()) e = get_manager().mk_not(e);
+ exprs.push_back(e);
+ }
+ log_axiom_instantiation(get_manager().mk_or(exprs.size(), exprs.c_ptr()));
+ m.trace_stream() << "[end-of-instance]\n";
+ }
return true;
}
@@ -4571,12 +4589,17 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
if (!lits.empty()) {
TRACE("seq", tout << "creating intersection " << e3 << "\n";);
lits.push_back(lit);
- literal inter = mk_literal(m_util.re.mk_in_re(s, e3));
+ expr* e = m_util.re.mk_in_re(s, e3);
+ literal inter = mk_literal(e);
justification* js =
ctx.mk_justification(
ext_theory_propagation_justification(
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), inter));
ctx.assign(inter, js);
+ if (m.has_trace_stream()) {
+ log_axiom_instantiation(e);
+ m.trace_stream() << "[end-of-instance]\n";
+ }
return;
}
@@ -4592,16 +4615,21 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
unsigned_vector states;
a->get_epsilon_closure(a->init(), states);
lits.push_back(~lit);
+ ptr_vector<expr> exprs;
for (unsigned st : states) {
- lits.push_back(mk_accept(s, zero, e3, st));
+ literal acc = mk_accept(s, zero, e3, st);
+ lits.push_back(acc);
+ exprs.push_back(ctx.bool_var2expr(acc.var()));
}
if (lits.size() == 2) {
propagate_lit(nullptr, 1, &lit, lits[1]);
}
else {
TRACE("seq", ctx.display_literals_verbose(tout, lits) << "\n";);
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(n, get_manager().mk_or(exprs.size(), exprs.c_ptr())));
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}
@@ -5060,19 +5088,28 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
return lit;
}
+void theory_seq::push_lit_as_expr(literal l, ptr_vector<expr>& buf) {
+ expr* e = get_context().bool_var2expr(l.var());
+ if (l.sign()) e = get_manager().mk_not(e);
+ buf.push_back(e);
+}
+
void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, literal l5) {
context& ctx = get_context();
literal_vector lits;
+ ptr_vector<expr> exprs;
if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal || l5 == true_literal) return;
- if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); }
- if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); }
- if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); }
- if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); }
- if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); }
+ if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); push_lit_as_expr(l1, exprs); }
+ if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); push_lit_as_expr(l2, exprs); }
+ if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); push_lit_as_expr(l3, exprs); }
+ if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); push_lit_as_expr(l4, exprs); }
+ if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); push_lit_as_expr(l5, exprs); }
TRACE("seq", ctx.display_literals_verbose(tout << "assert:\n", lits) << "\n";);
m_new_propagation = true;
++m_stats.m_add_axiom;
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_or(exprs.size(), exprs.c_ptr()));
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
expr* theory_seq::coalesce_chars(expr* const& e) {
@@ -5195,7 +5232,9 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
m_new_propagation = true;
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_eq(e1, e2));
ctx.assign_eq(n1, n2, eq_justification(js));
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
@@ -5237,7 +5276,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
lits.push_back(mk_literal(d));
}
++m_stats.m_add_axiom;
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(e, get_manager().mk_or(disj.size(), disj.c_ptr())));
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
for (expr* d : disj) {
add_axiom(lit, ~mk_literal(d));
}
@@ -5557,14 +5598,19 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
eautomaton::moves mvs;
aut->get_moves_from(src, mvs);
TRACE("seq", tout << mvs.size() << "\n";);
+ ptr_vector<expr> exprs;
for (auto const& mv : mvs) {
expr_ref nth = mk_nth(e, idx);
expr_ref t = mv.t()->accept(nth);
get_context().get_rewriter()(t);
- literal step = mk_literal(mk_step(e, idx, re, src, mv.dst(), t));
+ expr* step_e = mk_step(e, idx, re, src, mv.dst(), t);
+ literal step = mk_literal(step_e);
lits.push_back(step);
+ exprs.push_back(step_e);
}
+ if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(acc, get_manager().mk_or(exprs.size(), exprs.c_ptr())));
get_context().mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index aa278e972..83da23401 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -542,6 +542,7 @@ namespace smt {
// terms whose meaning are encoded using axioms.
void enque_axiom(expr* e);
void deque_axiom(expr* e);
+ void push_lit_as_expr(literal l, ptr_vector<expr>& buf);
void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);
void add_indexof_axiom(expr* e);
void add_replace_axiom(expr* e);
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index f0e11c248..3bfda2379 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -217,7 +217,9 @@ namespace smt {
}
literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit);
+ if (m.has_trace_stream()) log_axiom_instantiation(e);
ctx.mk_th_axiom(get_id(), 1, &lit);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
// crash/error avoidance: add all axioms to the trail
m_trail.push_back(e);
@@ -1084,7 +1086,9 @@ namespace smt {
literal lit(mk_eq(len_str, len, false));
ctx.mark_as_relevant(lit);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var()));
ctx.mk_th_axiom(get_id(), 1, &lit);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
} else {
// build axiom 1: Length(a_str) >= 0
{
@@ -1126,7 +1130,9 @@ namespace smt {
TRACE("str", tout << "string axiom 2: " << mk_ismt2_pp(lhs, m) << " <=> " << mk_ismt2_pp(rhs, m) << std::endl;);
literal l(mk_eq(lhs, rhs, true));
ctx.mark_as_relevant(l);
+ if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
ctx.mk_th_axiom(get_id(), 1, &l);
+ if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}