调用CVC4中带有类型参数的自定义数据类型的无参数构造函数

huangapple
go评论101阅读模式
英文:

Invoking no-arg constructors of custom data types with type parameters in CVC4

问题

以下是您提供的内容的翻译：

  1. public class Cvc4Test3 {
  3.     public static void main(String... args) {
  4.         Cvc4Solver.loadLibrary();
  5.         ExprManager em = new ExprManager();
  6.         SmtEngine smt = new SmtEngine(em);
  8.         DatatypeType dt = createOptionDatatype(em);
  9.         // 实例化为整数
  10.         DatatypeType dtInt = dt.instantiate(vector(em.integerType()));
  12.         // x 是一个整数变量
  13.         Expr x = em.mkVar("x", em.integerType());
  15.         // 创建方程式: None::option[INT] = Some(x)
  16.         Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("None"));
  17.         Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(dtInt)), l);
  18.         Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
  19.         Expr eq = em.mkExpr(Kind.EQUAL, la, r);
  21.         // 尝试解决方程式:
  22.         smt.setOption("produce-models", new SExpr(true));
  23.         smt.assertFormula(eq);
  24.         Result res = smt.checkSat();
  25.         System.out.println("res = " + res);
  26.     }
  28.     /**
  29.      * DATATYPE option[T] =
  30.      * None
  31.      * | Some(elem: T)
  32.      * END;
  33.      */
  34.     private static DatatypeType createOptionDatatype(ExprManager em) {
  35.         Type t = em.mkSort("T");
  36.         vectorType types = vector(t);
  37.         Datatype dt = new Datatype("option", types);
  38.         DatatypeConstructor cNone = new DatatypeConstructor("None");
  39.         dt.addConstructor(cNone);
  40.         DatatypeConstructor cSome = new DatatypeConstructor("Some");
  41.         cSome.addArg("elem", t);
  42.         dt.addConstructor(cSome);
  43.         return em.mkDatatypeType(dt);
  44.     }
  46.     private static vectorType vector(Type... types) {
  47.         vectorType res = new vectorType();
  48.         for (Type t : types) {
  49.             res.add(t);
  50.         }
  51.         return res;
  52.     }
  53. }

这段代码尝试使用 Java API 定义一个带参数的数据类型 option 在 CVC4 中。在代码中，您创建了一个名为 Cvc4Test3 的类，其中包含主要方法 main 和一些辅助方法，用于创建数据类型和方程式，并尝试解决方程式。

英文:

I am trying to define a parameterized datatype option in CVC4 using the Java API.

  1.  DATATYPE option[T] =
  2. None
  3. | Some(elem: T)
  4. END;

My problem is that I don't know how to invoke the None constructor.
I tried the following code:

  1. class Cvc4Test3 {
  2. public static void main(String... args) {
  3. Cvc4Solver.loadLibrary();
  4. ExprManager em = new ExprManager();
  5. SmtEngine smt = new SmtEngine(em);
  6. DatatypeType dt = createOptionDatatype(em);
  7. // instantiate to int
  8. DatatypeType dtInt = dt.instantiate(vector(em.integerType()));
  9. // x is an integer variable
  10. Expr x = em.mkVar("x", em.integerType());
  11. // create equation: None::option[INT] = Some(x)
  12. Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("None"));
  13. Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(dtInt)), l);
  14. Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
  15. Expr eq = em.mkExpr(Kind.EQUAL, la, r);
  16. // Try to solve equation:
  17. smt.setOption("produce-models", new SExpr(true));
  18. smt.assertFormula(eq);
  19. Result res = smt.checkSat();
  20. System.out.println("res = " + res);
  21. }
  22. /**
  23. * DATATYPE option[T] =
  24. * None
  25. * | Some(elem: T)
  26. * END;
  27. */
  28. private static DatatypeType createOptionDatatype(ExprManager em) {
  29. Type t = em.mkSort("T");
  30. vectorType types = vector(t);
  31. Datatype dt = new Datatype("option", types);
  32. DatatypeConstructor cNone = new DatatypeConstructor("None");
  33. dt.addConstructor(cNone);
  34. DatatypeConstructor cSome = new DatatypeConstructor("Some");
  35. cSome.addArg("elem", t);
  36. dt.addConstructor(cSome);
  37. return em.mkDatatypeType(dt);
  38. }
  39. private static vectorType vector(Type... types) {
  40. vectorType res = new vectorType();
  41. for (Type t : types) {
  42. res.add(t);
  43. }
  44. return res;
  45. }
  46. }

