From 7ae78da850212441f0d5ab8c8e1df6d693044e15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 15:56:08 +0200 Subject: [PATCH] adding access to characters over API Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 1 + src/api/api_seq.cpp | 20 +++++++++++++ src/api/c++/z3++.h | 8 ++++- src/api/java/CMakeLists.txt | 1 + src/api/java/CharSort.java | 33 +++++++++++++++++++++ src/api/java/Context.java | 59 ++++++++++++++++++++++++------------- src/api/java/SeqSort.java | 1 + src/api/z3_api.h | 31 ++++++++++++++++--- 8 files changed, 128 insertions(+), 26 deletions(-) create mode 100644 src/api/java/CharSort.java 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..4403d1605 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1437,7 +1437,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 +3204,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/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..a7d541242 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.