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

Moved dead code to dead branch

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-01 08:40:20 -07:00
parent 8f7494cb04
commit 81df5ca96f
123 changed files with 0 additions and 33328 deletions
Download patch file Download diff file Expand all files Collapse all files

1792
src/tactic/arith/dead/lu.cpp
View file

File diff suppressed because it is too large Load diff

404
src/tactic/arith/dead/lu.h
View file

@ -1,404 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
lu.h
Abstract:
Simple LU factorization module based on the paper:
"Maintaining LU factors of a General Sparse Matrix"
P. E. Gill, W. Murray, M. Saunders, M. Wright
Author:
Leonardo de Moura (leonardo) 2011-06-09
Revision History:
--*/
#ifndef _LU_H_
#define _LU_H_
#include"vector.h"
#include"mpq.h"
#include"double_manager.h"
#include"permutation.h"
#include"params.h"
#include"strategy_exception.h"
MK_ST_EXCEPTION(lu_exception);
template<typename NumManager>
class lu {
public:
typedef NumManager manager;
typedef typename NumManager::numeral numeral;
typedef svector<numeral> numeral_vector;
private:
manager & m_manager;
// Configuration
numeral m_mu; // maximum multiplier when selecting a pivot
unsigned m_selection_cutoff;
// Matrix size
unsigned m_sz; // supporting only square matrices
// Permutations
permutation P;
permutation Q;
// L
//
// It is 3 parallel vectors representing the sequence (product) of matrices
// L[0] L[1] ... L[m-1]
// where each L[i] is a tuple (A[i], indc[i], indr[i]).
// Each tuple represents a triangular factor. That is, an identity matrix
// where the position at row indc[i], and column indr[i] contains the value A[i].
// Remark: The product L[0] L[1] ... L[n-1] is not really a triangular matrix.
struct L_file {
numeral_vector A;
unsigned_vector indc;
unsigned_vector indr;
};
L_file L;
// U
//
// It is not really upper triangular, but the product PUQ is.
// The rows of U are stored in the parallel vectors (A, indr)
// Only the non-zero values are stored at U.
// The non-zeros of row i start at position begr[i] and end at
// position endr[i] of the parallel vectors (A, indr).
// The length of the row is endr[i] - begr[i].
// The coefficients are stored in A, and the column ids at indr.
//
// The factorization of a matrix A is represented as:
// L[0] L[1] ... L[m-1] P U Q
struct U_file {
numeral_vector A;
unsigned_vector indr;
unsigned_vector begr;
unsigned_vector endr;
unsigned num_entries;
U_file():num_entries(0) {}
};
U_file U;
// The actual factorization
// T_file: temporary file used for factorization
struct T_file {
// row list
unsigned_vector indr;
unsigned_vector begr;
unsigned_vector endr;
// column list
numeral_vector A;
unsigned_vector indc;
unsigned_vector begc;
unsigned_vector endc;
unsigned num_entries;
T_file():num_entries(0) {}
};
T_file T;
// Auxiliary fields
unsigned_vector locw;
// -----------------------
//
// Main
//
// -----------------------
public:
lu(manager & m, params_ref const & p);
~lu();
manager & m() const { return m_manager; }
void updt_params(params_ref const & p);
void reset();
unsigned size() const { return m_sz; }
protected:
void del_nums(numeral_vector & nums);
// -----------------------
//
// Initialization
//
// -----------------------
public:
// Contract for setting up the initial matrix:
// lu.init(size)
// - for each row r in the matrix
// - for each non-zero (a,x) in the row
// lu.add_entry(a, x)
// lu.end_row()
void init(unsigned size);
void add_entry(numeral const & a, unsigned x);
void end_row();
protected:
// auxiliary fields used during initialization
bool ini; // try if the matrix T is being setup using the protocol above
unsigned ini_irow;
unsigned fillin_for(unsigned sz);
void move_col_to_end(unsigned x);
void move_row_to_end(unsigned x);
// -----------------------
//
// Factorization
//
// -----------------------
public:
void fact();
protected:
class todo {
unsigned_vector m_elem2len;
unsigned_vector m_elem2pos;
vector<unsigned_vector> m_elems_per_len;
unsigned m_size;
public:
todo():m_size(0) {}
bool contains(unsigned elem) const { return m_elem2pos[elem] != UINT_MAX; }
void init(unsigned capacity);
void updt_len(unsigned elem, unsigned len);
unsigned len(unsigned elem) const { return m_elem2len[elem]; }
void erase(unsigned elem);
unsigned size() const { return m_size; }
void display(std::ostream & out) const;
class iterator {
todo const & m_todo;
unsigned m_i;
unsigned m_j;
unsigned m_c;
void find_next();
public:
iterator(todo const & t):m_todo(t), m_i(0), m_j(0), m_c(0) { if (!at_end()) find_next(); }
bool at_end() const { return m_c == m_todo.m_size; }
unsigned curr() const {
unsigned_vector const & v_i = m_todo.m_elems_per_len[m_i];
return v_i[m_j];
}
void next() { SASSERT(!at_end()); m_j++; m_c++; find_next(); }
};
};
todo m_todo_rows;
todo m_todo_cols;
svector<bool> m_enabled_rows;
svector<bool> m_enabled_cols;
bool enabled_row(unsigned r) const { return m_enabled_rows[r]; }
bool enabled_col(unsigned c) const { return m_enabled_cols[c]; }
unsigned_vector m_toadd_rows;
svector<bool> m_marked_rows;
// Temporary numerals
// I do not use local numerals to avoid memory leaks
numeral tol;
numeral C_max;
numeral A_ij;
numeral A_best;
numeral A_aux;
numeral tmp;
numeral mu_best;
numeral mu_1;
void init_fact();
bool stability_test(unsigned rin, unsigned cin, bool improvingM);
void select_pivot(unsigned & r_out, unsigned & c_out);
void process_pivot_core(unsigned r, unsigned c);
void process_pivot(unsigned i, unsigned r, unsigned c);
bool check_locw() const;
void dec_lenr(unsigned r);
void inc_lenr(unsigned r);
void dec_lenc(unsigned c);
void inc_lenc(unsigned c);
void del_row_entry(unsigned r, unsigned c);
void del_disabled_cols(unsigned r);
void add_row_entry(unsigned r, unsigned c);
void add_col_entry(unsigned r, unsigned c, numeral const & a);
void compress_rows();
void compress_columns();
void compress_if_needed();
void copy_T_to_U();
bool check_lenr() const;
bool check_lenc() const;
// -----------------------
//
// Solving
//
// -----------------------
public:
// Temporary vector used to interact with different solvers.
// The vector has support for tracking non-zeros.
class dense_vector {
public:
typedef typename lu<NumManager>::manager manager;
typedef typename lu<NumManager>::numeral numeral;
private:
friend class lu;
manager & m_manager;
unsigned_vector m_non_zeros; // positions that may contain non-zeros. if a position is not here, then it must contain a zero
char_vector m_in_non_zeros; // m_in_non_zeros[i] == true if m_non_zeros contains i.
numeral_vector m_values;
public:
dense_vector(manager & m, unsigned sz);
~dense_vector();
manager & m() const { return m_manager; }
void reset();
void reset(unsigned new_sz);
unsigned size() const { return m_values.size(); }
numeral const & operator[](unsigned idx) const { return m_values[idx]; }
void swap(dense_vector & other) {
m_non_zeros.swap(other.m_non_zeros);
m_in_non_zeros.swap(other.m_in_non_zeros);
m_values.swap(other.m_values);
}
// Get a given position for performing an update.
// idx is inserted into m_non_zeros.
numeral & get(unsigned idx) {
if (!m_in_non_zeros[idx]) {
m_in_non_zeros[idx] = true;
m_non_zeros.push_back(idx);
}
return m_values[idx];
}
typedef unsigned_vector::const_iterator iterator;
// iterator for positions that may contain non-zeros
iterator begin_non_zeros() const { return m_non_zeros.begin(); }
iterator end_non_zeros() const { return m_non_zeros.end(); }
void display(std::ostream & out) const;
void display_non_zeros(std::ostream & out) const;
void display_pol(std::ostream & out) const;
void elim_zeros();
};
// Solve: Lx = y
// The result is stored in y.
void solve_Lx_eq_y(dense_vector & y);
// Solve: PUQx = y
// The result is stored in y.
void solve_Ux_eq_y(dense_vector & y);
// Solve: LPUQx = y
// The result is stored in y.
void solve_Ax_eq_y(dense_vector & y) {
solve_Lx_eq_y(y);
solve_Ux_eq_y(y);
}
// Solve: xL = y
// The result is stored in y.
void solve_xL_eq_y(dense_vector & y);
// Solve: xPUQ = y
// The result is stored in y.
void solve_xU_eq_y(dense_vector & y);
// Solve: xA = y
// The result is stored in y.
void solve_xA_eq_y(dense_vector & y) {
solve_xU_eq_y(y);
solve_xL_eq_y(y);
}
private:
dense_vector m_tmp_xU_vector;
dense_vector m_tmp_replace_column_vector;
dense_vector m_tmp_vector;
dense_vector m_tmp_row;
public:
dense_vector & get_tmp_vector() { return m_tmp_vector; }
dense_vector & get_tmp_row(unsigned size) { m_tmp_row.reset(size); return m_tmp_row; }
// -----------------------
//
// Column replacement
//
// -----------------------
public:
void replace_column(unsigned j, dense_vector & new_col);
void replace_U_column(unsigned j, dense_vector & new_col);
unsigned get_num_replacements() const { return m_num_replacements; }
dense_vector & get_tmp_col() { return m_tmp_col; }
private:
unsigned m_num_replacements;
dense_vector m_tmp_col;
void del_U_row_entry(unsigned r, unsigned c);
void compress_U_rows();
void compress_U_if_needed();
void move_U_row_to_end(unsigned r);
void add_U_row_entry(unsigned r, unsigned c, numeral const & a);
void add_replace_U_row_entry(unsigned r, unsigned c, numeral const & a);
unsigned replace_U_column_core(unsigned j, dense_vector & new_col);
bool check_U_except_col(unsigned c) const;
bool check_U_except_row(unsigned r) const;
// -----------------------
//
// Invariants
//
// -----------------------
public:
bool check_P() const;
bool check_Q() const;
bool check_L() const;
bool check_U() const;
bool T_col_contains(unsigned c, unsigned r) const;
bool T_row_contains(unsigned r, unsigned c) const;
bool check_T() const;
bool check_invariant() const;
void display_T(std::ostream & out) const;
void display_U(std::ostream & out, unsigned_vector const * var_ids = 0) const;
void display_L(std::ostream & out) const;
void display(std::ostream & out, unsigned_vector const * var_ids = 0) const;
// -----------------------
//
// Info
//
// -----------------------
public:
unsigned L_size() const { return L.indc.size(); }
unsigned U_size() const { return U.num_entries; }
};
typedef lu<unsynch_mpq_manager> rational_lu;
typedef lu<double_manager> double_lu;
#endif

