From 66234ff4bd6f2fd325a4e817d1bcfb558d4c0041 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Oct 2012 14:08:00 -0700 Subject: [PATCH] deleted assertion_sets (aka old tactic framework) Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 3 - src/assertion_set/README | 1 - src/assertion_set/assertion_set.cpp | 430 ------ src/assertion_set/assertion_set.h | 98 -- src/assertion_set/assertion_set_rewriter.cpp | 122 -- src/assertion_set/assertion_set_rewriter.h | 56 - src/assertion_set/assertion_set_strategy.cpp | 1255 ----------------- src/assertion_set/assertion_set_strategy.h | 223 --- src/assertion_set/assertion_set_util.cpp | 220 --- src/assertion_set/assertion_set_util.h | 91 -- src/assertion_set/der_strategy.cpp | 94 -- src/assertion_set/der_strategy.h | 47 - src/assertion_set/elim_distinct.cpp | 232 --- src/assertion_set/elim_distinct.h | 54 - .../elim_var_model_converter.cpp | 120 -- src/assertion_set/elim_var_model_converter.h | 56 - src/assertion_set/gaussian_elim.cpp | 775 ---------- src/assertion_set/gaussian_elim.h | 66 - .../num_occurs_assertion_set.cpp | 29 - src/assertion_set/num_occurs_assertion_set.h | 38 - src/assertion_set/reduce_args.cpp | 521 ------- src/assertion_set/reduce_args.h | 92 -- .../shallow_context_simplifier.cpp | 257 ---- .../shallow_context_simplifier.h | 59 - src/assertion_set/st2tactic.cpp | 77 - src/assertion_set/st2tactic.h | 27 - src/assertion_set/strategy_exception.cpp | 26 - src/assertion_set/strategy_exception.h | 53 - 28 files changed, 5122 deletions(-) delete mode 100644 src/assertion_set/README delete mode 100644 src/assertion_set/assertion_set.cpp delete mode 100644 src/assertion_set/assertion_set.h delete mode 100644 src/assertion_set/assertion_set_rewriter.cpp delete mode 100644 src/assertion_set/assertion_set_rewriter.h delete mode 100644 src/assertion_set/assertion_set_strategy.cpp delete mode 100644 src/assertion_set/assertion_set_strategy.h delete mode 100644 src/assertion_set/assertion_set_util.cpp delete mode 100644 src/assertion_set/assertion_set_util.h delete mode 100644 src/assertion_set/der_strategy.cpp delete mode 100644 src/assertion_set/der_strategy.h delete mode 100644 src/assertion_set/elim_distinct.cpp delete mode 100644 src/assertion_set/elim_distinct.h delete mode 100644 src/assertion_set/elim_var_model_converter.cpp delete mode 100644 src/assertion_set/elim_var_model_converter.h delete mode 100644 src/assertion_set/gaussian_elim.cpp delete mode 100644 src/assertion_set/gaussian_elim.h delete mode 100644 src/assertion_set/num_occurs_assertion_set.cpp delete mode 100644 src/assertion_set/num_occurs_assertion_set.h delete mode 100644 src/assertion_set/reduce_args.cpp delete mode 100644 src/assertion_set/reduce_args.h delete mode 100644 src/assertion_set/shallow_context_simplifier.cpp delete mode 100644 src/assertion_set/shallow_context_simplifier.h delete mode 100644 src/assertion_set/st2tactic.cpp delete mode 100644 src/assertion_set/st2tactic.h delete mode 100644 src/assertion_set/strategy_exception.cpp delete mode 100644 src/assertion_set/strategy_exception.h diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 13a3696a7..475959888 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -39,9 +39,6 @@ add_lib('tactic', ['ast', 'model']) # However, it is still used by many old components. add_lib('old_params', ['model', 'simplifier']) add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier']) -# Assertion set is the old tactic framework used in Z3 3.x. It will be deleted as soon as we finish the porting old -# code to the new tactic framework. -add_lib('assertion_set', ['cmd_context']) add_lib('substitution', ['ast'], 'ast/substitution') add_lib('normal_forms', ['tactic', 'old_params']) add_lib('pattern', ['normal_forms'], 'ast/pattern') diff --git a/src/assertion_set/README b/src/assertion_set/README deleted file mode 100644 index ed699ed82..000000000 --- a/src/assertion_set/README +++ /dev/null @@ -1 +0,0 @@ -This module is obsolete. It is subsumed by the tactic module. \ No newline at end of file diff --git a/src/assertion_set/assertion_set.cpp b/src/assertion_set/assertion_set.cpp deleted file mode 100644 index 0436f45dc..000000000 --- a/src/assertion_set/assertion_set.cpp +++ /dev/null @@ -1,430 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - assertion_set.cpp - -Abstract: - - Assertion set. - -Author: - - Leonardo de Moura (leonardo) 2011-04-20 - -Revision History: - ---*/ -#include"assertion_set.h" -#include"cmd_context.h" -#include"ast_ll_pp.h" -#include"ast_smt2_pp.h" -#include"for_each_expr.h" - -void assertion_set::copy(assertion_set & target) const { - if (this == &target) - return; - m().copy(m_forms, target.m_forms); - m().copy(m_proofs, target.m_proofs); - target.m_inconsistent = m_inconsistent; -} - -void assertion_set::push_back(expr * f, proof * pr) { - if (m().is_true(f)) - return; - if (m().is_false(f)) { - m().del(m_forms); - m().del(m_proofs); - m_inconsistent = true; - } - else { - SASSERT(!m_inconsistent); - } - m().push_back(m_forms, f); - if (m().proofs_enabled()) - m().push_back(m_proofs, pr); -} - -void assertion_set::quick_process(bool save_first, expr * & f) { - if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) { - if (!save_first) { - push_back(f, 0); - } - return; - } - typedef std::pair expr_pol; - sbuffer todo; - todo.push_back(expr_pol(f, true)); - while (!todo.empty()) { - if (m_inconsistent) - return; - expr_pol p = todo.back(); - expr * curr = p.first; - bool pol = p.second; - todo.pop_back(); - if (pol && m().is_and(curr)) { - app * t = to_app(curr); - unsigned i = t->get_num_args(); - while (i > 0) { - --i; - todo.push_back(expr_pol(t->get_arg(i), true)); - } - } - else if (!pol && m().is_or(curr)) { - app * t = to_app(curr); - unsigned i = t->get_num_args(); - while (i > 0) { - --i; - todo.push_back(expr_pol(t->get_arg(i), false)); - } - } - else if (m().is_not(curr)) { - todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol)); - } - else { - if (!pol) - curr = m().mk_not(curr); - if (save_first) { - f = curr; - save_first = false; - } - else { - push_back(curr, 0); - } - } - } -} - -void assertion_set::process_and(bool save_first, app * f, proof * pr, expr_ref & out_f, proof_ref & out_pr) { - unsigned num = f->get_num_args(); - for (unsigned i = 0; i < num; i++) { - if (m_inconsistent) - return; - slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), out_f, out_pr); - } -} - -void assertion_set::process_not_or(bool save_first, app * f, proof * pr, expr_ref & out_f, proof_ref & out_pr) { - unsigned num = f->get_num_args(); - for (unsigned i = 0; i < num; i++) { - if (m_inconsistent) - return; - expr * child = f->get_arg(i); - if (m().is_not(child)) { - expr * not_child = to_app(child)->get_arg(0); - slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), out_f, out_pr); - } - else { - expr_ref not_child(m()); - not_child = m().mk_not(child); - slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), out_f, out_pr); - } - } -} - -void assertion_set::slow_process(bool save_first, expr * f, proof * pr, expr_ref & out_f, proof_ref & out_pr) { - if (m().is_and(f)) - process_and(save_first, to_app(f), pr, out_f, out_pr); - else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0))) - process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, out_f, out_pr); - else if (save_first) { - out_f = f; - out_pr = pr; - } - else { - push_back(f, pr); - } -} - -void assertion_set::slow_process(expr * f, proof * pr) { - expr_ref out_f(m()); - proof_ref out_pr(m()); - slow_process(false, f, pr, out_f, out_pr); -} - -void assertion_set::assert_expr(expr * f, proof * pr) { - SASSERT(m().proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); - if (m_inconsistent) - return; - if (m().proofs_enabled()) - slow_process(f, pr); - else - quick_process(false, f); -} - -void assertion_set::update(unsigned i, expr * f, proof * pr) { - SASSERT(m().proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); - if (m_inconsistent) - return; - if (m().proofs_enabled()) { - expr_ref out_f(m()); - proof_ref out_pr(m()); - slow_process(true, f, pr, out_f, out_pr); - if (!m_inconsistent) { - if (m().is_false(out_f)) { - push_back(out_f, out_pr); - } - else { - m().set(m_forms, i, out_f); - m().set(m_proofs, i, out_pr); - } - } - } - else { - quick_process(true, f); - if (!m_inconsistent) { - if (m().is_false(f)) - push_back(f, 0); - else - m().set(m_forms, i, f); - } - } -} - -void assertion_set::reset() { - m().del(m_forms); - m().del(m_proofs); - m_inconsistent = false; -} - -void assertion_set::display(cmd_context & ctx, std::ostream & out) const { - out << "(assertion-set"; - unsigned sz = size(); - for (unsigned i = 0; i < sz; i++) { - out << "\n "; - ctx.display(out, form(i), 2); - } - out << ")" << std::endl; -} - -void assertion_set::display(cmd_context & ctx) const { - display(ctx, ctx.regular_stream()); -} - -void assertion_set::display(std::ostream & out) const { - out << "(assertion-set"; - unsigned sz = size(); - for (unsigned i = 0; i < sz; i++) { - out << "\n "; - out << mk_ismt2_pp(form(i), m(), 2); - } - out << ")" << std::endl; -} - -void assertion_set::display_as_and(std::ostream & out) const { - ptr_buffer args; - unsigned sz = size(); - for (unsigned i = 0; i < sz; i++) - args.push_back(form(i)); - expr_ref tmp(m()); - tmp = m().mk_and(args.size(), args.c_ptr()); - out << mk_ismt2_pp(tmp, m()) << "\n"; -} - -void assertion_set::display_ll(std::ostream & out) const { - unsigned sz = size(); - for (unsigned i = 0; i < sz; i++) { - out << mk_ll_pp(form(i), m()) << "\n"; - } -} - -/** - \brief Assumes that the formula is already in CNF. -*/ -void assertion_set::display_dimacs(std::ostream & out) const { - obj_map expr2var; - unsigned num_vars = 0; - unsigned num_cls = size(); - for (unsigned i = 0; i < num_cls; i++) { - expr * f = form(i); - unsigned num_lits; - expr * const * lits; - if (m().is_or(f)) { - num_lits = to_app(f)->get_num_args(); - lits = to_app(f)->get_args(); - } - else { - num_lits = 1; - lits = &f; - } - for (unsigned j = 0; j < num_lits; j++) { - expr * l = lits[j]; - if (m().is_not(l)) - l = to_app(l)->get_arg(0); - if (expr2var.contains(l)) - continue; - num_vars++; - expr2var.insert(l, num_vars); - } - } - out << "p cnf " << num_vars << " " << num_cls << "\n"; - for (unsigned i = 0; i < num_cls; i++) { - expr * f = form(i); - unsigned num_lits; - expr * const * lits; - if (m().is_or(f)) { - num_lits = to_app(f)->get_num_args(); - lits = to_app(f)->get_args(); - } - else { - num_lits = 1; - lits = &f; - } - for (unsigned j = 0; j < num_lits; j++) { - expr * l = lits[j]; - if (m().is_not(l)) { - out << "-"; - l = to_app(l)->get_arg(0); - } - unsigned id = UINT_MAX; - expr2var.find(l, id); - SASSERT(id != UINT_MAX); - out << id << " "; - } - out << "0\n"; - } -} - -unsigned assertion_set::num_exprs() const { - expr_fast_mark1 visited; - unsigned sz = size(); - unsigned r = 0; - for (unsigned i = 0; i < sz; i++) { - r += get_num_exprs(form(i), visited); - } - return r; -} - -/** - \brief Eliminate true formulas. -*/ -void assertion_set::elim_true() { - unsigned sz = size(); - unsigned j = 0; - for (unsigned i = 0; i < sz; i++) { - expr * f = form(i); - if (m().is_true(f)) - continue; - if (i == j) { - j++; - continue; - } - m().set(m_forms, j, f); - if (m().proofs_enabled()) - m().set(m_proofs, j, m().get(m_proofs, i)); - j++; - } - for (; j < sz; j++) { - m().pop_back(m_forms); - if (m().proofs_enabled()) - m().pop_back(m_proofs); - } -} - -void assertion_set::elim_redundancies() { - if (inconsistent()) - return; - expr_ref_fast_mark1 neg_lits(m()); - expr_ref_fast_mark2 pos_lits(m()); - unsigned sz = size(); - unsigned j = 0; - for (unsigned i = 0; i < sz; i++) { - expr * f = form(i); - if (m().is_true(f)) - continue; - if (m().is_not(f)) { - expr * atom = to_app(f)->get_arg(0); - if (neg_lits.is_marked(atom)) - continue; - if (pos_lits.is_marked(atom)) { - proof * p = 0; - if (m().proofs_enabled()) { - proof * pr1 = 0; - proof * pr2 = pr(i); - for (unsigned j = 0; j < i; j++) { - if (form(j) == atom) { - pr1 = pr(j); - break; - } - } - SASSERT(pr1); - proof * prs[2] = { pr1, pr2 }; - p = m().mk_unit_resolution(2, prs); - } - push_back(m().mk_false(), p); - return; - } - neg_lits.mark(atom); - } - else { - if (pos_lits.is_marked(f)) - continue; - if (neg_lits.is_marked(f)) { - proof * p = 0; - if (m().proofs_enabled()) { - proof * pr1 = 0; - proof * pr2 = pr(i); - for (unsigned j = 0; j < i; j++) { - expr * curr = form(j); - expr * atom; - if (m().is_not(curr, atom) && atom == f) { - pr1 = pr(j); - break; - } - } - SASSERT(pr1); - proof * prs[2] = { pr1, pr2 }; - p = m().mk_unit_resolution(2, prs); - } - push_back(m().mk_false(), p); - return; - } - pos_lits.mark(f); - } - if (i == j) { - j++; - continue; - } - m().set(m_forms, j, f); - if (m().proofs_enabled()) - m().set(m_proofs, j, pr(i)); - j++; - } - - for (; j < sz; j++) { - m().pop_back(m_forms); - if (m().proofs_enabled()) - m().pop_back(m_proofs); - } -} - -/** - \brief Assert expressions from ctx into t. -*/ -void assert_exprs_from(cmd_context const & ctx, assertion_set & t) { - ptr_vector::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - for (; it != end; ++it) { - t.assert_expr(*it); - } -} - -/** - \brief Translate the assertion set to a new one that uses a different ast_manager. -*/ -assertion_set * assertion_set::translate(ast_translation & translator) const { - ast_manager & m_to = translator.to(); - assertion_set * res = alloc(assertion_set, m_to); - - unsigned sz = m().size(m_forms); - for (unsigned i = 0; i < sz; i++) { - res->m().push_back(res->m_forms, translator(m().get(m_forms, i))); - if (m_to.proofs_enabled()) - res->m().push_back(res->m_proofs, translator(m().get(m_proofs, i))); - } - - res->m_inconsistent = m_inconsistent; - - return res; -} diff --git a/src/assertion_set/assertion_set.h b/src/assertion_set/assertion_set.h deleted file mode 100644 index 3fdbdbbe2..000000000 --- a/src/assertion_set/assertion_set.h +++ /dev/null @@ -1,98 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - assertion_set.h - -Abstract: - - Assertion set. - -Author: - - Leonardo de Moura (leonardo) 2011-04-20 - -Revision History: - ---*/ -#ifndef _ASSERTION_SET_H_ -#define _ASSERTION_SET_H_ - -#include"ast.h" -#include"ast_translation.h" -#include"for_each_expr.h" - -class cmd_context; - -class assertion_set { - ast_manager & m_manager; - bool m_inconsistent; - expr_array m_forms; - expr_array m_proofs; - - void push_back(expr * f, proof * pr); - void quick_process(bool save_first, expr * & f); - void process_and(bool save_first, app * f, proof * pr, expr_ref & out_f, proof_ref & out_pr); - void process_not_or(bool save_first, app * f, proof * pr, expr_ref & out_f, proof_ref & out_pr); - void slow_process(bool save_first, expr * f, proof * pr, expr_ref & out_f, proof_ref & out_pr); - void slow_process(expr * f, proof * pr); - -public: - assertion_set(ast_manager & m):m_manager(m), m_inconsistent(false) {} - ~assertion_set() { reset(); } - - ast_manager & m() const { return m_manager; } - - bool inconsistent() const { return m_inconsistent; } - - void reset(); - - void copy(assertion_set & target) const; - - void assert_expr(expr * f, proof * pr); - - void assert_expr(expr * f) { - assert_expr(f, m().mk_asserted(f)); - } - - unsigned size() const { return m().size(m_forms); } - - unsigned num_exprs() const; - - expr * form(unsigned i) const { return m().get(m_forms, i); } - - proof * pr(unsigned i) const { return m().proofs_enabled() ? static_cast(m().get(m_proofs, i)) : 0; } - - void update(unsigned i, expr * f, proof * pr = 0); - - void elim_true(); - - void elim_redundancies(); - - void display(cmd_context & ctx, std::ostream & out) const; - - void display(cmd_context & ctx) const; - - void display(std::ostream & out) const; - - void display_ll(std::ostream & out) const; - - void display_as_and(std::ostream & out) const; - - void display_dimacs(std::ostream & out) const; - - assertion_set * translate(ast_translation & translator) const; -}; - -void assert_exprs_from(cmd_context const & ctx, assertion_set & t); - -template -void for_each_expr_as(ForEachProc& proc, assertion_set const& s) { - expr_mark visited; - for (unsigned i = 0; i < s.size(); ++i) { - for_each_expr(proc, visited, s.form(i)); - } -} - -#endif diff --git a/src/assertion_set/assertion_set_rewriter.cpp b/src/assertion_set/assertion_set_rewriter.cpp deleted file mode 100644 index 431739024..000000000 --- a/src/assertion_set/assertion_set_rewriter.cpp +++ /dev/null @@ -1,122 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - assertion_set_rewriter.cpp - -Abstract: - - Apply rewriting rules in an assertion set. - -Author: - - Leonardo (leonardo) 2011-04-27 - -Notes: - ---*/ -#include"assertion_set_rewriter.h" -#include"th_rewriter.h" -#include"ast_smt2_pp.h" -#include"assertion_set_util.h" - -struct assertion_set_rewriter::imp { - ast_manager & m_manager; - th_rewriter m_r; - unsigned m_num_steps; - - imp(ast_manager & m, params_ref const & p): - m_manager(m), - m_r(m, p), - m_num_steps(0) { - } - - ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { - m_r.set_cancel(f); - } - - void reset() { - m_r.reset(); - m_num_steps = 0; - } - - void operator()(assertion_set & s) { - SASSERT(is_well_sorted(s)); - as_st_report report("simplifier", s); - TRACE("before_simplifier", s.display(tout);); - m_num_steps = 0; - if (s.inconsistent()) - return; - expr_ref new_curr(m()); - proof_ref new_pr(m()); - unsigned size = s.size(); - for (unsigned idx = 0; idx < size; idx++) { - if (s.inconsistent()) - break; - expr * curr = s.form(idx); - m_r(curr, new_curr, new_pr); - m_num_steps += m_r.get_num_steps(); - if (m().proofs_enabled()) { - proof * pr = s.pr(idx); - new_pr = m().mk_modus_ponens(pr, new_pr); - } - s.update(idx, new_curr, new_pr); - } - TRACE("after_simplifier_bug", s.display(tout);); - s.elim_redundancies(); - TRACE("after_simplifier", s.display(tout);); - SASSERT(is_well_sorted(s)); - } - - unsigned get_num_steps() const { return m_num_steps; } -}; - -assertion_set_rewriter::assertion_set_rewriter(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); -} - -assertion_set_rewriter::~assertion_set_rewriter() { - dealloc(m_imp); -} - -void assertion_set_rewriter::updt_params(params_ref const & p) { - m_params = p; - m_imp->m_r.updt_params(p); -} - -void assertion_set_rewriter::get_param_descrs(param_descrs & r) { - th_rewriter::get_param_descrs(r); -} - -void assertion_set_rewriter::operator()(assertion_set & s) { - m_imp->operator()(s); -} - -void assertion_set_rewriter::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} - -void assertion_set_rewriter::cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; - #pragma omp critical (as_st_cancel) - { - m_imp = 0; - } - dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (as_st_cancel) - { - m_imp = d; - } -} - -unsigned assertion_set_rewriter::get_num_steps() const { - return m_imp->get_num_steps(); -} - diff --git a/src/assertion_set/assertion_set_rewriter.h b/src/assertion_set/assertion_set_rewriter.h deleted file mode 100644 index fd93db930..000000000 --- a/src/assertion_set/assertion_set_rewriter.h +++ /dev/null @@ -1,56 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - assertion_set_rewriter.h - -Abstract: - - Apply rewriting rules in an assertion set. - -Author: - - Leonardo (leonardo) 2011-04-22 - -Notes: - ---*/ -#ifndef _ASSERTION_SET_REWRITER_H_ -#define _ASSERTION_SET_REWRITER_H_ - -#include"assertion_set_strategy.h" - -class assertion_set_rewriter : public assertion_set_strategy { - struct imp; - imp * m_imp; - params_ref m_params; -public: - assertion_set_rewriter(ast_manager & m, params_ref const & ref = params_ref()); - virtual ~assertion_set_rewriter(); - - virtual void updt_params(params_ref const & p); - static void get_param_descrs(param_descrs & r); - virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } - - /** - \brief Apply rewriting/simplification rules on the assertion set \c s. - */ - void operator()(assertion_set & s); - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - operator()(s); - mc = 0; - } - - virtual void cleanup(); - - unsigned get_num_steps() const; - virtual void set_cancel(bool f); -}; - -inline as_st * mk_simplifier(ast_manager & m, params_ref const & p = params_ref()) { - return clean(alloc(assertion_set_rewriter, m, p)); -} - -#endif diff --git a/src/assertion_set/assertion_set_strategy.cpp b/src/assertion_set/assertion_set_strategy.cpp deleted file mode 100644 index 209f20351..000000000 --- a/src/assertion_set/assertion_set_strategy.cpp +++ /dev/null @@ -1,1255 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - assertion_set_strategy.h - -Abstract: - - Abstract strategy for assertion sets, and simple combinators. - -Author: - - Leonardo (leonardo) 2011-05-17 - -Notes: - ---*/ -#include"assertion_set_strategy.h" -#include"assertion_set_util.h" -#include"cooperate.h" -#include"scoped_timer.h" -#include"cancel_eh.h" -#include"front_end_params.h" -#include"progress_callback.h" -#include"params2front_end_params.h" -#include"stopwatch.h" -#include"ast_translation.h" -#include"model_v2_pp.h" -#include -#include"z3_omp.h" - -struct as_st_report::imp { - char const * m_id; - assertion_set & m_set; - stopwatch m_watch; - double m_start_memory; - - imp(char const * id, assertion_set & s): - m_id(id), - m_set(s), - m_start_memory(static_cast(memory::get_allocation_size())/static_cast(1024*1024)) { - m_watch.start(); - } - - ~imp() { - m_watch.stop(); - double end_memory = static_cast(memory::get_allocation_size())/static_cast(1024*1024); - verbose_stream() << "(" << m_id - << " :num-exprs " << m_set.num_exprs() - << " :num-asts " << m_set.m().get_num_asts() - << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() - << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory - << " :after-memory " << std::fixed << std::setprecision(2) << end_memory - << ")" << std::endl; - } -}; - -as_st_report::as_st_report(char const * id, assertion_set & s) { - if (get_verbosity_level() >= ST_VERBOSITY_LVL) - m_imp = alloc(imp, id, s); - else - m_imp = 0; -} - -void report_st_progress(char const * id, unsigned val) { - if (val > 0) { - IF_VERBOSE(ST_VERBOSITY_LVL, verbose_stream() << "(" << id << " " << val << ")" << std::endl;); - } -} - -as_st_report::~as_st_report() { - if (m_imp) - dealloc(m_imp); -} - -class report_verbose_st : public assertion_set_strategy { - std::string m_msg; - unsigned m_lvl; -public: - report_verbose_st(char const* msg, unsigned lvl) : m_msg(msg), m_lvl(lvl) {} - - virtual void cleanup() {} - virtual void operator()(assertion_set& s, model_converter_ref & mc) { - IF_VERBOSE(m_lvl, verbose_stream() << m_msg << "\n";); - } -}; - -as_st * mk_report_verbose_st(char const* msg, unsigned lvl) { - return alloc(report_verbose_st, msg, lvl); -} - - -void assertion_set_strategy::cancel() { - #pragma omp critical (as_st_cancel) - { - set_cancel(true); - } -} - -void assertion_set_strategy::reset_cancel() { - #pragma omp critical (as_st_cancel) - { - set_cancel(false); - } -} - -bool is_equal(assertion_set const & s1, assertion_set const & s2) { - if (s1.size() != s2.size()) - return false; - unsigned num1 = 0; // num unique ASTs in s1 - unsigned num2 = 0; // num unique ASTs in s2 - expr_fast_mark1 visited1; - expr_fast_mark2 visited2; - unsigned sz = s1.size(); - for (unsigned i = 0; i < sz; i++) { - expr * f1 = s1.form(i); - if (visited1.is_marked(f1)) - continue; - num1++; - visited1.mark(f1); - } - SASSERT(num1 <= sz); - SASSERT(0 <= num1); - for (unsigned i = 0; i < sz; i++) { - expr * f2 = s2.form(i); - if (visited2.is_marked(f2)) - continue; - num2++; - visited2.mark(f2); - if (!visited1.is_marked(f2)) - return false; - } - SASSERT(num2 <= sz); - SASSERT(0 <= num2); - SASSERT(num1 >= num2); - return num1 == num2; -} - -class composite_as_st : public as_st { -protected: - ptr_vector m_sts; - volatile bool m_cancel; - - void checkpoint() { - if (m_cancel) - throw strategy_exception(STE_CANCELED_MSG); - } - -public: - composite_as_st(unsigned num, as_st * const * sts):m_cancel(false) { - for (unsigned i = 0; i < num; i++) { - m_sts.push_back(sts[i]); - sts[i]->inc_ref(); - } - DEBUG_CODE({ - for (unsigned i = 0; i < num; i++) { - SASSERT(sts[i]); - } - }); - } - - virtual ~composite_as_st() { - ptr_buffer old_sts; - unsigned sz = m_sts.size(); - old_sts.append(sz, m_sts.c_ptr()); - #pragma omp critical (as_st_cancel) - { - for (unsigned i = 0; i < sz; i++) { - m_sts[i] = 0; - } - } - for (unsigned i = 0; i < sz; i++) { - old_sts[i]->dec_ref(); - } - } - - virtual void updt_params(params_ref const & p) { - TRACE("composite_updt_params", tout << "updt_params: " << p << "\n";); - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) - (*it)->updt_params(p); - } - - virtual void collect_param_descrs(param_descrs & r) { - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) - (*it)->collect_param_descrs(r); - } - - virtual void collect_statistics(statistics & st) const { - ptr_vector::const_iterator it = m_sts.begin(); - ptr_vector::const_iterator end = m_sts.end(); - for (; it != end; ++it) - (*it)->collect_statistics(st); - } - - virtual void reset_statistics() { - ptr_vector::const_iterator it = m_sts.begin(); - ptr_vector::const_iterator end = m_sts.end(); - for (; it != end; ++it) - (*it)->reset_statistics(); - } - - virtual void cleanup() { - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) - (*it)->cleanup(); - } - - virtual void reset() { - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) - (*it)->reset(); - } - - virtual void set_front_end_params(front_end_params & p) { - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) - (*it)->set_front_end_params(p); - } - - virtual void set_logic(symbol const & l) { - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) - (*it)->set_logic(l); - } - - virtual void set_progress_callback(progress_callback * callback) { - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) - (*it)->set_progress_callback(callback); - } - -protected: - /** - \brief Reset cancel flag of st if this was not canceled. - */ - void parent_reset_cancel(as_st & st) { - #pragma omp critical (as_st_cancel) - { - if (!m_cancel) { - st.set_cancel(false); - } - } - } - - virtual void set_cancel(bool f) { - m_cancel = f; - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) - if (*it) - (*it)->set_cancel(f); - } -}; - -class and_then_as_st : public composite_as_st { -public: - and_then_as_st(unsigned num, as_st * const * sts):composite_as_st(num, sts) {} - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - mc = 0; - if (s.inconsistent()) - return; - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) { - checkpoint(); - as_st & st = *(*it); - model_converter_ref mc1; // force mc1 to be 0 at every iteration... otherwise, it may contain value of the previous iteration. - try { - st(s, mc1); - } - catch (strategy_exception & ex) { - mc = 0; - throw ex; - } - mc = concat(mc.get(), mc1.get()); - } - } -}; - -as_st * and_then(unsigned num, as_st * const * sts) { - return alloc(and_then_as_st, num, sts); -} - -as_st * and_then(as_st * st1, as_st * st2) { - as_st * sts[2] = { st1, st2 }; - return and_then(2, sts); -} - -as_st * and_then(as_st * st1, as_st * st2, as_st * st3) { - as_st * sts[3] = { st1, st2, st3 }; - return and_then(3, sts); -} - -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4) { - as_st * sts[4] = { st1, st2, st3, st4 }; - return and_then(4, sts); -} - -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5) { - as_st * sts[5] = { st1, st2, st3, st4, st5 }; - return and_then(5, sts); -} - -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6) { - as_st * sts[6] = { st1, st2, st3, st4, st5, st6 }; - return and_then(6, sts); -} - -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7) { - as_st * sts[7] = { st1, st2, st3, st4, st5, st6, st7 }; - return and_then(7, sts); -} - -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8) { - as_st * sts[8] = { st1, st2, st3, st4, st5, st6, st7, st8 }; - return and_then(8, sts); -} - -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8, as_st * st9) { - as_st * sts[9] = { st1, st2, st3, st4, st5, st6, st7, st8, st9 }; - return and_then(9, sts); -} - -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8, as_st * st9, as_st * st10) { - as_st * sts[10] = { st1, st2, st3, st4, st5, st6, st7, st8, st9, st10 }; - return and_then(10, sts); - -} - -class or_else_as_st : public composite_as_st { -public: - or_else_as_st(unsigned num, as_st * const * sts):composite_as_st(num, sts) {} - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - if (s.inconsistent()) - return; - assertion_set orig_s(s.m()); - s.copy(orig_s); - unsigned sz = m_sts.size(); - unsigned i; - for (i = 0; i < sz - 1; i++) { - checkpoint(); - as_st & st = *(m_sts[i]); - mc = 0; - try { - st(s, mc); - return; - } - catch (strategy_exception ex) { - mc = 0; - s.reset(); - orig_s.copy(s); - } - } - checkpoint(); - SASSERT(i == sz - 1); - as_st & st = *(m_sts[i]); - st(s, mc); - } -}; - - -as_st * or_else(unsigned num, as_st * const * sts) { - return alloc(or_else_as_st, num, sts); -} - -as_st * or_else(as_st * st1, as_st * st2) { - as_st * sts[2] = { st1, st2 }; - return or_else(2, sts); -} - -as_st * or_else(as_st * st1, as_st * st2, as_st * st3) { - as_st * sts[3] = { st1, st2, st3 }; - return or_else(3, sts); -} - -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4) { - as_st * sts[4] = { st1, st2, st3, st4 }; - return or_else(4, sts); -} - -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5) { - as_st * sts[5] = { st1, st2, st3, st4, st5 }; - return or_else(5, sts); -} - -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6) { - as_st * sts[6] = { st1, st2, st3, st4, st5, st6 }; - return or_else(6, sts); -} - -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7) { - as_st * sts[7] = { st1, st2, st3, st4, st5, st6, st7 }; - return or_else(7, sts); -} - -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8) { - as_st * sts[8] = { st1, st2, st3, st4, st5, st6, st7, st8 }; - return or_else(8, sts); -} - -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8, as_st * st9) { - as_st * sts[9] = { st1, st2, st3, st4, st5, st6, st7, st8, st9 }; - return or_else(9, sts); -} - -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8, as_st * st9, as_st * st10) { - as_st * sts[10] = { st1, st2, st3, st4, st5, st6, st7, st8, st9, st10 }; - return or_else(10, sts); -} - -class par_as_st : public or_else_as_st { -public: - par_as_st(unsigned num, as_st * const * sts):or_else_as_st(num, sts) {} - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - if (s.inconsistent()) { - mc = 0; - return; - } - - if (omp_in_parallel()) { - // execute tasks sequentially - or_else_as_st::operator()(s, mc); - return; - } - - ast_manager & m = s.m(); - - sbuffer s_copies; - ptr_vector::iterator it = m_sts.begin(); - ptr_vector::iterator end = m_sts.end(); - for (; it != end; ++it) { - s_copies.push_back(assertion_set(m)); - assertion_set & s_copy = s_copies.back(); - s.copy(s_copy); - } - - unsigned finished_id = UINT_MAX; - char const * ex1_msg = 0; - std::string z3_ex1_msg; - - int sz = m_sts.size(); - - cooperation_section section; - omp_set_num_threads(sz); - #pragma omp parallel for - for (int i = 0; i < sz; i++) { - init_task task("par_as_st"); - as_st & st = *(m_sts[i]); - try { - model_converter_ref tmp_mc; - assertion_set & s_copy = s_copies[i]; - st(s_copy, tmp_mc); - bool first = false; - #pragma omp critical (par_as_st) - { - if (finished_id == UINT_MAX) { - finished_id = i; - first = true; - } - } - if (first) { - mc = tmp_mc; - s_copy.copy(s); - for (int j = 0; j < sz; j++) { - if (i != j) - m_sts[j]->cancel(); - } - } - } - catch (strategy_exception & ex) { - if (i == 0) - ex1_msg = ex.msg(); - } - catch (z3_error & ex) { - throw ex; - } - catch (z3_exception & z3_ex) { - if (i == 0) - z3_ex1_msg = z3_ex.msg(); - } - } - - if (finished_id == UINT_MAX) { - mc = 0; - if (ex1_msg != 0) - throw strategy_exception(ex1_msg); - else - throw default_exception(z3_ex1_msg.c_str()); - } - } -}; - -as_st * par(unsigned num, as_st * const * sts) { - return alloc(par_as_st, num, sts); -} - -as_st * par(as_st * st1, as_st * st2) { - as_st * sts[2] = { st1, st2 }; - return par(2, sts); -} - -as_st * par(as_st * st1, as_st * st2, as_st * st3) { - as_st * sts[3] = { st1, st2, st3 }; - return par(3, sts); -} - -as_st * par(as_st * st1, as_st * st2, as_st * st3, as_st * st4) { - as_st * sts[4] = { st1, st2, st3, st4 }; - return par(4, sts); -} - -class par_or_as_st : public as_st { - ptr_vector m_stfs; - ptr_vector m_sts; - std::string m_exc_msg; - params_ref m_params; - - void dec_ref_sts() { - unsigned sz = m_sts.size(); - for (unsigned i = 0; i < sz; i++) { - as_st * st = m_sts[i]; - #pragma omp critical (as_st_cancel) - { - m_sts[i] = 0; - } - st->dec_ref(); - } - } - - void exec_seq(assertion_set & s, model_converter_ref & mc) { - for (unsigned i = 0; i < m_stfs.size(); i++) { - as_st_f & f = *m_stfs[i]; - as_st * new_st = f(s.m(), m_params); - new_st->inc_ref(); - #pragma omp critical (as_st_cancel) - { - m_sts[i] = new_st; - } - } - or_else_as_st(m_sts.size(), m_sts.c_ptr())(s, mc); - dec_ref_sts(); - } - -public: - par_or_as_st(unsigned num, as_st_f * const * stfs) { - m_stfs.append(num, stfs); - m_sts.resize(num, 0); - } - - virtual ~par_or_as_st() { - DEBUG_CODE({ - for (unsigned i = 0; i < m_sts.size(); i++) { - SASSERT(m_sts[i] == 0); - } - }); - std::for_each(m_stfs.begin(), m_stfs.end(), delete_proc()); - } - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - if (s.inconsistent()) { - mc = 0; - return; - } - - ast_manager & m = s.m(); - - if (omp_in_parallel()) { - exec_seq(s, mc); - return; - } - - ptr_buffer managers; - - unsigned num = m_stfs.size(); - for (unsigned i = 0; i < num; i++) { - SASSERT(!m.is_format_manager()); - managers.push_back(alloc(ast_manager, m.proof_mode())); - managers.back()->copy_families_plugins(m); // has to be the first operation on the new managers. - as_st_f & f = *m_stfs[i]; - ast_manager & m_i = *managers.back(); - as_st * new_st = f(m_i, m_params); - new_st->inc_ref(); - #pragma omp critical (as_st_cancel) - { - m_sts[i] = new_st; - } - } - - int sz = m_sts.size(); - unsigned finished_id = UINT_MAX; - bool got_z3_exc = false; - m_exc_msg = ""; - bool good_abort = false; - - #pragma omp parallel for - for (int i = 0; i < sz; i++) { -#ifdef _WINDOWS - DWORD_PTR am = (0x01 << (omp_get_thread_num() % omp_get_num_procs())); - SetThreadAffinityMask(GetCurrentThread(), am); -#endif - as_st & st = *(m_sts[i]); - ast_manager & s_m = *managers[i]; - ast_translation input_translator(m, s_m); - assertion_set * s_copy = s.translate(input_translator); - - try { - model_converter_ref tmp_mc; - st(*s_copy, tmp_mc); - - #pragma omp critical (par_or_as_st) - { - if (finished_id == UINT_MAX) // ... and we're the first! - finished_id = i; - } - - if (finished_id == static_cast(i)) { - good_abort = true; - for (int j = 0; j < sz; j++) { - if (i != j) - m_sts[j]->cancel(); - } - - ast_translation output_translator(s_m, m); - mc = (tmp_mc) ? tmp_mc->translate(output_translator) : 0; - - assertion_set * temp_set = s_copy->translate(output_translator); - temp_set->copy(s); - dealloc(temp_set); - } - } - catch (strategy_exception & ex) { - if (!good_abort) { - #pragma omp critical (par_or_as_st_ex) - { - m_exc_msg = ex.msg(); - got_z3_exc = false; - } - } - } - catch (z3_error & ex) { - throw ex; - } - catch (z3_exception & z3_ex) { - if (!good_abort) { - #pragma omp critical (par_or_as_st_ex) - { - m_exc_msg = z3_ex.msg(); - got_z3_exc = true; - } - } - } - catch (...) { - if (!good_abort) { - #pragma omp critical (par_or_as_st_ex) - { - m_exc_msg = "unidentified exception in parallel region."; - got_z3_exc = false; - } - } - } - - dealloc(s_copy); - } - - dec_ref_sts(); - - for (unsigned i = 0; i < num; i++) { - dealloc(managers[i]); - } - - if (finished_id == UINT_MAX) { - mc = 0; - if (got_z3_exc) - throw default_exception(m_exc_msg.c_str()); - else - throw strategy_exception(m_exc_msg.c_str()); - } - } - - virtual void cleanup() { - // Cleanup is invoked to free memory allocated by the strategy, - // but it must leave the strategy object in a usable state. - // par_or does not need a cleanup since it only has factories. - } - - virtual void set_cancel(bool f) { - for (unsigned i = 0; i < m_sts.size(); i++) - if (m_sts[i]) - m_sts[i]->set_cancel(f); - } - - virtual void updt_params(params_ref const & p) { - m_params = p; - } -}; - -as_st * par_or(ast_manager & m, unsigned num, as_st_f * const * stfs) { -#ifdef _Z3_BUILD_PARALLEL_SMT - return alloc(par_or_as_st, num, stfs); -#else - // If Z3 was not compiled using _Z3_BUILD_PARALLEL_SMT, then - // it is not safe to use par_or (symbol and big_num managers are not protected). - // We use par instead - ptr_buffer sts; - params_ref p; - for (unsigned i = 0; i < num; i++) - sts.push_back(stfs[i]->operator()(m, p)); - return par(num, sts.c_ptr()); -#endif -} - -class fail_as_st : public as_st { -public: - fail_as_st() {} - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - throw strategy_exception("failed"); - } - void cleanup() {} -}; - -as_st * fail() { - return alloc(fail_as_st); -} - -as_st * fail_if_not_decided(as_st * st) { - return and_then(st, cond(check_decided(), noop(), fail())); -} - -class fail_if_unsat_st : public as_st { -public: - fail_if_unsat_st() {} - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - TRACE("fail_if_unsat", s.display(tout);); - if (s.inconsistent()) - throw strategy_exception("failed: not unsat"); - } - void cleanup() {} -}; - -class fail_if_sat_st : public as_st { -public: - fail_if_sat_st() {} - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - TRACE("fail_if_sat", s.display(tout);); - if (s.size() == 0) - throw strategy_exception("failed: not sat"); - } - void cleanup() {} -}; - -as_st * fail_if_unsat() { - return alloc(fail_if_unsat_st); -} - -as_st * fail_if_sat() { - return alloc(fail_if_sat_st); -} - -struct fail_if_not_small_st : public assertion_set_strategy { - unsigned m_size; - fail_if_not_small_st(unsigned sz):m_size(sz) {} - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - TRACE("fail_if_not_small", tout << "fail_if_not_small: executing, s.num_exprs(): " << s.num_exprs() << ", threshold: " << m_size << "\n";); - if (s.num_exprs() >= m_size) { - TRACE("fail_if_not_small", tout << "fail_if_not_small: failed\n";); - throw strategy_exception("failed: not small"); - } - } - - virtual void cleanup() {} -}; - -as_st * fail_if_not_small(unsigned sz) { - return alloc(fail_if_not_small_st, sz); -} - -struct fail_if_not_small_set_st : public assertion_set_strategy { - unsigned m_size; - fail_if_not_small_set_st(unsigned sz):m_size(sz) {} - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - TRACE("fail_if_not_small_set", tout << "fail_if_not_small: executing, s.size(): " << s.size() << ", threshold: " << m_size << "\n";); - if (s.size() >= m_size) { - TRACE("fail_if_not_small_set", tout << "fail_if_not_small: failed\n";); - throw strategy_exception("failed: not small"); - } - } - - virtual void cleanup() {} -}; - -as_st * fail_if_not_small_set(unsigned sz) { - return alloc(fail_if_not_small_set_st, sz); -} - -class round_robin_as_st : public composite_as_st { - unsigned m_start_timeout; - unsigned m_end_timeout; - unsigned m_delta_timeout; -public: - round_robin_as_st(unsigned num, as_st * const * sts, unsigned start, unsigned end, unsigned delta): - composite_as_st(num, sts), - m_start_timeout(start), - m_end_timeout(end), - m_delta_timeout(delta) {} - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - mc = 0; - if (s.inconsistent()) - return; - assertion_set orig_s(s.m()); - s.copy(orig_s); - unsigned timeout = m_start_timeout; - while (true) { - unsigned sz = m_sts.size(); - unsigned i; - for (i = 0; i < sz; i++) { - checkpoint(); - as_st & st = *(m_sts[i]); - cancel_eh eh(st); - { - scoped_timer timer(timeout, &eh); - mc = 0; - try { - st(s, mc); - return; - } - catch (strategy_exception & ex) { - parent_reset_cancel(st); - mc = 0; - if (i == sz - 1 && timeout + m_delta_timeout > m_end_timeout) - throw ex; // last strategy in the last round - s.reset(); - orig_s.copy(s); - } - } - } - timeout += m_delta_timeout; - } - } -}; - -as_st * round_robin(unsigned num, as_st * const * sts, unsigned start, unsigned end, unsigned delta) { - return alloc(round_robin_as_st, num, sts, start, end, delta); -} - -as_st * round_robin(as_st * st1, as_st * st2, unsigned start, unsigned end, unsigned delta) { - as_st * sts[2] = { st1, st2 }; - return round_robin(2, sts, start, end, delta); -} - -as_st * round_robin(as_st * st1, as_st * st2, as_st * st3, unsigned start, unsigned end, unsigned delta) { - as_st * sts[3] = { st1, st2, st3 }; - return round_robin(3, sts, start, end, delta); -} - -as_st * round_robin(as_st * st1, as_st * st2, as_st * st3, as_st * st4, unsigned start, unsigned end, unsigned delta) { - as_st * sts[4] = { st1, st2, st3, st4 }; - return round_robin(4, sts, start, end, delta); -} - -wrapper_as_st::~wrapper_as_st() { - as_st * d = m_st; - #pragma omp critical (as_st_cancel) - { - m_st = 0; - } - d->dec_ref(); -} - -class try_for_as_st : public wrapper_as_st { - unsigned m_timeout; -public: - try_for_as_st(as_st * s, unsigned t):wrapper_as_st(s), m_timeout(t) {} - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - cancel_eh eh(*m_st); - { - // Warning: scoped_timer is not thread safe in Linux. - scoped_timer timer(m_timeout, &eh); - wrapper_as_st::operator()(s, mc); - } - } -}; - -as_st * try_for(as_st * st, unsigned msecs) { - return alloc(try_for_as_st, st, msecs); -} - -class cleanup_as_st : public wrapper_as_st { -public: - cleanup_as_st(as_st * s):wrapper_as_st(s) {} - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - try { - wrapper_as_st::operator()(s, mc); - wrapper_as_st::cleanup(); - } - catch (strategy_exception & ex) { - wrapper_as_st::cleanup(); - throw ex; - } - } -}; - -as_st * clean(as_st * st) { - return alloc(cleanup_as_st, st); -} - -class using_params_as_st : public wrapper_as_st { - params_ref m_params; -public: - using_params_as_st(as_st * s, params_ref const & p):wrapper_as_st(s), m_params(p) { - s->updt_params(p); - } - - virtual void updt_params(params_ref const & p) { - TRACE("using_params", - tout << "before p: " << p << "\n"; - tout << "m_params: " << m_params << "\n"; - ;); - - params_ref new_p = p; - new_p.append(m_params); - wrapper_as_st::updt_params(new_p); - - TRACE("using_params", - tout << "after p: " << p << "\n"; - tout << "m_params: " << m_params << "\n"; - tout << "new_p: " << new_p << "\n";); - } -}; - -as_st * using_params(as_st * st, params_ref const & p) { - return alloc(using_params_as_st, st, p); -} - -/** - \brief For debugging purposes: display model converter in the trace. -*/ -class trace_mc_as_st : public wrapper_as_st { -public: - trace_mc_as_st(as_st * s):wrapper_as_st(s) { - } - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - wrapper_as_st::operator()(s, mc); - TRACE("trace_mc", tout << "trace_mc...\n"; if (mc) mc->display(tout);); - } -}; - -as_st * trace_mc(as_st * st) { - return alloc(trace_mc_as_st, st); -} - -class repeat_as_st : public wrapper_as_st { - unsigned m_max; - volatile bool m_cancel; - - void checkpoint() { - if (m_cancel) - throw strategy_exception(STE_CANCELED_MSG); - } - -public: - repeat_as_st(as_st * s, unsigned max):wrapper_as_st(s), m_max(max), m_cancel(false) { - } - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - mc = 0; - if (s.inconsistent()) - return; - unsigned counter = 0; - while (true) { - checkpoint(); - - assertion_set orig_s(s.m()); - s.copy(orig_s); - - model_converter_ref mc1; - try { - (*m_st)(s, mc1); - } - catch (strategy_exception & ex) { - mc = 0; - throw ex; - } - - mc = concat(mc.get(), mc1.get()); - counter++; - if (counter >= m_max) - return; - if (is_equal(orig_s, s)) - return; - } - } - - virtual void set_cancel(bool f) { - m_cancel = f; - wrapper_as_st::set_cancel(f); - } -}; - -as_st * repeat(as_st * st, unsigned max) { - return alloc(repeat_as_st, st, max); -} - -class noop_as_st : public assertion_set_strategy { -public: - virtual void set_cancel(bool f) {} - virtual void operator()(assertion_set & s, model_converter_ref & mc) {} - virtual void cleanup() {} -}; - -as_st * noop() { - return alloc(noop_as_st); -} - -MK_ST_EXCEPTION(check_is_sat_exception); -MK_ST_EXCEPTION(check_is_unsat_exception); - -class filter_is_sat_st : public wrapper_as_st { - bool const& m_unless_condition; -public: - filter_is_sat_st(as_st* st, bool const& unless_condition): - wrapper_as_st(st), m_unless_condition(unless_condition) {} - virtual ~filter_is_sat_st() {} - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - TRACE("filter_is_sat_bug", tout << "cond: " << m_unless_condition << "\n"; s.display(tout); mc->display(tout);); - wrapper_as_st::operator()(s, mc); - if (!m_unless_condition && (s.size() > 0 || s.inconsistent())) { - throw check_is_sat_exception("Solver did not establish satisfiability"); - } - } -}; - -as_st * filter_is_sat(as_st* st, bool const& unless_condition) { - return alloc(filter_is_sat_st, st, unless_condition); -} - - -class filter_is_unsat_st : public wrapper_as_st { - bool const& m_unless_condition; -public: - filter_is_unsat_st(as_st* st, bool const& unless_condition): - wrapper_as_st(st), m_unless_condition(unless_condition) {} - virtual ~filter_is_unsat_st() {} - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - wrapper_as_st::operator()(s, mc); - if (!m_unless_condition && !s.inconsistent()) { - throw check_is_unsat_exception("Solver did not establish unsatisfiability"); - } - } -}; - -as_st * filter_is_unsat(as_st* st, bool const& unless_condition) { - return alloc(filter_is_unsat_st, st, unless_condition); -} - - - -class cond_as_st : public as_st { -protected: - as_test * m_cond; - as_st * m_then; - as_st * m_else; - volatile bool m_cancel; -public: - cond_as_st(as_test * c, as_st * t, as_st * e):m_cond(c), m_then(t), m_else(e), m_cancel(false) { - SASSERT(c); SASSERT(t); SASSERT(e); - c->inc_ref(); - t->inc_ref(); - e->inc_ref(); - } - - virtual ~cond_as_st() { - as_st * d1 = m_then; - as_st * d2 = m_else; - #pragma omp critical (as_st_cancel) - { - m_then = 0; - m_else = 0; - } - m_cond->dec_ref(); - d1->dec_ref(); - d2->dec_ref(); - } - - virtual void updt_params(params_ref const & p) { - m_then->updt_params(p); - m_else->updt_params(p); - } - - virtual void collect_param_descrs(param_descrs & r) { - m_then->collect_param_descrs(r); - m_else->collect_param_descrs(r); - } - - virtual void collect_statistics(statistics & s) const { - m_then->collect_statistics(s); - m_else->collect_statistics(s); - } - - virtual void reset_statistics() { - m_then->reset_statistics(); - m_else->reset_statistics(); - } - - virtual void cleanup() { - m_then->cleanup(); - m_else->cleanup(); - } - - virtual void reset() { - m_then->reset(); - m_else->reset(); - } - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - if (s.inconsistent()) - return; - assertion_set orig_s(s.m()); - s.copy(orig_s); - bool c = (*m_cond)(s); - if (m_cancel) - throw strategy_exception(STE_CANCELED_MSG); - if (c) - (*m_then)(s, mc); - else - (*m_else)(s, mc); - } - - virtual void set_front_end_params(front_end_params & p) { - m_then->set_front_end_params(p); - m_else->set_front_end_params(p); - } - - virtual void set_logic(symbol const & l) { - m_then->set_logic(l); - m_else->set_logic(l); - } - - virtual void set_progress_callback(progress_callback * callback) { - m_then->set_progress_callback(callback); - m_else->set_progress_callback(callback); - } - -protected: - virtual void set_cancel(bool f) { - m_cancel = f; - if (m_then) - m_then->set_cancel(f); - if (m_else) - m_else->set_cancel(f); - } -}; - - -as_st * cond(as_test * c, as_st * t, as_st * e) { - return alloc(cond_as_st, c, t, e); -} - -struct check_mem_test : public as_test { - unsigned m_limit; - check_mem_test(unsigned l):m_limit(l) {} - virtual bool operator()(assertion_set const & s) const { - return memory::get_allocation_size() < m_limit; - } -}; - -as_test * check_mem(unsigned l) { return alloc(check_mem_test, l); } - -struct check_as_size_test : public as_test { - unsigned m_limit; - check_as_size_test(unsigned l):m_limit(l) {} - virtual bool operator()(assertion_set const & s) const { return s.num_exprs() < m_limit; } -}; - -as_test * check_as_size(unsigned l) { return alloc(check_as_size_test, l); } - -struct check_decided_test : public as_test { - check_decided_test() {} - virtual bool operator()(assertion_set const & s) const { return s.size()==0 || s.inconsistent(); } -}; - -as_test * check_decided() { return alloc(check_decided_test); } - -/** - \brief Execute strategy st on the given assertion set. -*/ -void exec(as_st * st, assertion_set & s, model_converter_ref & mc) { - st->reset_statistics(); - st->reset_cancel(); - try { - (*st)(s, mc); - st->cleanup(); - } - catch (strategy_exception & ex) { - IF_VERBOSE(ST_VERBOSITY_LVL, verbose_stream() << "(strategy-exception \"" << escaped(ex.msg()) << "\")" << std::endl;); - st->cleanup(); - throw ex; - } -} - -/** - \brief Use strategy st to check wether the assertion set s is satisfiable or not. - If result == l_true and model generation is enabled, then the model is stored in md. - If result == l_false and proof generation is enabled, then the proof is stored in pr. - If result == l_undef, the reason for failure is stored in reason_unknown. -*/ -lbool check_sat(as_st * st, assertion_set & s, model_ref & md, proof_ref & pr, std::string & reason_unknown) { - ast_manager & m = s.m(); - model_converter_ref mc; - try { - exec(st, s, mc); - } - catch (strategy_exception & ex) { - reason_unknown = ex.msg(); - return l_undef; - } - if (s.size() == 0) { - if (mc) { - TRACE("check_sat_model", tout << "model-converter:\n"; mc->display(tout);); - md = alloc(model, m); - (*mc)(md); - TRACE("check_sat_model", tout << "model:\n"; model_v2_pp(tout, *md);); - } - return l_true; - } - if (s.size() == 1 && m.is_false(s.form(0))) { - pr = s.pr(0); - return l_false; - } - if (mc) { - md = alloc(model, m); - (*mc)(md); - } - reason_unknown = "incomplete"; - return l_undef; -} diff --git a/src/assertion_set/assertion_set_strategy.h b/src/assertion_set/assertion_set_strategy.h deleted file mode 100644 index 0b02fad49..000000000 --- a/src/assertion_set/assertion_set_strategy.h +++ /dev/null @@ -1,223 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - assertion_set_strategy.h - -Abstract: - - Abstract strategy for assertion sets, and simple combinators. - -Author: - - Leonardo (leonardo) 2011-05-17 - -Notes: - ---*/ -#ifndef _AS_STRATEGY_H_ -#define _AS_STRATEGY_H_ - -#include"params.h" -#include"assertion_set.h" -#include"model_converter.h" -#include"statistics.h" -#include"strategy_exception.h" -#include"lbool.h" -#include"assertion_set_util.h" - -struct front_end_params; - -class progress_callback; - -// minimum verbosity level for strategies -#define ST_VERBOSITY_LVL 10 - -class as_st_report { - struct imp; - imp * m_imp; -public: - as_st_report(char const * id, assertion_set & s); - ~as_st_report(); -}; - -void report_st_progress(char const * id, unsigned val); - -/** - \brief Abstract assertion-set strategy. -*/ -class assertion_set_strategy { - unsigned m_ref_count; -public: - assertion_set_strategy():m_ref_count(0) {} - virtual ~assertion_set_strategy() {} - void inc_ref() { m_ref_count++; } - void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); } - virtual void updt_params(params_ref const & p) {} - virtual void collect_param_descrs(param_descrs & r) {} - void cancel(); - void reset_cancel(); - virtual void set_cancel(bool f) {} - virtual void operator()(assertion_set & s, model_converter_ref & mc) = 0; - virtual void collect_statistics(statistics & st) const {} - virtual void reset_statistics() {} - virtual void cleanup() = 0; - virtual void reset() { cleanup(); } - // for backward compatibility - virtual void set_front_end_params(front_end_params & p) {} - virtual void set_logic(symbol const & l) {} - virtual void set_progress_callback(progress_callback * callback) {} -}; - -bool is_equal(assertion_set const & s1, assertion_set const & s2); - -// dummy for using ref_vector -struct assertion_set_strategy_context { - static void inc_ref(assertion_set_strategy * st) { st->inc_ref(); } - static void dec_ref(assertion_set_strategy * st) { st->dec_ref(); } -}; - -typedef assertion_set_strategy as_st; -typedef assertion_set_strategy_context as_st_ctx; - -typedef ref as_st_ref; -typedef ref_vector as_st_ref_vector; -typedef ref_buffer as_st_ref_buffer; - -as_st * and_then(unsigned num, as_st * const * sts); -as_st * and_then(as_st * st1, as_st * st2); -as_st * and_then(as_st * st1, as_st * st2, as_st * st3); -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4); -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5); -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6); -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7); -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8); -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8, as_st * st9); -as_st * and_then(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8, as_st * st9, as_st * st10); - -as_st * or_else(unsigned num, as_st * const * sts); -as_st * or_else(as_st * st1, as_st * st2); -as_st * or_else(as_st * st1, as_st * st2, as_st * st3); -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4); -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5); -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6); -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7); -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8); -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8, as_st * st9); -as_st * or_else(as_st * st1, as_st * st2, as_st * st3, as_st * st4, as_st * st5, as_st * st6, as_st * st7, as_st * st8, as_st * st9, as_st * st10); - -as_st * par(unsigned num, as_st * const * sts); -as_st * par(as_st * st1, as_st * st2); -as_st * par(as_st * st1, as_st * st2, as_st * st3); -as_st * par(as_st * st1, as_st * st2, as_st * st3, as_st * st4); - -as_st * round_robin(unsigned num, as_st * const * sts, unsigned start, unsigned end, unsigned delta); -as_st * round_robin(as_st * st1, as_st * st2, unsigned start, unsigned end, unsigned delta); -as_st * round_robin(as_st * st1, as_st * st2, as_st * st3, unsigned start, unsigned end, unsigned delta); -as_st * round_robin(as_st * st1, as_st * st2, as_st * st3, as_st * st4, unsigned start, unsigned end, unsigned delta); - -as_st * try_for(as_st * st, unsigned msecs); -as_st * clean(as_st * st); -as_st * using_params(as_st * st, params_ref const & p); -as_st * noop(); -as_st * trace_mc(as_st * st); - -as_st * filter_is_sat(as_st* st, bool const& unless_condition); -as_st * filter_is_unsat(as_st* st, bool const& unless_condition); - -as_st * mk_report_verbose_st(char const* msg, unsigned lvl); - -as_st * repeat(as_st * st, unsigned max = UINT_MAX); - -class wrapper_as_st : public as_st { -protected: - as_st * m_st; -public: - wrapper_as_st(as_st * s): m_st(s) { SASSERT(s); s->inc_ref(); } - virtual ~wrapper_as_st(); - - virtual void operator()(assertion_set& s, model_converter_ref& mc) { (*m_st)(s, mc); } - virtual void cleanup(void) { m_st->cleanup(); } - virtual void collect_statistics(statistics & st) const { m_st->collect_statistics(st); } - virtual void reset_statistics() { m_st->reset_statistics(); } - virtual void set_front_end_params(front_end_params & p) { m_st->set_front_end_params(p); } - virtual void updt_params(params_ref const & p) { m_st->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { m_st->collect_param_descrs(r); } - virtual void reset() { m_st->reset(); } - virtual void set_logic(symbol const& l) { m_st->set_logic(l); } - virtual void set_progress_callback(progress_callback * callback) { m_st->set_progress_callback(callback); } - -protected: - virtual void set_cancel(bool f) { if (m_st) m_st->set_cancel(f); } -}; - - -class as_test { - unsigned m_ref_count; -public: - as_test():m_ref_count(0) {} - void inc_ref() { m_ref_count++; } - void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); } - virtual bool operator()(assertion_set const & s) const = 0; -}; - -as_test * check_mem(unsigned l); -as_test * check_as_size(unsigned l); -as_test * check_decided(); -as_st * cond(as_test * c, as_st * t, as_st * e); - -void exec(as_st * st, assertion_set & s, model_converter_ref & mc); -lbool check_sat(as_st * st, assertion_set & s, model_ref & md, proof_ref & pr, std::string & reason_unknown); - -class assertion_set_strategy_factory { -public: - virtual ~assertion_set_strategy_factory() {} - virtual as_st * operator()(ast_manager & m, params_ref const & p) = 0; -}; - -typedef assertion_set_strategy_factory as_st_f; - -as_st * fail(); -as_st * fail_if_not_decided(as_st * st); -as_st * fail_if_sat(); -as_st * fail_if_unsat(); -as_st * fail_if_not_small(unsigned sz); -as_st * fail_if_not_small_set(unsigned sz); - -#define MK_FAIL_IF(NAME, TEST, MSG) \ -class NAME ## _st : public assertion_set_strategy { \ -public: \ - virtual void operator()(assertion_set & s, model_converter_ref & mc) { if (TEST) throw strategy_exception(MSG); } \ - virtual void cleanup() {} \ -}; \ -inline as_st * NAME() { return alloc(NAME ## _st); } - -as_st * par_or(ast_manager & m, unsigned num, as_st_f * const * stfs); - -#define MK_ST_FACTORY(NAME, CODE) \ -class NAME : public assertion_set_strategy_factory { \ -public: \ - virtual ~NAME() {} \ - virtual as_st * operator()(ast_manager & m, params_ref const & p) { CODE } \ -}; - -#define MK_SIMPLE_ST_FACTORY(NAME, ST) MK_ST_FACTORY(NAME, return ST;) - -struct is_qfbv_test : public as_test { - virtual bool operator()(assertion_set const & s) const { return is_qfbv(s); } -}; - -struct is_qflia_test : public as_test { - virtual bool operator()(assertion_set const & s) const { return is_qflia(s); } -}; - -struct is_qflra_test : public as_test { - virtual bool operator()(assertion_set const & s) const { return is_qflra(s); } -}; - -inline as_test * is_qfbv() { return alloc(is_qfbv_test); } -inline as_test * is_qflia() { return alloc(is_qflia_test); } -inline as_test * is_qflra() { return alloc(is_qflra_test); } - -#endif diff --git a/src/assertion_set/assertion_set_util.cpp b/src/assertion_set/assertion_set_util.cpp deleted file mode 100644 index c596b53c4..000000000 --- a/src/assertion_set/assertion_set_util.cpp +++ /dev/null @@ -1,220 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - assertion_set_util.cpp - -Abstract: - - Assertion set goodies - -Author: - - Leonardo de Moura (leonardo) 2011-04-28 - -Revision History: - ---*/ -#include"assertion_set_util.h" -#include"well_sorted.h" -#include"for_each_expr.h" -#include"bv_decl_plugin.h" -#include"arith_decl_plugin.h" - -void as_shared_occs::operator()(assertion_set const & s) { - m_occs.reset(); - shared_occs_mark visited; - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - expr * t = s.form(i); - m_occs(t, visited); - } -} - -bool is_well_sorted(assertion_set const & s) { - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - expr * t = s.form(i); - if (!is_well_sorted(s.m(), t)) - return false; - } - return true; -} - -struct is_non_propositional { - struct found {}; - ast_manager & m; - - is_non_propositional(ast_manager & _m):m(_m) {} - void operator()(var *) { throw found(); } - void operator()(quantifier *) { throw found(); } - void operator()(app * n) { - if (!m.is_bool(n)) - throw found(); - - family_id fid = n->get_family_id(); - if (fid == m.get_basic_family_id()) - return; - - if (is_uninterp_const(n)) - return; - - throw found(); - } -}; - -struct is_non_qfbv { - struct found {}; - ast_manager & m; - bv_util u; - - is_non_qfbv(ast_manager & _m):m(_m), u(m) {} - - void operator()(var *) { throw found(); } - - void operator()(quantifier *) { throw found(); } - - void operator()(app * n) { - if (!m.is_bool(n) && !u.is_bv(n)) - throw found(); - family_id fid = n->get_family_id(); - if (fid == m.get_basic_family_id()) - return; - if (fid == u.get_family_id()) - return; - if (is_uninterp_const(n)) - return; - - throw found(); - } -}; - -bool is_propositional(assertion_set const & s) { - return !test(s); -} - -bool is_qfbv(assertion_set const & s) { - return !test(s); -} - -struct is_non_qflira { - struct found {}; - ast_manager & m; - arith_util u; - bool m_int; - bool m_real; - - is_non_qflira(ast_manager & _m, bool _int, bool _real):m(_m), u(m), m_int(_int), m_real(_real) {} - - void operator()(var *) { throw found(); } - - void operator()(quantifier *) { throw found(); } - - bool compatible_sort(app * n) const { - if (m.is_bool(n)) - return true; - if (m_int && u.is_int(n)) - return true; - if (m_real && u.is_real(n)) - return true; - return false; - } - - void operator()(app * n) { - if (!compatible_sort(n)) - throw found(); - family_id fid = n->get_family_id(); - if (fid == m.get_basic_family_id()) - return; - if (fid == u.get_family_id()) { - switch (n->get_decl_kind()) { - case OP_LE: case OP_GE: case OP_LT: case OP_GT: - case OP_ADD: case OP_NUM: - return; - case OP_MUL: - if (n->get_num_args() != 2) - throw found(); - if (!u.is_numeral(n->get_arg(0))) - throw found(); - return; - case OP_TO_REAL: - if (!m_real) - throw found(); - break; - default: - throw found(); - } - return; - } - if (is_uninterp_const(n)) - return; - throw found(); - } -}; - -bool is_qflia(assertion_set const & s) { - is_non_qflira proc(s.m(), true, false); - return !test(s, proc); -} - -bool is_qflra(assertion_set const & s) { - is_non_qflira proc(s.m(), false, true); - return !test(s, proc); -} - -bool is_qflira(assertion_set const & s) { - is_non_qflira proc(s.m(), true, true); - return !test(s, proc); -} - -bool is_lp(assertion_set const & s) { - ast_manager & m = s.m(); - arith_util u(m); - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - expr * f = s.form(i); - bool sign = false; - while (m.is_not(f, f)) - sign = !sign; - if (m.is_eq(f) && !sign) { - if (m.get_sort(to_app(f)->get_arg(0))->get_family_id() != u.get_family_id()) - return false; - continue; - } - if (u.is_le(f) || u.is_ge(f) || u.is_lt(f) || u.is_gt(f)) - continue; - return false; - } - return true; -} - -bool is_ilp(assertion_set const & s) { - if (!is_qflia(s)) - return false; - if (has_term_ite(s)) - return false; - return is_lp(s); -} - -bool is_mip(assertion_set const & s) { - if (!is_qflira(s)) - return false; - if (has_term_ite(s)) - return false; - return is_lp(s); -} - -struct has_term_ite_proc { - struct found {}; - ast_manager & m; - has_term_ite_proc(ast_manager & _m):m(_m) {} - void operator()(var *) {} - void operator()(quantifier *) {} - void operator()(app * n) { if (m.is_term_ite(n)) throw found(); } -}; - -bool has_term_ite(assertion_set const & s) { - return test(s); -} - diff --git a/src/assertion_set/assertion_set_util.h b/src/assertion_set/assertion_set_util.h deleted file mode 100644 index 425b20707..000000000 --- a/src/assertion_set/assertion_set_util.h +++ /dev/null @@ -1,91 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - assertion_set_util.h - -Abstract: - - Assertion set goodies - -Author: - - Leonardo de Moura (leonardo) 2011-04-28 - -Revision History: - ---*/ -#ifndef _ASSERTION_SET_UTIL_H_ -#define _ASSERTION_SET_UTIL_H_ - -#include"assertion_set.h" -#include"shared_occs.h" - -/** - \brief Functor for computing the set of shared occurrences in an assertion set. - - It is essentially a wrapper for shared_occs functor. -*/ -class as_shared_occs { - shared_occs m_occs; -public: - as_shared_occs(ast_manager & m, bool track_atomic = false, bool visit_quantifiers = true, bool visit_patterns = false): - m_occs(m, track_atomic, visit_quantifiers, visit_patterns) { - } - void operator()(assertion_set const & s); - bool is_shared(expr * t) { return m_occs.is_shared(t); } - unsigned num_shared() const { return m_occs.num_shared(); } - void reset() { return m_occs.reset(); } - void cleanup() { return m_occs.cleanup(); } - void display(std::ostream & out, ast_manager & m) const { m_occs.display(out, m); } -}; - -bool is_well_sorted(assertion_set const & s); - -// Return true if the assertion set is propositional logic -bool is_propositional(assertion_set const & s); - -// Return true if the assertion set is in QF_BV -bool is_qfbv(assertion_set const & s); - -// Return true if the assertion set is in QF_LIA -bool is_qflia(assertion_set const & s); - -// Return true if the assertion set is in QF_LRA -bool is_qflra(assertion_set const & s); - -// Return true if the assertion set is in QF_LIRA -bool is_qflira(assertion_set const & s); - -// Return true if the assertion set is in ILP problem (that is QF_LIA without boolean structure) -bool is_ilp(assertion_set const & s); - -// Return true if the assertion set is in MIP problem (that is QF_LIRA without boolean structure) -bool is_mip(assertion_set const & s); - -bool has_term_ite(assertion_set const & s); - -inline bool is_decided(assertion_set const & s) { return s.size() == 0 || s.inconsistent(); } - -template -bool test(assertion_set const & s, Predicate & proc) { - expr_fast_mark1 visited; - try { - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) - quick_for_each_expr(proc, visited, s.form(i)); - } - catch (typename Predicate::found) { - return true; - } - return false; -} - -template -bool test(assertion_set const & s) { - Predicate proc(s.m()); - return test(s, proc); -} - -#endif diff --git a/src/assertion_set/der_strategy.cpp b/src/assertion_set/der_strategy.cpp deleted file mode 100644 index ba294f2ee..000000000 --- a/src/assertion_set/der_strategy.cpp +++ /dev/null @@ -1,94 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - der_strategy.cpp - -Abstract: - - DER strategy - -Author: - - Leonardo de Moura (leonardo) 2012-10-20 - ---*/ -#include"der_strategy.h" - -struct der_strategy::imp { - ast_manager & m_manager; - der_rewriter m_r; - - imp(ast_manager & m): - m_manager(m), - m_r(m) { - } - - ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { - m_r.set_cancel(f); - } - - void reset() { - m_r.reset(); - } - - void operator()(assertion_set & s) { - SASSERT(is_well_sorted(s)); - as_st_report report("der", s); - TRACE("before_der", s.display(tout);); - if (s.inconsistent()) - return; - expr_ref new_curr(m()); - proof_ref new_pr(m()); - unsigned size = s.size(); - for (unsigned idx = 0; idx < size; idx++) { - if (s.inconsistent()) - break; - expr * curr = s.form(idx); - m_r(curr, new_curr, new_pr); - if (m().proofs_enabled()) { - proof * pr = s.pr(idx); - new_pr = m().mk_modus_ponens(pr, new_pr); - } - s.update(idx, new_curr, new_pr); - } - s.elim_redundancies(); - TRACE("after_der", s.display(tout);); - SASSERT(is_well_sorted(s)); - } -}; - -der_strategy::der_strategy(ast_manager & m) { - m_imp = alloc(imp, m); -} - -der_strategy::~der_strategy() { - dealloc(m_imp); -} - -void der_strategy::operator()(assertion_set & s) { - m_imp->operator()(s); -} - -void der_strategy::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} - -void der_strategy::cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; - #pragma omp critical (as_st_cancel) - { - m_imp = 0; - } - dealloc(d); - d = alloc(imp, m); - #pragma omp critical (as_st_cancel) - { - m_imp = d; - } -} diff --git a/src/assertion_set/der_strategy.h b/src/assertion_set/der_strategy.h deleted file mode 100644 index ace90eb3c..000000000 --- a/src/assertion_set/der_strategy.h +++ /dev/null @@ -1,47 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - der_strategy.h - -Abstract: - - DER strategy - -Author: - - Leonardo de Moura (leonardo) 2012-10-20 - ---*/ -#ifndef _DER_STRATEGY_H_ -#define _DER_STRATEGY_H_ - -#include"der.h" -#include"assertion_set_strategy.h" - -// TODO: delete obsolete class -class der_strategy : public assertion_set_strategy { - struct imp; - imp * m_imp; -public: - der_strategy(ast_manager & m); - virtual ~der_strategy(); - - void operator()(assertion_set & s); - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - operator()(s); - mc = 0; - } - - virtual void cleanup(); - virtual void set_cancel(bool f); -}; - -inline as_st * mk_der(ast_manager & m) { - return alloc(der_strategy, m); -} - - -#endif diff --git a/src/assertion_set/elim_distinct.cpp b/src/assertion_set/elim_distinct.cpp deleted file mode 100644 index bf4502822..000000000 --- a/src/assertion_set/elim_distinct.cpp +++ /dev/null @@ -1,232 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - elim_distinct.cpp - -Abstract: - - Replace one distinct(t0, ..., tn) with (t0 = 0 and ... and tn = n) - when the sort of t0...tn is uninterpreted. - -Author: - - Leonardo de Moura (leonardo) 2011-04-28 - -Revision History: - ---*/ -#include"elim_distinct.h" -#include"assertion_set.h" -#include"model_converter.h" -#include"arith_decl_plugin.h" -#include"rewriter_def.h" -#include"critical_flet.h" - -struct elim_distinct::imp { - struct mc : public model_converter { - ast_ref_vector m_asts; - sort * m_usort; - obj_map m_inv_map; - public: - mc(ast_manager & m):m_asts(m) { - } - }; - - struct u2i_cfg : public default_rewriter_cfg { - arith_util m_autil; - ast_ref_vector m_asts; - sort * m_usort; - sort * m_int_sort; - obj_map m_f2f; - - ast_manager & m() const { return m_asts.get_manager(); } - - bool must_remap(func_decl * f) const { - if (f->get_range() == m_usort) - return true; - for (unsigned i = 0; i < f->get_arity(); i++) { - if (f->get_domain(i) == m_usort) - return true; - } - return false; - } - - sort * remap(sort * s) { - return (s == m_usort) ? m_int_sort : s; - } - - func_decl * remap(func_decl * f) { - ptr_buffer new_domain; - sort * new_range = remap(f->get_range()); - for (unsigned i = 0; i < f->get_arity(); i++) - new_domain.push_back(remap(f->get_domain(i))); - func_decl * new_f = m().mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), new_range); - m_asts.push_back(new_f); - m_asts.push_back(f); - m_f2f.insert(f, new_f); - return new_f; - } - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - result_pr = 0; - func_decl * new_f; - if (m_f2f.find(f, new_f)) { - result = m().mk_app(new_f, num, args); - return BR_DONE; - } - - if (!must_remap(f)) - return BR_FAILED; - - if (m().is_eq(f)) { - result = m().mk_eq(args[0], args[1]); - return BR_DONE; - } - - if (m().is_ite(f)) { - result = m().mk_ite(args[0], args[1], args[2]); - return BR_DONE; - } - - if (f->get_family_id() != null_family_id || f->get_info() != 0) { - throw elim_distinct_exception("uninterpreted sort is used in interpreted function symbol"); - } - - new_f = remap(f); - result = m().mk_app(new_f, num, args); - return BR_DONE; - } - - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, - expr * const * new_no_patterns, - expr_ref & result, - proof_ref & result_pr) { - throw elim_distinct_exception("elim-distinct tactic does not support quantifiers"); - } - - u2i_cfg(ast_manager & m, sort * u): - m_autil(m), - m_asts(m), - m_usort(u) { - m_asts.push_back(u); - m_int_sort = m_autil.mk_int(); - m_asts.push_back(m_int_sort); - } - }; - - class u2i : public rewriter_tpl { - u2i_cfg m_cfg; - public: - u2i(ast_manager & m, sort * u): - rewriter_tpl(m, false, m_cfg), - m_cfg(m, u) { - if (m.proofs_enabled()) - throw elim_distinct_exception("elim-distinct tactic does not support proof generation"); - } - arith_util & autil() { return cfg().m_autil; } - }; - - ast_manager & m_manager; - u2i * m_u2i; - - imp(ast_manager & m):m_manager(m), m_u2i(0) {} - ast_manager & m() const { return m_manager; } - - bool is_distinct(expr * t) { - if (!m().is_distinct(t)) - return false; - if (to_app(t)->get_num_args() == 0) - return false; - return m().is_uninterp(m().get_sort(to_app(t)->get_arg(0))); - } - - model_converter * operator()(assertion_set & s, app * d) { - if (d && !is_distinct(d)) - d = 0; - app * r = 0; - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - expr * curr = s.form(i); - if (curr == d) - break; - if (is_distinct(curr)) { - if (!r || to_app(curr)->get_num_args() > r->get_num_args()) - r = to_app(curr); - } - } - if (d != 0) - r = d; - if (r == 0) - return 0; - sort * u = m().get_sort(to_app(r)->get_arg(0)); - u2i conv(m(), u); - { - critical_flet l1(m_u2i, &conv); - expr_ref new_curr(m()); - for (unsigned i = 0; i < sz; i++) { - expr * curr = s.form(i); - if (curr == r) { - unsigned num = r->get_num_args(); - for (unsigned j = 0; j < num; j++) { - expr * arg = r->get_arg(j); - conv(arg, new_curr); - expr * eq = m().mk_eq(new_curr, conv.autil().mk_numeral(rational(j), true)); - s.assert_expr(eq); - } - new_curr = m().mk_true(); - } - else { - conv(curr, new_curr); - } - - s.update(i, new_curr); - } - } - - // TODO: create model converter - return 0; - } - - void cancel() { - // Remark: m_u2i is protected by the omp global critical section. - // If this is a performance problem, then replace critical_flet by a custom flet that uses a different - // section name - #pragma omp critical (critical_flet) - { - if (m_u2i) - m_u2i->cancel(); - } - } -}; - -template class rewriter_tpl; - -elim_distinct::elim_distinct(ast_manager & m) { - m_imp = alloc(imp, m); -} - -elim_distinct::~elim_distinct() { - dealloc(m_imp); -} - -model_converter * elim_distinct::operator()(assertion_set & s, app * d) { - return m_imp->operator()(s, d); -} - -void elim_distinct::cancel() { - m_imp->cancel(); -} - -void elim_distinct::reset() { - cleanup(); -} - -void elim_distinct::cleanup() { - ast_manager & m = m_imp->m(); - dealloc(m_imp); - m_imp = alloc(imp, m); -} diff --git a/src/assertion_set/elim_distinct.h b/src/assertion_set/elim_distinct.h deleted file mode 100644 index 2e04997bd..000000000 --- a/src/assertion_set/elim_distinct.h +++ /dev/null @@ -1,54 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - elim_distinct.h - -Abstract: - - Replace one distinct(t0, ..., tn) with (t0 = 0 and ... and tn = n) - when the sort of t0...tn is uninterpreted. - -Author: - - Leonardo de Moura (leonardo) 2011-04-28 - -Revision History: - ---*/ -#ifndef _ELIM_DISTINCT_H_ -#define _ELIM_DISTINCT_H_ - -#include"assertion_set.h" - -class model_converter; -class ast_manager; -class assertion_set; - -class elim_distinct_exception : public default_exception { -public: - elim_distinct_exception(char const * msg):default_exception(msg) {} -}; - -class elim_distinct { - struct imp; - imp * m_imp; -public: - elim_distinct(ast_manager & m); - ~elim_distinct(); - - /** - \brief It throws an elim_distinct_exception if the strategy failed. - If d == 0, then search for the biggest distinct(t0, ..., tn) in the assertion set. - if d != 0, then succeed only if d is in the assertion set. - */ - model_converter * operator()(assertion_set & s, app * d); - - void cancel(); - - void reset(); - void cleanup(); -}; - -#endif diff --git a/src/assertion_set/elim_var_model_converter.cpp b/src/assertion_set/elim_var_model_converter.cpp deleted file mode 100644 index 3acc5918a..000000000 --- a/src/assertion_set/elim_var_model_converter.cpp +++ /dev/null @@ -1,120 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - elim_var_model_converter.cpp - -Abstract: - - Model converter that introduces eliminated variables in a model. - -Author: - - Leonardo (leonardo) 2011-05-05 - -Notes: - ---*/ -#include"elim_var_model_converter.h" -#include"model_evaluator.h" -#include"ast_smt2_pp.h" -#include"model_v2_pp.h" -#include"ast_pp.h" - -elim_var_model_converter::~elim_var_model_converter() { -} - -struct elim_var_model_converter::set_eval { - elim_var_model_converter * m_owner; - model_evaluator * m_old; - set_eval(elim_var_model_converter * owner, model_evaluator * ev) { - m_owner = owner; - m_old = owner->m_eval; - #pragma omp critical (elim_var_model_converter) - { - owner->m_eval = ev; - } - } - ~set_eval() { - #pragma omp critical (elim_var_model_converter) - { - m_owner->m_eval = m_old; - } - } - -}; - -static void display_decls_info(std::ostream & out, model_ref & md) { - ast_manager & m = md->get_manager(); - unsigned sz = md->get_num_decls(); - for (unsigned i = 0; i < sz; i++) { - func_decl * d = md->get_decl(i); - out << d->get_name(); - out << " ("; - for (unsigned j = 0; j < d->get_arity(); j++) - out << mk_pp(d->get_domain(j), m); - out << mk_pp(d->get_range(), m); - out << ") "; - if (d->get_info()) - out << *(d->get_info()); - out << " :id " << d->get_id() << "\n"; - } -} - -void elim_var_model_converter::operator()(model_ref & md) { - TRACE("elim_var_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); - model_evaluator ev(*(md.get())); - ev.set_model_completion(true); - expr_ref val(m()); - { - set_eval setter(this, &ev); - unsigned i = m_vars.size(); - while (i > 0) { - --i; - expr * def = m_defs.get(i); - ev(def, val); - TRACE("elim_var_mc", tout << m_vars.get(i)->get_name() << " ->\n" << mk_ismt2_pp(def, m()) << "\n==>\n" << mk_ismt2_pp(val, m()) << "\n";); - func_decl * f = m_vars.get(i); - unsigned arity = f->get_arity(); - if (arity == 0) { - md->register_decl(f, val); - } - else { - func_interp * new_fi = alloc(func_interp, m(), arity); - new_fi->set_else(val); - md->register_decl(f, new_fi); - } - } - } - TRACE("elim_var_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); -} - -void elim_var_model_converter::cancel() { - #pragma omp critical (elim_var_model_converter) - { - if (m_eval) - m_eval->cancel(); - } -} - -void elim_var_model_converter::display(std::ostream & out) { - ast_manager & m = m_vars.get_manager(); - out << "(elim-var-model-converter"; - for (unsigned i = 0; i < m_vars.size(); i++) { - out << "\n (" << m_vars.get(i)->get_name() << " "; - unsigned indent = m_vars.get(i)->get_name().size() + 4; - out << mk_ismt2_pp(m_defs.get(i), m, indent) << ")"; - } - out << ")" << std::endl; -} - -model_converter * elim_var_model_converter::translate(ast_translation & translator) { - elim_var_model_converter * res = alloc(elim_var_model_converter, translator.to()); - for (unsigned i = 0; i < m_vars.size(); i++) - res->m_vars.push_back(translator(m_vars[i].get())); - for (unsigned i = 0; i < m_defs.size(); i++) - res->m_defs.push_back(translator(m_defs[i].get())); - // m_eval is a transient object. So, it doesn't need to be translated. - return res; -} diff --git a/src/assertion_set/elim_var_model_converter.h b/src/assertion_set/elim_var_model_converter.h deleted file mode 100644 index 7efdd9224..000000000 --- a/src/assertion_set/elim_var_model_converter.h +++ /dev/null @@ -1,56 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - elim_var_model_converter.h - -Abstract: - - Model converter that introduces eliminated variables in a model. - -Author: - - Leonardo (leonardo) 2011-05-05 - -Notes: - ---*/ -#ifndef _ELIM_VAR_MODEL_CONVERTER_H_ -#define _ELIM_VAR_MODEL_CONVERTER_H_ - -#include"ast.h" -#include"model_converter.h" - -class model_evaluator; - -class elim_var_model_converter : public model_converter { - func_decl_ref_vector m_vars; - expr_ref_vector m_defs; - model_evaluator * m_eval; - struct set_eval; -public: - elim_var_model_converter(ast_manager & m):m_vars(m), m_defs(m), m_eval(0) { - } - - virtual ~elim_var_model_converter(); - - ast_manager & m() const { return m_vars.get_manager(); } - - virtual void operator()(model_ref & md); - - virtual void cancel(); - - virtual void display(std::ostream & out); - - // register a variable that was eliminated - void insert(func_decl * v, expr * def) { - m_vars.push_back(v); - m_defs.push_back(def); - } - - virtual model_converter * translate(ast_translation & translator); -}; - - -#endif diff --git a/src/assertion_set/gaussian_elim.cpp b/src/assertion_set/gaussian_elim.cpp deleted file mode 100644 index a3aa667f3..000000000 --- a/src/assertion_set/gaussian_elim.cpp +++ /dev/null @@ -1,775 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - gaussian_elim.cpp - -Abstract: - - (extended) Gaussian elimination for assertion sets. - It also supports other theories besides arithmetic. - -Author: - - Leonardo (leonardo) 2011-04-29 - -Notes: - ---*/ -#include"gaussian_elim.h" -#include"ast.h" -#include"expr_replacer.h" -#include"model_converter.h" -#include"assertion_set.h" -#include"ast_smt2_pp.h" -#include"elim_var_model_converter.h" -#include"occurs.h" -#include"cooperate.h" -#include"assertion_set_util.h" - -struct gaussian_elim::imp { - ast_manager & m_manager; - expr_replacer * m_r; - bool m_r_owner; - arith_util m_a_util; - obj_map m_num_occs; - unsigned m_num_steps; - unsigned m_num_eliminated_vars; - bool m_produce_models; - bool m_theory_solver; - bool m_ite_solver; - unsigned m_max_occs; - - void updt_params(params_ref const & p) { - m_produce_models = p.get_bool(":produce-models", false); - m_ite_solver = p.get_bool(":ite-solver", true); - m_theory_solver = p.get_bool(":theory-solver", true); - m_max_occs = p.get_uint(":gaussian-max-occs", UINT_MAX); - } - - typedef elim_var_model_converter gmc; - - expr_substitution m_subst; - expr_substitution m_norm_subst; - expr_sparse_mark m_candidate_vars; - expr_sparse_mark m_candidate_set; - ptr_vector m_candidates; - ptr_vector m_vars; - ptr_vector m_ordered_vars; - volatile bool m_cancel; - - imp(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner): - m_manager(m), - m_r(r), - m_r_owner(r == 0 || owner), - m_a_util(m), - m_num_steps(0), - m_num_eliminated_vars(0), - m_subst(m), - m_norm_subst(m), - m_cancel(false) { - updt_params(p); - if (m_r == 0) - m_r = mk_default_expr_replacer(m); - } - - ~imp() { - if (m_r_owner) - dealloc(m_r); - } - - ast_manager & m() const { return m_manager; } - - bool check_occs(expr * t) const { - if (m_max_occs == UINT_MAX) - return true; - unsigned num = 0; - m_num_occs.find(t, num); - TRACE("gaussian_check_occs", tout << mk_ismt2_pp(t, m_manager) << " num_occs: " << num << " max: " << m_max_occs << "\n";); - return num <= m_max_occs; - } - - // Use: (= x def) and (= def x) - bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) { - if (is_uninterp_const(lhs) && !m_candidate_vars.is_marked(lhs) && !occurs(lhs, rhs) && check_occs(lhs)) { - var = to_app(lhs); - def = rhs; - pr = 0; - return true; - } - else if (is_uninterp_const(rhs) && !m_candidate_vars.is_marked(rhs) && !occurs(rhs, lhs) && check_occs(rhs)) { - var = to_app(rhs); - def = lhs; - if (m_manager.proofs_enabled()) - pr = m().mk_commutativity(m().mk_eq(lhs, rhs)); - return true; - } - return false; - } - - // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2)) - bool solve_ite_core(app * ite, expr * lhs1, expr * rhs1, expr * lhs2, expr * rhs2, app_ref & var, expr_ref & def, proof_ref & pr) { - if (lhs1 != lhs2) - return false; - if (!is_uninterp_const(lhs1) || m_candidate_vars.is_marked(lhs1)) - return false; - if (occurs(lhs1, ite->get_arg(0)) || occurs(lhs1, rhs1) || occurs(lhs1, rhs2)) - return false; - if (!check_occs(lhs1)) - return false; - var = to_app(lhs1); - def = m().mk_ite(ite->get_arg(0), rhs1, rhs2); - - if (m().proofs_enabled()) - pr = m().mk_rewrite(ite, m().mk_eq(var, def)); - return true; - } - - // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2)) - bool solve_ite(app * ite, app_ref & var, expr_ref & def, proof_ref & pr) { - expr * t = ite->get_arg(1); - expr * e = ite->get_arg(2); - - if (!m().is_eq(t) || !m().is_eq(e)) - return false; - - expr * lhs1 = to_app(t)->get_arg(0); - expr * rhs1 = to_app(t)->get_arg(1); - expr * lhs2 = to_app(e)->get_arg(0); - expr * rhs2 = to_app(e)->get_arg(1); - - return - solve_ite_core(ite, lhs1, rhs1, lhs2, rhs2, var, def, pr) || - solve_ite_core(ite, rhs1, lhs1, lhs2, rhs2, var, def, pr) || - solve_ite_core(ite, lhs1, rhs1, rhs2, lhs2, var, def, pr) || - solve_ite_core(ite, rhs1, lhs1, rhs2, lhs2, var, def, pr); - } - - bool is_pos_literal(expr * n) { - return is_app(n) && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id; - } - - bool is_neg_literal(expr * n) { - if (m_manager.is_not(n)) - return is_pos_literal(to_app(n)->get_arg(0)); - return false; - } - -#if 0 - bool not_bool_eq(expr * f, app_ref & var, expr_ref & def, proof_ref & pr) { - if (!m().is_not(f)) - return false; - expr * eq = to_app(f)->get_arg(0); - if (!m().is_eq(f)) - return false; - - } -#endif - - /** - \brief Given t of the form (f s_0 ... s_n), - return true if x occurs in some s_j for j != i - */ - bool occurs_except(expr * x, app * t, unsigned i) { - unsigned num = t->get_num_args(); - for (unsigned j = 0; j < num; j++) { - if (i != j && occurs(x, t->get_arg(j))) - return true; - } - return false; - } - - bool solve_arith_core(app * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) { - SASSERT(m_a_util.is_add(lhs)); - bool is_int = m_a_util.is_int(lhs); - expr * a; - expr * v; - rational a_val; - unsigned num = lhs->get_num_args(); - unsigned i; - for (i = 0; i < num; i++) { - expr * arg = lhs->get_arg(i); - if (is_uninterp_const(arg) && !m_candidate_vars.is_marked(arg) && check_occs(arg) && !occurs(arg, rhs) && !occurs_except(arg, lhs, i)) { - a_val = rational(1); - v = arg; - break; - } - else if (m_a_util.is_mul(arg, a, v) && - is_uninterp_const(v) && !m_candidate_vars.is_marked(v) && - m_a_util.is_numeral(a, a_val) && - !a_val.is_zero() && - (!is_int || a_val.is_minus_one()) && - check_occs(v) && - !occurs(v, rhs) && - !occurs_except(v, lhs, i)) { - break; - } - } - if (i == num) - return false; - var = to_app(v); - expr_ref inv_a(m()); - if (!a_val.is_one()) { - inv_a = m_a_util.mk_numeral(rational(1)/a_val, is_int); - rhs = m_a_util.mk_mul(inv_a, rhs); - } - - ptr_buffer other_args; - for (unsigned j = 0; j < num; j++) { - if (i != j) { - if (inv_a) - other_args.push_back(m_a_util.mk_mul(inv_a, lhs->get_arg(j))); - else - other_args.push_back(lhs->get_arg(j)); - } - } - switch (other_args.size()) { - case 0: - def = rhs; - break; - case 1: - def = m_a_util.mk_sub(rhs, other_args[0]); - break; - default: - def = m_a_util.mk_sub(rhs, m_a_util.mk_add(other_args.size(), other_args.c_ptr())); - break; - } - if (m().proofs_enabled()) { - pr = m().mk_rewrite(eq, m().mk_eq(var, def)); - } - return true; - } - - bool solve_arith(expr * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) { - return - (m_a_util.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, var, def, pr)) || - (m_a_util.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, def, pr)); - } - - bool solve(expr * f, app_ref & var, expr_ref & def, proof_ref & pr) { - if (m().is_eq(f)) { - if (trivial_solve(to_app(f)->get_arg(0), to_app(f)->get_arg(1), var, def, pr)) - return true; - if (m_theory_solver) { - expr * lhs = to_app(f)->get_arg(0); - expr * rhs = to_app(f)->get_arg(1); - if (solve_arith(lhs, rhs, f, var, def, pr)) - return true; - } - return false; - } - - if (m().is_iff(f)) - return trivial_solve(to_app(f)->get_arg(0), to_app(f)->get_arg(1), var, def, pr); - -#if 0 - if (not_bool_eq(f, var, def, pr)) - return true; -#endif - - if (m_ite_solver && m().is_ite(f)) - return solve_ite(to_app(f), var, def, pr); - - if (is_pos_literal(f)) { - if (m_candidate_vars.is_marked(f)) - return false; - var = to_app(f); - def = m().mk_true(); - if (m().proofs_enabled()) { - // [rewrite]: (iff (iff l true) l) - // [symmetry T1]: (iff l (iff l true)) - pr = m().mk_rewrite(m().mk_eq(var, def), var); - pr = m().mk_symmetry(pr); - } - TRACE("gaussian_elim_bug2", tout << "eliminating: " << mk_ismt2_pp(f, m()) << "\n";); - return true; - } - - if (is_neg_literal(f)) { - var = to_app(to_app(f)->get_arg(0)); - if (m_candidate_vars.is_marked(var)) - return false; - def = m().mk_false(); - if (m().proofs_enabled()) { - // [rewrite]: (iff (iff l false) ~l) - // [symmetry T1]: (iff ~l (iff l false)) - pr = m().mk_rewrite(m().mk_eq(var, def), f); - pr = m().mk_symmetry(pr); - } - return true; - } - - return false; - } - - void checkpoint() { - if (m_cancel) - throw gaussian_elim_exception(STE_CANCELED_MSG); - cooperate("gaussian elimination"); - } - - /** - \brief Start collecting candidates - */ - void collect(assertion_set & set) { - m_subst.reset(); - m_norm_subst.reset(); - m_r->set_substitution(0); - m_candidate_vars.reset(); - m_candidate_set.reset(); - m_candidates.reset(); - m_vars.reset(); - - app_ref var(m()); - expr_ref def(m()); - proof_ref pr(m()); - unsigned size = set.size(); - for (unsigned idx = 0; idx < size; idx++) { - checkpoint(); - expr * f = set.form(idx); - if (solve(f, var, def, pr)) { - m_vars.push_back(var); - m_candidates.push_back(f); - m_candidate_set.mark(f); - m_candidate_vars.mark(var); - if (m().proofs_enabled()) { - if (pr == 0) - pr = set.pr(idx); - else - pr = m().mk_modus_ponens(set.pr(idx), pr); - } - m_subst.insert(var, def, pr); - } - m_num_steps++; - } - - TRACE("gaussian_elim", - tout << "candidate vars:\n"; - ptr_vector::iterator it = m_vars.begin(); - ptr_vector::iterator end = m_vars.end(); - for (; it != end; ++it) { - tout << mk_ismt2_pp(*it, m()) << " "; - } - tout << "\n";); - } - - - void sort_vars() { - SASSERT(m_candidates.size() == m_vars.size()); - TRACE("gaussian_elim_bug", tout << "sorting vars...\n";); - m_ordered_vars.reset(); - - - // The variables (and its definitions) in m_subst must remain alive until the end of this procedure. - // Reason: they are scheduled for unmarking in visiting/done. - // They should remain alive while they are on the stack. - // To make sure this is the case, whenever a variable (and its definition) is removed from m_subst, - // I add them to the saved vector. - - expr_ref_vector saved(m()); - - expr_fast_mark1 visiting; - expr_fast_mark2 done; - - typedef std::pair frame; - svector todo; - ptr_vector::const_iterator it = m_vars.begin(); - ptr_vector::const_iterator end = m_vars.end(); - unsigned num; - for (; it != end; ++it) { - checkpoint(); - app * v = *it; - if (!m_candidate_vars.is_marked(v)) - continue; - todo.push_back(frame(v, 0)); - while (!todo.empty()) { - start: - frame & fr = todo.back(); - expr * t = fr.first; - m_num_steps++; - TRACE("gaussian_elim_bug", tout << "processing:\n" << mk_ismt2_pp(t, m()) << "\n";); - if (t->get_ref_count() > 1 && done.is_marked(t)) { - todo.pop_back(); - continue; - } - switch (t->get_kind()) { - case AST_VAR: - todo.pop_back(); - break; - case AST_QUANTIFIER: - num = to_quantifier(t)->get_num_children(); - while (fr.second < num) { - expr * c = to_quantifier(t)->get_child(fr.second); - fr.second++; - if (c->get_ref_count() > 1 && done.is_marked(c)) - continue; - todo.push_back(frame(c, 0)); - goto start; - } - if (t->get_ref_count() > 1) - done.mark(t); - todo.pop_back(); - break; - case AST_APP: - num = to_app(t)->get_num_args(); - if (num == 0) { - if (fr.second == 0) { - if (m_candidate_vars.is_marked(t)) { - if (visiting.is_marked(t)) { - // cycle detected: remove t - visiting.reset_mark(t); - m_candidate_vars.mark(t, false); - SASSERT(!m_candidate_vars.is_marked(t)); - - // Must save t and its definition. - // See comment in the beginning of the function - expr * def = 0; - proof * pr; - m_subst.find(to_app(t), def, pr); - SASSERT(def != 0); - saved.push_back(t); - saved.push_back(def); - // - - m_subst.erase(t); - } - else { - visiting.mark(t); - fr.second = 1; - expr * def = 0; - proof * pr; - m_subst.find(to_app(t), def, pr); - SASSERT(def != 0); - todo.push_back(frame(def, 0)); - goto start; - } - } - } - else { - SASSERT(fr.second == 1); - if (m_candidate_vars.is_marked(t)) { - visiting.reset_mark(t); - m_ordered_vars.push_back(to_app(t)); - } - else { - // var was removed from the list of candidate vars to elim cycle - // do nothing - } - } - } - else { - while (fr.second < num) { - expr * arg = to_app(t)->get_arg(fr.second); - fr.second++; - if (arg->get_ref_count() > 1 && done.is_marked(arg)) - continue; - todo.push_back(frame(arg, 0)); - goto start; - } - } - if (t->get_ref_count() > 1) - done.mark(t); - todo.pop_back(); - break; - default: - UNREACHABLE(); - todo.pop_back(); - break; - } - } - } - - // cleanup - it = m_vars.begin(); - for (unsigned idx = 0; it != end; ++it, ++idx) { - if (!m_candidate_vars.is_marked(*it)) { - m_candidate_set.mark(m_candidates[idx], false); - } - } - - TRACE("gaussian_elim", - tout << "ordered vars:\n"; - ptr_vector::iterator it = m_ordered_vars.begin(); - ptr_vector::iterator end = m_ordered_vars.end(); - for (; it != end; ++it) { - SASSERT(m_candidate_vars.is_marked(*it)); - tout << mk_ismt2_pp(*it, m()) << " "; - } - tout << "\n";); - m_candidate_vars.reset(); - } - - void normalize() { - m_norm_subst.reset(); - m_r->set_substitution(&m_norm_subst); - - expr_ref new_def(m()); - proof_ref new_pr(m()); - unsigned size = m_ordered_vars.size(); - for (unsigned idx = 0; idx < size; idx++) { - checkpoint(); - expr * v = m_ordered_vars[idx]; - expr * def = 0; - proof * pr = 0; - m_subst.find(v, def, pr); - SASSERT(def != 0); - m_r->operator()(def, new_def, new_pr); - m_num_steps += m_r->get_num_steps() + 1; - if (m().proofs_enabled()) - new_pr = m().mk_transitivity(pr, new_pr); - m_norm_subst.insert(v, new_def, new_pr); - // we updated the substituting, but we don't need to reset m_r - // because all cached values there do not depend on v. - } - m_subst.reset(); - TRACE("gaussian_elim", - tout << "after normalizing variables\n"; - for (unsigned i = 0; i < m_ordered_vars.size(); i++) { - expr * v = m_ordered_vars[i]; - expr * def = 0; - proof * pr = 0; - m_norm_subst.find(v, def, pr); - tout << mk_ismt2_pp(v, m()) << "\n----->\n" << mk_ismt2_pp(def, m()) << "\n\n"; - }); -#if 0 - DEBUG_CODE({ - for (unsigned i = 0; i < m_ordered_vars.size(); i++) { - expr * v = m_ordered_vars[i]; - expr * def = 0; - proof * pr = 0; - m_norm_subst.find(v, def, pr); - SASSERT(def != 0); - CASSERT("gaussian_elim_bug", !occurs(v, def)); - } - }); -#endif - } - - void substitute(assertion_set & set) { - // force the cache of m_r to be reset. - m_r->set_substitution(&m_norm_subst); - - expr_ref new_f(m()); - proof_ref new_pr(m()); - unsigned size = set.size(); - for (unsigned idx = 0; idx < size; idx++) { - checkpoint(); - expr * f = set.form(idx); - TRACE("gaussian_leak", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";); - if (m_candidate_set.is_marked(f)) { - // f may be deleted after the following update. - // so, we must remove remove the mark before doing the update - m_candidate_set.mark(f, false); - SASSERT(!m_candidate_set.is_marked(f)); - set.update(idx, m().mk_true(), m().mk_true_proof()); - m_num_steps ++; - continue; - } - else { - m_r->operator()(f, new_f, new_pr); - } - TRACE("gaussian_elim_subst", tout << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n";); - m_num_steps += m_r->get_num_steps() + 1; - if (m().proofs_enabled()) { - new_pr = m().mk_modus_ponens(set.pr(idx), new_pr); - } - set.update(idx, new_f, new_pr); - if (set.inconsistent()) - return; - } - set.elim_true(); - TRACE("gaussian_elim", - tout << "after applying substitution\n"; - set.display(tout);); -#if 0 - DEBUG_CODE({ - for (unsigned i = 0; i < m_ordered_vars.size(); i++) { - expr * v = m_ordered_vars[i]; - for (unsigned j = 0; j < set.size(); j++) { - CASSERT("gaussian_elim_bug", !occurs(v, set.form(j))); - } - }}); -#endif - } - - void save_elim_vars(model_converter_ref & mc) { - IF_VERBOSE(100, if (!m_ordered_vars.empty()) verbose_stream() << "num. eliminated vars: " << m_ordered_vars.size() << "\n";); - m_num_eliminated_vars += m_ordered_vars.size(); - if (m_produce_models) { - if (mc.get() == 0) - mc = alloc(gmc, m()); - ptr_vector::iterator it = m_ordered_vars.begin(); - ptr_vector::iterator end = m_ordered_vars.end(); - for (; it != end; ++it) { - app * v = *it; - expr * def = 0; - proof * pr; - m_norm_subst.find(v, def, pr); - SASSERT(def != 0); - static_cast(mc.get())->insert(v->get_decl(), def); - } - } - } - - - void collect_num_occs(expr * t, expr_fast_mark1 & visited) { - ptr_buffer stack; - -#define VISIT(ARG) { \ - if (is_uninterp_const(ARG)) { \ - obj_map::obj_map_entry * entry = m_num_occs.insert_if_not_there2(ARG, 0); \ - entry->get_data().m_value++; \ - } \ - if (!visited.is_marked(ARG)) { \ - visited.mark(ARG, true); \ - stack.push_back(ARG); \ - } \ - } - - VISIT(t); - - while (!stack.empty()) { - expr * t = stack.back(); - stack.pop_back(); - if (!is_app(t)) - continue; - unsigned j = to_app(t)->get_num_args(); - while (j > 0) { - --j; - expr * arg = to_app(t)->get_arg(j); - VISIT(arg); - } - } - } - - void collect_num_occs(assertion_set & s) { - if (m_max_occs == UINT_MAX) - return; // no need to compute num occs - m_num_occs.reset(); - expr_fast_mark1 visited; - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) - collect_num_occs(s.form(i), visited); - } - - void operator()(assertion_set & s, model_converter_ref & mc) { - SASSERT(is_well_sorted(s)); - as_st_report report("gaussian-elimination", s); - TRACE("gaussian_elim", tout << "starting guassian elimination\n"; s.display(tout); tout << "\n";); - m_num_steps = 0; - mc = 0; - if (s.inconsistent()) - return; - - while (true) { - collect_num_occs(s); - collect(s); - if (m_subst.empty()) - break; - sort_vars(); - if (m_ordered_vars.empty()) - break; - normalize(); - substitute(s); - if (s.inconsistent()) { - mc = 0; - break; - } - save_elim_vars(mc); - TRACE("gaussian_elim_round", s.display(tout); if (mc) mc->display(tout);); - } - TRACE("gaussian_elim", s.display(tout);); - SASSERT(is_well_sorted(s)); - } - - void set_cancel(bool f) { - m_cancel = f; - m_r->set_cancel(f); - } - - unsigned get_num_steps() const { - return m_num_steps; - } - - unsigned get_num_eliminated_vars() const { - return m_num_eliminated_vars; - } -}; - -gaussian_elim::gaussian_elim(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner): - m_params(p) { - m_imp = alloc(imp, m, p, r, owner); -} - -gaussian_elim::~gaussian_elim() { - dealloc(m_imp); -} - -ast_manager & gaussian_elim::m() const { - return m_imp->m(); -} - -void gaussian_elim::updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); -} - -void gaussian_elim::get_param_descrs(param_descrs & r) { - insert_produce_models(r); - r.insert(":gaussian-max-occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations."); - r.insert(":theory-solver", CPK_BOOL, "(default: true) use theory solvers."); - r.insert(":ite-solver", CPK_BOOL, "(default: true) use if-then-else solver."); -} - -void gaussian_elim::operator()(assertion_set & s, model_converter_ref & mc) { - m_imp->operator()(s, mc); - report_st_progress(":num-elim-vars", get_num_eliminated_vars()); -} - -void gaussian_elim::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} - -void gaussian_elim::cleanup() { - unsigned num_elim_vars = m_imp->m_num_eliminated_vars; - ast_manager & m = m_imp->m(); - imp * d = m_imp; - expr_replacer * r = m_imp->m_r_owner ? m_imp->m_r : 0; - if (r) - r->set_substitution(0); - bool owner = m_imp->m_r_owner; - m_imp->m_r_owner = false; // stole replacer - #pragma omp critical (as_st_cancel) - { - m_imp = 0; - } - dealloc(d); - d = alloc(imp, m, m_params, r, owner); - #pragma omp critical (as_st_cancel) - { - m_imp = d; - } - m_imp->m_num_eliminated_vars = num_elim_vars; -} - -unsigned gaussian_elim::get_num_steps() const { - return m_imp->get_num_steps(); -} - -unsigned gaussian_elim::get_num_eliminated_vars() const { - return m_imp->get_num_eliminated_vars(); -} - -void gaussian_elim::collect_statistics(statistics & st) const { - st.update("eliminated vars", get_num_eliminated_vars()); -} - -void gaussian_elim::reset_statistics() { - m_imp->m_num_eliminated_vars = 0; -} - -as_st * mk_gaussian(ast_manager & m, params_ref const & p) { - return clean(alloc(gaussian_elim, m, p, mk_expr_simp_replacer(m, p), true)); -} diff --git a/src/assertion_set/gaussian_elim.h b/src/assertion_set/gaussian_elim.h deleted file mode 100644 index 994e9623a..000000000 --- a/src/assertion_set/gaussian_elim.h +++ /dev/null @@ -1,66 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - gaussian_elim.h - -Abstract: - - (extended) Gaussian elimination for assertion sets. - It also supports other theories besides arithmetic. - -Author: - - Leonardo (leonardo) 2011-04-21 - -Notes: - ---*/ -#ifndef _GAUSSIAN_ELIM_H_ -#define _GAUSSIAN_ELIM_H_ - -#include"assertion_set_strategy.h" - -class expr_replacer; - -MK_ST_EXCEPTION(gaussian_elim_exception); - -class gaussian_elim : public assertion_set_strategy { - struct imp; - imp * m_imp; - params_ref m_params; -public: - gaussian_elim(ast_manager & m, params_ref const & p = params_ref(), expr_replacer * r = 0, bool owner = false); - virtual ~gaussian_elim(); - - ast_manager & m () const; - - virtual void updt_params(params_ref const & p); - static void get_param_descrs(param_descrs & r); - virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } - - /** - \brief Apply gaussian elimination on the assertion set \c s. - Return a model_converter that converts any model for the updated set into a model for the old set. - */ - virtual void operator()(assertion_set & s, model_converter_ref & mc); - - virtual void cleanup(); - - unsigned get_num_steps() const; - unsigned get_num_eliminated_vars() const; - - virtual void collect_statistics(statistics & st) const; - virtual void reset_statistics(); -protected: - virtual void set_cancel(bool f); -}; - -as_st * mk_gaussian(ast_manager & m, params_ref const & p = params_ref()); - -inline as_st * mk_eq_solver(ast_manager & m, params_ref const & p = params_ref()) { - return mk_gaussian(m, p); -} - -#endif diff --git a/src/assertion_set/num_occurs_assertion_set.cpp b/src/assertion_set/num_occurs_assertion_set.cpp deleted file mode 100644 index 2f35d4b5c..000000000 --- a/src/assertion_set/num_occurs_assertion_set.cpp +++ /dev/null @@ -1,29 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - num_occurs_assertion_set.cpp - -Abstract: - - TODO: delete - -Author: - - Leonardo de Moura (leonardo) 2012-10-20. - -Revision History: - ---*/ -#include"num_occurs_assertion_set.h" -#include"assertion_set.h" - -// TODO delete -void num_occurs_as::operator()(assertion_set const & s) { - expr_fast_mark1 visited; - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - process(s.form(i), visited); - } -} diff --git a/src/assertion_set/num_occurs_assertion_set.h b/src/assertion_set/num_occurs_assertion_set.h deleted file mode 100644 index 50e8ac4e8..000000000 --- a/src/assertion_set/num_occurs_assertion_set.h +++ /dev/null @@ -1,38 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - num_occurs_assertion_set.h - -Abstract: - - TODO: delete - -Author: - - Leonardo de Moura (leonardo) 2012-10-20. - -Revision History: - ---*/ -#ifndef _NUM_OCCURS_AS_H_ -#define _NUM_OCCURS_AS_H_ - -#include"num_occurs.h" - -class assertion_set; - -/** - \brief Functor for computing the number of occurrences of each sub-expression in a expression F. -*/ -class num_occurs_as : public num_occurs { -public: - num_occurs_as(bool ignore_ref_count1 = false, bool ignore_quantifiers = false): - num_occurs(ignore_ref_count1, ignore_quantifiers) { - } - - void operator()(assertion_set const & s); // TODO delete -}; - -#endif diff --git a/src/assertion_set/reduce_args.cpp b/src/assertion_set/reduce_args.cpp deleted file mode 100644 index d6e2a3516..000000000 --- a/src/assertion_set/reduce_args.cpp +++ /dev/null @@ -1,521 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - reduce_args.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-04-06. - -Revision History: - ---*/ -#include"reduce_args.h" -#include"cooperate.h" -#include"ast_smt2_pp.h" -#include"map.h" -#include"rewriter_def.h" -#include"elim_var_model_converter.h" -#include"filter_model_converter.h" - -struct reduce_args::imp { - ast_manager & m_manager; - bool m_produce_models; - volatile bool m_cancel; - - ast_manager & m() const { return m_manager; } - - imp(ast_manager & m, params_ref const & p): - m_manager(m) { - updt_params(p); - m_cancel = false; - } - - void updt_params(params_ref const & p) { - m_produce_models = p.get_bool(":produce-models", false); - } - - void set_cancel(bool f) { - m_cancel = f; - } - - void checkpoint() { - if (m_cancel) - throw reduce_args_exception(STE_CANCELED_MSG); - cooperate("reduce-args"); - } - - struct find_non_candidates_proc { - ast_manager & m_manager; - obj_hashtable & m_non_cadidates; - - find_non_candidates_proc(ast_manager & m, obj_hashtable & non_cadidates): - m_manager(m), - m_non_cadidates(non_cadidates) { - } - - void operator()(var * n) {} - - void operator()(quantifier * n) {} - - void operator()(app * n) { - if (n->get_num_args() == 0) - return; // ignore constants - func_decl * d = n->get_decl(); - if (d->get_family_id() != null_family_id) - return; // ignore interpreted symbols - if (m_non_cadidates.contains(d)) - return; // it is already in the set. - unsigned j = n->get_num_args(); - while (j > 0) { - --j; - if (m_manager.is_value(n->get_arg(j))) - return; - } - m_non_cadidates.insert(d); - } - }; - - /** - \brief Populate the table non_cadidates with function declarations \c f - such that there is a function application (f t1 ... tn) where t1 ... tn are not values. - */ - void find_non_candidates(assertion_set const & s, obj_hashtable & non_candidates) { - non_candidates.reset(); - find_non_candidates_proc proc(m_manager, non_candidates); - expr_fast_mark1 visited; - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - checkpoint(); - quick_for_each_expr(proc, visited, s.form(i)); - } - - TRACE("reduce_args", tout << "non_candidates:\n"; - obj_hashtable::iterator it = non_candidates.begin(); - obj_hashtable::iterator end = non_candidates.end(); - for (; it != end; ++it) { - func_decl * d = *it; - tout << d->get_name() << "\n"; - }); - } - - struct populate_decl2args_proc { - ast_manager & m_manager; - obj_hashtable & m_non_cadidates; - obj_map & m_decl2args; - - populate_decl2args_proc(ast_manager & m, obj_hashtable & nc, obj_map & d): - m_manager(m), m_non_cadidates(nc), m_decl2args(d) {} - - void operator()(var * n) {} - void operator()(quantifier * n) {} - void operator()(app * n) { - if (n->get_num_args() == 0) - return; // ignore constants - func_decl * d = n->get_decl(); - if (d->get_family_id() != null_family_id) - return; // ignore interpreted symbols - if (m_non_cadidates.contains(d)) - return; // declaration is not a candidate - unsigned j = n->get_num_args(); - obj_map::iterator it = m_decl2args.find_iterator(d); - if (it == m_decl2args.end()) { - m_decl2args.insert(d, bit_vector()); - it = m_decl2args.find_iterator(d); - SASSERT(it != m_decl2args.end()); - it->m_value.reserve(j); - while (j > 0) { - --j; - it->m_value.set(j, m_manager.is_value(n->get_arg(j))); - } - } else { - SASSERT(j == it->m_value.size()); - while (j > 0) { - --j; - it->m_value.set(j, it->m_value.get(j) && m_manager.is_value(n->get_arg(j))); - } - } - } - }; - - void populate_decl2args(assertion_set const & s, - obj_hashtable & non_candidates, - obj_map & decl2args) { - expr_fast_mark1 visited; - decl2args.reset(); - populate_decl2args_proc proc(m_manager, non_candidates, decl2args); - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - checkpoint(); - quick_for_each_expr(proc, visited, s.form(i)); - } - - // Remove all cases where the simplification is not applicable. - ptr_buffer bad_decls; - obj_map::iterator it = decl2args.begin(); - obj_map::iterator end = decl2args.end(); - for (; it != end; it++) { - bool is_zero = true; - for (unsigned i = 0; i < it->m_value.size() && is_zero ; i++) { - if (it->m_value.get(i)) - is_zero = false; - } - if (is_zero) - bad_decls.push_back(it->m_key); - } - - ptr_buffer::iterator it2 = bad_decls.begin(); - ptr_buffer::iterator end2 = bad_decls.end(); - for (; it2 != end2; ++it2) - decl2args.erase(*it2); - - TRACE("reduce_args", tout << "decl2args:" << std::endl; - for (obj_map::iterator it = decl2args.begin() ; it != decl2args.end() ; it++) { - tout << it->m_key->get_name() << ": "; - for (unsigned i = 0 ; i < it->m_value.size() ; i++) - tout << (it->m_value.get(i) ? "1" : "0"); - tout << std::endl; - }); - } - - struct arg2func_hash_proc { - bit_vector const & m_bv; - - arg2func_hash_proc(bit_vector const & bv):m_bv(bv) {} - unsigned operator()(app const * n) const { - // compute the hash-code using only the arguments where m_bv is true. - unsigned a = 0x9e3779b9; - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - if (!m_bv.get(i)) - continue; // ignore argument - a = hash_u_u(a, n->get_arg(i)->get_id()); - } - return a; - } - }; - - struct arg2func_eq_proc { - bit_vector const & m_bv; - - arg2func_eq_proc(bit_vector const & bv):m_bv(bv) {} - bool operator()(app const * n1, app const * n2) const { - // compare only the arguments where m_bv is true - SASSERT(n1->get_num_args() == n2->get_num_args()); - unsigned num_args = n1->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - if (!m_bv.get(i)) - continue; // ignore argument - if (n1->get_arg(i) != n2->get_arg(i)) - return false; - } - return true; - } - }; - - typedef map arg2func; - typedef obj_map decl2arg2func_map; - - struct reduce_args_ctx { - ast_manager & m_manager; - decl2arg2func_map m_decl2arg2funcs; - - reduce_args_ctx(ast_manager & m): m_manager(m) { - } - - ~reduce_args_ctx() { - obj_map::iterator it = m_decl2arg2funcs.begin(); - obj_map::iterator end = m_decl2arg2funcs.end(); - for (; it != end; ++it) { - arg2func * map = it->m_value; - arg2func::iterator it2 = map->begin(); - arg2func::iterator end2 = map->end(); - for (; it2 != end2; ++it2) { - m_manager.dec_ref(it2->m_key); - m_manager.dec_ref(it2->m_value); - } - dealloc(map); - } - } - }; - - struct populate_decl2arg_set_proc { - ast_manager & m_manager; - obj_map & m_decl2args; - decl2arg2func_map & m_decl2arg2funcs; - - populate_decl2arg_set_proc(ast_manager & m, - obj_map & d, - decl2arg2func_map & ds): - m_manager(m), m_decl2args(d), m_decl2arg2funcs(ds) {} - - void operator()(var * n) {} - void operator()(quantifier * n) {} - - void operator()(app * n) { - if (n->get_num_args() == 0) - return; // ignore constants - func_decl * d = n->get_decl(); - if (d->get_family_id() != null_family_id) - return; // ignore interpreted symbols - obj_map::iterator it = m_decl2args.find_iterator(d); - if (it == m_decl2args.end()) - return; // not reducing the arguments of this declaration - bit_vector & bv = it->m_value; - arg2func * map = 0; - decl2arg2func_map::iterator it2 = m_decl2arg2funcs.find_iterator(d); - if (it2 == m_decl2arg2funcs.end()) { - map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv)); - m_decl2arg2funcs.insert(d, map); - } - else { - map = it2->m_value; - } - if (!map->contains(n)) { - // create fresh symbol... - ptr_buffer domain; - unsigned arity = d->get_arity(); - for (unsigned i = 0; i < arity; i++) { - if (!bv.get(i)) - domain.push_back(d->get_domain(i)); - } - func_decl * new_d = m_manager.mk_fresh_func_decl(d->get_name(), symbol::null, domain.size(), domain.c_ptr(), d->get_range()); - map->insert(n, new_d); - m_manager.inc_ref(n); - m_manager.inc_ref(new_d); - } - } - }; - - void populate_decl2arg_set(assertion_set const & s, - obj_map & decl2args, - decl2arg2func_map & decl2arg2funcs) { - expr_fast_mark1 visited; - - populate_decl2arg_set_proc proc(m_manager, decl2args, decl2arg2funcs); - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - checkpoint(); - quick_for_each_expr(proc, visited, s.form(i)); - } - } - - struct reduce_args_rw_cfg : public default_rewriter_cfg { - ast_manager & m; - imp & m_owner; - obj_map & m_decl2args; - decl2arg2func_map & m_decl2arg2funcs; - - reduce_args_rw_cfg(imp & owner, obj_map & decl2args, decl2arg2func_map & decl2arg2funcs): - m(owner.m_manager), - m_owner(owner), - m_decl2args(decl2args), - m_decl2arg2funcs(decl2arg2funcs) { - } - - bool max_steps_exceeded(unsigned num_steps) const { - m_owner.checkpoint(); - return false; - } - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - result_pr = 0; - if (f->get_arity() == 0) - return BR_FAILED; // ignore constants - if (f->get_family_id() != null_family_id) - return BR_FAILED; // ignore interpreted symbols - decl2arg2func_map::iterator it = m_decl2arg2funcs.find_iterator(f); - if (it == m_decl2arg2funcs.end()) - return BR_FAILED; - SASSERT(m_decl2args.contains(f)); - bit_vector & bv = m_decl2args.find(f); - arg2func * map = it->m_value; - app_ref tmp(m); - tmp = m.mk_app(f, num, args); - CTRACE("reduce_args", !map->contains(tmp), - tout << "map does not contain tmp f: " << f->get_name() << "\n"; - tout << mk_ismt2_pp(tmp, m) << "\n"; - arg2func::iterator it = map->begin(); - arg2func::iterator end = map->end(); - for (; it != end; ++it) { - tout << mk_ismt2_pp(it->m_key, m) << "\n---> " << it->m_value->get_name() << "\n"; - }); - SASSERT(map->contains(tmp)); - func_decl * new_f = map->find(tmp); - ptr_buffer new_args; - for (unsigned i = 0; i < num; i++) { - if (!bv.get(i)) - new_args.push_back(args[i]); - } - result = m.mk_app(new_f, new_args.size(), new_args.c_ptr()); - return BR_DONE; - } - }; - - struct reduce_args_rw : rewriter_tpl { - reduce_args_rw_cfg m_cfg; - public: - reduce_args_rw(imp & owner, obj_map & decl2args, decl2arg2func_map & decl2arg2funcs): - rewriter_tpl(owner.m_manager, false, m_cfg), - m_cfg(owner, decl2args, decl2arg2funcs) { - } - }; - - model_converter * mk_mc(obj_map & decl2args, decl2arg2func_map & decl2arg2funcs) { - ptr_buffer new_args; - var_ref_vector new_vars(m_manager); - ptr_buffer new_eqs; - elim_var_model_converter * e_mc = alloc(elim_var_model_converter, m_manager); - filter_model_converter * f_mc = alloc(filter_model_converter, m_manager); - decl2arg2func_map::iterator it = decl2arg2funcs.begin(); - decl2arg2func_map::iterator end = decl2arg2funcs.end(); - for (; it != end; ++it) { - func_decl * f = it->m_key; - arg2func * map = it->m_value; - expr * def = 0; - SASSERT(decl2args.contains(f)); - bit_vector & bv = decl2args.find(f); - new_vars.reset(); - new_args.reset(); - for (unsigned i = 0; i < f->get_arity(); i++) { - new_vars.push_back(m_manager.mk_var(i, f->get_domain(i))); - if (!bv.get(i)) - new_args.push_back(new_vars.back()); - } - arg2func::iterator it2 = map->begin(); - arg2func::iterator end2 = map->end(); - for (; it2 != end2; ++it2) { - app * t = it2->m_key; - func_decl * new_def = it2->m_value; - f_mc->insert(new_def); - SASSERT(new_def->get_arity() == new_args.size()); - app * new_t = m_manager.mk_app(new_def, new_args.size(), new_args.c_ptr()); - if (def == 0) { - def = new_t; - } - else { - new_eqs.reset(); - for (unsigned i = 0; i < f->get_arity(); i++) { - if (bv.get(i)) - new_eqs.push_back(m_manager.mk_eq(new_vars.get(i), t->get_arg(i))); - } - SASSERT(new_eqs.size() > 0); - expr * cond; - if (new_eqs.size() == 1) - cond = new_eqs[0]; - else - cond = m_manager.mk_and(new_eqs.size(), new_eqs.c_ptr()); - def = m_manager.mk_ite(cond, new_t, def); - } - } - SASSERT(def); - e_mc->insert(f, def); - } - return concat(f_mc, e_mc); - } - - void operator()(assertion_set & s, model_converter_ref & mc) { - mc = 0; - if (s.inconsistent()) - return; - if (m().proofs_enabled()) - throw reduce_args_exception("reduce-args does not support proofs"); - as_st_report report("reduce-args", s); - TRACE("reduce_args", s.display(tout);); - - obj_hashtable non_candidates; - obj_map decl2args; - find_non_candidates(s, non_candidates); - populate_decl2args(s, non_candidates, decl2args); - - if (decl2args.empty()) - return; - - ptr_vector arg2funcs; - reduce_args_ctx ctx(m_manager); - populate_decl2arg_set(s, decl2args, ctx.m_decl2arg2funcs); - - reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs); - - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - if (s.inconsistent()) - break; - expr * f = s.form(i); - expr_ref new_f(m_manager); - rw(f, new_f); - s.update(i, new_f); - } - - report_st_progress(":reduced-funcs", decl2args.size()); - - if (m_produce_models) - mc = mk_mc(decl2args, ctx.m_decl2arg2funcs); - - TRACE("reduce_args", s.display(tout); if (mc) mc->display(tout);); - } -}; - -reduce_args::reduce_args(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); -} - -reduce_args::~reduce_args() { - dealloc(m_imp); -} - -ast_manager & reduce_args::m() const { - return m_imp->m(); -} - -void reduce_args::updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); -} - -void reduce_args::get_param_descrs(param_descrs & r) { - insert_produce_models(r); -} - -void reduce_args::operator()(assertion_set & s, model_converter_ref & mc) { - m_imp->operator()(s, mc); -} - -void reduce_args::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} - -void reduce_args::cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; - #pragma omp critical (as_st_cancel) - { - m_imp = 0; - } - dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (as_st_cancel) - { - m_imp = d; - } -} - -void reduce_args::collect_statistics(statistics & st) const { -} - -void reduce_args::reset_statistics() { -} - -as_st * mk_reduce_args(ast_manager & m, params_ref const & p) { - return clean(alloc(reduce_args, m, p)); -} - - diff --git a/src/assertion_set/reduce_args.h b/src/assertion_set/reduce_args.h deleted file mode 100644 index 8dd20176f..000000000 --- a/src/assertion_set/reduce_args.h +++ /dev/null @@ -1,92 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - reduce_args.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-04-05. - -Revision History: - - Make it a strategy 2011-07-26. - ---*/ -#ifndef _REDUCE_ARGS_H_ -#define _REDUCE_ARGS_H_ - -#include"assertion_set_strategy.h" - -MK_ST_EXCEPTION(reduce_args_exception); - -/** - \brief Reduce the number of arguments in function applications. - - Example, suppose we have a function f with 2 arguments. - There are 1000 applications of this function, but the first argument is always "a", "b" or "c". - Thus, we replace the f(t1, t2) - with - f_a(t2) if t1 = a - f_b(t2) if t2 = b - f_c(t2) if t2 = c - - Since f_a, f_b, f_c are new symbols, satisfiability is preserved. - - This transformation is very similar in spirit to the Ackermman's reduction. - - This transformation should work in the following way: - - 1- Create a mapping decl2arg_map from declarations to tuples of booleans, an entry [f -> (true, false, true)] - means that f is a declaration with 3 arguments where the first and third arguments are always values. - 2- Traverse the formula and populate the mapping. - For each function application f(t1, ..., tn) do - a) Create a boolean tuple (is_value(t1), ..., is_value(tn)) and do - the logical-and with the tuple that is already in the mapping. If there is no such tuple - in the mapping, we just add a new entry. - - If all entries are false-tuples, then there is nothing to be done. The transformation is not applicable. - - Now, we create a mapping decl2new_decl from (decl, val_1, ..., val_n) to decls. Note that, n may be different for each entry, - but it is the same for the same declaration. - For example, suppose we have [f -> (true, false, true)] in decl2arg_map, and applications f(1, a, 2), f(1, b, 2), f(1, b, 3), f(2, b, 3), f(2, c, 3) in the formula. - Then, decl2arg_map would contain - (f, 1, 2) -> f_1_2 - (f, 1, 3) -> f_1_3 - (f, 2, 3) -> f_2_3 - where f_1_2, f_1_3 and f_2_3 are new function symbols. - Using the new map, we can replace the occurrences of f. -*/ -class reduce_args : public assertion_set_strategy { - struct imp; - imp * m_imp; - params_ref m_params; -public: - reduce_args(ast_manager & m, params_ref const & p = params_ref()); - virtual ~reduce_args(); - - ast_manager & m () const; - - virtual void updt_params(params_ref const & p); - static void get_param_descrs(param_descrs & r); - virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } - - virtual void operator()(assertion_set & s, model_converter_ref & mc); - - virtual void cleanup(); - - virtual void collect_statistics(statistics & st) const; - virtual void reset_statistics(); -protected: - virtual void set_cancel(bool f); -}; - -as_st * mk_reduce_args(ast_manager & m, params_ref const & p = params_ref()); - -#endif /* _REDUCE_ARGS_H_ */ - diff --git a/src/assertion_set/shallow_context_simplifier.cpp b/src/assertion_set/shallow_context_simplifier.cpp deleted file mode 100644 index ff9a7ffef..000000000 --- a/src/assertion_set/shallow_context_simplifier.cpp +++ /dev/null @@ -1,257 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - shallow_context_simplifier.h - -Abstract: - - Depth 1 context simplifier. - -Author: - - Leonardo de Moura (leonardo) 2011-04-28 - - -Revision History: - ---*/ -#include"shallow_context_simplifier.h" -#include"assertion_set_util.h" -#include"expr_substitution.h" -#include"th_rewriter.h" -#include"ast_smt2_pp.h" -#include"assertion_set_util.h" - -struct shallow_context_simplifier::imp { - ast_manager & m_manager; - th_rewriter m_r; - expr_substitution m_subst; - assertion_set * m_set; - as_shared_occs m_occs; - unsigned m_idx; - unsigned m_num_steps; - unsigned m_max_rounds; - bool m_modified; - - imp(ast_manager & m, params_ref const & p): - m_manager(m), - m_r(m, p), - m_subst(m), - m_set(0), - m_occs(m, true /* track atoms */) { - m_r.set_substitution(&m_subst); - updt_params_core(p); - } - - 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); - } - - ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { - m_r.set_cancel(f); - } - - void reset() { - m_subst.reset(); - m_set = 0; - m_num_steps = 0; - } - - void push_result(expr * new_curr, proof * new_pr) { - if (m().proofs_enabled()) { - proof * pr = m_set->pr(m_idx); - new_pr = m().mk_modus_ponens(pr, new_pr); - } - - m_set->update(m_idx, new_curr, new_pr); - - if (is_shared(new_curr)) { - m_subst.insert(new_curr, m().mk_true(), m().mk_iff_true(new_pr)); - } - expr * atom; - if (is_shared_neg(new_curr, atom)) { - m_subst.insert(atom, m().mk_false(), m().mk_iff_false(new_pr)); - } - 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); - } - } - - void process_current() { - expr * curr = m_set->form(m_idx); - expr_ref new_curr(m()); - proof_ref new_pr(m()); - - - if (!m_subst.empty()) { - m_r(curr, new_curr, new_pr); - m_num_steps += m_r.get_num_steps(); - } - 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";); - push_result(new_curr, new_pr); - if (new_curr != curr) - m_modified = true; - } - - void operator()(assertion_set & s) { - SASSERT(is_well_sorted(s)); - as_st_report report("shallow-context-simplifier", s); - m_num_steps = 0; - if (s.inconsistent()) - return; - SASSERT(m_set == 0); - bool forward = true; - m_set = &s; - m_occs(*m_set); - TRACE("shallow_context_simplifier_bug", m_occs.display(tout, m()); ); - - unsigned size = s.size(); - m_idx = 0; - m_modified = false; - - - expr_ref new_curr(m()); - proof_ref new_pr(m()); - - unsigned round = 0; - - while (true) { - TRACE("shallow_context_simplifier_round", s.display(tout);); - if (forward) { - for (; m_idx < size; m_idx++) { - process_current(); - if (m_set->inconsistent()) - goto end; - } - if (m_subst.empty() && !m_modified) - goto end; - m_occs(*m_set); - m_idx = m_set->size(); - forward = false; - m_subst.reset(); - m_r.set_substitution(&m_subst); // reset, but keep substitution - } - else { - while (m_idx > 0) { - m_idx--; - process_current(); - if (m_set->inconsistent()) - goto end; - } - if (!m_modified) - goto end; - m_subst.reset(); - m_r.set_substitution(&m_subst); // reset, but keep substitution - m_modified = false; - m_occs(*m_set); - m_idx = 0; - size = m_set->size(); - forward = true; - } - round++; - if (round >= m_max_rounds) - break; - IF_VERBOSE(100, verbose_stream() << "starting new round, assertion-set size: " << m_set->num_exprs() << std::endl;); - TRACE("shallow_context_simplifier", tout << "round finished\n"; m_set->display(tout); tout << "\n";); - } - end: - m_set = 0; - SASSERT(is_well_sorted(s)); - } - - bool is_shared(expr * t) { - return m_occs.is_shared(t); - } - - bool is_shared_neg(expr * t, expr * & atom) { - if (!m().is_not(t)) - return false; - atom = to_app(t)->get_arg(0); - return is_shared(atom); - } - - bool is_shared_eq(expr * t, expr * & lhs, expr * & value) { - if (!m().is_eq(t)) - return false; - expr * arg1 = to_app(t)->get_arg(0); - expr * arg2 = to_app(t)->get_arg(1); - 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; - } - - unsigned get_num_steps() const { return m_num_steps; } -}; - -shallow_context_simplifier::shallow_context_simplifier(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); -} - -shallow_context_simplifier::~shallow_context_simplifier() { - dealloc(m_imp); -} - -void shallow_context_simplifier::updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); -} - -void shallow_context_simplifier::get_param_descrs(param_descrs & r) { - th_rewriter::get_param_descrs(r); - r.insert(":max-rounds", CPK_UINT, "(default: 2) maximum number of rounds."); -} - -void shallow_context_simplifier::operator()(assertion_set & s) { - m_imp->operator()(s); -} - -void shallow_context_simplifier::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} - -void shallow_context_simplifier::cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; - #pragma omp critical (as_st_cancel) - { - m_imp = 0; - } - dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (as_st_cancel) - { - m_imp = d; - } -} - -unsigned shallow_context_simplifier::get_num_steps() const { - return m_imp->get_num_steps(); -} - diff --git a/src/assertion_set/shallow_context_simplifier.h b/src/assertion_set/shallow_context_simplifier.h deleted file mode 100644 index 0cc834af0..000000000 --- a/src/assertion_set/shallow_context_simplifier.h +++ /dev/null @@ -1,59 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - shallow_context_simplifier.h - -Abstract: - - Depth 1 context simplifier. - -Author: - - Leonardo de Moura (leonardo) 2011-04-28 - - -Revision History: - ---*/ -#ifndef _SHALLOW_CONTEXT_SIMPLIFIER_H_ -#define _SHALLOW_CONTEXT_SIMPLIFIER_H_ - -#include"assertion_set_strategy.h" - -class shallow_context_simplifier : public assertion_set_strategy { - struct imp; - imp * m_imp; - params_ref m_params; -public: - shallow_context_simplifier(ast_manager & m, params_ref const & p = params_ref()); - virtual ~shallow_context_simplifier(); - - virtual void updt_params(params_ref const & p); - static void get_param_descrs(param_descrs & r); - virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } - - void operator()(assertion_set & s); - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - operator()(s); - mc = 0; - } - - virtual void cleanup(); - - unsigned get_num_steps() const; -protected: - virtual void set_cancel(bool f); -}; - -inline as_st * mk_shallow_simplifier(ast_manager & m, params_ref const & p = params_ref()) { - return clean(alloc(shallow_context_simplifier, m, p)); -} - -inline as_st * mk_constant_propagation(ast_manager & m, params_ref const & p = params_ref()) { - return mk_shallow_simplifier(m, p); -} - -#endif diff --git a/src/assertion_set/st2tactic.cpp b/src/assertion_set/st2tactic.cpp deleted file mode 100644 index a880c8ebe..000000000 --- a/src/assertion_set/st2tactic.cpp +++ /dev/null @@ -1,77 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - st2tactic.h - -Abstract: - - Temporary adapter that converts a assertion_set_strategy into a tactic. - -Author: - - Leonardo (leonardo) 2012-02-19 - -Notes: - ---*/ -#include"assertion_set_strategy.h" -#include"tactic.h" - -class st2tactic_wrapper : public tactic { - assertion_set_strategy * m_st; - params_ref m_params; -public: - st2tactic_wrapper(assertion_set_strategy * st):m_st(st) {} - ~st2tactic_wrapper() { dealloc(m_st); } - - virtual tactic * translate(ast_manager & m) { - // st2tactic_wrapper is a temporary hack to support the old strategy framework. - // This class will be deleted in the future. - UNREACHABLE(); - NOT_IMPLEMENTED_YET(); - return 0; - } - - virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - SASSERT(g->is_well_sorted()); - pc = 0; mc = 0; core = 0; - fail_if_unsat_core_generation("st2tactic", g); - assertion_set s(g->m()); - for (unsigned i = 0; i < g->size(); i++) - s.assert_expr(g->form(i), g->pr(i)); - if (g->models_enabled()) { - params_ref mp = m_params; - mp.set_bool(":produce-models", true); - m_st->updt_params(mp); - } - try { - (*m_st)(s, mc); - } - catch (strategy_exception & ex) { - throw tactic_exception(ex.msg()); - } - g->reset(); - for (unsigned i = 0; i < s.size(); i++) { - g->assert_expr(s.form(i), s.pr(i), 0); - } - g->inc_depth(); - result.push_back(g.get()); - SASSERT(g->is_well_sorted()); - } - - virtual void updt_params(params_ref const & p) { m_params = p; m_st->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { m_st->collect_param_descrs(r); } - virtual void cleanup() { m_st->cleanup(); } - virtual void set_cancel(bool f) { m_st->set_cancel(f); } - virtual void collect_statistics(statistics & st) const { m_st->collect_statistics(st); } - virtual void reset_statistics() { m_st->reset_statistics(); } - virtual void set_front_end_params(front_end_params & p) { m_st->set_front_end_params(p); } - virtual void set_logic(symbol const & l) { m_st->set_logic(l); } - virtual void set_progress_callback(progress_callback * callback) { m_st->set_progress_callback(callback); } -}; - -tactic * st2tactic(assertion_set_strategy * st) { - return alloc(st2tactic_wrapper, st); -} diff --git a/src/assertion_set/st2tactic.h b/src/assertion_set/st2tactic.h deleted file mode 100644 index 68b6f35be..000000000 --- a/src/assertion_set/st2tactic.h +++ /dev/null @@ -1,27 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - st2tactic.h - -Abstract: - - Temporary adapter that converts a assertion_set_strategy into a tactic. - -Author: - - Leonardo (leonardo) 2012-02-19 - -Notes: - ---*/ -#ifndef _ST2TACTIC_H_ -#define _ST2TACTIC_H_ - -class tactic; -class assertion_set_strategy; - -tactic * st2tactic(assertion_set_strategy * st); - -#endif diff --git a/src/assertion_set/strategy_exception.cpp b/src/assertion_set/strategy_exception.cpp deleted file mode 100644 index c57275a91..000000000 --- a/src/assertion_set/strategy_exception.cpp +++ /dev/null @@ -1,26 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - strategy_exception.cpp - -Abstract: - - Strategy exception - -Author: - - Leonardo (leonardo) 2011-05-02 - -Notes: - ---*/ -#include"strategy_exception.h" - -char const * strategy_exception::g_ste_canceled_msg = "canceled"; -char const * strategy_exception::g_ste_max_memory_msg = "max. memory exceeded"; -char const * strategy_exception::g_ste_max_scopes_msg = "max. scopes exceeded"; -char const * strategy_exception::g_ste_max_steps_msg = "max. steps exceeded"; -char const * strategy_exception::g_ste_max_frames_msg = "max. frames exceeded"; -char const * strategy_exception::g_ste_no_proofs_msg = "strategy does not support proof generation"; diff --git a/src/assertion_set/strategy_exception.h b/src/assertion_set/strategy_exception.h deleted file mode 100644 index 379517396..000000000 --- a/src/assertion_set/strategy_exception.h +++ /dev/null @@ -1,53 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - strategy_exception.h - -Abstract: - - Strategy exception - -Author: - - Leonardo (leonardo) 2011-05-02 - -Notes: - ---*/ -#ifndef _STRATEGY_EXCEPTION_H_ -#define _STRATEGY_EXCEPTION_H_ - -#include"z3_exception.h" - -class strategy_exception : public z3_exception { -public: - static char const * g_ste_canceled_msg; - static char const * g_ste_max_memory_msg; - static char const * g_ste_max_scopes_msg; - static char const * g_ste_max_steps_msg; - static char const * g_ste_max_frames_msg; - static char const * g_ste_no_proofs_msg; -protected: - char const * m_msg; -public: - strategy_exception(char const * msg):m_msg(msg) {} - virtual ~strategy_exception() {} - virtual char const * msg() const { return m_msg; } -}; - -#define STE_CANCELED_MSG strategy_exception::g_ste_canceled_msg -#define STE_MAX_MEMORY_MSG strategy_exception::g_ste_max_memory_msg -#define STE_MAX_SCOPES_MSG strategy_exception::g_ste_max_scopes_msg -#define STE_MAX_STEPS_MSG strategy_exception::g_ste_max_steps_msg -#define STE_MAX_FRAMES_MSG strategy_exception::g_ste_max_frames_msg -#define STE_NO_PROOF_GEN_MSG strategy_exception::g_ste_no_proofs_msg - -#define MK_ST_EXCEPTION(NAME) \ -class NAME : public strategy_exception { \ -public: \ - NAME(char const * msg):strategy_exception(msg) {} \ -} - -#endif