diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 4b4574b65c3..10a98c4778c 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -719,7 +719,7 @@ extern "C" { else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) { return Z3_RE_SORT; } - else if (fid == mk_c(c)->get_char_fid() && k == CHAR_SORT) { + else if (fid == mk_c(c)->get_char_fid() && k == CHAR_SORT) { return Z3_CHAR_SORT; } else { @@ -1230,6 +1230,18 @@ extern "C" { } } + if (mk_c(c)->get_char_fid() == _d->get_family_id()) { + switch (_d->get_decl_kind()) { + case OP_CHAR_LE: return Z3_OP_CHAR_LE; + case OP_CHAR_TO_INT: return Z3_OP_CHAR_TO_INT; + case OP_CHAR_TO_BV: return Z3_OP_CHAR_TO_BV; + case OP_CHAR_FROM_BV: return Z3_OP_CHAR_FROM_BV; + case OP_CHAR_IS_DIGIT: return Z3_OP_CHAR_IS_DIGIT; + default: + return Z3_OP_INTERNAL; + } + } + if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) { switch (_d->get_decl_kind()) { case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 01e93235305..f0f1d903eab 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -275,6 +275,11 @@ extern "C" { MK_SORTED(Z3_mk_re_empty, mk_c(c)->sutil().re.mk_empty); MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full_seq); + MK_BINARY(Z3_mk_char_le, mk_c(c)->get_char_fid(), OP_CHAR_LE, SKIP); + MK_UNARY(Z3_mk_char_to_int, mk_c(c)->get_char_fid(), OP_CHAR_TO_INT, SKIP); + MK_UNARY(Z3_mk_char_to_bv, mk_c(c)->get_char_fid(), OP_CHAR_TO_BV, SKIP); + MK_UNARY(Z3_mk_char_from_bv, mk_c(c)->get_char_fid(), OP_CHAR_FROM_BV, SKIP); + MK_UNARY(Z3_mk_char_is_digit, mk_c(c)->get_char_fid(), OP_CHAR_IS_DIGIT, SKIP); }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index d715c73cb75..754f78857e3 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1445,6 +1445,26 @@ namespace z3 { check_error(); return expr(ctx(), r); } + expr char_to_int() const { + Z3_ast r = Z3_mk_char_to_int(ctx(), *this); + check_error(); + return expr(ctx(), r); + } + expr char_to_bv() const { + Z3_ast r = Z3_mk_char_to_bv(ctx(), *this); + check_error(); + return expr(ctx(), r); + } + expr char_from_bv() const { + Z3_ast r = Z3_mk_char_from_bv(ctx(), *this); + check_error(); + return expr(ctx(), r); + } + expr is_digit() const { + Z3_ast r = Z3_mk_char_is_digit(ctx(), *this); + check_error(); + return expr(ctx(), r); + } friend expr range(expr const& lo, expr const& hi); /** diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 7279fe84725..07759b1fae4 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -567,7 +567,7 @@ public void AddRecDef(FuncDecl f, Expr[] args, Expr body) CheckContextMatch(body); IntPtr[] argsNative = AST.ArrayToNative(args); Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); - } + } /// /// Creates a new function declaration. @@ -2693,7 +2693,53 @@ public ReExpr MkRange(SeqExpr lo, SeqExpr hi) CheckContextMatch(lo, hi); return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject)); } - + + /// + /// Create less than or equal to between two characters. + /// + public BoolExpr MkCharLe(Expr ch1, Expr ch2) + { + Debug.Assert(ch1 != null); + Debug.Assert(ch2 != null); + return new BoolExpr(this, Native.Z3_mk_char_le(nCtx, ch1.NativeObject, ch2.NativeObject)); + } + + /// + /// Create an integer (code point) from character. + /// + public IntExpr CharToInt(Expr ch) + { + Debug.Assert(ch != null); + return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject)); + } + + /// + /// Create a bit-vector (code point) from character. + /// + public BitVecExpr CharToBV(Expr ch) + { + Debug.Assert(ch != null); + return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject)); + } + + /// + /// Create a character from a bit-vector (code point). + /// + public Expr CharFromBV(BitVecExpr bv) + { + Debug.Assert(bv != null); + return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject)); + } + + /// + /// Create a check if the character is a digit. + /// + public BoolExpr MkIsDigit(Expr ch) + { + Debug.Assert(ch != null); + return new BoolExpr(this, Native.Z3_mk_char_is_digit(nCtx, ch.NativeObject)); + } + #endregion #region Pseudo-Boolean constraints diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 1e581c4826a..6b49e9e2770 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -508,11 +508,11 @@ public FuncDecl mkRecFuncDecl(Symbol name, Sort[] domain, R */ public void AddRecDef(FuncDecl f, Expr[] args, Expr body) { - checkContextMatch(f); - checkContextMatch(args); - checkContextMatch(body); - long[] argsNative = AST.arrayToNative(args); - Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject()); + checkContextMatch(f); + checkContextMatch(args); + checkContextMatch(body); + long[] argsNative = AST.arrayToNative(args); + Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject()); } /** @@ -2025,7 +2025,7 @@ public SeqExpr mkString(String s) */ 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())); } /** @@ -2033,7 +2033,7 @@ public SeqExpr intToString(Expr e) */ public SeqExpr ubvToString(Expr e) { - return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject())); } /** @@ -2041,7 +2041,7 @@ public SeqExpr ubvToString(Expr e) */ public SeqExpr sbvToString(Expr e) { - return (SeqExpr) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject())); } /** @@ -2049,7 +2049,7 @@ public SeqExpr sbvToString(Expr e) */ public IntExpr stringToInt(Expr> e) { - return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject())); + return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject())); } /** @@ -2111,7 +2111,7 @@ public SeqExpr mkAt(Expr> s, Expr index) /** * 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())); @@ -2252,7 +2252,7 @@ public final ReExpr mkIntersect(Expr>... t) */ public ReExpr mkEmptyRe(R s) { - return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject())); } /** @@ -2260,7 +2260,7 @@ public ReExpr mkEmptyRe(R s) */ public ReExpr mkFullRe(R s) { - return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); } /** @@ -2272,6 +2272,50 @@ public ReExpr mkRange(Expr> lo, Expr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject())); } + /** + * Create less than or equal to between two characters. + */ + public BoolExpr mkCharLe(Expr ch1, Expr ch2) + { + checkContextMatch(ch1, ch2); + return (BoolExpr) Expr.create(this, Native.mkCharLe(nCtx(), ch1.getNativeObject(), ch2.getNativeObject())); + } + + /** + * Create an integer (code point) from character. + */ + public IntExpr charToInt(Expr ch) + { + checkContextMatch(ch); + return (IntExpr) Expr.create(this, Native.mkCharToInt(nCtx(), ch.getNativeObject())); + } + + /** + * Create a bit-vector (code point) from character. + */ + public BitVecExpr charToBv(Expr ch) + { + checkContextMatch(ch); + return (BitVecExpr) Expr.create(this, Native.mkCharToBv(nCtx(), ch.getNativeObject())); + } + + /** + * Create a character from a bit-vector (code point). + */ + public Expr charFromBv(BitVecExpr bv) + { + checkContextMatch(bv); + return (Expr) Expr.create(this, Native.mkCharFromBv(nCtx(), bv.getNativeObject())); + } + + /** + * Create a check if the character is a digit. + */ + public BoolExpr mkIsDigit(Expr ch) + { + checkContextMatch(ch); + return (BoolExpr) Expr.create(this, Native.mkCharIsDigit(nCtx(), ch.getNativeObject())); + } /** * Create an at-most-k constraint. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ac7a23a6e51..a15e77788eb 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1221,6 +1221,13 @@ typedef enum { Z3_OP_RE_FULL_SET, Z3_OP_RE_COMPLEMENT, + // char + Z3_OP_CHAR_LE, + Z3_OP_CHAR_TO_INT, + Z3_OP_CHAR_TO_BV, + Z3_OP_CHAR_FROM_BV, + Z3_OP_CHAR_IS_DIGIT, + // Auxiliary Z3_OP_LABEL = 0x700, Z3_OP_LABEL_LIT, @@ -1533,6 +1540,7 @@ extern "C" { - model model generation for solvers, this parameter can be overwritten when creating a solver - model_validate validate models produced by solvers - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver + - encoding the string encoding used internally (must be either "unicode" - 18 bit, "bmp" - 16 bit or "ascii" - 8 bit) \sa Z3_set_param_value \sa Z3_del_config @@ -3442,7 +3450,7 @@ extern "C" { /** \brief Create a sort for unicode strings. - def_API('Z3_mk_string_sort', SORT ,(_in(CONTEXT), )) + def_API('Z3_mk_string_sort', SORT, (_in(CONTEXT), )) */ Z3_sort Z3_API Z3_mk_string_sort(Z3_context c); @@ -3452,7 +3460,7 @@ extern "C" { 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), )) + def_API('Z3_mk_char_sort', SORT, (_in(CONTEXT), )) */ Z3_sort Z3_API Z3_mk_char_sort(Z3_context c); @@ -3472,7 +3480,7 @@ extern "C" { /** \brief Create a string constant out of the string that is passed in - def_API('Z3_mk_string' ,AST ,(_in(CONTEXT), _in(STRING))) + def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING))) */ Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s); @@ -3481,7 +3489,7 @@ extern "C" { It takes the length of the string as well to take into account 0 characters. The string is unescaped. - def_API('Z3_mk_lstring' ,AST ,(_in(CONTEXT), _in(UINT), _in(STRING))) + def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING))) */ Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s); @@ -3497,7 +3505,7 @@ extern "C" { \pre Z3_is_string(c, s) - def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST))) + def_API('Z3_get_string', STRING, (_in(CONTEXT), _in(AST))) */ Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s); @@ -3506,7 +3514,7 @@ extern "C" { \pre Z3_is_string(c, s) - def_API('Z3_get_lstring' ,CHAR_PTR ,(_in(CONTEXT), _in(AST), _out(UINT))) + def_API('Z3_get_lstring', CHAR_PTR, (_in(CONTEXT), _in(AST), _out(UINT))) */ Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length); @@ -3515,14 +3523,14 @@ extern "C" { \pre s is a sequence sort. - def_API('Z3_mk_seq_empty' ,AST ,(_in(CONTEXT), _in(SORT))) + def_API('Z3_mk_seq_empty', AST ,(_in(CONTEXT), _in(SORT))) */ Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq); /** \brief Create a unit sequence of \c a. - def_API('Z3_mk_seq_unit' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_seq_unit', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a); @@ -3531,7 +3539,7 @@ extern "C" { \pre n > 0 - def_API('Z3_mk_seq_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + def_API('Z3_mk_seq_concat', AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) */ Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]); @@ -3540,7 +3548,7 @@ extern "C" { \pre prefix and s are the same sequence sorts. - def_API('Z3_mk_seq_prefix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_prefix', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s); @@ -3549,7 +3557,7 @@ extern "C" { \pre \c suffix and \c s are the same sequence sorts. - def_API('Z3_mk_seq_suffix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_suffix', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s); @@ -3558,7 +3566,7 @@ extern "C" { \pre \c container and \c containee are the same sequence sorts. - def_API('Z3_mk_seq_contains' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_contains', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee); @@ -3568,7 +3576,7 @@ extern "C" { \pre \c s1 and \c s2 are strings - def_API('Z3_mk_str_lt' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_str_lt', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s); @@ -3577,21 +3585,21 @@ extern "C" { \pre \c s1 and \c s2 are strings - def_API('Z3_mk_str_le' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_str_le', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s); /** \brief Extract subsequence starting at \c offset of \c length. - def_API('Z3_mk_seq_extract' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + def_API('Z3_mk_seq_extract', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length); /** \brief Replace the first occurrence of \c src with \c dst in \c s. - def_API('Z3_mk_seq_replace' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + def_API('Z3_mk_seq_replace', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst); @@ -3599,7 +3607,7 @@ extern "C" { \brief Retrieve from \c s the unit sequence positioned at position \c index. The sequence is empty if the index is out of bounds. - def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_at', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index); @@ -3607,14 +3615,14 @@ extern "C" { \brief Retrieve from \c s the element positioned at position \c index. The function is under-specified if the index is out of bounds. - def_API('Z3_mk_seq_nth' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_nth', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index); /** \brief Return the length of the sequence \c s. - def_API('Z3_mk_seq_length' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_seq_length', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s); @@ -3624,7 +3632,7 @@ extern "C" { If \c s does not contain \c substr, then the value is -1, if \c offset is the length of \c s, then the value is -1 as well. The value is -1 if \c offset is negative or larger than the length of \c s. - def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + def_API('Z3_mk_seq_index', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset); @@ -3638,7 +3646,7 @@ extern "C" { /** \brief Convert string to integer. - def_API('Z3_mk_str_to_int' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_str_to_int', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s); @@ -3646,56 +3654,56 @@ extern "C" { /** \brief Integer to string conversion. - def_API('Z3_mk_int_to_str' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_int_to_str', AST ,(_in(CONTEXT), _in(AST))) */ 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))) + 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 Signed bit-vector to string conversion. - def_API('Z3_mk_sbv_to_str' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_sbv_to_str', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s); /** \brief Create a regular expression that accepts the sequence \c seq. - def_API('Z3_mk_seq_to_re' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_seq_to_re', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq); /** \brief Check if \c seq is in the language generated by the regular expression \c re. - def_API('Z3_mk_seq_in_re' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_in_re', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re); /** \brief Create the regular language \c re+. - def_API('Z3_mk_re_plus' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_re_plus', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re); /** \brief Create the regular language \c re*. - def_API('Z3_mk_re_star' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_re_star', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re); /** \brief Create the regular language \c [re]. - def_API('Z3_mk_re_option' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_re_option', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re); @@ -3704,7 +3712,7 @@ extern "C" { \pre n > 0 - def_API('Z3_mk_re_union' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + def_API('Z3_mk_re_union', AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) */ Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]); @@ -3713,7 +3721,7 @@ extern "C" { \pre n > 0 - def_API('Z3_mk_re_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + def_API('Z3_mk_re_concat', AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) */ Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]); @@ -3721,7 +3729,7 @@ extern "C" { /** \brief Create the range regular expression over two sequences of length 1. - def_API('Z3_mk_re_range' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_re_range', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi); @@ -3748,14 +3756,14 @@ extern "C" { \pre n > 0 - def_API('Z3_mk_re_intersect' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + def_API('Z3_mk_re_intersect', AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) */ Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[]); /** \brief Create the complement of the regular language \c re. - def_API('Z3_mk_re_complement' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_re_complement', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re); @@ -3764,7 +3772,7 @@ extern "C" { \pre re is a regular expression sort. - def_API('Z3_mk_re_empty' ,AST ,(_in(CONTEXT), _in(SORT))) + def_API('Z3_mk_re_empty', AST ,(_in(CONTEXT), _in(SORT))) */ Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re); @@ -3774,10 +3782,45 @@ extern "C" { \pre re is a regular expression sort. - def_API('Z3_mk_re_full' ,AST ,(_in(CONTEXT), _in(SORT))) + def_API('Z3_mk_re_full', AST ,(_in(CONTEXT), _in(SORT))) */ Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re); + /** + \brief Create less than or equal to between two characters. + + def_API('Z3_mk_char_le', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_le(Z3_context c, Z3_ast ch1, Z3_ast ch2); + + /** + \brief Create an integer (code point) from character. + + def_API('Z3_mk_char_to_int', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch); + + /** + \brief Create a bit-vector (code point) from character. + + def_API('Z3_mk_char_to_bv', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch); + + /** + \brief Create a character from a bit-vector (code point). + + def_API('Z3_mk_char_from_bv', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv); + + /** + \brief Create a check if the character is a digit. + + def_API('Z3_mk_char_is_digit', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch); + /*@}*/ diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index 0f6f78486a4..2ab4def9aa8 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -90,7 +90,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, else if (!b.is_bv_sort(domain[0]) || b.get_bv_size(domain[0]) != num_bits()) msg << "expected bit-vector sort argument with " << num_bits(); else { - m.mk_func_decl(symbol("char.to_bv"), arity, domain, m_char, func_decl_info(m_family_id, k, 0, nullptr)); + return m.mk_func_decl(symbol("char.from_bv"), arity, domain, m_char, func_decl_info(m_family_id, k, 0, nullptr)); } m.raise_exception(msg.str()); }