mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

reorganizing the code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-23 21:53:34 -07:00
parent b89d35dd69
commit 9e299b88c4
101 changed files with 16 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

288
src/math/subpaving/subpaving.cpp Normal file
View file

@ -0,0 +1,288 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving.cpp
Abstract:
Subpaving for non-linear arithmetic.
This is a wrapper for the different implementations
of the subpaving module.
This wrapper is the main interface between Z3 other modules and subpaving.
Thus, it assumes that polynomials have precise integer coefficients, and
bounds are rationals. If a particular implementation uses floats, then
internally the bounds are approximated.
Author:
Leonardo de Moura (leonardo) 2012-08-07.
Revision History:
--*/
#include"subpaving.h"
#include"subpaving_types.h"
#include"subpaving_mpq.h"
#include"subpaving_mpf.h"
#include"subpaving_hwf.h"
#include"subpaving_mpff.h"
#include"subpaving_mpfx.h"
namespace subpaving {
template<typename CTX>
class context_wrapper : public context {
protected:
CTX m_ctx;
public:
context_wrapper(typename CTX::numeral_manager & m, params_ref const & p, small_object_allocator * a):m_ctx(m, p, a) {}
virtual ~context_wrapper() {}
virtual unsigned num_vars() const { return m_ctx.num_vars(); }
virtual var mk_var(bool is_int) { return m_ctx.mk_var(is_int); }
virtual bool is_int(var x) const { return m_ctx.is_int(x); }
virtual var mk_monomial(unsigned sz, power const * pws) { return m_ctx.mk_monomial(sz, pws); }
virtual void inc_ref(ineq * a) { m_ctx.inc_ref(reinterpret_cast<typename CTX::ineq*>(a)); }
virtual void dec_ref(ineq * a) { m_ctx.dec_ref(reinterpret_cast<typename CTX::ineq*>(a)); }
virtual void add_clause(unsigned sz, ineq * const * atoms) { m_ctx.add_clause(sz, reinterpret_cast<typename CTX::ineq * const *>(atoms)); }
virtual void display_constraints(std::ostream & out, bool use_star) const { m_ctx.display_constraints(out, use_star); }
virtual void set_cancel(bool f) { m_ctx.set_cancel(f); }
virtual void set_display_proc(display_var_proc * p) { m_ctx.set_display_proc(p); }
virtual void reset_statistics() { m_ctx.reset_statistics(); }
virtual void collect_statistics(statistics & st) const { m_ctx.collect_statistics(st); }
virtual void collect_param_descrs(param_descrs & r) { m_ctx.collect_param_descrs(r); }
virtual void updt_params(params_ref const & p) { m_ctx.updt_params(p); }
virtual void operator()() { m_ctx(); }
virtual void display_bounds(std::ostream & out) const { m_ctx.display_bounds(out); }
};
class context_mpq_wrapper : public context_wrapper<context_mpq> {
scoped_mpq m_c;
scoped_mpq_vector m_as;
public:
context_mpq_wrapper(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a):
context_wrapper<context_mpq>(m, p, a),
m_c(m),
m_as(m)
{}
virtual ~context_mpq_wrapper() {}
virtual unsynch_mpq_manager & qm() const { return m_ctx.nm(); }
virtual var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) {
m_as.reserve(sz);
for (unsigned i = 0; i < sz; i++) {
m_ctx.nm().set(m_as[i], as[i]);
}
m_ctx.nm().set(m_c, c);
return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs);
}
virtual ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) {
return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, k, lower, open));
}
};
class context_mpf_wrapper : public context_wrapper<context_mpf> {
f2n<mpf_manager> & m_fm;
unsynch_mpq_manager & m_qm;
scoped_mpf m_c;
scoped_mpf_vector m_as;
scoped_mpq m_q1, m_q2;
// Convert the mpz (integer) into a mpf, and throws an exception if the conversion is not precise.
void int2mpf(mpz const & a, mpf & o) {
m_qm.set(m_q1, a);
m_ctx.nm().set(o, m_q1);
m_ctx.nm().m().to_rational(o, m_q2);
if (!m_qm.eq(m_q1, m_q2))
throw subpaving::exception();
}
public:
context_mpf_wrapper(f2n<mpf_manager> & fm, params_ref const & p, small_object_allocator * a):
context_wrapper<context_mpf>(fm, p, a),
m_fm(fm),
m_qm(fm.m().mpq_manager()),
m_c(fm.m()),
m_as(fm.m()),
m_q1(m_qm),
m_q2(m_qm) {
}
virtual ~context_mpf_wrapper() {}
virtual unsynch_mpq_manager & qm() const { return m_qm; }
virtual var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) {
try {
m_as.reserve(sz);
for (unsigned i = 0; i < sz; i++) {
int2mpf(as[i], m_as[i]);
}
int2mpf(c, m_c);
return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs);
}
catch (f2n<mpf_manager>::exception) {
throw subpaving::exception();
}
}
virtual ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) {
try {
f2n<mpf_manager> & m = m_ctx.nm();
if (lower)
m.round_to_minus_inf();
else
m.round_to_plus_inf();
m.set(m_c, k);
return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, m_c, lower, open));
}
catch (f2n<mpf_manager>::exception) {
throw subpaving::exception();
}
}
};
class context_hwf_wrapper : public context_wrapper<context_hwf> {
f2n<hwf_manager> & m_fm;
unsynch_mpq_manager & m_qm;
hwf m_c;
svector<hwf> m_as;
// Convert the mpz (integer) into a hwf, and throws an exception if the conversion is not precise.
void int2hwf(mpz const & a, hwf & o) {
if (!m_qm.is_int64(a))
throw subpaving::exception();
int64 val = m_qm.get_int64(a);
double dval = static_cast<double>(val);
m_ctx.nm().set(o, dval);
double _dval = m_ctx.nm().m().to_double(o);
// TODO check the following test
if (static_cast<int64>(_dval) != val)
throw subpaving::exception();
}
public:
context_hwf_wrapper(f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
context_wrapper<context_hwf>(fm, p, a),
m_fm(fm),
m_qm(qm) {
}
virtual ~context_hwf_wrapper() {}
virtual unsynch_mpq_manager & qm() const { return m_qm; }
virtual var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) {
try {
m_as.reserve(sz);
for (unsigned i = 0; i < sz; i++) {
int2hwf(as[i], m_as[i]);
}
int2hwf(c, m_c);
return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs);
}
catch (f2n<mpf_manager>::exception) {
throw subpaving::exception();
}
}
virtual ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) {
try {
f2n<hwf_manager> & m = m_ctx.nm();
if (lower)
m.round_to_minus_inf();
else
m.round_to_plus_inf();
m.set(m_c, k);
return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, m_c, lower, open));
}
catch (f2n<mpf_manager>::exception) {
throw subpaving::exception();
}
}
};
template<typename context_fpoint>
class context_fpoint_wrapper : public context_wrapper<context_fpoint> {
unsynch_mpq_manager & m_qm;
_scoped_numeral<typename context_fpoint::numeral_manager> m_c;
_scoped_numeral_vector<typename context_fpoint::numeral_manager> m_as;
scoped_mpz m_z1, m_z2;
void int2fpoint(mpz const & a, typename context_fpoint::numeral & o) {
m_qm.set(m_z1, a);
this->m_ctx.nm().set(o, m_qm, m_z1);
this->m_ctx.nm().to_mpz(o, m_qm, m_z2);
if (!m_qm.eq(m_z1, m_z2))
throw subpaving::exception();
}
public:
context_fpoint_wrapper(typename context_fpoint::numeral_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
context_wrapper<context_fpoint>(m, p, a),
m_qm(qm),
m_c(m),
m_as(m),
m_z1(m_qm),
m_z2(m_qm) {
}
virtual ~context_fpoint_wrapper() {}
virtual unsynch_mpq_manager & qm() const { return m_qm; }
virtual var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) {
try {
m_as.reserve(sz);
for (unsigned i = 0; i < sz; i++) {
int2fpoint(as[i], m_as[i]);
}
int2fpoint(c, m_c);
return this->m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs);
}
catch (typename context_fpoint::numeral_manager::exception) {
throw subpaving::exception();
}
}
virtual ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) {
try {
typename context_fpoint::numeral_manager & m = this->m_ctx.nm();
if (lower)
m.round_to_minus_inf();
else
m.round_to_plus_inf();
m.set(m_c, m_qm, k);
return reinterpret_cast<ineq*>(this->m_ctx.mk_ineq(x, m_c, lower, open));
}
catch (typename context_fpoint::numeral_manager::exception) {
throw subpaving::exception();
}
}
};
typedef context_fpoint_wrapper<context_mpff> context_mpff_wrapper;
typedef context_fpoint_wrapper<context_mpfx> context_mpfx_wrapper;
context * mk_mpq_context(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpq_wrapper, m, p, a);
}
context * mk_mpf_context(f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpf_wrapper, m, p, a);
}
context * mk_hwf_context(f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
return alloc(context_hwf_wrapper, m, qm, p, a);
}
context * mk_mpff_context(mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpff_wrapper, m, qm, p, a);
}
context * mk_mpfx_context(mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpfx_wrapper, m, qm, p, a);
}
};

