mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-15 00:05:13 +02:00
parent 4c6e2acd45 79c261736b
commit db3c42b02d
32 changed files with 521 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
CMakeLists.txt
View file

@ -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

5
RELEASE_NOTES
View file

@ -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.

2
scripts/mk_project.py
View file

@ -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():

3
scripts/release.yml
View file

@ -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"

1
src/api/api_ast.cpp
View file

@ -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;

20
src/api/api_seq.cpp
View file

@ -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) {

15
src/api/c++/z3++.h
View file

@ -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); }

1
src/api/dotnet/CMakeLists.txt
View file

@ -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

35
src/api/dotnet/CharSort.cs Normal file
View file

@ -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
{
/// <summary>
/// A Character sort
/// </summary>
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
}
}

26
src/api/dotnet/Context.cs
View file

@ -89,7 +89,6 @@ namespace Microsoft.Z3
/// </remarks>
public IntSymbol MkSymbol(int i)
{
return new IntSymbol(this, i);
}
@ -98,7 +97,6 @@ namespace Microsoft.Z3
/// </summary>
public StringSymbol MkSymbol(string name)
{
return new StringSymbol(this, name);
}
@ -107,7 +105,6 @@ namespace Microsoft.Z3
/// </summary>
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;
/// <summary>
/// Retrieves the Boolean sort of the context.
@ -155,6 +153,18 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Retrieves the String sort of the context.
/// </summary>
public CharSort CharSort
{
get
{
if (m_charSort == null) m_charSort = new CharSort(this); return m_charSort;
}
}
/// <summary>
/// Retrieves the String sort of the context.
/// </summary>
@ -2385,6 +2395,16 @@ namespace Microsoft.Z3
return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
}
/// <summary>
/// Convert a bit-vector expression, represented as an unsigned number, to a string.
/// </summary>
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));
}
/// <summary>
/// Convert an integer expression to a string.
/// </summary>

5
src/api/dotnet/SeqSort.cs
View file

@ -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
}
}

1
src/api/java/CMakeLists.txt
View file

@ -108,6 +108,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
BitVecSort.java
BoolExpr.java
BoolSort.java
CharSort.java
ConstructorDecRefQueue.java
Constructor.java
ConstructorListDecRefQueue.java

33
src/api/java/CharSort.java Normal file
View file

@ -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())); { }}
}

59
src/api/java/Context.java
View file

