mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2014-07-02 23:49:04 +02:00
commit 9d221c037a
8 changed files with 134 additions and 99 deletions
Download patch file Download diff file Expand all files Collapse all files

31
scripts/mk_util.py
View file

@ -80,7 +80,7 @@ GPROF=False
GIT_HASH=False GIT_HASH=False
def check_output(cmd): def check_output(cmd):
return subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0].rstrip('\r\n') return str(subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).rstrip('\r\n')
def git_hash(): def git_hash():
try: try:
@ -810,6 +810,9 @@ class Component:
def require_mem_initializer(self): def require_mem_initializer(self):
return False return False
def mk_install_deps(self, out):
return
def mk_install(self, out): def mk_install(self, out):
return return
@ -853,6 +856,9 @@ class LibComponent(Component):
out.write('\n') out.write('\n')
out.write('%s: %s\n\n' % (self.name, libfile)) out.write('%s: %s\n\n' % (self.name, libfile))
def mk_install_dep(self, out):
out.write('%s' % libfile)
def mk_install(self, out): def mk_install(self, out):
for include in self.includes2install: for include in self.includes2install:
out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(PREFIX)', 'include', include))) out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(PREFIX)', 'include', include)))
@ -935,6 +941,9 @@ class ExeComponent(Component):
def main_component(self): def main_component(self):
return self.install return self.install
def mk_install_dep(self, out):
out.write('%s' % exefile)
def mk_install(self, out): def mk_install(self, out):
if self.install: if self.install:
exefile = '%s$(EXE_EXT)' % self.exe_name exefile = '%s$(EXE_EXT)' % self.exe_name
@ -1076,6 +1085,11 @@ class DLLComponent(Component):
def require_def_file(self): def require_def_file(self):
return IS_WINDOWS and self.export_files return IS_WINDOWS and self.export_files
def mk_install_dep(self, out):
out.write('%s$(SO_EXT)' % self.dll_name)
if self.static:
out.write(' %s$(LIB_EXT)' % self.dll_name)
def mk_install(self, out): def mk_install(self, out):
if self.install: if self.install:
dllfile = '%s$(SO_EXT)' % self.dll_name dllfile = '%s$(SO_EXT)' % self.dll_name
@ -1611,7 +1625,11 @@ def mk_config():
print('Java Compiler: %s' % JAVAC) print('Java Compiler: %s' % JAVAC)
def mk_install(out): def mk_install(out):
out.write('install:\n') out.write('install: ')
for c in get_components():
c.mk_install_deps(out)
out.write(' ')
out.write('\n')
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'bin')) out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'bin'))
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'include')) out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'include'))
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'lib')) out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'lib'))
@ -2573,16 +2591,17 @@ def mk_vs_proj(name, components):
def mk_win_dist(build_path, dist_path): def mk_win_dist(build_path, dist_path):
for c in get_components(): for c in get_components():
c.mk_win_dist(build_path, dist_path) c.mk_win_dist(build_path, dist_path)
# Add Z3Py to lib directory # Add Z3Py to bin directory
for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)): print "Adding to %s\n" % dist_path
for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
shutil.copy(os.path.join(build_path, pyc), shutil.copy(os.path.join(build_path, pyc),
os.path.join(dist_path, 'bin', pyc)) os.path.join(dist_path, 'bin', pyc))
def mk_unix_dist(build_path, dist_path): def mk_unix_dist(build_path, dist_path):
for c in get_components(): for c in get_components():
c.mk_unix_dist(build_path, dist_path) c.mk_unix_dist(build_path, dist_path)
# Add Z3Py to lib directory # Add Z3Py to bin directory
for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)): for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
shutil.copy(os.path.join(build_path, pyc), shutil.copy(os.path.join(build_path, pyc),
os.path.join(dist_path, 'bin', pyc)) os.path.join(dist_path, 'bin', pyc))

17
src/ast/macros/quasi_macros.cpp
View file

