如何使用 C++ API for CVC4 定义谓词答案

【问题标题】：How to define predicates using C++ API for CVC4如何使用 C++ API for CVC4 定义谓词
【发布时间】：2014-11-29 17:28:36
【问题描述】：

这是一个原生 CVC 语言的示例：

isblue: STRING -> BOOLEAN;
ASSERT isblue("sky");
ASSERT isblue("water");
QUERY isblue("sky"); //valid
QUERY isblue("pig"); //invalid

如何使用 CVC4 的 C++ API 编写它？找不到有关如何执行此操作的任何文档。

【问题讨论】：

我猜你必须编写自己的定理证明器或使用 C++ 提供的现有证明器。 C++ 不是一阶逻辑语言。
对不起，应该说清楚：如何使用 CVC4 的 C++ API 编写它？

标签： c++ smt cvc4

【解决方案1】：

源代码分发中有一些 API 示例可能会对您有所帮助。特别是，examples/api/combination.cpp 创建了一些函数和谓词并进行了一些断言：

https://github.com/CVC4/CVC4/blob/master/examples/api/combination.cpp

在您的情况下，您将使用 ExprManager::mkFunctionType() 创建一个谓词类型，然后使用 ExprManager::mkVar() 构造一个“isblue”谓词给它该类型。它看起来像这样（假设你已经完成了“使用命名空间 CVC4”和#included ）：

  ExprManager em;
  SmtEngine smt(&em);

  Type predType = em.mkFunctionType(em.stringType(), em.booleanType());
  Expr isblue = em.mkVar(predType);

然后你可以断言和查询你的谓词的应用：

  smt.assertFormula(em.mkExpr(kind::APPLY_UF, isblue, em.mkConst(String("sky"))));
  smt.assertFormula(em.mkExpr(kind::APPLY_UF, isblue, em.mkConst(String("water"))));
  smt.query(em.mkExpr(kind::APPLY_UF, isblue, em.mkConst(String("sky"))));
  smt.query(em.mkExpr(kind::APPLY_UF, isblue, em.mkConst(String("pig"))));

【讨论】：