124
src/math/subpaving/subpaving.h Normal file
View file

@ -0,0 +1,124 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving.h
Abstract:
Subpaving for non-linear arithmetic.
This is a wrapper for the different implementations
of the subpaving module.
This wrapper is the main interface between Z3 other modules and subpaving.
Thus, it assumes that polynomials have precise integer coefficients, and
bounds are rationals. If a particular implementation uses floats, then
internally the bounds are approximated.
Author:
Leonardo de Moura (leonardo) 2012-08-07.
Revision History:
--*/
#ifndef __SUBPAVING_H_
#define __SUBPAVING_H_
#include"mpq.h"
#include"subpaving_types.h"
#include"params.h"
#include"statistics.h"
template<typename fmanager> class f2n;
class mpf_manager;
class hwf_manager;
class mpff_manager;
class mpfx_manager;
namespace subpaving {
class context {
public:
virtual ~context() {}
virtual unsynch_mpq_manager & qm() const = 0;
/**
\brief Return the number of variables in this subpaving object.
*/
virtual unsigned num_vars() const = 0;
/**
\brief Create a new variable.
*/
virtual var mk_var(bool is_int) = 0;
/**
\brief Return true if \c x is an integer variable.
*/
virtual bool is_int(var x) const = 0;
/**
\brief Create the monomial xs[0]^ks[0] * ... * xs[sz-1]^ks[sz-1].
The result is a variable y s.t. y = xs[0]^ks[0] * ... * xs[sz-1]^ks[sz-1].
\pre for all i \in [0, sz-1] : ks[i] > 0
\pre sz > 0
*/
virtual var mk_monomial(unsigned sz, power const * pws) = 0;
/**
\brief Create the sum c + as[0]*xs[0] + ... + as[sz-1]*xs[sz-1].
The result is a variable y s.t. y = c + as[0]*xs[0] + ... + as[sz-1]*xs[sz-1].
\pre sz > 0
\pre for all i \in [0, sz-1] : as[i] != 0
*/
virtual var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) = 0;
/**
\brief Create an inequality.
*/
virtual ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) = 0;
virtual void inc_ref(ineq * a) = 0;
virtual void dec_ref(ineq * a) = 0;
/**
\brief Assert the clause atoms[0] \/ ... \/ atoms[sz-1]
\pre sz >= 1
*/
virtual void add_clause(unsigned sz, ineq * const * atoms) = 0;
/**
\brief Display constraints asserted in the subpaving.
*/
virtual void display_constraints(std::ostream & out, bool use_star = false) const = 0;
virtual void set_cancel(bool f) = 0;
virtual void collect_param_descrs(param_descrs & r) = 0;
virtual void updt_params(params_ref const & p) = 0;
virtual void set_display_proc(display_var_proc * p) = 0;
virtual void reset_statistics() = 0;
virtual void collect_statistics(statistics & st) const = 0;
virtual void operator()() = 0;
virtual void display_bounds(std::ostream & out) const = 0;
};
context * mk_mpq_context(unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpf_context(f2n<mpf_manager> & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_hwf_context(f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpff_context(mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpfx_context(mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
};
#endif

23
src/math/subpaving/subpaving_hwf.cpp Normal file
View file

@ -0,0 +1,23 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_hwf.cpp
Abstract:
Subpaving for non-linear arithmetic using hardware floats.
Author:
Leonardo de Moura (leonardo) 2012-08-06.
Revision History:
--*/
#include"subpaving_hwf.h"
#include"subpaving_t_def.h"
// force template instantiation
template class subpaving::context_t<subpaving::config_hwf>;

48
src/math/subpaving/subpaving_hwf.h Normal file
View file

@ -0,0 +1,48 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_hwf.h
Abstract:
Subpaving for non-linear arithmetic using hardware floats.
Author:
Leonardo de Moura (leonardo) 2012-08-06.
Revision History:
--*/
#ifndef __SUBPAVING_HWF_H_
#define __SUBPAVING_HWF_H_
#include"subpaving_t.h"
#include"f2n.h"
#include"hwf.h"
namespace subpaving {
struct config_hwf {
f2n<hwf_manager> & m_manager;
public:
typedef f2n<hwf_manager> numeral_manager;
typedef f2n<hwf_manager>::exception exception;
static void round_to_minus_inf(numeral_manager & m) { m.round_to_minus_inf(); }
static void round_to_plus_inf(numeral_manager & m) { m.round_to_plus_inf(); }
static void set_rounding(numeral_manager & m, bool to_plus_inf) { m.set_rounding(to_plus_inf); }
config_hwf(f2n<hwf_manager> & m):m_manager(m) {}
f2n<hwf_manager> & m() const { return const_cast<f2n<hwf_manager> &>(m_manager); }
};
class context_hwf : public context_t<config_hwf> {
public:
context_hwf(f2n<hwf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_hwf>(config_hwf(m), p, a) {}
};
};
#endif

23
src/math/subpaving/subpaving_mpf.cpp Normal file
View file

@ -0,0 +1,23 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_mpf.cpp
Abstract:
Subpaving for non-linear arithmetic using multi-precision floats.
Author:
Leonardo de Moura (leonardo) 2012-07-31.
Revision History:
--*/
#include"subpaving_mpf.h"
#include"subpaving_t_def.h"
// force template instantiation
template class subpaving::context_t<subpaving::config_mpf>;

49
src/math/subpaving/subpaving_mpf.h Normal file
View file

@ -0,0 +1,49 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_mpf.h
Abstract:
Subpaving for non-linear arithmetic using multi-precision floats.
Author:
Leonardo de Moura (leonardo) 2012-07-31.
Revision History:
--*/
#ifndef __SUBPAVING_MPF_H_
#define __SUBPAVING_MPF_H_
#include"subpaving_t.h"
#include"mpf.h"
#include"f2n.h"
namespace subpaving {
struct config_mpf {
f2n<mpf_manager> & m_manager;
public:
typedef f2n<mpf_manager> numeral_manager;
typedef mpf numeral;
typedef f2n<mpf_manager>::exception exception;
static void round_to_minus_inf(numeral_manager & m) { m.round_to_minus_inf(); }
static void round_to_plus_inf(numeral_manager & m) { m.round_to_plus_inf(); }
static void set_rounding(numeral_manager & m, bool to_plus_inf) { m.set_rounding(to_plus_inf); }
config_mpf(f2n<mpf_manager> & m):m_manager(m) {}
f2n<mpf_manager> & m() const { return const_cast<f2n<mpf_manager> &>(m_manager); }
};
class context_mpf : public context_t<config_mpf> {
public:
context_mpf(f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_mpf>(config_mpf(m), p, a) {}
};
};
#endif

23
src/math/subpaving/subpaving_mpff.cpp Normal file
View file

@ -0,0 +1,23 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_mpff.cpp
Abstract:
Subpaving for non-linear arithmetic using mpff numerals.
Author:
Leonardo de Moura (leonardo) 2012-09-18.
Revision History:
--*/
#include"subpaving_mpff.h"
#include"subpaving_t_def.h"
// force template instantiation
template class subpaving::context_t<subpaving::config_mpff>;

45
src/math/subpaving/subpaving_mpff.h Normal file
View file

@ -0,0 +1,45 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_mpff.h
Abstract:
Subpaving for non-linear arithmetic using mpff numerals
Author:
Leonardo de Moura (leonardo) 2012-09-18.
Revision History:
--*/
#ifndef __SUBPAVING_MPFF_H_
#define __SUBPAVING_MPFF_H_
#include"subpaving_t.h"
#include"mpff.h"
namespace subpaving {
struct config_mpff {
typedef mpff_manager numeral_manager;
typedef mpff_manager::exception exception;
static void round_to_minus_inf(numeral_manager & m) { m.round_to_minus_inf(); }
static void round_to_plus_inf(numeral_manager & m) { m.round_to_plus_inf(); }
static void set_rounding(numeral_manager & m, bool to_plus_inf) { m.set_rounding(to_plus_inf); }
numeral_manager & m_manager;
config_mpff(numeral_manager & m):m_manager(m) {}
numeral_manager & m() const { return m_manager; }
};
typedef context_t<config_mpff> context_mpff;
};
#endif

23
src/math/subpaving/subpaving_mpfx.cpp Normal file
View file

@ -0,0 +1,23 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_mpfx.cpp
Abstract:
Subpaving for non-linear arithmetic using mpfx numerals.
Author:
Leonardo de Moura (leonardo) 2012-09-18.
Revision History:
--*/
#include"subpaving_mpfx.h"
#include"subpaving_t_def.h"
// force template instantiation
template class subpaving::context_t<subpaving::config_mpfx>;

45
src/math/subpaving/subpaving_mpfx.h Normal file
View file

@ -0,0 +1,45 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_mpfx.h
Abstract:
Subpaving for non-linear arithmetic using mpfx numerals
Author:
Leonardo de Moura (leonardo) 2012-09-20.
Revision History:
--*/
#ifndef __SUBPAVING_MPFX_H_
#define __SUBPAVING_MPFX_H_
#include"subpaving_t.h"
#include"mpfx.h"
namespace subpaving {
struct config_mpfx {
typedef mpfx_manager numeral_manager;
typedef mpfx_manager::exception exception;
static void round_to_minus_inf(numeral_manager & m) { m.round_to_minus_inf(); }
static void round_to_plus_inf(numeral_manager & m) { m.round_to_plus_inf(); }
static void set_rounding(numeral_manager & m, bool to_plus_inf) { m.set_rounding(to_plus_inf); }
numeral_manager & m_manager;
config_mpfx(numeral_manager & m):m_manager(m) {}
numeral_manager & m() const { return m_manager; }
};
typedef context_t<config_mpfx> context_mpfx;
};
#endif

23
src/math/subpaving/subpaving_mpq.cpp Normal file
View file

@ -0,0 +1,23 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_mpq.cpp
Abstract:
Subpaving for non-linear arithmetic using rationals.
Author:
Leonardo de Moura (leonardo) 2012-07-31.
Revision History:
--*/
#include"subpaving_mpq.h"
#include"subpaving_t_def.h"
// force template instantiation
template class subpaving::context_t<subpaving::config_mpq>;

43
src/math/subpaving/subpaving_mpq.h Normal file
View file

@ -0,0 +1,43 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_mpq.h
Abstract:
Subpaving for non-linear arithmetic using rationals
Author:
Leonardo de Moura (leonardo) 2012-07-31.
Revision History:
--*/
#ifndef __SUBPAVING_MPQ_H_
#define __SUBPAVING_MPQ_H_
#include"subpaving_t.h"
#include"mpq.h"
namespace subpaving {
struct config_mpq {
typedef unsynch_mpq_manager numeral_manager;
struct exception {};
static void round_to_minus_inf(numeral_manager & m) {}
static void round_to_plus_inf(numeral_manager & m) {}
static void set_rounding(numeral_manager & m, bool to_plus_info) {}
numeral_manager & m_manager;
config_mpq(numeral_manager & m):m_manager(m) {}
numeral_manager & m() const { return m_manager; }
};
typedef context_t<config_mpq> context_mpq;
};
#endif

853
src/math/subpaving/subpaving_t.h Normal file
View file

@ -0,0 +1,853 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_t.h
Abstract:
Subpaving template for non-linear arithmetic.
Author:
Leonardo de Moura (leonardo) 2012-07-31.
Revision History:
--*/
#ifndef __SUBPAVING_T_H_
#define __SUBPAVING_T_H_
#include<iostream>
#include"tptr.h"
#include"small_object_allocator.h"
#include"chashtable.h"
#include"parray.h"
#include"interval.h"
#include"scoped_numeral_vector.h"
#include"subpaving_types.h"
#include"params.h"
#include"statistics.h"
#include"lbool.h"
#include"id_gen.h"
#ifdef _MSC_VER
#pragma warning(disable : 4200)
#pragma warning(disable : 4355)
#endif
namespace subpaving {
template<typename C>
class context_t {
public:
typedef typename C::numeral_manager numeral_manager;
typedef typename numeral_manager::numeral numeral;
/**
\brief Inequalities used to encode a problem.
*/
class ineq {
friend class context_t;
var m_x;
numeral m_val;
unsigned m_ref_count:30;
unsigned m_lower:1;
unsigned m_open:1;
public:
var x() const { return m_x; }
numeral const & value() const { return m_val; }
bool is_lower() const { return m_lower; }
bool is_open() const { return m_open; }
void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc = display_var_proc());
struct lt_var_proc { bool operator()(ineq const * a, ineq const * b) const { return a->m_x < b->m_x; } };
};
class node;
class constraint {
public:
enum kind {
CLAUSE, MONOMIAL, POLYNOMIAL
// TODO: add SIN, COS, TAN, ...
};
protected:
kind m_kind;
uint64 m_timestamp;
public:
constraint(kind k):m_kind(k), m_timestamp(0) {}
kind get_kind() const { return m_kind; }
// Return the timestamp of the last propagation visit
uint64 timestamp() const { return m_timestamp; }
// Reset propagation visit time
void set_visited(uint64 ts) { m_timestamp = ts; }
};
/**
\brief Clauses in the problem description and lemmas learned during paving.
*/
class clause : public constraint {
friend class context_t;
unsigned m_size; //!< Number of atoms in the clause.
unsigned m_lemma:1; //!< True if it is a learned clause.
unsigned m_watched:1; //!< True if it we are watching this clause. All non-lemmas are watched.
unsigned m_num_jst:30; //!< Number of times it is used to justify some bound.
ineq * m_atoms[0];
static unsigned get_obj_size(unsigned sz) { return sizeof(clause) + sz*sizeof(ineq*); }
public:
clause():constraint(constraint::CLAUSE) {}
unsigned size() const { return m_size; }
bool watched() const { return m_watched; }
ineq * operator[](unsigned i) const { SASSERT(i < size()); return m_atoms[i]; }
void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc = display_var_proc());
};
class justification {
void * m_data;
public:
enum kind {
AXIOM = 0,
ASSUMPTION,
CLAUSE,
VAR_DEF
};
justification(bool axiom = true) {
m_data = axiom ? reinterpret_cast<void*>(static_cast<size_t>(AXIOM)) : reinterpret_cast<void*>(static_cast<size_t>(ASSUMPTION));
}
justification(justification const & source) { m_data = source.m_data; }
explicit justification(clause * c) { m_data = TAG(void*, c, CLAUSE); }
explicit justification(var x) { m_data = BOXTAGINT(void*, x, VAR_DEF); }
kind get_kind() const { return static_cast<kind>(GET_TAG(m_data)); }
bool is_clause() const { return get_kind() == CLAUSE; }
bool is_axiom() const { return get_kind() == AXIOM; }
bool is_assumption() const { return get_kind() == ASSUMPTION; }
bool is_var_def() const { return get_kind() == VAR_DEF; }
clause * get_clause() const {
SASSERT(is_clause());
return UNTAG(clause*, m_data);
}
var get_var() const {
SASSERT(is_var_def());
return UNBOXINT(m_data);
}
bool operator==(justification const & other) const { return m_data == other.m_data; }
bool operator!=(justification const & other) const { return !operator==(other); }
};
class bound {
friend class context_t;
numeral m_val;
unsigned m_x:29;
unsigned m_lower:1;
unsigned m_open:1;
unsigned m_mark:1;
uint64 m_timestamp;
bound * m_prev;
justification m_jst;
void set_timestamp(uint64 ts) { m_timestamp = ts; }
public:
var x() const { return static_cast<var>(m_x); }
numeral const & value() const { return m_val; }
numeral & value() { return m_val; }
bool is_lower() const { return m_lower; }
bool is_open() const { return m_open; }
uint64 timestamp() const { return m_timestamp; }
bound * prev() const { return m_prev; }
justification jst() const { return m_jst; }
void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc = display_var_proc());
};
struct bound_array_config {
typedef context_t value_manager;
typedef small_object_allocator allocator;
typedef bound * value;
static const bool ref_count = false;
static const bool preserve_roots = true;
static const unsigned max_trail_sz = 16;
static const unsigned factor = 2;
};
// auxiliary declarations for parray_manager
void dec_ref(bound *) {}
void inc_ref(bound *) {}
typedef parray_manager<bound_array_config> bound_array_manager;
typedef typename bound_array_manager::ref bound_array;
/**
\brief Node in the context_t.
*/
class node {
bound_array_manager & m_bm;
bound_array m_lowers;
bound_array m_uppers;
var m_conflict;
unsigned m_id;
unsigned m_depth;
bound * m_trail;
node * m_parent; //!< parent node
node * m_first_child;
node * m_next_sibling;
// Doubly linked list of leaves to be processed
node * m_prev;
node * m_next;
public:
node(context_t & s, unsigned id);
node(node * parent, unsigned id);
// return unique indentifier.
unsigned id() const { return m_id; }
bound_array_manager & bm() const { return m_bm; }
bound_array & lowers() { return m_lowers; }
bound_array & uppers() { return m_uppers; }
bool inconsistent() const { return m_conflict != null_var; }
void set_conflict(var x) { SASSERT(!inconsistent()); m_conflict = x; }
bound * trail_stack() const { return m_trail; }
bound * parent_trail_stack() const { return m_parent == 0 ? 0 : m_parent->m_trail; }
bound * lower(var x) const { return bm().get(m_lowers, x); }
bound * upper(var x) const { return bm().get(m_uppers, x); }
node * parent() const { return m_parent; }
node * first_child() const { return m_first_child; }
node * next_sibling() const { return m_next_sibling; }
node * prev() const { return m_prev; }
node * next() const { return m_next; }
/**
\brief Return true if x is unbounded in this node
*/
bool is_unbounded(var x) const { return lower(x) == 0 && upper(x) == 0; }
void push(bound * b);
void set_first_child(node * n) { m_first_child = n; }
void set_next_sibling(node * n) { m_next_sibling = n; }
void set_next(node * n) { m_next = n; }
void set_prev(node * n) { m_prev = n; }
unsigned depth() const { return m_depth; }
};
/**
\brief Intervals are just temporary place holders.
The pavers maintain bounds.
*/
struct interval {
bool m_constant; // Flag: constant intervals are pairs <node*, var>
// constant intervals
node * m_node;
var m_x;
// mutable intervals
numeral m_l_val;
bool m_l_inf;
bool m_l_open;
numeral m_u_val;
bool m_u_inf;
bool m_u_open;
interval():m_constant(false) {}
void set_constant(node * n, var x) {
m_constant = true;
m_node = n;
m_x = x;
}
void set_mutable() { m_constant = false; }
};
class interval_config {
public:
typedef typename C::numeral_manager numeral_manager;
typedef typename numeral_manager::numeral numeral;
typedef typename context_t::interval interval;
private:
numeral_manager & m_manager;
public:
interval_config(numeral_manager & m):m_manager(m) {}
numeral_manager & m() const { return m_manager; }
void round_to_minus_inf() { C::round_to_minus_inf(m()); }
void round_to_plus_inf() { C::round_to_plus_inf(m()); }
void set_rounding(bool to_plus_inf) { C::set_rounding(m(), to_plus_inf); }
numeral const & lower(interval const & a) const {
if (a.m_constant) {
bound * b = a.m_node->lower(a.m_x);
return b == 0 ? a.m_l_val /* don't care */ : b->value();
}
return a.m_l_val;
}
numeral const & upper(interval const & a) const {
if (a.m_constant) {
bound * b = a.m_node->upper(a.m_x);
return b == 0 ? a.m_u_val /* don't care */ : b->value();
}
return a.m_u_val;
}
numeral & lower(interval & a) { SASSERT(!a.m_constant); return a.m_l_val; }
numeral & upper(interval & a) { SASSERT(!a.m_constant); return a.m_u_val; }
bool lower_is_inf(interval const & a) const { return a.m_constant ? a.m_node->lower(a.m_x) == 0 : a.m_l_inf; }
bool upper_is_inf(interval const & a) const { return a.m_constant ? a.m_node->upper(a.m_x) == 0 : a.m_u_inf; }
bool lower_is_open(interval const & a) const {
if (a.m_constant) {
bound * b = a.m_node->lower(a.m_x);
return b == 0 || b->is_open();
}
return a.m_l_open;
}
bool upper_is_open(interval const & a) const {
if (a.m_constant) {
bound * b = a.m_node->upper(a.m_x);
return b == 0 || b->is_open();
}
return a.m_u_open;
}
// Setters
void set_lower(interval & a, numeral const & n) { SASSERT(!a.m_constant); m().set(a.m_l_val, n); }
void set_upper(interval & a, numeral const & n) { SASSERT(!a.m_constant); m().set(a.m_u_val, n); }
void set_lower_is_open(interval & a, bool v) { SASSERT(!a.m_constant); a.m_l_open = v; }
void set_upper_is_open(interval & a, bool v) { SASSERT(!a.m_constant); a.m_u_open = v; }
void set_lower_is_inf(interval & a, bool v) { SASSERT(!a.m_constant); a.m_l_inf = v; }
void set_upper_is_inf(interval & a, bool v) { SASSERT(!a.m_constant); a.m_u_inf = v; }
};
typedef ::interval_manager<interval_config> interval_manager;
class definition : public constraint {
public:
definition(typename constraint::kind k):constraint(k) {}
};
class monomial : public definition {
friend class context_t;
unsigned m_size;
power m_powers[0];
monomial(unsigned sz, power const * pws);
static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz*sizeof(power); }
public:
unsigned size() const { return m_size; }
power const & get_power(unsigned idx) const { SASSERT(idx < size()); return m_powers[idx]; }
power const * get_powers() const { return m_powers; }
var x(unsigned idx) const { return get_power(idx).x(); }
unsigned degree(unsigned idx) const { return get_power(idx).degree(); }
void display(std::ostream & out, display_var_proc const & proc = display_var_proc(), bool use_star = false) const;
};
class polynomial : public definition {
friend class context_t;
unsigned m_size;
numeral m_c;
numeral * m_as;
var * m_xs;
static unsigned get_obj_size(unsigned sz) { return sizeof(polynomial) + sz*sizeof(numeral) + sz*sizeof(var); }
public:
polynomial():definition(constraint::POLYNOMIAL) {}
unsigned size() const { return m_size; }
numeral const & a(unsigned i) const { return m_as[i]; }
var x(unsigned i) const { return m_xs[i]; }
var const * xs() const { return m_xs; }
numeral const * as() const { return m_as; }
numeral const & c() const { return m_c; }
void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc = display_var_proc(), bool use_star = false) const;
};
/**
\brief Watched element (aka occurence) can be:
- A clause
- A definition (i.e., a variable)
Remark: we cannot use the two watched literal approach since we process multiple nodes.
*/
class watched {
public:
enum kind { CLAUSE=0, DEFINITION };
private:
void * m_data;
public:
watched():m_data(0) {}
explicit watched(var x) { m_data = BOXTAGINT(void*, x, DEFINITION); }
explicit watched(clause * c) { m_data = TAG(void*, c, CLAUSE); }
kind get_kind() const { return static_cast<kind>(GET_TAG(m_data)); }
bool is_clause() const { return get_kind() != DEFINITION; }
bool is_definition() const { return get_kind() == DEFINITION; }
clause * get_clause() const { SASSERT(is_clause()); return UNTAG(clause*, m_data); }
var get_var() const { SASSERT(is_definition()); return UNBOXINT(m_data); }
bool operator==(watched const & other) const { return m_data == other.m_data; }
bool operator!=(watched const & other) const { return !operator==(other); }
};
/**
\brief Abstract functor for selecting the next leaf node to be explored.
*/
class node_selector {
context_t * m_ctx;
public:
node_selector(context_t * ctx):m_ctx(ctx) {}
virtual ~node_selector() {}
context_t * ctx() const { return m_ctx; }
// Return the next leaf node to be processed.
// Front and back are the first and last nodes in the doubly linked list of
// leaf nodes.
// Remark: new nodes are always inserted in the front of the list.
virtual node * operator()(node * front, node * back) = 0;
};
/**
\brief Abstract functor for selecting the next variable to branch.
*/
class var_selector {
context_t * m_ctx;
public:
var_selector(context_t * ctx):m_ctx(ctx) {}
virtual ~var_selector() {}
context_t * ctx() const { return m_ctx; }
// Return the next variable to branch.
virtual var operator()(node * n) = 0;
// -----------------------------------
//
// Event handlers
//
// -----------------------------------
// Invoked when a new variable is created.
virtual void new_var_eh(var x) {}
// Invoked when node n is created
virtual void new_node_eh(node * n) {}
// Invoked before deleting node n.
virtual void del_node_eh(node * n) {}
// Invoked when variable x is used during conflict resolution.
virtual void used_var_eh(node * n, var x) {}
};
class node_splitter;
friend class node_splitter;
/**
\brief Abstract functor for creating children for node n by branching on a given variable.
*/
class node_splitter {
context_t * m_ctx;
public:
node_splitter(context_t * ctx):m_ctx(ctx) {}
virtual ~node_splitter() {}
context_t * ctx() const { return m_ctx; }
node * mk_node(node * p) { return ctx()->mk_node(p); }
bound * mk_decided_bound(var x, numeral const & val, bool lower, bool open, node * n) {
return ctx()->mk_bound(x, val, lower, open, n, justification());
}
/**
\brief Create children nodes for n by splitting on x.
\pre n is a leaf. The interval for x in n has more than one element.
*/
virtual void operator()(node * n, var x) = 0;
};
/**
\brief Return most recent splitting var for node n.
*/
var splitting_var(node * n) const;
/**
\brief Return true if x is a definition.
*/
bool is_definition(var x) const { return m_defs[x] != 0; }
typedef svector<watched> watch_list;
typedef _scoped_numeral_vector<numeral_manager> scoped_numeral_vector;
private:
C m_c;
bool m_arith_failed; //!< True if the arithmetic module produced an exception.
bool m_own_allocator;
small_object_allocator * m_allocator;
bound_array_manager m_bm;
interval_manager m_im;
scoped_numeral_vector m_num_buffer;
svector<bool> m_is_int;
ptr_vector<definition> m_defs;
vector<watch_list> m_wlist;
ptr_vector<ineq> m_unit_clauses;
ptr_vector<clause> m_clauses;
ptr_vector<clause> m_lemmas;
id_gen m_node_id_gen;
uint64 m_timestamp;
node * m_root;
// m_leaf_head is the head of a doubly linked list of leaf nodes to be processed.
node * m_leaf_head;
node * m_leaf_tail;
var m_conflict;
ptr_vector<bound> m_queue;
unsigned m_qhead;
display_var_proc m_default_display_proc;
display_var_proc * m_display_proc;
scoped_ptr<node_selector> m_node_selector;
scoped_ptr<var_selector> m_var_selector;
scoped_ptr<node_splitter> m_node_splitter;
svector<power> m_pws;
// Configuration
numeral m_epsilon; //!< If upper - lower < epsilon, then new bound is not propagated.
bool m_zero_epsilon;
numeral m_max_bound; //!< Bounds > m_max and < -m_max are not propagated
numeral m_minus_max_bound; //!< -m_max_bound
numeral m_nth_root_prec; //!< precision for computing the nth root
unsigned m_max_depth; //!< Maximum depth
unsigned m_max_nodes; //!< Maximum number of nodes in the tree
unsigned long long m_max_memory; // in bytes
// Counters
unsigned m_num_nodes;
// Statistics
unsigned m_num_conflicts;
unsigned m_num_mk_bounds;
unsigned m_num_splits;
unsigned m_num_visited;
// Temporary
numeral m_tmp1, m_tmp2, m_tmp3;
interval m_i_tmp1, m_i_tmp2, m_i_tmp3;
// Cancel flag
volatile bool m_cancel;
friend class node;
void set_arith_failed() { m_arith_failed = true; }
void checkpoint();
bound_array_manager & bm() { return m_bm; }
interval_manager & im() { return m_im; }
small_object_allocator & allocator() const { return *m_allocator; }
bound * mk_bound(var x, numeral const & val, bool lower, bool open, node * n, justification jst);
void del_bound(bound * b);
// Create a new bound and add it to the propagation queue.
void propagate_bound(var x, numeral const & val, bool lower, bool open, node * n, justification jst);
bool is_int(monomial const * m) const;
bool is_int(polynomial const * p) const;
bool is_monomial(var x) const { return m_defs[x] != 0 && m_defs[x]->get_kind() == constraint::MONOMIAL; }
monomial * get_monomial(var x) const { SASSERT(is_monomial(x)); return static_cast<monomial*>(m_defs[x]); }
bool is_polynomial(var x) const { return m_defs[x] != 0 && m_defs[x]->get_kind() == constraint::POLYNOMIAL; }
polynomial * get_polynomial(var x) const { SASSERT(is_polynomial(x)); return static_cast<polynomial*>(m_defs[x]); }
static void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc, var x, numeral & k, bool lower, bool open);
void display(std::ostream & out, var x) const;
void display_definition(std::ostream & out, definition const * d, bool use_star = false) const;
void display(std::ostream & out, constraint * a, bool use_star = false) const;
void display(std::ostream & out, bound * b) const;
void display(std::ostream & out, ineq * a) const;
void display_params(std::ostream & out) const;
void add_unit_clause(ineq * a, bool axiom);
// Remark: Not all lemmas need to be watched. Some of them can be used to justify clauses only.
void add_clause_core(unsigned sz, ineq * const * atoms, bool lemma, bool watched);
void del_clause(clause * cls);
node * mk_node(node * parent = 0);
void del_node(node * n);
void del_nodes();
void del(interval & a);
void del_clauses(ptr_vector<clause> & cs);
void del_unit_clauses();
void del_clauses();
void del_monomial(monomial * m);
void del_sum(polynomial * p);
void del_definitions();
/**
\brief Insert n in the beginning of the doubly linked list of leaves.
\pre n is a leaf, and it is not already in the list.
*/
void push_front(node * n);
/**
\brief Insert n in the end of the doubly linked list of leaves.
\pre n is a leaf, and it is not already in the list.
*/
void push_back(node * n);
/**
\brief Remove n from the doubly linked list of leaves.
\pre n is a leaf, and it is in the list.
*/
void remove_from_leaf_dlist(node * n);
/**
\brief Remove all nodes from the leaf dlist.
*/
void reset_leaf_dlist();
/**
\brief Add all leaves back to the leaf dlist.
*/
void rebuild_leaf_dlist(node * n);
// -----------------------------------
//
// Propagation
//
// -----------------------------------
/**
\brief Return true if the given node is in an inconsistent state.
*/
bool inconsistent(node * n) const { return n->inconsistent(); }
/**
\brief Set a conflict produced by the bounds of x at the given node.
*/
void set_conflict(var x, node * n);
/**
\brief Return true if bound b may propagate a new bound using constraint c at node n.
*/
bool may_propagate(bound * b, constraint * c, node * n);
/**
\brief Normalize bound if x is integer.
Examples:
x < 2 --> x <= 1
x <= 2.3 --> x <= 2
*/
void normalize_bound(var x, numeral & val, bool lower, bool & open);
/**
\brief Return true if (x, k, lower, open) is a relevant new bound at node n.
That is, it improves the current bound, and satisfies m_epsilon and m_max_bound.
*/
bool relevant_new_bound(var x, numeral const & k, bool lower, bool open, node * n);
/**
\brief Return true if the lower and upper bounds of x are 0 at node n.
*/
bool is_zero(var x, node * n) const;
/**
\brief Return true if upper bound of x is 0 at node n.
*/
bool is_upper_zero(var x, node * n) const;
/**
\brief Return true if lower and upper bounds of x are conflicting at node n. That is, upper(x) < lower(x)
*/
bool conflicting_bounds(var x, node * n) const;
/**
\brief Return true if x is unbounded at node n.
*/
bool is_unbounded(var x, node * n) const { return n->is_unbounded(x); }
/**
\brief Return true if b is the most recent lower/upper bound for variable b->x() at node n.
*/
bool most_recent(bound * b, node * n) const;
/**
\brief Add most recent bounds of node n into the propagation queue.
That is, all bounds b s.t. b is in the trail of n, but not in the tail of parent(n), and most_recent(b, n).
*/
void add_recent_bounds(node * n);
/**
\brief Propagate new bounds at node n using get_monomial(x)
\pre is_monomial(x)
*/
void propagate_monomial(var x, node * n);
void propagate_monomial_upward(var x, node * n);
void propagate_monomial_downward(var x, node * n, unsigned i);
/**
\brief Propagate new bounds at node n using get_polynomial(x)
\pre is_polynomial(x)
*/
void propagate_polynomial(var x, node * n);
// Propagate a new bound for y using the polynomial associated with x. x may be equal to y.
void propagate_polynomial(var x, node * n, var y);
/**
\brief Propagate new bounds at node n using clause c.
*/
void propagate_clause(clause * c, node * n);
/**
\brief Return the truth value of inequaliy t at node n.
*/
lbool value(ineq * t, node * n);
/**
\brief Propagate new bounds at node n using the definition of variable x.
\pre is_definition(x)
*/
void propagate_def(var x, node * n);
/**
\brief Propagate constraints in b->x()'s watch list.
*/
void propagate(node * n, bound * b);
/**
\brief Perform bound propagation at node n.
*/
void propagate(node * n);
/**
\brief Try to propagate at node n using all definitions.
*/
void propagate_all_definitions(node * n);
// -----------------------------------
//
// Main
//
// -----------------------------------
void init();
/**
\brief Assert unit clauses in the node n.
*/
void assert_units(node * n);
// -----------------------------------
//
// Debugging support
//
// -----------------------------------
/**
\brief Return true if b is a bound for node n.
*/
bool is_bound_of(bound * b, node * n) const;
/**
\brief Check the consistency of the doubly linked list of leaves.
*/
bool check_leaf_dlist() const;
/**
\brief Check paving tree structure.
*/
bool check_tree() const;
/**
\brief Check main invariants.
*/
bool check_invariant() const;
public:
context_t(C const & c, params_ref const & p, small_object_allocator * a);
~context_t();
/**
\brief Return true if the arithmetic module failed.
*/
bool arith_failed() const { return m_arith_failed; }
numeral_manager & nm() const { return m_c.m(); }
unsigned num_vars() const { return m_is_int.size(); }
bool is_int(var x) const { SASSERT(x < num_vars()); return m_is_int[x]; }
/**
\brief Create a new variable.
*/
var mk_var(bool is_int);
/**
\brief Create the monomial xs[0]^ks[0] * ... * xs[sz-1]^ks[sz-1].
The result is a variable y s.t. y = xs[0]^ks[0] * ... * xs[sz-1]^ks[sz-1].
\pre for all i \in [0, sz-1] : ks[i] > 0
\pre sz > 0
*/
var mk_monomial(unsigned sz, power const * pws);
/**
\brief Create the sum c + as[0]*xs[0] + ... + as[sz-1]*xs[sz-1].
The result is a variable y s.t. y = c + as[0]*xs[0] + ... + as[sz-1]*xs[sz-1].
\pre sz > 0
\pre for all i \in [0, sz-1] : as[i] != 0
*/
var mk_sum(numeral const & c, unsigned sz, numeral const * as, var const * xs);
/**
\brief Create an inequality.
*/
ineq * mk_ineq(var x, numeral const & k, bool lower, bool open);
void inc_ref(ineq * a);
void dec_ref(ineq * a);
/**
\brief Assert the clause atoms[0] \/ ... \/ atoms[sz-1]
\pre sz > 1
*/
void add_clause(unsigned sz, ineq * const * atoms) { add_clause_core(sz, atoms, false, true); }
/**
\brief Assert a constraint of one of the forms: x < k, x > k, x <= k, x >= k.
If axiom == true, then the constraint is not tracked in proofs.
*/
void add_ineq(var x, numeral const & k, bool lower, bool open, bool axiom);
/**
\brief Store in the given vector all leaves of the paving tree.
*/
void collect_leaves(ptr_vector<node> & leaves) const;
/**
\brief Display constraints asserted in the subpaving.
*/
void display_constraints(std::ostream & out, bool use_star = false) const;
/**
\brief Display bounds for each leaf of the tree.
*/
void display_bounds(std::ostream & out) const;
void display_bounds(std::ostream & out, node * n) const;
void set_display_proc(display_var_proc * p) { m_display_proc = p; }
void set_cancel(bool f) { m_cancel = f; im().set_cancel(f); }
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);
void reset_statistics();
void collect_statistics(statistics & st) const;
void operator()();
};
};
#endif

