From ed5058d225f63a1f78e796d976c424f7ceee931a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 21 Aug 2017 18:21:31 +0100 Subject: [PATCH 01/12] Fixed typo in ML API. Relates to #1214. --- src/api/ml/z3.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 0207a53ed..4f10b275a 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1912,7 +1912,7 @@ sig (* union of regular expressions *) val mk_re_union : context -> Expr.expr list -> Expr.expr - (* concatenation of regular expressions* ) + (* concatenation of regular expressions *) val mk_re_concat : context -> Expr.expr list -> Expr.expr (* regular expression for the range between two characters *) From cb87d47f08281f3e2cefac07d4e4ea80e97e21e9 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Tue, 22 Aug 2017 17:03:20 +0000 Subject: [PATCH 02/12] obj_hashtable: Constify --- src/util/obj_hashtable.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 9c3473e3d..189d1e1a0 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -134,7 +134,7 @@ public: return m_table.end(); } - void insert(Key * k, Value const & v) { + void insert(Key * const k, Value const & v) { m_table.insert(key_data(k, v)); } @@ -150,7 +150,7 @@ public: return m_table.find_core(key_data(k)); } - bool find(Key * k, Value & v) const { + bool find(Key * const k, Value & v) const { obj_map_entry * e = find_core(k); if (e) { v = e->get_data().m_value; From 4cb7f72509b6a590b1f706f0f7be09e76ac6e1a5 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Thu, 17 Aug 2017 16:43:25 +0000 Subject: [PATCH 03/12] First version of the inj. tactic --- scripts/mk_project.py | 10 +- src/tactic/core/injectivity_tactic.cpp | 305 +++++++++++++++++++++++++ src/tactic/core/injectivity_tactic.h | 32 +++ 3 files changed, 342 insertions(+), 5 deletions(-) create mode 100644 src/tactic/core/injectivity_tactic.cpp create mode 100644 src/tactic/core/injectivity_tactic.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b40205445..64dd93faa 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -23,6 +23,10 @@ def init_project_def(): add_lib('subpaving', ['interval'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) add_lib('rewriter', ['ast', 'polynomial', 'automata'], 'ast/rewriter') + # Simplifier module will be deleted in the future. + # It has been replaced with rewriter module. + add_lib('simplifier', ['rewriter'], 'ast/simplifier') + add_lib('macros', ['simplifier'], 'ast/macros') add_lib('normal_forms', ['rewriter'], 'ast/normal_forms') add_lib('model', ['rewriter']) add_lib('tactic', ['ast', 'model']) @@ -30,7 +34,7 @@ def init_project_def(): add_lib('parser_util', ['ast'], 'parsers/util') add_lib('grobner', ['ast'], 'math/grobner') add_lib('euclid', ['util'], 'math/euclid') - add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core') + add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter'], 'tactic/core') add_lib('sat_tactic', ['tactic', 'sat'], 'sat/tactic') add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith') add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic') @@ -43,11 +47,7 @@ def init_project_def(): add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds') add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2') add_lib('proof_checker', ['rewriter'], 'ast/proof_checker') - # Simplifier module will be deleted in the future. - # It has been replaced with rewriter module. - add_lib('simplifier', ['rewriter'], 'ast/simplifier') add_lib('fpa', ['ast', 'util', 'simplifier', 'model'], 'ast/fpa') - add_lib('macros', ['simplifier'], 'ast/macros') add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern') add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster') add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params') diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp new file mode 100644 index 000000000..d8b5e6acf --- /dev/null +++ b/src/tactic/core/injectivity_tactic.cpp @@ -0,0 +1,305 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + injectivity_tactic.cpp + +Abstract: + + Injectivity tactics + - Discover axioms of the form `forall x. (= (g (f x)) x` + Mark `f` as injective + - Rewrite (sub)terms of the form `(= (f x) (f y))` to `(= x y)` whenever `f` is injective. + +Author: + + Nicolas Braud-Santoni (t-nibrau) 2017-08-10 + +Notes: + +--*/ +#include +#include +#include "tactic/tactical.h" +#include "ast/rewriter/rewriter_def.h" +#include "tactic/core/injectivity_tactic.h" +#include "util/dec_ref_util.h" + + +class injectivity_tactic : public tactic { + + struct InjHelper : public obj_map*> { + ast_manager & m_manager; + + void insert(func_decl* const f, func_decl* const g) { + obj_hashtable *m; + if (! obj_map::find(f, m)) { + m_manager.inc_ref(f); + m = alloc(obj_hashtable); // TODO: Check we don't leak memory + obj_map::insert(f, m); + } + if (!m->contains(g)) { + m_manager.inc_ref(g); + m->insert(g); + } + } + + bool find(func_decl* const f, func_decl* const g) const { + obj_hashtable *m; + if(! obj_map::find(f, m)) + return false; + + return m->contains(g); + } + + InjHelper(ast_manager& m) : obj_map*>(), m_manager(m) {} + ~InjHelper() { + for(auto m : *this) { + for (func_decl* f : *m.get_value()) + m_manager.dec_ref(f); + + m_manager.dec_ref(m.m_key); + dealloc(m.m_value); + } + } + + }; + + struct finder { + ast_manager & m_manager; + InjHelper & inj_map; + + finder(ast_manager & m, InjHelper & map, params_ref const & p) : + m_manager(m), + inj_map(map) { + updt_params(p); + } + + ast_manager & m() const { return m_manager; } + + bool is_axiom(expr* n, func_decl* &f, func_decl* &g) { + if (!is_quantifier(n)) + return false; + + quantifier* const q = to_quantifier(n); + if (!q->is_forall() || q->get_num_decls() != 1) + return false; + + const expr * const body = q->get_expr(); + + // n ~= forall x. body + + if (!m().is_eq(body)) + return false; + + const app * const body_a = to_app(body); + if (body_a->get_num_args() != 2) + return false; + + const expr* a = body_a->get_arg(0); + const expr* b = body_a->get_arg(1); + + // n ~= forall x. (= a b) + + if (is_app(a) && is_var(b)) { + // Do nothing + } + else if (is_app(b) && is_var(a)) { + std::swap(a, b); + } + else + return false; + + const app* const a_app = to_app(a); + const var* const b_var = to_var(b); + + if (b_var->get_idx() != 0) // idx is the De Bruijn's index + return false; + + if (a_app->get_num_args() != 1) + return false; + + g = a_app->get_decl(); + const expr* const a_body = a_app->get_arg(0); + + // n ~= forall x. (= (g a_body) x) + + if (!is_app(a_body)) + return false; + const app* const a_body_app = to_app(a_body); + if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions + return false; + + f = a_body_app->get_decl(); + const expr* const a_body_body = a_body_app->get_arg(0); + + // n ~= forall x. (= (g (f a_body_body)) x) + if (a_body_body != b_var) + return false; + + // n ~= forall x. (= (g (f x)) x) + + return true; + } + + void operator()(goal_ref const & goal, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(goal->is_well_sorted()); + mc = 0; pc = 0; core = 0; + tactic_report report("injectivity", *goal); + fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores + fail_if_proof_generation("injectivity", goal); + + for (unsigned i = 0; i < goal->size(); ++i) { + func_decl *f, *g; + if (!is_axiom(goal->form(i), f, g)) continue; + TRACE("injectivity_finder", tout << "Marking " << f->get_name() << " as injective" << std::endl;); + inj_map.insert(f, g); + // TODO: Record that g is f's pseudoinverse + } + } + + void updt_params(params_ref const & p) {} + }; + + struct rewriter_eq_cfg : public default_rewriter_cfg { + ast_manager & m_manager; + InjHelper & inj_map; +// expr_ref_vector m_out; +// sort_ref_vector m_bindings; + + ast_manager & m() const { return m_manager; } + + rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) { + } + + ~rewriter_eq_cfg() { + } + + void cleanup_buffers() { +// m_out.finalize(); + } + + void reset() { + } + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + if(num != 2) + return BR_FAILED; + + if (!m().is_eq(f)) + return BR_FAILED; + + // We are rewriting (= a b) + if (!is_app(args[0]) || !is_app(args[1])) + return BR_FAILED; + + const app* const a = to_app(args[0]); + const app* const b = to_app(args[1]); + + // a and b are applications of the same function + if (a->get_decl() != b->get_decl()) + return BR_FAILED; + + // Maybe TODO: Generalize to multi-parameter functions ? + if (a->get_num_args() != 1 || b->get_num_args() != 1) + return BR_FAILED; + + if (!inj_map.contains(a->get_decl())) + return BR_FAILED; + + SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0))); + TRACE("injectivity_eq", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << + " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); + result = m().mk_eq(a->get_arg(0), b->get_arg(0)); + result_pr = nullptr; + return BR_DONE; + } + + }; + + struct rewriter_eq : public rewriter_tpl { + rewriter_eq_cfg m_cfg; + rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, map, p) { + } + }; + + struct rewriter_inverse { }; + + finder * m_finder; + rewriter_eq * m_eq; + InjHelper * m_map; +// rewriter_inverse * m_inverse; + + params_ref m_params; + ast_manager & m_manager; + +public: + injectivity_tactic(ast_manager & m, params_ref const & p): + m_params(p), + m_manager(m) { + TRACE("injectivity", tout << "constructed new tactic" << std::endl;); + m_map = alloc(InjHelper, m); + m_finder = alloc(finder, m, *m_map, p); + m_eq = alloc(rewriter_eq, m, *m_map, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(injectivity_tactic, m, m_params); + } + + virtual ~injectivity_tactic() { + dealloc(m_finder); + dealloc(m_eq); + dealloc(m_map); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_finder->updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + insert_produce_models(r); + r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); + } + + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + std::cerr << "injectivity finder: " << m_finder << std::endl; + (*m_finder)(g, result, mc, pc, core); + + for (unsigned i = 0; i < g->size(); ++i) { + std::cerr << "injectivity rewrite " << i << std::endl; + expr* curr = g->form(i); + expr_ref rw(m_manager); + proof_ref pr(m_manager); + (*m_eq)(curr, rw, pr); + g->update(i, rw, pr, g->dep(i)); + } + } + + virtual void cleanup() { + InjHelper * m = alloc(InjHelper, m_manager); + finder * f = alloc(finder, m_manager, *m, m_params); + rewriter_eq * r = alloc(rewriter_eq, m_manager, *m, m_params); + std::swap(m, m_map), std::swap(f, m_finder), std::swap(r, m_eq); + dealloc(m), dealloc(f), dealloc(r); + } + + +}; + +tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p) { + return alloc(injectivity_tactic, m, p); +} diff --git a/src/tactic/core/injectivity_tactic.h b/src/tactic/core/injectivity_tactic.h new file mode 100644 index 000000000..447357912 --- /dev/null +++ b/src/tactic/core/injectivity_tactic.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + injectivity_tactic.h + +Abstract: + + Injectivity tactics + +Author: + + Nicolas Braud-Santoni (t-nibrau) 2017-08-10 + +Notes: + +--*/ +#ifndef INJECTIVITY_TACTIC_H_ +#define INJECTIVITY_TACTIC_H_ + +#include "util/params.h" +class ast_manager; +class tactic; + +tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("injectivity", "Identifies and applies injectivity axioms.", "mk_injectivity_tactic(m, p)") +*/ + +#endif From c0b6d00e8aa9a19d2cca474aaad9d0fd37af408e Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Tue, 22 Aug 2017 18:09:38 +0000 Subject: [PATCH 04/12] Update debug output --- src/tactic/core/injectivity_tactic.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index d8b5e6acf..75685c891 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -157,7 +157,7 @@ class injectivity_tactic : public tactic { for (unsigned i = 0; i < goal->size(); ++i) { func_decl *f, *g; if (!is_axiom(goal->form(i), f, g)) continue; - TRACE("injectivity_finder", tout << "Marking " << f->get_name() << " as injective" << std::endl;); + TRACE("injectivity", tout << "Marking " << f->get_name() << " as injective" << std::endl;); inj_map.insert(f, g); // TODO: Record that g is f's pseudoinverse } @@ -213,7 +213,7 @@ class injectivity_tactic : public tactic { return BR_FAILED; SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0))); - TRACE("injectivity_eq", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << + TRACE("injectivity", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); result = m().mk_eq(a->get_arg(0), b->get_arg(0)); result_pr = nullptr; @@ -276,11 +276,9 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - std::cerr << "injectivity finder: " << m_finder << std::endl; (*m_finder)(g, result, mc, pc, core); for (unsigned i = 0; i < g->size(); ++i) { - std::cerr << "injectivity rewrite " << i << std::endl; expr* curr = g->form(i); expr_ref rw(m_manager); proof_ref pr(m_manager); From 33dd168195cf561786163adce7e471f82f011aeb Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Tue, 22 Aug 2017 18:09:57 +0000 Subject: [PATCH 05/12] Remove unnecessary parameter --- src/tactic/core/injectivity_tactic.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 75685c891..4dc3fe5d5 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -268,7 +268,6 @@ public: virtual void collect_param_descrs(param_descrs & r) { insert_max_memory(r); insert_produce_models(r); - r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); } virtual void operator()(goal_ref const & g, From 27fd879b8ceb5aee860ae1c7ffa3e1afe2727159 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Tue, 22 Aug 2017 18:44:34 +0000 Subject: [PATCH 06/12] injectivity: Fixup rewriter --- src/tactic/core/injectivity_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 4dc3fe5d5..95e380982 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -284,7 +284,8 @@ public: (*m_eq)(curr, rw, pr); g->update(i, rw, pr, g->dep(i)); } - } + result.push_back(g.get()); + } virtual void cleanup() { InjHelper * m = alloc(InjHelper, m_manager); From ae9ace232143af631af831a23d48c9f7fbd471c1 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Wed, 23 Aug 2017 10:25:33 +0000 Subject: [PATCH 07/12] injectivity: Cleanup whitespace --- src/tactic/core/injectivity_tactic.cpp | 340 ++++++++++++------------- 1 file changed, 170 insertions(+), 170 deletions(-) diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 95e380982..7d90a2155 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -29,120 +29,120 @@ Notes: class injectivity_tactic : public tactic { - struct InjHelper : public obj_map*> { - ast_manager & m_manager; + struct InjHelper : public obj_map*> { + ast_manager & m_manager; - void insert(func_decl* const f, func_decl* const g) { - obj_hashtable *m; - if (! obj_map::find(f, m)) { - m_manager.inc_ref(f); - m = alloc(obj_hashtable); // TODO: Check we don't leak memory - obj_map::insert(f, m); - } - if (!m->contains(g)) { - m_manager.inc_ref(g); - m->insert(g); - } - } + void insert(func_decl* const f, func_decl* const g) { + obj_hashtable *m; + if (! obj_map::find(f, m)) { + m_manager.inc_ref(f); + m = alloc(obj_hashtable); // TODO: Check we don't leak memory + obj_map::insert(f, m); + } + if (!m->contains(g)) { + m_manager.inc_ref(g); + m->insert(g); + } + } - bool find(func_decl* const f, func_decl* const g) const { - obj_hashtable *m; - if(! obj_map::find(f, m)) - return false; + bool find(func_decl* const f, func_decl* const g) const { + obj_hashtable *m; + if(! obj_map::find(f, m)) + return false; - return m->contains(g); - } + return m->contains(g); + } - InjHelper(ast_manager& m) : obj_map*>(), m_manager(m) {} - ~InjHelper() { - for(auto m : *this) { - for (func_decl* f : *m.get_value()) - m_manager.dec_ref(f); + InjHelper(ast_manager& m) : obj_map*>(), m_manager(m) {} + ~InjHelper() { + for(auto m : *this) { + for (func_decl* f : *m.get_value()) + m_manager.dec_ref(f); - m_manager.dec_ref(m.m_key); - dealloc(m.m_value); - } - } + m_manager.dec_ref(m.m_key); + dealloc(m.m_value); + } + } - }; + }; struct finder { ast_manager & m_manager; - InjHelper & inj_map; + InjHelper & inj_map; - finder(ast_manager & m, InjHelper & map, params_ref const & p) : + finder(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), - inj_map(map) { + inj_map(map) { updt_params(p); } - + ast_manager & m() const { return m_manager; } - bool is_axiom(expr* n, func_decl* &f, func_decl* &g) { - if (!is_quantifier(n)) - return false; + bool is_axiom(expr* n, func_decl* &f, func_decl* &g) { + if (!is_quantifier(n)) + return false; - quantifier* const q = to_quantifier(n); - if (!q->is_forall() || q->get_num_decls() != 1) - return false; + quantifier* const q = to_quantifier(n); + if (!q->is_forall() || q->get_num_decls() != 1) + return false; - const expr * const body = q->get_expr(); + const expr * const body = q->get_expr(); - // n ~= forall x. body + // n ~= forall x. body - if (!m().is_eq(body)) - return false; + if (!m().is_eq(body)) + return false; - const app * const body_a = to_app(body); - if (body_a->get_num_args() != 2) - return false; + const app * const body_a = to_app(body); + if (body_a->get_num_args() != 2) + return false; - const expr* a = body_a->get_arg(0); - const expr* b = body_a->get_arg(1); + const expr* a = body_a->get_arg(0); + const expr* b = body_a->get_arg(1); - // n ~= forall x. (= a b) + // n ~= forall x. (= a b) - if (is_app(a) && is_var(b)) { - // Do nothing - } - else if (is_app(b) && is_var(a)) { - std::swap(a, b); - } - else - return false; + if (is_app(a) && is_var(b)) { + // Do nothing + } + else if (is_app(b) && is_var(a)) { + std::swap(a, b); + } + else + return false; - const app* const a_app = to_app(a); - const var* const b_var = to_var(b); + const app* const a_app = to_app(a); + const var* const b_var = to_var(b); - if (b_var->get_idx() != 0) // idx is the De Bruijn's index - return false; + if (b_var->get_idx() != 0) // idx is the De Bruijn's index + return false; - if (a_app->get_num_args() != 1) - return false; + if (a_app->get_num_args() != 1) + return false; - g = a_app->get_decl(); - const expr* const a_body = a_app->get_arg(0); + g = a_app->get_decl(); + const expr* const a_body = a_app->get_arg(0); - // n ~= forall x. (= (g a_body) x) + // n ~= forall x. (= (g a_body) x) - if (!is_app(a_body)) - return false; - const app* const a_body_app = to_app(a_body); - if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions - return false; + if (!is_app(a_body)) + return false; + const app* const a_body_app = to_app(a_body); + if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions + return false; - f = a_body_app->get_decl(); - const expr* const a_body_body = a_body_app->get_arg(0); - - // n ~= forall x. (= (g (f a_body_body)) x) - if (a_body_body != b_var) - return false; + f = a_body_app->get_decl(); + const expr* const a_body_body = a_body_app->get_arg(0); - // n ~= forall x. (= (g (f x)) x) + // n ~= forall x. (= (g (f a_body_body)) x) + if (a_body_body != b_var) + return false; + + // n ~= forall x. (= (g (f x)) x) + + return true; + } - return true; - } - void operator()(goal_ref const & goal, goal_ref_buffer & result, model_converter_ref & mc, @@ -152,112 +152,112 @@ class injectivity_tactic : public tactic { mc = 0; pc = 0; core = 0; tactic_report report("injectivity", *goal); fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores - fail_if_proof_generation("injectivity", goal); + fail_if_proof_generation("injectivity", goal); - for (unsigned i = 0; i < goal->size(); ++i) { - func_decl *f, *g; - if (!is_axiom(goal->form(i), f, g)) continue; - TRACE("injectivity", tout << "Marking " << f->get_name() << " as injective" << std::endl;); - inj_map.insert(f, g); - // TODO: Record that g is f's pseudoinverse - } + for (unsigned i = 0; i < goal->size(); ++i) { + func_decl *f, *g; + if (!is_axiom(goal->form(i), f, g)) continue; + TRACE("injectivity", tout << "Marking " << f->get_name() << " as injective" << std::endl;); + inj_map.insert(f, g); + // TODO: Record that g is f's pseudoinverse + } } void updt_params(params_ref const & p) {} }; - struct rewriter_eq_cfg : public default_rewriter_cfg { - ast_manager & m_manager; - InjHelper & inj_map; -// expr_ref_vector m_out; -// sort_ref_vector m_bindings; + struct rewriter_eq_cfg : public default_rewriter_cfg { + ast_manager & m_manager; + InjHelper & inj_map; +// expr_ref_vector m_out; +// sort_ref_vector m_bindings; - ast_manager & m() const { return m_manager; } + ast_manager & m() const { return m_manager; } - rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) { - } + rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) { + } - ~rewriter_eq_cfg() { - } + ~rewriter_eq_cfg() { + } - void cleanup_buffers() { -// m_out.finalize(); - } + void cleanup_buffers() { +// m_out.finalize(); + } - void reset() { - } + void reset() { + } - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - if(num != 2) - return BR_FAILED; + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + if(num != 2) + return BR_FAILED; - if (!m().is_eq(f)) - return BR_FAILED; + if (!m().is_eq(f)) + return BR_FAILED; - // We are rewriting (= a b) - if (!is_app(args[0]) || !is_app(args[1])) - return BR_FAILED; + // We are rewriting (= a b) + if (!is_app(args[0]) || !is_app(args[1])) + return BR_FAILED; - const app* const a = to_app(args[0]); - const app* const b = to_app(args[1]); + const app* const a = to_app(args[0]); + const app* const b = to_app(args[1]); - // a and b are applications of the same function - if (a->get_decl() != b->get_decl()) - return BR_FAILED; + // a and b are applications of the same function + if (a->get_decl() != b->get_decl()) + return BR_FAILED; - // Maybe TODO: Generalize to multi-parameter functions ? - if (a->get_num_args() != 1 || b->get_num_args() != 1) - return BR_FAILED; + // Maybe TODO: Generalize to multi-parameter functions ? + if (a->get_num_args() != 1 || b->get_num_args() != 1) + return BR_FAILED; - if (!inj_map.contains(a->get_decl())) - return BR_FAILED; + if (!inj_map.contains(a->get_decl())) + return BR_FAILED; - SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0))); - TRACE("injectivity", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << - " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); - result = m().mk_eq(a->get_arg(0), b->get_arg(0)); - result_pr = nullptr; - return BR_DONE; - } + SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0))); + TRACE("injectivity", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << + " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); + result = m().mk_eq(a->get_arg(0), b->get_arg(0)); + result_pr = nullptr; + return BR_DONE; + } - }; + }; - struct rewriter_eq : public rewriter_tpl { - rewriter_eq_cfg m_cfg; - rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) : - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m, map, p) { - } - }; + struct rewriter_eq : public rewriter_tpl { + rewriter_eq_cfg m_cfg; + rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, map, p) { + } + }; - struct rewriter_inverse { }; + struct rewriter_inverse { }; finder * m_finder; - rewriter_eq * m_eq; - InjHelper * m_map; -// rewriter_inverse * m_inverse; + rewriter_eq * m_eq; + InjHelper * m_map; +// rewriter_inverse * m_inverse; params_ref m_params; - ast_manager & m_manager; + ast_manager & m_manager; public: injectivity_tactic(ast_manager & m, params_ref const & p): m_params(p), - m_manager(m) { - TRACE("injectivity", tout << "constructed new tactic" << std::endl;); - m_map = alloc(InjHelper, m); + m_manager(m) { + TRACE("injectivity", tout << "constructed new tactic" << std::endl;); + m_map = alloc(InjHelper, m); m_finder = alloc(finder, m, *m_map, p); - m_eq = alloc(rewriter_eq, m, *m_map, p); + m_eq = alloc(rewriter_eq, m, *m_map, p); } virtual tactic * translate(ast_manager & m) { return alloc(injectivity_tactic, m, m_params); } - + virtual ~injectivity_tactic() { dealloc(m_finder); - dealloc(m_eq); - dealloc(m_map); + dealloc(m_eq); + dealloc(m_map); } virtual void updt_params(params_ref const & p) { @@ -269,30 +269,30 @@ public: insert_max_memory(r); insert_produce_models(r); } - - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, + + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { (*m_finder)(g, result, mc, pc, core); - - for (unsigned i = 0; i < g->size(); ++i) { - expr* curr = g->form(i); - expr_ref rw(m_manager); - proof_ref pr(m_manager); - (*m_eq)(curr, rw, pr); - g->update(i, rw, pr, g->dep(i)); - } - result.push_back(g.get()); - } - + + for (unsigned i = 0; i < g->size(); ++i) { + expr* curr = g->form(i); + expr_ref rw(m_manager); + proof_ref pr(m_manager); + (*m_eq)(curr, rw, pr); + g->update(i, rw, pr, g->dep(i)); + } + result.push_back(g.get()); + } + virtual void cleanup() { - InjHelper * m = alloc(InjHelper, m_manager); - finder * f = alloc(finder, m_manager, *m, m_params); - rewriter_eq * r = alloc(rewriter_eq, m_manager, *m, m_params); - std::swap(m, m_map), std::swap(f, m_finder), std::swap(r, m_eq); - dealloc(m), dealloc(f), dealloc(r); + InjHelper * m = alloc(InjHelper, m_manager); + finder * f = alloc(finder, m_manager, *m, m_params); + rewriter_eq * r = alloc(rewriter_eq, m_manager, *m, m_params); + std::swap(m, m_map), std::swap(f, m_finder), std::swap(r, m_eq); + dealloc(m), dealloc(f), dealloc(r); } From b877c962caa73ae29be01a4dd28c7a82ac7600d3 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Wed, 23 Aug 2017 10:27:55 +0000 Subject: [PATCH 08/12] injectivity: Add tactic to CMake-based builds --- src/tactic/core/CMakeLists.txt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 1f766bd47..f192b4fa6 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -9,6 +9,7 @@ z3_add_component(core_tactics distribute_forall_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp + injectivity_tactic.cpp nnf_tactic.cpp occf_tactic.cpp pb_preprocess_tactic.cpp @@ -22,6 +23,7 @@ z3_add_component(core_tactics collect_occs.cpp COMPONENT_DEPENDENCIES normal_forms + rewriter tactic TACTIC_HEADERS blast_term_ite_tactic.h @@ -32,6 +34,7 @@ z3_add_component(core_tactics distribute_forall_tactic.h elim_term_ite_tactic.h elim_uncnstr_tactic.h + injectivity_tactic.h nnf_tactic.h occf_tactic.h pb_preprocess_tactic.h From 3e960eadd2b14f1da9b89927e6dd17cf77eea063 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 23 Aug 2017 12:14:19 +0100 Subject: [PATCH 09/12] (Re-)added option to disable lemma deletion in the smt_context. --- src/smt/params/smt_params.h | 31 +- src/smt/smt_context.cpp | 556 ++++++++++++++++++------------------ 2 files changed, 295 insertions(+), 292 deletions(-) diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 4539ebe58..b01499c04 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -31,7 +31,7 @@ Revision History: #include "smt/params/preprocessor_params.h" #include "cmd_context/context_params.h" -enum phase_selection { +enum phase_selection { PS_ALWAYS_FALSE, PS_ALWAYS_TRUE, PS_CACHING, @@ -52,7 +52,8 @@ enum restart_strategy { enum lemma_gc_strategy { LGC_FIXED, LGC_GEOMETRIC, - LGC_AT_RESTART + LGC_AT_RESTART, + LGC_NONE }; enum initial_activity { @@ -71,11 +72,11 @@ enum case_split_strategy { CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity }; -struct smt_params : public preprocessor_params, - public dyn_ack_params, - public qi_params, - public theory_arith_params, - public theory_array_params, +struct smt_params : public preprocessor_params, + public dyn_ack_params, + public qi_params, + public theory_arith_params, + public theory_array_params, public theory_bv_params, public theory_str_params, public theory_pb_params, @@ -153,12 +154,12 @@ struct smt_params : public preprocessor_params, unsigned m_lemma_gc_initial; double m_lemma_gc_factor; unsigned m_new_old_ratio; //!< the ratio of new and old clauses. - unsigned m_new_clause_activity; + unsigned m_new_clause_activity; unsigned m_old_clause_activity; unsigned m_new_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant. unsigned m_old_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant. double m_inv_clause_decay; //!< clause activity decay - + // ----------------------------------- // // SMT-LIB (debug) pretty printer @@ -166,7 +167,7 @@ struct smt_params : public preprocessor_params, // ----------------------------------- bool m_smtlib_dump_lemmas; symbol m_logic; - + // ----------------------------------- // // Statistics for Profiling @@ -179,10 +180,10 @@ struct smt_params : public preprocessor_params, // ----------------------------------- // - // Model generation + // Model generation // // ----------------------------------- - bool m_model; + bool m_model; bool m_model_compact; bool m_model_on_timeout; bool m_model_on_final_check; @@ -213,7 +214,7 @@ struct smt_params : public preprocessor_params, unsigned m_timeout; unsigned m_rlimit; bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples. - bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples. + bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples. bool m_dump_goal_as_smt; bool m_auto_config; @@ -237,7 +238,7 @@ struct smt_params : public preprocessor_params, m_display_proof(false), m_display_dot_proof(false), m_display_unsat_core(false), - m_check_proof(false), + m_check_proof(false), m_eq_propagation(true), m_binary_clause_opt(true), m_relevancy_lvl(2), @@ -279,7 +280,7 @@ struct smt_params : public preprocessor_params, m_new_old_ratio(16), m_new_clause_activity(10), m_old_clause_activity(500), - m_new_clause_relevancy(45), + m_new_clause_relevancy(45), m_old_clause_relevancy(6), m_inv_clause_decay(1), m_smtlib_dump_lemmas(false), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index daa408161..b966b8380 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -95,7 +95,7 @@ namespace smt { if (!relevancy()) m_fparams.m_relevancy_lemma = false; - + m_model_generator->set_context(this); } @@ -106,29 +106,29 @@ namespace smt { ast_manager& src_m = src_ctx.get_manager(); expr_ref dst_f(dst_m); - SASSERT(lit != false_literal && lit != true_literal); - bool_var v = b2v.get(lit.var(), null_bool_var); - if (v == null_bool_var) { - expr* e = src_ctx.m_bool_var2expr.get(lit.var(), 0); - SASSERT(e); - dst_f = tr(e); + SASSERT(lit != false_literal && lit != true_literal); + bool_var v = b2v.get(lit.var(), null_bool_var); + if (v == null_bool_var) { + expr* e = src_ctx.m_bool_var2expr.get(lit.var(), 0); + SASSERT(e); + dst_f = tr(e); v = dst_ctx.get_bool_var_of_id_option(dst_f->get_id()); - if (v != null_bool_var) { - } + if (v != null_bool_var) { + } else if (src_m.is_not(e) || src_m.is_and(e) || src_m.is_or(e) || - src_m.is_iff(e) || src_m.is_ite(e)) { - v = dst_ctx.mk_bool_var(dst_f); - } - else { - dst_ctx.internalize_formula(dst_f, false); - v = dst_ctx.get_bool_var(dst_f); - } - b2v.setx(lit.var(), v, null_bool_var); - } - return literal(v, lit.sign()); + src_m.is_iff(e) || src_m.is_ite(e)) { + v = dst_ctx.mk_bool_var(dst_f); + } + else { + dst_ctx.internalize_formula(dst_f, false); + v = dst_ctx.get_bool_var(dst_f); + } + b2v.setx(lit.var(), v, null_bool_var); + } + return literal(v, lit.sign()); } - bool context::get_cancel_flag() { + bool context::get_cancel_flag() { return !m_manager.limit().inc(); } @@ -137,12 +137,12 @@ namespace smt { ast_manager& dst_m = dst_ctx.get_manager(); ast_manager& src_m = src_ctx.get_manager(); src_ctx.pop_to_base_lvl(); - + if (src_ctx.m_base_lvl > 0) { throw default_exception("Cloning contexts within a user-scope is not allowed"); } SASSERT(src_ctx.m_base_lvl == 0); - + ast_translation tr(src_m, dst_m, false); dst_ctx.set_logic(src_ctx.m_setup.get_logic()); @@ -151,7 +151,7 @@ namespace smt { asserted_formulas& src_af = src_ctx.m_asserted_formulas; asserted_formulas& dst_af = dst_ctx.m_asserted_formulas; - // Copy asserted formulas. + // Copy asserted formulas. for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) { expr_ref fml(dst_m); proof_ref pr(dst_m); @@ -160,7 +160,7 @@ namespace smt { if (pr_src) { pr = tr(pr_src); } - dst_af.assert_expr(fml, pr); + dst_af.assert_expr(fml, pr); } if (!src_ctx.m_setup.already_configured()) { @@ -191,7 +191,7 @@ namespace smt { lits.push_back(lit); } dst_ctx.mk_clause(lits.size(), lits.c_ptr(), 0, src_cls.get_kind(), 0); - } + } vector::const_iterator it = src_ctx.m_watches.begin(); vector::const_iterator end = src_ctx.m_watches.end(); literal ls[2]; @@ -207,12 +207,12 @@ namespace smt { ls[0] = TRANSLATE(neg_l1); ls[1] = TRANSLATE(l2); dst_ctx.mk_clause(2, ls, 0, CLS_AUX, 0); - } + } } } #endif - - TRACE("smt_context", + + TRACE("smt_context", src_ctx.display(tout); dst_ctx.display(tout);); } @@ -227,7 +227,7 @@ namespace smt { // copy missing simplifier_plugins // remark: some simplifier_plugins are automatically created by the asserted_formulas class. simplifier & src_s = src.get_simplifier(); - simplifier & dst_s = dst.get_simplifier(); + simplifier & dst_s = dst.get_simplifier(); ptr_vector::const_iterator it1 = src_s.begin_plugins(); ptr_vector::const_iterator end1 = src_s.end_plugins(); for (; it1 != end1; ++it1) { @@ -248,9 +248,9 @@ namespace smt { context * context::mk_fresh(symbol const * l, smt_params * p) { context * new_ctx = alloc(context, m_manager, p == 0 ? m_fparams : *p); new_ctx->set_logic(l == 0 ? m_setup.get_logic() : *l); - copy_plugins(*this, *new_ctx); + copy_plugins(*this, *new_ctx); return new_ctx; - } + } void context::init() { app * t = m_manager.mk_true(); @@ -299,9 +299,9 @@ namespace smt { d.set_justification(j); } - + void context::assign_core(literal l, b_justification j, bool decision) { - TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; + TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n"; display(tout, j);); m_assigned_literals.push_back(l); @@ -319,7 +319,7 @@ namespace smt { d.m_phase = !l.sign(); TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";); - TRACE("relevancy", + TRACE("relevancy", tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";); if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l))) m_atom_propagation_queue.push_back(l); @@ -331,12 +331,12 @@ namespace smt { // a unit is asserted at search level. Mark it as relevant. // this addresses bug... where a literal becomes fixed to true (false) // as a conflict gets assigned misses relevancy (and quantifier instantiation). - // + // if (false && !decision && relevancy() && at_search_level() && !is_relevant_core(l)) { mark_as_relevant(l); } } - + bool context::bcp() { SASSERT(!inconsistent()); while (m_qhead < m_assigned_literals.size()) { @@ -385,17 +385,17 @@ namespace smt { cls->set_literal(0, cls->get_literal(1)); cls->set_literal(1, not_l); } - + SASSERT(cls->get_literal(1) == not_l); - - literal first_lit = cls->get_literal(0); + + literal first_lit = cls->get_literal(0); lbool first_lit_val = get_assignment(first_lit); - - if (first_lit_val == l_true) { - *it2 = *it; // clause is already satisfied, keep it + + if (first_lit_val == l_true) { + *it2 = *it; // clause is already satisfied, keep it it2++; } - else { + else { literal * it3 = cls->begin_literals() + 2; literal * end3 = cls->end_literals(); for(; it3 != end3; ++it3) { @@ -408,7 +408,7 @@ namespace smt { goto found_watch; } } - // did not find watch... + // did not find watch... if (first_lit_val == l_false) { // CONFLICT // copy remaining watches @@ -427,8 +427,8 @@ namespace smt { // PROPAGATION SASSERT(first_lit_val == l_undef); SASSERT(get_assignment(first_lit) == l_undef); - SASSERT(is_unit_clause(cls)); - *it2 = *it; + SASSERT(is_unit_clause(cls)); + *it2 = *it; it2++; // keep clause m_stats.m_num_propagations++; // It is safe to call assign_core instead of assign because first_lit is unassigned @@ -440,13 +440,13 @@ namespace smt { //if (!(m_manager.is_eq(e) && m_manager.get_sort(to_app(e)->get_arg(0))->get_family_id() == m_manager.get_family_id("array"))) mark_as_relevant(e); } - } - found_watch:; - } + } + found_watch:; + } } - SASSERT(it2 <= end); + SASSERT(it2 <= end); w.set_end_clause(it2); - } + } return true; } @@ -473,7 +473,7 @@ namespace smt { theory * t = get_theory(th); if (t->get_enode(lhs)->is_interpreted() && t->get_enode(rhs)->is_interpreted()) return; - TRACE("add_diseq", + TRACE("add_diseq", tout << "#" << t->get_enode(lhs)->get_owner_id() << " != " << "#" << t->get_enode(rhs)->get_owner_id() << "\n";); @@ -490,7 +490,7 @@ namespace smt { m_n1(n1), m_r2_num_parents(r2_num_parents) { } - + virtual void undo(context & ctx) { ctx.undo_add_eq(m_r1, m_n1, m_r2_num_parents); } @@ -506,27 +506,27 @@ namespace smt { TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";); TRACE("add_eq_detail", tout << "assigning\n" << mk_pp(n1->get_owner(), m_manager) << "\n" << mk_pp(n2->get_owner(), m_manager) << "\n"; tout << "kind: " << js.get_kind() << "\n";); - + m_stats.m_num_add_eq++; enode * r1 = n1->get_root(); enode * r2 = n2->get_root(); - + if (r1 == r2) { TRACE("add_eq", tout << "redundant constraint.\n";); return; } - + if (r1->is_interpreted() && r2->is_interpreted()) { TRACE("add_eq", tout << "interpreted roots conflict.\n";); set_conflict(mk_justification(eq_conflict_justification(n1, n2, js))); return; } - + // Swap r1 and r2: // 1. if the "equivalence" class of r1 is bigger than the equivalence class of r2 // OR // 2. r1 is interpreted but r2 is not. - // + // // The second condition is used to enforce the invariant that if a class contain // an interepreted enode then the root is also interpreted. if ((r1->get_class_size() > r2->get_class_size() && !r2->is_interpreted()) || r1->is_interpreted()) { @@ -534,10 +534,10 @@ namespace smt { std::swap(n1, n2); std::swap(r1, r2); } - - TRACE("add_eq", tout << "merging: #" << r1->get_owner_id() << " #" << r2->get_owner_id() << + + TRACE("add_eq", tout << "merging: #" << r1->get_owner_id() << " #" << r2->get_owner_id() << " n1: #" << n1->get_owner_id() << "\n";); - + // It is necessary to propagate relevancy to other elements of // the equivalence class. This is nessary to enforce the invariant // in the field m_parent of the enode class. @@ -554,13 +554,13 @@ namespace smt { else if (is_relevant(r2)) { // && !m_manager.is_eq(r2->get_owner())) { // !is_eq HACK mark_as_relevant(r1); } - + push_trail(add_eq_trail(r1, n1, r2->get_num_parents())); - + m_qmanager->add_eq_eh(r1, r2); - + merge_theory_vars(n2, n1, js); - + // 'Proof' tree // n1 -> ... -> r1 // n2 -> ... -> r2 @@ -571,8 +571,8 @@ namespace smt { SASSERT(r1->trans_reaches(n1)); // --------------- // r1 -> .. -> n1 -> n2 -> ... -> r2 - - + + #if 0 { static unsigned counter = 0; @@ -584,35 +584,35 @@ namespace smt { num_bad_adds++; } if (num_adds % 100000 == 0) { - verbose_stream() << "[add-eq]: " << num_bad_adds << " " << num_adds << " " + verbose_stream() << "[add-eq]: " << num_bad_adds << " " << num_adds << " " << static_cast(num_bad_adds)/static_cast(num_adds) << "\n"; } } #endif - - + + remove_parents_from_cg_table(r1); - + enode * curr = r1; do { curr->m_root = r2; curr = curr->m_next; } while(curr != r1); - + SASSERT(r1->get_root() == r2); - + reinsert_parents_into_cg_table(r1, r2, n1, n2, js); - + if (n2->is_bool()) propagate_bool_enode_assignment(r1, r2, n1, n2); - + // Merge "equivalence" classes std::swap(r1->m_next, r2->m_next); - + // Update "equivalence" class size r2->m_class_size += r1->m_class_size; - + CASSERT("add_eq", check_invariant()); } catch (...) { @@ -642,12 +642,12 @@ namespace smt { num_eqs++; num_parents++; if (num_parents % 100000 == 0) { - verbose_stream() << "[remove-cg] " << num_eqs << " " << num_parents << " " + verbose_stream() << "[remove-cg] " << num_eqs << " " << num_parents << " " << static_cast(num_eqs)/static_cast(num_parents) << "\n"; } } #endif - SASSERT(parent->is_marked() || !parent->is_cgc_enabled() || + SASSERT(parent->is_marked() || !parent->is_cgc_enabled() || (!parent->is_true_eq() && parent->is_cgr() == m_cg_table.contains_ptr(parent)) || (parent->is_true_eq() && !m_cg_table.contains_ptr(parent))); if (!parent->is_marked() && parent->is_cgr() && !parent->is_true_eq()) { @@ -667,12 +667,12 @@ namespace smt { cg_table at remove_parents_from_cg_table. Some of these parents will become congruent to other enodes, and a new equality will be propagated. Moreover, this method is also used for doing equality propagation. - + The parents of r1 that remain as congruence roots are copied to the r2->m_parents. The n1, n2, js arguments are used to implement dynamic ackermanization. - js is a justification for n1 and n2 being equal, and the equality n1 = n2 is + js is a justification for n1 and n2 being equal, and the equality n1 = n2 is the one that implied r1 = r2. */ void context::reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js) { @@ -737,7 +737,7 @@ namespace smt { the following sequence starting at n and ending at n->get_root. - N1 = n + N1 = n N_{i+1} = N_i->m_trans.m_target and, there is an k such that N_k = n->get_root() @@ -768,12 +768,12 @@ namespace smt { This method is used to improve the quality of the conflict clauses produced by the logical context. - + Consider the following example: - Consider the following sequence of equalities: n1 = n2 = n3 = n4 = n5 = n6 - + - Now, assume that n1 is the root of the equivalence class after each merge. So, the 'proof' branch will have the following shape: @@ -782,12 +782,12 @@ namespace smt { - Assuming that all nodes are attached to theory variable, then the following sequence of equalities is sent to the theory if the method get_closest_var is not used: - + n1 = n2, n1 = n3, n1 = n4, n1 = n5, n1 = n6 - This sequence is bad, and bad justifications may be produced by theory. For example, assume the following arithmetic constraint - + n5 < n6 For the arithmetic module, the best justification will be: @@ -798,7 +798,7 @@ namespace smt { When the method get_closest_var is used in the communication with theories, the logical context will send the natural sequence of equalities to the theories: - + n1 = n2 = n3 = n4 = n5 = n6 */ theory_var context::get_closest_var(enode * n, theory_id th_id) { @@ -816,7 +816,7 @@ namespace smt { /** \brief Merge the theory variables of n2->get_root() and n1->get_root(), the result is stored in n2->get_root(). New th_var equalities are propagated to the theories. - + \remark In most cases, an enode is attached to at most one theory var. */ void context::merge_theory_vars(enode * n2, enode * n1, eq_justification js) { @@ -826,7 +826,7 @@ namespace smt { TRACE("merge_theory_vars", tout << "Neither have theory vars #" << n1->get_owner()->get_id() << " #" << n2->get_owner()->get_id() << "\n";); return; } - + theory_id from_th = null_theory_id; if (js.get_kind() == eq_justification::JUSTIFICATION) @@ -839,8 +839,8 @@ namespace smt { // verbose_stream() << "[merge_theory_vars] t2: " << t2 << ", t1: " << t1 << "\n"; theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t2) : r2->m_th_var_list.get_th_var(); theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : r1->m_th_var_list.get_th_var(); - TRACE("merge_theory_vars", - tout << "v2: " << v2 << " #" << r2->get_owner_id() << ", v1: " << v1 << " #" << r1->get_owner_id() + TRACE("merge_theory_vars", + tout << "v2: " << v2 << " #" << r2->get_owner_id() << ", v1: " << v1 << " #" << r1->get_owner_id() << ", t2: " << t2 << ", t1: " << t1 << "\n";); if (v2 != null_theory_var && v1 != null_theory_var) { if (t1 == t2) { @@ -867,7 +867,7 @@ namespace smt { } else { // r1 and/or r2 have more than one theory variable. - TRACE("merge_theory_vars", + TRACE("merge_theory_vars", tout << "#" << r1->get_owner_id() << " == #" << r2->get_owner_id() << "\n";); @@ -889,7 +889,7 @@ namespace smt { } l2 = l2->get_next(); } - + theory_var_list * l1 = r1->get_th_var_list(); while (l1) { theory_id t1 = l1->get_th_id(); @@ -905,7 +905,7 @@ namespace smt { } } } - + /** \brief Propabate the boolean assignment when two equivalence classes are merged. */ @@ -959,7 +959,7 @@ namespace smt { bool_var v2 = enode2bool_var(target); lbool val2 = get_assignment(v2); if (val2 != val) { - if (val2 != l_undef && congruent(source, target) && source->get_num_args() > 0) + if (val2 != l_undef && congruent(source, target) && source->get_num_args() > 0) m_dyn_ack_manager.cg_conflict_eh(source->get_owner(), target->get_owner()); assign(literal(v2, sign), mk_justification(mp_iff_justification(source, target))); } @@ -986,7 +986,7 @@ namespace smt { enode * parent = *it; if (parent->is_cgc_enabled()) { TRACE("add_eq_parents", tout << "removing: #" << parent->get_owner_id() << "\n";); - CTRACE("add_eq", !parent->is_cgr(), + CTRACE("add_eq", !parent->is_cgr(), tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" << parent->get_owner_id() << ", parents: \n"; for (unsigned i = 0; i < r2->m_parents.size(); i++) { @@ -1017,10 +1017,10 @@ namespace smt { TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";); if (parent->is_cgc_enabled()) { enode * cg = parent->m_cg; - if (!parent->is_true_eq() && + if (!parent->is_true_eq() && (parent == cg || // parent was root of the congruence class before and after the merge !congruent(parent, cg) // parent was root of the congruence class before but not after the merge - )) { + )) { TRACE("add_eq_parents", tout << "trying to reinsert\n";); m_cg_table.insert(parent); parent->m_cg = parent; @@ -1057,17 +1057,17 @@ namespace smt { // n2 -> ... -> r2 SASSERT(n1->trans_reaches(r1)); SASSERT(r1->m_trans.m_target == 0); - + CASSERT("add_eq", check_invariant()); } /** - \brief Auxiliary method for undo_add_eq. + \brief Auxiliary method for undo_add_eq. It restores the theory variables of a given root enode. This method deletes any theory variable v2 of r2 (for a theory t2) whenever: - get_theory(t2)->get_enode(v2)->get_root() != r2 + get_theory(t2)->get_enode(v2)->get_root() != r2 That is, v2 is not equivalent to r2 anymore. */ @@ -1078,7 +1078,7 @@ namespace smt { while (l2) { theory_var v2 = l2->get_th_var(); theory_id t2 = l2->get_th_id(); - + if (get_theory(t2)->get_enode(v2)->get_root() != r2) { SASSERT(get_theory(t2)->get_enode(v2)->get_root() == r1); l2 = l2->get_next(); @@ -1122,7 +1122,7 @@ namespace smt { #ifdef Z3DEBUG push_trail(push_back_trail(m_diseq_vector)); m_diseq_vector.push_back(enode_pair(n1, n2)); -#endif +#endif if (r1 == r2) { TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";); @@ -1166,7 +1166,7 @@ namespace smt { } return true; } - + /** \brief Return true if n1 and n2 are known to be disequal in the logical context. @@ -1215,7 +1215,7 @@ namespace smt { if (parent->is_eq() && is_relevant(parent->get_owner()) && get_assignment(enode2bool_var(parent)) == l_false && ((parent->get_arg(0)->get_root() == n1->get_root() && parent->get_arg(1)->get_root() == n2->get_root()) || (parent->get_arg(1)->get_root() == n1->get_root() && parent->get_arg(0)->get_root() == n2->get_root()))) { - TRACE("is_diseq_bug", tout << "parent: #" << parent->get_owner_id() << ", parent->root: #" << + TRACE("is_diseq_bug", tout << "parent: #" << parent->get_owner_id() << ", parent->root: #" << parent->get_root()->get_owner_id() << " assignment(parent): " << get_assignment(enode2bool_var(parent)) << " args: #" << parent->get_arg(0)->get_owner_id() << " #" << parent->get_arg(1)->get_owner_id() << "\n";); return true; @@ -1274,7 +1274,7 @@ namespace smt { enode * arg2 = p2->get_arg(j)->get_root(); if (arg1 == arg2) continue; - if ((arg1 == r1 || arg1 == r2) && + if ((arg1 == r1 || arg1 == r2) && (arg2 == r1 || arg2 == r2)) continue; break; @@ -1353,8 +1353,8 @@ namespace smt { expr * arg = r->get_owner()->get_arg(i); SASSERT(e_internalized(arg)); enode * _arg = get_enode(arg); - CTRACE("eq_to_bug", args[i]->get_root() != _arg->get_root(), - tout << "#" << args[i]->get_owner_id() << " #" << args[i]->get_root()->get_owner_id() + CTRACE("eq_to_bug", args[i]->get_root() != _arg->get_root(), + tout << "#" << args[i]->get_owner_id() << " #" << args[i]->get_root()->get_owner_id() << " #" << _arg->get_owner_id() << " #" << _arg->get_root()->get_owner_id() << "\n"; tout << "#" << r->get_owner_id() << "\n"; display(tout);); @@ -1367,8 +1367,8 @@ namespace smt { } /** - \brief Process the equality propagation queue. - + \brief Process the equality propagation queue. + \remark The method assign_eq adds a new entry on this queue. */ bool context::propagate_eqs() { @@ -1385,7 +1385,7 @@ namespace smt { std::cout << counter1 << " " << counter2 << "\n"; #endif add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification); - if (inconsistent()) + if (inconsistent()) return false; } m_eq_propagation_queue.reset(); @@ -1403,7 +1403,7 @@ namespace smt { bool_var v = l.var(); bool_var_data & d = get_bdata(v); lbool val = get_assignment(v); - TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() + TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() << " tag: " << (d.is_eq()?"eq":"") << (d.is_theory_atom()?"th":"") << (d.is_quantifier()?"q":"") << " " << l << "\n";); SASSERT(val != l_undef); if (d.is_enode()) @@ -1435,7 +1435,7 @@ namespace smt { // Remark: when RELEVANCY_LEMMA is true, a quantifier can be asserted to false and marked as relevant. // This happens when a quantifier is part of a lemma (conflict-clause), and this conflict clause // becomes an unit-clause and the remaining literal is the negation of a quantifier. - CTRACE("assign_quantifier_bug", get_assignment(v) != l_true, + CTRACE("assign_quantifier_bug", get_assignment(v) != l_true, tout << "#" << bool_var2expr(v)->get_id() << " val: " << get_assignment(v) << "\n"; tout << mk_pp(bool_var2expr(v), m_manager) << "\n"; display(tout);); @@ -1562,7 +1562,7 @@ namespace smt { /** \brief Return the truth assignment for an expression that is attached to a boolean variable. - + \pre The expression must be attached to a boolean variable. */ inline lbool context::get_assignment_core(expr * n) const { @@ -1582,7 +1582,7 @@ namespace smt { lbool context::get_assignment(expr * n) const { if (m_manager.is_false(n)) return l_false; - if (m_manager.is_not(n)) + if (m_manager.is_not(n)) return ~get_assignment_core(to_app(n)->get_arg(0)); return get_assignment_core(n); } @@ -1621,14 +1621,14 @@ namespace smt { */ void context::get_assignments(expr_ref_vector& assignments) { literal_vector::const_iterator it = m_assigned_literals.begin(); - literal_vector::const_iterator end = m_assigned_literals.end(); + literal_vector::const_iterator end = m_assigned_literals.end(); for (; it != end; ++it) { expr_ref e(m_manager); literal2expr(*it, e); assignments.push_back(e); } } - + void context::relevant_eh(expr * n) { if (b_internalized(n)) { bool_var v = get_bool_var(n); @@ -1646,7 +1646,7 @@ namespace smt { #ifndef SMTCOMP m_case_split_queue->relevant_eh(n); #endif - + if (is_app(n)) { if (e_internalized(n)) { SASSERT(relevancy()); @@ -1663,15 +1663,15 @@ namespace smt { propagated_th = th; // <<< mark that relevancy_eh was already invoked for theory th. } } - + if (e_internalized(n)) { - enode * e = get_enode(n); + enode * e = get_enode(n); theory_var_list * l = e->get_th_var_list(); while (l) { theory_id th_id = l->get_th_id(); theory * th = get_theory(th_id); // I don't want to invoke relevant_eh twice for the same n. - if (th != propagated_th) + if (th != propagated_th) th->relevant_eh(to_app(n)); l = l->get_next(); } @@ -1749,7 +1749,7 @@ namespace smt { } bool context::can_propagate() const { - return + return m_qhead != m_assigned_literals.size() || m_relevancy_propagator->can_propagate() || !m_atom_propagation_queue.empty() || @@ -1776,7 +1776,7 @@ namespace smt { } SASSERT(!inconsistent()); propagate_relevancy(qhead); - if (inconsistent()) + if (inconsistent()) return false; if (!propagate_atoms()) return false; @@ -1784,7 +1784,7 @@ namespace smt { return false; propagate_th_eqs(); propagate_th_diseqs(); - if (inconsistent()) + if (inconsistent()) return false; if (!propagate_theories()) return false; @@ -1820,11 +1820,11 @@ namespace smt { return m_fingerprints.contains(q, q->get_id(), num_bindings, bindings); } - bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, + bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, ptr_vector & used_enodes) { return m_qmanager->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes); } - + void context::rescale_bool_var_activity() { TRACE("case_split", tout << "rescale\n";); svector::iterator it = m_activity.begin(); @@ -1851,15 +1851,15 @@ namespace smt { static unsigned counter = 0; counter++; if (counter % 100 == 0) { - TRACE("activity_profile", + TRACE("activity_profile", for (unsigned i=0; i m_lit_occs[(~l).index()].size(); + is_pos = m_lit_occs[l.index()].size() > m_lit_occs[(~l).index()].size(); break; } default: @@ -1972,7 +1972,7 @@ namespace smt { m_fingerprints.push_scope(); m_case_split_queue->push_scope(); m_asserted_formulas.push_scope(); - + ptr_vector::iterator it = m_theory_set.begin(); ptr_vector::iterator end = m_theory_set.end(); for (; it != end; ++it) @@ -1989,7 +1989,7 @@ namespace smt { /** \brief Remove watch literal idx from the given clause. - + \pre idx must be 0 or 1. */ void context::remove_watch_literal(clause * cls, unsigned idx) { @@ -2015,13 +2015,13 @@ namespace smt { } /** - \brief Delete the given clause. - + \brief Delete the given clause. + \pre Clause is not in the reinit stack. */ void context::del_clause(clause * cls) { SASSERT(m_flushing || !cls->in_reinit_stack()); - if (!cls->deleted()) + if (!cls->deleted()) remove_cls_occs(cls); cls->deallocate(m_manager); m_stats.m_num_del_clause++; @@ -2067,7 +2067,7 @@ namespace smt { d.set_null_justification(); m_case_split_queue->unassign_var_eh(v); } - + m_assigned_literals.shrink(old_lim); m_qhead = old_lim; SASSERT(m_qhead == m_assigned_literals.size()); @@ -2137,8 +2137,8 @@ namespace smt { /** \brief When a clause is reinitialized (see reinit_clauses) enodes and literals may need to be recreated. When an enode is recreated, I want to use the same generation - number it had before being deleted. Otherwise the generation will be 0, and will affect - the loop prevetion heuristics used to control quantifier instantiation. + number it had before being deleted. Otherwise the generation will be 0, and will affect + the loop prevetion heuristics used to control quantifier instantiation. Thus, I cache the generation number of enodes that will be deleted during backtracking and recreated by reinit_clauses. */ @@ -2184,11 +2184,11 @@ namespace smt { for(unsigned i = 0; i < num_lits; i++) { bool_var v = lits[i].var(); unsigned ilvl = get_intern_level(v); - if (ilvl > new_scope_lvl) + if (ilvl > new_scope_lvl) cache_generation(bool_var2expr(v), new_scope_lvl); } } - + /** \brief See cache_generation(unsigned new_scope_lvl) */ @@ -2223,7 +2223,7 @@ namespace smt { } } } - + /** \brief See cache_generation(unsigned new_scope_lvl) */ @@ -2235,7 +2235,7 @@ namespace smt { /** \brief Reinitialize learned clauses (lemmas) that contain boolean variables that were deleted during backtracking. - + \remark num_bool_vars contains the number of boolean variables alive after backtracking. So, a clause contains a dead variable if it contains a literal l where l.var() >= num_bool_vars. @@ -2290,20 +2290,20 @@ namespace smt { } } } - + unsigned ilvl = 0; (void)ilvl; for (unsigned j = 0; j < num; j++) { expr * atom = cls->get_atom(j); bool sign = cls->get_atom_sign(j); - // Atom can be (NOT foo). This can happen, for example, when + // Atom can be (NOT foo). This can happen, for example, when // the NOT-application is a child of an uninterpreted function symbol. // So, when reinternalizing the NOT-atom I should set the gate_ctx to false, // and force expression to be reinternalized. // Otherwise I set gate_ctx to true bool gate_ctx = !m_manager.is_not(atom); internalize(atom, gate_ctx); - SASSERT(b_internalized(atom)); + SASSERT(b_internalized(atom)); bool_var v = get_bool_var(atom); DEBUG_CODE({ if (get_intern_level(v) > ilvl) @@ -2322,7 +2322,7 @@ namespace smt { if (lit_occs_enabled()) add_lit_occs(cls); - + literal l1 = cls->get_literal(0); literal l2 = cls->get_literal(1); @@ -2330,9 +2330,9 @@ namespace smt { set_conflict(b_justification(cls)); else if (get_assignment(l2) == l_false) assign(l1, b_justification(cls)); - + TRACE("reinit_clauses", tout << "reinit clause:\n"; display_clause_detail(tout, cls); tout << "\n"; - tout << "activity: " << cls->get_activity() << ", num_bool_vars: " << num_bool_vars << ", scope_lvl: " + tout << "activity: " << cls->get_activity() << ", num_bool_vars: " << num_bool_vars << ", scope_lvl: " << m_scope_lvl << "\n";); keep = true; } @@ -2349,8 +2349,8 @@ namespace smt { keep = true; } } - - // SASSERT(!(cls->get_num_literals() == 3 && + + // SASSERT(!(cls->get_num_literals() == 3 && // (cls->get_literal(0).index() == 624 || cls->get_literal(0).index() == 103 || cls->get_literal(0).index() == 629) && // (cls->get_literal(1).index() == 624 || cls->get_literal(1).index() == 103 || cls->get_literal(1).index() == 629) && // (cls->get_literal(2).index() == 624 || cls->get_literal(2).index() == 103 || cls->get_literal(2).index() == 629))); @@ -2398,7 +2398,7 @@ namespace smt { of boolean variables before reinitializing clauses. This value is useful because it can be used to detect which boolean variables were deleted. - + \warning This method will not invoke reset_cache_generation. */ unsigned context::pop_scope_core(unsigned num_scopes) { @@ -2406,25 +2406,25 @@ namespace smt { try { if (m_manager.has_trace_stream()) m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n"; - + TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";); TRACE("pop_scope_detail", display(tout);); SASSERT(num_scopes > 0); SASSERT(num_scopes <= m_scope_lvl); SASSERT(m_scopes.size() == m_scope_lvl); - + unsigned new_lvl = m_scope_lvl - num_scopes; - + cache_generation(new_lvl); m_qmanager->pop(num_scopes); m_case_split_queue->pop_scope(num_scopes); - + TRACE("pop_scope", tout << "backtracking: " << num_scopes << ", new_lvl: " << new_lvl << "\n";); scope & s = m_scopes[new_lvl]; TRACE("context", tout << "backtracking new_lvl: " << new_lvl << "\n";); - + unsigned units_to_reassert_lim = s.m_units_to_reassert_lim; - + if (new_lvl < m_base_lvl) { base_scope & bs = m_base_scopes[new_lvl]; del_clauses(m_lemmas, bs.m_lemmas_lim); @@ -2441,35 +2441,35 @@ namespace smt { m_not_l = null_literal; } del_clauses(m_aux_clauses, s.m_aux_clauses_lim); - + m_relevancy_propagator->pop(num_scopes); - + m_fingerprints.pop_scope(num_scopes); unassign_vars(s.m_assigned_literals_lim); undo_trail_stack(s.m_trail_stack_lim); - + for (theory* th : m_theory_set) { th->pop_scope_eh(num_scopes); } - + del_justifications(m_justifications, s.m_justifications_lim); - + m_asserted_formulas.pop_scope(num_scopes); - + m_eq_propagation_queue.reset(); m_th_eq_propagation_queue.reset(); m_th_diseq_propagation_queue.reset(); m_atom_propagation_queue.reset(); - + m_region.pop_scope(num_scopes); m_scopes.shrink(new_lvl); - + m_scope_lvl = new_lvl; if (new_lvl < m_base_lvl) { m_base_lvl = new_lvl; m_search_lvl = new_lvl; // Remark: not really necessary } - + unsigned num_bool_vars = get_num_bool_vars(); // any variable >= num_bool_vars was deleted during backtracking. reinit_clauses(num_scopes, num_bool_vars); @@ -2516,32 +2516,32 @@ namespace smt { bool context::simplify_clause(clause * cls) { SASSERT(m_scope_lvl == m_base_lvl); unsigned s = cls->get_num_literals(); - if (get_assignment(cls->get_literal(0)) == l_true || + if (get_assignment(cls->get_literal(0)) == l_true || get_assignment(cls->get_literal(1)) == l_true) { // clause is already satisfied. - return true; + return true; } - + literal_buffer simp_lits; unsigned i = 2; - unsigned j = i; - for(; i < s; i++) { + unsigned j = i; + for(; i < s; i++) { literal l = cls->get_literal(i); switch(get_assignment(l)) { - case l_false: - if (m_manager.proofs_enabled()) + case l_false: + if (m_manager.proofs_enabled()) simp_lits.push_back(~l); - if (lit_occs_enabled()) + if (lit_occs_enabled()) m_lit_occs[l.index()].erase(cls); break; - case l_undef: + case l_undef: cls->set_literal(j, l); j++; break; - case l_true: + case l_true: return true; - } + } } if (j < s) { @@ -2554,15 +2554,15 @@ namespace smt { justification * js = cls->get_justification(); justification * new_js = 0; if (js->in_region()) - new_js = mk_justification(unit_resolution_justification(m_region, - js, + new_js = mk_justification(unit_resolution_justification(m_region, + js, simp_lits.size(), simp_lits.c_ptr())); else new_js = alloc(unit_resolution_justification, js, simp_lits.size(), simp_lits.c_ptr()); cls->set_justification(new_js); } - return false; + return false; } /** @@ -2598,7 +2598,7 @@ namespace smt { SASSERT(m_search_lvl == m_base_lvl); literal_buffer simp_lits; unsigned num_lits = cls->get_num_literals(); - for(unsigned i = 0; i < num_lits; i++) { + for(unsigned i = 0; i < num_lits; i++) { if (i != idx) { literal l = cls->get_literal(i); SASSERT(l != l0); @@ -2610,13 +2610,13 @@ namespace smt { if (!cls_js || cls_js->in_region()) { // If cls_js is 0 or is allocated in a region, then // we can allocate the new justification in a region too. - js = mk_justification(unit_resolution_justification(m_region, + js = mk_justification(unit_resolution_justification(m_region, cls_js, simp_lits.size(), - simp_lits.c_ptr())); + simp_lits.c_ptr())); } else { - js = alloc(unit_resolution_justification, cls_js, simp_lits.size(), simp_lits.c_ptr()); + js = alloc(unit_resolution_justification, cls_js, simp_lits.size(), simp_lits.c_ptr()); // js took ownership of the justification object. cls->set_justification(0); m_justifications.push_back(js); @@ -2648,7 +2648,7 @@ namespace smt { // Remark: when assumptions are used m_scope_lvl >= m_search_lvl > m_base_lvl. Therefore, no simplification is performed. if (m_scope_lvl > m_base_lvl) return; - + unsigned sz = m_assigned_literals.size(); SASSERT(m_simp_qhead <= sz); @@ -2678,7 +2678,7 @@ namespace smt { // a variable during propagation. // m_simp_counter = 0; - // the field m_simp_qhead is used to check whether there are + // the field m_simp_qhead is used to check whether there are // new assigned literals at the base level. m_simp_qhead = m_assigned_literals.size(); @@ -2709,13 +2709,15 @@ namespace smt { \brief Delete low activity lemmas */ inline void context::del_inactive_lemmas() { - if (m_fparams.m_lemma_gc_half) + if (m_fparams.m_lemma_gc_strategy == LGC_NONE) + return; + else if (m_fparams.m_lemma_gc_half) del_inactive_lemmas1(); else del_inactive_lemmas2(); m_num_conflicts_since_lemma_gc = 0; - if (m_fparams.m_lemma_gc_strategy == LGC_GEOMETRIC) + if (m_fparams.m_lemma_gc_strategy == LGC_GEOMETRIC) m_lemma_gc_threshold = static_cast(m_lemma_gc_threshold * m_fparams.m_lemma_gc_factor); } @@ -2737,12 +2739,12 @@ namespace smt { unsigned i = start_del_at; unsigned j = i; unsigned num_del_cls = 0; - TRACE("del_inactive_lemmas", tout << "sz: " << sz << ", start_at: " << start_at << ", end_at: " << end_at + TRACE("del_inactive_lemmas", tout << "sz: " << sz << ", start_at: " << start_at << ", end_at: " << end_at << ", start_del_at: " << start_del_at << "\n";); for (; i < end_at; i++) { clause * cls = m_lemmas[i]; if (can_delete(cls)) { - TRACE("del_inactive_lemmas", tout << "deleting: "; display_clause(tout, cls); tout << ", activity: " << + TRACE("del_inactive_lemmas", tout << "deleting: "; display_clause(tout, cls); tout << ", activity: " << cls->get_activity() << "\n";); del_clause(cls); num_del_cls++; @@ -2763,7 +2765,7 @@ namespace smt { m_lemmas[j] = cls; j++; } - } + } m_lemmas.shrink(j); if (m_fparams.m_clause_decay > 1) { // rescale activity @@ -2805,7 +2807,7 @@ namespace smt { } // A clause is deleted if it has low activity and the number of unknowns is greater than a threshold. // The activity threshold depends on how old the clause is. - unsigned act_threshold = m_fparams.m_old_clause_activity - + unsigned act_threshold = m_fparams.m_old_clause_activity - (m_fparams.m_old_clause_activity - m_fparams.m_new_clause_activity) * ((i - start_at) / real_sz); if (cls->get_activity() < act_threshold) { unsigned rel_threshold = (i >= new_first_idx ? m_fparams.m_new_clause_relevancy : m_fparams.m_old_clause_relevancy); @@ -2843,10 +2845,10 @@ namespace smt { return false; } - void context::register_plugin(simplifier_plugin * s) { + void context::register_plugin(simplifier_plugin * s) { SASSERT(!already_internalized()); SASSERT(m_scope_lvl == 0); - m_asserted_formulas.register_simplifier_plugin(s); + m_asserted_formulas.register_simplifier_plugin(s); } #ifdef Z3DEBUG @@ -2873,7 +2875,7 @@ namespace smt { } #endif - void context::register_plugin(theory * th) { + void context::register_plugin(theory * th) { if (m_theories.get_plugin(th->get_family_id()) != 0) { dealloc(th); return; // context already has a theory for the given family id. @@ -2881,7 +2883,7 @@ namespace smt { SASSERT(std::find(m_theory_set.begin(), m_theory_set.end(), th) == m_theory_set.end()); SASSERT(!already_internalized_theory(th)); th->init(this); - m_theories.register_plugin(th); + m_theories.register_plugin(th); m_theory_set.push_back(th); { #ifdef Z3DEBUG @@ -2933,18 +2935,18 @@ namespace smt { ptr_vector::iterator it = m_theory_set.begin(); ptr_vector::iterator end = m_theory_set.end(); for (; it != end; ++it) - (*it)->flush_eh(); + (*it)->flush_eh(); undo_trail_stack(0); m_qmanager = 0; del_clauses(m_aux_clauses, 0); del_clauses(m_lemmas, 0); del_justifications(m_justifications, 0); - if (m_is_diseq_tmp) { + if (m_is_diseq_tmp) { m_is_diseq_tmp->del_eh(m_manager, false); - m_manager.dec_ref(m_is_diseq_tmp->get_owner()); + m_manager.dec_ref(m_is_diseq_tmp->get_owner()); enode::del_dummy(m_is_diseq_tmp); - m_is_diseq_tmp = 0; - } + m_is_diseq_tmp = 0; + } std::for_each(m_almost_cg_tables.begin(), m_almost_cg_tables.end(), delete_proc()); } @@ -3042,7 +3044,7 @@ namespace smt { // not counting any literals that get assigned by this method // this relies on bcp() to give us its old m_qhead and therefore // bcp() should always be called before this method - + unsigned assigned_literal_end = m_assigned_literals.size(); for (; qhead < assigned_literal_end; ++qhead) { literal l = m_assigned_literals[qhead]; @@ -3129,7 +3131,7 @@ namespace smt { return true; if (m.is_not(assumption, arg) && is_uninterp_const(arg)) return true; - if (!is_app(assumption)) + if (!is_app(assumption)) return false; if (to_app(assumption)->get_num_args() == 0) return true; @@ -3146,7 +3148,7 @@ namespace smt { SASSERT(assumptions[i]); if (!is_valid_assumption(m_manager, assumptions[i])) { warning_msg("an assumption must be a propositional variable or the negation of one"); - return false; + return false; } } return true; @@ -3158,11 +3160,11 @@ namespace smt { m_unsat_core.reset(); if (num_assumptions > 0) { // We must give a chance to the theories to propagate before we create a new scope... - propagate(); + propagate(); // Internal backtracking scopes (created with push_scope()) must only be created when we are // in a consistent context. if (inconsistent()) - return; + return; if (get_cancel_flag()) return; push_scope(); @@ -3270,9 +3272,9 @@ namespace smt { /** \brief Setup the logical context based on the current set of asserted formulas and execute the check command. - + \remark A logical context can only be configured at scope level 0, - and before internalizing any formulas. + and before internalizing any formulas. */ lbool context::setup_and_check(bool reset_cancel) { if (!check_preamble(reset_cancel)) @@ -3371,7 +3373,7 @@ namespace smt { expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions); if (!already_did_theory_assumptions) { - add_theory_assumptions(all_assumptions); + add_theory_assumptions(all_assumptions); } unsigned num_assumptions = all_assumptions.size(); @@ -3484,7 +3486,7 @@ namespace smt { lbool context::search() { -#ifndef _EXTERNAL_RELEASE +#ifndef _EXTERNAL_RELEASE if (m_fparams.m_abort_after_preproc) { exit(1); } @@ -3507,16 +3509,16 @@ namespace smt { status = bounded_search(); TRACE("search_bug", tout << "status: " << status << ", inconsistent: " << inconsistent() << "\n";); - TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout); + TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout); tout << ", num_assigned: " << m_assigned_literals.size() << "\n";); - + if (!restart(status, curr_lvl)) { break; } } - + TRACE("search_lite", tout << "status: " << status << "\n";); - TRACE("guessed_literals", + TRACE("guessed_literals", expr_ref_vector guessed_lits(m_manager); get_guessed_literals(guessed_lits); unsigned sz = guessed_lits.size(); @@ -3547,7 +3549,7 @@ namespace smt { // possible outcomes DONE l_true, DONE l_undef, CONTINUE quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value()); if (cmr == quantifier_manager::SAT) { - // done + // done status = l_true; return false; } @@ -3562,7 +3564,7 @@ namespace smt { inc_limits(); if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) { SASSERT(!inconsistent()); - IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations + IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations << " :decisions " << m_stats.m_num_decisions << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold; if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) { @@ -3582,9 +3584,9 @@ namespace smt { ptr_vector::iterator end = m_theory_set.end(); for (; it != end && !inconsistent(); ++it) (*it)->restart_eh(); - TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); + TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); if (!inconsistent()) { - m_qmanager->restart_eh(); + m_qmanager->restart_eh(); } if (inconsistent()) { VERIFY(!resolve_conflict()); @@ -3600,7 +3602,7 @@ namespace smt { status = l_undef; return true; } - + void context::tick(unsigned & counter) const { counter++; if (counter > m_fparams.m_tick) { @@ -3617,7 +3619,7 @@ namespace smt { lbool context::bounded_search() { unsigned counter = 0; - + TRACE("bounded_search", tout << "starting bounded search...\n";); while (true) { @@ -3636,14 +3638,14 @@ namespace smt { return l_false; SASSERT(m_scope_lvl >= m_base_lvl); - + if (!inconsistent()) { if (resource_limits_exceeded()) return l_undef; if (get_cancel_flag()) return l_undef; - + if (m_num_conflicts_since_restart > m_restart_threshold && m_scope_lvl - m_base_lvl > 2) { TRACE("search_bug", tout << "bounded-search return undef, inconsistent: " << inconsistent() << "\n";); return l_undef; // restart @@ -3664,7 +3666,7 @@ namespace smt { m_dyn_ack_manager.propagate_eh(); CASSERT("dyn_ack", check_clauses(m_lemmas) && check_clauses(m_aux_clauses)); } - + if (resource_limits_exceeded() && !inconsistent()) { return l_undef; } @@ -3674,7 +3676,7 @@ namespace smt { if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses) simplify_clauses(); - + if (!decide()) { final_check_status fcs = final_check(); TRACE("final_check_result", tout << "fcs: " << fcs << " last_search_failure: " << m_last_search_failure << "\n";); @@ -3697,11 +3699,11 @@ namespace smt { bool context::resource_limits_exceeded() { if (m_searching) { - // Some of the flags only make sense to check when searching. + // Some of the flags only make sense to check when searching. // For example, the timer is only started in init_search(). if (m_last_search_failure != OK) return true; - + if (m_timer.ms_timeout(m_fparams.m_timeout)) { m_last_search_failure = TIMEOUT; return true; @@ -3715,12 +3717,12 @@ namespace smt { } } } - + if (get_cancel_flag()) { m_last_search_failure = CANCELED; return true; } - + if (memory::above_high_watermark()) { m_last_search_failure = MEMOUT; return true; @@ -3771,15 +3773,15 @@ namespace smt { ok = m_qmanager->final_check_eh(true); TRACE("final_check_step", tout << "quantifier ok: " << ok << " " << "inconsistent " << inconsistent() << "\n";); } - + m_final_check_idx = (m_final_check_idx + 1) % range; // IF_VERBOSE(1000, verbose_stream() << "final check status: " << ok << "\n";); - + switch (ok) { - case FC_DONE: + case FC_DONE: break; case FC_GIVEUP: - result = FC_GIVEUP; + result = FC_GIVEUP; break; case FC_CONTINUE: return FC_CONTINUE; @@ -3844,23 +3846,23 @@ namespace smt { unsigned new_lvl = m_conflict_resolution->get_new_scope_lvl(); unsigned num_lits = m_conflict_resolution->get_lemma_num_literals(); literal * lits = m_conflict_resolution->get_lemma_literals(); - + SASSERT(num_lits > 0); unsigned conflict_lvl = get_assign_level(lits[0]); SASSERT(conflict_lvl <= m_scope_lvl); - // When num_lits == 1, then the default behavior is to go + // When num_lits == 1, then the default behavior is to go // to base-level. If the problem has quantifiers, it may be // too expensive to do that, since all instances will need to // be recreated. If that is the case, I store the assertions in // a special vector and keep reasserting whenever I backtrack. // Moreover, I backtrack only one level. - bool delay_forced_restart = + bool delay_forced_restart = m_fparams.m_delay_units && - internalized_quantifiers() && - num_lits == 1 && - conflict_lvl > m_search_lvl + 1 && - !m_manager.proofs_enabled() && + internalized_quantifiers() && + num_lits == 1 && + conflict_lvl > m_search_lvl + 1 && + !m_manager.proofs_enabled() && m_units_to_reassert.size() < m_fparams.m_delay_units_threshold; if (delay_forced_restart) { new_lvl = conflict_lvl - 1; @@ -3868,20 +3870,20 @@ namespace smt { // Some of the literals/enodes of the conflict clause will be destroyed during // backtracking, and will need to be recreated. However, I want to keep - // the generation number for enodes that are going to be recreated. See + // the generation number for enodes that are going to be recreated. See // comment in cache_generation(unsigned). if (m_conflict_resolution->get_lemma_intern_lvl() > new_lvl) cache_generation(num_lits, lits, new_lvl); SASSERT(new_lvl < m_scope_lvl); - TRACE("resolve_conflict_bug", + TRACE("resolve_conflict_bug", tout << "m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " << m_conflict_resolution->get_lemma_intern_lvl() << "\n"; tout << "num_lits: " << num_lits << "\n"; for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; tout << l << " "; - display_literal(tout, l); - tout << ", ilvl: " << get_intern_level(l.var()) << "\n" + display_literal(tout, l); + tout << ", ilvl: " << get_intern_level(l.var()) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n"; }); @@ -3891,7 +3893,7 @@ namespace smt { m_manager.trace_stream() << "\n"; } -#ifdef Z3DEBUG +#ifdef Z3DEBUG expr_ref_vector expr_lits(m_manager); svector expr_signs; for (unsigned i = 0; i < num_lits; i++) { @@ -3906,7 +3908,7 @@ namespace smt { pr = m_conflict_resolution->get_lemma_proof(); // check_proof(pr); TRACE("context_proof", tout << mk_ll_pp(pr, m_manager);); - TRACE("context_proof_hack", + TRACE("context_proof_hack", static ast_mark visited; ast_ll_pp(tout, m_manager, pr, visited);); } @@ -3948,15 +3950,15 @@ namespace smt { if (relevancy()) restore_relevancy(num_lits, lits); // Resetting the cache manually because I did not invoke pop_scope, but pop_scope_core reset_cache_generation(); - TRACE("resolve_conflict_bug", - tout << "AFTER m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " << + TRACE("resolve_conflict_bug", + tout << "AFTER m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " << m_conflict_resolution->get_lemma_intern_lvl() << "\n"; tout << "num_lits: " << num_lits << "\n"; for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; tout << l << " "; - display_literal(tout, l); - tout << ", ilvl: " << get_intern_level(l.var()) << "\n" + display_literal(tout, l); + tout << ", ilvl: " << get_intern_level(l.var()) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n"; }); #ifdef Z3DEBUG @@ -3980,7 +3982,7 @@ namespace smt { } #if 0 { - static unsigned counter = 0; + static unsigned counter = 0; static uint64 total = 0; static unsigned max = 0; counter++; @@ -4006,13 +4008,13 @@ namespace smt { m_units_to_reassert_sign.push_back(unit_sign); TRACE("reassert_units", tout << "asserting #" << unit->get_id() << " " << unit_sign << " @ " << m_scope_lvl << "\n";); } - + m_conflict_resolution->release_lemma_atoms(); - TRACE("context_lemma", tout << "new lemma: "; + TRACE("context_lemma", tout << "new lemma: "; literal_vector v(num_lits, lits); std::sort(v.begin(), v.end()); for (unsigned i = 0; i < num_lits; i++) { - display_literal(tout, v[i]); + display_literal(tout, v[i]); tout << "\n"; v[i].display(tout, m_manager, m_bool_var2expr.c_ptr()); tout << "\n\n"; @@ -4028,7 +4030,7 @@ namespace smt { } return false; } - + /* \brief we record and restore relevancy information for literals in conflict clauses. A literal may have been marked relevant within the scope that gets popped during @@ -4064,11 +4066,11 @@ namespace smt { if (!checker.check(fml)) { warning_msg("Boogie generated formula that can require multiple '@' labels in a counter-example"); break; - } + } } } } - + SASSERT(!inconsistent()); unsigned sz = m_b_internalized_stack.size(); for (unsigned i = 0; i < sz; i++) { @@ -4079,7 +4081,7 @@ namespace smt { } } } - + /** \brief Collect relevant literals that may be used to block the current assignment. If at_lbls is true, then only labels that contains '@' are considered. (This is a hack for Boogie). @@ -4192,7 +4194,7 @@ namespace smt { } bool r = false; if (!b_internalized(eq)) { - // I do not invoke internalize(eq, true), because I want to + // I do not invoke internalize(eq, true), because I want to // mark the try_true_first flag before invoking theory::internalize_eq_eh. // Reason: Theories like arithmetic should be able to know if the try_true_first flag is // marked or not. They use this information to also mark auxiliary atoms such as: @@ -4254,13 +4256,13 @@ namespace smt { if (m_qmanager->is_shared(n)) { return true; } - - // the variabe is shared if the equivalence class of n + + // the variabe is shared if the equivalence class of n // contains a parent application. - + theory_var_list * l = n->get_th_var_list(); theory_id th_id = l->get_th_id(); - + enode_vector::const_iterator it = n->begin_parents(); enode_vector::const_iterator end = n->end_parents(); for (; it != end; ++it) { @@ -4271,12 +4273,12 @@ namespace smt { return true; } } - + // Some theories implement families of theories. Examples: // Arrays and Tuples. For example, array theory is a // parametric theory, that is, it implements several theories: // (array int int), (array int (array int int)), ... - // + // // Example: // // a : (array int int) @@ -4323,18 +4325,18 @@ namespace smt { if (fcs == FC_DONE) { mk_proto_model(l_true); m_model = m_proto_model->mk_model(); - add_rec_funs_to_model(); + add_rec_funs_to_model(); } - + return fcs == FC_DONE; } void context::mk_proto_model(lbool r) { - TRACE("get_model", - display(tout); + TRACE("get_model", + display(tout); display_normalized_enodes(tout); display_enodes_lbls(tout); - m_fingerprints.display(tout); + m_fingerprints.display(tout); ); failure fl = get_last_search_failure(); if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) { @@ -4351,7 +4353,7 @@ namespace smt { if (m_fparams.m_model_compact) m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); - } + } else { } @@ -4363,19 +4365,19 @@ namespace smt { return m_unsat_proof; } - void context::get_model(model_ref & m) const { + void context::get_model(model_ref & m) const { if (inconsistent()) m = 0; else - m = const_cast(m_model.get()); + m = const_cast(m_model.get()); } void context::get_proto_model(proto_model_ref & m) const { m = const_cast(m_proto_model.get()); } - failure context::get_last_search_failure() const { - return m_last_search_failure; + failure context::get_last_search_failure() const { + return m_last_search_failure; } void context::add_rec_funs_to_model() { @@ -4394,7 +4396,7 @@ namespace smt { func_decl* f = to_app(fn)->get_decl(); func_interp* fi = alloc(func_interp, m, f->get_arity()); fi->set_else(body); - m_model->register_decl(f, fi); + m_model->register_decl(f, fi); } } } From 6f8a9545325cb1b73fb07055755c54a8cc113e12 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 23 Aug 2017 12:37:26 +0100 Subject: [PATCH 10/12] added missing addition to smt_params_helper.pyg --- src/smt/params/smt_params_helper.pyg | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index a501f474a..5b5c7328c 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -80,5 +80,6 @@ def_module_params(module_name='smt', ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'), ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'), ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'), - ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body') + ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'), + ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none') )) From 58f152a92a0fa3ad6d5f0fcf64501b1108097c69 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 23 Aug 2017 19:21:32 +0100 Subject: [PATCH 11/12] [CMake] Teach CMake to support git worktrees. This fixes the bug reported by @nbraud reported in #1227. Previously the CMake build system assumed that the `.git` file must be a directory. This is not the case when the working directory is a "git worktree". In this case the `.git` file is just a plain file that points to a directory within the true `.git` directory. This commit essentially implements the logic to traverse this extra level of indirection and removes some assumptions that the `.git` file is a directory. --- cmake/git_utils.cmake | 82 ++++++++++++++++++++++++++++++------------- 1 file changed, 58 insertions(+), 24 deletions(-) diff --git a/cmake/git_utils.cmake b/cmake/git_utils.cmake index f98aca205..dbc95d8df 100644 --- a/cmake/git_utils.cmake +++ b/cmake/git_utils.cmake @@ -4,23 +4,55 @@ # of the git directory changes CMake will be forced to re-run. This useful # for fetching the current git hash and including it in the build. # -# `GIT_DIR` is the path to the git directory (i.e. the `.git` directory) +# `GIT_DOT_FILE` is the path to the git directory (i.e. the `.git` directory) or +# `.git` file used by a git worktree. # `SUCCESS_VAR` is the name of the variable to set. It will be set to TRUE # if the dependency was successfully added and FALSE otherwise. -function(add_git_dir_dependency GIT_DIR SUCCESS_VAR) +function(add_git_dir_dependency GIT_DOT_FILE SUCCESS_VAR) if (NOT "${ARGC}" EQUAL 2) message(FATAL_ERROR "Invalid number (${ARGC}) of arguments") endif() - if (NOT IS_ABSOLUTE "${GIT_DIR}") - message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not an absolute path") + if (NOT IS_ABSOLUTE "${GIT_DOT_FILE}") + message(FATAL_ERROR "GIT_DOT_FILE (\"${GIT_DOT_FILE}\") is not an absolute path") endif() - if (NOT IS_DIRECTORY "${GIT_DIR}") - message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not a directory") + if (NOT EXISTS "${GIT_DOT_FILE}") + message(FATAL_ERROR "GIT_DOT_FILE (\"${GIT_DOT_FILE}\") does not exist") endif() - set(GIT_HEAD_FILE "${GIT_DIR}/HEAD") + if (NOT IS_DIRECTORY "${GIT_DOT_FILE}") + # Might be a git worktree. In this case we need parse out the worktree + # git directory + file(READ "${GIT_DOT_FILE}" GIT_DOT_FILE_DATA LIMIT 512) + string(STRIP "${GIT_DOT_FILE_DATA}" GIT_DOT_FILE_DATA_STRIPPED) + if ("${GIT_DOT_FILE_DATA_STRIPPED}" MATCHES "^gitdir:[ ]*(.+)$") + # Git worktree + message(STATUS "Found git worktree") + set(GIT_WORKTREE_DIR "${CMAKE_MATCH_1}") + set(GIT_HEAD_FILE "${GIT_WORKTREE_DIR}/HEAD") + # Figure out where real git directory lives + set(GIT_COMMON_DIR_FILE "${GIT_WORKTREE_DIR}/commondir") + if (NOT EXISTS "${GIT_COMMON_DIR_FILE}") + message(FATAL_ERROR "Found git worktree dir but could not find \"${GIT_COMMON_DIR_FILE}\"") + endif() + file(READ "${GIT_COMMON_DIR_FILE}" GIT_COMMON_DIR_FILE_DATA LIMIT 512) + string(STRIP "${GIT_COMMON_DIR_FILE_DATA}" GIT_COMMON_DIR_FILE_DATA_STRIPPED) + get_filename_component(GIT_DIR "${GIT_WORKTREE_DIR}/${GIT_COMMON_DIR_FILE_DATA_STRIPPED}" ABSOLUTE) + if (NOT IS_DIRECTORY "${GIT_DIR}") + message(FATAL_ERROR "Failed to compute path to git directory from git worktree") + endif() + else() + message(FATAL_ERROR "GIT_DOT_FILE (\"${GIT_DOT_FILE}\") is not a directory or a pointer to git worktree directory") + endif() + else() + # Just a normal `.git` directory + message(STATUS "Found simple git working directory") + set(GIT_HEAD_FILE "${GIT_DOT_FILE}/HEAD") + set(GIT_DIR "${GIT_DOT_FILE}") + endif() + message(STATUS "Found git directory \"${GIT_DIR}\"") + if (NOT EXISTS "${GIT_HEAD_FILE}") message(AUTHOR_WARNING "Git head file \"${GIT_HEAD_FILE}\" cannot be found") set(${SUCCESS_VAR} FALSE PARENT_SCOPE) @@ -79,24 +111,25 @@ function(add_git_dir_dependency GIT_DIR SUCCESS_VAR) set(${SUCCESS_VAR} TRUE PARENT_SCOPE) endfunction() -# get_git_head_hash(GIT_DIR OUTPUT_VAR) +# get_git_head_hash(GIT_DOT_FILE OUTPUT_VAR) # -# Retrieve the current commit hash for a git working directory where `GIT_DIR` -# is the `.git` directory in the root of the git working directory. +# Retrieve the current commit hash for a git working directory where +# `GIT_DOT_FILE` is the `.git` directory or `.git` pointer file in a git +# worktree in the root of the git working directory. # # `OUTPUT_VAR` should be the name of the variable to put the result in. If this # function fails then either a fatal error will be raised or `OUTPUT_VAR` will # contain a string with the suffix `NOTFOUND` which can be used in CMake `if()` # commands. -function(get_git_head_hash GIT_DIR OUTPUT_VAR) +function(get_git_head_hash GIT_DOT_FILE OUTPUT_VAR) if (NOT "${ARGC}" EQUAL 2) message(FATAL_ERROR "Invalid number of arguments") endif() - if (NOT IS_DIRECTORY "${GIT_DIR}") - message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory") + if (NOT EXISTS "${GIT_DOT_FILE}") + message(FATAL_ERROR "\"${GIT_DOT_FILE}\" does not exist") endif() - if (NOT IS_ABSOLUTE "${GIT_DIR}") - message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path") + if (NOT IS_ABSOLUTE "${GIT_DOT_FILE}") + message(FATAL_ERROR \""${GIT_DOT_FILE}\" is not an absolute path") endif() find_package(Git) # NOTE: Use `GIT_FOUND` rather than `Git_FOUND` which was only @@ -105,7 +138,7 @@ function(get_git_head_hash GIT_DIR OUTPUT_VAR) set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE) return() endif() - get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY) + get_filename_component(GIT_WORKING_DIR "${GIT_DOT_FILE}" DIRECTORY) execute_process( COMMAND "${GIT_EXECUTABLE}" @@ -128,24 +161,25 @@ function(get_git_head_hash GIT_DIR OUTPUT_VAR) set(${OUTPUT_VAR} "${Z3_GIT_HASH}" PARENT_SCOPE) endfunction() -# get_git_head_describe(GIT_DIR OUTPUT_VAR) +# get_git_head_describe(GIT_DOT_FILE OUTPUT_VAR) # # Retrieve the output of `git describe` for a git working directory where -# `GIT_DIR` is the `.git` directory in the root of the git working directory. +# `GIT_DOT_FILE` is the `.git` directory or `.git` pointer file in a git +# worktree in the root of the git working directory. # # `OUTPUT_VAR` should be the name of the variable to put the result in. If this # function fails then either a fatal error will be raised or `OUTPUT_VAR` will # contain a string with the suffix `NOTFOUND` which can be used in CMake `if()` # commands. -function(get_git_head_describe GIT_DIR OUTPUT_VAR) +function(get_git_head_describe GIT_DOT_FILE OUTPUT_VAR) if (NOT "${ARGC}" EQUAL 2) message(FATAL_ERROR "Invalid number of arguments") endif() - if (NOT IS_DIRECTORY "${GIT_DIR}") - message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory") + if (NOT EXISTS "${GIT_DOT_FILE}") + message(FATAL_ERROR "\"${GIT_DOT_FILE}\" does not exist") endif() - if (NOT IS_ABSOLUTE "${GIT_DIR}") - message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path") + if (NOT IS_ABSOLUTE "${GIT_DOT_FILE}") + message(FATAL_ERROR \""${GIT_DOT_FILE}\" is not an absolute path") endif() find_package(Git) # NOTE: Use `GIT_FOUND` rather than `Git_FOUND` which was only @@ -154,7 +188,7 @@ function(get_git_head_describe GIT_DIR OUTPUT_VAR) set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE) return() endif() - get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY) + get_filename_component(GIT_WORKING_DIR "${GIT_DOT_FILE}" DIRECTORY) execute_process( COMMAND "${GIT_EXECUTABLE}" From 40f2afb5afc8a59526678337afa2d02f8a2b6e0a Mon Sep 17 00:00:00 2001 From: Dewald de Jager Date: Wed, 23 Aug 2017 23:09:47 +0200 Subject: [PATCH 12/12] [Doxygen] Fix function name in docstring Amending the changes made in https://github.com/Z3Prover/z3/commit/fe702d7782db990cb90ff2bea390b100fdd65872 --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 8d53c9255..43c175ca8 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1530,7 +1530,7 @@ extern "C" { In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects are determined by the scope level of #Z3_solver_push and #Z3_solver_pop. In other words, a Z3_ast object remains valid until there is a - call to Z3_pop that takes the current scope below the level where + call to Z3_solver_pop that takes the current scope below the level where the object was created. Note that all other reference counted objects, including Z3_model,