mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fixing unit tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-05 12:02:08 -08:00
commit 3bf86e1a49
75 changed files with 876 additions and 874 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/dyn_ack.cpp
View file

@ -58,7 +58,7 @@ namespace smt {
\remark if negate == true, then the hypothesis is actually (not (= lhs rhs))
*/
proof * mk_hypothesis(ast_manager & m, app * eq, bool negate, expr * lhs, expr * rhs) {
SASSERT(m.is_eq(eq));
SASSERT(m.is_eq(eq) || m.is_iff(eq));
SASSERT((eq->get_arg(0) == lhs && eq->get_arg(1) == rhs) ||
(eq->get_arg(0) == rhs && eq->get_arg(1) == lhs));
app * h = negate ? m.mk_not(eq) : eq;

79
src/smt/params/params2smt_params.cpp
View file

@ -1,79 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
params2smt_params.h
Abstract:
Backward compatibility utilities for parameter setting
Author:
Leonardo de Moura (leonardo) 2011-05-19.
Revision History:
--*/
#include"smt_params.h"
#include"params.h"
/**
Update smt_params using s.
Only the most frequently used options are updated.
This function is mainly used to allow smt::context to be used in
the new strategy framework.
*/
void params2smt_params(params_ref const & s, smt_params & t) {
t.m_relevancy_lvl = s.get_uint("relevancy", t.m_relevancy_lvl);
TRACE("qi_cost", s.display(tout); tout << "\n";);
t.m_qi_cost = s.get_str("qi_cost", t.m_qi_cost.c_str());
t.m_mbqi = s.get_bool("mbqi", t.m_mbqi);
t.m_mbqi_max_iterations = s.get_uint("mbqi_max_iterations", t.m_mbqi_max_iterations);
t.m_random_seed = s.get_uint("random_seed", t.m_random_seed);
t.m_model = s.get_bool("produce_models", t.m_model);
if (s.get_bool("produce_proofs", false))
t.m_proof_mode = PGM_FINE;
t.m_qi_eager_threshold = s.get_double("qi_eager_threshold", t.m_qi_eager_threshold);
t.m_qi_lazy_threshold = s.get_double("qi_lazy_threshold", t.m_qi_lazy_threshold);
t.m_preprocess = s.get_bool("preprocess", t.m_preprocess);
t.m_hi_div0 = s.get_bool("hi_div0", t.m_hi_div0);
t.m_auto_config = s.get_bool("auto_config", t.m_auto_config);
t.m_array_simplify = s.get_bool("array_old_simplifier", t.m_array_simplify);
t.m_arith_branch_cut_ratio = s.get_uint("arith_branch_cut_ratio", t.m_arith_branch_cut_ratio);
t.m_arith_expand_eqs = s.get_bool("arith_expand_eqs", t.m_arith_expand_eqs);
if (s.get_bool("arith_greatest_error_pivot", false))
t.m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
else if (s.get_bool("arith_least_error_pivot", false))
t.m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR;
}
/**
\brief Copy parameters (from s) that affect the semantics of Z3 (e.g., HI_DIV0).
It also copies the model construction parameter. Thus, model construction
can be enabled at the command line.
*/
void smt_params2params(smt_params const & s, params_ref & t) {
if (s.m_model)
t.set_bool("produce_models", true);
if (!s.m_hi_div0)
t.set_bool("hi_div0", false);
}
/**
\brief Bridge for using params_ref with smt::context.
*/
void solver_smt_params_descrs(param_descrs & r) {
r.insert("hi_div0", CPK_BOOL, "(default: true) if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted");
r.insert("relevancy", CPK_UINT, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant");
r.insert("mbqi", CPK_BOOL, "model based quantifier instantiation (MBQI)");
r.insert("mbqi_max_iterations", CPK_UINT, "maximum number of rounds of MBQI");
r.insert("random_seed", CPK_UINT, "random seed for smt solver");
r.insert("qi_eager_threshold", CPK_DOUBLE, "threshold for eager quantifier instantiation");
r.insert("qi_lazy_threshold", CPK_DOUBLE, "threshold for lazy quantifier instantiation");
r.insert("auto_config", CPK_BOOL, "use heuristics to automatically configure smt solver");
r.insert("arith_branch_cut_ratio", CPK_UINT, "branch&bound / gomory cut ratio");
}

31
src/smt/params/params2smt_params.h
View file

@ -1,31 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
params2smt_params.h
Abstract:
Backward compatibility utilities for parameter setting
Author:
Leonardo de Moura (leonardo) 2011-05-19.
Revision History:
--*/
#ifndef _PARAMS2SMT_PARAMS_H_
#define _PARAMS2SMT_PARAMS_H_
class params_ref;
struct smt_params;
void params2smt_params(params_ref const & s, smt_params & t);
void smt_params2params(smt_params const & s, params_ref & t);
void solver_smt_params_descrs(param_descrs & r);
#endif

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

@ -1,50 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smt_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-02-20.
Revision History:
--*/
#include"smt_params.h"
#include"smt_params_helper.hpp"
void smt_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
m_auto_config = p.auto_config();
m_ematching = p.ematching();
m_phase_selection = static_cast<phase_selection>(p.phase_selection());
m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
m_restart_factor = p.restart_factor();
m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
m_delay_units = p.delay_units();
m_delay_units_threshold = p.delay_units_threshold();
m_proof_mode = _p.get_bool("produce_proofs", false)? PGM_FINE : PGM_DISABLED;
}
void smt_params::updt_params(params_ref const & p) {
preprocessor_params::updt_params(p);
qi_params::updt_params(p);
theory_arith_params::updt_params(p);
theory_bv_params::updt_params(p);
updt_local_params(p);
}
void smt_params::updt_params(context_params const & p) {
m_auto_config = p.m_auto_config;
m_soft_timeout = p.m_timeout;
m_model = p.m_model;
m_model_validate = p.m_validate_model;
m_proof_mode = p.m_proof ? PGM_FINE : PGM_DISABLED;
}

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

@ -207,7 +207,6 @@ struct smt_params : public preprocessor_params,
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;
proof_gen_mode m_proof_mode;
bool m_auto_config;
smt_params(params_ref const & p = params_ref()):
@ -277,7 +276,6 @@ struct smt_params : public preprocessor_params,
m_at_labels_cex(false),
m_check_at_labels(false),
m_dump_goal_as_smt(false),
m_proof_mode(PGM_DISABLED),
m_auto_config(true) {
updt_local_params(p);
}

3
src/smt/params/smt_params_helper.pyg
View file

@ -3,6 +3,8 @@ def_module_params(module_name='smt',
description='smt solver based on lazy smt',
export=True,
params=(('auto_config', BOOL, True, 'automatically configure solver'),
('random_seed', UINT, 0, 'random seed for the smt solver'),
('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'),
('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
('phase_selection', UINT, 4, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
@ -33,6 +35,7 @@ def_module_params(module_name='smt',
('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic'),
('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real')))

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

@ -32,6 +32,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_branch_cut_ratio = p.arith_branch_cut_ratio();
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());
}

19
src/smt/qi_queue.cpp
View file

@ -47,10 +47,21 @@ namespace smt {
void qi_queue::setup() {
TRACE("qi_cost", tout << "qi_cost: " << m_params.m_qi_cost << "\n";);
if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function))
throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str());
if (!m_parser.parse_string(m_params.m_qi_new_gen.c_str(), m_new_gen_function))
throw default_exception("invalid new-gen function %s", m_params.m_qi_new_gen.c_str());
if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) {
// it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided.
// throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str());
// using warning message instead
warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str());
// Trying again with default function
VERIFY(m_parser.parse_string("(+ weight generation)", m_cost_function));
}
if (!m_parser.parse_string(m_params.m_qi_new_gen.c_str(), m_new_gen_function)) {
// See comment above
// throw default_exception("invalid new-gen function %s", m_params.m_qi_new_gen.c_str());
warning_msg("invalid new_gen function '%s', switching to default one", m_params.m_qi_new_gen.c_str());
VERIFY(m_parser.parse_string("cost", m_new_gen_function));
}
m_eager_cost_threshold = m_params.m_qi_eager_threshold;
}

