diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9ea244d17..30ae48058 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -2,7 +2,8 @@
cmake_minimum_required(VERSION 3.4)
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.8.12.0 LANGUAGES CXX C)
+project(Z3 VERSION 4.8.13.0 LANGUAGES CXX C)
+>>>>>>> 79c261736bf6a6b2018813f4e33519cab4256fb0
################################################################################
# Project version
diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 89f839cae..dae1e81b8 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -11,6 +11,11 @@ Version 4.8.next
turned off by default.
+Version 4.8.12
+==============
+Release provided to fix git tag discrepancy issues with 4.8.11
+
+
Version 4.8.11
==============
- self-contained character theory, direct support for UTF8, Unicode character sets.
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index fb0ea0440..00388c6fd 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -8,7 +8,7 @@
from mk_util import *
def init_version():
- set_version(4, 8, 12, 0)
+ set_version(4, 8, 13, 0)
# Z3 Project definition
def init_project_def():
diff --git a/scripts/release.yml b/scripts/release.yml
index cc5946a91..901afc575 100644
--- a/scripts/release.yml
+++ b/scripts/release.yml
@@ -6,7 +6,7 @@
trigger: none
variables:
- ReleaseVersion: '4.8.11'
+ ReleaseVersion: '4.8.12'
stages:
@@ -107,7 +107,6 @@ stages:
inputs:
artifactName: 'UbuntuDoc'
targetPath: $(Build.ArtifactStagingDirectory)
-
- job: ManyLinuxBuild
displayName: "ManyLinux build"
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index ef9d26889..648e3cd97 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1202,6 +1202,7 @@ extern "C" {
case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
+ case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR;
case OP_STRING_LT: return Z3_OP_STRING_LT;
case OP_STRING_LE: return Z3_OP_STRING_LE;
diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index 39e5b80cc..fc336da74 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -79,6 +79,16 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
+ Z3_sort Z3_API Z3_mk_char_sort(Z3_context c) {
+ Z3_TRY;
+ LOG_Z3_mk_char_sort(c);
+ RESET_ERROR_CODE();
+ sort* ty = mk_c(c)->sutil().mk_char_sort();
+ mk_c(c)->save_ast_trail(ty);
+ RETURN_Z3(of_sort(ty));
+ Z3_CATCH_RETURN(nullptr);
+ }
+
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s) {
Z3_TRY;
LOG_Z3_is_seq_sort(c, s);
@@ -121,6 +131,15 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
+ bool Z3_API Z3_is_char_sort(Z3_context c, Z3_sort s) {
+ Z3_TRY;
+ LOG_Z3_is_char_sort(c, s);
+ RESET_ERROR_CODE();
+ return mk_c(c)->sutil().is_char(to_sort(s));
+ Z3_CATCH_RETURN(false);
+ }
+
+
bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) {
Z3_TRY;
LOG_Z3_is_string_sort(c, s);
@@ -225,6 +244,7 @@ extern "C" {
MK_UNARY(Z3_mk_int_to_str, mk_c(c)->get_seq_fid(), OP_STRING_ITOS, SKIP);
MK_UNARY(Z3_mk_str_to_int, mk_c(c)->get_seq_fid(), OP_STRING_STOI, SKIP);
+ MK_UNARY(Z3_mk_ubv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_UBVTOS, SKIP);
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) {
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index e0276c9e5..792b038e9 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -253,8 +253,13 @@ namespace z3 {
\brief Return the Bit-vector sort of size \c sz. That is, the sort for bit-vectors of size \c sz.
*/
sort bv_sort(unsigned sz);
+
/**
- \brief Return the sort for ASCII strings.
+ \brief Return the sort for Unicode characters.
+ */
+ sort char_sort();
+ /**
+ \brief Return the sort for Unicode strings.
*/
sort string_sort();
/**
@@ -1437,7 +1442,12 @@ namespace z3 {
check_error();
return expr(ctx(), r);
}
-
+ expr ubvtos() const {
+ Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
+ check_error();
+ return expr(ctx(), r);
+ }
+
friend expr range(expr const& lo, expr const& hi);
/**
\brief create a looping regular expression.
@@ -3199,6 +3209,7 @@ namespace z3 {
inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
+ inline sort context::char_sort() { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }
inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
inline sort context::fpa_sort(unsigned ebits, unsigned sbits) { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }
diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index c7ae98762..98d4b9503 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -55,6 +55,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
BitVecSort.cs
BoolExpr.cs
BoolSort.cs
+ CharSort.cs
Constructor.cs
ConstructorList.cs
Context.cs
diff --git a/src/api/dotnet/CharSort.cs b/src/api/dotnet/CharSort.cs
new file mode 100644
index 000000000..d5410e6c4
--- /dev/null
+++ b/src/api/dotnet/CharSort.cs
@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ CharSort.cs
+
+Abstract:
+
+ Z3 Managed API: Character Sorts
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+
+--*/
+
+using System.Diagnostics;
+using System;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// A Character sort
+ ///
+ public class CharSort : Sort
+ {
+ #region Internal
+ internal CharSort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
+ internal CharSort(Context ctx) : base(ctx, Native.Z3_mk_char_sort(ctx.nCtx)) { Debug.Assert(ctx != null); }
+ #endregion
+ }
+}
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index b4afabe0e..d40281a81 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -89,7 +89,6 @@ namespace Microsoft.Z3
///
public IntSymbol MkSymbol(int i)
{
-
return new IntSymbol(this, i);
}
@@ -98,7 +97,6 @@ namespace Microsoft.Z3
///
public StringSymbol MkSymbol(string name)
{
-
return new StringSymbol(this, name);
}
@@ -107,7 +105,6 @@ namespace Microsoft.Z3
///
internal Symbol[] MkSymbols(string[] names)
{
-
if (names == null) return null;
Symbol[] result = new Symbol[names.Length];
for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
@@ -120,6 +117,7 @@ namespace Microsoft.Z3
private IntSort m_intSort = null;
private RealSort m_realSort = null;
private SeqSort m_stringSort = null;
+ private CharSort m_charSort = null;
///
/// Retrieves the Boolean sort of the context.
@@ -155,6 +153,18 @@ namespace Microsoft.Z3
}
}
+ ///
+ /// Retrieves the String sort of the context.
+ ///
+ public CharSort CharSort
+ {
+ get
+ {
+ if (m_charSort == null) m_charSort = new CharSort(this); return m_charSort;
+ }
+ }
+
+
///
/// Retrieves the String sort of the context.
///
@@ -2385,6 +2395,16 @@ namespace Microsoft.Z3
return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
}
+ ///
+ /// Convert a bit-vector expression, represented as an unsigned number, to a string.
+ ///
+ public SeqExpr UbvToString(Expr e)
+ {
+ Debug.Assert(e != null);
+ Debug.Assert(e is ArithExpr);
+ return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
+ }
+
///
/// Convert an integer expression to a string.
///
diff --git a/src/api/dotnet/SeqSort.cs b/src/api/dotnet/SeqSort.cs
index 2902b1e9e..ae57885ca 100644
--- a/src/api/dotnet/SeqSort.cs
+++ b/src/api/dotnet/SeqSort.cs
@@ -33,11 +33,6 @@ namespace Microsoft.Z3
{
Debug.Assert(ctx != null);
}
- internal SeqSort(Context ctx)
- : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
- {
- Debug.Assert(ctx != null);
- }
#endregion
}
}
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index f886639f8..dd7115aaa 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -108,6 +108,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
BitVecSort.java
BoolExpr.java
BoolSort.java
+ CharSort.java
ConstructorDecRefQueue.java
Constructor.java
ConstructorListDecRefQueue.java
diff --git a/src/api/java/CharSort.java b/src/api/java/CharSort.java
new file mode 100644
index 000000000..2d843c8ac
--- /dev/null
+++ b/src/api/java/CharSort.java
@@ -0,0 +1,33 @@
+/**
+Copyright (c) 2012-2014 Microsoft Corporation
+
+Module Name:
+
+ CharSort.java
+
+Abstract:
+
+Author:
+
+ @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+
+**/
+
+package com.microsoft.z3;
+
+/**
+ * A Character sort
+ **/
+public class CharSort extends Sort
+{
+ CharSort(Context ctx, long obj)
+ {
+ super(ctx, obj);
+ }
+
+ CharSort(Context ctx) { super(ctx, Native.mkCharSort(ctx.nCtx())); { }}
+
+}
+
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 160dfa7db..a6b867eb8 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -120,7 +120,7 @@ public class Context implements AutoCloseable {
private BoolSort m_boolSort = null;
private IntSort m_intSort = null;
private RealSort m_realSort = null;
- private SeqSort m_stringSort = null;
+ private SeqSort m_stringSort = null;
/**
* Retrieves the Boolean sort of the context.
@@ -164,9 +164,18 @@ public class Context implements AutoCloseable {
}
/**
- * Retrieves the Integer sort of the context.
+ * Creates character sort object.
**/
- public SeqSort getStringSort()
+
+ public CharSort mkCharSort()
+ {
+ return new CharSort(this);
+ }
+
+ /**
+ * Retrieves the String sort of the context.
+ **/
+ public SeqSort getStringSort()
{
if (m_stringSort == null) {
m_stringSort = mkStringSort();
@@ -239,7 +248,7 @@ public class Context implements AutoCloseable {
/**
* Create a new string sort
**/
- public SeqSort mkStringSort()
+ public SeqSort mkStringSort()
{
return new SeqSort<>(this, Native.mkStringSort(nCtx()));
}
@@ -2006,23 +2015,31 @@ public class Context implements AutoCloseable {
/**
* Create a string constant.
*/
- public SeqExpr mkString(String s)
+ public SeqExpr mkString(String s)
{
- return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
+ return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
}
/**
* Convert an integer expression to a string.
*/
- public SeqExpr intToString(Expr e)
+ public SeqExpr intToString(Expr e)
{
- return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
+ return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
+ }
+
+ /**
+ * Convert an unsigned bitvector expression to a string.
+ */
+ public SeqExpr ubvToString(Expr e)
+ {
+ return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
}
/**
* Convert an integer expression to a string.
*/
- public IntExpr stringToInt(Expr> e)
+ public IntExpr stringToInt(Expr> e)
{
return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
}
@@ -2041,7 +2058,7 @@ public class Context implements AutoCloseable {
/**
* Retrieve the length of a given sequence.
*/
- public IntExpr mkLength(Expr> s)
+ public IntExpr mkLength(Expr> s)
{
checkContextMatch(s);
return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
@@ -2050,7 +2067,7 @@ public class Context implements AutoCloseable {
/**
* Check for sequence prefix.
*/
- public BoolExpr mkPrefixOf(Expr> s1, Expr> s2)
+ public BoolExpr mkPrefixOf(Expr> s1, Expr> s2)
{
checkContextMatch(s1, s2);
return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
@@ -2059,7 +2076,7 @@ public class Context implements AutoCloseable {
/**
* Check for sequence suffix.
*/
- public BoolExpr mkSuffixOf(Expr> s1, Expr> s2)
+ public BoolExpr mkSuffixOf(Expr> s1, Expr> s2)
{
checkContextMatch(s1, s2);
return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
@@ -2068,7 +2085,7 @@ public class Context implements AutoCloseable {
/**
* Check for sequence containment of s2 in s1.
*/
- public BoolExpr mkContains(Expr> s1, Expr> s2)
+ public BoolExpr mkContains(Expr> s1, Expr> s2)
{
checkContextMatch(s1, s2);
return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
@@ -2077,7 +2094,7 @@ public class Context implements AutoCloseable {
/**
* Retrieve sequence of length one at index.
*/
- public SeqExpr mkAt(Expr> s, Expr index)
+ public SeqExpr mkAt(Expr> s, Expr index)
{
checkContextMatch(s, index);
return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
@@ -2086,7 +2103,7 @@ public class Context implements AutoCloseable {
/**
* Retrieve element at index.
*/
- public Expr MkNth(Expr> s, Expr index)
+ public Expr MkNth(Expr> s, Expr index)
{
checkContextMatch(s, index);
return (Expr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
@@ -2096,7 +2113,7 @@ public class Context implements AutoCloseable {
/**
* Extract subsequence.
*/
- public SeqExpr mkExtract(Expr> s, Expr offset, Expr length)
+ public SeqExpr mkExtract(Expr> s, Expr offset, Expr length)
{
checkContextMatch(s, offset, length);
return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
@@ -2105,7 +2122,7 @@ public class Context implements AutoCloseable {
/**
* Extract index of sub-string starting at offset.
*/
- public IntExpr mkIndexOf(Expr> s, Expr> substr, Expr offset)
+ public IntExpr mkIndexOf(Expr> s, Expr> substr, Expr offset)
{
checkContextMatch(s, substr, offset);
return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
@@ -2114,7 +2131,7 @@ public class Context implements AutoCloseable {
/**
* Replace the first occurrence of src by dst in s.
*/
- public SeqExpr mkReplace(Expr> s, Expr> src, Expr> dst)
+ public SeqExpr mkReplace(Expr> s, Expr> src, Expr> dst)
{
checkContextMatch(s, src, dst);
return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
@@ -2123,7 +2140,7 @@ public class Context implements AutoCloseable {
/**
* Convert a regular expression that accepts sequence s.
*/
- public ReExpr mkToRe(Expr> s)
+ public ReExpr mkToRe(Expr> s)
{
checkContextMatch(s);
return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
@@ -2133,7 +2150,7 @@ public class Context implements AutoCloseable {
/**
* Check for regular expression membership.
*/
- public BoolExpr mkInRe(Expr> s, Expr> re)
+ public BoolExpr mkInRe(Expr> s, Expr> re)
{
checkContextMatch(s, re);
return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
@@ -2241,7 +2258,7 @@ public class Context implements AutoCloseable {
/**
* Create a range expression.
*/
- public ReExpr mkRange(Expr> lo, Expr> hi)
+ public ReExpr mkRange(Expr> lo, Expr> hi)
{
checkContextMatch(lo, hi);
return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
diff --git a/src/api/java/SeqSort.java b/src/api/java/SeqSort.java
index 28b865733..4650021b9 100644
--- a/src/api/java/SeqSort.java
+++ b/src/api/java/SeqSort.java
@@ -27,3 +27,4 @@ public class SeqSort extends Sort
super(ctx, obj);
}
}
+
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index cf650a5fa..f636e7caa 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1202,6 +1202,7 @@ typedef enum {
// strings
Z3_OP_STR_TO_INT,
Z3_OP_INT_TO_STR,
+ Z3_OP_UBV_TO_STR,
Z3_OP_STRING_LT,
Z3_OP_STRING_LE,
@@ -3437,15 +3438,22 @@ extern "C" {
Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s);
/**
- \brief Create a sort for 8 bit strings.
-
- This function creates a sort for ASCII strings.
- Each character is 8 bits.
+ \brief Create a sort for unicode strings.
def_API('Z3_mk_string_sort', SORT ,(_in(CONTEXT), ))
*/
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
+ /**
+ \brief Create a sort for unicode characters.
+
+ The sort for characters can be changed to ASCII by setting
+ the global parameter \c unicode to \c false.
+
+ def_API('Z3_mk_char_sort', SORT ,(_in(CONTEXT), ))
+ */
+ Z3_sort Z3_API Z3_mk_char_sort(Z3_context c);
+
/**
\brief Check if \c s is a string sort.
@@ -3453,6 +3461,13 @@ extern "C" {
*/
bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
+ /**
+ \brief Check if \c s is a character sort.
+
+ def_API('Z3_is_char_sort', BOOL, (_in(CONTEXT), _in(SORT)))
+ */
+ bool Z3_API Z3_is_char_sort(Z3_context c, Z3_sort s);
+
/**
\brief Create a string constant out of the string that is passed in
def_API('Z3_mk_string' ,AST ,(_in(CONTEXT), _in(STRING)))
@@ -3633,6 +3648,14 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
+ /**
+ \brief Unsigned bit-vector to string conversion.
+
+ def_API('Z3_mk_ubv_to_str' ,AST ,(_in(CONTEXT), _in(AST)))
+ */
+ Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s);
+
+
/**
\brief Create a regular expression that accepts the sequence \c seq.
diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
index 62dbd74b5..f7ba8132f 100644
--- a/src/ast/ast_ll_pp.cpp
+++ b/src/ast/ast_ll_pp.cpp
@@ -303,7 +303,9 @@ public:
}
void display_bounded(ast * n, unsigned depth) {
- if (is_app(n)) {
+ if (!n)
+ m_out << "null";
+ else if (is_app(n)) {
display(to_expr(n), depth);
}
else if (is_var(n)) {
diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 44389eb6c..cffef51a0 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -769,6 +769,67 @@ namespace seq {
}
}
+ void axioms::ubv2s_axiom(expr* b, unsigned k) {
+ expr_ref ge10k(m), ge10k1(m), eq(m);
+ bv_util bv(m);
+ sort* bv_sort = b->get_sort();
+ rational pow(1);
+ for (unsigned i = 0; i < k; ++i)
+ pow *= 10;
+ if (k == 0) {
+ ge10k = m.mk_true();
+ }
+ else {
+ ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b);
+ }
+ ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b);
+ unsigned sz = bv.get_bv_size(b);
+ expr_ref_vector es(m);
+ expr_ref bb(b, m), ten(bv.mk_numeral(10, sz), m);
+ pow = 1;
+ for (unsigned i = 0; i <= k; ++i) {
+ if (pow > 1)
+ bb = bv.mk_bv_udiv(b, bv.mk_numeral(pow, bv_sort));
+ es.push_back(seq.str.mk_unit(m_sk.mk_ubv2ch(bv.mk_bv_urem(bb, ten))));
+ pow *= 10;
+ }
+ es.reverse();
+ eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort()));
+ add_clause(~ge10k, ge10k1, eq);
+ }
+
+ /*
+ * len(ubv2s(b)) = k => 10^k-1 <= b < 10^{k} k > 1
+ * len(ubv2s(b)) = 1 => b < 10^{1} k = 1
+ */
+ void axioms::ubv2s_len_axiom(expr* b, unsigned k) {
+ expr_ref ge10k(m), ge10k1(m), eq(m);
+ bv_util bv(m);
+ sort* bv_sort = b->get_sort();
+ unsigned sz = bv.get_bv_size(bv_sort);
+ rational pow(1);
+ for (unsigned i = 1; i < k; ++i)
+ pow *= 10;
+ if (pow * 10 >= rational::power_of_two(sz))
+ return; // TODO: add conflict when k is too large or avoid overflow bounds and limits
+ ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b);
+ ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b);
+ eq = m.mk_eq(seq.str.mk_length(seq.str.mk_ubv2s(b)), a.mk_int(k));
+ add_clause(~eq, ~ge10k1);
+ if (k > 1)
+ add_clause(~eq, ge10k);
+ }
+
+ void axioms::ubv2ch_axiom(sort* bv_sort) {
+ bv_util bv(m);
+ expr_ref eq(m);
+ unsigned sz = bv.get_bv_size(bv_sort);
+ for (unsigned i = 0; i < 10; ++i) {
+ eq = m.mk_eq(m_sk.mk_ubv2ch(bv.mk_numeral(i, sz)), seq.mk_char('0' + i));
+ add_clause(eq);
+ }
+ }
+
/**
Let s := itos(e)
diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h
index d124dd39f..c9cdbfc9a 100644
--- a/src/ast/rewriter/seq_axioms.h
+++ b/src/ast/rewriter/seq_axioms.h
@@ -94,6 +94,9 @@ namespace seq {
void stoi_axiom(expr* n);
void stoi_axiom(expr* e, unsigned k);
void itos_axiom(expr* s, unsigned k);
+ void ubv2s_axiom(expr* b, unsigned k);
+ void ubv2s_len_axiom(expr* b, unsigned k);
+ void ubv2ch_axiom(sort* bv_sort);
void lt_axiom(expr* n);
void le_axiom(expr* n);
void is_digit_axiom(expr* n);
diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp
index 2c595090e..e293743f8 100644
--- a/src/ast/rewriter/seq_eq_solver.cpp
+++ b/src/ast/rewriter/seq_eq_solver.cpp
@@ -16,6 +16,7 @@ Author:
--*/
#include "ast/rewriter/seq_eq_solver.h"
+#include "ast/bv_decl_plugin.h"
namespace seq {
@@ -37,6 +38,10 @@ namespace seq {
return true;
if (reduce_itos3(e, r))
return true;
+ if (reduce_ubv2s1(e, r))
+ return true;
+ if (reduce_ubv2s2(e, r))
+ return true;
if (reduce_binary_eq(e, r))
return true;
if (reduce_nth_solved(e, r))
@@ -184,8 +189,8 @@ namespace seq {
expr_ref digit = m_ax.sk().mk_digit2int(u);
add_consequence(m_ax.mk_ge(digit, 1));
}
- expr_ref y(seq.str.mk_concat(e.rs, e.ls[0]->get_sort()), m);
- ctx.add_solution(e.ls[0], y);
+ expr_ref y(seq.str.mk_concat(es, es[0]->get_sort()), m);
+ ctx.add_solution(seq.str.mk_itos(n), y);
return true;
}
@@ -209,6 +214,105 @@ namespace seq {
}
+
+ /**
+ * from_ubv(s) == from_ubv(t)
+ * --------------------------
+ * s = t
+ */
+
+ bool eq_solver::match_ubv2s1(eqr const& e, expr*& a, expr*& b) {
+ return
+ e.ls.size() == 1 && e.rs.size() == 1 &&
+ seq.str.is_ubv2s(e.ls[0], a) && seq.str.is_ubv2s(e.rs[0], b);
+ return false;
+ }
+
+ bool eq_solver::reduce_ubv2s1(eqr const& e, eq_ptr& r) {
+ expr* s = nullptr, * t = nullptr;
+ if (!match_ubv2s1(e, s, t))
+ return false;
+ expr_ref eq = mk_eq(s, t);
+ add_consequence(eq);
+ return true;
+ }
+
+ /**
+ *
+ * bv2s(n) = [d1]+[d2]+...+[dk]
+ * ---------------------------------
+ * n = 10^{k-1}*d1 + ... + dk
+ *
+ * k > 1 => d1 > 0
+ */
+ bool eq_solver::match_ubv2s2(eqr const& e, expr*& n, expr_ref_vector const*& es) {
+ if (e.ls.size() == 1 && seq.str.is_ubv2s(e.ls[0], n)) {
+ es = &e.rs;
+ return true;
+ }
+ if (e.rs.size() == 1 && seq.str.is_ubv2s(e.rs[0], n)) {
+ es = &e.ls;
+ return true;
+ }
+ return false;
+ }
+
+ bool eq_solver::reduce_ubv2s2(eqr const& e, eq_ptr& r) {
+ expr* n = nullptr;
+ expr_ref_vector const* _es = nullptr;
+ if (!match_ubv2s2(e, n, _es))
+ return false;
+
+ expr_ref_vector const& es = *_es;
+ if (es.empty()) {
+ set_conflict();
+ return true;
+ }
+ expr* u = nullptr;
+ for (expr* r : es) {
+ if (seq.str.is_unit(r, u)) {
+ expr_ref is_digit = m_ax.is_digit(u);
+ if (!m.is_true(ctx.expr2rep(is_digit)))
+ add_consequence(is_digit);
+ }
+ }
+ if (!all_units(es, 0, es.size()))
+ return false;
+
+ expr_ref num(m);
+ bv_util bv(m);
+ sort* bv_sort = n->get_sort();
+ unsigned sz = bv.get_bv_size(n);
+ if (es.size() > (sz + log2(10)-1)/log2(10)) {
+ set_conflict();
+ return true;
+ }
+
+ for (expr* r : es) {
+ VERIFY(seq.str.is_unit(r, u));
+ expr_ref digit = m_ax.sk().mk_digit2bv(u, bv_sort);
+ if (!num)
+ num = digit;
+ else
+ num = bv.mk_bv_add(bv.mk_bv_mul(bv.mk_numeral(10, sz), num), digit);
+ }
+
+ expr_ref eq(m.mk_eq(n, num), m);
+ m_ax.rewrite(eq);
+ add_consequence(eq);
+ if (es.size() > 1) {
+ VERIFY(seq.str.is_unit(es[0], u));
+ expr_ref digit = m_ax.sk().mk_digit2bv(u, bv_sort);
+ expr_ref eq0(m.mk_eq(digit, bv.mk_numeral(0, sz)), m);
+ expr_ref neq0(m.mk_not(eq0), m);
+ add_consequence(neq0);
+ }
+ expr_ref y(seq.str.mk_concat(es, es[0]->get_sort()), m);
+ ctx.add_solution(seq.str.mk_ubv2s(n), y);
+ return true;
+ }
+
+
/**
* Equation is of the form x ++ xs = ys ++ x
* where |xs| = |ys| are units of same length
diff --git a/src/ast/rewriter/seq_eq_solver.h b/src/ast/rewriter/seq_eq_solver.h
index e014bb8e1..6be2531b2 100644
--- a/src/ast/rewriter/seq_eq_solver.h
+++ b/src/ast/rewriter/seq_eq_solver.h
@@ -64,6 +64,12 @@ namespace seq {
bool reduce_itos3(eqr const& e, eq_ptr& r);
bool match_itos3(eqr const& e, expr*& n, expr_ref_vector const* & es);
+ bool match_ubv2s1(eqr const& e, expr*& s, expr*& t);
+ bool reduce_ubv2s1(eqr const& e, eq_ptr& r);
+
+ bool match_ubv2s2(eqr const& e, expr*& n, expr_ref_vector const*& es);
+ bool reduce_ubv2s2(eqr const& e, eq_ptr& r);
+
bool match_binary_eq(eqr const& e, expr_ref& x, ptr_vector& xs, ptr_vector& ys, expr_ref& y);
bool reduce_binary_eq(eqr const& e, eq_ptr& r);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 6e0d0f7b7..0bd653232 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -714,6 +714,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
SASSERT(num_args == 1);
st = mk_str_stoi(args[0], result);
break;
+ case OP_STRING_UBVTOS:
+ SASSERT(num_args == 1);
+ st = mk_str_ubv2s(args[0], result);
+ break;
case _OP_STRING_CONCAT:
case _OP_STRING_PREFIX:
case _OP_STRING_SUFFIX:
@@ -2204,6 +2208,17 @@ br_status seq_rewriter::mk_str_is_digit(expr* a, expr_ref& result) {
}
+br_status seq_rewriter::mk_str_ubv2s(expr* a, expr_ref& result) {
+ bv_util bv(m());
+ rational val;
+ if (bv.is_numeral(a, val)) {
+ result = str().mk_string(zstring(val));
+ return BR_DONE;
+ }
+ return BR_FAILED;
+}
+
+
br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
rational r;
if (m_autil.is_numeral(a, r)) {
@@ -2265,6 +2280,11 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one());
return BR_DONE;
}
+ if (str().is_ubv2s(a, b)) {
+ bv_util bv(m());
+ result = bv.mk_bv2int(b);
+ return BR_DONE;
+ }
expr* c = nullptr, *t = nullptr, *e = nullptr;
if (m().is_ite(a, c, t, e)) {
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 60e4cf031..7d102a5fb 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -228,6 +228,7 @@ class seq_rewriter {
br_status mk_str_units(func_decl* f, expr_ref& result);
br_status mk_str_itos(expr* a, expr_ref& result);
br_status mk_str_stoi(expr* a, expr_ref& result);
+ br_status mk_str_ubv2s(expr* a, expr_ref& result);
br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
br_status mk_str_to_regexp(expr* a, expr_ref& result);
br_status mk_str_le(expr* a, expr* b, expr_ref& result);
diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp
index c76efda57..ecefe8374 100644
--- a/src/ast/rewriter/seq_skolem.cpp
+++ b/src/ast/rewriter/seq_skolem.cpp
@@ -201,3 +201,6 @@ expr_ref skolem::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, e
return expr_ref(seq.mk_skolem(m_aut_step, args.size(), args.data(), m.mk_bool_sort()), m);
}
+expr_ref skolem::mk_digit2bv(expr* ch, sort* bv_sort) {
+ return mk(symbol("seq.digit2bv"), ch, nullptr, nullptr, nullptr, bv_sort);
+}
diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h
index 56baf8def..a7d4be917 100644
--- a/src/ast/rewriter/seq_skolem.h
+++ b/src/ast/rewriter/seq_skolem.h
@@ -93,6 +93,8 @@ namespace seq {
expr_ref mk_is_digit(expr* ch) { return mk(symbol("seq.is_digit"), ch, nullptr, nullptr, nullptr, m.mk_bool_sort()); }
expr_ref mk_unit_inv(expr* n);
expr_ref mk_digit2int(expr* ch) { return mk(symbol("seq.digit2int"), ch, nullptr, nullptr, nullptr, a.mk_int()); }
+ expr_ref mk_digit2bv(expr* ch, sort* bv_sort);
+ expr_ref mk_ubv2ch(expr* b) { return mk(symbol("seq.ubv2ch"), b, nullptr, nullptr, nullptr, seq.mk_char_sort()); }
expr_ref mk_left(expr* x, expr* y, expr* z = nullptr) { return mk("seq.left", x, y, z); }
expr_ref mk_right(expr* x, expr* y, expr* z = nullptr) { return mk("seq.right", x, y, z); }
expr_ref mk_max_unfolding_depth(unsigned d);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 7c76b3f64..ea073f23f 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -350,6 +350,17 @@ func_decl* seq_decl_plugin::mk_left_assoc_fun(decl_kind k, unsigned arity, sort*
return mk_assoc_fun(k, arity, domain, range, k_seq, k_string, false);
}
+func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) {
+ ast_manager& m = *m_manager;
+ if (arity != 1)
+ m.raise_exception("Invalid str.from_ubv expects one bit-vector argument");
+ bv_util bv(m);
+ if (!bv.is_bv_sort(domain[0]))
+ m.raise_exception("Invalid str.from_ubv expects one bit-vector argument");
+ sort* rng = m_string;
+ return m.mk_func_decl(symbol("str.from_ubv"), arity, domain, rng, func_decl_info(m_family_id, OP_STRING_UBVTOS));
+}
+
func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string, bool is_right) {
ast_manager& m = *m_manager;
sort_ref rng(m);
@@ -400,14 +411,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_STRING_STOI:
case OP_STRING_LT:
case OP_STRING_LE:
- match(*m_sigs[k], arity, domain, range, rng);
- return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
case OP_STRING_IS_DIGIT:
case OP_STRING_TO_CODE:
case OP_STRING_FROM_CODE:
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
-
+ case OP_STRING_UBVTOS:
+ return mk_ubv2s(arity, domain);
+
case _OP_REGEXP_FULL_CHAR:
m_has_re = true;
if (!range) range = mk_reglan();
@@ -615,6 +626,7 @@ void seq_decl_plugin::get_op_names(svector & op_names, symbol cons
op_names.push_back(builtin_name("int.to.str", OP_STRING_ITOS));
op_names.push_back(builtin_name("re.nostr", _OP_REGEXP_EMPTY));
op_names.push_back(builtin_name("re.complement", OP_RE_COMPLEMENT));
+ op_names.push_back(builtin_name("str.from_ubv", OP_STRING_UBVTOS));
}
void seq_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) {
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 8ce0f7a4e..61bbf7ba1 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -79,6 +79,7 @@ enum seq_op_kind {
OP_STRING_CONST,
OP_STRING_ITOS,
OP_STRING_STOI,
+ OP_STRING_UBVTOS,
OP_STRING_LT,
OP_STRING_LE,
OP_STRING_IS_DIGIT,
@@ -149,6 +150,7 @@ class seq_decl_plugin : public decl_plugin {
func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq);
func_decl* mk_left_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq);
func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq, bool is_right);
+ func_decl* mk_ubv2s(unsigned arity, sort* const* domain);
void init();
@@ -294,6 +296,7 @@ public:
app* mk_char_bit(expr* e, unsigned i);
app* mk_itos(expr* i) const { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); }
app* mk_stoi(expr* s) const { return m.mk_app(m_fid, OP_STRING_STOI, 1, &s); }
+ app* mk_ubv2s(expr* b) const { return m.mk_app(m_fid, OP_STRING_UBVTOS, 1, &b); }
app* mk_is_empty(expr* s) const;
app* mk_lex_lt(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LT, 2, es); }
app* mk_lex_le(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LE, 2, es); }
@@ -332,6 +335,7 @@ public:
bool is_suffix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); }
bool is_itos(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
bool is_stoi(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STOI); }
+ bool is_ubv2s(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_UBVTOS); }
bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
bool is_lt(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_LT); }
@@ -369,6 +373,7 @@ public:
MATCH_BINARY(is_le);
MATCH_UNARY(is_itos);
MATCH_UNARY(is_stoi);
+ MATCH_UNARY(is_ubv2s);
MATCH_UNARY(is_is_digit);
MATCH_UNARY(is_from_code);
MATCH_UNARY(is_to_code);
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index e8c9bb54f..f66c4a331 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -286,11 +286,9 @@ namespace euf {
void solver::asserted(literal l) {
expr* e = m_bool_var2expr.get(l.var(), nullptr);
- if (!e) {
- TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << "\n";);
+ TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
+ if (!e)
return;
- }
- TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
euf::enode* n = m_egraph.find(e);
if (!n)
return;
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index e1dd99b64..c5aa68e0a 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -79,6 +79,9 @@ namespace smt {
void add_stoi_axiom(expr* n) { m_ax.stoi_axiom(n); }
void add_stoi_axiom(expr* e, unsigned k) { m_ax.stoi_axiom(e, k); }
void add_itos_axiom(expr* s, unsigned k) { m_ax.itos_axiom(s, k); }
+ void add_ubv2s_axiom(expr* b, unsigned k) { m_ax.ubv2s_axiom(b, k); }
+ void add_ubv2s_len_axiom(expr* b, unsigned k) { m_ax.ubv2s_len_axiom(b, k); }
+ void add_ubv2ch_axioms(sort* s) { m_ax.ubv2ch_axiom(s); }
void add_lt_axiom(expr* n) { m_ax.lt_axiom(n); }
void add_le_axiom(expr* n) { m_ax.le_axiom(n); }
void add_is_digit_axiom(expr* n) { m_ax.is_digit_axiom(n); }
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 9f1103da2..ba601272d 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -735,10 +735,6 @@ namespace smt {
else if (m_params.m_string_solver == "none") {
// don't register any solver.
}
- else if (m_params.m_string_solver == "char") {
- setup_QF_BV();
- setup_char();
- }
else {
throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
}
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index da6b1415e..c4bf2634b 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -262,6 +262,7 @@ theory_seq::theory_seq(context& ctx):
m_axioms(m),
m_axioms_head(0),
m_int_string(m),
+ m_ubv_string(m),
m_length(m),
m_length_limit(m),
m_mg(nullptr),
@@ -368,6 +369,11 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("int_string");
return FC_CONTINUE;
}
+ if (check_ubv_string()) {
+ ++m_stats.m_ubv_string;
+ TRACEFIN("ubv_string");
+ return FC_CONTINUE;
+ }
if (reduce_length_eq()) {
++m_stats.m_branch_variable;
TRACEFIN("reduce_length");
@@ -1525,6 +1531,77 @@ bool theory_seq::add_length_to_eqc(expr* e) {
return change;
}
+void theory_seq::add_ubv_string(expr* e) {
+ bool has_sort = false;
+ expr* b = nullptr;
+ VERIFY(m_util.str.is_ubv2s(e, b));
+ for (auto* e2 : m_ubv_string) {
+ expr* b2 = nullptr;
+ VERIFY(m_util.str.is_ubv2s(e2, b2));
+ has_sort |= b2->get_sort() == b->get_sort();
+ }
+ if (!has_sort)
+ m_ax.add_ubv2ch_axioms(b->get_sort());
+ m_ubv_string.push_back(e);
+ m_trail_stack.push(push_back_vector(m_ubv_string));
+ add_length_to_eqc(e);
+}
+
+bool theory_seq::check_ubv_string() {
+ bool change = false;
+ for (expr* e : m_ubv_string) {
+ if (check_ubv_string(e))
+ change = true;
+ }
+ return change;
+}
+
+bool theory_seq::check_ubv_string(expr* e) {
+ expr* n = nullptr;
+ if (ctx.inconsistent())
+ return true;
+ if (m_has_ubv_axiom.contains(e))
+ return false;
+ expr* b = nullptr;
+ bv_util bv(m);
+ VERIFY(m_util.str.is_ubv2s(e, b));
+ rational len;
+ if (get_length(e, len) && len.is_unsigned())
+ m_ax.add_ubv2s_len_axiom(b, len.get_unsigned());
+
+
+ unsigned sz = bv.get_bv_size(b);
+ rational value(0);
+ bool all_bits_assigned = true;
+ for (unsigned i = 0; i < sz; ++i) {
+ expr_ref bit(bv.mk_bit2bool(b, i), m);
+ literal lit = mk_literal(bit);
+ switch (ctx.get_assignment(lit)) {
+ case l_undef:
+ ctx.mark_as_relevant(lit);
+ all_bits_assigned = false;
+ break;
+ case l_true:
+ value += rational::power_of_two(i);
+ break;
+ case l_false:
+ break;
+ }
+ }
+ if (!all_bits_assigned)
+ return true;
+ unsigned k = 0;
+ while (value >= 10) {
+ k++;
+ value = div(value, rational(10));
+ }
+
+ m_has_ubv_axiom.insert(e);
+ m_trail_stack.push(insert_obj_trail(m_has_ubv_axiom, e));
+ m_ax.add_ubv2s_axiom(b, k);
+ return true;
+}
+
void theory_seq::add_int_string(expr* e) {
m_int_string.push_back(e);
m_trail_stack.push(push_back_vector(m_int_string));
@@ -1761,6 +1838,7 @@ void theory_seq::collect_statistics(::statistics & st) const {
st.update("seq extensionality", m_stats.m_extensionality);
st.update("seq fixed length", m_stats.m_fixed_length);
st.update("seq int.to.str", m_stats.m_int_string);
+ st.update("seq str.from_ubv", m_stats.m_ubv_string);
}
void theory_seq::init_search_eh() {
@@ -3099,6 +3177,9 @@ void theory_seq::relevant_eh(app* n) {
add_int_string(n);
}
+ if (m_util.str.is_ubv2s(n))
+ add_ubv_string(n);
+
expr* arg = nullptr;
if (m_sk.is_tail(n, arg)) {
add_length_limit(arg, m_max_unfolding_depth, true);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index b7ea9517a..ad6ef0695 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -323,6 +323,7 @@ namespace smt {
unsigned m_fixed_length;
unsigned m_propagate_contains;
unsigned m_int_string;
+ unsigned m_ubv_string;
};
typedef hashtable rational_set;
@@ -348,6 +349,8 @@ namespace smt {
unsigned m_axioms_head; // index of first axiom to add.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
expr_ref_vector m_int_string;
+ expr_ref_vector m_ubv_string; // list all occurrences of str.from_ubv that have been seen
+ obj_hashtable m_has_ubv_axiom; // keep track of ubv that have been axiomatized within scope.
obj_hashtable m_has_length; // is length applied
expr_ref_vector m_length; // length applications themselves
obj_map m_length_limit_map; // sequences that have length limit predicates
@@ -569,6 +572,11 @@ namespace smt {
bool branch_itos();
bool branch_itos(expr* e);
+ // functions that convert ubv to string
+ void add_ubv_string(expr* e);
+ bool check_ubv_string();
+ bool check_ubv_string(expr* e);
+
expr_ref add_elim_string_axiom(expr* n);
void add_in_re_axiom(expr* n);
literal mk_simplified_literal(expr* n);