From e3f32ca3a8820e4f26615fe366ffc1b96aca9f2a Mon Sep 17 00:00:00 2001
From: "KangJing Huang (Chaserhkj)" <huangkangjing@gmail.com>
Date: Wed, 14 Jun 2017 02:18:21 -0400
Subject: [PATCH 1/2] Fix Z3_PRINT_SMTLIB_FULL not working as expected
---
src/api/api_ast.cpp | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 3cec4ec02..7342b3c49 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -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;
From d8a02bc0400e08786132779d1c81607cbc2109bb Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 14 Jun 2017 13:24:54 +0100
Subject: [PATCH 2/2] Fixed AST translation functions in .NET and Java APIs.
Fixes #1073.
---
examples/dotnet/Program.cs | 27 +++++++++++++++++++++++++++
examples/java/JavaExample.java | 33 +++++++++++++++++++++++++++++----
src/api/dotnet/AST.cs | 16 ++++++++--------
src/api/dotnet/Expr.cs | 24 +++++++++---------------
src/api/dotnet/FuncDecl.cs | 16 +++++-----------
src/api/dotnet/Quantifier.cs | 12 +++++++++++-
src/api/dotnet/Sort.cs | 20 +++++++++++++++-----
src/api/java/AST.java | 4 +---
src/api/java/Expr.java | 9 +--------
src/api/java/FuncDecl.java | 8 +-------
src/api/java/Quantifier.java | 13 +++++++++++++
src/api/java/Sort.java | 13 +++++++++++++
12 files changed, 133 insertions(+), 62 deletions(-)
diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index 20bb012b1..64149a553 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -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!");
diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index 5810dab37..25076e27c 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -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())
diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs
index 2ffaaa661..c7ca1851e 100644
--- a/src/api/dotnet/AST.cs
+++ b/src/api/dotnet/AST.cs
@@ -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;
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 5e0abcb74..6c52b83c8 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -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
diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs
index 345019892..0587a2276 100644
--- a/src/api/dotnet/FuncDecl.cs
+++ b/src/api/dotnet/FuncDecl.cs
@@ -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);
}
diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs
index eb21ed2b9..eca4e3c7e 100644
--- a/src/api/dotnet/Quantifier.cs
+++ b/src/api/dotnet/Quantifier.cs
@@ -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)
diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs
index e1b8ca1b7..e6f195434 100644
--- a/src/api/dotnet/Sort.cs
+++ b/src/api/dotnet/Sort.cs
@@ -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
- }
+ }
}
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index e1cde837f..350830443 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -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()));
}
}
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 707f3300d..6cabbb1b8 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -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);
}
/**
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index 8b1ad4b44..255bc2c4a 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -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);
}
/**
diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java
index bc2537107..ce2adce21 100644
--- a/src/api/java/Quantifier.java
+++ b/src/api/java/Quantifier.java
@@ -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.
*
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index 0763a69a3..e7a186ad2 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -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
**/