135
src/tactic/arith/dead/mip_tactic.cpp
View file

@ -1,135 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
mip_tactic.cpp
Abstract:
Tactic for solvig MIP (mixed integer) problem.
This is a temporary tactic. It should be deleted
after theory_arith is upgraded.
Author:
Leonardo (leonardo) 2012-02-26
Notes:
--*/
#include"tactical.h"
#include"smt_solver_exp.h"
class mip_tactic : public tactic {
struct imp;
ast_manager & m;
params_ref m_params;
statistics m_stats;
scoped_ptr<smt::solver_exp> m_solver;
void init_solver() {
smt::solver_exp * new_solver = alloc(smt::solver_exp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_solver = new_solver;
}
}
public:
mip_tactic(ast_manager & _m, params_ref const & p):
m(_m),
m_params(p) {
}
virtual tactic * translate(ast_manager & m) {
return alloc(mip_tactic, m, m_params);
}
virtual ~mip_tactic() {}
virtual void updt_params(params_ref const & p) {
m_params = p;
}
virtual void collect_param_descrs(param_descrs & r) {
}
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());
bool produce_models = g->models_enabled();
mc = 0; pc = 0; core = 0; result.reset();
tactic_report report("mip", *g);
fail_if_proof_generation("mip", g);
fail_if_unsat_core_generation("mip", g);
g->elim_redundancies();
if (g->inconsistent()) {
result.push_back(g.get());
return;
}
init_solver();
m_solver->assert_goal(*g);
lbool r;
try {
r = m_solver->check();
}
catch (strategy_exception & ex) {
// solver_exp uses assertion_sets and strategy_exception's
throw tactic_exception(ex.msg());
}
m_solver->collect_statistics(m_stats);
if (r == l_false) {
g->reset();
g->assert_expr(m.mk_false());
}
else if (r == l_true) {
g->reset();
if (produce_models) {
model_ref md;
m_solver->get_model(md);
mc = model2model_converter(md.get());
}
}
else {
// failed
}
g->inc_depth();
result.push_back(g.get());
TRACE("mip", g->display(tout););
SASSERT(g->is_well_sorted());
}
virtual void cleanup() {
if (m_solver)
m_solver->collect_statistics(m_stats);
#pragma omp critical (tactic_cancel)
{
m_solver = 0;
}
}
virtual void collect_statistics(statistics & st) const {
st.copy(m_stats);
}
virtual void reset_statistics() {
m_stats.reset();
}
virtual void set_cancel(bool f) {
if (m_solver)
m_solver->set_cancel(f);
}
};
tactic * mk_mip_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(mip_tactic, m, p));
}