1942
src/math/subpaving/subpaving_t_def.h Normal file
View file

File diff suppressed because it is too large Load diff

52
src/math/subpaving/subpaving_types.h Normal file
View file

@ -0,0 +1,52 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_types.h
Abstract:
Subpaving auxiliary types.
Author:
Leonardo de Moura (leonardo) 2012-08-07.
Revision History:
--*/
#ifndef __SUBPAVING_TYPES_H_
#define __SUBPAVING_TYPES_H_
namespace subpaving {
class ineq;
typedef unsigned var;
const var null_var = UINT_MAX;
class exception {
};
class power : public std::pair<var, unsigned> {
public:
power():std::pair<var, unsigned>() {}
power(var v, unsigned d):std::pair<var, unsigned>(v, d) {}
power(power const & p):std::pair<var, unsigned>(p) {}
var x() const { return first; }
var get_var() const { return first; }
unsigned degree() const { return second; }
unsigned & degree() { return second; }
void set_var(var x) { first = x; }
struct lt_proc { bool operator()(power const & p1, power const & p2) { return p1.get_var() < p2.get_var(); } };
};
struct display_var_proc {
virtual void operator()(std::ostream & out, var x) const { out << "x" << x; }
};
};
#endif

395
src/math/subpaving/tactic/expr2subpaving.cpp Normal file
View file

