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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-12-21 17:10:41 -08:00
parent b0b6394c6c 3104291b80
commit 95db37d105
14 changed files with 1068 additions and 1160 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -43,6 +43,7 @@ bld_dbg/*
bld_rel/*
bld_dbg_x64/*
bld_rel_x64/*
.vscode
# Auto generated files.
config.log
config.status

2
CMakeLists.txt
View file

@ -34,7 +34,7 @@ endif()
################################################################################
set(Z3_VERSION_MAJOR 4)
set(Z3_VERSION_MINOR 8)
set(Z3_VERSION_PATCH 4)
set(Z3_VERSION_PATCH 5)
set(Z3_VERSION_TWEAK 0)
set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified

10
RELEASE_NOTES
View file

@ -1,5 +1,15 @@
RELEASE NOTES
Version 4.8.4
=============
- Notes
- fixes bugs
- a substantial update to how the seq theory solver handles regular
expressions. Other performance improvements to the seq solver.
- Managed .NET DLLs include dotnet standard 1.4 on supported platforms.
- Windows Managed DLLs are strong signed in the released binaries.
Version 4.8.3
=============
- New features

2
scripts/mk_project.py
View file

@ -8,7 +8,7 @@
from mk_util import *
def init_version():
set_version(4, 8, 4, 0)
set_version(4, 8, 5, 0)
# Z3 Project definition
def init_project_def():

8
src/qe/qe_lite.cpp
View file

@ -2370,6 +2370,7 @@ void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_re
(*m_impl)(index_set, index_of_bound, fmls);
}
namespace {
class qe_lite_tactic : public tactic {
struct imp {
@ -2494,7 +2495,6 @@ public:
(*m_imp)(in, result);
}
void collect_statistics(statistics & st) const override {
// m_imp->collect_statistics(st);
}
@ -2503,14 +2503,14 @@ public:
// m_imp->reset_statistics();
}
void cleanup() override {
ast_manager & m = m_imp->m;
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
m_imp->~imp();
m_imp = new (m_imp) imp(m, m_params);
}
};
}
tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
return alloc(qe_lite_tactic, m, p);

5
src/qe/qe_lite.h
View file

@ -18,8 +18,7 @@ Revision History:
--*/
#ifndef QE_LITE_H_
#define QE_LITE_H_
#pragma once
#include "ast/ast.h"
#include "util/uint_set.h"
@ -67,5 +66,3 @@ tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref())
/*
ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)")
*/
#endif