30
src/tactic/arith/dead/mip_tactic.h
View file

@ -1,30 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
mip_tactic.h
Abstract:
Tactic for solvig MIP (mixed integer) problem.
This is a temporary tactic. It should be deleted
after theory_arith is upgraded.
Author:
Leonardo (leonardo) 2012-02-26
Notes:
--*/
#ifndef _MIP_TACTIC_H_
#define _MIP_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_mip_tactic(ast_manager & m, params_ref const & p = params_ref());
#endif

3605
src/tactic/arith/dead/smt_arith.cpp
View file

File diff suppressed because it is too large Load diff

56
src/tactic/arith/dead/smt_arith.h
View file

@ -1,56 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_arith.h
Abstract:
Arithmetic solver for smt::solver
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
--*/
#ifndef _SMT_ARITH_H_
#define _SMT_ARITH_H_
#include"ast.h"
#include"smt_solver_types.h"
#include"params.h"
#include"statistics.h"
class model;
namespace smt {
class arith {
struct imp;
imp * m_imp;
params_ref m_params;
public:
arith(ast_manager & m, params_ref const & p);
~arith();
void updt_params(params_ref const & p);
void assert_axiom(expr * t, bool neg);
void mk_atom(expr * t, atom_id id);
void asserted(atom_id id, bool is_true);
bool inconsistent() const;
void push();
void pop(unsigned num_scopes);
void set_cancel(bool f);
void simplify();
void display(std::ostream & out) const;
void reset();
void preprocess();
void collect_statistics(statistics & st) const;
void reset_statistics();
lbool check();
void mk_model(model * md);
};
};
#endif

