mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

add options for logging learned lemmas and theory axioms

Browse source 
- 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
This commit is contained in:
Nikolaj Bjorner 2022-08-08 11:18:56 +03:00
parent 410eed9bd5
commit 63f48f8fd4
32 changed files with 260 additions and 319 deletions
Download patch file Download diff file Expand all files Collapse all files

5
RELEASE_NOTES.md
View file

@ -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
==============

1
src/smt/.#smt_justification.h Normal file
View file

@ -0,0 +1 @@
nbjorner@DESKTOP-7DPTQP8.49008:1659539981

7
src/smt/params/smt_params.cpp
View file

@ -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);

212
src/smt/params/smt_params.h
View file

@ -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);
}

2
src/smt/params/theory_arith_params.cpp
View file

@ -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);

1
src/smt/params/theory_arith_params.h
View file

@ -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;

2
src/smt/seq_axioms.cpp
View file

@ -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;
}

7
src/smt/smt_context.cpp
View file

@ -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()));

4
src/smt/smt_context.h
View file

@ -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);

50
src/smt/smt_internalizer.cpp
View file

@ -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);
}

40
src/smt/smt_justification.cpp
View file

@ -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):

56
src/smt/smt_justification.h
View file

@ -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;

6
src/smt/smt_model_checker.cpp
View file

@ -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);
}
}

3
src/smt/theory_arith.h
View file

@ -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(); }

24
src/smt/theory_arith_core.h
View file

@ -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))));
}

2
src/smt/theory_arith_eq.h
View file

@ -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,

41
src/smt/theory_arith_int.h
View file

@ -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";
}
}

2
src/smt/theory_bv.cpp
View file

@ -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;
}

4
src/smt/theory_char.cpp
View file

@ -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));
}

22
src/smt/theory_datatype.cpp
View file

@ -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 {

1
src/smt/theory_dense_diff_logic.h
View file

@ -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;

8
src/smt/theory_dense_diff_logic_def.h
View file

@ -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;
}

2
src/smt/theory_diff_logic.h
View file

@ -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);

11
src/smt/theory_diff_logic_def.h
View file

@ -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())));
}

22
src/smt/theory_lra.cpp
View file

@ -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());

12
src/smt/theory_pb.cpp
View file

@ -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;
}

8
src/smt/theory_seq.cpp
View file

@ -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;

6
src/smt/theory_special_relations.cpp
View file

@ -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);
}

2
src/smt/theory_user_propagator.cpp
View file

@ -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 {

9
src/smt/theory_utvpi_def.h
View file

@ -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();

5
src/smt/theory_wmaxsat.cpp
View file

@ -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)));
}

2
src/solver/solver_params.pyg
View file

@ -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'),
))