mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

deleted assertion_sets (aka old tactic framework)

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-24 14:08:00 -07:00
parent 4f6b34bc7b
commit 66234ff4bd
28 changed files with 0 additions and 5122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_make.py
View file

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

1
src/assertion_set/README
View file

@ -1 +0,0 @@
This module is obsolete. It is subsumed by the tactic module.

430
src/assertion_set/assertion_set.cpp
View file

@ -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 *, bool> expr_pol;
sbuffer<expr_pol, 64> 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<expr> 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<expr, unsigned> 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<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::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;
}

98
src/assertion_set/assertion_set.h
View file

@ -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<proof*>(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<typename ForEachProc>
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

122
src/assertion_set/assertion_set_rewriter.cpp
View file

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

56
src/assertion_set/assertion_set_rewriter.h
View file

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

1255
src/assertion_set/assertion_set_strategy.cpp
View file

File diff suppressed because it is too large Load diff

223
src/assertion_set/assertion_set_strategy.h
View file

@ -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> as_st_ref;
typedef ref_vector<as_st, as_st_ctx> as_st_ref_vector;
typedef ref_buffer<as_st, as_st_ctx> 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

220
src/assertion_set/assertion_set_util.cpp
View file

@ -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<is_non_propositional>(s);
}
bool is_qfbv(assertion_set const & s) {
return !test<is_non_qfbv>(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<has_term_ite_proc>(s);
}

91
src/assertion_set/assertion_set_util.h
View file

@ -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<typename Predicate>
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<typename Predicate>
bool test(assertion_set const & s) {
Predicate proc(s.m());
return test(s, proc);
}
#endif

94
src/assertion_set/der_strategy.cpp
View file

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

47
src/assertion_set/der_strategy.h
View file

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

232
src/assertion_set/elim_distinct.cpp
View file

@ -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<func_decl, func_decl *> 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<func_decl, func_decl *> 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<sort> 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> {
u2i_cfg m_cfg;
public:
u2i(ast_manager & m, sort * u):
rewriter_tpl<u2i_cfg>(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<u2i*> 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::imp::u2i_cfg>;
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);
}

54
src/assertion_set/elim_distinct.h
View file

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

120
src/assertion_set/elim_var_model_converter.cpp
View file

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

56
src/assertion_set/elim_var_model_converter.h
View file

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

775
src/assertion_set/gaussian_elim.cpp
View file

@ -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<expr, unsigned> 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<expr> m_candidates;
ptr_vector<app> m_vars;
ptr_vector<app> 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<expr> 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<app>::iterator it = m_vars.begin();
ptr_vector<app>::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<expr *, unsigned> frame;
svector<frame> todo;
ptr_vector<app>::const_iterator it = m_vars.begin();
ptr_vector<app>::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<app>::iterator it = m_ordered_vars.begin();
ptr_vector<app>::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<app>::iterator it = m_ordered_vars.begin();
ptr_vector<app>::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<gmc*>(mc.get())->insert(v->get_decl(), def);
}
}
}
void collect_num_occs(expr * t, expr_fast_mark1 & visited) {
ptr_buffer<expr, 128> stack;
#define VISIT(ARG) { \
if (is_uninterp_const(ARG)) { \
obj_map<expr, unsigned>::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));
}

66
src/assertion_set/gaussian_elim.h
View file

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

29
src/assertion_set/num_occurs_assertion_set.cpp
View file

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

38
src/assertion_set/num_occurs_assertion_set.h
View file

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

521
src/assertion_set/reduce_args.cpp
View file

@ -1,521 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
reduce_args.cpp
Abstract:
<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<func_decl> & m_non_cadidates;
find_non_candidates_proc(ast_manager & m, obj_hashtable<func_decl> & 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<func_decl> & 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<func_decl>::iterator it = non_candidates.begin();
obj_hashtable<func_decl>::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<func_decl> & m_non_cadidates;
obj_map<func_decl, bit_vector> & m_decl2args;
populate_decl2args_proc(ast_manager & m, obj_hashtable<func_decl> & nc, obj_map<func_decl, bit_vector> & 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<func_decl, bit_vector>::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<func_decl> & non_candidates,
obj_map<func_decl, bit_vector> & 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<func_decl> bad_decls;
obj_map<func_decl, bit_vector>::iterator it = decl2args.begin();
obj_map<func_decl, bit_vector>::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<func_decl>::iterator it2 = bad_decls.begin();
ptr_buffer<func_decl>::iterator end2 = bad_decls.end();
for (; it2 != end2; ++it2)
decl2args.erase(*it2);
TRACE("reduce_args", tout << "decl2args:" << std::endl;
for (obj_map<func_decl, bit_vector>::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<app *, func_decl *, arg2func_hash_proc, arg2func_eq_proc> arg2func;
typedef obj_map<func_decl, arg2func *> 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<func_decl, arg2func *>::iterator it = m_decl2arg2funcs.begin();
obj_map<func_decl, arg2func *>::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<func_decl, bit_vector> & m_decl2args;
decl2arg2func_map & m_decl2arg2funcs;
populate_decl2arg_set_proc(ast_manager & m,
obj_map<func_decl, bit_vector> & 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<func_decl, bit_vector>::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<sort> 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<func_decl, bit_vector> & 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<func_decl, bit_vector> & m_decl2args;
decl2arg2func_map & m_decl2arg2funcs;
reduce_args_rw_cfg(imp & owner, obj_map<func_decl, bit_vector> & 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<expr> 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> {
reduce_args_rw_cfg m_cfg;
public:
reduce_args_rw(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
rewriter_tpl<reduce_args_rw_cfg>(owner.m_manager, false, m_cfg),
m_cfg(owner, decl2args, decl2arg2funcs) {
}
};
model_converter * mk_mc(obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs) {
ptr_buffer<expr> new_args;
var_ref_vector new_vars(m_manager);
ptr_buffer<expr> 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<func_decl> non_candidates;
obj_map<func_decl, bit_vector> decl2args;
find_non_candidates(s, non_candidates);
populate_decl2args(s, non_candidates, decl2args);
if (decl2args.empty())
return;
ptr_vector<arg2func> 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));
}

92
src/assertion_set/reduce_args.h
View file

@ -1,92 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
reduce_args.h
Abstract:
<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_ */

257
src/assertion_set/shallow_context_simplifier.cpp
View file

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

59
src/assertion_set/shallow_context_simplifier.h
View file

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

77
src/assertion_set/st2tactic.cpp
View file

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

27
src/assertion_set/st2tactic.h
View file

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

26
src/assertion_set/strategy_exception.cpp
View file

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

53
src/assertion_set/strategy_exception.h
View file

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