218
src/tactic/arith/dead/smt_formula_compiler.cpp
View file

@ -1,218 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_formula_compiler.cpp
Abstract:
Auxiliary class for smt::solver
Convert Exprs into Internal data-structures.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
This was an experiment to rewrite Z3 kernel.
It will be deleted after we finish revamping Z3 kernel.
--*/
#include"smt_formula_compiler.h"
#include"smt_solver_exp.h"
#include"assertion_set_util.h"
#include"assertion_set2sat.h"
#include"for_each_expr.h"
namespace smt {
formula_compiler::formula_compiler(solver_exp & _s, params_ref const & p):
s(_s),
m_a_util(s.m),
m_normalizer(s.m),
m_elim_ite(s.m) {
updt_params(p);
params_ref s_p;
s_p.set_bool(":elim-and", true);
s_p.set_bool(":blast-distinct", true);
s_p.set_bool(":eq2ineq", true);
s_p.set_bool(":arith-lhs", true);
s_p.set_bool(":gcd-rounding", true);
s_p.set_bool(":sort-sums", true);
s_p.set_bool(":som", true);
m_normalizer.updt_params(s_p);
}
formula_compiler::~formula_compiler() {
}
// mark theory axioms: literals that do not occur in the boolean structure
void formula_compiler::mark_axioms(assertion_set const & s, expr_fast_mark2 & axioms) {
ast_manager & m = s.m();
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = s.form(i);
while (m.is_not(f, f));
if (!is_app(f) || to_app(f)->get_family_id() != m.get_basic_family_id()) {
axioms.mark(f);
continue;
}
SASSERT(is_app(f));
SASSERT(to_app(f)->get_family_id() == m.get_basic_family_id());
switch (to_app(f)->get_decl_kind()) {
case OP_OR:
case OP_IFF:
break;
case OP_ITE:
SASSERT(m.is_bool(to_app(f)->get_arg(1)));
break;
case OP_EQ:
if (!m.is_bool(to_app(f)->get_arg(1)))
axioms.mark(f);
break;
case OP_AND:
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT:
UNREACHABLE();
break;
default:
break;
}
}
}
struct unmark_axioms_proc {
expr_fast_mark2 & m_axioms;
unmark_axioms_proc(expr_fast_mark2 & axioms):m_axioms(axioms) {}
void operator()(quantifier *) {}
void operator()(var *) {}
void operator()(app * t) {
m_axioms.reset_mark(t);
}
};
/**
\brief Unmark atoms that occur in the boolean structure.
*/
void formula_compiler::unmark_nested_atoms(assertion_set const & s, expr_fast_mark2 & axioms) {
ast_manager & m = s.m();
expr_fast_mark1 visited;
unmark_axioms_proc proc(axioms);
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = s.form(i);
while (m.is_not(f, f));
if (axioms.is_marked(f))
continue;
quick_for_each_expr(proc, visited, f);
}
}
void formula_compiler::assert_axiom(expr * f, bool neg) {
if (is_app(f)) {
if (to_app(f)->get_family_id() == m_a_util.get_family_id())
s.m_arith.assert_axiom(f, neg);
}
}
void formula_compiler::register_atom(expr * f, sat::bool_var p) {
if (is_app(f)) {
if (to_app(f)->get_family_id() == m_a_util.get_family_id())
s.m_arith.mk_atom(f, p);
}
}
void formula_compiler::compile_formulas(assertion_set const & assertions) {
ast_manager & m = assertions.m();
expr_fast_mark2 axioms;
mark_axioms(assertions, axioms);
unmark_nested_atoms(assertions, axioms);
ptr_vector<expr> formulas;
// send axioms to theories, and save formulas to compile
unsigned sz = assertions.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = assertions.form(i);
bool neg = false;
while (m.is_not(f, f))
neg = !neg;
if (axioms.is_marked(f)) {
assert_axiom(f, neg);
}
else {
formulas.push_back(f);
}
}
// compile formulas into sat::solver
m_to_sat(m, formulas.size(), formulas.c_ptr(), s.m_params, *(s.m_sat), s.m_atom2bvar);
// register atoms nested in the boolean structure in the theories
atom2bool_var::recent_iterator it = s.m_atom2bvar.begin_recent();
atom2bool_var::recent_iterator end = s.m_atom2bvar.end_recent();
for (; it != end; ++it) {
expr * atom = *it;
register_atom(atom, s.m_atom2bvar.to_bool_var(atom));
}
s.m_atom2bvar.reset_recent();
}
void formula_compiler::normalize() {
// make sure that the assertions are in the right format.
m_normalizer(s.m_assertions);
m_normalizer.cleanup();
}
void formula_compiler::elim_term_ite() {
if (has_term_ite(s.m_assertions)) {
model_converter_ref mc;
m_elim_ite(s.m_assertions, mc);
s.m_mc = concat(s.m_mc.get(), mc.get());
m_elim_ite.cleanup();
}
}
void formula_compiler::operator()() {
if (s.m_assertions.inconsistent())
return;
// normalization
elim_term_ite();
normalize();
TRACE("before_formula_compiler", s.m_assertions.display(tout););
s.init();
compile_formulas(s.m_assertions);
s.m_arith.preprocess();
TRACE("after_formula_compiler", s.display_state(tout););
}
void formula_compiler::updt_params(params_ref const & p) {
// TODO
}
void formula_compiler::collect_param_descrs(param_descrs & d) {
// TODO
}
void formula_compiler::collect_statistics(statistics & st) {
// TODO
}
void formula_compiler::reset_statistics() {
// TODO
}
void formula_compiler::set_cancel(bool f) {
m_normalizer.set_cancel(f);
m_elim_ite.set_cancel(f);
m_to_sat.set_cancel(f);
}
};

