mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 11:41:22 +00:00
Code Activity

working on hilbert basis

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-02-15 09:09:58 -08:00
commit aaf0c16e08
9 changed files with 480 additions and 450 deletions
Download patch file Download diff file Expand all files Collapse all files

2
RELEASE_NOTES
View file

@ -59,6 +59,8 @@ Version 4.3.2
- Fixed http://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model. - Fixed http://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model.
- Fixed bugs in the C++ API (Thanks to Andrey Kupriyanov).
Version 4.3.1 Version 4.3.1
============= =============

2
scripts/mk_unix_dist.py
View file

@ -190,7 +190,7 @@ def mk_zip():
try: try:
os.chdir(DIST_DIR) os.chdir(DIST_DIR)
zfname = '%s.zip' % dist_path zfname = '%s.zip' % dist_path
ZIPOUT = zipfile.ZipFile(zfname, 'w') ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
os.path.walk(dist_path, mk_zip_visitor, '*') os.path.walk(dist_path, mk_zip_visitor, '*')
if is_verbose(): if is_verbose():
print "Generated '%s'" % zfname print "Generated '%s'" % zfname

5
scripts/mk_util.py
View file

@ -76,10 +76,7 @@ GPROF=False
GIT_HASH=False GIT_HASH=False
def check_output(cmd): def check_output(cmd):
try: return subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0].rstrip('\r\n')
return subprocess.check_output(cmd, shell=True).rstrip('\r\n')
except:
return subprocess.check_output(cmd).rstrip('\r\n')
def git_hash(): def git_hash():
try: try:

2
scripts/mk_win_dist.py
View file

@ -205,7 +205,7 @@ def mk_zip_core(x64):
try: try:
os.chdir(DIST_DIR) os.chdir(DIST_DIR)
zfname = '%s.zip' % dist_path zfname = '%s.zip' % dist_path
ZIPOUT = zipfile.ZipFile(zfname, 'w') ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
os.path.walk(dist_path, mk_zip_visitor, '*') os.path.walk(dist_path, mk_zip_visitor, '*')
if is_verbose(): if is_verbose():
print "Generated '%s'" % zfname print "Generated '%s'" % zfname

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

@ -619,6 +619,8 @@ namespace z3 {
a.check_error(); a.check_error();
return expr(a.ctx(), r); return expr(a.ctx(), r);
} }
friend expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
friend expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
/** /**
\brief Create the if-then-else expression <tt>ite(c, t, e)</tt> \brief Create the if-then-else expression <tt>ite(c, t, e)</tt>
@ -758,7 +760,7 @@ namespace z3 {
return expr(a.ctx(), r); return expr(a.ctx(), r);
} }
friend expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); } friend expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - a; } friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
friend expr operator<=(expr const & a, expr const & b) { friend expr operator<=(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
@ -777,7 +779,7 @@ namespace z3 {
return expr(a.ctx(), r); return expr(a.ctx(), r);
} }
friend expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); } friend expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= a; } friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
friend expr operator>=(expr const & a, expr const & b) { friend expr operator>=(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
@ -796,7 +798,7 @@ namespace z3 {
return expr(a.ctx(), r); return expr(a.ctx(), r);
} }
friend expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); } friend expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= a; } friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
friend expr operator<(expr const & a, expr const & b) { friend expr operator<(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
@ -815,7 +817,7 @@ namespace z3 {
return expr(a.ctx(), r); return expr(a.ctx(), r);
} }
friend expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); } friend expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < a; } friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
friend expr operator>(expr const & a, expr const & b) { friend expr operator>(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
@ -834,7 +836,7 @@ namespace z3 {
return expr(a.ctx(), r); return expr(a.ctx(), r);
} }
friend expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); } friend expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > a; } friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
friend expr operator&(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); } friend expr operator&(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
friend expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); } friend expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
@ -888,31 +890,31 @@ namespace z3 {
*/ */
inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); } inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); } inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), a); } inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
/** /**
\brief unsigned less than operator for bitvectors. \brief unsigned less than operator for bitvectors.
*/ */
inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); } inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); } inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), a); } inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
/** /**
\brief unsigned greater than or equal to operator for bitvectors. \brief unsigned greater than or equal to operator for bitvectors.
*/ */
inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); } inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); } inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), a); } inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
/** /**
\brief unsigned greater than operator for bitvectors. \brief unsigned greater than operator for bitvectors.
*/ */
inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); } inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); } inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), a); } inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
/** /**
\brief unsigned division operator for bitvectors. \brief unsigned division operator for bitvectors.
*/ */
inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); } inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); } inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), a); } inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
// Basic functions for creating quantified formulas. // Basic functions for creating quantified formulas.
// The C API should be used for creating quantifiers with patterns, weights, many variables, etc. // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.

