mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-02-26 19:15:04 -08:00
commit 5d2d89a85c
13 changed files with 333 additions and 200 deletions
Download patch file Download diff file Expand all files Collapse all files

64
src/api/c++/z3++.h
View file

@ -63,6 +63,11 @@ namespace z3 {
class statistics;
class apply_result;
class fixedpoint;
template<typename T> class ast_vector_tpl;
typedef ast_vector_tpl<ast> ast_vector;
typedef ast_vector_tpl<expr> expr_vector;
typedef ast_vector_tpl<sort> sort_vector;
typedef ast_vector_tpl<func_decl> func_decl_vector;
inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
@ -190,7 +195,13 @@ namespace z3 {
Example: Given a context \c c, <tt>c.array_sort(c.int_sort(), c.bool_sort())</tt> is an array sort from integer to Boolean.
*/
sort array_sort(sort d, sort r);
/**
\brief Return an enumeration sort: enum_names[0], ..., enum_names[n-1].
\c cs and \c ts are output parameters. The method stores in \c cs the constants corresponding to the enumerated elements,
and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration.
*/
sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
func_decl function(char const * name, sort const & domain, sort const & range);
@ -240,8 +251,8 @@ namespace z3 {
array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
~array() { delete[] m_array; }
unsigned size() const { return m_size; }
T & operator[](unsigned i) { assert(i < m_size); return m_array[i]; }
T const & operator[](unsigned i) const { assert(i < m_size); return m_array[i]; }
T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
T const * ptr() const { return m_array; }
T * ptr() { return m_array; }
};
@ -414,6 +425,7 @@ namespace z3 {
bool is_const() const { return arity() == 0; }
expr operator()() const;
expr operator()(unsigned n, expr const * args) const;
expr operator()(expr const & a) const;
expr operator()(int a) const;
@ -1004,7 +1016,7 @@ namespace z3 {
~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
operator Z3_ast_vector() const { return m_vector; }
unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
T operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
T back() const { return operator[](size() - 1); }
@ -1020,11 +1032,6 @@ namespace z3 {
friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
};
typedef ast_vector_tpl<ast> ast_vector;
typedef ast_vector_tpl<expr> expr_vector;
typedef ast_vector_tpl<sort> sort_vector;
typedef ast_vector_tpl<func_decl> func_decl_vector;
class func_entry : public object {
Z3_func_entry m_entry;
void init(Z3_func_entry e) {
@ -1105,7 +1112,10 @@ namespace z3 {
func_decl get_const_decl(unsigned i) const { Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
func_decl get_func_decl(unsigned i) const { Z3_func_decl r = Z3_model_get_func_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
unsigned size() const { return num_consts() + num_funcs(); }
func_decl operator[](unsigned i) const { return i < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts()); }
func_decl operator[](int i) const {
assert(0 <= i);
return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
}
expr get_const_interp(func_decl c) const {
check_context(*this, c);
@ -1253,7 +1263,7 @@ namespace z3 {
}
void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
expr operator[](unsigned i) const { Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
@ -1261,6 +1271,19 @@ namespace z3 {
unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
expr as_expr() const {
unsigned n = size();
if (n == 0)
return ctx().bool_val(false);
else if (n == 1)
return operator[](0);
else {
array<Z3_ast> args(n);
for (unsigned i = 0; i < n; i++)
args[i] = operator[](i);
return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
}
}
friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
};
@ -1283,8 +1306,7 @@ namespace z3 {
return *this;
}
unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
goal operator[](unsigned i) const { Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
goal operator[](int i) const { assert(i >= 0); return this->operator[](static_cast<unsigned>(i)); }
goal operator[](int i) const { assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
model convert_model(model const & m, unsigned i = 0) const {
check_context(*this, m);
Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
@ -1437,6 +1459,17 @@ namespace z3 {
inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
array<Z3_symbol> _enum_names(n);
for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
array<Z3_func_decl> _cs(n);
array<Z3_func_decl> _ts(n);
Z3_symbol _name = Z3_mk_string_symbol(*this, name);
sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
check_error();
for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
return s;
}
inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
array<Z3_sort> args(arity);
@ -1538,6 +1571,11 @@ namespace z3 {
return expr(ctx(), r);
}
inline expr func_decl::operator()() const {
Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
ctx().check_error();
return expr(ctx(), r);
}
inline expr func_decl::operator()(expr const & a) const {
check_context(*this, a);
Z3_ast args[1] = { a };

8
src/api/dotnet/Fixedpoint.cs
View file

@ -78,6 +78,14 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Alias for Assert.
/// </summary>
public void Add(params BoolExpr[] constraints)
{
Assert(constraints);
}
/// <summary>
/// Register predicate as recursive relation.
/// </summary>

8
src/api/dotnet/Goal.cs
View file

@ -90,6 +90,14 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Alias for Assert.
/// </summary>
public void Add(params BoolExpr[] constraints)
{
Assert(constraints);
}
/// <summary>
/// Indicates whether the goal contains `false'.
/// </summary>

8
src/api/dotnet/Solver.cs
View file

@ -117,6 +117,14 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Alias for Assert.
/// </summary>
public void Add(params BoolExpr[] constraints)
{
Assert(constraints);
}
/// <summary>
/// Assert multiple constraints into the solver, and track them (in the unsat) core
/// using the Boolean constants in ps.

2
src/api/java/Fixedpoint.java
View file

@ -51,7 +51,7 @@ public class Fixedpoint extends Z3Object
*
* @throws Z3Exception
**/
public void assert_(BoolExpr ... constraints) throws Z3Exception
public void add(BoolExpr ... constraints) throws Z3Exception
{
getContext().checkContextMatch(constraints);
for (BoolExpr a : constraints)

2
src/api/java/Goal.java
View file

@ -65,7 +65,7 @@ public class Goal extends Z3Object
*
* @throws Z3Exception
**/
public void assert_(BoolExpr ... constraints) throws Z3Exception
public void add(BoolExpr ... constraints) throws Z3Exception
{
getContext().checkContextMatch(constraints);
for (BoolExpr c : constraints)

2
src/api/java/Solver.java
View file

@ -94,7 +94,7 @@ public class Solver extends Z3Object
*
* @throws Z3Exception
**/
public void assert_(BoolExpr... constraints) throws Z3Exception
public void add(BoolExpr... constraints) throws Z3Exception
{
getContext().checkContextMatch(constraints);
for (BoolExpr a : constraints)

104
src/muz_qe/hilbert_basis.cpp
View file

@ -193,19 +193,9 @@ class hilbert_basis::value_index2 {
checker m_checker;
vector<numeral> m_keys;
#if 1
numeral const* get_keys(values const& vs) {
return vs()-1;
}
#else
numeral const* get_keys(values const& vs) {
unsigned sz = m_keys.size();
for (unsigned i = 0; i < sz; ++i) {
m_keys[sz-i-1] = vs()[i-1];
}
return m_keys.c_ptr();
}
#endif
public:
value_index2(hilbert_basis& hb): hb(hb), m_init(false) {
@ -507,7 +497,11 @@ class hilbert_basis::passive2 {
}
};
hilbert_basis& hb;
svector<offset_t> const& m_sos;
svector<offset_t> m_pos_sos;
svector<offset_t> m_neg_sos;
vector<numeral> m_pos_sos_sum;
vector<numeral> m_neg_sos_sum;
vector<numeral> m_sum_abs;
unsigned_vector m_psos;
svector<offset_t> m_pas;
vector<numeral> m_weight;
@ -528,40 +522,59 @@ class hilbert_basis::passive2 {
public:
passive2(hilbert_basis& hb):
hb(hb),
m_sos(hb.m_sos),
m_lt(&m_this),
m_heap(10, m_lt)
{
m_this = this;
}
void init(svector<offset_t> const& I) {
for (unsigned i = 0; i < I.size(); ++i) {
numeral const& w = hb.vec(I[i]).weight();
if (w.is_pos()) {
m_pos_sos.push_back(I[i]);
m_pos_sos_sum.push_back(sum_abs(I[i]));
}
else {
m_neg_sos.push_back(I[i]);
m_neg_sos_sum.push_back(sum_abs(I[i]));
}
}
}
void reset() {
m_heap.reset();
m_free_list.reset();
m_psos.reset();
m_pas.reset();
m_sum_abs.reset();
m_pos_sos.reset();
m_neg_sos.reset();
m_pos_sos_sum.reset();
m_neg_sos_sum.reset();
m_weight.reset();
}
void insert(offset_t idx, unsigned offset) {
SASSERT(!m_sos.empty());
SASSERT(!m_pos_sos.empty());
unsigned v;
numeral w = sum_abs(idx) + sum_abs(m_sos[0]);
if (m_free_list.empty()) {
v = m_pas.size();
m_pas.push_back(idx);
m_psos.push_back(offset);
m_weight.push_back(w);
m_weight.push_back(numeral(0));
m_heap.set_bounds(v+1);
m_sum_abs.push_back(sum_abs(idx));
}
else {
v = m_free_list.back();
m_free_list.pop_back();
m_pas[v] = idx;
m_psos[v] = offset;
m_weight[v] = w;
m_weight[v] = numeral(0);
m_sum_abs[v] = sum_abs(idx);
}
next_resolvable(v);
next_resolvable(hb.vec(idx).weight().is_pos(), v);
}
bool empty() const {
@ -571,12 +584,13 @@ public:
unsigned pop(offset_t& sos, offset_t& pas) {
SASSERT (!empty());
unsigned val = static_cast<unsigned>(m_heap.erase_min());
unsigned psos = m_psos[val];
sos = m_sos[psos];
pas = m_pas[val];
m_psos[val]++;
next_resolvable(val);
numeral old_weight = hb.vec(pas).weight();
bool is_positive = old_weight.is_pos();
unsigned psos = m_psos[val];
sos = is_positive?m_neg_sos[psos]:m_pos_sos[psos];
m_psos[val]++;
next_resolvable(is_positive, val);
numeral new_weight = hb.vec(sos).weight() + old_weight;
if (new_weight.is_pos() != old_weight.is_pos()) {
psos = 0;
@ -600,7 +614,7 @@ public:
public:
iterator(passive2& p, unsigned i): p(p), m_idx(i) { fwd(); }
offset_t pas() const { return p.m_pas[m_idx]; }
offset_t sos() const { return p.m_sos[p.m_psos[m_idx]]; }
offset_t sos() const { return (p.hb.vec(pas()).weight().is_pos()?p.m_neg_sos:p.m_pos_sos)[p.m_psos[m_idx]]; }
iterator& operator++() { ++m_idx; fwd(); return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& it) const {return m_idx == it.m_idx; }
@ -615,12 +629,14 @@ public:
return iterator(*this, m_pas.size());
}
private:
void next_resolvable(unsigned v) {
void next_resolvable(bool is_positive, unsigned v) {
offset_t pas = m_pas[v];
while (m_psos[v] < m_sos.size()) {
offset_t sos = m_sos[m_psos[v]];
if (hb.can_resolve(sos, pas)) {
m_weight[v] = sum_abs(pas) + sum_abs(sos);
svector<offset_t> const& soss = is_positive?m_neg_sos:m_pos_sos;
while (m_psos[v] < soss.size()) {
unsigned psos = m_psos[v];
offset_t sos = soss[psos];
if (hb.can_resolve(sos, pas, false)) {
m_weight[v] = m_sum_abs[v] + (is_positive?m_neg_sos_sum[psos]:m_pos_sos_sum[psos]);
m_heap.insert(v);
return;
}
@ -746,7 +762,7 @@ unsigned hilbert_basis::get_num_vars() const {
}
hilbert_basis::values hilbert_basis::vec(offset_t offs) const {
return values(m_store.c_ptr() + (get_num_vars() + 1)*offs.m_offset);
return values(m_ineqs.size(), m_store.c_ptr() + offs.m_offset);
}
void hilbert_basis::init_basis() {
@ -814,6 +830,9 @@ lbool hilbert_basis::saturate_orig(num_vector const& ineq, bool is_eq) {
offset_t idx = *it;
values v = vec(idx);
v.weight() = get_weight(v, ineq);
for (unsigned k = 0; k < m_current_ineq; ++k) {
v.weight(k) = get_weight(v, m_ineqs[k]);
}
add_goal(idx);
if (m_use_support) {
support.insert(idx.m_offset);
@ -833,7 +852,7 @@ lbool hilbert_basis::saturate_orig(num_vector const& ineq, bool is_eq) {
continue;
}
for (unsigned i = 0; !m_cancel && i < m_active.size(); ++i) {
if ((!m_use_support || support.contains(m_active[i].m_offset)) && can_resolve(idx, m_active[i])) {
if ((!m_use_support || support.contains(m_active[i].m_offset)) && can_resolve(idx, m_active[i], true)) {
resolve(idx, m_active[i], j);
if (add_goal(j)) {
j = alloc_vector();
@ -884,6 +903,9 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) {
offset_t idx = m_basis[i];
values v = vec(idx);
v.weight() = get_weight(v, ineq);
for (unsigned k = 0; k < m_current_ineq; ++k) {
v.weight(k) = get_weight(v, m_ineqs[k]);
}
m_index->insert(idx, v);
if (v.weight().is_zero()) {
m_zero.push_back(idx);
@ -896,6 +918,7 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) {
}
}
m_basis.resize(init_basis_size);
m_passive2->init(m_sos);
// ASSERT basis is sorted by weight.
// initialize passive
@ -912,7 +935,7 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) {
offset_t sos, pas;
TRACE("hilbert_basis", display(tout); );
unsigned offset = m_passive2->pop(sos, pas);
SASSERT(can_resolve(sos, pas));
SASSERT(can_resolve(sos, pas, true));
resolve(sos, pas, idx);
if (is_subsumed(idx)) {
continue;
@ -1053,6 +1076,9 @@ void hilbert_basis::resolve(offset_t i, offset_t j, offset_t r) {
u[k] = v[k] + w[k];
}
u.weight() = v.weight() + w.weight();
for (unsigned k = 0; k < m_current_ineq; ++k) {
u.weight(k) = v.weight(k) + w.weight(k);
}
TRACE("hilbert_basis_verbose",
display(tout, i);
display(tout, j);
@ -1063,10 +1089,11 @@ void hilbert_basis::resolve(offset_t i, offset_t j, offset_t r) {
hilbert_basis::offset_t hilbert_basis::alloc_vector() {
if (m_free_list.empty()) {
unsigned num_vars = get_num_vars();
unsigned idx = m_store.size();
m_store.resize(idx + 1 + num_vars);
return offset_t(idx/(1+num_vars));
unsigned sz = m_ineqs.size() + get_num_vars();
unsigned idx = m_store.size();
m_store.resize(idx + sz);
// std::cout << "alloc vector: " << idx << " " << sz << " " << m_store.c_ptr() + idx << " " << m_ineqs.size() << "\n";
return offset_t(idx);
}
else {
offset_t result = m_free_list.back();
@ -1101,10 +1128,11 @@ bool hilbert_basis::is_subsumed(offset_t idx) {
return false;
}
bool hilbert_basis::can_resolve(offset_t i, offset_t j) const {
if (get_sign(i) == get_sign(j)) {
bool hilbert_basis::can_resolve(offset_t i, offset_t j, bool check_sign) const {
if (check_sign && get_sign(i) == get_sign(j)) {
return false;
}
SASSERT(get_sign(i) != get_sign(j));
values const& v1 = vec(i);
values const& v2 = vec(j);
if (v1[0].is_one() && v2[0].is_one()) {
@ -1123,7 +1151,7 @@ bool hilbert_basis::can_resolve(offset_t i, offset_t j) const {
}
hilbert_basis::sign_t hilbert_basis::get_sign(offset_t idx) const {
numeral val = vec(idx).weight();
numeral const& val = vec(idx).weight();
if (val.is_pos()) {
return pos;
}
@ -1267,7 +1295,7 @@ bool hilbert_basis::is_subsumed(offset_t i, offset_t j) const {
n >= m && (!m.is_neg() || n == m) &&
is_geq(v, w);
for (unsigned k = 0; r && k < m_current_ineq; ++k) {
r = get_weight(vec(i), m_ineqs[k]) >= get_weight(vec(j), m_ineqs[k]);
r = v.weight(k) >= w.weight(k);
}
CTRACE("hilbert_basis", r,
display(tout, i);

16
src/muz_qe/hilbert_basis.h
View file

@ -56,12 +56,14 @@ private:
class values {
numeral* m_values;
public:
values(numeral* v):m_values(v) {}
numeral& weight() { return m_values[0]; } // value of a*x
numeral& operator[](unsigned i) { return m_values[i+1]; } // value of x_i
numeral const& weight() const { return m_values[0]; } // value of a*x
numeral const& operator[](unsigned i) const { return m_values[i+1]; } // value of x_i
numeral const* operator()() const { return m_values + 1; }
values(unsigned offset, numeral* v): m_values(v+offset) { }
numeral& weight() { return m_values[-1]; } // value of a*x
numeral const& weight() const { return m_values[-1]; } // value of a*x
numeral& weight(int i) { return m_values[-2-i]; } // value of b_i*x for 0 <= i < current inequality.
numeral const& weight(int i) const { return m_values[-2-i]; } // value of b_i*x
numeral& operator[](unsigned i) { return m_values[i]; } // value of x_i
numeral const& operator[](unsigned i) const { return m_values[i]; } // value of x_i
numeral const* operator()() const { return m_values; }
};
vector<num_vector> m_ineqs; // set of asserted inequalities
@ -114,7 +116,7 @@ private:
bool is_subsumed(offset_t idx);
bool is_subsumed(offset_t i, offset_t j) const;
void recycle(offset_t idx);
bool can_resolve(offset_t i, offset_t j) const;
bool can_resolve(offset_t i, offset_t j, bool check_sign) const;
sign_t get_sign(offset_t idx) const;
bool add_goal(offset_t idx);
offset_t alloc_vector();

2
src/test/hilbert_basis.cpp
View file

@ -521,6 +521,8 @@ void tst_hilbert_basis() {
tst2();
tst3();
tst4();
tst4();
tst4();
tst5();
tst6();
tst7();