@ -0,0 +1,395 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
expr2subpaving.cpp
Abstract:
Translator from Z3 expressions into generic subpaving data-structure.
Author:
Leonardo (leonardo) 2012-08-08
Notes:
--*/
#include"expr2subpaving.h"
#include"expr2var.h"
#include"ref_util.h"
#include"z3_exception.h"
#include"cooperate.h"
#include"arith_decl_plugin.h"
#include"scoped_numeral_buffer.h"
struct expr2subpaving::imp {
struct frame {
app * m_curr;
unsigned m_idx;
frame():m_curr(0), m_idx(0) {}
frame(app * t):m_curr(t), m_idx(0) {}
};
ast_manager & m_manager;
subpaving::context & m_subpaving;
unsynch_mpq_manager & m_qm;
arith_util m_autil;
expr2var * m_expr2var;
bool m_expr2var_owner;
expr_ref_vector m_var2expr;
typedef svector<subpaving::var> var_vector;
obj_map<expr, unsigned> m_cache;
var_vector m_cached_vars;
scoped_mpz_vector m_cached_numerators;
scoped_mpz_vector m_cached_denominators;
obj_map<expr, subpaving::ineq*> m_lit_cache;
volatile bool m_cancel;
imp(ast_manager & m, subpaving::context & s, expr2var * e2v):
m_manager(m),
m_subpaving(s),
m_qm(s.qm()),
m_autil(m),
m_var2expr(m),
m_cached_numerators(m_qm),
m_cached_denominators(m_qm) {
if (e2v == 0) {
m_expr2var = alloc(expr2var, m);
m_expr2var_owner = true;
}
else {
m_expr2var = e2v;
m_expr2var_owner = false;
}
m_cancel = false;
}
~imp() {
reset_cache();
if (m_expr2var_owner)
dealloc(m_expr2var);
}
ast_manager & m() { return m_manager; }
subpaving::context & s() { return m_subpaving; }
unsynch_mpq_manager & qm() const { return m_qm; }
void reset_cache() {
dec_ref_map_keys(m(), m_cache);
m_cached_vars.reset();
m_cached_numerators.reset();
m_cached_denominators.reset();
dec_ref_map_key_values(m(), s(), m_lit_cache);
}
void checkpoint() {
if (m_cancel)
throw default_exception("canceled");
cooperate("expr2subpaving");
}
subpaving::var mk_var_for(expr * t) {
SASSERT(!m_autil.is_numeral(t));
subpaving::var x = m_expr2var->to_var(t);
if (x == subpaving::null_var) {
bool is_int = m_autil.is_int(t);
x = s().mk_var(is_int);
m_expr2var->insert(t, x);
if (x >= m_var2expr.size())
m_var2expr.resize(x+1, 0);
m_var2expr.set(x, t);
}
return x;
}
void found_non_simplified() {
throw default_exception("you must apply simplifier before internalizing expressions into the subpaving module.");
}
bool is_cached(expr * t) {
return t->get_ref_count() > 1 && m_cache.contains(t);
}
bool is_int_real(expr * t) {
return m_autil.is_int_real(t);
}
void cache_result(expr * t, subpaving::var x, mpz const & n, mpz const & d) {
SASSERT(!m_cache.contains(t));
SASSERT(m_cached_numerators.size() == m_cached_vars.size());
SASSERT(m_cached_denominators.size() == m_cached_vars.size());
if (t->get_ref_count() <= 1)
return;
unsigned idx = m_cached_vars.size();
m_cache.insert(t, idx);
m().inc_ref(t);
m_cached_vars.push_back(x);
m_cached_numerators.push_back(n);
m_cached_denominators.push_back(d);
}
subpaving::var process_num(app * t, unsigned depth, mpz & n, mpz & d) {
rational k;
VERIFY(m_autil.is_numeral(t, k));
qm().set(n, k.to_mpq().numerator());
qm().set(d, k.to_mpq().denominator());
return subpaving::null_var;
}
// Put t as a^k.
void as_power(expr * t, expr * & a, unsigned & k) {
if (!m_autil.is_power(t)) {
a = t;
k = 1;
return;
}
rational _k;
if (!m_autil.is_numeral(to_app(t)->get_arg(1), _k) || !_k.is_int() || !_k.is_unsigned()) {
a = t;
k = 1;
return;
}
a = to_app(t)->get_arg(0);
k = _k.get_unsigned();
}
subpaving::var process_mul(app * t, unsigned depth, mpz & n, mpz & d) {
unsigned num_args = t->get_num_args();
if (num_args <= 1)
found_non_simplified();
rational k;
expr * m;
if (m_autil.is_numeral(t->get_arg(0), k)) {
if (num_args != 2)
found_non_simplified();
qm().set(n, k.to_mpq().numerator());
qm().set(d, k.to_mpq().denominator());
m = t->get_arg(1);
}
else {
qm().set(n, 1);
qm().set(d, 1);
m = t;
}
expr * const * margs;
unsigned sz;
if (m_autil.is_mul(m)) {
margs = to_app(m)->get_args();
sz = to_app(m)->get_num_args();
}
else {
margs = &m;
sz = 1;
}
scoped_mpz n_arg(qm());
scoped_mpz d_arg(qm());
sbuffer<subpaving::power> pws;
for (unsigned i = 0; i < sz; i++) {
expr * arg = margs[i];
unsigned k;
as_power(arg, arg, k);
subpaving::var x_arg = process(arg, depth+1, n_arg, d_arg);
qm().power(n_arg, k, n_arg);
qm().power(d_arg, k, d_arg);
qm().mul(n, n_arg, n);
qm().mul(d, d_arg, d);
if (x_arg != subpaving::null_var)
pws.push_back(subpaving::power(x_arg, k));
}
subpaving::var x;
if (pws.empty())
x = subpaving::null_var;
else if (pws.size() == 1 && pws[0].degree() == 1)
x = pws[0].get_var();
else
x = s().mk_monomial(pws.size(), pws.c_ptr());
cache_result(t, x, n, d);
return x;
}
typedef _scoped_numeral_buffer<unsynch_mpz_manager> mpz_buffer;
typedef sbuffer<subpaving::var> var_buffer;
subpaving::var process_add(app * t, unsigned depth, mpz & n, mpz & d) {
unsigned num_args = t->get_num_args();
mpz_buffer ns(qm()), ds(qm());
var_buffer xs;
scoped_mpq c(qm()), c_arg(qm());
scoped_mpz n_arg(qm()), d_arg(qm());
for (unsigned i = 0; i < num_args; i++) {
expr * arg = t->get_arg(i);
subpaving::var x_arg = process(arg, depth+1, n_arg, d_arg);
if (x_arg == subpaving::null_var) {
qm().set(c_arg, n_arg, d_arg);
qm().add(c, c_arg, c);
}
else {
xs.push_back(x_arg);
ns.push_back(n_arg);
ds.push_back(d_arg);
}
}
qm().set(d, c.get().denominator());
unsigned sz = xs.size();
for (unsigned i = 0; i < sz; i++) {
qm().lcm(d, ds[i], d);
}
scoped_mpz & k = d_arg;
qm().div(d, c.get().denominator(), k);
scoped_mpz sum_c(qm());
qm().mul(c.get().numerator(), k, sum_c);
for (unsigned i = 0; i < sz; i++) {
qm().div(d, ds[i], k);
qm().mul(ns[i], k, ns[i]);
}
subpaving::var x;
if (sz == 0) {
qm().set(n, sum_c);
x = subpaving::null_var;
}
else {
x = s().mk_sum(sum_c, sz, ns.c_ptr(), xs.c_ptr());
qm().set(n, 1);
}
cache_result(t, x, n, d);
return x;
}
subpaving::var process_power(app * t, unsigned depth, mpz & n, mpz & d) {
rational k;
SASSERT(t->get_num_args() == 2);
if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_int() || !k.is_unsigned()) {
qm().set(n, 1);
qm().set(d, 1);
return mk_var_for(t);
}
unsigned _k = k.get_unsigned();
subpaving::var x = process(t->get_arg(0), depth+1, n, d);
if (x != subpaving::null_var) {
subpaving::power p(x, _k);
x = s().mk_monomial(1, &p);
}
qm().power(n, _k, n);
qm().power(d, _k, d);
cache_result(t, x, n, d);
return x;
}
subpaving::var process_arith_app(app * t, unsigned depth, mpz & n, mpz & d) {
SASSERT(m_autil.is_arith_expr(t));
switch (t->get_decl_kind()) {
case OP_NUM:
return process_num(t, depth, n, d);
case OP_ADD:
return process_add(t, depth, n, d);
case OP_MUL:
return process_mul(t, depth, n, d);
case OP_POWER:
return process_power(t, depth, n, d);
case OP_TO_REAL:
return process(t->get_arg(0), depth+1, n, d);
case OP_SUB:
case OP_UMINUS:
found_non_simplified();
break;
case OP_TO_INT:
case OP_DIV:
case OP_IDIV:
case OP_MOD:
case OP_REM:
case OP_IRRATIONAL_ALGEBRAIC_NUM:
throw default_exception("you must apply arithmetic purifier before internalizing expressions into the subpaving module.");
case OP_SIN:
case OP_COS:
case OP_TAN:
case OP_ASIN:
case OP_ACOS:
case OP_ATAN:
case OP_SINH:
case OP_COSH:
case OP_TANH:
case OP_ASINH:
case OP_ACOSH:
case OP_ATANH:
// TODO
throw default_exception("transcendental and hyperbolic functions are not supported yet.");
default:
UNREACHABLE();
}
return subpaving::null_var;
}
subpaving::var process(expr * t, unsigned depth, mpz & n, mpz & d) {
SASSERT(is_int_real(t));
checkpoint();
if (is_cached(t)) {
unsigned idx = m_cache.find(t);
qm().set(n, m_cached_numerators[idx]);
qm().set(d, m_cached_denominators[idx]);
return m_cached_vars[idx];
}
SASSERT(!is_quantifier(t));
if (::is_var(t) || !m_autil.is_arith_expr(t)) {
qm().set(n, 1);
qm().set(d, 1);
return mk_var_for(t);
}
return process_arith_app(to_app(t), depth, n, d);
}
bool is_var(expr * t) const {
return m_expr2var->is_var(t);
}
void set_cancel(bool f) {
m_cancel = f;
}
subpaving::var internalize_term(expr * t, mpz & n, mpz & d) {
return process(t, 0, n, d);
}
};
expr2subpaving::expr2subpaving(ast_manager & m, subpaving::context & s, expr2var * e2v) {
m_imp = alloc(imp, m, s, e2v);
}
expr2subpaving::~expr2subpaving() {
dealloc(m_imp);
}
ast_manager & expr2subpaving::m() const {
return m_imp->m();
}
subpaving::context & expr2subpaving::s() const {
return m_imp->s();
}
bool expr2subpaving::is_var(expr * t) const {
return m_imp->is_var(t);
}
void expr2subpaving::set_cancel(bool f) {
m_imp->set_cancel(f);
}
subpaving::var expr2subpaving::internalize_term(expr * t, mpz & n, mpz & d) {
return m_imp->internalize_term(t, n, d);
}

