mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

adding access to characters over API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-13 15:56:08 +02:00
parent 3a402ca2c1
commit 7ae78da850
8 changed files with 128 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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

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

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