@ -41,7 +41,7 @@ void quasi_macros::find_occurrences(expr * e) {
// we remember whether we have seen an expr once, or more than once; // we remember whether we have seen an expr once, or more than once;
// when we see it the second time, we don't have to visit it another time, // when we see it the second time, we don't have to visit it another time,
// as we are only intersted in finding unique function applications. // as we are only interested in finding unique function applications.
m_visited_once.reset(); m_visited_once.reset();
m_visited_more.reset(); m_visited_more.reset();
@ -61,7 +61,7 @@ void quasi_macros::find_occurrences(expr * e) {
case AST_VAR: break; case AST_VAR: break;
case AST_QUANTIFIER: m_todo.push_back(to_quantifier(cur)->get_expr()); break; case AST_QUANTIFIER: m_todo.push_back(to_quantifier(cur)->get_expr()); break;
case AST_APP: case AST_APP:
if (is_uninterp(cur) && !is_ground(cur)) { if (is_non_ground_uninterp(cur)) {
func_decl * f = to_app(cur)->get_decl(); func_decl * f = to_app(cur)->get_decl();
m_occurrences.insert_if_not_there(f, 0); m_occurrences.insert_if_not_there(f, 0);
occurrences_map::iterator it = m_occurrences.find_iterator(f); occurrences_map::iterator it = m_occurrences.find_iterator(f);
@ -76,6 +76,10 @@ void quasi_macros::find_occurrences(expr * e) {
} }
}; };
bool quasi_macros::is_non_ground_uninterp(expr const * e) const {
return is_non_ground(e) && is_uninterp(e);
}
bool quasi_macros::is_unique(func_decl * f) const { bool quasi_macros::is_unique(func_decl * f) const {
return m_occurrences.find(f) == 1; return m_occurrences.find(f) == 1;
} }
@ -149,6 +153,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
// Our definition of a quasi-macro: // Our definition of a quasi-macro:
// Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted, // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted,
// f[X] contains all universally quantified variables, and f does not occur in T[X]. // f[X] contains all universally quantified variables, and f does not occur in T[X].
TRACE("quasi_macros", tout << "Checking for quasi macro: " << mk_pp(e, m_manager) << std::endl;);
if (is_quantifier(e) && to_quantifier(e)->is_forall()) { if (is_quantifier(e) && to_quantifier(e)->is_forall()) {
quantifier * q = to_quantifier(e); quantifier * q = to_quantifier(e);
@ -157,23 +162,23 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
expr * lhs = to_app(qe)->get_arg(0); expr * lhs = to_app(qe)->get_arg(0);
expr * rhs = to_app(qe)->get_arg(1); expr * rhs = to_app(qe)->get_arg(1);
if (is_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) && if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
!depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) { !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
a = to_app(lhs); a = to_app(lhs);
t = rhs; t = rhs;
return true; return true;
} else if (is_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) && } else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
!depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) { !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {
a = to_app(rhs); a = to_app(rhs);
t = lhs; t = lhs;
return true; return true;
} }
} else if (m_manager.is_not(qe) && is_uninterp(to_app(qe)->get_arg(0)) && } else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) &&
is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false
a = to_app(to_app(qe)->get_arg(0)); a = to_app(to_app(qe)->get_arg(0));
t = m_manager.mk_false(); t = m_manager.mk_false();
return true; return true;
} else if (is_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true } else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
a = to_app(qe); a = to_app(qe);
t = m_manager.mk_true(); t = m_manager.mk_true();
return true; return true;

1
src/ast/macros/quasi_macros.h
View file

@ -45,6 +45,7 @@ class quasi_macros {
expr_mark m_visited_more; expr_mark m_visited_more;
bool is_unique(func_decl * f) const; bool is_unique(func_decl * f) const;
bool is_non_ground_uninterp(expr const * e) const;
bool fully_depends_on(app * a, quantifier * q) const; bool fully_depends_on(app * a, quantifier * q) const;
bool depends_on(expr * e, func_decl * f) const; bool depends_on(expr * e, func_decl * f) const;

1
src/smt/params/theory_arith_params.cpp
View file

@ -22,6 +22,7 @@ Revision History:
void theory_arith_params::updt_params(params_ref const & _p) { void theory_arith_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p); smt_params_helper p(_p);
m_arith_random_initial_value = p.arith_random_initial_value(); m_arith_random_initial_value = p.arith_random_initial_value();
m_arith_random_seed = p.random_seed();
m_arith_mode = static_cast<arith_solver_id>(p.arith_solver()); m_arith_mode = static_cast<arith_solver_id>(p.arith_solver());
m_nl_arith = p.arith_nl(); m_nl_arith = p.arith_nl();
m_nl_arith_gb = p.arith_nl_gb(); m_nl_arith_gb = p.arith_nl_gb();

2
src/smt/smt_context.cpp
View file

@ -3945,7 +3945,7 @@ namespace smt {
m_fingerprints.display(tout); m_fingerprints.display(tout);
); );
failure fl = get_last_search_failure(); failure fl = get_last_search_failure();
if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) { if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == THEORY) {
// don't generate model. // don't generate model.
return; return;
} }

