英文:
Invoking no-arg constructors of custom data types with type parameters in CVC4
问题
以下是您提供的内容的翻译:
public class Cvc4Test3 {
public static void main(String... args) {
Cvc4Solver.loadLibrary();
ExprManager em = new ExprManager();
SmtEngine smt = new SmtEngine(em);
DatatypeType dt = createOptionDatatype(em);
// 实例化为整数
DatatypeType dtInt = dt.instantiate(vector(em.integerType()));
// x 是一个整数变量
Expr x = em.mkVar("x", em.integerType());
// 创建方程式: None::option[INT] = Some(x)
Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("None"));
Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(dtInt)), l);
Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
Expr eq = em.mkExpr(Kind.EQUAL, la, r);
// 尝试解决方程式:
smt.setOption("produce-models", new SExpr(true));
smt.assertFormula(eq);
Result res = smt.checkSat();
System.out.println("res = " + res);
}
/**
* DATATYPE option[T] =
* None
* | Some(elem: T)
* END;
*/
private static DatatypeType createOptionDatatype(ExprManager em) {
Type t = em.mkSort("T");
vectorType types = vector(t);
Datatype dt = new Datatype("option", types);
DatatypeConstructor cNone = new DatatypeConstructor("None");
dt.addConstructor(cNone);
DatatypeConstructor cSome = new DatatypeConstructor("Some");
cSome.addArg("elem", t);
dt.addConstructor(cSome);
return em.mkDatatypeType(dt);
}
private static vectorType vector(Type... types) {
vectorType res = new vectorType();
for (Type t : types) {
res.add(t);
}
return res;
}
}
这段代码尝试使用 Java API 定义一个带参数的数据类型 option
在 CVC4 中。在代码中,您创建了一个名为 Cvc4Test3
的类,其中包含主要方法 main
和一些辅助方法,用于创建数据类型和方程式,并尝试解决方程式。
英文:
I am trying to define a parameterized datatype option
in CVC4 using the Java API.
DATATYPE option[T] =
None
| Some(elem: T)
END;
My problem is that I don't know how to invoke the None
constructor.
I tried the following code:
class Cvc4Test3 {
public static void main(String... args) {
Cvc4Solver.loadLibrary();
ExprManager em = new ExprManager();
SmtEngine smt = new SmtEngine(em);
DatatypeType dt = createOptionDatatype(em);
// instantiate to int
DatatypeType dtInt = dt.instantiate(vector(em.integerType()));
// x is an integer variable
Expr x = em.mkVar("x", em.integerType());
// create equation: None::option[INT] = Some(x)
Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("None"));
Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(dtInt)), l);
Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
Expr eq = em.mkExpr(Kind.EQUAL, la, r);
// Try to solve equation:
smt.setOption("produce-models", new SExpr(true));
smt.assertFormula(eq);
Result res = smt.checkSat();
System.out.println("res = " + res);
}
/**
* DATATYPE option[T] =
* None
* | Some(elem: T)
* END;
*/
private static DatatypeType createOptionDatatype(ExprManager em) {
Type t = em.mkSort("T");
vectorType types = vector(t);
Datatype dt = new Datatype("option", types);
DatatypeConstructor cNone = new DatatypeConstructor("None");
dt.addConstructor(cNone);
DatatypeConstructor cSome = new DatatypeConstructor("Some");
cSome.addArg("elem", t);
dt.addConstructor(cSome);
return em.mkDatatypeType(dt);
}
private static vectorType vector(Type... types) {
vectorType res = new vectorType();
for (Type t : types) {
res.add(t);
}
return res;
}
}
This results in the following error:
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
at edu.nyu.acsys.CVC4.CVC4JNI.SmtEngine_assertFormula__SWIG_1(Native Method)
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:
Exception in thread "main" java.lang.RuntimeException: Subexpressions must have a common base type:
Equation: None = Some(x)
Type 1: option[T]
Type 2: option[INT]
: Subexpressions must have a common base type:
Equation: None = Some(x)
Type 1: option[T]
Type 2: option[INT]
at edu.nyu.acsys.CVC4.CVC4JNI.SmtEngine_assertFormula__SWIG_1(Native Method)
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]的构造函数的类型",或者我们所称的"构造函数类型"。
以下是创建表达式的更正代码:
// 创建方程式:None::option[INT] = Some(x)
Type noneInt = dtInt.getDatatype().get("None").getSpecializedConstructorType(dtInt);
Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(noneInt)), dtInt.getConstructor("None"));
Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, la);
Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
Expr eq = em.mkExpr(Kind.EQUAL, l, r);
- "option[INT]"类型和"option[INT]"构造函数类型之间存在差异。类型注释需要使用构造函数类型。
- 注释必须放在构造函数上,而不是应用的构造函数上。
英文:
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:
// create equation: None::option[INT] = Some(x)
Type noneInt = dtInt.getDatatype().get("None").getSpecializedConstructorType(dtInt);
Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(noneInt)), dtInt.getConstructor("None"));
Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, la);
Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
Expr eq = em.mkExpr(Kind.EQUAL, l, r);
- There is a difference between the type option[INT] and the constructor type option[INT]. The type ascription needs to use the constructor type.
- The ascription must go on the constructor and not on the applied constructor.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库,让每个人都能够通过互相帮助和分享经验来进步。
评论