mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-06-14 21:41:31 -07:00
parent 8ac43c981a d8a02bc040
commit f4214e1c71
13 changed files with 140 additions and 65 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
examples/dotnet/Program.cs
View file

@ -2152,6 +2152,31 @@ namespace test_mapi
Console.WriteLine("OK, model: {0}", s.Model.ToString());
}
public static void TranslationExample()
{
Context ctx1 = new Context();
Context ctx2 = new Context();
Sort s1 = ctx1.IntSort;
Sort s2 = ctx2.IntSort;
Sort s3 = s1.Translate(ctx2);
Console.WriteLine(s1 == s2);
Console.WriteLine(s1.Equals(s2));
Console.WriteLine(s2.Equals(s3));
Console.WriteLine(s1.Equals(s3));
Expr e1 = ctx1.MkIntConst("e1");
Expr e2 = ctx2.MkIntConst("e1");
Expr e3 = e1.Translate(ctx2);
Console.WriteLine(e1 == e2);
Console.WriteLine(e1.Equals(e2));
Console.WriteLine(e2.Equals(e3));
Console.WriteLine(e1.Equals(e3));
}
static void Main(string[] args)
{
try
@ -2225,6 +2250,8 @@ namespace test_mapi
QuantifierExample4(ctx);
}
TranslationExample();
Log.Close();
if (Log.isOpen())
Console.WriteLine("Log is still open!");

33
examples/java/JavaExample.java
View file

@ -281,7 +281,7 @@ class JavaExample
}
void disprove(Context ctx, BoolExpr f, boolean useMBQI)
throws TestFailedException
throws TestFailedException
{
BoolExpr[] a = {};
disprove(ctx, f, useMBQI, a);
@ -2279,6 +2279,29 @@ class JavaExample
System.out.println(my);
}
public void translationExample() {
Context ctx1 = new Context();
Context ctx2 = new Context();
Sort s1 = ctx1.getIntSort();
Sort s2 = ctx2.getIntSort();
Sort s3 = s1.translate(ctx2);
System.out.println(s1 == s2);
System.out.println(s1.equals(s2));
System.out.println(s2.equals(s3));
System.out.println(s1.equals(s3));
Expr e1 = ctx1.mkIntConst("e1");
Expr e2 = ctx2.mkIntConst("e1");
Expr e3 = e1.translate(ctx2);
System.out.println(e1 == e2);
System.out.println(e1.equals(e2));
System.out.println(e2.equals(e3));
System.out.println(e1.equals(e3));
}
public static void main(String[] args)
{
JavaExample p = new JavaExample();
@ -2300,8 +2323,8 @@ class JavaExample
HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
Context ctx = new Context(cfg);
p.optimizeExample(ctx);
p.optimizeExample(ctx);
p.basicTests(ctx);
p.castingTest(ctx);
p.sudokuExample(ctx);
@ -2355,7 +2378,9 @@ class JavaExample
Context ctx = new Context(cfg);
p.quantifierExample3(ctx);
p.quantifierExample4(ctx);
}
}
p.translationExample();
Log.close();
if (Log.isOpen())

10
src/api/api_ast.cpp
View file