50
src/tactic/core/cofactor_elim_term_ite.cpp
View file

@ -29,6 +29,7 @@ struct cofactor_elim_term_ite::imp {
ast_manager & m; ast_manager & m;
params_ref m_params; params_ref m_params;
unsigned long long m_max_memory; unsigned long long m_max_memory;
bool m_cofactor_equalities;
volatile bool m_cancel; volatile bool m_cancel;
void checkpoint() { void checkpoint() {
@ -36,7 +37,7 @@ struct cofactor_elim_term_ite::imp {
if (memory::get_allocation_size() > m_max_memory) if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG); throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
if (m_cancel) if (m_cancel)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG); throw tactic_exception(TACTIC_CANCELED_MSG);
} }
// Collect atoms that contain term if-then-else // Collect atoms that contain term if-then-else
@ -111,7 +112,7 @@ struct cofactor_elim_term_ite::imp {
frame & fr = m_frame_stack.back(); frame & fr = m_frame_stack.back();
expr * t = fr.m_t; expr * t = fr.m_t;
bool form_ctx = fr.m_form_ctx; bool form_ctx = fr.m_form_ctx;
TRACE("cofactor_ite_analyzer", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";); TRACE("cofactor", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
m_owner.checkpoint(); m_owner.checkpoint();
@ -150,7 +151,7 @@ struct cofactor_elim_term_ite::imp {
} }
if (i < num_args) { if (i < num_args) {
m_has_term_ite.mark(t); m_has_term_ite.mark(t);
TRACE("cofactor_ite_analyzer", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";); TRACE("cofactor", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
save_candidate(t, form_ctx); save_candidate(t, form_ctx);
} }
} }
@ -167,6 +168,7 @@ struct cofactor_elim_term_ite::imp {
}; };
expr * get_first(expr * t) { expr * get_first(expr * t) {
TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";);
typedef std::pair<expr *, unsigned> frame; typedef std::pair<expr *, unsigned> frame;
expr_fast_mark1 visited; expr_fast_mark1 visited;
sbuffer<frame> stack; sbuffer<frame> stack;
@ -225,6 +227,7 @@ struct cofactor_elim_term_ite::imp {
\brief Fuctor for selecting the term if-then-else condition with the most number of occurrences. \brief Fuctor for selecting the term if-then-else condition with the most number of occurrences.
*/ */
expr * get_best(expr * t) { expr * get_best(expr * t) {
TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";);
typedef std::pair<expr *, unsigned> frame; typedef std::pair<expr *, unsigned> frame;
obj_map<expr, unsigned> occs; obj_map<expr, unsigned> occs;
expr_fast_mark1 visited; expr_fast_mark1 visited;
@ -299,12 +302,17 @@ struct cofactor_elim_term_ite::imp {
} }
} }
visited.reset(); visited.reset();
CTRACE("cofactor_ite_get_best", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";); CTRACE("cofactor", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";);
return best; return best;
} }
void updt_params(params_ref const & p) { void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_cofactor_equalities = p.get_bool("cofactor_equalities", true);
}
void collect_param_descrs(param_descrs & r) {
r.insert("cofactor_equalities", CPK_BOOL, "(default: true) use equalities to rewrite bodies of ite-expressions. This is potentially expensive.");
} }
void set_cancel(bool f) { void set_cancel(bool f) {
@ -354,16 +362,16 @@ struct cofactor_elim_term_ite::imp {
m_term = 0; m_term = 0;
expr * lhs; expr * lhs;
expr * rhs; expr * rhs;
if (m.is_eq(t, lhs, rhs)) { if (m_owner.m_cofactor_equalities && m.is_eq(t, lhs, rhs)) {
if (m.is_unique_value(lhs)) { if (m.is_unique_value(lhs)) {
m_term = rhs; m_term = rhs;
m_value = to_app(lhs); m_value = to_app(lhs);
TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";); TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
} }
else if (m.is_unique_value(rhs)) { else if (m.is_unique_value(rhs)) {
m_term = lhs; m_term = lhs;
m_value = to_app(rhs); m_value = to_app(rhs);
TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";); TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
} }
} }
// TODO: bounds // TODO: bounds
@ -467,7 +475,7 @@ struct cofactor_elim_term_ite::imp {
m_cofactor.set_cofactor_atom(neg_c); m_cofactor.set_cofactor_atom(neg_c);
m_cofactor(curr, neg_cofactor); m_cofactor(curr, neg_cofactor);
curr = m.mk_ite(c, pos_cofactor, neg_cofactor); curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";); TRACE("cofactor", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
} }
} }
return false; return false;
@ -522,7 +530,7 @@ struct cofactor_elim_term_ite::imp {
void cofactor(expr * t, expr_ref & r) { void cofactor(expr * t, expr_ref & r) {
unsigned step = 0; unsigned step = 0;
TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";); TRACE("cofactor", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";);
expr_ref curr(m); expr_ref curr(m);
curr = t; curr = t;
while (true) { while (true) {
@ -543,21 +551,20 @@ struct cofactor_elim_term_ite::imp {
m_cofactor(curr, neg_cofactor); m_cofactor(curr, neg_cofactor);
if (pos_cofactor == neg_cofactor) { if (pos_cofactor == neg_cofactor) {
curr = pos_cofactor; curr = pos_cofactor;
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
continue;
} }
if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) { else if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) {
curr = c; curr = c;
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
continue;
} }
if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) { else if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) {
curr = neg_c; curr = neg_c;
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
continue;
} }
else {
curr = m.mk_ite(c, pos_cofactor, neg_cofactor); curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";); }
TRACE("cofactor",
tout << "cofactor_ite step: " << step << "\n";
tout << "cofactor: " << mk_ismt2_pp(c, m) << "\n";
tout << mk_ismt2_pp(curr, m) << "\n";);
} }
} }
@ -570,6 +577,7 @@ struct cofactor_elim_term_ite::imp {
void operator()(expr * t, expr_ref & r) { void operator()(expr * t, expr_ref & r) {
ptr_vector<expr> new_args; ptr_vector<expr> new_args;
SASSERT(m_frames.empty());
m_frames.push_back(frame(t, true)); m_frames.push_back(frame(t, true));
while (!m_frames.empty()) { while (!m_frames.empty()) {
m_owner.checkpoint(); m_owner.checkpoint();
@ -649,7 +657,8 @@ struct cofactor_elim_term_ite::imp {
imp(ast_manager & _m, params_ref const & p): imp(ast_manager & _m, params_ref const & p):
m(_m), m(_m),
m_params(p) { m_params(p),
m_cofactor_equalities(true) {
m_cancel = false; m_cancel = false;
updt_params(p); updt_params(p);
} }
@ -686,7 +695,8 @@ void cofactor_elim_term_ite::updt_params(params_ref const & p) {
m_imp->updt_params(p); m_imp->updt_params(p);
} }
void cofactor_elim_term_ite::get_param_descrs(param_descrs & r) { void cofactor_elim_term_ite::collect_param_descrs(param_descrs & r) {
m_imp->collect_param_descrs(r);
} }
void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) { void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {

2
src/tactic/core/cofactor_elim_term_ite.h
View file

@ -31,7 +31,7 @@ public:
virtual ~cofactor_elim_term_ite(); virtual ~cofactor_elim_term_ite();
void updt_params(params_ref const & p); void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r); void collect_param_descrs(param_descrs & r);
void operator()(expr * t, expr_ref & r); void operator()(expr * t, expr_ref & r);

3
src/tactic/core/cofactor_term_ite_tactic.cpp
View file

@ -52,8 +52,7 @@ public:
virtual ~cofactor_term_ite_tactic() {} virtual ~cofactor_term_ite_tactic() {}
virtual void updt_params(params_ref const & p) { m_params = p; m_elim_ite.updt_params(p); } virtual void updt_params(params_ref const & p) { m_params = p; m_elim_ite.updt_params(p); }
static void get_param_descrs(param_descrs & r) { cofactor_elim_term_ite::get_param_descrs(r); } virtual void collect_param_descrs(param_descrs & r) { m_elim_ite.collect_param_descrs(r); }
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
virtual void operator()(goal_ref const & g, virtual void operator()(goal_ref const & g,
goal_ref_buffer & result, goal_ref_buffer & result,