diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 5a7afc02d..48b97583e 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -14,6 +14,11 @@ Version 4.11.0
==============
- remove `Z3_bool`, `Z3_TRUE`, `Z3_FALSE` from the API. Use `bool`, `true`, `false` instead.
- z3++.h no longer includes `<sstream>` as it did not use it.
+- add solver.axioms2files
+ - prints negated theory axioms to files. Each file should be unsat
+- add solver.lemmas2console
+ - prints lemmas to the console.
+- remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
Version 4.10.2
==============
diff --git a/src/smt/.#smt_justification.h b/src/smt/.#smt_justification.h
new file mode 100644
index 000000000..0852723f4
--- /dev/null
+++ b/src/smt/.#smt_justification.h
@@ -0,0 +1 @@
+nbjorner@DESKTOP-7DPTQP8.49008:1659539981
\ No newline at end of file
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index ab5ee9a98..55b73030c 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -19,6 +19,7 @@ Revision History:
#include "smt/params/smt_params.h"
#include "smt/params/smt_params_helper.hpp"
#include "util/gparams.h"
+#include "solver/solver_params.hpp"
void smt_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
@@ -59,6 +60,9 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_dump_benchmarks = false;
m_dump_min_time = 0.5;
m_dump_recheck = false;
+ solver_params sp(_p);
+ m_axioms2files = sp.axioms2files();
+ m_lemmas2console = sp.lemmas2console();
}
void smt_params::updt_params(params_ref const & p) {
@@ -150,7 +154,8 @@ void smt_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_old_clause_relevancy);
DISPLAY_PARAM(m_inv_clause_decay);
- DISPLAY_PARAM(m_smtlib_dump_lemmas);
+ DISPLAY_PARAM(m_axioms2files);
+ DISPLAY_PARAM(m_lemmas2console);
DISPLAY_PARAM(m_logic);
DISPLAY_PARAM(m_string_solver);
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 5a13c69ac..29a5f94b4 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -82,144 +82,145 @@ struct smt_params : public preprocessor_params,
public theory_seq_params,
public theory_pb_params,
public theory_datatype_params {
- bool m_display_proof;
- bool m_display_dot_proof;
- bool m_display_unsat_core;
- bool m_check_proof;
- bool m_eq_propagation;
- bool m_binary_clause_opt;
- unsigned m_relevancy_lvl;
- bool m_relevancy_lemma;
- unsigned m_random_seed;
- double m_random_var_freq;
- double m_inv_decay;
+ bool m_display_proof = false;
+ bool m_display_dot_proof = false;
+ bool m_display_unsat_core = false;
+ bool m_check_proof = false;
+ bool m_eq_propagation = true;
+ bool m_binary_clause_opt = true;
+ unsigned m_relevancy_lvl = 2;
+ bool m_relevancy_lemma = false;
+ unsigned m_random_seed = 0;
+ double m_random_var_freq = 1.052;
+ double m_inv_decay = 1;
unsigned m_clause_decay;
- initial_activity m_random_initial_activity;
- phase_selection m_phase_selection;
- unsigned m_phase_caching_on;
- unsigned m_phase_caching_off;
- bool m_minimize_lemmas;
- unsigned m_max_conflicts;
+ initial_activity m_random_initial_activity = initial_activity::IA_RANDOM_WHEN_SEARCHING;
+ phase_selection m_phase_selection = phase_selection::PS_CACHING_CONSERVATIVE;
+ unsigned m_phase_caching_on = 700;
+ unsigned m_phase_caching_off = 100;
+ bool m_minimize_lemmas = true;
+ unsigned m_max_conflicts = UINT_MAX;
unsigned m_restart_max;
- unsigned m_cube_depth;
- unsigned m_threads;
- unsigned m_threads_max_conflicts;
- unsigned m_threads_cube_frequency;
- bool m_simplify_clauses;
- unsigned m_tick;
- bool m_display_features;
- bool m_new_core2th_eq;
- bool m_ematching;
- bool m_induction;
- bool m_clause_proof;
+ unsigned m_cube_depth = 1;
+ unsigned m_threads = 1;
+ unsigned m_threads_max_conflicts = UINT_MAX;
+ unsigned m_threads_cube_frequency = 2;
+ bool m_simplify_clauses = true;
+ unsigned m_tick = 1000;
+ bool m_display_features = false;
+ bool m_new_core2th_eq = true;
+ bool m_ematching = true;
+ bool m_induction = false;
+ bool m_clause_proof = false;
// -----------------------------------
//
// Case split strategy
//
// -----------------------------------
- case_split_strategy m_case_split_strategy;
- unsigned m_rel_case_split_order;
- bool m_lookahead_diseq;
- bool m_theory_case_split;
- bool m_theory_aware_branching;
+ case_split_strategy m_case_split_strategy = case_split_strategy::CS_ACTIVITY_DELAY_NEW;
+ unsigned m_rel_case_split_order = 0;
+ bool m_lookahead_diseq = false;
+ bool m_theory_case_split = false;
+ bool m_theory_aware_branching = false;
// -----------------------------------
//
// Delay units...
//
// -----------------------------------
- bool m_delay_units;
- unsigned m_delay_units_threshold;
+ bool m_delay_units = false;
+ unsigned m_delay_units_threshold = 32;
// -----------------------------------
//
// Conflict resolution
//
// -----------------------------------
- bool m_theory_resolve;
+ bool m_theory_resolve = false;
// -----------------------------------
//
// Restart
//
// -----------------------------------
- restart_strategy m_restart_strategy;
- unsigned m_restart_initial;
- double m_restart_factor;
- bool m_restart_adaptive;
- double m_agility_factor;
- double m_restart_agility_threshold;
+ restart_strategy m_restart_strategy = restart_strategy::RS_IN_OUT_GEOMETRIC;
+ unsigned m_restart_initial = 100;
+ double m_restart_factor = 1.1;
+ bool m_restart_adaptive = true;
+ double m_agility_factor = 0.9999;
+ double m_restart_agility_threshold = 0.18;
// -----------------------------------
//
// Lemma garbage collection
//
// -----------------------------------
- lemma_gc_strategy m_lemma_gc_strategy;
- bool m_lemma_gc_half;
- unsigned m_recent_lemmas_size;
- unsigned m_lemma_gc_initial;
- double m_lemma_gc_factor;
- unsigned m_new_old_ratio; //!< the ratio of new and old clauses.
- unsigned m_new_clause_activity;
- unsigned m_old_clause_activity;
- unsigned m_new_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant.
- unsigned m_old_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant.
- double m_inv_clause_decay; //!< clause activity decay
+ lemma_gc_strategy m_lemma_gc_strategy = lemma_gc_strategy::LGC_FIXED;
+ bool m_lemma_gc_half = false;
+ unsigned m_recent_lemmas_size = 100;
+ unsigned m_lemma_gc_initial = 5000;
+ double m_lemma_gc_factor = 1.1;
+ unsigned m_new_old_ratio = 16; //!< the ratio of new and old clauses.
+ unsigned m_new_clause_activity = 10;
+ unsigned m_old_clause_activity = 500;
+ unsigned m_new_clause_relevancy = 45; //!< Max. number of unassigned literals to be considered relevant.
+ unsigned m_old_clause_relevancy = 6; //!< Max. number of unassigned literals to be considered relevant.
+ double m_inv_clause_decay = 1; //!< clause activity decay
// -----------------------------------
//
// SMT-LIB (debug) pretty printer
//
// -----------------------------------
- bool m_smtlib_dump_lemmas;
- symbol m_logic;
+ bool m_axioms2files = false;
+ bool m_lemmas2console = false;
+ symbol m_logic = symbol::null;
// -----------------------------------
//
// Statistics for Profiling
//
// -----------------------------------
- bool m_profile_res_sub;
- bool m_display_bool_var2expr;
- bool m_display_ll_bool_var2expr;
+ bool m_profile_res_sub = false;
+ bool m_display_bool_var2expr = false;
+ bool m_display_ll_bool_var2expr = false;
// -----------------------------------
//
// Model generation
//
// -----------------------------------
- bool m_model;
- bool m_model_on_timeout;
- bool m_model_on_final_check;
+ bool m_model = true;
+ bool m_model_on_timeout = false;
+ bool m_model_on_final_check = false;
// -----------------------------------
//
// Progress sampling
//
// -----------------------------------
- unsigned m_progress_sampling_freq;
+ unsigned m_progress_sampling_freq = 0;
// -----------------------------------
//
// Debugging goodies
//
// -----------------------------------
- bool m_core_validate;
+ bool m_core_validate = false;
// -----------------------------------
//
// From front_end_params
//
// -----------------------------------
- bool m_preprocess; // temporary hack for disabling all preprocessing..
- bool m_user_theory_preprocess_axioms;
- bool m_user_theory_persist_axioms;
- bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
- bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
- bool m_dump_goal_as_smt;
- bool m_auto_config;
+ bool m_preprocess = true; // temporary hack for disabling all preprocessing..
+ bool m_user_theory_preprocess_axioms = false;
+ bool m_user_theory_persist_axioms = false;
+ bool m_at_labels_cex = false; // only use labels which contains the @ symbol when building multiple counterexamples.
+ bool m_check_at_labels = false; // check that @ labels are inserted to generate unique counter-examples.
+ bool m_dump_goal_as_smt = false;
+ bool m_auto_config = true;
// -----------------------------------
//
@@ -238,77 +239,6 @@ struct smt_params : public preprocessor_params,
symbol m_string_solver;
smt_params(params_ref const & p = params_ref()):
- m_display_proof(false),
- m_display_dot_proof(false),
- m_display_unsat_core(false),
- m_check_proof(false),
- m_eq_propagation(true),
- m_binary_clause_opt(true),
- m_relevancy_lvl(2),
- m_relevancy_lemma(false),
- m_random_seed(0),
- m_random_var_freq(0.01),
- m_inv_decay(1.052),
- m_clause_decay(1),
- m_random_initial_activity(initial_activity::IA_RANDOM_WHEN_SEARCHING),
- m_phase_selection(phase_selection::PS_CACHING_CONSERVATIVE),
- m_phase_caching_on(700),
- m_phase_caching_off(100),
- m_minimize_lemmas(true),
- m_max_conflicts(UINT_MAX),
- m_cube_depth(1),
- m_threads(1),
- m_threads_max_conflicts(UINT_MAX),
- m_threads_cube_frequency(2),
- m_simplify_clauses(true),
- m_tick(1000),
- m_display_features(false),
- m_new_core2th_eq(true),
- m_ematching(true),
- m_induction(false),
- m_clause_proof(false),
- m_case_split_strategy(case_split_strategy::CS_ACTIVITY_DELAY_NEW),
- m_rel_case_split_order(0),
- m_lookahead_diseq(false),
- m_theory_case_split(false),
- m_theory_aware_branching(false),
- m_delay_units(false),
- m_delay_units_threshold(32),
- m_theory_resolve(false),
- m_restart_strategy(restart_strategy::RS_IN_OUT_GEOMETRIC),
- m_restart_initial(100),
- m_restart_factor(1.1),
- m_restart_adaptive(true),
- m_agility_factor(0.9999),
- m_restart_agility_threshold(0.18),
- m_lemma_gc_strategy(lemma_gc_strategy::LGC_FIXED),
- m_lemma_gc_half(false),
- m_recent_lemmas_size(100),
- m_lemma_gc_initial(5000),
- m_lemma_gc_factor(1.1),
- m_new_old_ratio(16),
- m_new_clause_activity(10),
- m_old_clause_activity(500),
- m_new_clause_relevancy(45),
- m_old_clause_relevancy(6),
- m_inv_clause_decay(1),
- m_smtlib_dump_lemmas(false),
- m_logic(symbol::null),
- m_profile_res_sub(false),
- m_display_bool_var2expr(false),
- m_display_ll_bool_var2expr(false),
- m_model(true),
- m_model_on_timeout(false),
- m_model_on_final_check(false),
- m_progress_sampling_freq(0),
- m_core_validate(false),
- m_preprocess(true), // temporary hack for disabling all preprocessing..
- m_user_theory_preprocess_axioms(false),
- m_user_theory_persist_axioms(false),
- m_at_labels_cex(false),
- m_check_at_labels(false),
- m_dump_goal_as_smt(false),
- m_auto_config(true),
m_string_solver(symbol("auto")){
updt_local_params(p);
}
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index deec4e4da..565000ebe 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -34,7 +34,6 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_int_eq_branching = p.arith_int_eq_branch();
m_arith_ignore_int = p.arith_ignore_int();
m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
- m_arith_dump_lemmas = p.arith_dump_lemmas();
m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
m_arith_auto_config_simplex = p.arith_auto_config_simplex();
@@ -67,7 +66,6 @@ void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_arith_adaptive);
DISPLAY_PARAM(m_arith_adaptive_assertion_threshold);
DISPLAY_PARAM(m_arith_adaptive_propagation_threshold);
- DISPLAY_PARAM(m_arith_dump_lemmas);
DISPLAY_PARAM(m_arith_eager_eq_axioms);
DISPLAY_PARAM(m_arith_branch_cut_ratio);
DISPLAY_PARAM(m_arith_int_eq_branching);
diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h
index d45a902db..526cb6f09 100644
--- a/src/smt/params/theory_arith_params.h
+++ b/src/smt/params/theory_arith_params.h
@@ -72,7 +72,6 @@ struct theory_arith_params {
bool m_arith_adaptive = false;
double m_arith_adaptive_assertion_threshold = 0.2;
double m_arith_adaptive_propagation_threshold = 0.4;
- bool m_arith_dump_lemmas = false;
bool m_arith_eager_eq_axioms = true;
unsigned m_arith_branch_cut_ratio = 2;
bool m_arith_int_eq_branching = false;
diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index fee223612..bd4d8dec2 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -86,7 +86,7 @@ void seq_axioms::add_clause(expr_ref_vector const& clause) {
justification* js =
ctx().mk_justification(
ext_theory_eq_propagation_justification(
- th.get_id(), ctx().get_region(), 0, nullptr, 0, nullptr, n1, n2));
+ th.get_id(), ctx(), 0, nullptr, 0, nullptr, n1, n2));
ctx().assign_eq(n1, n2, eq_justification(js));
return;
}
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 420147256..b4f6a2309 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -80,7 +80,8 @@ namespace smt {
m_unsat_core(m),
m_mk_bool_var_trail(*this),
m_mk_enode_trail(*this),
- m_mk_lambda_trail(*this) {
+ m_mk_lambda_trail(*this),
+ m_lemma_visitor(m) {
SASSERT(m_scope_lvl == 0);
SASSERT(m_base_lvl == 0);
@@ -2560,7 +2561,7 @@ namespace smt {
justification * js = cls.get_justification();
justification * new_js = nullptr;
if (js->in_region())
- new_js = mk_justification(unit_resolution_justification(m_region,
+ new_js = mk_justification(unit_resolution_justification(*this,
js,
simp_lits.size(),
simp_lits.data()));
@@ -2618,7 +2619,7 @@ namespace smt {
if (!cls_js || cls_js->in_region()) {
// If cls_js is 0 or is allocated in a region, then
// we can allocate the new justification in a region too.
- js = mk_justification(unit_resolution_justification(m_region,
+ js = mk_justification(unit_resolution_justification(*this,
cls_js,
simp_lits.size(),
simp_lits.data()));
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 8d98fc60e..f91878632 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -892,6 +892,10 @@ namespace smt {
void remove_lit_occs(clause const& cls, unsigned num_bool_vars);
void add_lit_occs(clause const& cls);
+
+ ast_pp_util m_lemma_visitor;
+ void dump_lemma(unsigned n, literal const* lits);
+ void dump_axiom(unsigned n, literal const* lits);
public:
void ensure_internalized(expr* e);
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 092bc0127..648ea9b7e 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -24,6 +24,8 @@ Revision History:
#include "smt/smt_model_finder.h"
#include "ast/for_each_expr.h"
+#include <iostream>
+
namespace smt {
/**
@@ -1372,8 +1374,10 @@ namespace smt {
TRACE("mk_clause", display_literals_verbose(tout << "creating clause: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";);
m_clause_proof.add(num_lits, lits, k, j);
switch (k) {
- case CLS_AUX:
- case CLS_TH_AXIOM: {
+ case CLS_TH_AXIOM:
+ dump_axiom(num_lits, lits);
+ Z3_fallthrough;
+ case CLS_AUX: {
literal_buffer simp_lits;
if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) {
if (j && !j->in_region()) {
@@ -1384,11 +1388,12 @@ namespace smt {
}
DEBUG_CODE(for (literal lit : simp_lits) SASSERT(get_assignment(lit) == l_true););
if (!simp_lits.empty()) {
- j = mk_justification(unit_resolution_justification(m_region, j, simp_lits.size(), simp_lits.data()));
+ j = mk_justification(unit_resolution_justification(*this, j, simp_lits.size(), simp_lits.data()));
}
break;
}
- case CLS_TH_LEMMA:
+ case CLS_TH_LEMMA:
+ dump_lemma(num_lits, lits);
if (!simplify_aux_lemma_literals(num_lits, lits)) {
if (j && !j->in_region()) {
j->del_eh(m);
@@ -1398,7 +1403,10 @@ namespace smt {
}
// simplify_aux_lemma_literals does not delete literals assigned to false, so
// it is not necessary to create a unit_resolution_justification
- break;
+ break;
+ case CLS_LEARNED:
+ dump_lemma(num_lits, lits);
+ break;
default:
break;
}
@@ -1503,6 +1511,30 @@ namespace smt {
}}
}
+ void context::dump_axiom(unsigned n, literal const* lits) {
+ if (m_fparams.m_axioms2files) {
+ literal_buffer tmp;
+ neg_literals(n, lits, tmp);
+ SASSERT(tmp.size() == n);
+ display_lemma_as_smt_problem(tmp.size(), tmp.data(), false_literal, m_fparams.m_logic);
+ }
+ }
+
+ void context::dump_lemma(unsigned n, literal const* lits) {
+
+ if (m_fparams.m_lemmas2console) {
+ expr_ref fml(m);
+ expr_ref_vector fmls(m);
+ for (unsigned i = 0; i < n; ++i)
+ fmls.push_back(literal2expr(lits[i]));
+ fml = mk_or(fmls);
+ m_lemma_visitor.collect(fml);
+ m_lemma_visitor.display_decls(std::cout);
+ m_lemma_visitor.display_assert(std::cout, fml.get(), false);
+ }
+
+ }
+
void context::mk_clause(literal l1, literal l2, justification * j) {
literal ls[2] = { l1, l2 };
mk_clause(2, ls, j);
@@ -1518,13 +1550,7 @@ namespace smt {
TRACE("mk_th_axiom", display_literals_verbose(tout, num_lits, lits) << "\n";);
if (m.proofs_enabled()) {
- js = mk_justification(theory_axiom_justification(tid, m_region, num_lits, lits, num_params, params));
- }
- if (m_fparams.m_smtlib_dump_lemmas) {
- literal_buffer tmp;
- neg_literals(num_lits, lits, tmp);
- SASSERT(tmp.size() == num_lits);
- display_lemma_as_smt_problem(tmp.size(), tmp.data(), false_literal, m_fparams.m_logic);
+ js = mk_justification(theory_axiom_justification(tid, *this, num_lits, lits, num_params, params));
}
mk_clause(num_lits, lits, js, k);
}
diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp
index acdf03222..0124a1810 100644
--- a/src/smt/smt_justification.cpp
+++ b/src/smt/smt_justification.cpp
@@ -40,13 +40,14 @@ namespace smt {
return m_proof;
}
- unit_resolution_justification::unit_resolution_justification(region & r,
+ unit_resolution_justification::unit_resolution_justification(context& ctx,
justification * js,
unsigned num_lits,
literal const * lits):
m_antecedent(js),
m_num_literals(num_lits) {
SASSERT(!js || js->in_region());
+ auto& r = ctx.get_region();
m_literals = new (r) literal[num_lits];
memcpy(m_literals, lits, sizeof(literal) * num_lits);
TRACE("unit_resolution_justification_bug", tout << literal_vector(num_lits, lits) << "\n";);
@@ -101,6 +102,7 @@ namespace smt {
return m.mk_unit_resolution(prs.size(), prs.data());
}
+
void eq_conflict_justification::get_antecedents(conflict_resolution & cr) {
SASSERT(m_node1->get_root()->is_interpreted());
SASSERT(m_node2->get_root()->is_interpreted());
@@ -235,8 +237,9 @@ namespace smt {
return nullptr;
}
- simple_justification::simple_justification(region & r, unsigned num_lits, literal const * lits):
+ simple_justification::simple_justification(context& ctx, unsigned num_lits, literal const * lits):
m_num_literals(num_lits) {
+ region& r = ctx.get_region();
if (num_lits != 0) {
m_literals = new (r) literal[num_lits];
memcpy(m_literals, lits, sizeof(literal) * num_lits);
@@ -291,6 +294,12 @@ namespace smt {
return m.mk_th_lemma(m_th_id, fact, prs.size(), prs.data(), m_params.size(), m_params.data());
}
+ void theory_propagation_justification::log(context& ctx) {
+ if (ctx.get_fparams().m_axioms2files)
+ ctx.display_lemma_as_smt_problem(m_num_literals, m_literals, m_consequent);
+ }
+
+
proof * theory_conflict_justification::mk_proof(conflict_resolution & cr) {
ptr_buffer<proof> prs;
if (!antecedent2proof(cr, prs))
@@ -299,9 +308,16 @@ namespace smt {
return m.mk_th_lemma(m_th_id, m.mk_false(), prs.size(), prs.data(), m_params.size(), m_params.data());
}
- ext_simple_justification::ext_simple_justification(region & r, unsigned num_lits, literal const * lits, unsigned num_eqs, enode_pair const * eqs):
- simple_justification(r, num_lits, lits),
+ void theory_conflict_justification::log(context& ctx) {
+ if (ctx.get_fparams().m_axioms2files)
+ ctx.display_lemma_as_smt_problem(m_num_literals, m_literals);
+ }
+
+
+ ext_simple_justification::ext_simple_justification(context& ctx, unsigned num_lits, literal const * lits, unsigned num_eqs, enode_pair const * eqs):
+ simple_justification(ctx, num_lits, lits),
m_num_eqs(num_eqs) {
+ region& r = ctx.get_region();
m_eqs = new (r) enode_pair[num_eqs];
std::uninitialized_copy(eqs, eqs + num_eqs, m_eqs);
DEBUG_CODE({
@@ -342,6 +358,13 @@ namespace smt {
ctx.literal2expr(m_consequent, fact);
return m.mk_th_lemma(m_th_id, fact, prs.size(), prs.data(), m_params.size(), m_params.data());
}
+
+ void ext_theory_propagation_justification::log(context& ctx) {
+ if (ctx.get_fparams().m_axioms2files)
+ ctx.display_lemma_as_smt_problem(m_num_literals, m_literals, m_num_eqs, m_eqs, m_consequent);
+
+ }
+
proof * ext_theory_conflict_justification::mk_proof(conflict_resolution & cr) {
ptr_buffer<proof> prs;
@@ -351,6 +374,12 @@ namespace smt {
return m.mk_th_lemma(m_th_id, m.mk_false(), prs.size(), prs.data(), m_params.size(), m_params.data());
}
+ void ext_theory_conflict_justification::log(context& ctx) {
+ if (ctx.get_fparams().m_axioms2files)
+ ctx.display_lemma_as_smt_problem(m_num_literals, m_literals);
+ }
+
+
proof * ext_theory_eq_propagation_justification::mk_proof(conflict_resolution & cr) {
ptr_buffer<proof> prs;
if (!antecedent2proof(cr, prs))
@@ -361,6 +390,9 @@ namespace smt {
return m.mk_th_lemma(m_th_id, fact, prs.size(), prs.data(), m_params.size(), m_params.data());
}
+ void ext_theory_eq_propagation_justification::log(context& ctx) {
+ }
+
theory_lemma_justification::theory_lemma_justification(family_id fid, context & ctx, unsigned num_lits, literal const * lits,
unsigned num_params, parameter* params):
diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h
index b13d12743..161ffe839 100644
--- a/src/smt/smt_justification.h
+++ b/src/smt/smt_justification.h
@@ -95,6 +95,7 @@ namespace smt {
virtual char const * get_name() const { return "unknown"; }
virtual void display_debug_info(conflict_resolution & cr, std::ostream & out) { /* do nothing */ }
+
};
class justification_proof_wrapper : public justification {
@@ -118,7 +119,7 @@ namespace smt {
unsigned m_num_literals;
literal * m_literals;
public:
- unit_resolution_justification(region & r, justification * js, unsigned num_lits, literal const * lits);
+ unit_resolution_justification(context& ctx, justification * js, unsigned num_lits, literal const * lits);
unit_resolution_justification(justification * js, unsigned num_lits, literal const * lits);
@@ -137,6 +138,7 @@ namespace smt {
proof * mk_proof(conflict_resolution & cr) override;
char const * get_name() const override { return "unit-resolution"; }
+
};
class eq_conflict_justification : public justification {
@@ -218,7 +220,7 @@ namespace smt {
bool antecedent2proof(conflict_resolution & cr, ptr_buffer<proof> & result);
public:
- simple_justification(region & r, unsigned num_lits, literal const * lits);
+ simple_justification(context& ctx, unsigned num_lits, literal const * lits);
void get_antecedents(conflict_resolution & cr) override;
@@ -234,10 +236,10 @@ namespace smt {
vector<parameter> m_params;
public:
simple_theory_justification(
- family_id fid, region & r,
+ family_id fid, context& ctx,
unsigned num_lits, literal const * lits,
unsigned num_params, parameter* params):
- simple_justification(r, num_lits, lits),
+ simple_justification(ctx, num_lits, lits),
m_th_id(fid), m_params(num_params, params) {}
bool has_del_eh() const override { return !m_params.empty(); }
@@ -251,10 +253,10 @@ namespace smt {
class theory_axiom_justification : public simple_theory_justification {
public:
- theory_axiom_justification(family_id fid, region & r,
+ theory_axiom_justification(family_id fid, context& ctx,
unsigned num_lits, literal const * lits,
unsigned num_params = 0, parameter* params = nullptr):
- simple_theory_justification(fid, r, num_lits, lits, num_params, params) {}
+ simple_theory_justification(fid, ctx, num_lits, lits, num_params, params) {}
void get_antecedents(conflict_resolution & cr) override {}
@@ -265,10 +267,11 @@ namespace smt {
class theory_propagation_justification : public simple_theory_justification {
literal m_consequent;
+ void log(context& ctx);
public:
- theory_propagation_justification(family_id fid, region & r, unsigned num_lits, literal const * lits, literal consequent,
+ theory_propagation_justification(family_id fid, context& ctx, unsigned num_lits, literal const * lits, literal consequent,
unsigned num_params = 0, parameter* params = nullptr):
- simple_theory_justification(fid, r, num_lits, lits, num_params, params), m_consequent(consequent) {}
+ simple_theory_justification(fid, ctx, num_lits, lits, num_params, params), m_consequent(consequent) { log(ctx); }
proof * mk_proof(conflict_resolution & cr) override;
@@ -278,10 +281,11 @@ namespace smt {
};
class theory_conflict_justification : public simple_theory_justification {
+ void log(context& ctx);
public:
- theory_conflict_justification(family_id fid, region & r, unsigned num_lits, literal const * lits,
+ theory_conflict_justification(family_id fid, context& ctx, unsigned num_lits, literal const * lits,
unsigned num_params = 0, parameter* params = nullptr):
- simple_theory_justification(fid, r, num_lits, lits, num_params, params) {}
+ simple_theory_justification(fid, ctx, num_lits, lits, num_params, params) { log(ctx); }
proof * mk_proof(conflict_resolution & cr) override;
@@ -299,7 +303,7 @@ namespace smt {
bool antecedent2proof(conflict_resolution & cr, ptr_buffer<proof> & result);
public:
- ext_simple_justification(region & r, unsigned num_lits, literal const * lits,
+ ext_simple_justification(context& ctx, unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs);
void get_antecedents(conflict_resolution & cr) override;
@@ -318,10 +322,10 @@ namespace smt {
vector<parameter> m_params;
public:
- ext_theory_simple_justification(family_id fid, region & r, unsigned num_lits, literal const * lits,
+ ext_theory_simple_justification(family_id fid, context& ctx, unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,
unsigned num_params = 0, parameter* params = nullptr):
- ext_simple_justification(r, num_lits, lits, num_eqs, eqs), m_th_id(fid), m_params(num_params, params) {}
+ ext_simple_justification(ctx, num_lits, lits, num_eqs, eqs), m_th_id(fid), m_params(num_params, params) {}
bool has_del_eh() const override { return !m_params.empty(); }
@@ -332,26 +336,33 @@ namespace smt {
class ext_theory_propagation_justification : public ext_theory_simple_justification {
literal m_consequent;
+ void log(context& ctx);
public:
- ext_theory_propagation_justification(family_id fid, region & r,
+ ext_theory_propagation_justification(family_id fid, context & ctx,
unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,
literal consequent,
unsigned num_params = 0, parameter* params = nullptr):
- ext_theory_simple_justification(fid, r, num_lits, lits, num_eqs, eqs, num_params, params),
- m_consequent(consequent) {}
+ ext_theory_simple_justification(fid, ctx, num_lits, lits, num_eqs, eqs, num_params, params),
+ m_consequent(consequent) {
+ log(ctx);
+ }
proof * mk_proof(conflict_resolution & cr) override;
char const * get_name() const override { return "ext-theory-propagation"; }
+
};
class ext_theory_conflict_justification : public ext_theory_simple_justification {
+ void log(context& ctx);
public:
- ext_theory_conflict_justification(family_id fid, region & r, unsigned num_lits, literal const * lits,
+ ext_theory_conflict_justification(family_id fid, context& ctx, unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,
unsigned num_params = 0, parameter* params = nullptr):
- ext_theory_simple_justification(fid, r, num_lits, lits, num_eqs, eqs, num_params, params) {}
+ ext_theory_simple_justification(fid, ctx, num_lits, lits, num_eqs, eqs, num_params, params) {
+ log(ctx);
+ }
proof * mk_proof(conflict_resolution & cr) override;
@@ -361,19 +372,20 @@ namespace smt {
class ext_theory_eq_propagation_justification : public ext_theory_simple_justification {
enode * m_lhs;
enode * m_rhs;
+ void log(context& ctx);
public:
ext_theory_eq_propagation_justification(
- family_id fid, region & r,
+ family_id fid, context& ctx,
unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,
enode * lhs, enode * rhs,
unsigned num_params = 0, parameter* params = nullptr):
- ext_theory_simple_justification(fid, r, num_lits, lits, num_eqs, eqs, num_params, params), m_lhs(lhs), m_rhs(rhs) {}
+ ext_theory_simple_justification(fid, ctx, num_lits, lits, num_eqs, eqs, num_params, params), m_lhs(lhs), m_rhs(rhs) { log(ctx); }
ext_theory_eq_propagation_justification(
- family_id fid, region & r,
+ family_id fid, context& ctx,
enode * lhs, enode * rhs):
- ext_theory_simple_justification(fid, r, 0, nullptr, 0, nullptr, 0, nullptr), m_lhs(lhs), m_rhs(rhs) {}
+ ext_theory_simple_justification(fid, ctx, 0, nullptr, 0, nullptr, 0, nullptr), m_lhs(lhs), m_rhs(rhs) { log(ctx); }
proof * mk_proof(conflict_resolution & cr) override;
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 18a290d0a..039416f73 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -395,12 +395,14 @@ namespace smt {
m_fparams = alloc(smt_params, m_context->get_fparams());
m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3.
- m_fparams->m_arith_dump_lemmas = false;
+ m_fparams->m_axioms2files = false;
+ m_fparams->m_lemmas2console = false;
}
if (!m_aux_context) {
symbol logic;
params_ref p;
- p.set_bool("arith.dump_lemmas", false);
+ p.set_bool("solver.axioms2files", false);
+ p.set_bool("solver.lemmas2console", false);
m_aux_context = m_context->mk_fresh(&logic, m_fparams.get(), p);
}
}
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 32a9314f0..07709666b 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -544,9 +544,6 @@ namespace smt {
unsigned small_lemma_size() const { return m_params.m_arith_small_lemma_size; }
bool relax_bounds() const { return m_params.m_arith_stronger_lemmas; }
bool skip_big_coeffs() const { return m_params.m_arith_skip_rows_with_big_coeffs; }
- bool dump_lemmas() const { return m_params.m_arith_dump_lemmas; }
- void dump_lemmas(literal l, antecedents const& ante);
- void dump_lemmas(literal l, derived_bound const& ante);
bool process_atoms() const;
unsigned get_num_conflicts() const { return m_num_conflicts; }
var_kind get_var_kind(theory_var v) const { return m_data[v].kind(); }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 94bb8a802..3ad2831cb 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2982,23 +2982,7 @@ namespace smt {
}
}
- template<typename Ext>
- void theory_arith<Ext>::dump_lemmas(literal l, antecedents const& ante) {
- if (dump_lemmas()) {
- TRACE("arith", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";);
- ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().data(),
- ante.eqs().size(), ante.eqs().data(), l);
- }
- }
-
- template<typename Ext>
- void theory_arith<Ext>::dump_lemmas(literal l, derived_bound const& ante) {
- if (dump_lemmas()) {
- ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().data(),
- ante.eqs().size(), ante.eqs().data(), l);
- }
- }
template<typename Ext>
void theory_arith<Ext>::assign_bound_literal(literal l, row const & r, unsigned idx, bool is_lower, inf_numeral & delta) {
@@ -3010,7 +2994,6 @@ namespace smt {
ante.display(tout) << " --> ";
ctx.display_detailed_literal(tout, l);
tout << "\n";);
- dump_lemmas(l, ante);
if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) {
literal_vector & lits = m_tmp_literal_vector2;
@@ -3028,10 +3011,9 @@ namespace smt {
ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr);
}
else {
- region & r = ctx.get_region();
ctx.assign(l, ctx.mk_justification(
ext_theory_propagation_justification(
- get_id(), r, ante.lits().size(), ante.lits().data(),
+ get_id(), ctx, ante.lits().size(), ante.lits().data(),
ante.eqs().size(), ante.eqs().data(), l,
ante.num_params(), ante.params("assign-bounds"))));
}
@@ -3094,13 +3076,11 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::set_conflict(antecedents const& ante, antecedents& bounds, char const* proof_rule) {
set_conflict(ante.lits().size(), ante.lits().data(), ante.eqs().size(), ante.eqs().data(), bounds, proof_rule);
- dump_lemmas(false_literal, ante);
}
template<typename Ext>
void theory_arith<Ext>::set_conflict(derived_bound const& ante, antecedents& bounds, char const* proof_rule) {
set_conflict(ante.lits().size(), ante.lits().data(), ante.eqs().size(), ante.eqs().data(), bounds, proof_rule);
- dump_lemmas(false_literal, ante);
}
template<typename Ext>
@@ -3134,7 +3114,7 @@ namespace smt {
record_conflict(num_literals, lits, num_eqs, eqs, bounds.num_params(), bounds.params(proof_rule));
ctx.set_conflict(
ctx.mk_justification(
- ext_theory_conflict_justification(get_id(), ctx.get_region(), num_literals, lits, num_eqs, eqs,
+ ext_theory_conflict_justification(get_id(), ctx, num_literals, lits, num_eqs, eqs,
bounds.num_params(), bounds.params(proof_rule))));
}
diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h
index 0b8e41e20..fabdb6abd 100644
--- a/src/smt/theory_arith_eq.h
+++ b/src/smt/theory_arith_eq.h
@@ -336,7 +336,7 @@ namespace smt {
justification * js =
ctx.mk_justification(
ext_theory_eq_propagation_justification(
- get_id(), r,
+ get_id(), ctx,
lits.size(), lits.data(),
eqs.size(), eqs.data(),
_x, _y,
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index f6a713d0d..56fbd4ecf 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -487,13 +487,13 @@ namespace smt {
template<typename Ext>
class theory_arith<Ext>::gomory_cut_justification : public ext_theory_propagation_justification {
public:
- gomory_cut_justification(family_id fid, region & r,
+ gomory_cut_justification(family_id fid, context& ctx,
unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,
antecedents& bounds,
literal consequent):
- ext_theory_propagation_justification(fid, r, num_lits, lits, num_eqs, eqs, consequent,
- bounds.num_params(), bounds.params("gomory-cut")) {
+ ext_theory_propagation_justification(fid, ctx, num_lits, lits, num_eqs, eqs, consequent,
+ bounds.num_params(), bounds.params("gomory-cut")) {
}
// Remark: the assignment must be propagated back to arith
theory_id get_from_theory() const override { return null_theory_id; }
@@ -676,19 +676,16 @@ namespace smt {
l = ctx.get_literal(bound);
IF_VERBOSE(10, verbose_stream() << "cut " << bound << "\n");
ctx.mark_as_relevant(l);
- dump_lemmas(l, ante);
auto js = ctx.mk_justification(
gomory_cut_justification(
- get_id(), ctx.get_region(),
+ get_id(), ctx,
ante.lits().size(), ante.lits().data(),
ante.eqs().size(), ante.eqs().data(), ante, l));
- if (l == false_literal) {
+ if (l == false_literal)
ctx.mk_clause(0, nullptr, js, CLS_TH_LEMMA, nullptr);
- }
- else {
+ else
ctx.assign(l, js);
- }
return true;
}
@@ -760,7 +757,7 @@ namespace smt {
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(
- get_id(), ctx.get_region(), ante.lits().size(), ante.lits().data(),
+ get_id(), ctx, ante.lits().size(), ante.lits().data(),
ante.eqs().size(), ante.eqs().data(),
ante.num_params(), ante.params("gcd-test"))));
return false;
@@ -840,7 +837,7 @@ namespace smt {
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(
- get_id(), ctx.get_region(),
+ get_id(), ctx,
ante.lits().size(), ante.lits().data(), ante.eqs().size(), ante.eqs().data(),
ante.num_params(), ante.params("gcd-test"))));
return false;
@@ -858,11 +855,9 @@ namespace smt {
return true;
if (m_eager_gcd)
return true;
- typename vector<row>::const_iterator it = m_rows.begin();
- typename vector<row>::const_iterator end = m_rows.end();
- for (; it != end; ++it) {
- theory_var v = it->get_base_var();
- if (v != null_theory_var && is_int(v) && !get_value(v).is_int() && !gcd_test(*it)) {
+ for (auto const& e : m_rows) {
+ theory_var v = e.get_base_var();
+ if (v != null_theory_var && is_int(v) && !get_value(v).is_int() && !gcd_test(e)) {
if (m_params.m_arith_adaptive_gcd)
m_eager_gcd = true;
return false;
@@ -883,10 +878,8 @@ namespace smt {
for (;;) {
vars.reset();
// Collect infeasible integer variables.
- typename vector<row>::const_iterator it = m_rows.begin();
- typename vector<row>::const_iterator end = m_rows.end();
- for (; it != end; ++it) {
- theory_var v = it->get_base_var();
+ for (auto const& e : m_rows) {
+ theory_var v = e.get_base_var();
if (v != null_theory_var && is_int(v) && !get_value(v).is_int() && !is_bounded(v) && !already_processed.contains(v)) {
vars.push_back(v);
already_processed.insert(v);
@@ -1056,15 +1049,13 @@ namespace smt {
TRACE("arith_int_rows",
unsigned num = 0;
- typename vector<row>::const_iterator it = m_rows.begin();
- typename vector<row>::const_iterator end = m_rows.end();
- for (; it != end; ++it) {
- theory_var v = it->get_base_var();
+ for (auto const& e : m_rows) {
+ theory_var v = e.get_base_var();
if (v == null_theory_var)
continue;
if (is_int(v) && !get_value(v).is_int()) {
num++;
- display_simplified_row(tout, *it);
+ display_simplified_row(tout, e);
tout << "\n";
}
}
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 196f49281..556391250 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1510,7 +1510,7 @@ namespace smt {
eqs.push_back({n1, p->get_arg(0) });
eqs.push_back({n1, bv2int});
justification * js = ctx.mk_justification(
- ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), 0, nullptr, eqs.size(), eqs.data(), p, bv2int_arg));
+ ext_theory_eq_propagation_justification(get_id(), ctx, 0, nullptr, eqs.size(), eqs.data(), p, bv2int_arg));
ctx.assign_eq(p, bv2int_arg, eq_justification(js));
break;
}
diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp
index 772438986..dc41dfec5 100644
--- a/src/smt/theory_char.cpp
+++ b/src/smt/theory_char.cpp
@@ -138,7 +138,7 @@ namespace smt {
enode* n2 = ensure_enode(bits2char);
justification* j =
ctx.mk_justification(
- ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), n1, n2));
+ ext_theory_eq_propagation_justification(get_id(), ctx, n1, n2));
ctx.assign_eq(n1, n2, eq_justification(j));
}
++m_stats.m_num_blast;
@@ -267,7 +267,7 @@ namespace smt {
enode* n2 = ensure_enode(sum_bits);
justification* j =
ctx.mk_justification(
- ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), n1, n2));
+ ext_theory_eq_propagation_justification(get_id(), ctx, n1, n2));
ctx.assign_eq(n1, n2, eq_justification(j));
}
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index febd2763c..d1216c171 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -31,8 +31,8 @@ namespace smt {
class dt_eq_justification : public ext_theory_eq_propagation_justification {
public:
- dt_eq_justification(family_id fid, region & r, literal antecedent, enode * lhs, enode * rhs):
- ext_theory_eq_propagation_justification(fid, r, 1, &antecedent, 0, nullptr, lhs, rhs) {
+ dt_eq_justification(family_id fid, context& ctx, literal antecedent, enode * lhs, enode * rhs):
+ ext_theory_eq_propagation_justification(fid, ctx, 1, &antecedent, 0, nullptr, lhs, rhs) {
}
// Remark: the assignment must be propagated back to the datatype theory.
theory_id get_from_theory() const override { return null_theory_id; }
@@ -122,9 +122,8 @@ namespace smt {
}
else {
SASSERT(ctx.get_assignment(antecedent) == l_true);
- region & r = ctx.get_region();
enode * _rhs = ctx.get_enode(rhs);
- justification * js = ctx.mk_justification(dt_eq_justification(get_id(), r, antecedent, lhs, _rhs));
+ justification * js = ctx.mk_justification(dt_eq_justification(get_id(), ctx, antecedent, lhs, _rhs));
TRACE("datatype", tout << "assigning... #" << lhs->get_owner_id() << " #" << _rhs->get_owner_id() << "\n";
tout << "v" << lhs->get_th_var(get_id()) << " v" << _rhs->get_th_var(get_id()) << "\n";);
TRACE("datatype_detail", display(tout););
@@ -209,9 +208,8 @@ namespace smt {
l.neg();
SASSERT(ctx.get_assignment(l) == l_true);
enode_pair p(c, r->get_arg(0));
- region & reg = ctx.get_region();
clear_mark();
- ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, 1, &l, 1, &p)));
+ ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), ctx, 1, &l, 1, &p)));
}
/**
@@ -732,9 +730,8 @@ namespace smt {
if (res) {
// m_used_eqs should contain conflict
- region & r = ctx.get_region();
clear_mark();
- ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.data())));
+ ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), ctx, 0, nullptr, m_used_eqs.size(), m_used_eqs.data())));
}
return res;
}
@@ -859,10 +856,9 @@ namespace smt {
var_data * d2 = m_var_data[v2];
if (d2->m_constructor != nullptr) {
if (d1->m_constructor != nullptr && d1->m_constructor->get_decl() != d2->m_constructor->get_decl()) {
- region & r = ctx.get_region();
enode_pair p(d1->m_constructor, d2->m_constructor);
SASSERT(d1->m_constructor->get_root() == d2->m_constructor->get_root());
- ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, 1, &p)));
+ ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), ctx, 0, nullptr, 1, &p)));
}
if (d1->m_constructor == nullptr) {
m_trail_stack.push(set_ptr_trail<enode>(d1->m_constructor));
@@ -972,14 +968,13 @@ namespace smt {
if (num_unassigned == 0) {
// conflict
SASSERT(!lits.empty());
- region & reg = ctx.get_region();
TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_expr(), m) << "\n";
for (literal l : lits)
ctx.display_detailed_literal(tout, l) << "\n";
for (auto const& p : eqs)
tout << enode_eq_pp(p, ctx);
);
- ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, lits.size(), lits.data(), eqs.size(), eqs.data())));
+ ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data())));
}
else if (num_unassigned == 1) {
// propagate remaining recognizer
@@ -997,9 +992,8 @@ namespace smt {
consequent = literal(ctx.enode2bool_var(r));
}
ctx.mark_as_relevant(consequent);
- region & reg = ctx.get_region();
ctx.assign(consequent,
- ctx.mk_justification(ext_theory_propagation_justification(get_id(), reg, lits.size(), lits.data(),
+ ctx.mk_justification(ext_theory_propagation_justification(get_id(), ctx, lits.size(), lits.data(),
eqs.size(), eqs.data(), consequent)));
}
else {
diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h
index 8ab091a27..0a2987f8d 100644
--- a/src/smt/theory_dense_diff_logic.h
+++ b/src/smt/theory_dense_diff_logic.h
@@ -238,7 +238,6 @@ namespace smt {
void flush_eh() override;
void reset_eh() override;
- bool dump_lemmas() const { return m_params.m_arith_dump_lemmas; }
void display(std::ostream & out) const override;
virtual void display_atom(std::ostream & out, atom * a) const;
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index b5abc7a2a..46d2b0119 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -539,7 +539,7 @@ namespace smt {
literal_vector & antecedents = m_tmp_literals;
antecedents.reset();
get_antecedents(source, target, antecedents);
- ctx.assign(l, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), antecedents.size(), antecedents.data(), l)));
+ ctx.assign(l, ctx.mk_justification(theory_propagation_justification(get_id(), ctx, antecedents.size(), antecedents.data(), l)));
}
template<typename Ext>
@@ -592,11 +592,7 @@ namespace smt {
if (l != null_literal)
antecedents.push_back(l);
region & r = ctx.get_region();
- ctx.set_conflict(ctx.mk_justification(theory_conflict_justification(get_id(), r, antecedents.size(), antecedents.data())));
-
- if (dump_lemmas()) {
- ctx.display_lemma_as_smt_problem(antecedents.size(), antecedents.data(), false_literal);
- }
+ ctx.set_conflict(ctx.mk_justification(theory_conflict_justification(get_id(), ctx, antecedents.size(), antecedents.data())));
return;
}
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 99e70bd74..a613c8012 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -350,8 +350,6 @@ namespace smt {
bool propagate_eqs() const { return m_params.m_arith_propagate_eqs; }
- bool dump_lemmas() const { return m_params.m_arith_dump_lemmas; }
-
theory_var expand(bool pos, theory_var v, rational & k);
void new_eq_or_diseq(bool is_eq, theory_var v1, theory_var v2, justification& eq_just);
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 80fbe4022..807eb6cb6 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -665,10 +665,6 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
params.size(), params.data());
}
ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr);
- if (dump_lemmas()) {
- symbol logic(m_lia_or_lra == is_lia ? "QF_LIA" : "QF_LRA");
- ctx.display_lemma_as_smt_problem(lits.size(), lits.data(), false_literal, logic);
- }
#if 0
TRACE("arith",
@@ -707,11 +703,6 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
for (literal lit : lits) ctx.display_literal_info(tout, lit);
tout << "\n";);
- if (dump_lemmas()) {
- symbol logic(m_lia_or_lra == is_lia ? "QF_LIA" : "QF_LRA");
- ctx.display_lemma_as_smt_problem(lits.size(), lits.data(), false_literal, logic);
- }
-
vector<parameter> params;
if (m.proofs_enabled()) {
params.push_back(parameter(symbol("farkas")));
@@ -723,7 +714,7 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(
- get_id(), ctx.get_region(),
+ get_id(), ctx,
lits.size(), lits.data(), 0, nullptr, params.size(), params.data())));
}
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2db7f2332..b8001174e 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2331,7 +2331,6 @@ public:
literal_vector m_core2;
void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& params) {
- dump_assign(lit, core, eqs);
if (core.size() < small_lemma_size() && eqs.empty()) {
m_core2.reset();
for (auto const& c : core) {
@@ -2349,7 +2348,7 @@ public:
ctx().assign(
lit, ctx().mk_justification(
ext_theory_propagation_justification(
- get_id(), ctx().get_region(), core.size(), core.data(),
+ get_id(), ctx(), core.size(), core.data(),
eqs.size(), eqs.data(), lit, params.size(), params.data())));
}
}
@@ -2942,8 +2941,6 @@ public:
}
- bool dump_lemmas() const { return params().m_arith_dump_lemmas; }
-
bool propagate_eqs() const { return params().m_arith_propagate_eqs && m_num_conflicts < params().m_arith_propagation_threshold; }
bound_prop_mode propagation_mode() const { return m_num_conflicts < params().m_arith_propagation_threshold ? params().m_arith_bound_prop : bound_prop_mode::BP_NONE; }
@@ -3079,7 +3076,7 @@ public:
justification* js =
ctx().mk_justification(
ext_theory_eq_propagation_justification(
- get_id(), ctx().get_region(), m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), x, y));
+ get_id(), ctx(), m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), x, y));
TRACE("arith",
for (auto c : m_core)
@@ -3203,12 +3200,11 @@ public:
set_evidence(ev.ci(), m_core, m_eqs);
// SASSERT(validate_conflict(m_core, m_eqs));
- dump_conflict(m_core, m_eqs);
if (is_conflict) {
ctx().set_conflict(
ctx().mk_justification(
ext_theory_conflict_justification(
- get_id(), ctx().get_region(),
+ get_id(), ctx(),
m_core.size(), m_core.data(),
m_eqs.size(), m_eqs.data(), m_params.size(), m_params.data())));
}
@@ -3414,11 +3410,6 @@ public:
}
};
- void dump_conflict(literal_vector const& core, svector<enode_pair> const& eqs) {
- if (dump_lemmas()) {
- ctx().display_lemma_as_smt_problem(core.size(), core.data(), eqs.size(), eqs.data(), false_literal);
- }
- }
bool validate_conflict(literal_vector const& core, svector<enode_pair> const& eqs) {
if (params().m_arith_mode != arith_solver_id::AS_NEW_ARITH) return true;
@@ -3432,13 +3423,6 @@ public:
return result;
}
- void dump_assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs) {
- if (dump_lemmas()) {
- unsigned id = ctx().display_lemma_as_smt_problem(core.size(), core.data(), eqs.size(), eqs.data(), lit);
- (void)id;
- }
- }
-
bool validate_assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs) {
if (params().m_arith_mode != arith_solver_id::AS_NEW_ARITH) return true;
scoped_arith_mode _sa(ctx().get_fparams());
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 8809030e3..db076ef8c 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1486,9 +1486,9 @@ namespace smt {
class theory_pb::pb_justification : public theory_propagation_justification {
ineq& m_ineq;
public:
- pb_justification(ineq& c, family_id fid, region & r,
+ pb_justification(ineq& c, family_id fid, context& ctx,
unsigned num_lits, literal const * lits, literal consequent):
- theory_propagation_justification(fid, r, num_lits, lits, consequent),
+ theory_propagation_justification(fid, ctx, num_lits, lits, consequent),
m_ineq(c)
{}
ineq& get_ineq() { return m_ineq; }
@@ -1504,7 +1504,7 @@ namespace smt {
SASSERT(validate_antecedents(lits));
ctx.assign(l, ctx.mk_justification(
pb_justification(
- c, get_id(), ctx.get_region(), lits.size(), lits.data(), l)));
+ c, get_id(), ctx, lits.size(), lits.data(), l)));
}
@@ -2008,7 +2008,7 @@ namespace smt {
SASSERT(validate_antecedents(m_antecedents));
TRACE("pb", tout << "assign " << m_antecedents << " ==> " << alit << "\n";);
- ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.data(), alit, 0, nullptr)));
+ ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx, m_antecedents.size(), m_antecedents.data(), alit, 0, nullptr)));
DEBUG_CODE(
m_antecedents.push_back(~alit);
@@ -2029,7 +2029,7 @@ namespace smt {
literal lits[2] = { l1, l2 };
justification* js = nullptr;
if (proofs_enabled()) {
- js = ctx.mk_justification(theory_axiom_justification(get_id(), ctx.get_region(), 2, lits));
+ js = ctx.mk_justification(theory_axiom_justification(get_id(), ctx, 2, lits));
}
return js;
}
@@ -2037,7 +2037,7 @@ namespace smt {
justification* theory_pb::justify(literal_vector const& lits) {
justification* js = nullptr;
if (proofs_enabled()) {
- js = ctx.mk_justification(theory_axiom_justification(get_id(), ctx.get_region(), lits.size(), lits.data()));
+ js = ctx.mk_justification(theory_axiom_justification(get_id(), ctx, lits.size(), lits.data()));
}
return js;
}
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index bb509e549..de6742ec8 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -783,7 +783,7 @@ bool theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
justification* js =
ctx.mk_justification(
ext_theory_propagation_justification(
- get_id(), ctx.get_region(), lits.size(), lits.data(), eqs.size(), eqs.data(), lit));
+ get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data(), lit));
m_new_propagation = true;
ctx.assign(lit, js);
@@ -804,7 +804,7 @@ void theory_seq::set_conflict(enode_pair_vector const& eqs, literal_vector const
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(
- get_id(), ctx.get_region(), lits.size(), lits.data(), eqs.size(), eqs.data(), 0, nullptr)));
+ get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data(), 0, nullptr)));
validate_conflict(eqs, lits);
}
@@ -829,7 +829,7 @@ bool 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.data(), eqs.size(), eqs.data(), n1, n2));
+ get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data(), n1, n2));
{
std::function<expr*(void)> fn = [&]() { return m.mk_eq(n1->get_expr(), n2->get_expr()); };
@@ -2954,7 +2954,7 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
justification* js =
ctx.mk_justification(
ext_theory_eq_propagation_justification(
- get_id(), ctx.get_region(), lits.size(), lits.data(), eqs.size(), eqs.data(), n1, n2));
+ get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data(), n1, n2));
m_new_propagation = true;
diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
index 837547f72..aac93d935 100644
--- a/src/smt/theory_special_relations.cpp
+++ b/src/smt/theory_special_relations.cpp
@@ -279,7 +279,7 @@ namespace smt {
enode* tcn = ensure_enode(tc_app);
if (ctx.get_assignment(tcn) != l_true) {
literal consequent = ctx.get_literal(tc_app);
- justification* j = ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), 1, &lit, consequent));
+ justification* j = ctx.mk_justification(theory_propagation_justification(get_id(), ctx, 1, &lit, consequent));
TRACE("special_relations", tout << "propagate: " << tc_app << "\n";);
ctx.assign(consequent, j);
new_assertion = true;
@@ -469,7 +469,7 @@ namespace smt {
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(
- get_id(), ctx.get_region(),
+ get_id(), ctx,
lits.size(), lits.data(), 0, nullptr, params.size(), params.data())));
}
@@ -532,7 +532,7 @@ namespace smt {
literal_vector const& lits = r.m_explanation;
TRACE("special_relations", ctx.display_literals_verbose(tout << mk_pp(x->get_expr(), m) << " = " << mk_pp(y->get_expr(), m) << "\n", lits) << "\n";);
IF_VERBOSE(20, ctx.display_literals_verbose(verbose_stream() << mk_pp(x->get_expr(), m) << " = " << mk_pp(y->get_expr(), m) << "\n", lits) << "\n";);
- eq_justification js(ctx.mk_justification(ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), lits.size(), lits.data(), 0, nullptr,
+ eq_justification js(ctx.mk_justification(ext_theory_eq_propagation_justification(get_id(), ctx, lits.size(), lits.data(), 0, nullptr,
x, y)));
ctx.assign_eq(x, y, js);
}
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index ec0acd903..b8efea851 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -315,7 +315,7 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
if (m.is_false(prop.m_conseq)) {
js = ctx.mk_justification(
ext_theory_conflict_justification(
- get_id(), ctx.get_region(), m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), 0, nullptr));
+ get_id(), ctx, m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), 0, nullptr));
ctx.set_conflict(js);
}
else {
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index b43c8a57d..d4c6d684c 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -204,12 +204,7 @@ namespace smt {
inc_conflicts();
literal_vector const& lits = m_nc_functor.get_lits();
IF_VERBOSE(20, ctx.display_literals_smt2(verbose_stream() << "conflict:\n", lits));
- TRACE("utvpi", ctx.display_literals_smt2(tout << "conflict:\n", lits););
-
- if (m_params.m_arith_dump_lemmas) {
- symbol logic(m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA");
- ctx.display_lemma_as_smt_problem(lits.size(), lits.data(), false_literal, logic);
- }
+ TRACE("utvpi", ctx.display_literals_smt2(tout << "conflict:\n", lits););
vector<parameter> params;
if (m.proofs_enabled()) {
@@ -222,7 +217,7 @@ namespace smt {
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(
- get_id(), ctx.get_region(),
+ get_id(), ctx,
lits.size(), lits.data(), 0, nullptr, params.size(), params.data())));
m_nc_functor.reset();
diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp
index d6c6793e1..c5960a7b9 100644
--- a/src/smt/theory_wmaxsat.cpp
+++ b/src/smt/theory_wmaxsat.cpp
@@ -283,7 +283,7 @@ namespace smt {
ctx.set_conflict(
ctx.mk_justification(
- ext_theory_conflict_justification(get_id(), ctx.get_region(), lits.size(), lits.data(), 0, nullptr, 0, nullptr)));
+ ext_theory_conflict_justification(get_id(), ctx, lits.size(), lits.data(), 0, nullptr, 0, nullptr)));
}
bool theory_wmaxsat::max_unassigned_is_blocked() {
@@ -328,10 +328,9 @@ namespace smt {
ctx.display_literals_verbose(tout, lits.size(), lits.data());
ctx.display_literal_verbose(tout << " --> ", lit););
- region& r = ctx.get_region();
ctx.assign(lit, ctx.mk_justification(
ext_theory_propagation_justification(
- get_id(), r, lits.size(), lits.data(), 0, nullptr, lit, 0, nullptr)));
+ get_id(), ctx, lits.size(), lits.data(), 0, nullptr, lit, 0, nullptr)));
}
diff --git a/src/solver/solver_params.pyg b/src/solver/solver_params.pyg
index 21d0ab530..768509b5b 100644
--- a/src/solver/solver_params.pyg
+++ b/src/solver/solver_params.pyg
@@ -5,5 +5,7 @@ def_module_params('solver',
params=(('smtlib2_log', SYMBOL, '', "file to save solver interaction"),
('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"),
('timeout', UINT, UINT_MAX, "timeout on the solver object; overwrites a global timeout"),
+ ('lemmas2console', BOOL, False, 'print lemmas during search'),
+ ('axioms2files', BOOL, False, 'print negated theory axioms to separate files during search'),
))