@ -821,9 +821,13 @@ extern "C" {
RESET_ERROR_CODE();
std::ostringstream buffer;
switch (mk_c(c)->get_print_mode()) {
case Z3_PRINT_SMTLIB_FULL:
buffer << mk_pp(to_ast(a), mk_c(c)->m());
case Z3_PRINT_SMTLIB_FULL: {
params_ref p;
p.set_uint("max_depth", 4294967295u);
p.set_uint("min_alias_size", 4294967295u);
buffer << mk_pp(to_ast(a), mk_c(c)->m(), p);
break;
}
case Z3_PRINT_LOW_LEVEL:
buffer << mk_ll_pp(to_ast(a), mk_c(c)->m());
break;
@ -1066,7 +1070,7 @@ extern "C" {
case OP_BIT2BOOL: return Z3_OP_BIT2BOOL;
case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSDIV_I: return Z3_OP_BSDIV_I;
case OP_BUDIV_I: return Z3_OP_BUDIV_I;
case OP_BSREM_I: return Z3_OP_BSREM_I;

16
src/api/dotnet/AST.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-16
Notes:
--*/
using System;
@ -25,7 +25,7 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// The abstract syntax tree (AST) class.
/// The abstract syntax tree (AST) class.
/// </summary>
[ContractVerification(true)]
public class AST : Z3Object, IComparable
@ -35,7 +35,7 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="a">An AST</param>
/// <param name="b">An AST</param>
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context
/// and represent the same sort; false otherwise.</returns>
public static bool operator ==(AST a, AST b)
{
@ -51,7 +51,7 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="a">An AST</param>
/// <param name="b">An AST</param>
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
/// or represent different sorts; false otherwise.</returns>
public static bool operator !=(AST a, AST b)
{
@ -120,12 +120,12 @@ namespace Microsoft.Z3
if (ReferenceEquals(Context, ctx))
return this;
else
return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
return Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
}
/// <summary>
/// The kind of the AST.
/// </summary>
/// </summary>
public Z3_ast_kind ASTKind
{
get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); }
@ -224,10 +224,10 @@ namespace Microsoft.Z3
{
Native.Z3_dec_ref(ctx.nCtx, obj);
}
};
};
internal override void IncRef(IntPtr o)
{
{
// Console.WriteLine("AST IncRef()");
if (Context == null || o == IntPtr.Zero)
return;

24
src/api/dotnet/Expr.cs
View file

@ -163,13 +163,7 @@ namespace Microsoft.Z3
/// <returns>A copy of the term which is associated with <paramref name="ctx"/></returns>
new public Expr Translate(Context ctx)
{
Contract.Requires(ctx != null);
Contract.Ensures(Contract.Result<Expr>() != null);
if (ReferenceEquals(Context, ctx))
return this;
else
return Expr.Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
return (Expr)base.Translate(ctx);
}
/// <summary>
@ -809,7 +803,7 @@ namespace Microsoft.Z3
/// Retrieve string corresponding to string constant.
/// </summary>
/// <remarks>the expression should be a string constant, (IsString should be true).</remarks>
public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }
public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }
/// <summary>
/// Check whether expression is a concatentation.
@ -828,43 +822,43 @@ namespace Microsoft.Z3
/// </summary>
/// <returns>a Boolean</returns>
public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } }
/// <summary>
/// Check whether expression is a contains.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } }
/// <summary>
/// Check whether expression is an extract.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } }
/// <summary>
/// Check whether expression is a replace.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } }
/// <summary>
/// Check whether expression is an at.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } }
public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } }
/// <summary>
/// Check whether expression is a sequence length.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } }
/// <summary>
/// Check whether expression is a sequence index.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } }
#endregion