This results in the following error:

  1. Exception in thread "main" java.lang.RuntimeException: matching failed for type ascription argument of parameterized datatype: matching failed for type ascription argument of parameterized datatype
  2. at edu.nyu.acsys.CVC4.CVC4JNI.SmtEngine_assertFormula__SWIG_1(Native Method)
  3. at edu.nyu.acsys.CVC4.SmtEngine.assertFormula(SmtEngine.java:149)

When I remove the type ascription line, it does not infer the correct type, so I assume the type ascription is necessary. Here i the error I get without the type ascription:

  1. Exception in thread "main" java.lang.RuntimeException: Subexpressions must have a common base type:
  2. Equation: None = Some(x)
  3. Type 1: option[T]
  4. Type 2: option[INT]
  5. : Subexpressions must have a common base type:
  6. Equation: None = Some(x)
  7. Type 1: option[T]
  8. Type 2: option[INT]
  9. at edu.nyu.acsys.CVC4.CVC4JNI.SmtEngine_assertFormula__SWIG_1(Native Method)
  10. at edu.nyu.acsys.CVC4.SmtEngine.assertFormula(SmtEngine.java:149)

How do I create this datatype and formula correctly using the Java API?

答案1

得分: 0

收到了来自CVC4邮件列表的Andrew Reynolds的回复：

首先，请注意我们已经更新到了新的API（https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.h）。
巧合的是，我刚刚提交了一个PR，向新的API中添加了获取所需构造函数接口的功能，您可以在这个PR中找到：https://github.com/CVC4/CVC4/pull/4817

如果您对旧的API感兴趣，您的代码几乎是正确的，但是在我们期望的转换方式上有一个细微的差异。

特别地，在SMT-LIB中，转换是应用于构造函数操作符，而不是项（您可能对这个讨论感兴趣：https://github.com/Z3Prover/z3/issues/2135）。这意味着在CVC4中，转换为nil的项的AST是：（APPLY_CONSTRUCTOR（APPLY_TYPE_ASCRIPTION None T）），而不是（APPLY_TYPE_ASCRIPTION（APPLY_CONSTRUCTOR None）option[Int]）。不幸的是，旧的API中关于T的内容有点复杂。它不是"option[Int]"，而是"类型为option[Int]的构造函数的类型"，或者我们所称的"构造函数类型"。

以下是创建表达式的更正代码：

  1. // 创建方程式：None::option[INT] = Some(x)
  2. Type noneInt = dtInt.getDatatype().get("None").getSpecializedConstructorType(dtInt);
  3. Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(noneInt)), dtInt.getConstructor("None"));
  4. Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, la);
  5. Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
  6. Expr eq = em.mkExpr(Kind.EQUAL, l, r);
  1. "option[INT]"类型和"option[INT]"构造函数类型之间存在差异。类型注释需要使用构造函数类型。
  2. 注释必须放在构造函数上，而不是应用的构造函数上。
英文:

Got an answer from Andrew Reynolds on the CVC4 mailing list:

> First, notice that we have updated to a new API
> (https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.h).
> Coincidentally, I just submitted a PR that adds the interface for
> getting the required constructor you are looking for, in the new API:
> https://github.com/CVC4/CVC4/pull/4817
>
> If you are interested in the old API, your code is almost correct,
> however, there is a subtle difference in what we expect to be cast.
>
> In particular, in SMT-LIB casts are applied to constructor operators,
> not terms (you may be interested in this discussion
> https://github.com/Z3Prover/z3/issues/2135). This means that the AST
> of a casted nil term in CVC4 is: (APPLY_CONSTRUCTOR
> (APPLY_TYPE_ASCRIPTION None T)) not (APPLY_TYPE_ASCRIPTION
> (APPLY_CONSTRUCTOR None) option[Int]) Unfortunately, there is a
> complication in the old API about what T is. It is not "option[Int]",
> instead it is "the type of constructors of type option[Int]", or what
> we call a "constructor type".

Here is the corrected code for creating the expression:

  1.     // create equation: None::option[INT] = Some(x)
  2. Type noneInt = dtInt.getDatatype().get("None").getSpecializedConstructorType(dtInt);
  3. Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(noneInt)), dtInt.getConstructor("None"));
  4. Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, la);
  5. Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
  6. Expr eq = em.mkExpr(Kind.EQUAL, l, r);
  1. There is a difference between the type option[INT] and the constructor type option[INT]. The type ascription needs to use the constructor type.
  2. The ascription must go on the constructor and not on the applied constructor.

huangapple
  • 本文由 发表于 2020年7月27日 08:09:05
  • 转载请务必保留本文链接：https://go.coder-hub.com/63107078.html
  • cvc4
  • java
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定