Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added character functions to API #5549

Merged
merged 2 commits into from
Sep 15, 2021
Merged

Added character functions to API #5549

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6c190f0
Added character functions to API
CEisenhofer Sep 15, 2021
f324d3c
Changed names of c++ functions
CEisenhofer Sep 15, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 13 additions & 1 deletion src/api/api_ast.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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;
Expand Down
5 changes: 5 additions & 0 deletions src/api/api_seq.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);


};
25 changes: 25 additions & 0 deletions src/api/c++/z3++.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1445,6 +1445,31 @@ namespace z3 {
check_error();
return expr(ctx(), r);
}
expr charle() const {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Naming conventions elsewhere:
char_le
char_to_int
char_to_bv
...

Z3_ast r = Z3_mk_char_le(ctx(), *this);
check_error();
return expr(ctx(), r);
}
expr chartoint() const {
Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
check_error();
return expr(ctx(), r);
}
expr chartobv() const {
Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
check_error();
return expr(ctx(), r);
}
expr charfrombv() const {
Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
check_error();
return expr(ctx(), r);
}
expr isdigit() 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);
/**
Expand Down
50 changes: 48 additions & 2 deletions src/api/dotnet/Context.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}

/// <summary>
/// Creates a new function declaration.
Expand Down Expand Up @@ -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));
}


/// <summary>
/// Create less than or equal to between two characters.
/// </summary>
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));
}

/// <summary>
/// Create an integer (code point) from character.
/// </summary>
public IntExpr CharToInt(Expr ch)
{
Debug.Assert(ch != null);
return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject));
}

/// <summary>
/// Create a bit-vector (code point) from character.
/// </summary>
public BitVecExpr CharToBV(Expr ch)
{
Debug.Assert(ch != null);
return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject));
}

/// <summary>
/// Create a character from a bit-vector (code point).
/// </summary>
public Expr CharFromBV(BitVecExpr bv)
{
Debug.Assert(bv != null);
return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject));
}

/// <summary>
/// Create a check if the character is a digit.
/// </summary>
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
Expand Down
68 changes: 56 additions & 12 deletions src/api/java/Context.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -508,11 +508,11 @@ public <R extends Sort> FuncDecl<R> mkRecFuncDecl(Symbol name, Sort[] domain, R
*/
public <R extends Sort> void AddRecDef(FuncDecl<R> f, Expr<?>[] args, Expr<R> 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());
}

/**
Expand Down Expand Up @@ -2025,31 +2025,31 @@ public SeqExpr<CharSort> mkString(String s)
*/
public SeqExpr<CharSort> intToString(Expr<IntSort> e)
{
return (SeqExpr<CharSort>) 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()));
return (SeqExpr<CharSort>) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
}

/**
* Convert an signed bitvector expression to a string.
*/
public SeqExpr<CharSort> sbvToString(Expr<BitVecSort> e)
{
return (SeqExpr<CharSort>) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
return (SeqExpr<CharSort>) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
}

/**
* Convert an integer expression to a string.
*/
public IntExpr stringToInt(Expr<SeqSort<CharSort>> e)
{
return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
}

/**
Expand Down Expand Up @@ -2111,7 +2111,7 @@ public <R extends Sort> SeqExpr<R> mkAt(Expr<SeqSort<R>> s, Expr<IntSort> index)
/**
* Retrieve element at index.
*/
public <R extends Sort> Expr<R> MkNth(Expr<SeqSort<R>> 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()));
Expand Down Expand Up @@ -2252,15 +2252,15 @@ public final <R extends Sort> ReExpr<R> mkIntersect(Expr<ReSort<R>>... t)
*/
public <R extends Sort> ReExpr<R> mkEmptyRe(R s)
{
return (ReExpr<R>) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
return (ReExpr<R>) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
}

/**
* Create the full regular expression.
*/
public <R extends Sort> ReExpr<R> mkFullRe(R s)
{
return (ReExpr<R>) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
return (ReExpr<R>) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
}

/**
Expand All @@ -2272,6 +2272,50 @@ public <R extends Sort> ReExpr<R> mkRange(Expr<SeqSort<CharSort>> lo, Expr<SeqSo
return (ReExpr<R>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
}

/**
* Create less than or equal to between two characters.
*/
public BoolExpr mkCharLe(Expr<CharSort> ch1, Expr<CharSort> 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<CharSort> 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<CharSort> ch)
{
checkContextMatch(ch);
return (BitVecExpr) Expr.create(this, Native.mkCharToBv(nCtx(), ch.getNativeObject()));
}

/**
* Create a character from a bit-vector (code point).
*/
public Expr<CharSort> charFromBv(BitVecExpr bv)
{
checkContextMatch(bv);
return (Expr<CharSort>) Expr.create(this, Native.mkCharFromBv(nCtx(), bv.getNativeObject()));
}

/**
* Create a check if the character is a digit.
*/
public BoolExpr mkIsDigit(Expr<CharSort> ch)
{
checkContextMatch(ch);
return (BoolExpr) Expr.create(this, Native.mkCharIsDigit(nCtx(), ch.getNativeObject()));
}

/**
* Create an at-most-k constraint.
Expand Down
Loading