64
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -27,28 +27,8 @@ Notes:
#include "tactic/generic_model_converter.h"
#include "ast/ast_smt2_pp.h"
namespace {
class bv_size_reduction_tactic : public tactic {
struct imp;
imp * m_imp;
public:
bv_size_reduction_tactic(ast_manager & m);
tactic * translate(ast_manager & m) override {
return alloc(bv_size_reduction_tactic, m);
}
~bv_size_reduction_tactic() override;
void operator()(goal_ref const & g, goal_ref_buffer & result) override;
void cleanup() override;
};
tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(bv_size_reduction_tactic, m));
}
struct bv_size_reduction_tactic::imp {
typedef rational numeral;
typedef generic_model_converter bv_size_reduction_mc;
@ -63,12 +43,29 @@ struct bv_size_reduction_tactic::imp {
scoped_ptr<expr_replacer> m_replacer;
bool m_produce_models;
imp(ast_manager & _m):
m(_m),
public:
bv_size_reduction_tactic(ast_manager & m) :
m(m),
m_util(m),
m_replacer(mk_default_expr_replacer(m)) {
}
tactic * translate(ast_manager & m) override {
return alloc(bv_size_reduction_tactic, m);
}
void operator()(goal_ref const & g, goal_ref_buffer & result) override;
void cleanup() override {
m_signed_lowers.reset();
m_signed_uppers.reset();
m_unsigned_lowers.reset();
m_unsigned_uppers.reset();
m_mc = nullptr;
m_fmc = nullptr;
m_replacer->reset();
}
void update_signed_lower(app * v, numeral const & k) {
// k <= v
obj_map<app, numeral>::obj_map_entry * entry = m_signed_lowers.insert_if_not_there2(v, k);
@ -178,7 +175,7 @@ struct bv_size_reduction_tactic::imp {
throw tactic_exception(m.limit().get_cancel_msg());
}
void operator()(goal & g, model_converter_ref & mc) {
void run(goal & g, model_converter_ref & mc) {
if (g.inconsistent())
return;
TRACE("before_bv_size_reduction", g.display(tout););
@ -373,14 +370,6 @@ struct bv_size_reduction_tactic::imp {
};
bv_size_reduction_tactic::bv_size_reduction_tactic(ast_manager & m) {
m_imp = alloc(imp, m);
}
bv_size_reduction_tactic::~bv_size_reduction_tactic() {
dealloc(m_imp);
}
void bv_size_reduction_tactic::operator()(goal_ref const & g,
goal_ref_buffer & result) {
SASSERT(g->is_well_sorted());
@ -388,17 +377,14 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g,
fail_if_unsat_core_generation("bv-size-reduction", g);
result.reset();
model_converter_ref mc;
m_imp->operator()(*(g.get()), mc);
run(*(g.get()), mc);
g->inc_depth();
g->add(mc.get());
result.push_back(g.get());
SASSERT(g->is_well_sorted());
}
void bv_size_reduction_tactic::cleanup() {
ast_manager & m = m_imp->m;
m_imp->~imp();
new (m_imp) imp(m);
}
tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(bv_size_reduction_tactic, m));
}

5
src/tactic/bv/bv_size_reduction_tactic.h
View file

@ -21,8 +21,7 @@ Author:
Notes:
--*/
#ifndef BV_SIZE_REDUCTION_TACTIC_H_
#define BV_SIZE_REDUCTION_TACTIC_H_
#pragma once
#include "util/params.h"
class ast_manager;
@ -32,5 +31,3 @@ tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p = par
/*
ADD_TACTIC("reduce-bv-size", "try to reduce bit-vector sizes using inequalities.", "mk_bv_size_reduction_tactic(m, p)")
*/
#endif

108
src/tactic/bv/elim_small_bv_tactic.cpp
View file

@ -28,6 +28,7 @@ Revision History:
#include "tactic/bv/elim_small_bv_tactic.h"
namespace {
class elim_small_bv_tactic : public tactic {
struct rw_cfg : public default_rewriter_cfg {
@ -183,20 +184,6 @@ class elim_small_bv_tactic : public tactic {
return true;
}
bool pre_visit(expr * t) {
TRACE("elim_small_bv_pre", tout << "pre_visit: " << mk_ismt2_pp(t, m) << std::endl;);
if (is_quantifier(t)) {
quantifier * q = to_quantifier(t);
TRACE("elim_small_bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m) << std::endl;);
sort_ref_vector new_bindings(m);
for (unsigned i = 0; i < q->get_num_decls(); i++)
new_bindings.push_back(q->get_decl_sort(i));
SASSERT(new_bindings.size() == q->get_num_decls());
m_bindings.append(new_bindings);
}
return true;
}
void updt_params(params_ref const & p) {
m_params = p;
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
@ -214,69 +201,24 @@ class elim_small_bv_tactic : public tactic {
}
};
struct imp {
ast_manager & m;
rw m_rw;
ast_manager & m;
rw m_rw;
params_ref m_params;
imp(ast_manager & _m, params_ref const & p) :
m(_m),
m_rw(m, p) {
}
void updt_params(params_ref const & p) {
m_rw.cfg().updt_params(p);
}
void operator()(goal_ref const & g, goal_ref_buffer & result) {
SASSERT(g->is_well_sorted());
tactic_report report("elim-small-bv", *g);
bool produce_proofs = g->proofs_enabled();
fail_if_proof_generation("elim-small-bv", g);
fail_if_unsat_core_generation("elim-small-bv", g);
m_rw.cfg().m_produce_models = g->models_enabled();
m_rw.m_cfg.m_goal = g.get();
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned size = g->size();
for (unsigned idx = 0; idx < size; idx++) {
expr * curr = g->form(idx);
m_rw(curr, new_curr, new_pr);
if (produce_proofs) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
}
g->add(m_rw.m_cfg.m_mc.get());
report_tactic_progress(":elim-small-bv-num-eliminated", m_rw.m_cfg.m_num_eliminated);
g->inc_depth();
result.push_back(g.get());
TRACE("elim-small-bv", g->display(tout););
SASSERT(g->is_well_sorted());
}
};
imp * m_imp;
params_ref m_params;
public:
elim_small_bv_tactic(ast_manager & m, params_ref const & p) :
m(m),
m_rw(m, p),
m_params(p) {
m_imp = alloc(imp, m, p);
}
tactic * translate(ast_manager & m) override {
return alloc(elim_small_bv_tactic, m, m_params);
}
~elim_small_bv_tactic() override {
dealloc(m_imp);
}
void updt_params(params_ref const & p) override {
m_params = p;
m_imp->m_rw.cfg().updt_params(p);
m_rw.cfg().updt_params(p);
}
void collect_param_descrs(param_descrs & r) override {
@ -285,18 +227,44 @@ public:
r.insert("max_bits", CPK_UINT, "(default: 4) maximum bit-vector size of quantified bit-vectors to be eliminated.");
}
void operator()(goal_ref const & in,
void operator()(goal_ref const & g,
goal_ref_buffer & result) override {
(*m_imp)(in, result);
SASSERT(g->is_well_sorted());
tactic_report report("elim-small-bv", *g);
bool produce_proofs = g->proofs_enabled();
fail_if_proof_generation("elim-small-bv", g);
fail_if_unsat_core_generation("elim-small-bv", g);
m_rw.cfg().m_produce_models = g->models_enabled();
m_rw.m_cfg.m_goal = g.get();
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned size = g->size();
for (unsigned idx = 0; idx < size; idx++) {
expr * curr = g->form(idx);
m_rw(curr, new_curr, new_pr);
if (produce_proofs) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
}
g->add(m_rw.m_cfg.m_mc.get());
report_tactic_progress(":elim-small-bv-num-eliminated", m_rw.m_cfg.m_num_eliminated);
g->inc_depth();
result.push_back(g.get());
TRACE("elim-small-bv", g->display(tout););
SASSERT(g->is_well_sorted());
}
void cleanup() override {
ast_manager & m = m_imp->m;
m_imp->~imp();
m_imp = new (m_imp) imp(m, m_params);
m_rw.~rw();
new (&m_rw) rw(m, m_params);
}
};
}
tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(elim_small_bv_tactic, m, p));

5
src/tactic/bv/elim_small_bv_tactic.h
View file

@ -16,8 +16,7 @@ Author:
Revision History:
--*/
#ifndef ELIM_SMALL_BV_H_
#define ELIM_SMALL_BV_H_
#pragma once
#include "util/params.h"
class ast_manager;
@ -28,5 +27,3 @@ tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p = params_
/*
ADD_TACTIC("elim-small-bv", "eliminate small, quantified bit-vectors by expansion.", "mk_elim_small_bv_tactic(m, p)")
*/
#endif

1633
src/tactic/core/elim_uncnstr_tactic.cpp
View file

File diff suppressed because it is too large Load diff

5
src/tactic/core/elim_uncnstr_tactic.h
View file

@ -16,8 +16,7 @@ Author:
Notes:
--*/
#ifndef ELIM_UNCNSTR_TACTIC_H_
#define ELIM_UNCNSTR_TACTIC_H_
#pragma once
#include "util/params.h"
@ -29,5 +28,3 @@ tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p = params_r
/*
ADD_TACTIC("elim-uncnstr", "eliminate application containing unconstrained variables.", "mk_elim_uncnstr_tactic(m, p)")
*/
#endif

375
src/tactic/core/propagate_values_tactic.cpp
View file

@ -25,224 +25,206 @@ Revision History:
#include "tactic/goal_shared_occs.h"
#include "ast/pb_decl_plugin.h"
namespace {
class propagate_values_tactic : public tactic {
struct imp {
ast_manager & m;
th_rewriter m_r;
scoped_ptr<expr_substitution> m_subst;
goal * m_goal;
goal_shared_occs m_occs;
unsigned m_idx;
unsigned m_max_rounds;
bool m_modified;
imp(ast_manager & m, params_ref const & p):
m(m),
m_r(m, p),
m_goal(nullptr),
m_occs(m, true /* track atoms */) {
updt_params_core(p);
}
ast_manager & m;
th_rewriter m_r;
scoped_ptr<expr_substitution> m_subst;
goal * m_goal;
goal_shared_occs m_occs;
unsigned m_idx;
unsigned m_max_rounds;
bool m_modified;
params_ref m_params;
~imp() { }
void updt_params_core(params_ref const & p) {
m_max_rounds = p.get_uint("max_rounds", 4);
}
void updt_params_core(params_ref const & p) {
m_max_rounds = p.get_uint("max_rounds", 4);
}
void updt_params(params_ref const & p) {
m_r.updt_params(p);
updt_params_core(p);
}
bool is_shared(expr * t) {
return m_occs.is_shared(t);
}
bool is_shared_neg(expr * t, expr * & atom) {
if (!m.is_not(t, atom))
return false;
return is_shared(atom);
}
bool is_shared(expr * t) {
return m_occs.is_shared(t);
}
bool is_shared_eq(expr * t, expr * & lhs, expr * & value) {
expr* arg1, *arg2;
if (!m.is_eq(t, arg1, arg2))
return false;
if (m.is_value(arg1) && is_shared(arg2)) {
lhs = arg2;
value = arg1;
return true;
}
if (m.is_value(arg2) && is_shared(arg1)) {
lhs = arg1;
value = arg2;
return true;
}
bool is_shared_neg(expr * t, expr * & atom) {
if (!m.is_not(t, atom))
return false;
return is_shared(atom);
}
bool is_shared_eq(expr * t, expr * & lhs, expr * & value) {
expr* arg1, *arg2;
if (!m.is_eq(t, arg1, arg2))
return false;
if (m.is_value(arg1) && is_shared(arg2)) {
lhs = arg2;
value = arg1;
return true;
}
if (m.is_value(arg2) && is_shared(arg1)) {
lhs = arg1;
value = arg2;
return true;
}
return false;
}
void push_result(expr * new_curr, proof * new_pr) {
if (m_goal->proofs_enabled()) {
proof * pr = m_goal->pr(m_idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
void push_result(expr * new_curr, proof * new_pr) {
if (m_goal->proofs_enabled()) {
proof * pr = m_goal->pr(m_idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
expr_dependency_ref new_d(m);
if (m_goal->unsat_core_enabled()) {
new_d = m_goal->dep(m_idx);
expr_dependency * used_d = m_r.get_used_dependencies();
if (used_d != nullptr) {
new_d = m.mk_join(new_d, used_d);
m_r.reset_used_dependencies();
}
expr_dependency_ref new_d(m);
if (m_goal->unsat_core_enabled()) {
new_d = m_goal->dep(m_idx);
expr_dependency * used_d = m_r.get_used_dependencies();
if (used_d != nullptr) {
new_d = m.mk_join(new_d, used_d);
m_r.reset_used_dependencies();
}
m_goal->update(m_idx, new_curr, new_pr, new_d);
if (is_shared(new_curr)) {
m_subst->insert(new_curr, m.mk_true(), m.mk_iff_true(new_pr), new_d);
}
expr * atom;
if (is_shared_neg(new_curr, atom)) {
m_subst->insert(atom, m.mk_false(), m.mk_iff_false(new_pr), new_d);
}
expr * lhs, * value;
if (is_shared_eq(new_curr, lhs, value)) {
TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m) << "\n";);
m_subst->insert(lhs, value, new_pr, new_d);
}
}
void process_current() {
expr * curr = m_goal->form(m_idx);
expr_ref new_curr(m);
proof_ref new_pr(m);
if (!m_subst->empty()) {
m_r(curr, new_curr, new_pr);
}
else {
new_curr = curr;
if (m.proofs_enabled())
new_pr = m.mk_reflexivity(curr);
}
TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";);
if (new_curr != curr) {
m_modified = true;
//if (has_pb(curr))
// IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n");
}
push_result(new_curr, new_pr);
}
bool has_pb(expr* e) {
pb_util pb(m);
if (pb.is_ge(e)) return true;
if (m.is_or(e)) {
for (expr* a : *to_app(e)) {
if (pb.is_ge(a)) return true;
}
}
return false;
}
void run(goal_ref const & g, goal_ref_buffer & result) {
SASSERT(g->is_well_sorted());
tactic_report report("propagate-values", *g);
m_goal = g.get();
bool forward = true;
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned size = m_goal->size();
m_idx = 0;
m_modified = false;
unsigned round = 0;
if (m_goal->inconsistent())
goto end;
if (m_max_rounds == 0)
goto end;
m_subst = alloc(expr_substitution, m, g->unsat_core_enabled(), g->proofs_enabled());
m_r.set_substitution(m_subst.get());
m_occs(*m_goal);
while (true) {
TRACE("propagate_values", tout << "while(true) loop\n"; m_goal->display_with_dependencies(tout););
if (forward) {
for (; m_idx < size; m_idx++) {
process_current();
if (m_goal->inconsistent())
goto end;
}
}
m_goal->update(m_idx, new_curr, new_pr, new_d);
if (is_shared(new_curr)) {
m_subst->insert(new_curr, m.mk_true(), m.mk_iff_true(new_pr), new_d);
}
expr * atom;
if (is_shared_neg(new_curr, atom)) {
m_subst->insert(atom, m.mk_false(), m.mk_iff_false(new_pr), new_d);
}
expr * lhs, * value;
if (is_shared_eq(new_curr, lhs, value)) {
TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m) << "\n";);
m_subst->insert(lhs, value, new_pr, new_d);
}
}
void process_current() {
expr * curr = m_goal->form(m_idx);
expr_ref new_curr(m);
proof_ref new_pr(m);
if (!m_subst->empty()) {
m_r(curr, new_curr, new_pr);
if (m_subst->empty() && !m_modified)
goto end;
m_occs(*m_goal);
m_idx = m_goal->size();
forward = false;
m_subst->reset();
m_r.set_substitution(m_subst.get()); // reset, but keep substitution
}
else {
new_curr = curr;
if (m.proofs_enabled())
new_pr = m.mk_reflexivity(curr);
}
TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";);
if (new_curr != curr) {
m_modified = true;
//if (has_pb(curr))
// IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n");
}
push_result(new_curr, new_pr);
}
bool has_pb(expr* e) {
pb_util pb(m);
if (pb.is_ge(e)) return true;
if (m.is_or(e)) {
for (expr* a : *to_app(e)) {
if (pb.is_ge(a)) return true;
}
}
return false;
}
void operator()(goal_ref const & g,
goal_ref_buffer & result) {
SASSERT(g->is_well_sorted());
tactic_report report("propagate-values", *g);
m_goal = g.get();
bool forward = true;
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned size = m_goal->size();
m_idx = 0;
m_modified = false;
unsigned round = 0;
if (m_goal->inconsistent())
goto end;
if (m_max_rounds == 0)
goto end;
m_subst = alloc(expr_substitution, m, g->unsat_core_enabled(), g->proofs_enabled());
m_r.set_substitution(m_subst.get());
m_occs(*m_goal);
while (true) {
TRACE("propagate_values", tout << "while(true) loop\n"; m_goal->display_with_dependencies(tout););
if (forward) {
for (; m_idx < size; m_idx++) {
process_current();
if (m_goal->inconsistent())
goto end;
}
if (m_subst->empty() && !m_modified)
while (m_idx > 0) {
m_idx--;
process_current();
if (m_goal->inconsistent())
goto end;
m_occs(*m_goal);
m_idx = m_goal->size();
forward = false;
m_subst->reset();
m_r.set_substitution(m_subst.get()); // reset, but keep substitution
}
else {
while (m_idx > 0) {
m_idx--;
process_current();
if (m_goal->inconsistent())
goto end;
}
if (!m_modified)
goto end;
m_subst->reset();
m_r.set_substitution(m_subst.get()); // reset, but keep substitution
m_modified = false;
m_occs(*m_goal);
m_idx = 0;
size = m_goal->size();
forward = true;
}
round++;
if (round >= m_max_rounds)
break;
IF_VERBOSE(100, verbose_stream() << "starting new round, goal size: " << m_goal->num_exprs() << std::endl;);
TRACE("propagate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";);
if (!m_modified)
goto end;
m_subst->reset();
m_r.set_substitution(m_subst.get()); // reset, but keep substitution
m_modified = false;
m_occs(*m_goal);
m_idx = 0;
size = m_goal->size();
forward = true;
}
end:
m_goal->elim_redundancies();
m_goal->inc_depth();
result.push_back(m_goal);
SASSERT(m_goal->is_well_sorted());
TRACE("propagate_values", tout << "end\n"; m_goal->display(tout););
TRACE("propagate_values_core", m_goal->display_with_dependencies(tout););
m_goal = nullptr;
round++;
if (round >= m_max_rounds)
break;
IF_VERBOSE(100, verbose_stream() << "starting new round, goal size: " << m_goal->num_exprs() << std::endl;);
TRACE("propagate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";);
}
};
end:
m_goal->elim_redundancies();
m_goal->inc_depth();
result.push_back(m_goal);
SASSERT(m_goal->is_well_sorted());
TRACE("propagate_values", tout << "end\n"; m_goal->display(tout););
TRACE("propagate_values_core", m_goal->display_with_dependencies(tout););
m_goal = nullptr;
}
imp * m_imp;
params_ref m_params;
public:
propagate_values_tactic(ast_manager & m, params_ref const & p):
m(m),
m_r(m, p),
m_goal(nullptr),
m_occs(m, true /* track atoms */),
m_params(p) {
m_imp = alloc(imp, m, p);
updt_params_core(p);
}
tactic * translate(ast_manager & m) override {
return alloc(propagate_values_tactic, m, m_params);
}
~propagate_values_tactic() override {
dealloc(m_imp);
}
void updt_params(params_ref const & p) override {
m_params = p;
m_imp->updt_params(p);
m_r.updt_params(p);
updt_params_core(p);
}
void collect_param_descrs(param_descrs & r) override {
@ -252,7 +234,7 @@ public:
void operator()(goal_ref const & in, goal_ref_buffer & result) override {
try {
(*m_imp)(in, result);
run(in, result);
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());
@ -260,15 +242,14 @@ public:
}
void cleanup() override {
ast_manager & m = m_imp->m;
params_ref p = std::move(m_params);
m_imp->~imp();
new (m_imp) imp(m, p);
m_r.cleanup();
m_subst = nullptr;
m_occs.cleanup();
}
};
}
tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p) {
return alloc(propagate_values_tactic, m, p);
}

5
src/tactic/core/propagate_values_tactic.h
View file

@ -17,8 +17,7 @@ Author:
Revision History:
--*/
#ifndef PROPAGATE_VALUES_TACTIC_H_
#define PROPAGATE_VALUES_TACTIC_H_
#pragma once
#include "util/params.h"
class ast_manager;
@ -29,5 +28,3 @@ tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p = para
/*
ADD_TACTIC("propagate-values", "propagate constants.", "mk_propagate_values_tactic(m, p)")
*/
#endif