63
src/tactic/arith/dead/smt_formula_compiler.h
View file

@ -1,63 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_formula_compiler.h
Abstract:
Auxiliary class for smt::solver
Convert Exprs into Internal data-structures.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
--*/
#ifndef _SMT_FORMULA_COMPILER_H_
#define _SMT_FORMULA_COMPILER_H_
#include"smt_solver_types.h"
#include"assertion_set_rewriter.h"
#include"elim_term_ite_strategy.h"
#include"arith_decl_plugin.h"
#include"assertion_set2sat.h"
namespace smt {
class formula_compiler {
solver_exp & s;
arith_util m_a_util;
assertion_set_rewriter m_normalizer;
elim_term_ite_strategy m_elim_ite;
assertion_set2sat m_to_sat;
void normalize();
void elim_term_ite();
void mark_axioms(assertion_set const & s, expr_fast_mark2 & axioms);
void unmark_nested_atoms(assertion_set const & s, expr_fast_mark2 & axioms);
void assert_axiom(expr * f, bool neg);
void register_atom(expr * f, sat::bool_var p);
void compile_formulas(assertion_set const & assertions);
public:
formula_compiler(solver_exp & s, params_ref const & p);
~formula_compiler();
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);
void operator()();
void set_cancel(bool f);
void collect_statistics(statistics & st);
void reset_statistics();
};
};
#endif

