From 52e0f3b539847ecc78eb53e8350b5e41bcb04149 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Jun 2017 09:10:49 -0700 Subject: [PATCH 01/63] add string accessors to managed APIs #1051 Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Expr.cs | 16 +++++++++++++++ src/api/java/Expr.java | 20 +++++++++++++++++++ src/smt/theory_str.cpp | 44 +++++++++++------------------------------- src/smt/theory_str.h | 6 +++--- 4 files changed, 50 insertions(+), 36 deletions(-) diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index cac62d2f0..23ffe61bd 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -797,6 +797,22 @@ namespace Microsoft.Z3 public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } } #endregion + #region Sequences and Strings + + /// + /// Check whether expression is a string constant. + /// + /// a Boolean + public bool IsString { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } } + + /// + /// 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); } } + + #endregion + #region Proof Terms /// /// Indicates whether the term is a binary equivalence modulo namings. diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index ef86f510a..71a2e3e1e 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -1277,6 +1277,26 @@ public class Expr extends AST return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT; } + /** + * Check whether expression is a string constant. + * @return a boolean + */ + public boolean isString() + { + return isApp() && Native.isString(getContext().nCtx(), getNativeObject()); + } + + /** + * Retrieve string corresponding to string constant. + * Remark: the expression should be a string constant, (isString() should return true). + * @throws Z3Exception on error + * @return a string + */ + public String getString() + { + return Native.getString(getContext().nCtx(), getNativeObject()); + } + /** * Indicates whether the term is a binary equivalence modulo namings. * Remarks: This binary predicate is used in proof terms. It captures diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index c3e924f18..ddb54fbc6 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -25,6 +25,7 @@ #include #include"theory_seq_empty.h" #include"theory_arith.h" +#include"ast_util.h" namespace smt { @@ -98,7 +99,8 @@ namespace smt { if (defaultCharset) { // valid C strings can't contain the null byte ('\0') charSetSize = 255; - char_set = alloc_svect(char, charSetSize); + char_set.resize(256, 0); + charSetLookupTable.resize(256, 0); int idx = 0; // small letters for (int i = 97; i < 123; i++) { @@ -157,8 +159,8 @@ namespace smt { } else { const char setset[] = { 'a', 'b', 'c' }; int fSize = sizeof(setset) / sizeof(char); - - char_set = alloc_svect(char, fSize); + char_set.resize(fSize, 0); + charSetLookupTable.resize(fSize, 0); charSetSize = fSize; for (int i = 0; i < charSetSize; i++) { char_set[i] = setset[i]; @@ -9123,7 +9125,7 @@ namespace smt { zstring theory_str::gen_val_string(int len, int_vector & encoding) { SASSERT(charSetSize > 0); - SASSERT(char_set != NULL); + SASSERT(!char_set.empty()); std::string re(len, char_set[0]); for (int i = 0; i < (int) encoding.size() - 1; i++) { @@ -9240,8 +9242,7 @@ namespace smt { // ---------------------------------------------------------------------------------------- - ptr_vector orList; - ptr_vector andList; + expr_ref_vector orList(m), andList(m); for (long long i = l; i < h; i++) { orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) )); @@ -9262,7 +9263,7 @@ namespace smt { } else { strAst = mk_string(aStr); } - andList.push_back(m.mk_eq(orList[orList.size() - 1], m.mk_eq(freeVar, strAst))); + andList.push_back(m.mk_eq(orList[orList.size() - 1].get(), m.mk_eq(freeVar, strAst))); } if (!coverAll) { orList.push_back(m.mk_eq(val_indicator, mk_string("more"))); @@ -9273,21 +9274,8 @@ namespace smt { } } - expr ** or_items = alloc_svect(expr*, orList.size()); - expr ** and_items = alloc_svect(expr*, andList.size() + 1); - - for (int i = 0; i < (int) orList.size(); i++) { - or_items[i] = orList[i]; - } - if (orList.size() > 1) - and_items[0] = m.mk_or(orList.size(), or_items); - else - and_items[0] = or_items[0]; - - for (int i = 0; i < (int) andList.size(); i++) { - and_items[i + 1] = andList[i]; - } - expr * valTestAssert = m.mk_and(andList.size() + 1, and_items); + andList.push_back(mk_or(orList)); + expr_ref valTestAssert = mk_and(andList); // --------------------------------------- // If the new value tester is $$_val_x_16_i @@ -9300,17 +9288,7 @@ namespace smt { if (vTester != val_indicator) andList.push_back(m.mk_eq(vTester, mk_string("more"))); } - expr * assertL = NULL; - if (andList.size() == 1) { - assertL = andList[0]; - } else { - expr ** and_items = alloc_svect(expr*, andList.size()); - for (int i = 0; i < (int) andList.size(); i++) { - and_items[i] = andList[i]; - } - assertL = m.mk_and(andList.size(), and_items); - } - + expr_ref assertL = mk_and(andList); // (assertL => valTestAssert) <=> (!assertL OR valTestAssert) valTestAssert = m.mk_or(m.mk_not(assertL), valTestAssert); return valTestAssert; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 4752e8a1b..c56ea8ba2 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -330,9 +330,9 @@ protected: std::map regex_nfa_cache; // Regex term --> NFA - char * char_set; - std::map charSetLookupTable; - int charSetSize; + svector char_set; + svector charSetLookupTable; + int charSetSize; obj_pair_map concat_astNode_map; From fda59f5a242165948403bcfc11091e3f39d7ac4e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Jun 2017 09:32:17 -0700 Subject: [PATCH 02/63] expose operator kinds for internal functions using their sequence variants. Issue #1051 Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index c9cdc6ab3..3cec4ec02 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1124,6 +1124,20 @@ extern "C" { case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; + case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE; + case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT; + case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH; + case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS; + case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX; + case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX; + case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE; + case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE; + case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT; + case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT; + case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX; + case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET; + case _OP_REGEXP_FULL: return Z3_OP_RE_FULL_SET; + case OP_STRING_STOI: return Z3_OP_STR_TO_INT; case OP_STRING_ITOS: return Z3_OP_INT_TO_STR; From e9ed3af45587900ea179d0393635a0509a5669dc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Jun 2017 09:35:35 -0700 Subject: [PATCH 03/63] fix regression in str Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 2 -- src/smt/theory_str.h | 2 +- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 156e097fe..c2171b9bf 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -100,7 +100,6 @@ namespace smt { // valid C strings can't contain the null byte ('\0') charSetSize = 255; char_set.resize(256, 0); - charSetLookupTable.resize(256, 0); int idx = 0; // small letters for (int i = 97; i < 123; i++) { @@ -160,7 +159,6 @@ namespace smt { const char setset[] = { 'a', 'b', 'c' }; int fSize = sizeof(setset) / sizeof(char); char_set.resize(fSize, 0); - charSetLookupTable.resize(fSize, 0); charSetSize = fSize; for (int i = 0; i < charSetSize; i++) { char_set[i] = setset[i]; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index c56ea8ba2..ae659f0f0 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -331,7 +331,7 @@ protected: std::map regex_nfa_cache; // Regex term --> NFA svector char_set; - svector charSetLookupTable; + std::map charSetLookupTable; int charSetSize; obj_pair_map concat_astNode_map; From 2908ab40693aa96c0ae7175d4086b518753420e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Jun 2017 09:56:25 -0700 Subject: [PATCH 04/63] fix reference count issue with pinning to expr_ref Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 14 ++++++-------- src/smt/theory_str.h | 2 +- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index c2171b9bf..d560a54a1 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6927,9 +6927,9 @@ namespace smt { ast_manager & m = get_manager(); if (lenTester_fvar_map.contains(lenTester)) { expr * fVar = lenTester_fvar_map[lenTester]; - expr * toAssert = gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue); + expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m); TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); - if (toAssert != NULL) { + if (toAssert) { assert_axiom(toAssert); } } @@ -9173,7 +9173,7 @@ namespace smt { } } - expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, + expr* theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, zstring lenStr, int tries) { ast_manager & m = get_manager(); context & ctx = get_context(); @@ -9288,8 +9288,7 @@ namespace smt { } expr_ref assertL = mk_and(andList); // (assertL => valTestAssert) <=> (!assertL OR valTestAssert) - valTestAssert = m.mk_or(m.mk_not(assertL), valTestAssert); - return valTestAssert; + return m.mk_or(m.mk_not(assertL), valTestAssert); } expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, @@ -9354,7 +9353,7 @@ namespace smt { << " doesn't have an equivalence class value." << std::endl;); refresh_theory_var(aTester); - expr * makeupAssert = gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i); + expr_ref makeupAssert(gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i), m); TRACE("str", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl << mk_ismt2_pp(makeupAssert, m) << std::endl;); @@ -9376,8 +9375,7 @@ namespace smt { fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester)); print_value_tester_list(fvar_valueTester_map[freeVar][len]); } - expr * nextAssert = gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1); - return nextAssert; + return gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1); } return NULL; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index ae659f0f0..0bbc44ab8 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -553,7 +553,7 @@ protected: expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries); expr * gen_free_var_options(expr * freeVar, expr * len_indicator, zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr); - expr * gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, + expr* gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, zstring lenStr, int tries); void print_value_tester_list(svector > & testerList); bool get_next_val_encode(int_vector & base, int_vector & next); From efd5727676e8475c053a42661758a6b96d268a10 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Jun 2017 10:35:09 -0700 Subject: [PATCH 05/63] 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 06/63] 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 07/63] 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 08/63] 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 09/63] 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 10/63] [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 11/63] [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 12/63] [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 13/63] 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 14/63] 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 15/63] 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 16/63] 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 17/63] [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 18/63] 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 19/63] 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 20/63] [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 21/63] [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 22/63] [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 23/63] [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 24/63] 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 25/63] 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 26/63] 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 27/63] 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 28/63] 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 29/63] 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 30/63] 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 31/63] 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 32/63] 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 33/63] 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 34/63] 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 35/63] 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 36/63] 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 37/63] 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 38/63] 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)); } } From e547000bcfd45b62ac33512560212370c0712f52 Mon Sep 17 00:00:00 2001 From: Dennis Yurichev Date: Mon, 19 Jun 2017 13:52:30 +0300 Subject: [PATCH 39/63] typo --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 84a80ddf7..4234439d0 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -314,7 +314,7 @@ class AstRef(Z3PPObject): raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.") def sexpr(self): - """Return an string representing the AST node in s-expression notation. + """Return a string representing the AST node in s-expression notation. >>> x = Int('x') >>> ((x + 1)*x).sexpr() From 894c60bdf90841c2af9c73897232027e9a94ead9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Jun 2017 18:22:30 -0500 Subject: [PATCH 40/63] fix bug in qe-lite reported in #1086: bookkeeping of unconstrained variables only works for quantifier-free formulas Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 1 + src/qe/qe_lite.cpp | 7 ++++++- src/smt/theory_seq.cpp | 8 ++++++-- 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 7342b3c49..d34cad2f4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -558,6 +558,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_sort(c, a); RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, 0); Z3_sort r = of_sort(mk_c(c)->m().get_sort(to_expr(a))); RETURN_Z3(r); Z3_CATCH_RETURN(0); diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index eccc2d0c7..0e7db9971 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -1491,8 +1491,10 @@ namespace fm { unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { expr * f = g[i]; - if (is_occ(f)) + if (is_occ(f)) { + TRACE("qe_lite", tout << "OCC: " << mk_ismt2_pp(f, m) << "\n";); continue; + } TRACE("qe_lite", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";); quick_for_each_expr(proc, visited, f); } @@ -2221,6 +2223,9 @@ namespace fm { void operator()(expr_ref_vector& fmls) { init(fmls); init_use_list(fmls); + for (auto & f : fmls) { + if (has_quantifiers(f)) return; + } if (m_inconsistent) { m_new_fmls.reset(); m_new_fmls.push_back(m.mk_false()); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c98040c17..3b70e1426 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2180,8 +2180,12 @@ 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 + return internalize_term(a); +#else + if (is_skolem(m_eq, a)) { + return internalize_term(a); + } context & ctx = get_context(); bool_var bv = ctx.mk_bool_var(a); ctx.set_var_theory(bv, get_id()); @@ -2196,7 +2200,7 @@ bool theory_seq::internalize_atom(app* a, bool) { 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)) { + if (is_accept(a) || is_reject(a) || is_step(a) || is_skolem(symbol("seq.is_digit"), a)) { return true; } UNREACHABLE(); From f375016a11cd97d64de8ed35bd15def6aec4a162 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Jun 2017 18:23:27 -0500 Subject: [PATCH 41/63] disable tweak to seq until there are cycles to test further Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 3b70e1426..4dfff21c2 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2180,7 +2180,7 @@ void theory_seq::internalize_eq_eh(app * atom, bool_var v) { } bool theory_seq::internalize_atom(app* a, bool) { -#if 0 +#if 1 return internalize_term(a); #else if (is_skolem(m_eq, a)) { From 7b976883020cdf23e0181369744a5f69dbdf4d85 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jun 2017 14:36:40 +0100 Subject: [PATCH 42/63] Whitespace, typo. --- src/cmd_context/basic_cmds.cpp | 106 ++++++++++++++++----------------- 1 file changed, 53 insertions(+), 53 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index f6eea729f..563d44afa 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -39,7 +39,7 @@ class help_cmd : public cmd { ctx.regular_stream() << " (" << s; if (usage) ctx.regular_stream() << " " << escaped(usage, true) << ")\n"; - else + else ctx.regular_stream() << ")\n"; if (descr) { ctx.regular_stream() << " " << escaped(descr, true, 4) << "\n"; @@ -62,7 +62,7 @@ public: } m_cmds.push_back(s); } - + typedef std::pair named_cmd; struct named_cmd_lt { bool operator()(named_cmd const & c1, named_cmd const & c2) const { return c1.first.str() < c2.first.str(); } @@ -104,14 +104,14 @@ class get_model_cmd : public cmd { unsigned m_index; public: get_model_cmd(): cmd("get-model"), m_index(0) {} - virtual char const * get_usage() const { return "[]"; } - virtual char const * get_descr(cmd_context & ctx) const { - return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective"; + virtual char const * get_usage() const { return "[]"; } + virtual char const * get_descr(cmd_context & ctx) const { + return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective"; } - virtual unsigned get_arity() const { return VAR_ARITY; } + virtual unsigned get_arity() const { return VAR_ARITY; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; } - virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; } - virtual void execute(cmd_context & ctx) { + virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; } + virtual void execute(cmd_context & ctx) { if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) throw cmd_exception("model is not available"); model_ref m; @@ -122,7 +122,7 @@ public: ctx.get_check_sat_result()->get_model(m); } ctx.display_model(m); - } + } virtual void reset(cmd_context& ctx) { m_index = 0; } @@ -167,11 +167,11 @@ class cmd_is_declared : public ast_smt_pp::is_declared { cmd_context& m_ctx; public: cmd_is_declared(cmd_context& ctx): m_ctx(ctx) {} - - virtual bool operator()(func_decl* d) const { + + virtual bool operator()(func_decl* d) const { return m_ctx.is_func_decl(d->get_name()); } - virtual bool operator()(sort* s) const { + virtual bool operator()(sort* s) const { return m_ctx.is_sort_decl(s->get_name()); } }; @@ -189,13 +189,13 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) { throw cmd_exception("proof is not well sorted"); } - + pp_params params; if (params.pretty_proof()) { ctx.regular_stream() << mk_pp(pr, ctx.m()) << std::endl; } else { - // TODO: reimplement a new SMT2 pretty printer + // TODO: reimplement a new SMT2 pretty printer ast_smt_pp pp(ctx.m()); cmd_is_declared isd(ctx); pp.set_is_declared(&isd); @@ -206,19 +206,19 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { }); 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; + 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", { @@ -260,7 +260,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(); ctx.print_success();); -UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", CPK_SYMBOL, symbol const &, +UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", CPK_SYMBOL, symbol const &, if (ctx.set_logic(arg)) ctx.print_success(); else { @@ -269,9 +269,9 @@ UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", C } ); -UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr *, { +UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr *, { ctx.display(ctx.regular_stream(), arg); - ctx.regular_stream() << std::endl; + ctx.regular_stream() << std::endl; }); UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << "\"" << arg << "\"" << std::endl;); @@ -305,18 +305,18 @@ protected: symbol m_reproducible_resource_limit; bool is_builtin_option(symbol const & s) const { - return - s == m_print_success || s == m_print_warning || s == m_expand_definitions || + return + s == m_print_success || s == m_print_warning || s == m_expand_definitions || s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_unsat_assumptions || s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants || - s == m_regular_output_channel || s == m_diagnostic_output_channel || + s == m_regular_output_channel || s == m_diagnostic_output_channel || s == m_random_seed || s == m_verbosity || s == m_global_decls || s == m_global_declarations || s == m_produce_assertions || s == m_reproducible_resource_limit; } public: set_get_option_cmd(char const * name): - cmd(name), + cmd(name), m_true("true"), m_false("false"), m_print_success(":print-success"), @@ -348,7 +348,7 @@ public: class set_option_cmd : public set_get_option_cmd { bool m_unsupported; symbol m_option; - + bool to_bool(symbol const & value) const { if (value != m_true && value != m_false) throw cmd_exception("invalid option value, true/false expected"); @@ -369,7 +369,7 @@ class set_option_cmd : public set_get_option_cmd { throw cmd_exception(msg); } } - + void set_param(cmd_context & ctx, char const * value) { try { gparams::set(m_option, value); @@ -466,11 +466,11 @@ public: virtual void prepare(cmd_context & ctx) { m_unsupported = false; m_option = symbol::null; } - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return m_option == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE; } - virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { + virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { if (m_option == symbol::null) { m_option = opt; } @@ -525,7 +525,7 @@ class get_option_cmd : public set_get_option_cmd { static void print_bool(cmd_context & ctx, bool b) { ctx.regular_stream() << (b ? "true" : "false") << std::endl; } - + static void print_unsigned(cmd_context & ctx, unsigned v) { ctx.regular_stream() << v << std::endl; } @@ -542,11 +542,11 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "get configuration option."; } virtual unsigned get_arity() const { return 1; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; } - virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { + virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { if (opt == m_print_success) { - print_bool(ctx, ctx.print_success_enabled()); + print_bool(ctx, ctx.print_success_enabled()); } - // TODO: + // TODO: // else if (opt == m_print_warning) { // print_bool(ctx, ); // } @@ -636,7 +636,7 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "get information."; } virtual unsigned get_arity() const { return 1; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; } - virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { + virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { if (opt == m_error_behavior) { if (ctx.exit_on_error()) ctx.regular_stream() << "(:error-behavior immediate-exit)" << std::endl; @@ -692,12 +692,12 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "set information."; } virtual unsigned get_arity() const { return 2; } virtual void prepare(cmd_context & ctx) { m_info = symbol::null; } - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { - return m_info == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE; + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { + return m_info == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE; } virtual void set_next_arg(cmd_context & ctx, rational const & val) {} virtual void set_next_arg(cmd_context & ctx, char const * val) {} - virtual void set_next_arg(cmd_context & ctx, symbol const & s) { + virtual void set_next_arg(cmd_context & ctx, symbol const & s) { if (m_info == symbol::null) { m_info = s; } @@ -745,7 +745,7 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "declare a new array map operator with name using the given function declaration.\n ::= \n | ( (*) )\n | ((_ +) (*) )\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; } virtual unsigned get_arity() const { return 3; } virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_domain.reset(); } - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { if (m_name == symbol::null) return CPK_SYMBOL; if (m_domain.empty()) return CPK_SORT_LIST; return CPK_FUNC_DECL; @@ -756,10 +756,10 @@ public: throw cmd_exception("invalid map declaration, empty sort list"); m_domain.append(num, slist); } - virtual void set_next_arg(cmd_context & ctx, func_decl * f) { - m_f = f; - if (m_f->get_arity() == 0) - throw cmd_exception("invalid map declaration, function declaration must have arity > 0"); + virtual void set_next_arg(cmd_context & ctx, func_decl * f) { + m_f = f; + if (m_f->get_arity() == 0) + throw cmd_exception("invalid map declaration, function declaration must have arity > 0"); } virtual void reset(cmd_context & ctx) { m_array_fid = null_family_id; @@ -798,7 +798,7 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "retrieve consequences that fix values for supplied variables"; } virtual unsigned get_arity() const { return 2; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR_LIST; } - virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) { + virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) { if (m_count == 0) { m_assumptions.append(num, tlist); ++m_count; @@ -858,7 +858,7 @@ void install_basic_cmds(cmd_context & ctx) { ctx.insert(alloc(builtin_cmd, "declare-fun", " (*) ", "declare a new function/constant.")); ctx.insert(alloc(builtin_cmd, "declare-const", " ", "declare a new constant.")); ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(*) (+)", "declare mutually recursive datatypes.\n ::= ( +)\n ::= ( *)\n ::= ( )\nexample: (declare-datatypes (T) ((BinTree (leaf (value T)) (node (left BinTree) (right BinTree)))))")); - ctx.insert(alloc(builtin_cmd, "check-sat-asuming", "( hprop_literali* )", "check sat assuming a collection of literals")); + ctx.insert(alloc(builtin_cmd, "check-sat-assuming", "( hprop_literali* )", "check sat assuming a collection of literals")); ctx.insert(alloc(get_unsat_assumptions_cmd)); ctx.insert(alloc(reset_assertions_cmd)); From 054e139c0d9fded534ae8ef3596b279bc25d9f7b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jun 2017 14:37:26 +0100 Subject: [PATCH 43/63] Whitespace --- src/parsers/smt2/smt2scanner.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index fb2f9f34a..1763a4fa5 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -23,7 +23,7 @@ namespace smt2 { void scanner::next() { if (m_cache_input) - m_cache.push_back(m_curr); + m_cache.push_back(m_curr); SASSERT(!m_at_eof); if (m_interactive) { m_curr = m_stream.get(); @@ -293,11 +293,11 @@ namespace smt2 { } scanner::token scanner::scan() { - while (true) { + while (true) { signed char c = curr(); m_pos = m_spos; - if (m_at_eof) + if (m_at_eof) return EOF_TOKEN; switch (m_normalized[(unsigned char) c]) { From ab21caf55f52928b1a3cbaf927bcdd6fd73d92bd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jun 2017 14:39:22 +0100 Subject: [PATCH 44/63] Reverted fix for quoted echo strings when smtlib2_compliant=false. Kindly reported by Armael Gueneau. Fixes #1062. --- src/cmd_context/basic_cmds.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 563d44afa..e915b7b4e 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -274,7 +274,10 @@ 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(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr *, { + ctx.display(ctx.regular_stream(), arg); + ctx.regular_stream() << std::endl; +}); class set_get_option_cmd : public cmd { From a0b25147d9a1ead8bc0c5949a04ff6ffef67be93 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jun 2017 14:48:03 +0100 Subject: [PATCH 45/63] Fix for the fix for #1062. --- src/cmd_context/basic_cmds.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index e915b7b4e..ea6d1c232 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -274,10 +274,9 @@ UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr ctx.regular_stream() << std::endl; }); -UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr *, { - ctx.display(ctx.regular_stream(), arg); - ctx.regular_stream() << std::endl; -}); +UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, + bool smt2c = ctx.params().m_smtlib2_compliant; + ctx.regular_stream() << (smt2c ? "\"" : "") << arg << (smt2c ? "\"" : "") << std::endl;); class set_get_option_cmd : public cmd { From ee2fc41626d61d48afea8b3e14e2fe7169f6fc35 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jun 2017 15:17:49 +0100 Subject: [PATCH 46/63] Kick CI From 237e6dcd3f06e9804d5f1b876a9c79633a52447a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jun 2017 17:21:24 +0100 Subject: [PATCH 47/63] Kick CI From 78e8e8b89345417fd1209eee3c3b87504e34ae12 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jun 2017 18:06:18 +0100 Subject: [PATCH 48/63] Kick CI From 0fa6274a65b667af4d81a93396c4ce238d197626 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Jun 2017 14:18:43 -0700 Subject: [PATCH 49/63] Fix bug #1079, integrality testing seems to have been wrong Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 4 +++- src/smt/theory_arith_aux.h | 7 ++++--- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index f7936eacd..5fbdb2477 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1034,8 +1034,10 @@ namespace smt { lbool val = get_assignment(curr); switch(val) { case l_false: + TRACE("simplify_aux_clause_literals", display_literal(tout << get_assign_level(curr) << " " << get_scope_level() << " ", curr); tout << "\n"; ); simp_lits.push_back(~curr); - break; // ignore literal + break; // ignore literal + // fall through case l_undef: if (curr == ~prev) return false; // clause is equivalent to true diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 54b617152..670121328 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1412,7 +1412,7 @@ namespace smt { << "max gain: " << max_gain << "\n";); - SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); + SASSERT(max_gain.is_minu SASSERT(min_gain.is_minus_one() || min_gain.is_one()); SASSERT(is_int(x) == min_gain.is_one()); @@ -1458,7 +1458,7 @@ namespace smt { normalize_gain(min_gain.get_rational(), max_gain); } - if (is_int(x_i) && !max_gain.is_rational()) { + if (is_int(x_i) && !max_gain.is_int()) { max_gain = inf_numeral(floor(max_gain)); normalize_gain(min_gain.get_rational(), max_gain); } @@ -1483,7 +1483,7 @@ namespace smt { } } TRACE("opt", - tout << "v" << x_i << " a_ij " << a_ij << " " + tout << "v" << x_i << (is_int(x_i)?" int":" real") << " a_ij " << a_ij << " " << "min gain: " << min_gain << " " << "max gain: " << max_gain << " tighter: " << (is_tighter?"true":"false") << "\n";); @@ -1696,6 +1696,7 @@ namespace smt { if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; tout << "value x_j: " << get_value(x_j) << "\n"; ); + pivot(x_i, x_j, a_ij, false); SASSERT(is_non_base(x_i)); From 0ef14acf2e456475898b79866113d76556693f70 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Jun 2017 14:25:56 -0700 Subject: [PATCH 50/63] fix build break Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 670121328..679358932 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1412,7 +1412,7 @@ namespace smt { << "max gain: " << max_gain << "\n";); - SASSERT(max_gain.is_minu + SASSERT(max_gain.is_minus_one() || max_gain.is_one()); SASSERT(min_gain.is_minus_one() || min_gain.is_one()); SASSERT(is_int(x) == min_gain.is_one()); From e48e7ef7be6ecf1c9f5b58544f8b3a8e702e910d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Jun 2017 14:37:56 -0700 Subject: [PATCH 51/63] fix assertion, start addressing #1087 by using size_t --- src/smt/theory_arith_aux.h | 2 +- src/smt/theory_str.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 679358932..f94de7eba 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1412,7 +1412,7 @@ namespace smt { << "max gain: " << max_gain << "\n";); - SASSERT(max_gain.is_minus_one() || max_gain.is_one()); + SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); SASSERT(min_gain.is_minus_one() || min_gain.is_one()); SASSERT(is_int(x) == min_gain.is_one()); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index d560a54a1..523e087f2 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -9194,7 +9194,7 @@ namespace smt { // ---------------------------------------------------------------------------------------- int len = atoi(lenStr.encode().c_str()); bool coverAll = false; - vector options; + vector options; int_vector base; TRACE("str", tout From 69a3e984aa12aaaaa7a1318aad7913dbb035313d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:09:33 -0400 Subject: [PATCH 52/63] add is_hypothesis() method --- src/ast/ast.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ast/ast.h b/src/ast/ast.h index 6bb3b01c9..475e58ac7 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2082,6 +2082,7 @@ public: bool is_undef_proof(expr const * e) const { return e == m_undef_proof; } bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); } + bool is_hypothesis (expr const *e) const {return is_app_of (e, m_basic_family_id, PR_HYPOTHESIS);} bool is_goal(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_GOAL); } bool is_modus_ponens(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_MODUS_PONENS); } bool is_reflexivity(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_REFLEXIVITY); } @@ -2112,6 +2113,7 @@ public: bool is_skolemize(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_SKOLEMIZE); } MATCH_UNARY(is_asserted); + MATCH_UNARY(is_hypothesis); MATCH_UNARY(is_lemma); bool has_fact(proof const * p) const { From e9100854b9c0980b3aad2408e285b572b6448868 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:09:57 -0400 Subject: [PATCH 53/63] ensure that variable names are properly quoted --- src/ast/ast_smt2_pp.cpp | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 89af8bd3e..d5e46548a 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -557,7 +557,14 @@ class smt2_printer { format * f; if (v->get_idx() < m_var_names.size()) { symbol s = m_var_names[m_var_names.size() - v->get_idx() - 1]; - f = mk_string(m(), s.str().c_str()); + std::string vname; + if (is_smt2_quoted_symbol (s)) { + vname = mk_smt2_quoted_symbol (s); + } + else { + vname = s.str(); + } + f = mk_string(m(), vname.c_str ()); } else { // fallback... it is not supposed to happen when the printer is correctly used. @@ -884,7 +891,14 @@ class smt2_printer { symbol * it = m_var_names.end() - num_decls; for (unsigned i = 0; i < num_decls; i++, it++) { format * fs[1] = { m_env.pp_sort(q->get_decl_sort(i)) }; - buf.push_back(mk_seq1(m(), fs, fs+1, f2f(), it->str().c_str())); + std::string var_name; + if (is_smt2_quoted_symbol (*it)) { + var_name = mk_smt2_quoted_symbol (*it); + } + else { + var_name = it->str ();\ + } + buf.push_back(mk_seq1(m(), fs, fs+1, f2f(), var_name.c_str ())); } return mk_seq5(m(), buf.begin(), buf.end(), f2f()); } From 6eced8836d86d39bf1d26dc5137f13f5fa0de19e Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:10:22 -0400 Subject: [PATCH 54/63] expose iterators in expr_map --- src/ast/expr_map.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/ast/expr_map.h b/src/ast/expr_map.h index ddd94ea13..2b49a4a30 100644 --- a/src/ast/expr_map.h +++ b/src/ast/expr_map.h @@ -35,6 +35,13 @@ class expr_map { obj_map m_expr2expr; obj_map m_expr2pr; public: + typedef obj_map Map; + typedef Map::iterator iterator; + typedef Map::key key; + typedef Map::value value; + typedef Map::data data; + typedef Map::entry entry; + expr_map(ast_manager & m); expr_map(ast_manager & m, bool store_proofs); ~expr_map(); @@ -44,6 +51,8 @@ public: void erase(expr * k); void reset(); void flush(); + iterator begin () const { return m_expr2expr.begin (); } + iterator end () const {return m_expr2expr.end (); } void set_store_proofs(bool f) { if (m_store_proofs != f) flush(); m_store_proofs = f; From f3019a3de964a9e7af6f3bcc9224220647be0d08 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:52:06 -0400 Subject: [PATCH 55/63] api to accumulate stopwatches --- src/util/stopwatch.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index b1f6bba03..7a9066030 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -43,6 +43,8 @@ public: } ~stopwatch() {}; + + void add (const stopwatch &s) {/* TODO */} void reset() { m_elapsed.QuadPart = 0; } @@ -90,6 +92,8 @@ public: ~stopwatch() {} + void add (const stopwatch &s) {m_time += s.m_time;} + void reset() { m_time = 0ull; } @@ -141,6 +145,8 @@ public: ~stopwatch() {} + void add (const stopwatch &s) {m_time += s.m_time;} + void reset() { m_time = 0ull; } From 372e8b3c4910954d4df1e466a2000aca7a9b3df0 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:53:04 -0400 Subject: [PATCH 56/63] expose iterator api of obj_hashtable --- src/util/obj_hashtable.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 383ecaeb3..2720f1b00 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -70,6 +70,7 @@ public: m_value(v) { } Value const & get_value() const { return m_value; } + Key & get_key () const { return *m_key; } unsigned hash() const { return m_key->hash(); } bool operator==(key_data const & other) const { return m_key == other.m_key; } }; @@ -100,6 +101,8 @@ public: m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY) {} typedef typename table::iterator iterator; + typedef typename table::data data; + typedef typename table::entry entry; typedef Key key; typedef Value value; From 625874e66fde340fe9ba1399df43b3788026828e Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:54:43 -0400 Subject: [PATCH 57/63] remove debug code --- src/tactic/core/blast_term_ite_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index ea59641c9..483b59776 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -62,14 +62,14 @@ class blast_term_ite_tactic : public tactic { for (unsigned i = 0; i < num_args; ++i) { expr* c, *t, *e; if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) { - enable_trace("blast_term_ite"); + // enable_trace("blast_term_ite"); TRACE("blast_term_ite", result = m.mk_app(f, num_args, args); tout << result << "\n";); expr_ref e1(m), e2(m); ptr_vector args1(num_args, args); args1[i] = t; ++m_num_fresh; e1 = m.mk_app(f, num_args, args1.c_ptr()); - if (t == e) { + if (m.are_equal(t,e)) { result = e1; return BR_REWRITE1; } From ac6ca4d334ae957759c911cacb5eeb37b0100309 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 21:34:49 -0400 Subject: [PATCH 58/63] factored out is_variable_proc to a header file --- src/qe/qe_lite.cpp | 39 +--------------------------- src/qe/qe_vartest.h | 63 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 64 insertions(+), 38 deletions(-) create mode 100644 src/qe/qe_vartest.h diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 0e7db9971..62f6c41a6 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -36,44 +36,7 @@ Revision History: #include "cooperate.h" #include "datatype_decl_plugin.h" -class is_variable_proc { -public: - virtual bool operator()(expr* e) const = 0; -}; - -class is_variable_test : public is_variable_proc { - enum is_var_kind { BY_VAR_SET, BY_VAR_SET_COMPLEMENT, BY_NUM_DECLS }; - uint_set m_var_set; - unsigned m_num_decls; - is_var_kind m_var_kind; -public: - is_variable_test(uint_set const& vars, bool index_of_bound) : - m_var_set(vars), - m_num_decls(0), - m_var_kind(index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT) {} - - is_variable_test(unsigned num_decls) : - m_num_decls(num_decls), - m_var_kind(BY_NUM_DECLS) {} - - virtual bool operator()(expr* e) const { - if (!is_var(e)) { - return false; - } - unsigned idx = to_var(e)->get_idx(); - switch(m_var_kind) { - case BY_VAR_SET: - return m_var_set.contains(idx); - case BY_VAR_SET_COMPLEMENT: - return !m_var_set.contains(idx); - case BY_NUM_DECLS: - return idx < m_num_decls; - } - UNREACHABLE(); - return false; - } -}; - +#include "qe_vartest.h" namespace eq { class der { diff --git a/src/qe/qe_vartest.h b/src/qe/qe_vartest.h new file mode 100644 index 000000000..b2b4be649 --- /dev/null +++ b/src/qe/qe_vartest.h @@ -0,0 +1,63 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + qe_vartest.h + +Abstract: + + Utilities for quantifiers. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-08-28 + +Revision History: + +--*/ +#ifndef QE_VARTEST_H_ +#define QE_VARTEST_H_ + +#include "ast.h" +#include "uint_set.h" + +class is_variable_proc { +public: + virtual bool operator()(expr* e) const = 0; +}; + +class is_variable_test : public is_variable_proc { + enum is_var_kind { BY_VAR_SET, BY_VAR_SET_COMPLEMENT, BY_NUM_DECLS }; + uint_set m_var_set; + unsigned m_num_decls; + is_var_kind m_var_kind; +public: + is_variable_test(uint_set const& vars, bool index_of_bound) : + m_var_set(vars), + m_num_decls(0), + m_var_kind(index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT) {} + + is_variable_test(unsigned num_decls) : + m_num_decls(num_decls), + m_var_kind(BY_NUM_DECLS) {} + + virtual bool operator()(expr* e) const { + if (!is_var(e)) { + return false; + } + unsigned idx = to_var(e)->get_idx(); + switch(m_var_kind) { + case BY_VAR_SET: + return m_var_set.contains(idx); + case BY_VAR_SET_COMPLEMENT: + return !m_var_set.contains(idx); + case BY_NUM_DECLS: + return idx < m_num_decls; + } + UNREACHABLE(); + return false; + } +}; + +#endif From 9f73359a86c634fc31a60db2c0a2c997063df47d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 21:50:35 -0400 Subject: [PATCH 59/63] improve comments --- src/qe/qe_lite.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 62f6c41a6..e84ab5cb8 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -788,12 +788,13 @@ namespace ar { } /** - Ex A. A[x] = t & Phi where x \not\in A, t. A \not\in t, x + Ex A. A[x] = t & Phi[A] where x \not\in A, t. A \not\in t, x => Ex A. Phi[store(A,x,t)] + (Not implemented) Perhaps also: - Ex A. store(A,y,z)[x] = t & Phi where x \not\in A, t, y, z, A \not\in y z, t + Ex A. store(A,y,z)[x] = t & Phi[A] where x \not\in A, t, y, z, A \not\in y z, t => Ex A, v . (x = y => z = t) & Phi[store(store(A,x,t),y,v)] @@ -822,7 +823,8 @@ namespace ar { expr_safe_replace rep(m); rep.insert(A, B); expr_ref tmp(m); - std::cout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n"; + TRACE("qe_lite", + tout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";); for (unsigned j = 0; j < conjs.size(); ++j) { if (i == j) { conjs[j] = m.mk_true(); From ef62621f50eb71a13b9485280a5115e0aa0e3575 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 21:51:08 -0400 Subject: [PATCH 60/63] make qe_lite prefer simpler definitions --- src/qe/qe_lite.cpp | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index e84ab5cb8..ce182a97b 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -49,6 +49,7 @@ namespace eq { ptr_vector m_map; int_vector m_pos2var; + int_vector m_var2pos; ptr_vector m_inx2var; unsigned_vector m_order; expr_ref_vector m_subst_map; @@ -541,6 +542,7 @@ namespace eq { largest_vinx = 0; m_map.reset(); m_pos2var.reset(); + m_var2pos.reset(); m_inx2var.reset(); m_pos2var.reserve(num_args, -1); @@ -560,10 +562,48 @@ namespace eq { m_map[idx] = t; m_inx2var[idx] = v; m_pos2var[i] = idx; + m_var2pos.reserve(idx + 1, -1); + m_var2pos[idx] = i; def_count++; largest_vinx = std::max(idx, largest_vinx); m_new_exprs.push_back(t); } + else if (!m.is_value(m_map[idx])) { + // check if the new definition is simpler + expr *old_def = m_map[idx]; + + // -- prefer values + if (m.is_value(t)) { + m_pos2var[m_var2pos[idx]] = -1; + m_pos2var[i] = idx; + m_var2pos[idx] = i; + m_map[idx] = t; + m_new_exprs.push_back(t); + } + // -- prefer ground + else if (is_app(t) && to_app(t)->is_ground() && + (!is_app(old_def) || + !to_app(old_def)->is_ground())) { + m_pos2var[m_var2pos[idx]] = -1; + m_pos2var[i] = idx; + m_var2pos[idx] = i; + m_map[idx] = t; + m_new_exprs.push_back(t); + } + // -- prefer constants + else if (is_uninterp_const(t) + /* && !is_uninterp_const(old_def) */){ + m_pos2var[m_var2pos[idx]] = -1; + m_pos2var[i] = idx; + m_var2pos[idx] = i; + m_map[idx] = t; + m_new_exprs.push_back(t); + } + TRACE ("qe_def", + tout << "Replacing definition of VAR " << idx << " from " + << mk_pp(old_def, m) << " to " << mk_pp(t, m) + << " inferred from: " << mk_pp(args[i], m) << "\n";); + } } } } From 7840f6cead3e305d53293150d8625da47912e45a Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 22:17:35 -0400 Subject: [PATCH 61/63] typo in a comment --- src/muz/transforms/dl_mk_slice.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index 2f7d0d475..aa910002d 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -22,7 +22,7 @@ Revision History: input: x, z output: x, y - Let x_i, y_i, z_i be incides into the vectors x, y, z. + Let x_i, y_i, z_i be indices into the vectors x, y, z. Suppose that positions in P and R are annotated with what is slicable. From 50f794c4f59e2717ef35375810a5c84d0527d239 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 22:08:52 -0400 Subject: [PATCH 62/63] api for accessing dl_rule name --- src/muz/base/dl_rule.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index f7dc18b5e..856814531 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -298,7 +298,7 @@ namespace datalog { static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); } - rule() : m_ref_cnt(0) {} + rule() : m_ref_cnt(0), m_name(symbol::null) {} ~rule() {} void deallocate(ast_manager & m); @@ -355,7 +355,12 @@ namespace datalog { void display(context & ctx, std::ostream & out) const; - symbol const& name() const { return m_name; } + /** + \brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules. + + This possibly returns a ";"-separated list of names. + */ + symbol const& name() const { return m_name; } ; unsigned hash() const; From af280579804c5af624b89b9bbb172f7c3e1a30fe Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 22:04:35 -0400 Subject: [PATCH 63/63] preserve dl rule names during xforms --- src/muz/base/dl_rule.cpp | 3 ++- src/muz/transforms/dl_mk_filter_rules.cpp | 2 +- src/muz/transforms/dl_mk_interp_tail_simplifier.cpp | 4 ++-- src/muz/transforms/dl_mk_magic_sets.cpp | 2 +- src/muz/transforms/dl_mk_quantifier_abstraction.cpp | 2 +- src/muz/transforms/dl_mk_quantifier_instantiation.cpp | 2 +- src/muz/transforms/dl_mk_rule_inliner.cpp | 5 ++++- src/muz/transforms/dl_mk_subsumption_checker.cpp | 2 +- 8 files changed, 13 insertions(+), 9 deletions(-) diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index ffb964f47..27d62538e 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -784,7 +784,7 @@ namespace datalog { SASSERT(tail.size()==tail_neg.size()); rule_ref old_r = r; - r = mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr()); + r = mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), old_r->name()); r->set_accounting_parent_object(m_ctx, old_r); } @@ -1003,6 +1003,7 @@ namespace datalog { void rule::display(context & ctx, std::ostream & out) const { ast_manager & m = ctx.get_manager(); + out << m_name.str () << ":\n"; //out << mk_pp(m_head, m); output_predicate(ctx, m_head, out); if (m_tail_size == 0) { diff --git a/src/muz/transforms/dl_mk_filter_rules.cpp b/src/muz/transforms/dl_mk_filter_rules.cpp index b112f4c99..0d118a589 100644 --- a/src/muz/transforms/dl_mk_filter_rules.cpp +++ b/src/muz/transforms/dl_mk_filter_rules.cpp @@ -140,7 +140,7 @@ namespace datalog { if (rule_modified) { remove_duplicate_tails(new_tail, new_is_negated); SASSERT(new_tail.size() == new_is_negated.size()); - rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr()); + rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr(), r->name()); new_rule->set_accounting_parent_object(m_context, m_current); m_result->add_rule(new_rule); m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule); diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 455b06d3d..3c1d1b924 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -84,7 +84,7 @@ namespace datalog { mk_rule_inliner::remove_duplicate_tails(m_tail, m_neg); SASSERT(m_tail.size() == m_neg.size()); - res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr()); + res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr(),m_rule->name()); res->set_accounting_parent_object(m_context, m_rule); res->norm_vars(res.get_manager()); } @@ -557,7 +557,7 @@ namespace datalog { } SASSERT(m_tail.size() == m_tail_neg.size()); - res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr()); + res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr(), r->name()); res->set_accounting_parent_object(m_context, r); } else { diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp index 048decaf9..19dccf417 100644 --- a/src/muz/transforms/dl_mk_magic_sets.cpp +++ b/src/muz/transforms/dl_mk_magic_sets.cpp @@ -280,7 +280,7 @@ namespace datalog { new_tail.push_back(create_magic_literal(new_head)); negations.push_back(false); - rule * nr = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), negations.c_ptr()); + rule * nr = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), negations.c_ptr(), r->name()); result.add_rule(nr); nr->set_accounting_parent_object(m_context, r); } diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index caff79d2e..5c0d442df 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -341,7 +341,7 @@ namespace datalog { head = mk_head(source, *result, r.get_head(), cnt); fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head); proof_ref pr(m); - rm.mk_rule(fml, pr, *result); + rm.mk_rule(fml, pr, *result, r.name()); TRACE("dl", result->last()->display(m_ctx, tout);); } diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 5d36d26cc..586c52cd6 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -232,7 +232,7 @@ namespace datalog { rule_set added_rules(m_ctx); proof_ref pr(m); - rm.mk_rule(fml, pr, added_rules); + rm.mk_rule(fml, pr, added_rules, r.name()); if (r.get_proof()) { // use def-axiom to encode that new rule is a weakening of the original. proof* p1 = r.get_proof(); diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 7dabece2f..c6b3e8be7 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -114,7 +114,10 @@ namespace datalog { apply(src, false, UINT_MAX, tail, tail_neg); mk_rule_inliner::remove_duplicate_tails(tail, tail_neg); SASSERT(tail.size()==tail_neg.size()); - res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), tgt.name(), m_normalize); + std::ostringstream comb_name; + comb_name << tgt.name().str() << ";" << src.name().str(); + symbol combined_rule_name = symbol(comb_name.str().c_str()); + res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), combined_rule_name, m_normalize); res->set_accounting_parent_object(m_context, const_cast(&tgt)); TRACE("dl", tgt.display(m_context, tout << "tgt (" << tail_index << "): \n"); diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index 1967fdc93..8fae4ee35 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -159,7 +159,7 @@ namespace datalog { } SASSERT(tail.size()==tail_neg.size()); - res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr()); + res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), r->name()); res->set_accounting_parent_object(m_context, r); m_context.get_rule_manager().fix_unbound_vars(res, true); m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *res.get());