4
src/smt/smt_kernel.cpp
View file

@ -19,7 +19,7 @@ Revision History:
#include"smt_kernel.h"
#include"smt_context.h"
#include"ast_smt2_pp.h"
#include"params2smt_params.h"
#include"smt_params_helper.hpp"
namespace smt {
@ -345,7 +345,7 @@ namespace smt {
}
void kernel::collect_param_descrs(param_descrs & d) {
solver_smt_params_descrs(d);
smt_params_helper::collect_param_descrs(d);
}
context & kernel::get_context() {

15
src/smt/smt_model_checker.cpp
View file

@ -313,7 +313,7 @@ namespace smt {
TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";
tout << "model:\n"; model_pp(tout, *m_curr_model););
if (m_params.m_mbqi_trace) {
verbose_stream() << "[mbqi] started\n";
verbose_stream() << "(smt.mbqi \"started\")\n";
}
init_aux_context();
@ -325,13 +325,12 @@ namespace smt {
quantifier * q = *it;
if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
verbose_stream() << "[mbqi] checking: " << q->get_qid() << "\n";
verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
}
found_relevant = true;
if (!check(q)) {
IF_VERBOSE(5, verbose_stream() << "current model does not satisfy: " << q->get_qid() << "\n";);
if (m_params.m_mbqi_trace) {
verbose_stream() << "[mbqi] failed " << q->get_qid() << "\n";
if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
}
num_failures++;
}
@ -348,9 +347,9 @@ namespace smt {
m_curr_model->cleanup();
if (m_params.m_mbqi_trace) {
if (num_failures == 0)
verbose_stream() << "[mbqi] succeeded\n";
verbose_stream() << "(smt.mbqi :succeeded true)\n";
else
verbose_stream() << "[mbqi] num failures " << num_failures << "\n";
verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
}
return num_failures == 0;
}
@ -361,7 +360,7 @@ namespace smt {
}
void model_checker::restart_eh() {
IF_VERBOSE(100, verbose_stream() << "instantiating new instances...\n";);
IF_VERBOSE(100, verbose_stream() << "(smt.mbqi \"instantiating new instances...\")\n";);
assert_new_instances();
reset_new_instances();
}

3
src/smt/smt_quantifier.cpp
View file

@ -562,7 +562,7 @@ namespace smt {
virtual quantifier_manager::check_model_result
check_model(proto_model * m, obj_map<enode, app *> const & root2value) {
if (m_fparams->m_mbqi) {
IF_VERBOSE(10, verbose_stream() << "model based quantifier instantiation...\n";);
IF_VERBOSE(10, verbose_stream() << "(smt.mbqi)\n";);
if (m_model_checker->check(m, root2value)) {
return quantifier_manager::SAT;
}
@ -594,7 +594,6 @@ namespace smt {
final_check_status final_check_quant() {
if (use_ematching()) {
if (m_lazy_matching_idx < m_fparams->m_qi_max_lazy_multipattern_matching) {
IF_VERBOSE(100, verbose_stream() << "matching delayed multi-patterns... \n";);
m_lazy_mam->rematch();
m_context->push_trail(value_trail<context, unsigned>(m_lazy_matching_idx));
m_lazy_matching_idx++;

49
src/smt/smt_setup.cpp
View file

@ -266,8 +266,8 @@ namespace smt {
// Moreover, if model construction is enabled, then rational numbers may be needed
// to compute the actual value of epsilon even if the input does not have rational numbers.
// Example: (x < 1) and (x > 0)
if (m_params.m_proof_mode != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
if (m_manager.proofs_enabled()) {
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
if (!st.m_has_rational && !m_params.m_model && st.m_arith_k_sum < rational(INT_MAX / 8))
@ -343,8 +343,8 @@ namespace smt {
tout << "RELEVANCY: " << m_params.m_relevancy_lvl << "\n";
tout << "ARITH_EQ_BOUNDS: " << m_params.m_arith_eq_bounds << "\n";);
if (m_params.m_proof_mode != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
if (m_manager.proofs_enabled()) {
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
TRACE("setup", tout << "using dense diff logic...\n";);
@ -394,8 +394,8 @@ namespace smt {
m_params.m_lemma_gc_half = true;
m_params.m_restart_strategy = RS_GEOMETRIC;
if (m_params.m_proof_mode != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
if (m_manager.proofs_enabled()) {
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
else if (st.m_arith_k_sum < rational(INT_MAX / 8))
m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params));
@ -409,8 +409,8 @@ namespace smt {
m_params.m_restart_strategy = RS_GEOMETRIC;
m_params.m_restart_factor = 1.5;
m_params.m_restart_adaptive = false;
if (m_params.m_proof_mode != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
if (m_manager.proofs_enabled()) {
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
// else if (st.m_arith_k_sum < rational(INT_MAX / 8))
// m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params));
@ -683,21 +683,11 @@ namespace smt {
}
void setup::setup_i_arith() {
if (m_params.m_proof_mode != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
}
else {
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
}
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
}
void setup::setup_mi_arith() {
if (m_params.m_proof_mode != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
}
else {
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
void setup::setup_arith() {
@ -734,21 +724,10 @@ namespace smt {
}
break;
default:
if (m_params.m_proof_mode != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
}
// else if (m_params.m_arith_fixnum) {
// if (m_params.m_arith_int_only)
// m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params));
// else
// m_context.register_plugin(alloc(smt::theory_smi_arith, m_manager, m_params));
// }
else {
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
break;
}
}

36
src/smt/smt_solver.cpp
View file

@ -56,9 +56,13 @@ namespace smt {
virtual void init_core(ast_manager & m, symbol const & logic) {
reset();
#pragma omp critical (solver)
// We can throw exceptions when creating a smt::kernel object
// So, we should create the smt::kernel outside of the criticial section
// block. OMP does not allow exceptions to cross critical section boundaries.
smt::kernel * new_kernel = alloc(smt::kernel, m, m_params);
#pragma omp critical (solver)
{
m_context = alloc(smt::kernel, m, m_params);
m_context = new_kernel;
if (m_callback)
m_context->set_progress_callback(m_callback);
}
@ -77,59 +81,67 @@ namespace smt {
virtual void reset_core() {
if (m_context != 0) {
#pragma omp critical (solver)
#pragma omp critical (solver)
{
dealloc(m_context);
m_context = 0;
}
}
}
// An exception may be thrown when creating a smt::kernel.
// So, there is no guarantee that m_context != 0 when
// using smt_solver from the SMT 2.0 command line frontend.
void check_context() const {
if (m_context == 0)
throw default_exception("Z3 failed to create solver, check previous error messages");
}
virtual void assert_expr(expr * t) {
SASSERT(m_context);
check_context();
m_context->assert_expr(t);
}
virtual void push_core() {
SASSERT(m_context);
check_context();
m_context->push();
}
virtual void pop_core(unsigned n) {
SASSERT(m_context);
check_context();
m_context->pop(n);
}
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
SASSERT(m_context);
check_context();
TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";);
return m_context->check(num_assumptions, assumptions);
}
virtual void get_unsat_core(ptr_vector<expr> & r) {
SASSERT(m_context);
check_context();
unsigned sz = m_context->get_unsat_core_size();
for (unsigned i = 0; i < sz; i++)
r.push_back(m_context->get_unsat_core_expr(i));
}
virtual void get_model(model_ref & m) {
SASSERT(m_context);
check_context();
m_context->get_model(m);
}
virtual proof * get_proof() {
SASSERT(m_context);
check_context();
return m_context->get_proof();
}
virtual std::string reason_unknown() const {
SASSERT(m_context);
check_context();
return m_context->last_failure_as_string();
}
virtual void get_labels(svector<symbol> & r) {
SASSERT(m_context);
check_context();
buffer<symbol> tmp;
m_context->get_relevant_labels(0, tmp);
r.append(tmp.size(), tmp.c_ptr());

4
src/smt/tactic/smt_tactic.cpp
View file

@ -20,7 +20,7 @@ Notes:
#include"tactical.h"
#include"smt_kernel.h"
#include"smt_params.h"
#include"params2smt_params.h"
#include"smt_params_helper.hpp"
#include"rewriter_types.h"
class smt_tactic : public tactic {
@ -70,7 +70,7 @@ public:
virtual void collect_param_descrs(param_descrs & r) {
r.insert("candidate_models", CPK_BOOL, "(default: false) create candidate models even when quantifier or theory reasoning is incomplete.");
r.insert("fail_if_inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal.");
solver_smt_params_descrs(r);
smt_params_helper::collect_param_descrs(r);
}
virtual void set_cancel(bool f) {

1
src/smt/theory_arith.cpp
View file

@ -21,7 +21,6 @@ Revision History:
namespace smt {
template class theory_arith<mi_ext_with_proofs>;
template class theory_arith<mi_ext>;
template class theory_arith<i_ext>;
// template class theory_arith<si_ext>;

43
src/smt/theory_arith.h
View file

@ -87,8 +87,8 @@ namespace smt {
typedef vector<numeral> numeral_vector;
static const int dead_row_id = -1;
static const bool proofs_enabled = Ext::proofs_enabled;
protected:
bool proofs_enabled() const { return get_manager().proofs_enabled(); }
struct linear_monomial {
numeral m_coeff;
@ -233,8 +233,8 @@ namespace smt {
void reset();
literal_vector& lits() { return m_lits; }
eq_vector& eqs() { return m_eqs; }
void push_lit(literal l, numeral const& r);
void push_eq(enode_pair const& p, numeral const& r);
void push_lit(literal l, numeral const& r, bool proofs_enabled);
void push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled);
unsigned num_params() const { return empty()?0:m_eq_coeffs.size() + m_lit_coeffs.size() + 1; }
numeral const* lit_coeffs() const { return m_lit_coeffs.c_ptr(); }
numeral const* eq_coeffs() const { return m_eq_coeffs.c_ptr(); }
@ -284,8 +284,8 @@ namespace smt {
bool is_true() const { return m_is_true; }
void assign_eh(bool is_true, inf_numeral const & epsilon);
virtual bool has_justification() const { return true; }
virtual void push_justification(antecedents& a, numeral const& coeff) {
a.push_lit(literal(get_bool_var(), !m_is_true), coeff);
virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
a.push_lit(literal(get_bool_var(), !m_is_true), coeff, proofs_enabled);
}
};
@ -301,9 +301,9 @@ namespace smt {
}
virtual ~eq_bound() {}
virtual bool has_justification() const { return true; }
virtual void push_justification(antecedents& a, numeral const& coeff) {
virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
SASSERT(m_lhs->get_root() == m_rhs->get_root());
a.push_eq(enode_pair(m_lhs, m_rhs), coeff);
a.push_eq(enode_pair(m_lhs, m_rhs), coeff, proofs_enabled);
}
};
@ -316,7 +316,7 @@ namespace smt {
derived_bound(theory_var v, inf_numeral const & val, bound_kind k):bound(v, val, k, false) {}
virtual ~derived_bound() {}
virtual bool has_justification() const { return true; }
virtual void push_justification(antecedents& a, numeral const& coeff);
virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled);
virtual void push_lit(literal l, numeral const&) { m_lits.push_back(l); }
virtual void push_eq(enode_pair const& p, numeral const&) { m_eqs.push_back(p); }
};
@ -329,7 +329,7 @@ namespace smt {
justified_derived_bound(theory_var v, inf_numeral const & val, bound_kind k):derived_bound(v, val, k) {}
virtual ~justified_derived_bound() {}
virtual bool has_justification() const { return true; }
virtual void push_justification(antecedents& a, numeral const& coeff);
virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled);
virtual void push_lit(literal l, numeral const& coeff);
virtual void push_eq(enode_pair const& p, numeral const& coeff);
@ -1053,30 +1053,9 @@ namespace smt {
static inf_numeral mk_inf_numeral(numeral const & n, numeral const & r) {
return inf_numeral(n, r);
}
static const bool proofs_enabled = false;
mi_ext() : m_int_epsilon(rational(1)), m_real_epsilon(rational(0), true) {}
};
class mi_ext_with_proofs {
public:
typedef rational numeral;
typedef inf_rational inf_numeral;
inf_numeral m_int_epsilon;
inf_numeral m_real_epsilon;
numeral fractional_part(inf_numeral const& n) {
SASSERT(n.is_rational());
return n.get_rational() - floor(n);
}
static numeral fractional_part(numeral const & n) {
return n - floor(n);
}
static inf_numeral mk_inf_numeral(numeral const & n, numeral const & r) {
return inf_numeral(n, r);
}
static const bool proofs_enabled = true;
mi_ext_with_proofs() : m_int_epsilon(rational(1)), m_real_epsilon(rational(0), true) {}
};
class i_ext {
public:
typedef rational numeral;
@ -1090,7 +1069,6 @@ namespace smt {
UNREACHABLE();
return inf_numeral(n);
}
static const bool proofs_enabled = false;
i_ext() : m_int_epsilon(1), m_real_epsilon(1) {}
};
@ -1107,7 +1085,6 @@ namespace smt {
UNREACHABLE();
return inf_numeral(n);
}
static const bool proofs_enabled = false;
si_ext(): m_int_epsilon(s_integer(1)), m_real_epsilon(s_integer(1)) {}
};
@ -1128,12 +1105,10 @@ namespace smt {
static inf_numeral mk_inf_numeral(numeral const& n, numeral const& i) {
return inf_numeral(n, i);
}
static const bool proofs_enabled = false;
smi_ext() : m_int_epsilon(s_integer(1)), m_real_epsilon(s_integer(0), true) {}
};
typedef theory_arith<mi_ext> theory_mi_arith;
typedef theory_arith<mi_ext_with_proofs> theory_mi_arith_w_proofs;
typedef theory_arith<i_ext> theory_i_arith;
// typedef theory_arith<si_ext> theory_si_arith;
// typedef theory_arith<smi_ext> theory_smi_arith;

22
src/smt/theory_arith_aux.h
View file

@ -336,7 +336,7 @@ namespace smt {
}
template<typename Ext>
void theory_arith<Ext>::antecedents::push_lit(literal l, numeral const& r) {
void theory_arith<Ext>::antecedents::push_lit(literal l, numeral const& r, bool proofs_enabled) {
m_lits.push_back(l);
if (proofs_enabled) {
m_lit_coeffs.push_back(r);
@ -344,7 +344,7 @@ namespace smt {
}
template<typename Ext>
void theory_arith<Ext>::antecedents::push_eq(enode_pair const& p, numeral const& r) {
void theory_arith<Ext>::antecedents::push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled) {
m_eqs.push_back(p);
if (proofs_enabled) {
m_eq_coeffs.push_back(r);
@ -690,14 +690,14 @@ namespace smt {
// -----------------------------------
template<typename Ext>
void theory_arith<Ext>::derived_bound::push_justification(antecedents& a, numeral const& coeff) {
void theory_arith<Ext>::derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
if (proofs_enabled) {
for (unsigned i = 0; i < m_lits.size(); ++i) {
a.push_lit(m_lits[i], coeff);
a.push_lit(m_lits[i], coeff, proofs_enabled);
}
for (unsigned i = 0; i < m_eqs.size(); ++i) {
a.push_eq(m_eqs[i], coeff);
a.push_eq(m_eqs[i], coeff, proofs_enabled);
}
}
else {
@ -708,12 +708,12 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::justified_derived_bound::push_justification(antecedents& a, numeral const& coeff) {
void theory_arith<Ext>::justified_derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
for (unsigned i = 0; i < this->m_lits.size(); ++i) {
a.push_lit(this->m_lits[i], coeff*m_lit_coeffs[i]);
a.push_lit(this->m_lits[i], coeff*m_lit_coeffs[i], proofs_enabled);
}
for (unsigned i = 0; i < this->m_eqs.size(); ++i) {
a.push_eq(this->m_eqs[i], coeff*m_eq_coeffs[i]);
a.push_eq(this->m_eqs[i], coeff*m_eq_coeffs[i], proofs_enabled);
}
}
@ -755,7 +755,7 @@ namespace smt {
literal l = ante.lits()[i];
if (lits.contains(l.index()))
continue;
if (proofs_enabled) {
if (proofs_enabled()) {
new_bound.push_lit(l, ante.lit_coeffs()[i]);
}
else {
@ -768,7 +768,7 @@ namespace smt {
enode_pair const & p = ante.eqs()[i];
if (eqs.contains(p))
continue;
if (proofs_enabled) {
if (proofs_enabled()) {
new_bound.push_eq(p, ante.eq_coeffs()[i]);
}
else {
@ -796,7 +796,7 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::mk_bound_from_row(theory_var v, inf_numeral const & k, bound_kind kind, row const & r) {
inf_numeral k_norm = normalize_bound(v, k, kind);
derived_bound * new_bound = proofs_enabled?alloc(justified_derived_bound, v, k_norm, kind):alloc(derived_bound, v, k_norm, kind);
derived_bound * new_bound = proofs_enabled()?alloc(justified_derived_bound, v, k_norm, kind):alloc(derived_bound, v, k_norm, kind);
m_bounds_to_delete.push_back(new_bound);
m_asserted_bounds.push_back(new_bound);
m_tmp_lit_set.reset();

8
src/smt/theory_arith_core.h
View file

@ -2456,7 +2456,7 @@ namespace smt {
delta -= coeff*(k_2 - k_1);
}
TRACE("propagate_bounds", tout << "delta (after replace): " << delta << "\n";);
new_atom->push_justification(ante, coeff);
new_atom->push_justification(ante, coeff, proofs_enabled());
SASSERT(delta >= inf_numeral::zero());
}
}
@ -2569,7 +2569,7 @@ namespace smt {
for (; it != end; ++it)
lits.push_back(~(*it));
justification * js = 0;
if (proofs_enabled) {
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr(),
ante.num_params(), ante.params("assign-bounds"));
}
@ -2656,13 +2656,13 @@ namespace smt {
for (unsigned i = 0; i < num_literals; i++) {
ctx.display_detailed_literal(tout, lits[i]);
tout << " ";
if (proofs_enabled) {
if (proofs_enabled()) {
tout << "bound: " << bounds.lit_coeffs()[i] << "\n";
}
}
for (unsigned i = 0; i < num_eqs; i++) {
tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " ";
if (proofs_enabled) {
if (proofs_enabled()) {
tout << "bound: " << bounds.eq_coeffs()[i] << "\n";
}
}