232
src/tactic/arith/dead/smt_solver_exp.cpp
View file

@ -1,232 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_solver_exp.cpp
Abstract:
SMT solver using strategies and search on top of sat::solver
This solver uses assertion_set strategies during restarts.
It also uses the sat::solver to handle the Boolean structure of the problem.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
This was an experiment to rewrite Z3 kernel.
It will be deleted after we finish revamping Z3 kernel.
--*/
#include"smt_solver_exp.h"
#include"sat_solver.h"
#include"ast_translation.h"
#include"model.h"
namespace smt {
void solver_exp::bridge::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r) {
}
void solver_exp::bridge::asserted(sat::literal l) {
}
sat::check_result solver_exp::bridge::check() {
return sat::CR_DONE;
}
void solver_exp::bridge::push() {
}
void solver_exp::bridge::pop(unsigned n) {
}
void solver_exp::bridge::simplify() {
}
void solver_exp::bridge::clauses_modifed() {
}
lbool solver_exp::bridge::get_phase(sat::bool_var v) {
return l_undef;
}
solver_exp::solver_exp(ast_manager & ext_mng, params_ref const & p):
m_ext_mng(ext_mng),
m(ext_mng, true /* disable proof gen */),
m_compiler(*this, p),
m_assertions(m),
m_atom2bvar(m),
m_arith(m, p),
m_bridge(*this) {
updt_params_core(p);
m_cancel = false;
}
solver_exp::~solver_exp() {
}
void solver_exp::updt_params_core(params_ref const & p) {
m_params = p;
}
void solver_exp::updt_params(params_ref const & p) {
updt_params_core(p);
m_arith.updt_params(p);
if (m_sat)
m_sat->updt_params(p);
}
void solver_exp::collect_param_descrs(param_descrs & d) {
// TODO
}
void solver_exp::set_cancel(bool f) {
m_cancel = f;
#pragma omp critical (smt_solver_exp)
{
if (m_sat) {
m_sat->set_cancel(f);
}
}
m_arith.set_cancel(f);
m_compiler.set_cancel(f);
}
void solver_exp::init() {
m_atom2bvar.reset();
if (m_sat)
m_sat->collect_statistics(m_stats);
#pragma omp critical (smt_solver_exp)
{
m_sat = alloc(sat::solver, m_params, &m_bridge);
}
m_arith.collect_statistics(m_stats);
m_arith.reset();
set_cancel(m_cancel);
}
void solver_exp::assert_expr_core(expr * t, ast_translation & translator) {
expr * new_t = translator(t);
m_assertions.assert_expr(new_t);
}
/**
\brief Assert an expression t (owned by the external manager)
*/
void solver_exp::assert_expr(expr * t) {
ast_translation translator(m_ext_mng, m, false);
assert_expr_core(t, translator);
}
/**
\brief Assert an assertion set s (owned by the external manager)
*/
void solver_exp::assert_set(assertion_set const & s) {
SASSERT(&(s.m()) == &m_ext_mng);
ast_translation translator(m_ext_mng, m, false);
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
assert_expr_core(s.form(i), translator);
}
}
void solver_exp::assert_goal(goal const & g) {
SASSERT(&(g.m()) == &m_ext_mng);
ast_translation translator(m_ext_mng, m, false);
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
assert_expr_core(g.form(i), translator);
}
}
/**
\brief Store in r the current set of assertions.
r is (owned) by the external assertion set
*/
void solver_exp::get_assertions(assertion_set & r) {
SASSERT(&(r.m()) == &m_ext_mng);
ast_translation translator(m, m_ext_mng, false);
unsigned sz = m_assertions.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = m_assertions.form(i);
r.assert_expr(translator(f));
}
}
void solver_exp::get_model_converter(model_converter_ref & mc) {
ast_translation translator(m, m_ext_mng, false);
if (m_mc)
mc = m_mc->translate(translator);
else
mc = 0;
}
// -----------------------
//
// Search
//
// -----------------------
lbool solver_exp::check() {
compile();
lbool r = m_arith.check();
if (r == l_false)
return r;
if (m_sat->num_vars() == 0 && r == l_true) {
model_ref md = alloc(model, m);
m_arith.mk_model(md.get());
if (m_mc)
(*m_mc)(md);
ast_translation translator(m, m_ext_mng, false);
m_model = md->translate(translator);
return l_true;
}
return l_undef;
}
void solver_exp::compile() {
m_compiler();
}
// -----------------------
//
// Pretty Printing
//
// -----------------------
void solver_exp::display(std::ostream & out) const {
m_assertions.display(out);
}
void solver_exp::display_state(std::ostream & out) const {
if (m_sat) m_sat->display(out);
m_arith.display(out);
}
// -----------------------
//
// Statistics
//
// -----------------------
void solver_exp::collect_statistics(statistics & st) const {
solver_exp * _this = const_cast<solver_exp*>(this);
if (m_sat) {
m_sat->collect_statistics(_this->m_stats);
m_sat->reset_statistics();
}
m_arith.collect_statistics(_this->m_stats);
_this->m_arith.reset_statistics();
st.copy(m_stats);
}
void solver_exp::reset_statistics() {
m_stats.reset();
}
};