16
src/api/dotnet/FuncDecl.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-16
Notes:
--*/
using System;
@ -23,7 +23,7 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Function declarations.
/// Function declarations.
/// </summary>
[ContractVerification(true)]
public class FuncDecl : AST
@ -62,7 +62,7 @@ namespace Microsoft.Z3
/// <summary>
/// A hash code.
/// </summary>
/// </summary>
public override int GetHashCode()
{
return base.GetHashCode();
@ -205,7 +205,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Function declarations can have Parameters associated with them.
/// Function declarations can have Parameters associated with them.
/// </summary>
public class Parameter
{
@ -322,13 +322,7 @@ namespace Microsoft.Z3
/// <returns>A copy of the function declaration which is associated with <paramref name="ctx"/></returns>
new public FuncDecl Translate(Context ctx)
{
Contract.Requires(ctx != null);
Contract.Ensures(Contract.Result<FuncDecl>() != null);
if (ReferenceEquals(Context, ctx))
return this;
else
return new FuncDecl(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
return (FuncDecl) base.Translate(ctx);
}

12
src/api/dotnet/Quantifier.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-19
Notes:
--*/
using System;
@ -157,6 +157,16 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Translates (copies) the quantifier to the Context <paramref name="ctx"/>.
/// </summary>
/// <param name="ctx">A context</param>
/// <returns>A copy of the quantifier which is associated with <paramref name="ctx"/></returns>
new public Quantifier Translate(Context ctx)
{
return (Quantifier)base.Translate(ctx);
}
#region Internal
[ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)

20
src/api/dotnet/Sort.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
--*/
using System;
@ -33,7 +33,7 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="a">A Sort</param>
/// <param name="b">A Sort</param>
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context
/// and represent the same sort; false otherwise.</returns>
public static bool operator ==(Sort a, Sort b)
{
@ -49,7 +49,7 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="a">A Sort</param>
/// <param name="b">A Sort</param>
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
/// or represent different sorts; false otherwise.</returns>
public static bool operator !=(Sort a, Sort b)
{
@ -113,10 +113,20 @@ namespace Microsoft.Z3
return Native.Z3_sort_to_string(Context.nCtx, NativeObject);
}
/// <summary>
/// Translates (copies) the sort to the Context <paramref name="ctx"/>.
/// </summary>
/// <param name="ctx">A context</param>
/// <returns>A copy of the sort which is associated with <paramref name="ctx"/></returns>
new public Sort Translate(Context ctx)
{
return (Sort)base.Translate(ctx);
}
#region Internal
/// <summary>
/// Sort constructor
/// </summary>
/// </summary>
internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#if DEBUG
@ -154,5 +164,5 @@ namespace Microsoft.Z3
}
}
#endregion
}
}
}

4
src/api/java/AST.java
View file

@ -87,12 +87,10 @@ public class AST extends Z3Object implements Comparable<AST>
**/
public AST translate(Context ctx)
{
if (getContext() == ctx) {
return this;
} else {
return new AST(ctx, Native.translate(getContext().nCtx(),
getNativeObject(), ctx.nCtx()));
return create(ctx, Native.translate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
}
}

9
src/api/java/Expr.java
View file

@ -194,14 +194,7 @@ public class Expr extends AST
**/
public Expr translate(Context ctx)
{
if (getContext() == ctx) {
return this;
} else {
return Expr.create(
ctx,
Native.translate(getContext().nCtx(), getNativeObject(),
ctx.nCtx()));
}
return (Expr) super.translate(ctx);
}
/**

8
src/api/java/FuncDecl.java
View file

@ -68,13 +68,7 @@ public class FuncDecl extends AST
**/
public FuncDecl translate(Context ctx)
{
if (getContext() == ctx) {
return this;
} else {
return new FuncDecl(ctx, Native.translate(getContext().nCtx(),
getNativeObject(), ctx.nCtx()));
}
return (FuncDecl) super.translate(ctx);
}
/**

13
src/api/java/Quantifier.java
View file

@ -145,6 +145,19 @@ public class Quantifier extends BoolExpr
.nCtx(), getNativeObject()));
}
/**
* Translates (copies) the quantifier to the Context {@code ctx}.
*
* @param ctx A context
*
* @return A copy of the quantifier which is associated with {@code ctx}
* @throws Z3Exception on error
**/
public Quantifier translate(Context ctx)
{
return (Quantifier) super.translate(ctx);
}
/**
* Create a quantified expression.
*

13
src/api/java/Sort.java
View file

@ -87,6 +87,19 @@ public class Sort extends AST
return Native.sortToString(getContext().nCtx(), getNativeObject());
}
/**
* Translates (copies) the sort to the Context {@code ctx}.
*
* @param ctx A context
*
* @return A copy of the sort which is associated with {@code ctx}
* @throws Z3Exception on error
**/
public Sort translate(Context ctx)
{
return (Sort) super.translate(ctx);
}
/**
* Sort constructor
**/