12
src/ast/ast.cpp
View file

@ -1849,9 +1849,9 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
sort * given = get_sort(args[i]); sort * given = get_sort(args[i]);
if (!compatible_sorts(expected, given)) { if (!compatible_sorts(expected, given)) {
std::ostringstream buff; std::ostringstream buff;
buff << "Invalid function application for " << decl->get_name() << ". "; buff << "invalid function application for " << decl->get_name() << ", ";
buff << "Sort mismatch on argument at position " << (i+1) << ". "; buff << "sort mismatch on argument at position " << (i+1) << ", ";
buff << "Expected: " << mk_pp(expected, m) << " but given " << mk_pp(given, m); buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
throw ast_exception(buff.str().c_str()); throw ast_exception(buff.str().c_str());
} }
} }
@ -1865,9 +1865,9 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
sort * given = get_sort(args[i]); sort * given = get_sort(args[i]);
if (!compatible_sorts(expected, given)) { if (!compatible_sorts(expected, given)) {
std::ostringstream buff; std::ostringstream buff;
buff << "Invalid function application for " << decl->get_name() << ". "; buff << "invalid function application for " << decl->get_name() << ", ";
buff << "Sort mismatch on argument at position " << (i+1) << ". "; buff << "sort mismatch on argument at position " << (i+1) << ", ";
buff << "Expected: " << mk_pp(expected, m) << " but given " << mk_pp(given, m); buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
throw ast_exception(buff.str().c_str()); throw ast_exception(buff.str().c_str());
} }
} }

783
src/muz_qe/hilbert_basis.cpp
View file

File diff suppressed because it is too large Load diff

44
src/muz_qe/hilbert_basis.h
View file