58
src/math/subpaving/tactic/expr2subpaving.h Normal file
View file

@ -0,0 +1,58 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
expr2subpaving.h
Abstract:
Translator from Z3 expressions into generic subpaving data-structure.
Author:
Leonardo (leonardo) 2012-08-08
Notes:
--*/
#ifndef _EXPR2SUBPAVING_H_
#define _EXPR2SUBPAVING_H_
#include"ast.h"
#include"subpaving.h"
class expr2var;
class expr2subpaving {
struct imp;
imp * m_imp;
public:
expr2subpaving(ast_manager & m, subpaving::context & s, expr2var * e2v = 0);
~expr2subpaving();
ast_manager & m() const;
subpaving::context & s() const;
/**
\brief Return true if t was encoded as a variable by the translator.
*/
bool is_var(expr * t) const;
/**
\brief Cancel/Interrupt execution.
*/
void set_cancel(bool f);
/**
\brief Internalize a Z3 arithmetical expression into the subpaving data-structure.
\remark throws subpaving::exception there is a translation error (when using imprecise representations, i.e. floats, in the subpaving module)
*/
subpaving::var internalize_term(expr * t, /* out */ mpz & n, /* out */ mpz & d);
};
#endif

308
src/math/subpaving/tactic/subpaving_tactic.cpp Normal file
View file

