mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
seq, API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c1ebf6b4fc
commit
d7dcd022b9
|
@ -103,6 +103,7 @@ public class Context extends IDisposable
|
|||
private BoolSort m_boolSort = null;
|
||||
private IntSort m_intSort = null;
|
||||
private RealSort m_realSort = null;
|
||||
private SeqSort m_stringSort = null;
|
||||
|
||||
/**
|
||||
* Retrieves the Boolean sort of the context.
|
||||
|
@ -142,6 +143,16 @@ public class Context extends IDisposable
|
|||
return new BoolSort(this);
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieves the Integer sort of the context.
|
||||
**/
|
||||
public SeqSort getStringSort()
|
||||
{
|
||||
if (m_stringSort == null)
|
||||
m_stringSort = mkStringSort();
|
||||
return m_stringSort;
|
||||
}
|
||||
|
||||
/**
|
||||
* Create a new uninterpreted sort.
|
||||
**/
|
||||
|
@ -193,6 +204,31 @@ public class Context extends IDisposable
|
|||
return new ArraySort(this, domain, range);
|
||||
}
|
||||
|
||||
/**
|
||||
* Create a new string sort
|
||||
**/
|
||||
public SeqSort mkStringSort()
|
||||
{
|
||||
return new SeqSort(this, Native.mkStringSort(nCtx()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Create a new sequence sort
|
||||
**/
|
||||
public SeqSort mkSeqSort(Sort s)
|
||||
{
|
||||
return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Create a new regular expression sort
|
||||
**/
|
||||
public ReSort mkReSort(Sort s)
|
||||
{
|
||||
return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Create a new tuple sort.
|
||||
**/
|
||||
|
@ -1860,7 +1896,7 @@ public class Context extends IDisposable
|
|||
public SeqExpr MkEmptySeq(Sort s)
|
||||
{
|
||||
checkContextMatch(s);
|
||||
return new SeqExpr(this, Native.mkSeqEmpty(nCtx, s.NativeObject));
|
||||
return new SeqExpr(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1869,24 +1905,24 @@ public class Context extends IDisposable
|
|||
public SeqExpr MkUnit(Expr elem)
|
||||
{
|
||||
checkContextMatch(elem);
|
||||
return new SeqExpr(this, Native.mkSeqUnit(nCtx, elem.NativeObject));
|
||||
return new SeqExpr(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Create a string constant.
|
||||
*/
|
||||
public SeqExpr MkString(string s)
|
||||
public SeqExpr MkString(String s)
|
||||
{
|
||||
return new SeqExpr(this, Native.mkString(nCtx, s));
|
||||
return new SeqExpr(this, Native.mkString(nCtx(), s));
|
||||
}
|
||||
|
||||
/**
|
||||
* Concatentate sequences.
|
||||
*/
|
||||
public SeqExpr MkConcat(params SeqExpr[] t)
|
||||
public SeqExpr MkConcat(SeqExpr... t)
|
||||
{
|
||||
checkContextMatch(t);
|
||||
return new SeqExpr(this, Native.mkSeqConcat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
|
||||
return new SeqExpr(this, Native.mkSeqConcat(nCtx(), (int)t.length, AST.arrayToNative(t)));
|
||||
}
|
||||
|
||||
|
||||
|
@ -1896,7 +1932,7 @@ public class Context extends IDisposable
|
|||
public IntExpr MkLength(SeqExpr s)
|
||||
{
|
||||
checkContextMatch(s);
|
||||
return (IntExpr) Expr.Create(this, Native.mkSeqLength(nCtx, s.NativeObject));
|
||||
return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1905,7 +1941,7 @@ public class Context extends IDisposable
|
|||
public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
|
||||
{
|
||||
checkContextMatch(s1, s2);
|
||||
return new BoolExpr(this, Native.mkSeqPrefix(nCtx, s1.NativeObject, s2.NativeObject));
|
||||
return new BoolExpr(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1914,7 +1950,7 @@ public class Context extends IDisposable
|
|||
public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
|
||||
{
|
||||
checkContextMatch(s1, s2);
|
||||
return new BoolExpr(this, Native.mkSeqSuffix(nCtx, s1.NativeObject, s2.NativeObject));
|
||||
return new BoolExpr(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1923,7 +1959,7 @@ public class Context extends IDisposable
|
|||
public BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
|
||||
{
|
||||
checkContextMatch(s1, s2);
|
||||
return new BoolExpr(this, Native.mkSeqContains(nCtx, s1.NativeObject, s2.NativeObject));
|
||||
return new BoolExpr(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1932,7 +1968,7 @@ public class Context extends IDisposable
|
|||
public SeqExpr MkAt(SeqExpr s, IntExpr index)
|
||||
{
|
||||
checkContextMatch(s, index);
|
||||
return new SeqExpr(this, Native.mkSeqAt(nCtx, s.NativeObject, index.NativeObject));
|
||||
return new SeqExpr(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1941,7 +1977,7 @@ public class Context extends IDisposable
|
|||
public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
|
||||
{
|
||||
checkContextMatch(s, offset, length);
|
||||
return new SeqExpr(this, Native.mkSeqExtract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
|
||||
return new SeqExpr(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1950,7 +1986,7 @@ public class Context extends IDisposable
|
|||
public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
|
||||
{
|
||||
checkContextMatch(s, substr, offset);
|
||||
return new IntExpr(this, Native.mkSeqIndex(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
|
||||
return new IntExpr(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1959,7 +1995,7 @@ public class Context extends IDisposable
|
|||
public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
|
||||
{
|
||||
checkContextMatch(s, src, dst);
|
||||
return new SeqExpr(this, Native.mkSeqReplace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
|
||||
return new SeqExpr(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1968,7 +2004,7 @@ public class Context extends IDisposable
|
|||
public ReExpr MkToRe(SeqExpr s)
|
||||
{
|
||||
checkContextMatch(s);
|
||||
return new ReExpr(this, Native.mkSeqToRe(nCtx, s.NativeObject));
|
||||
return new ReExpr(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
|
@ -1978,7 +2014,7 @@ public class Context extends IDisposable
|
|||
public BoolExpr MkInRe(SeqExpr s, ReExpr re)
|
||||
{
|
||||
checkContextMatch(s, re);
|
||||
return new BoolExpr(this, Native.mkSeqInRe(nCtx, s.NativeObject, re.NativeObject));
|
||||
return new BoolExpr(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1987,7 +2023,7 @@ public class Context extends IDisposable
|
|||
public ReExpr MkStar(ReExpr re)
|
||||
{
|
||||
checkContextMatch(re);
|
||||
return new ReExpr(this, Native.mkReStar(nCtx, re.NativeObject));
|
||||
return new ReExpr(this, Native.mkReStar(nCtx(), re.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1996,7 +2032,7 @@ public class Context extends IDisposable
|
|||
public ReExpr MPlus(ReExpr re)
|
||||
{
|
||||
checkContextMatch(re);
|
||||
return new ReExpr(this, Native.mkRePlus(nCtx, re.NativeObject));
|
||||
return new ReExpr(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -2005,25 +2041,25 @@ public class Context extends IDisposable
|
|||
public ReExpr MOption(ReExpr re)
|
||||
{
|
||||
checkContextMatch(re);
|
||||
return new ReExpr(this, Native.mkReOption(nCtx, re.NativeObject));
|
||||
return new ReExpr(this, Native.mkReOption(nCtx(), re.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Create the concatenation of regular languages.
|
||||
*/
|
||||
public ReExpr MkConcat(ReExpr[] t)
|
||||
public ReExpr MkConcat(ReExpr... t)
|
||||
{
|
||||
checkContextMatch(t);
|
||||
return new ReExpr(this, Native.mkReConcat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
|
||||
return new ReExpr(this, Native.mkReConcat(nCtx(), (int)t.length, AST.arrayToNative(t)));
|
||||
}
|
||||
|
||||
/**
|
||||
* Create the union of regular languages.
|
||||
*/
|
||||
public ReExpr MkUnion(ReExpr[] t)
|
||||
public ReExpr MkUnion(ReExpr... t)
|
||||
{
|
||||
checkContextMatch(t);
|
||||
return new ReExpr(this, Native.mkReUnion(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
|
||||
return new ReExpr(this, Native.mkReUnion(nCtx(), (int)t.length, AST.arrayToNative(t)));
|
||||
}
|
||||
|
||||
|
||||
|
@ -4021,6 +4057,7 @@ public class Context extends IDisposable
|
|||
m_boolSort = null;
|
||||
m_intSort = null;
|
||||
m_realSort = null;
|
||||
m_stringSort = null;
|
||||
|
||||
synchronized (creation_lock) {
|
||||
if (m_refCount.get() == 0 && m_ctx != 0) {
|
||||
|
|
|
@ -88,8 +88,6 @@ struct
|
|||
(z3obj_create res) ;
|
||||
res
|
||||
|
||||
let ignore2 a b c = ignore a; ignore b
|
||||
let ignore3 a b c = ignore a; ignore2 b c
|
||||
|
||||
end
|
||||
|
||||
|
@ -837,20 +835,11 @@ end = struct
|
|||
let o = Z3native.mk_app (context_gno ctx) (AST.ptr_of_ast fa) (List.length args) (expr_lton args) in
|
||||
expr_of_ptr ctx o
|
||||
|
||||
let apply_un ctx f t =
|
||||
let r = expr_of_ptr ctx (f (context_gno ctx) (gno t)) in
|
||||
ignore t;
|
||||
r
|
||||
let apply1 ctx f t = expr_of_ptr ctx (f (context_gno ctx) (gno t)) in
|
||||
|
||||
let apply_bin ctx f t1 t2 =
|
||||
let r = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) in
|
||||
ignore2 t1 t2;
|
||||
r
|
||||
let apply2 ctx f t1 t2 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) in
|
||||
|
||||
let apply_ter ctx f t1 t2 t3 =
|
||||
let r = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) in
|
||||
ignore3 t1 t2 t3;
|
||||
r
|
||||
let apply3 ctx f t1 t2 t3 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) in
|
||||
|
||||
|
||||
let simplify ( x : expr ) ( p : Params.params option ) = match p with
|
||||
|
@ -874,17 +863,13 @@ end = struct
|
|||
if ((AST.is_app (ast_of_expr x)) && (List.length args <> (get_num_args x))) then
|
||||
raise (Z3native.Exception "Number of arguments does not match")
|
||||
else
|
||||
let r = expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) in
|
||||
ignore2 x args;
|
||||
r
|
||||
|
||||
expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args))
|
||||
|
||||
let substitute ( x : expr ) from to_ =
|
||||
if (List.length from) <> (List.length to_) then
|
||||
raise (Z3native.Exception "Argument sizes do not match")
|
||||
else
|
||||
let r = expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) in
|
||||
ignore3 from to_ x;
|
||||
r
|
||||
expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_))
|
||||
|
||||
let substitute_one ( x : expr ) from to_ =
|
||||
substitute ( x : expr ) [ from ] [ to_ ]
|
||||
|
@ -896,9 +881,7 @@ end = struct
|
|||
if (Expr.gc x) == to_ctx then
|
||||
x
|
||||
else
|
||||
let r = expr_of_ptr to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx)) in
|
||||
ignore2 x to_ctx;
|
||||
r
|
||||
expr_of_ptr to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx))
|
||||
|
||||
let to_string ( x : expr ) = Z3native.ast_to_string (gnc x) (gno x)
|
||||
|
||||
|
@ -959,39 +942,33 @@ struct
|
|||
let mk_val ( ctx : context ) ( value : bool ) =
|
||||
if value then mk_true ctx else mk_false ctx
|
||||
|
||||
let mk_not ( ctx : context ) ( a : expr ) = apply_un ctx Z3native.mk_not a
|
||||
let mk_not ( ctx : context ) ( a : expr ) = apply1 ctx Z3native.mk_not a
|
||||
|
||||
let mk_ite ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) =
|
||||
apply_ter ctx Z3native.mk_ite t1 t2 t3
|
||||
apply3 ctx Z3native.mk_ite t1 t2 t3
|
||||
|
||||
let mk_iff ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
apply_bin ctx Z3native.mk_iff t1 t2
|
||||
apply2 ctx Z3native.mk_iff t1 t2
|
||||
|
||||
let mk_implies ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
apply_bin ctx Z3native.mk_implies t1 t2
|
||||
apply2 ctx Z3native.mk_implies t1 t2
|
||||
|
||||
let mk_xor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
apply_bin ctx Z3native.mk_xor t1 t2
|
||||
apply2 ctx Z3native.mk_xor t1 t2
|
||||
|
||||
let mk_and ( ctx : context ) ( args : expr list ) =
|
||||
let f x = (Expr.gno (x)) in
|
||||
let r = expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (List.length args) (Array.of_list (List.map f args))) in
|
||||
ignore args;
|
||||
r
|
||||
expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (List.length args) (Array.of_list (List.map f args)))
|
||||
|
||||
let mk_or ( ctx : context ) ( args : expr list ) =
|
||||
let f x = (Expr.gno (x)) in
|
||||
let r = expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (List.length args) (Array.of_list(List.map f args))) in
|
||||
ignore args;
|
||||
r
|
||||
expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (List.length args) (Array.of_list(List.map f args)))
|
||||
|
||||
let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) =
|
||||
apply_bin ctx Z3native.mk_eq x y
|
||||
apply2 ctx Z3native.mk_eq x y
|
||||
|
||||
let mk_distinct ( ctx : context ) ( args : expr list ) =
|
||||
let r = expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args)) in
|
||||
ignore args;
|
||||
r
|
||||
expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args))
|
||||
|
||||
let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value (gnc x) (gno x))
|
||||
|
||||
|
@ -1097,12 +1074,10 @@ struct
|
|||
mk_list f n
|
||||
|
||||
let get_body ( x : quantifier ) =
|
||||
apply_un (gc x) Z3native.get_quantifier_body x
|
||||
apply1 (gc x) Z3native.get_quantifier_body x
|
||||
|
||||
let mk_bound ( ctx : context ) ( index : int ) ( ty : Sort.sort ) =
|
||||
let r = expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty)) in
|
||||
ignore ty;
|
||||
r
|
||||
expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty))
|
||||
|
||||
let mk_pattern ( ctx : context ) ( terms : expr list ) =
|
||||
if (List.length terms) == 0 then
|
||||
|
@ -1227,27 +1202,23 @@ struct
|
|||
mk_const ctx (Symbol.mk_string ctx name) domain range
|
||||
|
||||
let mk_select ( ctx : context ) ( a : expr ) ( i : expr ) =
|
||||
apply_bin ctx Z3native.mk_select a i
|
||||
apply2 ctx Z3native.mk_select a i
|
||||
|
||||
let mk_store ( ctx : context ) ( a : expr ) ( i : expr ) ( v : expr ) =
|
||||
apply_ter ctx Z3native.mk_store a i v
|
||||
apply3 ctx Z3native.mk_store a i v
|
||||
|
||||
let mk_const_array ( ctx : context ) ( domain : Sort.sort ) ( v : expr ) =
|
||||
let r = expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v)) in
|
||||
ignore2 domain v;
|
||||
r
|
||||
expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v))
|
||||
|
||||
let mk_map ( ctx : context ) ( f : func_decl ) ( args : expr list ) =
|
||||
let m x = (Expr.gno x) in
|
||||
let r = expr_of_ptr ctx (Z3native.mk_map (context_gno ctx) (FuncDecl.gno f) (List.length args) (Array.of_list (List.map m args))) in
|
||||
ignore2 f args;
|
||||
r
|
||||
expr_of_ptr ctx (Z3native.mk_map (context_gno ctx) (FuncDecl.gno f) (List.length args) (Array.of_list (List.map m args)))
|
||||
|
||||
let mk_term_array ( ctx : context ) ( arg : expr ) =
|
||||
apply_un ctx Z3native.mk_array_default arg
|
||||
apply1 ctx Z3native.mk_array_default arg
|
||||
|
||||
let mk_array_ext ( ctx : context) ( arg1 : expr ) ( arg2 : expr ) =
|
||||
apply_bin ctx Z3native.mk_array_ext arg1 arg2
|
||||
apply2 ctx Z3native.mk_array_ext arg1 arg2
|
||||
end
|
||||
|
||||
|
||||
|
@ -1270,14 +1241,13 @@ struct
|
|||
expr_of_ptr ctx (Z3native.mk_full_set (context_gno ctx) (Sort.gno domain))
|
||||
|
||||
let mk_set_add ( ctx : context ) ( set : expr ) ( element : expr ) =
|
||||
apply_bin ctx Z3native.mk_set_add set element
|
||||
apply2 ctx Z3native.mk_set_add set element
|
||||
|
||||
let mk_del ( ctx : context ) ( set : expr ) ( element : expr ) =
|
||||
apply_bin Z3native.mk_set_del set element
|
||||
apply2 Z3native.mk_set_del set element
|
||||
|
||||
let mk_union ( ctx : context ) ( args : expr list ) =
|
||||
let r = expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args)) in
|
||||
ignore r;
|
||||
r
|
||||
|
||||
let mk_intersection ( ctx : context ) ( args : expr list ) =
|
||||
|
|
Loading…
Reference in a new issue