@ -34,11 +34,9 @@ public:
typedef rational numeral; typedef rational numeral;
typedef vector<numeral> num_vector; typedef vector<numeral> num_vector;
private: private:
class rational_heap;
class value_index; class value_index;
class index; class index;
class passive; class passive;
class weight_map;
struct offset_t { struct offset_t {
unsigned m_offset; unsigned m_offset;
offset_t(unsigned o) : m_offset(o) {} offset_t(unsigned o) : m_offset(o) {}
@ -59,25 +57,28 @@ private:
numeral* m_values; numeral* m_values;
public: public:
values(numeral* v):m_values(v) {} values(numeral* v):m_values(v) {}
numeral& value() { return m_values[0]; } // value of a*x numeral& weight() { return m_values[0]; } // value of a*x
numeral& operator[](unsigned i) { return m_values[i+1]; } // value of x_i numeral& operator[](unsigned i) { return m_values[i+1]; } // value of x_i
numeral const& value() const { return m_values[0]; } // value of a*x 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[](unsigned i) const { return m_values[i+1]; } // value of x_i
}; };
vector<num_vector> m_ineqs; vector<num_vector> m_ineqs; // set of asserted inequalities
num_vector m_store; svector<bool> m_iseq; // inequalities that are equalities
svector<offset_t> m_basis; num_vector m_store; // store of vectors
svector<offset_t> m_free_list; svector<offset_t> m_basis; // vector of current basis
svector<offset_t> m_active; svector<offset_t> m_free_list; // free list of unused storage
svector<offset_t> m_zero; svector<offset_t> m_active; // active set
volatile bool m_cancel; svector<offset_t> m_zero; // zeros
passive* m_passive; // passive set
volatile bool m_cancel;
stats m_stats; stats m_stats;
index* m_index; index* m_index; // index of generated vectors
passive* m_passive; unsigned_vector m_ints; // indices that can be both positive and negative
unsigned m_current_ineq;
class iterator { class iterator {
hilbert_basis const& hb; hilbert_basis const& hb;
unsigned m_idx; unsigned m_idx;
public: public:
iterator(hilbert_basis const& hb, unsigned idx): hb(hb), m_idx(idx) {} iterator(hilbert_basis const& hb, unsigned idx): hb(hb), m_idx(idx) {}
offset_t operator*() const { return hb.m_basis[m_idx]; } offset_t operator*() const { return hb.m_basis[m_idx]; }
@ -89,10 +90,17 @@ private:
static offset_t mk_invalid_offset(); static offset_t mk_invalid_offset();
static bool is_invalid_offset(offset_t offs); static bool is_invalid_offset(offset_t offs);
lbool saturate(num_vector const& ineq); lbool saturate(num_vector const& ineq, bool is_eq);
void init_basis(); void init_basis();
void select_inequality();
unsigned get_num_nonzeros(num_vector const& ineq);
unsigned get_ineq_product(num_vector const& ineq);
void add_unit_vector(unsigned i, numeral const& e);
unsigned get_num_vars() const; unsigned get_num_vars() const;
void set_eval(values& val, num_vector const& ineq) const; numeral get_weight(values& val, num_vector const& ineq) const;
bool is_geq(values const& v, values const& w) const;
bool is_abs_geq(numeral const& v, numeral const& w) const;
bool is_subsumed(offset_t idx); bool is_subsumed(offset_t idx);
bool is_subsumed(offset_t i, offset_t j) const; bool is_subsumed(offset_t i, offset_t j) const;
void recycle(offset_t idx); void recycle(offset_t idx);
@ -108,7 +116,7 @@ private:
void display(std::ostream& out, offset_t o) const; void display(std::ostream& out, offset_t o) const;
void display(std::ostream& out, values const & v) const; void display(std::ostream& out, values const & v) const;
void display_ineq(std::ostream& out, num_vector const& v) const; void display_ineq(std::ostream& out, num_vector const& v, bool is_eq) const;
public: public:
@ -131,6 +139,8 @@ public:
void add_le(num_vector const& v, numeral const& b); void add_le(num_vector const& v, numeral const& b);
void add_eq(num_vector const& v, numeral const& b); void add_eq(num_vector const& v, numeral const& b);
void set_is_int(unsigned var_index);
lbool saturate(); lbool saturate();
void set_cancel(bool f) { m_cancel = f; } void set_cancel(bool f) { m_cancel = f; }

58
src/test/hilbert_basis.cpp
View file

@ -74,6 +74,14 @@ static void gorrila_test(unsigned seed, unsigned n, unsigned k, unsigned bound,
saturate_basis(hb); saturate_basis(hb);
} }
static vector<rational> vec(int i, int j) {
vector<rational> nv;
nv.resize(2);
nv[0] = rational(i);
nv[1] = rational(j);
return nv;
}
static vector<rational> vec(int i, int j, int k) { static vector<rational> vec(int i, int j, int k) {
vector<rational> nv; vector<rational> nv;
nv.resize(3); nv.resize(3);
@ -243,25 +251,37 @@ static void tst11() {
saturate_basis(hb); saturate_basis(hb);
} }
static void tst12() {
hilbert_basis hb;
hb.add_le(vec(1, 0), R(1));
hb.add_le(vec(0, 1), R(1));
saturate_basis(hb);
}
void tst_hilbert_basis() { void tst_hilbert_basis() {
std::cout << "hilbert basis test\n"; std::cout << "hilbert basis test\n";
#if 0 tst12();
tst1(); return;
tst2();
tst3(); if (true) {
tst4(); tst1();
tst5(); tst2();
tst6(); tst3();
tst7(); tst4();
tst8(); tst5();
tst9(); tst6();
tst10(); tst7();
tst11(); tst8();
gorrila_test(0, 4, 3, 20, 5); tst9();
gorrila_test(1, 4, 3, 20, 5); tst10();
gorrila_test(2, 4, 3, 20, 5); tst11();
gorrila_test(0, 4, 2, 20, 5); gorrila_test(0, 4, 3, 20, 5);
gorrila_test(0, 4, 2, 20, 5); gorrila_test(1, 4, 3, 20, 5);
#endif gorrila_test(2, 4, 3, 20, 5);
gorrila_test(0, 10, 7, 20, 11); gorrila_test(0, 4, 2, 20, 5);
gorrila_test(0, 4, 2, 20, 5);
}
else {
gorrila_test(0, 10, 7, 20, 11);
}
} }