diff --git a/README-CMake.md b/README-CMake.md
index 5b3cdfd36..1b7d89542 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -1,4 +1,4 @@
- # Z3's CMake build system
+# Z3's CMake build system
[CMake](https://cmake.org/) is a "meta build system" that reads a description
of the project written in the ``CMakeLists.txt`` files and emits a build
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;
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/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/api/java/Expr.java b/src/api/java/Expr.java
index ea3fd2147..71a2e3e1e 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -126,7 +126,7 @@ public class Expr extends AST
if (isApp() && args.length != getNumArgs()) {
throw new Z3Exception("Number of arguments does not match");
}
- return new Expr(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
+ return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
args.length, Expr.arrayToNative(args)));
}
@@ -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/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 8ad33d6fc..4d531d2db 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -935,9 +935,9 @@ bool datatype_util::is_recursive(sort * ty) {
bool datatype_util::is_enum_sort(sort* s) {
- if (!is_datatype(s)) {
- return false;
- }
+ if (!is_datatype(s)) {
+ return false;
+ }
bool r = false;
if (m_is_enum.find(s, r))
return r;
diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp
index 725c0b043..32b62342b 100644
--- a/src/ast/fpa/fpa2bv_rewriter.cpp
+++ b/src/ast/fpa/fpa2bv_rewriter.cpp
@@ -143,11 +143,11 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
- case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
+ case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
- case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
+ case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
- case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
+ case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE;
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index dc1931bac..ce707b108 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -92,25 +92,25 @@ public:
expr_ref fml(m.mk_true(), m);
return sym_expr::mk_pred(fml, m.mk_bool_sort());
}
- virtual T mk_and(T x, T y) {
- if (x->is_char() && y->is_char()) {
- if (x->get_char() == y->get_char()) {
- return x;
- }
- if (m.are_distinct(x->get_char(), y->get_char())) {
- expr_ref fml(m.mk_false(), m);
- return sym_expr::mk_pred(fml, x->get_sort());
- }
- }
+ virtual T mk_and(T x, T y) {
+ if (x->is_char() && y->is_char()) {
+ if (x->get_char() == y->get_char()) {
+ return x;
+ }
+ if (m.are_distinct(x->get_char(), y->get_char())) {
+ expr_ref fml(m.mk_false(), m);
+ return sym_expr::mk_pred(fml, x->get_sort());
+ }
+ }
- sort* s = x->get_sort();
- if (m.is_bool(s)) s = y->get_sort();
- var_ref v(m.mk_var(0, s), m);
- expr_ref fml1 = x->accept(v);
- expr_ref fml2 = y->accept(v);
- if (m.is_true(fml1)) {
- return y;
- }
+ sort* s = x->get_sort();
+ if (m.is_bool(s)) s = y->get_sort();
+ var_ref v(m.mk_var(0, s), m);
+ expr_ref fml1 = x->accept(v);
+ expr_ref fml2 = y->accept(v);
+ if (m.is_true(fml1)) {
+ return y;
+ }
if (m.is_true(fml2)) return x;
expr_ref fml(m.mk_and(fml1, fml2), m);
return sym_expr::mk_pred(fml, x->get_sort());
@@ -178,10 +178,10 @@ public:
return sym_expr::mk_pred(fml, x->get_sort());
}
- /*virtual vector, T>> generate_min_terms(vector constraints){
-
- return 0;
- }*/
+ /*virtual vector, T>> generate_min_terms(vector constraints){
+
+ return 0;
+ }*/
};
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}
diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp
index daf20e095..a3ad7fd07 100644
--- a/src/ast/static_features.cpp
+++ b/src/ast/static_features.cpp
@@ -391,7 +391,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
if (is_marked(e)) {
m_num_sharing++;
return;
- }
+ }
if (stack_depth > m_max_stack_depth) {
return;
}
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 7484a77fa..05bb5489a 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -1728,7 +1728,7 @@ namespace pdr {
void context::validate_search() {
expr_ref tr = m_search.get_trace(*this);
- TRACE("pdr", tout << tr << "\n";);
+ TRACE("pdr", tout << tr << "\n";);
smt::kernel solver(m, get_fparams());
solver.assert_expr(tr);
lbool res = solver.check();
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 83c31715d..b9ed925b0 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -130,13 +130,36 @@ public:
m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr());
}
+ bool is_literal(expr* e) const {
+ return
+ is_uninterp_const(e) ||
+ (m.is_not(e, e) && is_uninterp_const(e));
+ }
+
virtual lbool check_sat(unsigned sz, expr * const * assumptions) {
m_solver.pop_to_base_level();
+ expr_ref_vector _assumptions(m);
+ obj_map asm2fml;
+ for (unsigned i = 0; i < sz; ++i) {
+ if (!is_literal(assumptions[i])) {
+ expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m);
+ expr_ref fml(m.mk_eq(a, assumptions[i]), m);
+ assert_expr(fml);
+ _assumptions.push_back(a);
+ asm2fml.insert(a, assumptions[i]);
+ }
+ else {
+ _assumptions.push_back(assumptions[i]);
+ asm2fml.insert(assumptions[i], assumptions[i]);
+ }
+ }
+
+ TRACE("sat", tout << _assumptions << "\n";);
dep2asm_t dep2asm;
m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return r;
- r = internalize_assumptions(sz, assumptions, dep2asm);
+ r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm);
if (r != l_true) return r;
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
@@ -150,7 +173,7 @@ public:
case l_false:
// TBD: expr_dependency core is not accounted for.
if (!m_asms.empty()) {
- extract_core(dep2asm);
+ extract_core(dep2asm, asm2fml);
}
break;
default:
@@ -241,6 +264,7 @@ public:
sat::bool_var_vector bvars;
vector lconseq;
dep2asm_t dep2asm;
+ obj_map asm2fml;
m_solver.pop_to_base_level();
lbool r = internalize_formulas();
if (r != l_true) return r;
@@ -251,7 +275,7 @@ public:
r = m_solver.get_consequences(m_asms, bvars, lconseq);
if (r == l_false) {
if (!m_asms.empty()) {
- extract_core(dep2asm);
+ extract_core(dep2asm, asm2fml);
}
return r;
}
@@ -302,7 +326,6 @@ public:
return l_true;
}
-
virtual std::string reason_unknown() const {
return m_unknown;
}
@@ -569,7 +592,7 @@ private:
}
}
- void extract_core(dep2asm_t& dep2asm) {
+ void extract_core(dep2asm_t& dep2asm, obj_map const& asm2fml) {
u_map asm2dep;
extract_asm2dep(dep2asm, asm2dep);
sat::literal_vector const& core = m_solver.get_core();
@@ -590,6 +613,9 @@ private:
for (unsigned i = 0; i < core.size(); ++i) {
expr* e = 0;
VERIFY(asm2dep.find(core[i].index(), e));
+ if (asm2fml.contains(e)) {
+ e = asm2fml.find(e);
+ }
m_core.push_back(e);
}
}
diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index 129d77c85..41a269820 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -51,9 +51,9 @@ namespace smt {
if (!m_theory_var_priority.find(v2, p_v2)) {
p_v2 = 0.0;
}
- // add clause activity
- p_v1 += m_activity[v1];
- p_v2 += m_activity[v2];
+ // add clause activity
+ p_v1 += m_activity[v1];
+ p_v2 += m_activity[v2];
return p_v1 > p_v2;
}
};
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 50b957331..0c32f3c76 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3035,7 +3035,7 @@ namespace smt {
// not counting any literals that get assigned by this method
// this relies on bcp() to give us its old m_qhead and therefore
// bcp() should always be called before this method
-
+
unsigned assigned_literal_end = m_assigned_literals.size();
for (; qhead < assigned_literal_end; ++qhead) {
literal l = m_assigned_literals[qhead];
diff --git a/src/smt/smt_for_each_relevant_expr.cpp b/src/smt/smt_for_each_relevant_expr.cpp
index bf039e8a1..84f93dd33 100644
--- a/src/smt/smt_for_each_relevant_expr.cpp
+++ b/src/smt/smt_for_each_relevant_expr.cpp
@@ -23,7 +23,7 @@ Revision History:
namespace smt {
- bool check_at_labels::check(expr* n) {
+ bool check_at_labels::check(expr* n) {
m_first = true;
return count_at_labels_pos(n) <= 1;
}
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 279ea20cf..b50527acf 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -279,7 +279,7 @@ namespace smt {
m_aux_context->pop(1);
return r == l_false; // quantifier is satisfied by m_curr_model
}
-
+
model_ref complete_cex;
m_aux_context->get_model(complete_cex);
@@ -425,7 +425,7 @@ namespace smt {
ptr_vector::const_iterator end = m_qm->end_quantifiers();
for (; it != end; ++it) {
quantifier * q = *it;
- if(!m_qm->mbqi_enabled(q)) continue;
+ if(!m_qm->mbqi_enabled(q)) continue;
TRACE("model_checker",
tout << "Check: " << mk_pp(q, m) << "\n";
tout << m_context->get_assignment(q) << "\n";);
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index fa48fea57..6c47bf855 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -426,19 +426,19 @@ namespace smt {
ptr_buffer to_unmark;
unsigned num_vars = get_num_vars();
for (unsigned i = 0; i < num_vars; i++) {
- enode * n = get_enode(i);
+ enode * n = get_enode(i);
if (ctx.is_relevant(n)) {
- enode * r = n->get_root();
- if (!r->is_marked()){
- if(is_array_sort(r) && ctx.is_shared(r)) {
- TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
- theory_var r_th_var = r->get_th_var(get_id());
- SASSERT(r_th_var != null_theory_var);
- result.push_back(r_th_var);
- }
- r->set_mark();
- to_unmark.push_back(r);
- }
+ enode * r = n->get_root();
+ if (!r->is_marked()){
+ if(is_array_sort(r) && ctx.is_shared(r)) {
+ TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
+ theory_var r_th_var = r->get_th_var(get_id());
+ SASSERT(r_th_var != null_theory_var);
+ result.push_back(r_th_var);
+ }
+ r->set_mark();
+ to_unmark.push_back(r);
+ }
}
}
unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 05aa33d13..a5a34a079 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -487,7 +487,7 @@ namespace smt {
result = m_theory_var2var_index[v];
}
if (result == UINT_MAX) {
- result = m_solver->add_var(v);
+ result = m_solver->add_var(v); // TBD: is_int(v);
m_theory_var2var_index.setx(v, result, UINT_MAX);
m_var_index2theory_var.setx(result, v, UINT_MAX);
m_var_trail.push_back(v);
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 63f0a88bd..d560a54a1 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,7 @@ 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);
int idx = 0;
// small letters
for (int i = 97; i < 123; i++) {
@@ -157,8 +158,7 @@ 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);
charSetSize = fSize;
for (int i = 0; i < charSetSize; i++) {
char_set[i] = setset[i];
@@ -494,6 +494,7 @@ namespace smt {
sort * string_sort = u.str.mk_string_sort();
app * a = mk_fresh_const(name.c_str(), string_sort);
+ m_trail.push_back(a);
TRACE("str", tout << "a->get_family_id() = " << a->get_family_id() << std::endl
<< "this->get_family_id() = " << this->get_family_id() << std::endl;);
@@ -507,7 +508,6 @@ namespace smt {
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
- m_trail.push_back(a);
variable_set.insert(a);
internal_variable_set.insert(a);
track_variable_scope(a);
@@ -521,6 +521,7 @@ namespace smt {
sort * string_sort = u.str.mk_string_sort();
app * a = mk_fresh_const("regex", string_sort);
+ m_trail.push_back(a);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
@@ -529,7 +530,6 @@ namespace smt {
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
- m_trail.push_back(a);
variable_set.insert(a);
//internal_variable_set.insert(a);
regex_variable_set.insert(a);
@@ -5563,7 +5563,7 @@ namespace smt {
if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) {
ndVec.pop_back();
ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0]));
- for (int i = 1; i < arg1VecSize; i++) {
+ for (size_t i = 1; i < arg1VecSize; i++) {
ndVec.push_back(arg1_grdItor->first[i]);
}
} else {
@@ -5666,7 +5666,7 @@ namespace smt {
if (subStrCnt == 1) {
zstring subStrVal;
if (u.str.is_string(subStrVec[0], subStrVal)) {
- for (int i = 0; i < strCnt; i++) {
+ for (size_t i = 0; i < strCnt; i++) {
zstring strVal;
if (u.str.is_string(strVec[i], strVal)) {
if (strVal.contains(subStrVal)) {
@@ -5675,7 +5675,7 @@ namespace smt {
}
}
} else {
- for (int i = 0; i < strCnt; i++) {
+ for (size_t i = 0; i < strCnt; i++) {
if (strVec[i] == subStrVec[0]) {
return true;
}
@@ -5683,7 +5683,7 @@ namespace smt {
}
return false;
} else {
- for (int i = 0; i <= (strCnt - subStrCnt); i++) {
+ for (size_t i = 0; i <= (strCnt - subStrCnt); i++) {
// The first node in subStrVect should be
// * constant: a suffix of a note in strVec[i]
// * variable:
@@ -5712,7 +5712,7 @@ namespace smt {
// middle nodes
bool midNodesOK = true;
- for (int j = 1; j < subStrCnt - 1; j++) {
+ for (size_t j = 1; j < subStrCnt - 1; j++) {
if (subStrVec[j] != strVec[i + j]) {
midNodesOK = false;
break;
@@ -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);
}
}
@@ -9123,7 +9123,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++) {
@@ -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();
@@ -9240,8 +9240,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 +9261,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 +9272,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,20 +9286,9 @@ 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;
+ return m.mk_or(m.mk_not(assertL), valTestAssert);
}
expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator,
@@ -9378,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;);
@@ -9400,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 4752e8a1b..0bbc44ab8 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;
+ std::map charSetLookupTable;
+ int charSetSize;
obj_pair_map concat_astNode_map;
@@ -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);
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index 918e0fc6d..ca6390c9c 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -103,7 +103,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
tactic * st = main_p(and_then(preamble_st,
// If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
// symbols. In this case, we should not use the `sat', but instead `smt'. Alternatively,
- // the UFs can be eliminated by eager ackermannization in the preamble.
+ // the UFs can be eliminated by eager ackermannization in the preamble.
cond(mk_is_qfbv_eq_probe(),
and_then(mk_bv1_blaster_tactic(m),
using_params(smt, solver_p)),
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
index e577e15df..a522c9a41 100644
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
@@ -29,7 +29,7 @@ Revision History:
#include
#endif
-#if defined(__x86_64__) || defined(_M_X64) || \
+#if defined(__x86_64__) || defined(_M_X64) || \
defined(__i386) || defined(_M_IX86)
#define USE_INTRINSICS
#endif
diff --git a/src/util/trace.cpp b/src/util/trace.cpp
index 72984d808..05a3e49bd 100644
--- a/src/util/trace.cpp
+++ b/src/util/trace.cpp
@@ -52,7 +52,7 @@ void disable_trace(const char * tag) {
bool is_trace_enabled(const char * tag) {
return g_enable_all_trace_tags ||
- (g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast(tag)));
+ (g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast(tag)));
}
void close_trace() {
diff --git a/src/util/warning.cpp b/src/util/warning.cpp
index ed4cd8725..9c6a285b9 100644
--- a/src/util/warning.cpp
+++ b/src/util/warning.cpp
@@ -115,22 +115,22 @@ void format2ostream(std::ostream & out, char const* msg, va_list args) {
while (true) {
int nc = VPRF(buff.c_ptr(), buff.size(), msg, args);
#if !defined(_WINDOWS) && defined(_AMD64_)
- // For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf.
- // Z3 crashes when trying to use va_list args again.
+ // For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf.
+ // Z3 crashes when trying to use va_list args again.
// Hack: I truncate the message instead of expanding the buffer to make sure that
// va_list args is only used once.
- END_ERR_HANDLER();
- if (nc < 0) {
- // vsnprintf didn't work, so we just print the msg
- out << msg;
- return;
- }
- if (nc >= static_cast(buff.size())) {
+ END_ERR_HANDLER();
+ if (nc < 0) {
+ // vsnprintf didn't work, so we just print the msg
+ out << msg;
+ return;
+ }
+ if (nc >= static_cast(buff.size())) {
// truncate the message
buff[buff.size() - 1] = 0;
- }
+ }
out << buff.c_ptr();
- return;
+ return;
#else
if (nc >= 0 && nc < static_cast(buff.size()))
break; // success