@ -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<BitVecSort> m_stringSort = null;
private SeqSort<CharSort> 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<BitVecSort> getStringSort()
public CharSort mkCharSort()
{
return new CharSort(this);
}
/**
* Retrieves the String sort of the context.
**/
public SeqSort<CharSort> getStringSort()
{
if (m_stringSort == null) {
m_stringSort = mkStringSort();
@ -239,7 +248,7 @@ public class Context implements AutoCloseable {
/**
* Create a new string sort
**/
public SeqSort<BitVecSort> mkStringSort()
public SeqSort<CharSort> mkStringSort()
{
return new SeqSort<>(this, Native.mkStringSort(nCtx()));
}
@ -2006,23 +2015,31 @@ public class Context implements AutoCloseable {
/**
* Create a string constant.
*/
public SeqExpr<BitVecSort> mkString(String s)
public SeqExpr<CharSort> mkString(String s)
{
return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkString(nCtx(), s));
return (SeqExpr<CharSort>) Expr.create(this, Native.mkString(nCtx(), s));
}
/**
* Convert an integer expression to a string.
*/
public SeqExpr<BitVecSort> intToString(Expr<IntSort> e)
public SeqExpr<CharSort> intToString(Expr<IntSort> e)
{
return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
return (SeqExpr<CharSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
}
/**
* Convert an unsigned bitvector expression to a string.
*/
public SeqExpr<CharSort> ubvToString(Expr<BitVecSort> e)
{
return (SeqExpr<CharSort>) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
}
/**
* Convert an integer expression to a string.
*/
public IntExpr stringToInt(Expr<SeqSort<BitVecSort>> e)
public IntExpr stringToInt(Expr<SeqSort<CharSort>> 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 <R extends Sort> IntExpr mkLength(Expr<SeqSort<BitVecSort>> s)
public <R extends Sort> IntExpr mkLength(Expr<SeqSort<R>> 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 <R extends Sort> BoolExpr mkPrefixOf(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
public <R extends Sort> BoolExpr mkPrefixOf(Expr<SeqSort<R>> s1, Expr<SeqSort<R>> 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 <R extends Sort> BoolExpr mkSuffixOf(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
public <R extends Sort> BoolExpr mkSuffixOf(Expr<SeqSort<R>> s1, Expr<SeqSort<R>> 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 <R extends Sort> BoolExpr mkContains(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
public <R extends Sort> BoolExpr mkContains(Expr<SeqSort<R>> s1, Expr<SeqSort<R>> 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 <R extends Sort> SeqExpr<R> mkAt(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> index)
public <R extends Sort> SeqExpr<R> mkAt(Expr<SeqSort<R>> s, Expr<IntSort> index)
{
checkContextMatch(s, index);
return (SeqExpr<R>) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
@ -2086,7 +2103,7 @@ public class Context implements AutoCloseable {
/**
* Retrieve element at index.
*/
public <R extends Sort> Expr<R> MkNth(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> index)
public <R extends Sort> Expr<R> MkNth(Expr<SeqSort<R>> s, Expr<IntSort> index)
{
checkContextMatch(s, index);
return (Expr<R>) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
@ -2096,7 +2113,7 @@ public class Context implements AutoCloseable {
/**
* Extract subsequence.
*/
public <R extends Sort> SeqExpr<R> mkExtract(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> offset, Expr<IntSort> length)
public <R extends Sort> SeqExpr<R> mkExtract(Expr<SeqSort<R>> s, Expr<IntSort> offset, Expr<IntSort> length)
{
checkContextMatch(s, offset, length);
return (SeqExpr<R>) 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 <R extends Sort> IntExpr mkIndexOf(Expr<SeqSort<BitVecSort>> s, Expr<SeqSort<BitVecSort>> substr, Expr<IntSort> offset)
public <R extends Sort> IntExpr mkIndexOf(Expr<SeqSort<R>> s, Expr<SeqSort<R>> substr, Expr<IntSort> 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 <R extends Sort> SeqExpr<R> mkReplace(Expr<SeqSort<BitVecSort>> s, Expr<SeqSort<BitVecSort>> src, Expr<SeqSort<BitVecSort>> dst)
public <R extends Sort> SeqExpr<R> mkReplace(Expr<SeqSort<R>> s, Expr<SeqSort<R>> src, Expr<SeqSort<R>> dst)
{
checkContextMatch(s, src, dst);
return (SeqExpr<R>) 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 <R extends Sort> ReExpr<R> mkToRe(Expr<SeqSort<BitVecSort>> s)
public <R extends Sort> ReExpr<R> mkToRe(Expr<SeqSort<R>> s)
{
checkContextMatch(s);
return (ReExpr<R>) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
@ -2133,7 +2150,7 @@ public class Context implements AutoCloseable {
/**
* Check for regular expression membership.
*/
public <R extends Sort> BoolExpr mkInRe(Expr<SeqSort<BitVecSort>> s, Expr<ReSort<R>> re)
public <R extends Sort> BoolExpr mkInRe(Expr<SeqSort<R>> s, Expr<ReSort<R>> 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 <R extends Sort> ReExpr<R> mkRange(Expr<SeqSort<BitVecSort>> lo, Expr<SeqSort<BitVecSort>> hi)
public <R extends Sort> ReExpr<R> mkRange(Expr<SeqSort<CharSort>> lo, Expr<SeqSort<CharSort>> hi)
{
checkContextMatch(lo, hi);
return (ReExpr<R>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));

1
src/api/java/SeqSort.java
View file

@ -27,3 +27,4 @@ public class SeqSort<R extends Sort> extends Sort
super(ctx, obj);
}
}

31
src/api/z3_api.h
View file

@ -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.

4
src/ast/ast_ll_pp.cpp
View file

@ -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)) {

61
src/ast/rewriter/seq_axioms.cpp
View file

@ -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)

3
src/ast/rewriter/seq_axioms.h
View file

@ -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);

108
src/ast/rewriter/seq_eq_solver.cpp
View file

@ -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

6
src/ast/rewriter/seq_eq_solver.h
View file

@ -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<expr>& xs, ptr_vector<expr>& ys, expr_ref& y);
bool reduce_binary_eq(eqr const& e, eq_ptr& r);

20
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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)) {

1
src/ast/rewriter/seq_rewriter.h
View file

@ -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);

3
src/ast/rewriter/seq_skolem.cpp
View file

@ -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);
}

2
src/ast/rewriter/seq_skolem.h
View file

@ -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);

18
src/ast/seq_decl_plugin.cpp
View file

@ -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<builtin_name> & 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<builtin_name> & sort_names, symbol const & logic) {

5
src/ast/seq_decl_plugin.h
View file

@ -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);

6
src/sat/smt/euf_solver.cpp
View file

@ -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;

3
src/smt/seq_axioms.h
View file

@ -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); }

4
src/smt/smt_setup.cpp
View file

@ -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'");
}

81
src/smt/theory_seq.cpp
View file

@ -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<expr_ref_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<expr>(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<expr_ref_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);

8
src/smt/theory_seq.h
View file

@ -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, rational::hash_proc, rational::eq_proc> 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<expr> m_has_ubv_axiom; // keep track of ubv that have been axiomatized within scope.
obj_hashtable<expr> m_has_length; // is length applied
expr_ref_vector m_length; // length applications themselves
obj_map<expr, unsigned> 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);