java - 在 CVC4 中使用类型参数调用自定义数据类型的无参数构造函数
问题描述
我正在尝试option
使用 Java API 在 CVC4 中定义参数化数据类型。
DATATYPE option[T] =
None
| Some(elem: T)
END;
我的问题是我不知道如何调用None
构造函数。我尝试了以下代码:
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;
}
}
这会导致以下错误:
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)
当我删除类型归属行时,它不会推断出正确的类型,所以我认为类型归属是必要的。这是我在没有类型说明的情况下得到的错误:
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)
如何使用 Java API 正确创建此数据类型和公式?
解决方案
在 CVC4 邮件列表上得到了 Andrew Reynolds 的答复:
首先,请注意我们已经更新到一个新的 API ( https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.h )。
巧合的是,我刚刚提交了一个 PR,在新 API 中添加了获取所需构造函数的接口: 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)) not (APPLY_TYPE_ASCRIPTION (APPLY_CONSTRUCTOR None) option[Int]) 不幸的是,旧 API 中关于 T 是什么的复杂性。它不是“option[Int]”,而是“option[Int] 类型的构造函数的类型”,或者我们所说的“构造函数类型”。
这是创建表达式的更正代码:
// 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);
- 类型选项 [INT] 和构造函数类型选项 [INT] 之间存在差异。类型归属需要使用构造函数类型。
- 归属必须在构造函数上而不是在应用的构造函数上。
推荐阅读
- postgresql - 无法连接到远程 Postgres docker 容器
- android - notifyDataSetChanged 后如何避免闪烁效果
- google-app-maker - 如何在 Google 应用程序制造商中调用存储过程
- java - 正则表达式从字符串中删除非数字和非小数点
- python - 在 MacOS 上使用 pySerial 读取 RS-232 中的“\xa0”和“\xb”字符
- swift - Swift Vapor - 'Cannot invoke 'add' with a argument list of type ...' configure.swift 中的错误
- tensorflow - 如何在 TensorFlow 2.0 中初始化 LSTM 模型的变量?
- azure - 如何将数组输出分配给逻辑应用变量?
- android - 如何使用 aws ec2 作为 android 应用程序的后端
- swift - RealityKit - 拖动对象切换平面