@ -0,0 +1,308 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_tactic.cpp
Abstract:
"Fake" tactic used to test subpaving module.
Author:
Leonardo de Moura (leonardo) 2012-08-07.
Revision History:
--*/
#include"tactical.h"
#include"simplify_tactic.h"
#include"expr2subpaving.h"
#include"expr2var.h"
#include"arith_decl_plugin.h"
#include"ast_smt2_pp.h"
#include"hwf.h"
#include"mpff.h"
#include"mpfx.h"
#include"f2n.h"
class subpaving_tactic : public tactic {
struct display_var_proc : public subpaving::display_var_proc {
expr_ref_vector m_inv;
display_var_proc(expr2var & e2v):m_inv(e2v.m()) {
e2v.mk_inv(m_inv);
}
ast_manager & m() const { return m_inv.get_manager(); }
virtual void operator()(std::ostream & out, subpaving::var x) const {
expr * t = m_inv.get(x, 0);
if (t != 0)
out << mk_ismt2_pp(t, m());
else
out << "k!" << x;
}
};
struct imp {
enum engine_kind { MPQ, MPF, HWF, MPFF, MPFX, NONE };
ast_manager & m_manager;
unsynch_mpq_manager m_qm;
mpf_manager m_fm_core;
f2n<mpf_manager> m_fm;
hwf_manager m_hm_core;
f2n<hwf_manager> m_hm;
mpff_manager m_ffm;
mpfx_manager m_fxm;
arith_util m_autil;
engine_kind m_kind;
scoped_ptr<subpaving::context> m_ctx;
scoped_ptr<display_var_proc> m_proc;
expr2var m_e2v;
scoped_ptr<expr2subpaving> m_e2s;
bool m_display;
imp(ast_manager & m, params_ref const & p):
m_manager(m),
m_fm(m_fm_core),
m_hm(m_hm_core),
m_autil(m),
m_kind(NONE),
m_e2v(m) {
updt_params(p);
}
ast_manager & m() const { return m_manager; }
void collect_param_descrs(param_descrs & r) {
m_ctx->collect_param_descrs(r);
// #ifndef _EXTERNAL_RELEASE
r.insert(":numeral", CPK_SYMBOL, "(default: mpq) options: mpq, mpf, hwf, mpff, mpfx.");
r.insert(":print-nodes", CPK_BOOL, "(default: false) display subpaving tree leaves.");
// #endif
}
void updt_params(params_ref const & p) {
m_display = p.get_bool(":print-nodes", false);
symbol engine = p.get_sym(":numeral", symbol("mpq"));
engine_kind new_kind;
if (engine == "mpq")
new_kind = MPQ;
else if (engine == "mpf")
new_kind = MPF;
else if (engine == "mpff")
new_kind = MPFF;
else if (engine == "mpfx")
new_kind = MPFX;
else
new_kind = HWF;
if (m_kind != new_kind) {
m_kind = new_kind;
switch (m_kind) {
case MPQ: m_ctx = subpaving::mk_mpq_context(m_qm); break;
case MPF: m_ctx = subpaving::mk_mpf_context(m_fm); break;
case HWF: m_ctx = subpaving::mk_hwf_context(m_hm, m_qm); break;
case MPFF: m_ctx = subpaving::mk_mpff_context(m_ffm, m_qm); break;
case MPFX: m_ctx = subpaving::mk_mpfx_context(m_fxm, m_qm); break;
default: UNREACHABLE(); break;
}
m_e2s = alloc(expr2subpaving, m_manager, *m_ctx, &m_e2v);
}
m_ctx->updt_params(p);
}
void collect_statistics(statistics & st) const {
m_ctx->collect_statistics(st);
}
void reset_statistics() {
m_ctx->reset_statistics();
}
void set_cancel(bool f) {
m_e2s->set_cancel(f);
m_ctx->set_cancel(f);
}
subpaving::ineq * mk_ineq(expr * a) {
bool neg = false;
while (m().is_not(a, a))
neg = !neg;
bool lower;
bool open = false;
if (m_autil.is_le(a)) {
lower = false;
}
else if (m_autil.is_ge(a)) {
lower = true;
}
else {
throw tactic_exception("unsupported atom");
}
if (neg) {
lower = !lower;
open = !open;
}
rational _k;
if (!m_autil.is_numeral(to_app(a)->get_arg(1), _k))
throw tactic_exception("use simplify tactic with option :arith-lhs true");
scoped_mpq k(m_qm);
k = _k.to_mpq();
scoped_mpz n(m_qm), d(m_qm);
subpaving::var x = m_e2s->internalize_term(to_app(a)->get_arg(0), n, d);
m_qm.mul(d, k, k);
m_qm.div(k, n, k);
if (is_neg(n))
lower = !lower;
TRACE("subpaving_tactic", tout << x << " " << k << " " << lower << " " << open << "\n";);
return m_ctx->mk_ineq(x, k, lower, open);
}
void process_clause(expr * c) {
expr * const * args = 0;
unsigned sz;
if (m().is_or(c)) {
args = to_app(c)->get_args();
sz = to_app(c)->get_num_args();
}
else {
args = &c;
sz = 1;
}
ref_buffer<subpaving::ineq, subpaving::context> ineq_buffer(*m_ctx);
for (unsigned i = 0; i < sz; i++) {
ineq_buffer.push_back(mk_ineq(args[i]));
}
m_ctx->add_clause(sz, ineq_buffer.c_ptr());
}
void internalize(goal const & g) {
try {
for (unsigned i = 0; i < g.size(); i++) {
process_clause(g.form(i));
}
}
catch (subpaving::exception) {
throw tactic_exception("failed to internalize goal into subpaving module");
}
}
void process(goal const & g) {
internalize(g);
m_proc = alloc(display_var_proc, m_e2v);
m_ctx->set_display_proc(m_proc.get());
try {
(*m_ctx)();
}
catch (subpaving::exception) {
throw tactic_exception("failed building subpaving tree...");
}
if (m_display) {
m_ctx->display_constraints(std::cout);
std::cout << "bounds at leaves: \n";
m_ctx->display_bounds(std::cout);
}
}
};
imp * m_imp;
params_ref m_params;
statistics m_stats;
public:
subpaving_tactic(ast_manager & m, params_ref const & p):
m_imp(alloc(imp, m, p)),
m_params(p) {
}
virtual ~subpaving_tactic() {
dealloc(m_imp);
}
virtual tactic * translate(ast_manager & m) {
return alloc(subpaving_tactic, m, m_params);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
m_imp->updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {
m_imp->collect_param_descrs(r);
}
virtual void collect_statistics(statistics & st) const {
st.copy(m_stats);
}
virtual void reset_statistics() {
m_stats.reset();
}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
m_imp->process(*in);
m_imp->collect_statistics(m_stats);
result.reset();
result.push_back(in.get());
mc = 0;
pc = 0;
core = 0;
}
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = m_imp;
#pragma omp critical (tactic_cancel)
{
d = m_imp;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
protected:
virtual void set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
}
};
tactic * mk_subpaving_tactic_core(ast_manager & m, params_ref const & p) {
return alloc(subpaving_tactic, m, p);
}
tactic * mk_subpaving_tactic(ast_manager & m, params_ref const & p) {
params_ref simp_p = p;
simp_p.set_bool(":arith-lhs", true);
simp_p.set_bool(":expand-power", true);
simp_p.set_uint(":max-power", UINT_MAX);
simp_p.set_bool(":som", true);
simp_p.set_bool(":eq2ineq", true);
simp_p.set_bool(":elim-and", true);
simp_p.set_bool(":blast-distinct", true);
params_ref simp2_p = p;
simp2_p.set_bool(":mul-to-power", true);
return and_then(using_params(mk_simplify_tactic(m, p),
simp_p),
using_params(mk_simplify_tactic(m, p),
simp2_p),
mk_subpaving_tactic_core(m, p));
}

28
src/math/subpaving/tactic/subpaving_tactic.h Normal file
View file

@ -0,0 +1,28 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_tactic.h
Abstract:
"Fake" tactic used to test subpaving module.
Author:
Leonardo de Moura (leonardo) 2012-08-07.
Revision History:
--*/
#ifndef __SUBPAVING_TACTIC_H_
#define __SUBPAVING_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_subpaving_tactic(ast_manager & m, params_ref const & p = params_ref());
#endif