smt — Как определить предикаты, используя C ++ API для CVC4
Это пример на родном языке CVC:
isblue: STRING -> BOOLEAN;
ASSERT isblue("sky");
ASSERT isblue("water");
QUERY isblue("sky"); //valid
QUERY isblue("pig"); //invalid
Как бы я написал это, используя C ++ API для CVC4? Не удалось найти документацию о том, как это сделать.
Решение
В исходном выпуске есть несколько примеров API, которые могут вам помочь. В частности, examples / api / compatibility.cpp создает некоторые функции и предикаты и делает некоторые утверждения:
https://github.com/CVC4/CVC4/blob/master/examples/api/combination.cpp
В вашем случае вы создадите тип предиката с помощью ExprManager :: mkFunctionType (), а затем создадите предикат «isblue» с помощью ExprManager :: mkVar (), присвоив ему этот тип. Это будет выглядеть примерно так (при условии, что вы сделали «использование пространства имен 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"))));
Другие решения