130
src/tactic/arith/dead/smt_solver_exp.h
View file

@ -1,130 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_solver_exp.h
Abstract:
SMT solver using strategies and search on top of sat::solver
This solver uses assertion_set strategies during restarts.
It also uses the sat::solver to handle the Boolean structure of the problem.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
This was an experiment to rewrite Z3 kernel.
It will be deleted after we finish revamping Z3 kernel.
--*/
#ifndef _SMT_SOLVER_EXP_H_
#define _SMT_SOLVER_EXP_H_
#include"smt_solver_types.h"
#include"model.h"
#include"model_converter.h"
#include"smt_formula_compiler.h"
#include"smt_arith.h"
#include"sat_extension.h"
#include"goal.h"
namespace smt {
class solver_exp {
friend class formula_compiler;
struct bridge : public sat::extension {
solver_exp & s;
bridge(solver_exp & _s):s(_s) {}
virtual void propagate(sat::literal l, sat::ext_constraint_idx idx, bool & keep) {}
virtual void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r);
virtual void asserted(sat::literal l);
virtual sat::check_result check();
virtual void push();
virtual void pop(unsigned n);
virtual void simplify();
virtual void clauses_modifed();
virtual lbool get_phase(sat::bool_var v);
};
// External ASTs are coming from m_ext_mng
ast_manager & m_ext_mng;
// The ASTs are translated into the internal manager for the following reasons:
// 1. We can run multiple smt::solver_exps in parallel with minimal synchronization
// 2. Minimize gaps in the AST ids.
ast_manager m; // internal manager
params_ref m_params;
formula_compiler m_compiler;
// Set of asserted expressions.
// This assertion set belongs to ast_manager m.
assertion_set m_assertions;
model_ref m_model;
model_converter_ref m_mc; // chain of model converters
atom2bool_var m_atom2bvar;
scoped_ptr<sat::solver> m_sat;
arith m_arith;
bridge m_bridge;
statistics m_stats;
volatile bool m_cancel;
void updt_params_core(params_ref const & p);
void assert_expr_core(expr * t, ast_translation & translator);
void init();
void compile();
public:
solver_exp(ast_manager & ext_mng, params_ref const & p);
~solver_exp();
void updt_params(params_ref const & p);
void collect_param_descrs(param_descrs & d);
void set_cancel(bool f);
void assert_expr(expr * t);
void assert_set(assertion_set const & s);
void assert_goal(goal const & g);
void get_assertions(assertion_set & r);
// -----------------------
//
// Search
//
// -----------------------
public:
lbool check();
void get_model(model_ref & m) const { m = m_model.get(); }
void get_model_converter(model_converter_ref & mc);
// -----------------------
//
// Pretty Printing
//
// -----------------------
public:
void display(std::ostream & out) const;
void display_state(std::ostream & out) const;
// -----------------------
//
// Statistics
//
// -----------------------
public:
void collect_statistics(statistics & st) const;
void reset_statistics();
};
};
#endif

47
src/tactic/arith/dead/smt_solver_types.h
View file

@ -1,47 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_solver_types.h
Abstract:
Auxiliary definitions for smt::solver class.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
This was an experiment to rewrite Z3 kernel.
It will be deleted after we finish revamping Z3 kernel.
--*/
#ifndef _SMT_SOLVER_TYPES_H_
#define _SMT_SOLVER_TYPES_H_
#include"assertion_set.h"
#include"strategy_exception.h"
#include"params.h"
#include"statistics.h"
#include"lbool.h"
#include"sat_types.h"
class ast_translation;
namespace sat {
class solver;
};
namespace smt {
class solver_exp;
class formula_compiler;
typedef unsigned atom_id;
typedef unsigned_vector atom_id_vector;
const atom_id null_atom_id = sat::null_bool_var;
};
MK_ST_EXCEPTION(smt_solver_exception);
#endif