From efd5727676e8475c053a42661758a6b96d268a10 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Jun 2017 10:35:09 -0700 Subject: [PATCH 01/34] add shorthand for enumerating constants in a model Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Model.cs | 19 +++++++++++++++++++ src/sat/sat_solver/inc_sat_solver.cpp | 1 - 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index a7f62e6e8..12992fa8a 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -19,6 +19,7 @@ Notes: using System; using System.Diagnostics.Contracts; +using System.Collections.Generic; namespace Microsoft.Z3 { @@ -131,6 +132,24 @@ namespace Microsoft.Z3 } } + /// + /// Enumerate constants in model. + /// + public IEnumerable> Consts + { + get + { + uint nc = NumConsts; + for (uint i = 0; i < nc; ++i) + { + var f = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i)); + IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); + if (n == IntPtr.Zero) continue; + yield return new KeyValuePair(f, Expr.Create(Context, n)); + } + } + } + /// /// The number of function interpretations in the model. /// diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 4a4e0af38..b9ed925b0 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -326,7 +326,6 @@ public: return l_true; } - virtual std::string reason_unknown() const { return m_unknown; } From 668bad61216cd1b4b01a003cda7f7665d165f92f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Jun 2017 11:04:54 -0700 Subject: [PATCH 02/34] print success after reset assertions #1057 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 26cd0628e..a098f3c94 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -250,7 +250,7 @@ ATOMIC_CMD(get_assertions_cmd, "get-assertions", "retrieve asserted terms when i -ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions();); +ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions(); ctx.print_success();); UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", CPK_SYMBOL, symbol const &, if (ctx.set_logic(arg)) From 4f04301305d1ce26476ce832ea6a51cb1f8730a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Jun 2017 07:55:32 -0700 Subject: [PATCH 03/34] add documentation per #1058 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 45065f856..dec8f34dd 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5349,6 +5349,9 @@ extern "C" { /** \brief Add a new formula \c a to the given goal. + Conjunctions are split into separate formulas. + If the formula \c a is \c true, then nothing is added. + If the formula \c a is \c false, then the entire goal is replaced by the formula \c false. def_API('Z3_goal_assert', VOID, (_in(CONTEXT), _in(GOAL), _in(AST))) */ From af285d02c3ccf7c3c7f3f75e18ae56ae1857d5db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Jun 2017 08:38:28 -0700 Subject: [PATCH 04/34] add documentation per #1058 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index dec8f34dd..93da0b2c7 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5350,6 +5350,7 @@ extern "C" { /** \brief Add a new formula \c a to the given goal. Conjunctions are split into separate formulas. + If the goal is \c false, adding new formulas is a no-op. If the formula \c a is \c true, then nothing is added. If the formula \c a is \c false, then the entire goal is replaced by the formula \c false. From 83e9c40265ef66c771f673aca66f7eef1634102c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 6 Jun 2017 16:04:38 +0100 Subject: [PATCH 05/34] Added __deepcopy__ operators to ref-counted objects in the Python API --- src/api/python/z3/z3.py | 64 +++++++++++++++++++++++++++++++++++++++-- 1 file changed, 62 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b4cdf834b..b86e9a797 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -50,6 +50,7 @@ from fractions import Fraction import sys import io import math +import copy if sys.version < '3': def _is_int(v): @@ -288,6 +289,9 @@ class AstRef(Z3PPObject): if self.ctx.ref() is not None: Z3_dec_ref(self.ctx.ref(), self.as_ast()) + def __deepcopy__(self, memo={}): + return _to_ast_ref(self.ast, self.ctx) + def __str__(self): return obj_to_string(self) @@ -4355,6 +4359,11 @@ class Datatype: self.name = name self.constructors = [] + def __deepcopy__(self, memo={}): + r = Datatype(self.name, self.ctx) + r.constructors = copy.deepcopy(self.constructors) + return r + def declare_core(self, name, rec_name, *args): if __debug__: _z3_assert(isinstance(name, str), "String expected") @@ -4645,11 +4654,17 @@ class ParamsRef: Consider using the function `args2params` to create instances of this object. """ - def __init__(self, ctx=None): + def __init__(self, ctx=None, params=None): self.ctx = _get_ctx(ctx) - self.params = Z3_mk_params(self.ctx.ref()) + if params is None: + self.params = Z3_mk_params(self.ctx.ref()) + else: + self.params = params Z3_params_inc_ref(self.ctx.ref(), self.params) + def __deepcopy__(self, memo={}): + return ParamsRef(self.ctx, self.params) + def __del__(self): if self.ctx.ref() is not None: Z3_params_dec_ref(self.ctx.ref(), self.params) @@ -4709,6 +4724,9 @@ class ParamDescrsRef: self.descr = descr Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr) + def __deepcopy__(self, memo={}): + return ParamsDescrsRef(self.descr, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr) @@ -4770,6 +4788,9 @@ class Goal(Z3PPObject): self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs) Z3_goal_inc_ref(self.ctx.ref(), self.goal) + def __deepcopy__(self, memo={}): + return Goal(False, False, False, self.ctx, self.goal) + def __del__(self): if self.goal is not None and self.ctx.ref() is not None: Z3_goal_dec_ref(self.ctx.ref(), self.goal) @@ -5032,6 +5053,9 @@ class AstVector(Z3PPObject): self.ctx = ctx Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector) + def __deepcopy__(self, memo={}): + return AstVector(self.vector, self.ctx) + def __del__(self): if self.vector is not None and self.ctx.ref() is not None: Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector) @@ -5167,6 +5191,9 @@ class AstMap: self.ctx = ctx Z3_ast_map_inc_ref(self.ctx.ref(), self.map) + def __deepcopy__(self, memo={}): + return AstMap(self.map, self.ctx) + def __del__(self): if self.map is not None and self.ctx.ref() is not None: Z3_ast_map_dec_ref(self.ctx.ref(), self.map) @@ -5282,6 +5309,9 @@ class FuncEntry: self.ctx = ctx Z3_func_entry_inc_ref(self.ctx.ref(), self.entry) + def __deepcopy__(self, memo={}): + return FuncEntry(self.entry, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_func_entry_dec_ref(self.ctx.ref(), self.entry) @@ -5388,6 +5418,9 @@ class FuncInterp(Z3PPObject): if self.f is not None: Z3_func_interp_inc_ref(self.ctx.ref(), self.f) + def __deepcopy__(self, memo={}): + return FuncInterp(self.f, self.ctx) + def __del__(self): if self.f is not None and self.ctx.ref() is not None: Z3_func_interp_dec_ref(self.ctx.ref(), self.f) @@ -5498,6 +5531,9 @@ class ModelRef(Z3PPObject): self.ctx = ctx Z3_model_inc_ref(self.ctx.ref(), self.model) + def __deepcopy__(self, memo={}): + return ModelRef(self.m, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_model_dec_ref(self.ctx.ref(), self.model) @@ -5774,6 +5810,9 @@ class Statistics: self.ctx = ctx Z3_stats_inc_ref(self.ctx.ref(), self.stats) + def __deepcopy__(self, memo={}): + return Statistics(self.stats, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_stats_dec_ref(self.ctx.ref(), self.stats) @@ -5908,6 +5947,9 @@ class CheckSatResult: def __init__(self, r): self.r = r + def __deepcopy__(self, memo={}): + return CheckSatResult(self.r) + def __eq__(self, other): return isinstance(other, CheckSatResult) and self.r == other.r @@ -5947,6 +5989,9 @@ class Solver(Z3PPObject): self.solver = solver Z3_solver_inc_ref(self.ctx.ref(), self.solver) + def __deepcopy__(self, memo={}): + return Solver(self.solver, self.ctx) + def __del__(self): if self.solver is not None and self.ctx.ref() is not None: Z3_solver_dec_ref(self.ctx.ref(), self.solver) @@ -6367,6 +6412,9 @@ class Fixedpoint(Z3PPObject): Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint) self.vars = [] + def __deepcopy__(self, memo={}): + return FixedPoint(self.fixedpoint, self.ctx) + def __del__(self): if self.fixedpoint is not None and self.ctx.ref() is not None: Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint) @@ -6741,6 +6789,9 @@ class Optimize(Z3PPObject): self.optimize = Z3_mk_optimize(self.ctx.ref()) Z3_optimize_inc_ref(self.ctx.ref(), self.optimize) + def __deepcopy__(self, memo={}): + return Optimize(self.optimize, self.ctx) + def __del__(self): if self.optimize is not None and self.ctx.ref() is not None: Z3_optimize_dec_ref(self.ctx.ref(), self.optimize) @@ -6893,6 +6944,9 @@ class ApplyResult(Z3PPObject): self.ctx = ctx Z3_apply_result_inc_ref(self.ctx.ref(), self.result) + def __deepcopy__(self, memo={}): + return ApplyResult(self.result, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_apply_result_dec_ref(self.ctx.ref(), self.result) @@ -7021,6 +7075,9 @@ class Tactic: raise Z3Exception("unknown tactic '%s'" % tactic) Z3_tactic_inc_ref(self.ctx.ref(), self.tactic) + def __deepcopy__(self, memo={}): + return Tactic(self.tactic, self.ctx) + def __del__(self): if self.tactic is not None and self.ctx.ref() is not None: Z3_tactic_dec_ref(self.ctx.ref(), self.tactic) @@ -7293,6 +7350,9 @@ class Probe: raise Z3Exception("unknown probe '%s'" % probe) Z3_probe_inc_ref(self.ctx.ref(), self.probe) + def __deepcopy__(self, memo={}): + return Probe(self.probe, self.ctx) + def __del__(self): if self.probe is not None and self.ctx.ref() is not None: Z3_probe_dec_ref(self.ctx.ref(), self.probe) From 903709b9c145b011533f3ab54b6c4ae22d7b935c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 Jun 2017 17:09:01 +0100 Subject: [PATCH 06/34] [Doxygen] Fix bug where some header files were not being scanned. --- doc/z3api.cfg.in | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 9e946aa7f..9c4b464c2 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -704,10 +704,13 @@ INPUT_ENCODING = UTF-8 FILE_PATTERNS = website.dox \ z3_api.h \ z3_algebraic.h \ + z3_ast_containers.h \ + z3_fixedpoint.h \ + z3_fpa.h \ + z3_interp.h \ + z3_optimization.h \ z3_polynomial.h \ z3_rcf.h \ - z3_interp.h \ - z3_fpa.h \ z3++.h \ @PYTHON_API_FILES@ @DOTNET_API_FILES@ @JAVA_API_FILES@ From 85c7f5d8655b6a1e3721fa8ec308c51ffe87ead2 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 Jun 2017 18:22:38 +0100 Subject: [PATCH 07/34] [Doxygen] Fix some Doxygen warnings for `z3_optimization.h` --- src/api/z3_optimization.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index 795b4b8fd..f49e1b9ce 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -75,7 +75,7 @@ extern "C" { \brief Add a maximization constraint. \param c - context \param o - optimization context - \param a - arithmetical term + \param t - arithmetical term def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST))) */ unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t); @@ -84,7 +84,7 @@ extern "C" { \brief Add a minimization constraint. \param c - context \param o - optimization context - \param a - arithmetical term + \param t - arithmetical term def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST))) */ From bcb3981c5fd1988778699f3b40db8e9ce0d8c4f5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 Jun 2017 18:49:43 +0100 Subject: [PATCH 08/34] [Doxygen] Fixed mismatched `@{` and `@}` declaration which prevented the `capi` group from being declared properly. For example this prevented from `Z3_mk_solver()` from appearing in the `capi` group. --- 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 93da0b2c7..b862884c9 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -48,6 +48,7 @@ DEFINE_TYPE(Z3_rcf_num); /*@{*/ /** @name Types + @{ Most of the types in the C API are opaque pointers. @@ -5238,7 +5239,6 @@ extern "C" { def_API('Z3_get_error_msg', STRING, (_in(CONTEXT), _in(ERROR_CODE))) */ Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err); - /*@}*/ /** \brief Return a string describing the given error code. From d5f646929ef3881a0f499f40981bd98d04894e82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jun 2017 09:16:36 -0700 Subject: [PATCH 09/34] print success #1068 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 2 +- src/opt/opt_cmds.cpp | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index a098f3c94..5731f890a 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -266,7 +266,7 @@ UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr ctx.regular_stream() << std::endl; }); -UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << arg << std::endl;); +UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << "\"" << arg << "\"" << std::endl;); class set_get_option_cmd : public cmd { diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 571c26e2d..a5c163562 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -100,6 +100,7 @@ public: rational weight = ps().get_rat(symbol("weight"), rational::one()); symbol id = ps().get_sym(symbol("id"), symbol::null); get_opt(ctx, m_opt).add_soft_constraint(m_formula, weight, id); + ctx.print_success(); reset(ctx); } @@ -131,6 +132,7 @@ public: throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable"); } get_opt(ctx, m_opt).add_objective(to_app(t), m_is_max); + ctx.print_success(); } virtual void failure_cleanup(cmd_context & ctx) { From b8e8e090ad10b8557219ae6724ee215de7e7e76d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jun 2017 09:30:01 -0700 Subject: [PATCH 10/34] filter assumptions by membership in initial list #1065 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b9ed925b0..e9302bb35 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -597,16 +597,14 @@ private: extract_asm2dep(dep2asm, asm2dep); sat::literal_vector const& core = m_solver.get_core(); TRACE("sat", - dep2asm_t::iterator it2 = dep2asm.begin(); - dep2asm_t::iterator end2 = dep2asm.end(); - for (; it2 != end2; ++it2) { - tout << mk_pp(it2->m_key, m) << " |-> " << sat::literal(it2->m_value) << "\n"; + for (auto kv : dep2asm) { + tout << mk_pp(kv.m_key, m) << " |-> " << sat::literal(kv.m_value) << "\n"; } - tout << "core: "; - for (unsigned i = 0; i < core.size(); ++i) { - tout << core[i] << " "; + tout << "asm2fml: "; + for (auto kv : asm2fml) { + tout << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value, m) << "\n"; } - tout << "\n"; + tout << "core: "; for (auto c : core) tout << c << " "; tout << "\n"; ); m_core.reset(); @@ -615,8 +613,8 @@ private: VERIFY(asm2dep.find(core[i].index(), e)); if (asm2fml.contains(e)) { e = asm2fml.find(e); + m_core.push_back(e); } - m_core.push_back(e); } } From 8acb37e734f12cd889c297184ba84b256a936bce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jun 2017 09:45:18 -0700 Subject: [PATCH 11/34] revert change to 1065 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e9302bb35..b6904ef02 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -613,8 +613,8 @@ private: VERIFY(asm2dep.find(core[i].index(), e)); if (asm2fml.contains(e)) { e = asm2fml.find(e); - m_core.push_back(e); } + m_core.push_back(e); } } From f44a3e1bbcffafa9734b4d2f6292265501a14b45 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jun 2017 10:18:07 -0700 Subject: [PATCH 12/34] print_core as a function Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 5731f890a..72dfa7648 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -198,20 +198,21 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { } }); -#define PRINT_CORE() \ - ptr_vector core; \ - ctx.get_check_sat_result()->get_unsat_core(core); \ - ctx.regular_stream() << "("; \ - ptr_vector::const_iterator it = core.begin(); \ - ptr_vector::const_iterator end = core.end(); \ - for (bool first = true; it != end; ++it) { \ - if (first) \ - first = false; \ - else \ - ctx.regular_stream() << " "; \ - ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m()); \ - } \ - ctx.regular_stream() << ")" << std::endl; \ +static void print_core(cmd_context& ctx) { + ptr_vector core; + ctx.get_check_sat_result()->get_unsat_core(core); + ctx.regular_stream() << "("; + ptr_vector::const_iterator it = core.begin(); + ptr_vector::const_iterator end = core.end(); + for (bool first = true; it != end; ++it) { + if (first) + first = false; + else + ctx.regular_stream() << " "; + ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m()); + } + ctx.regular_stream() << ")" << std::endl; +} ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", { if (!ctx.produce_unsat_cores()) @@ -219,7 +220,7 @@ ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", { if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) throw cmd_exception("unsat core is not available"); - PRINT_CORE(); + print_core(ctx); }); ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset of assumptions sufficient for unsatisfiability", { @@ -228,7 +229,7 @@ ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) { throw cmd_exception("unsat assumptions is not available"); } - PRINT_CORE(); + print_core(ctx); }); From c629dcc53f431c84c6d67027cf42c7bc468f7e99 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 11 Jun 2017 14:04:18 +0100 Subject: [PATCH 13/34] [Doxygen] Rewrite documentation of `Z3_mk_solver()` and `Z3_mk_simple_solver()` to try to make it clearer what the differences are between these APIs. This an attempt to address issues noted in #1035. --- src/api/z3_api.h | 44 ++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 40 insertions(+), 4 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index b862884c9..555e6127e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5795,9 +5795,35 @@ extern "C" { /** @name Solvers*/ /*@{*/ /** - \brief Create a new (incremental) solver. This solver also uses a - set of builtin tactics for handling the first check-sat command, and - check-sat commands that take more than a given number of milliseconds to be solved. + \brief Create a new solver. This solver is a "combined solver" (see + combined_solver module) that internally uses a non-incremental (solver1) and an + incremental solver (solver2). This combined solver changes its behaviour based + on how it is used and how its parameters are set. + + If the solver is used in a non incremental way (i.e. no calls to + `Z3_solver_push()` or `Z3_solver_pop()`, and no calls to + `Z3_solver_assert()` or `Z3_solver_assert_and_track()` after checking + satisfiability without an intervening `Z3_solver_reset()`) then solver1 + will be used. This solver will apply Z3's "default" tactic. + + The "default" tactic will attempt to probe the logic used by the + assertions and will apply a specialized tactic if one is supported. + Otherwise the general `(and-then simplify smt)` tactic will be used. + + If the solver is used in an incremental way then the combined solver + will switch to using solver2 (which behaves similarly to the general + "smt" tactic). + + Note however it is possible to set the `solver2_timeout`, + `solver2_unknown`, and `ignore_solver1` parameters of the combined + solver to change its behaviour. + + The function #Z3_solver_get_model retrieves a model if the + assertions is satisfiable (i.e., the result is \c + Z3_L_TRUE) and model construction is enabled. + The function #Z3_solver_get_model can also be used even + if the result is \c Z3_L_UNDEF, but the returned model + is not guaranteed to satisfy quantified assertions. \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc. @@ -5807,7 +5833,17 @@ extern "C" { Z3_solver Z3_API Z3_mk_solver(Z3_context c); /** - \brief Create a new (incremental) solver. + \brief Create a new incremental solver. + + This is equivalent to applying the "smt" tactic. + + Unlike `Z3_mk_solver()` this solver + - Does not attempt to apply any logic specific tactics. + - Does not changes its behaviour based on whether it used + incrementally/non-incrementally. + + Note that these differences can result in very different performance + compared to `Z3_mk_solver()`. The function #Z3_solver_get_model retrieves a model if the assertions is satisfiable (i.e., the result is \c From f5b54f042c65cc15ee92d15aaa686623787b5ab1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jun 2017 11:40:39 -0700 Subject: [PATCH 14/34] apply correction by ddcc #1069 Signed-off-by: Nikolaj Bjorner --- 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 555e6127e..63f1d15ff 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5839,7 +5839,7 @@ extern "C" { Unlike `Z3_mk_solver()` this solver - Does not attempt to apply any logic specific tactics. - - Does not changes its behaviour based on whether it used + - Does not change its behaviour based on whether it used incrementally/non-incrementally. Note that these differences can result in very different performance From f0fa439c4871a7c6c08529a97bb60f674cf0d68f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jun 2017 17:17:47 -0700 Subject: [PATCH 15/34] escaping names in get-assignment #1061 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 72dfa7648..35e157af5 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -149,7 +149,7 @@ ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", { first = false; else ctx.regular_stream() << " "; - ctx.regular_stream() << "(" << name << " " << (ctx.m().is_true(val) ? "true" : "false") << ")"; + ctx.regular_stream() << "(" << escaped(name.str().c_str()) << " " << (ctx.m().is_true(val) ? "true" : "false") << ")"; } } } From 4b517b96df66c87b46a1f9c9b2e8a2d26ed0195b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 12 Jun 2017 10:21:50 +0100 Subject: [PATCH 16/34] [CMake] Move CMake files into their intended location so the `contrib/cmake/bootstrap.py` script no longer needs to be executed. The previous location of the CMake files was a compromise proposed by @agurfinkel in #461. While this has served us well (allowing progress to be made) over time limitations of this approach have appeared. The main problem is that doing many git operations (e.g. pull, rebase) means the CMake files don't get updated unless the user remembers to run the script. This can lead to broken and confusing build system behaviour. This commit only does the file moving and necessary changes to `.gitignore`. Other changes will be done in subsequent commits. --- .gitignore | 11 ----------- {contrib/cmake/cmake => cmake}/Z3Config.cmake.in | 0 .../cmake/cmake => cmake}/cmake_uninstall.cmake.in | 0 {contrib/cmake/cmake => cmake}/compiler_lto.cmake | 0 .../cmake/cmake => cmake}/compiler_warnings.cmake | 0 .../cxx_compiler_flags_overrides.cmake | 0 {contrib/cmake/cmake => cmake}/git_utils.cmake | 0 .../cmake => cmake}/modules/FindDotNetToolchain.cmake | 0 {contrib/cmake/cmake => cmake}/modules/FindGMP.cmake | 0 .../cmake/cmake => cmake}/msvc_legacy_quirks.cmake | 0 .../cmake/cmake => cmake}/target_arch_detect.cmake | 0 {contrib/cmake/cmake => cmake}/target_arch_detect.cpp | 0 {contrib/cmake/cmake => cmake}/z3_add_component.cmake | 0 {contrib/cmake/cmake => cmake}/z3_add_cxx_flag.cmake | 0 .../z3_append_linker_flag_list_to_target.cmake | 0 {contrib/cmake/doc => doc}/CMakeLists.txt | 0 {contrib/cmake/examples => examples}/CMakeLists.txt | 0 .../cmake/examples => examples}/c++/CMakeLists.txt | 0 {contrib/cmake/examples => examples}/c/CMakeLists.txt | 0 .../cmake/examples => examples}/python/CMakeLists.txt | 0 .../cmake/examples => examples}/tptp/CMakeLists.txt | 0 {contrib/cmake/src => src}/CMakeLists.txt | 0 .../cmake/src => src}/ackermannization/CMakeLists.txt | 0 {contrib/cmake/src => src}/api/CMakeLists.txt | 0 {contrib/cmake/src => src}/api/dll/CMakeLists.txt | 0 {contrib/cmake/src => src}/api/dotnet/CMakeLists.txt | 0 .../src => src}/api/dotnet/cmake_install_gac.cmake.in | 0 .../api/dotnet/cmake_uninstall_gac.cmake.in | 0 {contrib/cmake/src => src}/api/java/CMakeLists.txt | 0 {contrib/cmake/src => src}/api/python/CMakeLists.txt | 0 {contrib/cmake/src => src}/ast/CMakeLists.txt | 0 {contrib/cmake/src => src}/ast/fpa/CMakeLists.txt | 0 {contrib/cmake/src => src}/ast/macros/CMakeLists.txt | 0 .../cmake/src => src}/ast/normal_forms/CMakeLists.txt | 0 {contrib/cmake/src => src}/ast/pattern/CMakeLists.txt | 0 .../src => src}/ast/proof_checker/CMakeLists.txt | 0 .../cmake/src => src}/ast/rewriter/CMakeLists.txt | 0 .../ast/rewriter/bit_blaster/CMakeLists.txt | 0 .../cmake/src => src}/ast/simplifier/CMakeLists.txt | 0 .../cmake/src => src}/ast/substitution/CMakeLists.txt | 0 {contrib/cmake/src => src}/cmd_context/CMakeLists.txt | 0 .../src => src}/cmd_context/extra_cmds/CMakeLists.txt | 0 {contrib/cmake/src => src}/duality/CMakeLists.txt | 0 {contrib/cmake/src => src}/interp/CMakeLists.txt | 0 .../cmake/src => src}/math/automata/CMakeLists.txt | 0 {contrib/cmake/src => src}/math/euclid/CMakeLists.txt | 0 .../cmake/src => src}/math/grobner/CMakeLists.txt | 0 .../cmake/src => src}/math/hilbert/CMakeLists.txt | 0 .../cmake/src => src}/math/interval/CMakeLists.txt | 0 .../cmake/src => src}/math/polynomial/CMakeLists.txt | 0 .../cmake/src => src}/math/realclosure/CMakeLists.txt | 0 .../cmake/src => src}/math/simplex/CMakeLists.txt | 0 .../cmake/src => src}/math/subpaving/CMakeLists.txt | 0 .../src => src}/math/subpaving/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/model/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/base/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/bmc/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/clp/CMakeLists.txt | 0 .../cmake/src => src}/muz/dataflow/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/ddnf/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/duality/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/fp/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/pdr/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/rel/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/tab/CMakeLists.txt | 0 .../cmake/src => src}/muz/transforms/CMakeLists.txt | 0 {contrib/cmake/src => src}/nlsat/CMakeLists.txt | 0 .../cmake/src => src}/nlsat/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/opt/CMakeLists.txt | 0 {contrib/cmake/src => src}/parsers/smt/CMakeLists.txt | 0 .../cmake/src => src}/parsers/smt2/CMakeLists.txt | 0 .../cmake/src => src}/parsers/util/CMakeLists.txt | 0 {contrib/cmake/src => src}/qe/CMakeLists.txt | 0 {contrib/cmake/src => src}/sat/CMakeLists.txt | 0 .../cmake/src => src}/sat/sat_solver/CMakeLists.txt | 0 {contrib/cmake/src => src}/sat/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/shell/CMakeLists.txt | 0 {contrib/cmake/src => src}/smt/CMakeLists.txt | 0 {contrib/cmake/src => src}/smt/params/CMakeLists.txt | 0 .../cmake/src => src}/smt/proto_model/CMakeLists.txt | 0 {contrib/cmake/src => src}/smt/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/solver/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/aig/CMakeLists.txt | 0 .../cmake/src => src}/tactic/arith/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/bv/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/core/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/fpa/CMakeLists.txt | 0 .../cmake/src => src}/tactic/nlsat_smt/CMakeLists.txt | 0 .../cmake/src => src}/tactic/portfolio/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/sls/CMakeLists.txt | 0 .../cmake/src => src}/tactic/smtlogics/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/ufbv/CMakeLists.txt | 0 {contrib/cmake/src => src}/test/CMakeLists.txt | 0 .../cmake/src => src}/test/fuzzing/CMakeLists.txt | 0 {contrib/cmake/src => src}/util/CMakeLists.txt | 0 {contrib/cmake/src => src}/util/lp/CMakeLists.txt | 0 97 files changed, 11 deletions(-) rename {contrib/cmake/cmake => cmake}/Z3Config.cmake.in (100%) rename {contrib/cmake/cmake => cmake}/cmake_uninstall.cmake.in (100%) rename {contrib/cmake/cmake => cmake}/compiler_lto.cmake (100%) rename {contrib/cmake/cmake => cmake}/compiler_warnings.cmake (100%) rename {contrib/cmake/cmake => cmake}/cxx_compiler_flags_overrides.cmake (100%) rename {contrib/cmake/cmake => cmake}/git_utils.cmake (100%) rename {contrib/cmake/cmake => cmake}/modules/FindDotNetToolchain.cmake (100%) rename {contrib/cmake/cmake => cmake}/modules/FindGMP.cmake (100%) rename {contrib/cmake/cmake => cmake}/msvc_legacy_quirks.cmake (100%) rename {contrib/cmake/cmake => cmake}/target_arch_detect.cmake (100%) rename {contrib/cmake/cmake => cmake}/target_arch_detect.cpp (100%) rename {contrib/cmake/cmake => cmake}/z3_add_component.cmake (100%) rename {contrib/cmake/cmake => cmake}/z3_add_cxx_flag.cmake (100%) rename {contrib/cmake/cmake => cmake}/z3_append_linker_flag_list_to_target.cmake (100%) rename {contrib/cmake/doc => doc}/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/c++/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/c/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/python/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/tptp/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ackermannization/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/dll/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/dotnet/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/dotnet/cmake_install_gac.cmake.in (100%) rename {contrib/cmake/src => src}/api/dotnet/cmake_uninstall_gac.cmake.in (100%) rename {contrib/cmake/src => src}/api/java/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/python/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/fpa/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/macros/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/normal_forms/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/pattern/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/proof_checker/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/rewriter/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/rewriter/bit_blaster/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/simplifier/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/substitution/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/cmd_context/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/cmd_context/extra_cmds/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/duality/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/interp/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/automata/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/euclid/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/grobner/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/hilbert/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/interval/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/polynomial/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/realclosure/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/simplex/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/subpaving/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/subpaving/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/model/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/base/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/bmc/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/clp/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/dataflow/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/ddnf/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/duality/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/fp/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/pdr/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/rel/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/tab/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/transforms/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/nlsat/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/nlsat/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/opt/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/parsers/smt/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/parsers/smt2/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/parsers/util/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/qe/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/sat/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/sat/sat_solver/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/sat/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/shell/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/smt/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/smt/params/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/smt/proto_model/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/smt/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/solver/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/aig/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/arith/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/bv/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/core/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/fpa/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/nlsat_smt/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/portfolio/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/sls/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/smtlogics/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/ufbv/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/test/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/test/fuzzing/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/util/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/util/lp/CMakeLists.txt (100%) diff --git a/.gitignore b/.gitignore index cc1c2a754..b7e4a0186 100644 --- a/.gitignore +++ b/.gitignore @@ -75,14 +75,3 @@ src/api/ml/z3.mllib *.bak doc/api doc/code - -# CMake files copied over by the ``contrib/cmake/boostrap.py`` script -# See #461 -examples/CMakeLists.txt -examples/*/CMakeLists.txt -src/CMakeLists.txt -src/*/CMakeLists.txt -src/*/*/CMakeLists.txt -src/*/*/*/CMakeLists.txt -src/api/dotnet/cmake_install_gac.cmake.in -src/api/dotnet/cmake_uninstall_gac.cmake.in diff --git a/contrib/cmake/cmake/Z3Config.cmake.in b/cmake/Z3Config.cmake.in similarity index 100% rename from contrib/cmake/cmake/Z3Config.cmake.in rename to cmake/Z3Config.cmake.in diff --git a/contrib/cmake/cmake/cmake_uninstall.cmake.in b/cmake/cmake_uninstall.cmake.in similarity index 100% rename from contrib/cmake/cmake/cmake_uninstall.cmake.in rename to cmake/cmake_uninstall.cmake.in diff --git a/contrib/cmake/cmake/compiler_lto.cmake b/cmake/compiler_lto.cmake similarity index 100% rename from contrib/cmake/cmake/compiler_lto.cmake rename to cmake/compiler_lto.cmake diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake similarity index 100% rename from contrib/cmake/cmake/compiler_warnings.cmake rename to cmake/compiler_warnings.cmake diff --git a/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake b/cmake/cxx_compiler_flags_overrides.cmake similarity index 100% rename from contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake rename to cmake/cxx_compiler_flags_overrides.cmake diff --git a/contrib/cmake/cmake/git_utils.cmake b/cmake/git_utils.cmake similarity index 100% rename from contrib/cmake/cmake/git_utils.cmake rename to cmake/git_utils.cmake diff --git a/contrib/cmake/cmake/modules/FindDotNetToolchain.cmake b/cmake/modules/FindDotNetToolchain.cmake similarity index 100% rename from contrib/cmake/cmake/modules/FindDotNetToolchain.cmake rename to cmake/modules/FindDotNetToolchain.cmake diff --git a/contrib/cmake/cmake/modules/FindGMP.cmake b/cmake/modules/FindGMP.cmake similarity index 100% rename from contrib/cmake/cmake/modules/FindGMP.cmake rename to cmake/modules/FindGMP.cmake diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/cmake/msvc_legacy_quirks.cmake similarity index 100% rename from contrib/cmake/cmake/msvc_legacy_quirks.cmake rename to cmake/msvc_legacy_quirks.cmake diff --git a/contrib/cmake/cmake/target_arch_detect.cmake b/cmake/target_arch_detect.cmake similarity index 100% rename from contrib/cmake/cmake/target_arch_detect.cmake rename to cmake/target_arch_detect.cmake diff --git a/contrib/cmake/cmake/target_arch_detect.cpp b/cmake/target_arch_detect.cpp similarity index 100% rename from contrib/cmake/cmake/target_arch_detect.cpp rename to cmake/target_arch_detect.cpp diff --git a/contrib/cmake/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake similarity index 100% rename from contrib/cmake/cmake/z3_add_component.cmake rename to cmake/z3_add_component.cmake diff --git a/contrib/cmake/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake similarity index 100% rename from contrib/cmake/cmake/z3_add_cxx_flag.cmake rename to cmake/z3_add_cxx_flag.cmake diff --git a/contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake b/cmake/z3_append_linker_flag_list_to_target.cmake similarity index 100% rename from contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake rename to cmake/z3_append_linker_flag_list_to_target.cmake diff --git a/contrib/cmake/doc/CMakeLists.txt b/doc/CMakeLists.txt similarity index 100% rename from contrib/cmake/doc/CMakeLists.txt rename to doc/CMakeLists.txt diff --git a/contrib/cmake/examples/CMakeLists.txt b/examples/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/CMakeLists.txt rename to examples/CMakeLists.txt diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/c++/CMakeLists.txt rename to examples/c++/CMakeLists.txt diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/c/CMakeLists.txt rename to examples/c/CMakeLists.txt diff --git a/contrib/cmake/examples/python/CMakeLists.txt b/examples/python/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/python/CMakeLists.txt rename to examples/python/CMakeLists.txt diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/examples/tptp/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/tptp/CMakeLists.txt rename to examples/tptp/CMakeLists.txt diff --git a/contrib/cmake/src/CMakeLists.txt b/src/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/CMakeLists.txt rename to src/CMakeLists.txt diff --git a/contrib/cmake/src/ackermannization/CMakeLists.txt b/src/ackermannization/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ackermannization/CMakeLists.txt rename to src/ackermannization/CMakeLists.txt diff --git a/contrib/cmake/src/api/CMakeLists.txt b/src/api/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/CMakeLists.txt rename to src/api/CMakeLists.txt diff --git a/contrib/cmake/src/api/dll/CMakeLists.txt b/src/api/dll/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/dll/CMakeLists.txt rename to src/api/dll/CMakeLists.txt diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/dotnet/CMakeLists.txt rename to src/api/dotnet/CMakeLists.txt diff --git a/contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in b/src/api/dotnet/cmake_install_gac.cmake.in similarity index 100% rename from contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in rename to src/api/dotnet/cmake_install_gac.cmake.in diff --git a/contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in b/src/api/dotnet/cmake_uninstall_gac.cmake.in similarity index 100% rename from contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in rename to src/api/dotnet/cmake_uninstall_gac.cmake.in diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/java/CMakeLists.txt rename to src/api/java/CMakeLists.txt diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/python/CMakeLists.txt rename to src/api/python/CMakeLists.txt diff --git a/contrib/cmake/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/CMakeLists.txt rename to src/ast/CMakeLists.txt diff --git a/contrib/cmake/src/ast/fpa/CMakeLists.txt b/src/ast/fpa/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/fpa/CMakeLists.txt rename to src/ast/fpa/CMakeLists.txt diff --git a/contrib/cmake/src/ast/macros/CMakeLists.txt b/src/ast/macros/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/macros/CMakeLists.txt rename to src/ast/macros/CMakeLists.txt diff --git a/contrib/cmake/src/ast/normal_forms/CMakeLists.txt b/src/ast/normal_forms/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/normal_forms/CMakeLists.txt rename to src/ast/normal_forms/CMakeLists.txt diff --git a/contrib/cmake/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/pattern/CMakeLists.txt rename to src/ast/pattern/CMakeLists.txt diff --git a/contrib/cmake/src/ast/proof_checker/CMakeLists.txt b/src/ast/proof_checker/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/proof_checker/CMakeLists.txt rename to src/ast/proof_checker/CMakeLists.txt diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/rewriter/CMakeLists.txt rename to src/ast/rewriter/CMakeLists.txt diff --git a/contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt b/src/ast/rewriter/bit_blaster/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt rename to src/ast/rewriter/bit_blaster/CMakeLists.txt diff --git a/contrib/cmake/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/simplifier/CMakeLists.txt rename to src/ast/simplifier/CMakeLists.txt diff --git a/contrib/cmake/src/ast/substitution/CMakeLists.txt b/src/ast/substitution/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/substitution/CMakeLists.txt rename to src/ast/substitution/CMakeLists.txt diff --git a/contrib/cmake/src/cmd_context/CMakeLists.txt b/src/cmd_context/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/cmd_context/CMakeLists.txt rename to src/cmd_context/CMakeLists.txt diff --git a/contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt b/src/cmd_context/extra_cmds/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt rename to src/cmd_context/extra_cmds/CMakeLists.txt diff --git a/contrib/cmake/src/duality/CMakeLists.txt b/src/duality/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/duality/CMakeLists.txt rename to src/duality/CMakeLists.txt diff --git a/contrib/cmake/src/interp/CMakeLists.txt b/src/interp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/interp/CMakeLists.txt rename to src/interp/CMakeLists.txt diff --git a/contrib/cmake/src/math/automata/CMakeLists.txt b/src/math/automata/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/automata/CMakeLists.txt rename to src/math/automata/CMakeLists.txt diff --git a/contrib/cmake/src/math/euclid/CMakeLists.txt b/src/math/euclid/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/euclid/CMakeLists.txt rename to src/math/euclid/CMakeLists.txt diff --git a/contrib/cmake/src/math/grobner/CMakeLists.txt b/src/math/grobner/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/grobner/CMakeLists.txt rename to src/math/grobner/CMakeLists.txt diff --git a/contrib/cmake/src/math/hilbert/CMakeLists.txt b/src/math/hilbert/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/hilbert/CMakeLists.txt rename to src/math/hilbert/CMakeLists.txt diff --git a/contrib/cmake/src/math/interval/CMakeLists.txt b/src/math/interval/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/interval/CMakeLists.txt rename to src/math/interval/CMakeLists.txt diff --git a/contrib/cmake/src/math/polynomial/CMakeLists.txt b/src/math/polynomial/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/polynomial/CMakeLists.txt rename to src/math/polynomial/CMakeLists.txt diff --git a/contrib/cmake/src/math/realclosure/CMakeLists.txt b/src/math/realclosure/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/realclosure/CMakeLists.txt rename to src/math/realclosure/CMakeLists.txt diff --git a/contrib/cmake/src/math/simplex/CMakeLists.txt b/src/math/simplex/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/simplex/CMakeLists.txt rename to src/math/simplex/CMakeLists.txt diff --git a/contrib/cmake/src/math/subpaving/CMakeLists.txt b/src/math/subpaving/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/subpaving/CMakeLists.txt rename to src/math/subpaving/CMakeLists.txt diff --git a/contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt b/src/math/subpaving/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt rename to src/math/subpaving/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/model/CMakeLists.txt b/src/model/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/model/CMakeLists.txt rename to src/model/CMakeLists.txt diff --git a/contrib/cmake/src/muz/base/CMakeLists.txt b/src/muz/base/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/base/CMakeLists.txt rename to src/muz/base/CMakeLists.txt diff --git a/contrib/cmake/src/muz/bmc/CMakeLists.txt b/src/muz/bmc/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/bmc/CMakeLists.txt rename to src/muz/bmc/CMakeLists.txt diff --git a/contrib/cmake/src/muz/clp/CMakeLists.txt b/src/muz/clp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/clp/CMakeLists.txt rename to src/muz/clp/CMakeLists.txt diff --git a/contrib/cmake/src/muz/dataflow/CMakeLists.txt b/src/muz/dataflow/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/dataflow/CMakeLists.txt rename to src/muz/dataflow/CMakeLists.txt diff --git a/contrib/cmake/src/muz/ddnf/CMakeLists.txt b/src/muz/ddnf/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/ddnf/CMakeLists.txt rename to src/muz/ddnf/CMakeLists.txt diff --git a/contrib/cmake/src/muz/duality/CMakeLists.txt b/src/muz/duality/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/duality/CMakeLists.txt rename to src/muz/duality/CMakeLists.txt diff --git a/contrib/cmake/src/muz/fp/CMakeLists.txt b/src/muz/fp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/fp/CMakeLists.txt rename to src/muz/fp/CMakeLists.txt diff --git a/contrib/cmake/src/muz/pdr/CMakeLists.txt b/src/muz/pdr/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/pdr/CMakeLists.txt rename to src/muz/pdr/CMakeLists.txt diff --git a/contrib/cmake/src/muz/rel/CMakeLists.txt b/src/muz/rel/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/rel/CMakeLists.txt rename to src/muz/rel/CMakeLists.txt diff --git a/contrib/cmake/src/muz/tab/CMakeLists.txt b/src/muz/tab/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/tab/CMakeLists.txt rename to src/muz/tab/CMakeLists.txt diff --git a/contrib/cmake/src/muz/transforms/CMakeLists.txt b/src/muz/transforms/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/transforms/CMakeLists.txt rename to src/muz/transforms/CMakeLists.txt diff --git a/contrib/cmake/src/nlsat/CMakeLists.txt b/src/nlsat/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/nlsat/CMakeLists.txt rename to src/nlsat/CMakeLists.txt diff --git a/contrib/cmake/src/nlsat/tactic/CMakeLists.txt b/src/nlsat/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/nlsat/tactic/CMakeLists.txt rename to src/nlsat/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/opt/CMakeLists.txt rename to src/opt/CMakeLists.txt diff --git a/contrib/cmake/src/parsers/smt/CMakeLists.txt b/src/parsers/smt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/parsers/smt/CMakeLists.txt rename to src/parsers/smt/CMakeLists.txt diff --git a/contrib/cmake/src/parsers/smt2/CMakeLists.txt b/src/parsers/smt2/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/parsers/smt2/CMakeLists.txt rename to src/parsers/smt2/CMakeLists.txt diff --git a/contrib/cmake/src/parsers/util/CMakeLists.txt b/src/parsers/util/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/parsers/util/CMakeLists.txt rename to src/parsers/util/CMakeLists.txt diff --git a/contrib/cmake/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/qe/CMakeLists.txt rename to src/qe/CMakeLists.txt diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/sat/CMakeLists.txt rename to src/sat/CMakeLists.txt diff --git a/contrib/cmake/src/sat/sat_solver/CMakeLists.txt b/src/sat/sat_solver/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/sat/sat_solver/CMakeLists.txt rename to src/sat/sat_solver/CMakeLists.txt diff --git a/contrib/cmake/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/sat/tactic/CMakeLists.txt rename to src/sat/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/shell/CMakeLists.txt rename to src/shell/CMakeLists.txt diff --git a/contrib/cmake/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/CMakeLists.txt rename to src/smt/CMakeLists.txt diff --git a/contrib/cmake/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/params/CMakeLists.txt rename to src/smt/params/CMakeLists.txt diff --git a/contrib/cmake/src/smt/proto_model/CMakeLists.txt b/src/smt/proto_model/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/proto_model/CMakeLists.txt rename to src/smt/proto_model/CMakeLists.txt diff --git a/contrib/cmake/src/smt/tactic/CMakeLists.txt b/src/smt/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/tactic/CMakeLists.txt rename to src/smt/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/solver/CMakeLists.txt rename to src/solver/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/CMakeLists.txt rename to src/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/aig/CMakeLists.txt b/src/tactic/aig/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/aig/CMakeLists.txt rename to src/tactic/aig/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/arith/CMakeLists.txt rename to src/tactic/arith/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/bv/CMakeLists.txt rename to src/tactic/bv/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/core/CMakeLists.txt rename to src/tactic/core/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/fpa/CMakeLists.txt b/src/tactic/fpa/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/fpa/CMakeLists.txt rename to src/tactic/fpa/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt b/src/tactic/nlsat_smt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt rename to src/tactic/nlsat_smt/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/portfolio/CMakeLists.txt rename to src/tactic/portfolio/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/sls/CMakeLists.txt b/src/tactic/sls/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/sls/CMakeLists.txt rename to src/tactic/sls/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/smtlogics/CMakeLists.txt rename to src/tactic/smtlogics/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/ufbv/CMakeLists.txt b/src/tactic/ufbv/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/ufbv/CMakeLists.txt rename to src/tactic/ufbv/CMakeLists.txt diff --git a/contrib/cmake/src/test/CMakeLists.txt b/src/test/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/test/CMakeLists.txt rename to src/test/CMakeLists.txt diff --git a/contrib/cmake/src/test/fuzzing/CMakeLists.txt b/src/test/fuzzing/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/test/fuzzing/CMakeLists.txt rename to src/test/fuzzing/CMakeLists.txt diff --git a/contrib/cmake/src/util/CMakeLists.txt b/src/util/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/util/CMakeLists.txt rename to src/util/CMakeLists.txt diff --git a/contrib/cmake/src/util/lp/CMakeLists.txt b/src/util/lp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/util/lp/CMakeLists.txt rename to src/util/lp/CMakeLists.txt From 5be503798ff97f8f9249a46145be23955a2e41ae Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 12 Jun 2017 10:29:01 +0100 Subject: [PATCH 17/34] [CMake] Remove bootstrap check. Now that the CMake files are in their correct location we don't need it anymore. --- CMakeLists.txt | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 7400f67e2..5ed7ee06a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,16 +14,6 @@ if (POLICY CMP0054) cmake_policy(SET CMP0054 OLD) endif() -# Provide a friendly message if the user hasn't run the bootstrap script -# to copy all the CMake files into their correct location. -# It is unfortunate that we have to do this, see #461 for the discussion -# on this. -if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt")) - message(FATAL_ERROR "Cannot find \"${CMAKE_SOURCE_DIR}/src/CMakeLists.txt\"" - ". This probably means you need to run" - "``python contrib/cmake/bootstrap.py create``") -endif() - set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") project(Z3 CXX) From 5c3b11f034ff0550aaced0b61266382edb28ba9c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 12 Jun 2017 10:39:49 +0100 Subject: [PATCH 18/34] [CMake] Modify `contrib/cmake/bootstrap.py` to do nothing except print a warning. Now that the CMake files have been moved into their intended location it is no longer necessary for this script to exist. However we do not want to break out-of-tree scripts that build Z3 using CMake to suddenly break. So the script has been modified to do nothing except print a warning. Eventually we should remove this script. --- contrib/cmake/bootstrap.py | 233 ++----------------------------------- 1 file changed, 10 insertions(+), 223 deletions(-) diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py index a3c81fb25..dac08b383 100755 --- a/contrib/cmake/bootstrap.py +++ b/contrib/cmake/bootstrap.py @@ -1,25 +1,13 @@ #!/usr/bin/env python """ -This script is used to copy or delete the -CMake build system files from the contrib/cmake -folder into the their correct location in the Z3 -repository. +This script is an artifact of compromise that was +made when the CMake build system was first introduced +(see #461). -It offers two modes - -* create - This will symlink the ``cmake`` directory and copy (or hard link) -the appropriate files into their correct locations in the repository. - -* remove - This will remove the symlinked ``cmake`` -directory and remove the files added by the above -methods. - -This has the advantage -that editing the hard link edits the underlying file -(making development easier because copying files is -not neccessary) and CMake will regenerate correctly -because the modification time stamps will be correct. +This script now does nothing. It remains only to not +break out-of-tree scripts that build Z3 using CMake. +Eventually this script will be removed. """ import argparse import logging @@ -28,189 +16,6 @@ import pprint import shutil import sys -def get_full_path_to_script(): - return os.path.abspath(__file__) - -def get_cmake_contrib_dir(): - return os.path.dirname(get_full_path_to_script()) - -def get_repo_root_dir(): - r = os.path.dirname(os.path.dirname(get_cmake_contrib_dir())) - assert os.path.isdir(r) - return r - -# These are paths that should be ignored when checking if a folder -# in the ``contrib/cmake`` exists in the root of the repository -verificationExceptions = { - os.path.join(get_repo_root_dir(), 'cmake'), - os.path.join(get_repo_root_dir(), 'cmake', 'modules') -} - -def contribPathToRepoPath(path): - assert path.startswith(get_cmake_contrib_dir()) - stripped = path[len(get_cmake_contrib_dir()) + 1:] # Plus one is to remove leading slash - assert not os.path.isabs(stripped) - logging.debug('stripped:{}'.format(stripped)) - r = os.path.join(get_repo_root_dir(), stripped) - assert os.path.isabs(r) - logging.debug('Converted contrib path "{}" to repo path "{}"'.format(path, r)) - return r - -def verify_mirrored_directory_struture(): - """ - Check that the directories contained in ``contrib/cmake`` exist - in the root of the repo. - """ - for (dirpath, _, _) in os.walk(get_cmake_contrib_dir()): - expectedDir = contribPathToRepoPath(dirpath) - logging.debug('expectedDir:{}'.format(expectedDir)) - if (not (os.path.exists(expectedDir) and os.path.isdir(expectedDir)) and - expectedDir not in verificationExceptions): - logging.error(('Expected to find directory "{}" but it does not exist' - ' or is not a directory').format(expectedDir)) - return 1 - - return 0 - -def mk_sym_link(target, linkName): - logging.info('Making symbolic link target="{}", linkName="{}"'.format(target, linkName)) - if os.path.exists(linkName): - logging.info('Removing existing link "{}"'.format(linkName)) - if not os.path.islink(linkName): - logging.warning('"{}" overwriting file that is not a symlink'.format(linkName)) - delete_path(linkName) - if os.name == 'posix': - os.symlink(target, linkName) - else: - # TODO: Windows does support symlinks but the implementation to do that - # from python is a little complicated so for now lets just copy everyting - logging.warning('Creating symbolic links is not supported. Just making a copy instead') - if os.path.isdir(target): - # Recursively copy directory - shutil.copytree(src=target, dst=linkName, symlinks=False) - else: - # Copy file - assert os.path.isfile(target) - shutil.copy2(src=target, dst=linkName) - -def delete_path(path): - logging.info('Removing "{}"'.format(path)) - if not os.path.exists(path): - logging.warning('"{}" does not exist'.format(path)) - return - if os.path.isdir(path) and not os.path.islink(path): - # FIXME: If we can get symbolic link support on Windows we - # can disallow this completely. - assert os.name == 'nt' - shutil.rmtree(path) - else: - os.remove(path) - -def shouldSkipFile(path): - # Skip this script - if path == get_full_path_to_script(): - return True - # Skip the maintainers file - if path == os.path.join(get_cmake_contrib_dir(), 'maintainers.txt'): - return True - # Skip Vim temporary files - if os.path.basename(path).startswith('.') and path.endswith('.swp'): - return True - return False - - -def create(useHardLinks): - """ - Copy or hard link files in the CMake contrib directory - into the repository where they are intended to live. - - Note that symbolic links for the CMakeLists.txt files - are not appropriate because they won't have the right - file modification time when the files they point to - are modified. This would prevent CMake from correctly - reconfiguring when it detects this is required. - """ - - # Make the ``cmake`` directory a symbolic link. - # We treat this one specially as it is the only directory - # that doesn't already exist in the repository root so - # we can just use a symlink here - linkName = os.path.join(get_repo_root_dir(), 'cmake') - target = os.path.join(get_cmake_contrib_dir(), 'cmake') - specialDir = target - mk_sym_link(target, linkName) - - for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()): - # Skip the special directory and its children - if dirPath.startswith(specialDir): - logging.info('Skipping directory "{}"'.format(dirPath)) - continue - - for fileName in fileNames: - fileInContrib = os.path.join(dirPath, fileName) - # Skip files - if shouldSkipFile(fileInContrib): - logging.info('Skipping "{}"'.format(fileInContrib)) - continue - fileInRepo = contribPathToRepoPath(fileInContrib) - logging.info('"{}" => "{}"'.format(fileInContrib, fileInRepo)) - if useHardLinks: - if not os.name == 'posix': - logging.error('Hard links are not supported on your platform') - return False - if os.path.exists(fileInRepo): - delete_path(fileInRepo) - os.link(fileInContrib, fileInRepo) - else: - try: - shutil.copy2(src=fileInContrib, dst=fileInRepo) - except shutil.Error as e: - # Can hit this if used created hard links first and then run again without - # wanting hard links - if sys.version_info.major <= 2: - logging.error(e.message) - else: - # Python >= 3 - if isinstance(e, shutil.SameFileError): - logging.error('Trying to copy "{}" to "{}" but they are the same file'.format( - fileInContrib, fileInRepo)) - else: - logging.error(e) - logging.error('You should remove the files using the "remove" mode ' - 'and try to create again. You probably are mixing the ' - 'hard-link and non-hard-link create modes') - return False - return True - -def remove(): - """ - Remove the CMake files from their intended location in - the repository. This is used to remove - the files created by the ``create()`` function. - """ - # This directory is treated specially as it is normally - # a symlink. - linkName = os.path.join(get_repo_root_dir(), 'cmake') - delete_path(linkName) - specialDir = os.path.join(get_cmake_contrib_dir(), 'cmake') - - for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()): - # Skip the special directory and its children - if dirPath.startswith(specialDir): - logging.info('Skipping directory "{}"'.format(dirPath)) - continue - for fileName in fileNames: - fileInContrib = os.path.join(dirPath, fileName) - # Skip files - if shouldSkipFile(fileInContrib): - logging.info('Skipping "{}"'.format(fileInContrib)) - continue - fileInRepo = contribPathToRepoPath(fileInContrib) - if os.path.exists(fileInRepo): - logging.info('Removing "{}"'.format(fileInRepo)) - delete_path(fileInRepo) - return True - def main(args): logging.basicConfig(level=logging.INFO) parser = argparse.ArgumentParser(description=__doc__) @@ -233,28 +38,10 @@ def main(args): logLevel = getattr(logging, pargs.log_level.upper(),None) logging.basicConfig(level=logLevel) - - # Before we start make sure we can transplant the CMake files on to - # repository - if verify_mirrored_directory_struture() != 0: - logging.error('"{}" does not mirror "{}"'.format(get_cmake_contrib_dir(), get_repo_root_dir())) - return 1 - - if pargs.mode == "create": - if not create(useHardLinks=pargs.hard_link): - logging.error("Failed to create") - return 1 - elif pargs.mode == "create_hard_link": - if not create(useHardLinks=True): - logging.error("Failed to create_hard_link") - return 1 - elif pargs.mode == "remove": - if not remove(): - logging.error("Failed to remove") - return 1 - else: - logging.error('Unknown mode "{}"'.format(pargs.mode)) - + logging.warning('Use of this script is deprecated. The script will be removed in the future') + logging.warning('Action "{}" ignored'.format(pargs.mode)) + if pargs.hard_link: + logging.warning('Hard link option ignored') return 0 if __name__ == '__main__': From 814fcd6a17e2602ddeb446347d89441c56162402 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 12 Jun 2017 10:44:19 +0100 Subject: [PATCH 19/34] [CMake] Remove documentation on "Bootstrapping". It is no longer relevant. --- README-CMake.md | 66 ------------------------------------------------- 1 file changed, 66 deletions(-) diff --git a/README-CMake.md b/README-CMake.md index 1b7d89542..7550808fc 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -33,34 +33,6 @@ git clean -fx src which will remove the generated source files. -### Bootstrapping - -Most of Z3's CMake files do not live in their correct location. Instead those -files live in the ``contrib/cmake`` folder and a script is provided that will -copy (or hard link) the files into their correct location. - -To copy the files run - -``` -python contrib/cmake/bootstrap.py create -``` - -in the root of the repository. Once you have done this you can now build Z3 using CMake. -Make sure you remember to rerun this command if you pull down new code/rebase/change branch so -that the copied CMake files are up to date. - -To remove the copied files run - -``` -python contrib/cmake/bootstrap.py remove -``` - -Note if you plan to do development on Z3 you should read the developer -notes on bootstrapping in this document. - -What follows is a brief walk through of how to build Z3 using some -of the more commonly used CMake generators. - ### Unix Makefiles Run the following in the top level directory of the Z3 repository. @@ -328,44 +300,6 @@ link is not created when building under Windows. These notes are help developers and packagers of Z3. -### Boostrapping the CMake build - -Z3's CMake system is experimental and not officially supported. Consequently -Z3's developers have decided that they do not want the CMake files in the -``src/`` and ``examples/`` folders. Instead the ``contrib/cmake/bootstrap.py`` -script copies or hard links them into the correct locations. For context -on this decision see https://github.com/Z3Prover/z3/pull/461 . - -The ``contrib/cmake/bootstrap.py create`` command just copies over files which makes -development harder because you have to copy your modifications over to the -files in ``contrib/cmake`` for your changes to committed to git. If you are on a UNIX like -platform you can create hard links instead by running - -``` -contrib/cmake/boostrap.py create --hard-link -``` - -Using hard links means that modifying any of the "copied" files also modifies the -file under version control. Using hard links also means that the file modification time -will appear correct (i.e. the hard-linked "copies" have the same file modification time -as the corresponding file under version control) which means CMake will correctly reconfigure -when invoked. This is why using symbolic links is not an option because the file modification -time of a symbolic link is not the same as the file modification of the file being pointed to. - -Unfortunately a downside to using hard links (or just plain copies) is that if -you pull down new code (i.e. ``git pull``) then some of the CMake files under -version control may change but the corresponding hard-linked "copies" will not. - -This mean that (regardless of whether or not you use hard links) every time you -pull down new code or change branch or do an interactive rebase you must run -(with or without ``--hard-link``): - -``` -contrb/cmake/boostrap.py create -``` - -in order to be sure that the copied CMake files are not out of date. - ### Install/Uninstall Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to From 6bce1732483531e2ca65f34369bb449ba9e9c5fc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Jun 2017 18:35:02 -0700 Subject: [PATCH 20/34] properly quote symbols #1061 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 35e157af5..f6eea729f 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -149,7 +149,14 @@ ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", { first = false; else ctx.regular_stream() << " "; - ctx.regular_stream() << "(" << escaped(name.str().c_str()) << " " << (ctx.m().is_true(val) ? "true" : "false") << ")"; + ctx.regular_stream() << "("; + if (is_smt2_quoted_symbol(name)) { + ctx.regular_stream() << mk_smt2_quoted_symbol(name); + } + else { + ctx.regular_stream() << name; + } + ctx.regular_stream() << " " << (ctx.m().is_true(val) ? "true" : "false") << ")"; } } } From 3a692fe33c2992576ad381d050836a3b0913c996 Mon Sep 17 00:00:00 2001 From: "KangJing Huang (Chaserhkj)" Date: Tue, 13 Jun 2017 00:25:36 -0400 Subject: [PATCH 21/34] Add translate method for FuncDecl in java api --- src/api/java/FuncDecl.java | 32 +++++++++++++++++++++++++------- 1 file changed, 25 insertions(+), 7 deletions(-) diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 273e853c0..5909540b4 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -1,6 +1,6 @@ /** Copyright (c) 2012-2014 Microsoft Corporation - + Module Name: FuncDecl.java @@ -12,8 +12,8 @@ Author: @author Christoph Wintersteiger (cwinter) 2012-03-15 Notes: - -**/ + +**/ package com.microsoft.z3; @@ -59,6 +59,24 @@ public class FuncDecl extends AST return Native.getFuncDeclId(getContext().nCtx(), getNativeObject()); } + /** + * Translates (copies) the AST to the Context {@code ctx}. + * @param ctx A context + * + * @return A copy of the AST which is associated with {@code ctx} + * @throws Z3Exception on error + **/ + public FuncDecl translate(Context ctx) + { + + if (getContext() == ctx) { + return this; + } else { + return new FuncDecl(ctx, Native.translate(getContext().nCtx(), + getNativeObject(), ctx.nCtx())); + } + } + /** * The arity of the function declaration **/ @@ -68,7 +86,7 @@ public class FuncDecl extends AST } /** - * The size of the domain of the function declaration + * The size of the domain of the function declaration * @see #getArity **/ public int getDomainSize() @@ -324,7 +342,7 @@ public class FuncDecl extends AST } FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) - + { super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(), AST.arrayLength(domain), AST.arrayToNative(domain), @@ -333,7 +351,7 @@ public class FuncDecl extends AST } FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range) - + { super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, AST.arrayLength(domain), AST.arrayToNative(domain), @@ -351,7 +369,7 @@ public class FuncDecl extends AST } /** - * Create expression that applies function to arguments. + * Create expression that applies function to arguments. **/ public Expr apply(Expr ... args) { From 5799947183980eb440cfff243ca794e14872ce0b Mon Sep 17 00:00:00 2001 From: "KangJing Huang (Chaserhkj)" Date: Tue, 13 Jun 2017 02:37:41 -0400 Subject: [PATCH 22/34] Fix docstrings for FuncDecl.translate --- src/api/java/FuncDecl.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 5909540b4..8b1ad4b44 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -60,10 +60,10 @@ public class FuncDecl extends AST } /** - * Translates (copies) the AST to the Context {@code ctx}. + * Translates (copies) the function declaration to the Context {@code ctx}. * @param ctx A context * - * @return A copy of the AST which is associated with {@code ctx} + * @return A copy of the function declaration which is associated with {@code ctx} * @throws Z3Exception on error **/ public FuncDecl translate(Context ctx) From a59ee8032c0e6e7483f0b2bdad4b0dbe71ea4d1f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jun 2017 19:02:59 -0700 Subject: [PATCH 23/34] fix unsoundness bug in axiomatization of str.at. #1067 Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/FuncDecl.cs | 1 - src/smt/smt_conflict_resolution.cpp | 4 +++- src/smt/theory_seq.cpp | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 2f5cd0ce8..df90f9cd4 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -342,6 +342,5 @@ namespace Microsoft.Z3 Context.CheckContextMatch(args); return Expr.Create(Context, this, args); } - } } diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 8d90f9583..ade667e34 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -1405,6 +1405,7 @@ namespace smt { switch (js.get_kind()) { case b_justification::CLAUSE: { clause * cls = js.get_clause(); + TRACE("unsat_core_bug", m_ctx.display_clause_detail(tout, cls);); unsigned num_lits = cls->get_num_literals(); unsigned i = 0; if (consequent != false_literal) { @@ -1422,8 +1423,9 @@ namespace smt { process_antecedent_for_unsat_core(~l); } justification * js = cls->get_justification(); - if (js) + if (js) { process_justification_for_unsat_core(js); + } break; } case b_justification::BIN_CLAUSE: diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 3f8845546..af8b9e395 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3567,8 +3567,8 @@ void theory_seq::add_at_axiom(expr* e) { add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false)); add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false)); - add_axiom(i_ge_0, mk_eq(s, emp, false)); - add_axiom(~i_ge_len_s, mk_eq(s, emp, false)); + add_axiom(i_ge_0, mk_eq(e, emp, false)); + add_axiom(~i_ge_len_s, mk_eq(e, emp, false)); } /** From c2acbc295774ef2da927a89002fe433138bb29cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jun 2017 19:11:28 -0700 Subject: [PATCH 24/34] port FuncDecl copy to dotnet, continuation of #1073 Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/FuncDecl.cs | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index df90f9cd4..345019892 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -315,6 +315,23 @@ namespace Microsoft.Z3 #endif #endregion + /// + /// Translates (copies) the function declaration to the Context . + /// + /// A context + /// A copy of the function declaration which is associated with + new public FuncDecl Translate(Context ctx) + { + Contract.Requires(ctx != null); + Contract.Ensures(Contract.Result() != null); + + if (ReferenceEquals(Context, ctx)) + return this; + else + return new FuncDecl(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx)); + } + + /// /// Create expression that applies function to arguments. /// From 8b12cc0bdfc1bee9f5f405ac596309dbbe16d140 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jun 2017 19:58:55 -0700 Subject: [PATCH 25/34] fix build warning Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 2 +- src/cmd_context/cmd_context.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index d4273d42d..caafbfb8c 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -325,8 +325,8 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_status(UNKNOWN), m_numeral_as_real(false), m_ignore_check(false), - m_exit_on_error(false), m_processing_pareto(false), + m_exit_on_error(false), m_manager(m), m_own_manager(m == 0), m_manager_initialized(false), diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index ed92ab909..b231e3c82 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -159,7 +159,7 @@ protected: bool m_produce_assignments; status m_status; bool m_numeral_as_real; - bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. + bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. bool m_processing_pareto; // used when re-entering check-sat for pareto front. bool m_exit_on_error; From b978f78c21b639bee034693d5bfc627d914e7424 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jun 2017 20:35:35 -0700 Subject: [PATCH 26/34] add sequence recognizers Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Expr.cs | 55 +++++++++++++++++++++++++++++++++ src/cmd_context/cmd_context.cpp | 1 + 2 files changed, 56 insertions(+) diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 23ffe61bd..5e0abcb74 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -811,6 +811,61 @@ namespace Microsoft.Z3 /// the expression should be a string constant, (IsString should be true). public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } } + /// + /// Check whether expression is a concatentation. + /// + /// a Boolean + public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } } + + /// + /// Check whether expression is a prefix. + /// + /// a Boolean + public bool IsPrefix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } } + + /// + /// Check whether expression is a suffix. + /// + /// a Boolean + public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } } + + /// + /// Check whether expression is a contains. + /// + /// a Boolean + public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } } + + /// + /// Check whether expression is an extract. + /// + /// a Boolean + public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } } + + /// + /// Check whether expression is a replace. + /// + /// a Boolean + public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } } + + /// + /// Check whether expression is an at. + /// + /// a Boolean + public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } } + + /// + /// Check whether expression is a sequence length. + /// + /// a Boolean + public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } } + + /// + /// Check whether expression is a sequence index. + /// + /// a Boolean + public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } } + + #endregion #region Proof Terms diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index caafbfb8c..af16f5796 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -15,6 +15,7 @@ Author: Notes: --*/ + #include #include"tptr.h" #include"cmd_context.h" From c980cfd783fd9ff297e7971b695a2e425b6f7d60 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jun 2017 20:51:55 -0700 Subject: [PATCH 27/34] add concat recognizer Signed-off-by: Nikolaj Bjorner --- src/api/java/Expr.java | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 71a2e3e1e..707f3300d 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -1297,6 +1297,15 @@ public class Expr extends AST return Native.getString(getContext().nCtx(), getNativeObject()); } + /** + * Check whether expression is a concatenation + * @return a boolean + */ + public boolean isConcat() + { + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SEQ_CONCAT; + } + /** * Indicates whether the term is a binary equivalence modulo namings. * Remarks: This binary predicate is used in proof terms. It captures From e3f32ca3a8820e4f26615fe366ffc1b96aca9f2a Mon Sep 17 00:00:00 2001 From: "KangJing Huang (Chaserhkj)" Date: Wed, 14 Jun 2017 02:18:21 -0400 Subject: [PATCH 28/34] Fix Z3_PRINT_SMTLIB_FULL not working as expected --- src/api/api_ast.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 3cec4ec02..7342b3c49 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -821,9 +821,13 @@ extern "C" { RESET_ERROR_CODE(); std::ostringstream buffer; switch (mk_c(c)->get_print_mode()) { - case Z3_PRINT_SMTLIB_FULL: - buffer << mk_pp(to_ast(a), mk_c(c)->m()); + case Z3_PRINT_SMTLIB_FULL: { + params_ref p; + p.set_uint("max_depth", 4294967295u); + p.set_uint("min_alias_size", 4294967295u); + buffer << mk_pp(to_ast(a), mk_c(c)->m(), p); break; + } case Z3_PRINT_LOW_LEVEL: buffer << mk_ll_pp(to_ast(a), mk_c(c)->m()); break; @@ -1066,7 +1070,7 @@ extern "C" { case OP_BIT2BOOL: return Z3_OP_BIT2BOOL; case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL; case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL; - case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL; + case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL; case OP_BSDIV_I: return Z3_OP_BSDIV_I; case OP_BUDIV_I: return Z3_OP_BUDIV_I; case OP_BSREM_I: return Z3_OP_BSREM_I; From d8a02bc0400e08786132779d1c81607cbc2109bb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 14 Jun 2017 13:24:54 +0100 Subject: [PATCH 29/34] Fixed AST translation functions in .NET and Java APIs. Fixes #1073. --- examples/dotnet/Program.cs | 27 +++++++++++++++++++++++++++ examples/java/JavaExample.java | 33 +++++++++++++++++++++++++++++---- src/api/dotnet/AST.cs | 16 ++++++++-------- src/api/dotnet/Expr.cs | 24 +++++++++--------------- src/api/dotnet/FuncDecl.cs | 16 +++++----------- src/api/dotnet/Quantifier.cs | 12 +++++++++++- src/api/dotnet/Sort.cs | 20 +++++++++++++++----- src/api/java/AST.java | 4 +--- src/api/java/Expr.java | 9 +-------- src/api/java/FuncDecl.java | 8 +------- src/api/java/Quantifier.java | 13 +++++++++++++ src/api/java/Sort.java | 13 +++++++++++++ 12 files changed, 133 insertions(+), 62 deletions(-) diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 20bb012b1..64149a553 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -2152,6 +2152,31 @@ namespace test_mapi Console.WriteLine("OK, model: {0}", s.Model.ToString()); } + public static void TranslationExample() + { + Context ctx1 = new Context(); + Context ctx2 = new Context(); + + Sort s1 = ctx1.IntSort; + Sort s2 = ctx2.IntSort; + Sort s3 = s1.Translate(ctx2); + + Console.WriteLine(s1 == s2); + Console.WriteLine(s1.Equals(s2)); + Console.WriteLine(s2.Equals(s3)); + Console.WriteLine(s1.Equals(s3)); + + Expr e1 = ctx1.MkIntConst("e1"); + Expr e2 = ctx2.MkIntConst("e1"); + Expr e3 = e1.Translate(ctx2); + + Console.WriteLine(e1 == e2); + Console.WriteLine(e1.Equals(e2)); + Console.WriteLine(e2.Equals(e3)); + Console.WriteLine(e1.Equals(e3)); + } + + static void Main(string[] args) { try @@ -2225,6 +2250,8 @@ namespace test_mapi QuantifierExample4(ctx); } + TranslationExample(); + Log.Close(); if (Log.isOpen()) Console.WriteLine("Log is still open!"); diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 5810dab37..25076e27c 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -281,7 +281,7 @@ class JavaExample } void disprove(Context ctx, BoolExpr f, boolean useMBQI) - throws TestFailedException + throws TestFailedException { BoolExpr[] a = {}; disprove(ctx, f, useMBQI, a); @@ -2279,6 +2279,29 @@ class JavaExample System.out.println(my); } + public void translationExample() { + Context ctx1 = new Context(); + Context ctx2 = new Context(); + + Sort s1 = ctx1.getIntSort(); + Sort s2 = ctx2.getIntSort(); + Sort s3 = s1.translate(ctx2); + + System.out.println(s1 == s2); + System.out.println(s1.equals(s2)); + System.out.println(s2.equals(s3)); + System.out.println(s1.equals(s3)); + + Expr e1 = ctx1.mkIntConst("e1"); + Expr e2 = ctx2.mkIntConst("e1"); + Expr e3 = e1.translate(ctx2); + + System.out.println(e1 == e2); + System.out.println(e1.equals(e2)); + System.out.println(e2.equals(e3)); + System.out.println(e1.equals(e3)); + } + public static void main(String[] args) { JavaExample p = new JavaExample(); @@ -2300,8 +2323,8 @@ class JavaExample HashMap cfg = new HashMap(); cfg.put("model", "true"); Context ctx = new Context(cfg); - - p.optimizeExample(ctx); + + p.optimizeExample(ctx); p.basicTests(ctx); p.castingTest(ctx); p.sudokuExample(ctx); @@ -2355,7 +2378,9 @@ class JavaExample Context ctx = new Context(cfg); p.quantifierExample3(ctx); p.quantifierExample4(ctx); - } + } + + p.translationExample(); Log.close(); if (Log.isOpen()) diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index 2ffaaa661..c7ca1851e 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-16 Notes: - + --*/ using System; @@ -25,7 +25,7 @@ using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// - /// The abstract syntax tree (AST) class. + /// The abstract syntax tree (AST) class. /// [ContractVerification(true)] public class AST : Z3Object, IComparable @@ -35,7 +35,7 @@ namespace Microsoft.Z3 /// /// An AST /// An AST - /// True if and are from the same context + /// True if and are from the same context /// and represent the same sort; false otherwise. public static bool operator ==(AST a, AST b) { @@ -51,7 +51,7 @@ namespace Microsoft.Z3 /// /// An AST /// An AST - /// True if and are not from the same context + /// True if and are not from the same context /// or represent different sorts; false otherwise. public static bool operator !=(AST a, AST b) { @@ -120,12 +120,12 @@ namespace Microsoft.Z3 if (ReferenceEquals(Context, ctx)) return this; else - return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx)); + return Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx)); } /// /// The kind of the AST. - /// + /// public Z3_ast_kind ASTKind { get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); } @@ -224,10 +224,10 @@ namespace Microsoft.Z3 { Native.Z3_dec_ref(ctx.nCtx, obj); } - }; + }; internal override void IncRef(IntPtr o) - { + { // Console.WriteLine("AST IncRef()"); if (Context == null || o == IntPtr.Zero) return; diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 5e0abcb74..6c52b83c8 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -163,13 +163,7 @@ namespace Microsoft.Z3 /// A copy of the term which is associated with new public Expr Translate(Context ctx) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); - - if (ReferenceEquals(Context, ctx)) - return this; - else - return Expr.Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx)); + return (Expr)base.Translate(ctx); } /// @@ -809,7 +803,7 @@ namespace Microsoft.Z3 /// Retrieve string corresponding to string constant. /// /// the expression should be a string constant, (IsString should be true). - public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } } + public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } } /// /// Check whether expression is a concatentation. @@ -828,43 +822,43 @@ namespace Microsoft.Z3 /// /// a Boolean public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } } - + /// /// Check whether expression is a contains. /// /// a Boolean public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } } - + /// /// Check whether expression is an extract. /// /// a Boolean public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } } - + /// /// Check whether expression is a replace. /// /// a Boolean public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } } - + /// /// Check whether expression is an at. /// /// a Boolean - public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } } + public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } } /// /// Check whether expression is a sequence length. /// /// a Boolean public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } } - + /// /// Check whether expression is a sequence index. /// /// a Boolean public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } } - + #endregion diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 345019892..0587a2276 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-16 Notes: - + --*/ using System; @@ -23,7 +23,7 @@ using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// - /// Function declarations. + /// Function declarations. /// [ContractVerification(true)] public class FuncDecl : AST @@ -62,7 +62,7 @@ namespace Microsoft.Z3 /// /// A hash code. - /// + /// public override int GetHashCode() { return base.GetHashCode(); @@ -205,7 +205,7 @@ namespace Microsoft.Z3 } /// - /// Function declarations can have Parameters associated with them. + /// Function declarations can have Parameters associated with them. /// public class Parameter { @@ -322,13 +322,7 @@ namespace Microsoft.Z3 /// A copy of the function declaration which is associated with new public FuncDecl Translate(Context ctx) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); - - if (ReferenceEquals(Context, ctx)) - return this; - else - return new FuncDecl(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx)); + return (FuncDecl) base.Translate(ctx); } diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index eb21ed2b9..eca4e3c7e 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-19 Notes: - + --*/ using System; @@ -157,6 +157,16 @@ namespace Microsoft.Z3 } } + /// + /// Translates (copies) the quantifier to the Context . + /// + /// A context + /// A copy of the quantifier which is associated with + new public Quantifier Translate(Context ctx) + { + return (Quantifier)base.Translate(ctx); + } + #region Internal [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs index e1b8ca1b7..e6f195434 100644 --- a/src/api/dotnet/Sort.cs +++ b/src/api/dotnet/Sort.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-15 Notes: - + --*/ using System; @@ -33,7 +33,7 @@ namespace Microsoft.Z3 /// /// A Sort /// A Sort - /// True if and are from the same context + /// True if and are from the same context /// and represent the same sort; false otherwise. public static bool operator ==(Sort a, Sort b) { @@ -49,7 +49,7 @@ namespace Microsoft.Z3 /// /// A Sort /// A Sort - /// True if and are not from the same context + /// True if and are not from the same context /// or represent different sorts; false otherwise. public static bool operator !=(Sort a, Sort b) { @@ -113,10 +113,20 @@ namespace Microsoft.Z3 return Native.Z3_sort_to_string(Context.nCtx, NativeObject); } + /// + /// Translates (copies) the sort to the Context . + /// + /// A context + /// A copy of the sort which is associated with + new public Sort Translate(Context ctx) + { + return (Sort)base.Translate(ctx); + } + #region Internal /// /// Sort constructor - /// + /// internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } #if DEBUG @@ -154,5 +164,5 @@ namespace Microsoft.Z3 } } #endregion - } + } } diff --git a/src/api/java/AST.java b/src/api/java/AST.java index e1cde837f..350830443 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -87,12 +87,10 @@ public class AST extends Z3Object implements Comparable **/ public AST translate(Context ctx) { - if (getContext() == ctx) { return this; } else { - return new AST(ctx, Native.translate(getContext().nCtx(), - getNativeObject(), ctx.nCtx())); + return create(ctx, Native.translate(getContext().nCtx(), getNativeObject(), ctx.nCtx())); } } diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 707f3300d..6cabbb1b8 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -194,14 +194,7 @@ public class Expr extends AST **/ public Expr translate(Context ctx) { - if (getContext() == ctx) { - return this; - } else { - return Expr.create( - ctx, - Native.translate(getContext().nCtx(), getNativeObject(), - ctx.nCtx())); - } + return (Expr) super.translate(ctx); } /** diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 8b1ad4b44..255bc2c4a 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -68,13 +68,7 @@ public class FuncDecl extends AST **/ public FuncDecl translate(Context ctx) { - - if (getContext() == ctx) { - return this; - } else { - return new FuncDecl(ctx, Native.translate(getContext().nCtx(), - getNativeObject(), ctx.nCtx())); - } + return (FuncDecl) super.translate(ctx); } /** diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index bc2537107..ce2adce21 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -145,6 +145,19 @@ public class Quantifier extends BoolExpr .nCtx(), getNativeObject())); } + /** + * Translates (copies) the quantifier to the Context {@code ctx}. + * + * @param ctx A context + * + * @return A copy of the quantifier which is associated with {@code ctx} + * @throws Z3Exception on error + **/ + public Quantifier translate(Context ctx) + { + return (Quantifier) super.translate(ctx); + } + /** * Create a quantified expression. * diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 0763a69a3..e7a186ad2 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -87,6 +87,19 @@ public class Sort extends AST return Native.sortToString(getContext().nCtx(), getNativeObject()); } + /** + * Translates (copies) the sort to the Context {@code ctx}. + * + * @param ctx A context + * + * @return A copy of the sort which is associated with {@code ctx} + * @throws Z3Exception on error + **/ + public Sort translate(Context ctx) + { + return (Sort) super.translate(ctx); + } + /** * Sort constructor **/ From 8ac43c981a5e88432c0e0127e292ad859fb438f8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Jun 2017 21:40:16 -0700 Subject: [PATCH 30/34] use less memory #1078 --- src/tactic/bv/bv_bounds_tactic.cpp | 78 ++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 1b324b2eb..69575b2dc 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -234,6 +234,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { return false; } +#if 0 expr_set* get_expr_vars(expr* t) { unsigned id = t->get_id(); m_expr_vars.reserve(id + 1); @@ -259,7 +260,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { } return set; } +#endif +#if 0 expr_cnt* get_expr_bounds(expr* t) { unsigned id = t->get_id(); m_bound_exprs.reserve(id + 1); @@ -288,6 +291,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { } return set; } +#endifx public: bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { @@ -392,17 +396,86 @@ public: return result != 0; } + // check if t contains v + ptr_vector todo; + bool contains(expr* t, expr* v) { + ast_fast_mark1 mark; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark.is_marked(t)) { + continue; + } + if (t == v) { + todo.reset(); + return true; + } + mark.mark(t); + + if (!is_app(t)) { + continue; + } + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + bool contains_bound(expr* t) { + ast_fast_mark1 mark1; + ast_fast_mark2 mark2; + + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark1.is_marked(t)) { + continue; + } + mark1.mark(t); + + if (!is_app(t)) { + continue; + } + interval b; + expr* e; + if (is_bound(t, e, b)) { + if (mark2.is_marked(e)) { + todo.reset(); + return true; + } + mark2.mark(e); + if (m_bound.contains(e)) { + todo.reset(); + return true; + } + } + + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + virtual bool may_simplify(expr* t) { if (m_bv.is_numeral(t)) return false; while (m.is_not(t, t)); + for (auto & v : m_bound) { + if (contains(t, v.m_key)) return true; + } + +#if 0 expr_set* used_exprs = get_expr_vars(t); for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { + if (contains(t, I->m_key)) return true; if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) return true; } +#endif expr* t1; interval b; @@ -411,11 +484,16 @@ public: return b.is_full() || m_bound.contains(t1); } + if (contains_bound(t)) { + return true; + } +#if 0 expr_cnt* bounds = get_expr_bounds(t); for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { if (I->m_value > 1 || m_bound.contains(I->m_key)) return true; } +#endif return false; } From d3320f8b8143c64badc1a291fd210bb4aef96693 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Jun 2017 21:48:19 -0700 Subject: [PATCH 31/34] fix build Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/bv_bounds_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 69575b2dc..94c9935b9 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -291,7 +291,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { } return set; } -#endifx +#endif public: bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { From 5be3e959ab66b8d97cc1a53d12cd10077ed6ff6f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Jun 2017 20:46:47 -0700 Subject: [PATCH 32/34] address issues raised in #998 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 4 +++ src/smt/theory_seq.cpp | 57 ++++++++++++++++++++++++++++++++++++++++-- src/smt/theory_seq.h | 5 ++-- 3 files changed, 62 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 9c70f5999..17c3b1b88 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -980,6 +980,10 @@ namespace smt { void push_eq(enode * lhs, enode * rhs, eq_justification const & js) { SASSERT(lhs != rhs); + { + seq_util u(get_manager()); + SASSERT(!u.is_re(lhs->get_owner())); + } m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index af8b9e395..da275de24 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2176,8 +2176,59 @@ bool theory_seq::simplify_and_solve_eqs() { return m_new_propagation || ctx.inconsistent(); } -void theory_seq::internalize_eq_eh(app * atom, bool_var v) {} +void theory_seq::internalize_eq_eh(app * atom, bool_var v) { +} +bool theory_seq::internalize_atom(app* a, bool) { + context & ctx = get_context(); + bool_var bv = ctx.mk_bool_var(a); + ctx.set_var_theory(bv, get_id()); + ctx.mark_as_relevant(bv); + + expr* e1, *e2; + if (m_util.str.is_in_re(a, e1, e2)) { + return internalize_term(to_app(e1)) && internalize_re(e2); + } + if (m_util.str.is_contains(a, e1, e2) || + m_util.str.is_prefix(a, e1, e2) || + m_util.str.is_suffix(a, e1, e2)) { + return internalize_term(to_app(e1)) && internalize_term(to_app(e2)); + } + if (is_accept(a) || is_reject(a) || is_skolem(m_eq, a) || is_step(a) || is_skolem(symbol("seq.is_digit"), a)) { + return true; + } + UNREACHABLE(); + return internalize_term(a); +} + +bool theory_seq::internalize_re(expr* e) { + expr* e1, *e2; + unsigned lc; + if (m_util.re.is_to_re(e, e1)) { + return internalize_term(to_app(e1)); + } + if (m_util.re.is_star(e, e1) || + m_util.re.is_plus(e, e1) || + m_util.re.is_opt(e, e1) || + m_util.re.is_loop(e, e1, lc) || + m_util.re.is_complement(e, e1)) { + return internalize_re(e1); + } + if (m_util.re.is_union(e, e1, e2) || + m_util.re.is_intersection(e, e1, e2) || + m_util.re.is_concat(e, e1, e2)) { + return internalize_re(e1) && internalize_re(e2); + } + if (m_util.re.is_full(e) || + m_util.re.is_empty(e)) { + return true; + } + if (m_util.re.is_range(e, e1, e2)) { + return internalize_term(to_app(e1)) && internalize_term(to_app(e2)); + } + UNREACHABLE(); + return internalize_term(to_app(e)); +} bool theory_seq::internalize_term(app* term) { context & ctx = get_context(); @@ -3875,7 +3926,9 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { enforce_length_coherence(n1, n2); } else if (n1 != n2 && m_util.is_re(n1->get_owner())) { - warning_msg("equality between regular expressions is not yet supported"); + // ignore + UNREACHABLE(); + // eautomaton* a1 = get_automaton(n1->get_owner()); // eautomaton* a2 = get_automaton(n2->get_owner()); // eautomaton* b1 = mk_difference(*a1, *a2); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index e145d3077..5fd31e2ca 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -341,8 +341,8 @@ namespace smt { virtual void init(context* ctx); virtual final_check_status final_check_eh(); - virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); } - virtual bool internalize_term(app*); + virtual bool internalize_atom(app* atom, bool); + virtual bool internalize_term(app*); virtual void internalize_eq_eh(app * atom, bool_var v); virtual void new_eq_eh(theory_var, theory_var); virtual void new_diseq_eh(theory_var, theory_var); @@ -387,6 +387,7 @@ namespace smt { vector const& ll, vector const& rl); bool set_empty(expr* x); bool is_complex(eq const& e); + bool internalize_re(expr* e); bool check_extensionality(); bool check_contains(); From e67572ffa6f9c72d8ff85864c33d26cef16b50a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Jun 2017 20:47:59 -0700 Subject: [PATCH 33/34] address issues raised in #998 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 4 ---- src/smt/theory_seq.cpp | 2 -- 2 files changed, 6 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 17c3b1b88..9c70f5999 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -980,10 +980,6 @@ namespace smt { void push_eq(enode * lhs, enode * rhs, eq_justification const & js) { SASSERT(lhs != rhs); - { - seq_util u(get_manager()); - SASSERT(!u.is_re(lhs->get_owner())); - } m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index da275de24..ec22e8520 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3927,8 +3927,6 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { } else if (n1 != n2 && m_util.is_re(n1->get_owner())) { // ignore - UNREACHABLE(); - // eautomaton* a1 = get_automaton(n1->get_owner()); // eautomaton* a2 = get_automaton(n2->get_owner()); // eautomaton* b1 = mk_difference(*a1, *a2); From 02161f2ff7438d7b293a194675e1fa5fdbedcb7c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Jun 2017 21:13:25 -0700 Subject: [PATCH 34/34] revert internalize logic for re until debugged Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ec22e8520..c98040c17 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2180,6 +2180,8 @@ void theory_seq::internalize_eq_eh(app * atom, bool_var v) { } bool theory_seq::internalize_atom(app* a, bool) { + return internalize_term(a); +#if 0 context & ctx = get_context(); bool_var bv = ctx.mk_bool_var(a); ctx.set_var_theory(bv, get_id()); @@ -2199,11 +2201,12 @@ bool theory_seq::internalize_atom(app* a, bool) { } UNREACHABLE(); return internalize_term(a); +#endif } bool theory_seq::internalize_re(expr* e) { expr* e1, *e2; - unsigned lc; + unsigned lc, uc; if (m_util.re.is_to_re(e, e1)) { return internalize_term(to_app(e1)); } @@ -2211,6 +2214,7 @@ bool theory_seq::internalize_re(expr* e) { m_util.re.is_plus(e, e1) || m_util.re.is_opt(e, e1) || m_util.re.is_loop(e, e1, lc) || + m_util.re.is_loop(e, e1, lc, uc) || m_util.re.is_complement(e, e1)) { return internalize_re(e1); } @@ -3013,6 +3017,7 @@ void theory_seq::deque_axiom(expr* n) { add_length_axiom(n); } else if (m_util.str.is_empty(n) && !has_length(n) && !m_length.empty()) { + ensure_enode(n); enforce_length(get_context().get_enode(n)); } else if (m_util.str.is_index(n)) { @@ -4046,7 +4051,7 @@ void theory_seq::relevant_eh(app* n) { } expr* arg; - if (m_util.str.is_length(n, arg) && !has_length(arg)) { + if (m_util.str.is_length(n, arg) && !has_length(arg) && get_context().e_internalized(arg)) { enforce_length(get_context().get_enode(arg)); } }