c++ - CVC4 の C++ API を使用して述語を定義する方法

Question

これは、ネイティブ CVC 言語の例です。

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

CVC4 の C++ API を使用してどのように記述しますか? これを行う方法に関するドキュメントが見つかりませんでした。

Answer 1

ソース配布物には、役立つ API の例がいくつか含まれています。特に、examples/api/combination.cpp はいくつかの関数と述語を作成し、いくつかのアサーションを作成します。

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

あなたの場合、ExprManager::mkFunctionType() で述語型を作成し、その型を与える ExprManager::mkVar() で「isblue」述語を作成します。これは次のようになります (「名前空間 CVC4 の使用」と #included <cvc4/cvc4.h> を行ったと仮定します):

  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"))));