mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

mising files

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-26 01:55:03 -07:00
parent 9b53646a34
commit e3e965883f
2 changed files with 6 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/smt/asserted_formulas_new.cpp
View file

@ -84,7 +84,6 @@ asserted_formulas_new::~asserted_formulas_new() {
void asserted_formulas_new::push_assertion(expr * e, proof * pr, vector<justified_expr>& result) {
if (inconsistent()) {
SASSERT(!result.empty());
return;
}
expr* e1 = 0;
@ -106,13 +105,8 @@ void asserted_formulas_new::push_assertion(expr * e, proof * pr, vector<justifie
for (unsigned i = 0; i < to_app(e1)->get_num_args(); ++i) {
expr* arg = to_app(e1)->get_arg(i), *e2;
proof_ref _pr(m.mk_not_or_elim(pr, i), m);
if (m.is_not(arg, e2)) {
push_assertion(e2, _pr, result);
}
else {
expr_ref narg(m.mk_not(arg), m);
push_assertion(narg, _pr, result);
}
expr_ref narg(mk_not(m, arg), m);
push_assertion(narg, _pr, result);
}
}
else {
@ -154,8 +148,7 @@ void asserted_formulas_new::assert_expr(expr * e, proof * _in_pr) {
}
void asserted_formulas_new::assert_expr(expr * e) {
if (!inconsistent())
assert_expr(e, m.mk_asserted(e));
assert_expr(e, m.mk_asserted(e));
}
void asserted_formulas_new::get_assertions(ptr_vector<expr> & result) const {
@ -220,8 +213,8 @@ void asserted_formulas_new::reduce() {
if (!m_params.m_preprocess)
return;
if (m_macro_manager.has_macros())
expand_macros();
invoke(m_find_macros);
TRACE("before_reduce", display(tout););
CASSERT("well_sorted", check_well_sorted());
@ -313,11 +306,6 @@ void asserted_formulas_new::swap_asserted_formulas(vector<justified_expr>& formu
m_formulas.append(formulas);
}
void asserted_formulas_new::find_macros_fn::operator()() {
TRACE("before_find_macros", af.display(tout););
af.find_macros_core();
TRACE("after_find_macros", af.display(tout););
}
void asserted_formulas_new::find_macros_core() {
vector<justified_expr> new_fmls;
@ -327,12 +315,6 @@ void asserted_formulas_new::find_macros_core() {
reduce_and_solve();
}
void asserted_formulas_new::expand_macros() {
IF_IVERBOSE(10, verbose_stream() << "(smt.expand-macros)\n";);
find_macros_core();
}
void asserted_formulas_new::apply_quasi_macros() {
TRACE("before_quasi_macros", display(tout););
vector<justified_expr> new_fmls;

2
src/smt/asserted_formulas_new.h
View file

@ -87,7 +87,7 @@ class asserted_formulas_new {
class find_macros_fn : public simplify_fmls {
public:
find_macros_fn(asserted_formulas_new& af): simplify_fmls(af, "find-macros") {}
virtual void operator()();
virtual void operator()() { af.find_macros_core(); }
virtual bool should_apply() const { return af.m_params.m_macro_finder && af.has_quantifiers(); }
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
};