2

我试图弄清楚如何使用 C++ 接口在 CVC4 中编写量词。这是我试图运行但不能运行的示例。

int main() {
    SmtEngine smt(&em);
    smt.setLogic("AUFLIRA"); // Set the logic

    Expr three = em.mkConst(Rational(3));
    Expr  four = em.mkConst(Rational(4));

    // make the list of bound variables in CVC4
    Expr bound_var = em.mkBoundVar("x_bound",  em.integerType());
    vector<Expr> bound_vars;
    bound_vars.push_back(bound_var);
    Expr bound_var_list = em.mkExpr(kind::BOUND_VAR_LIST, bound_vars);

    Expr declare = em.mkExpr(kind::EQUAL, bound_var, three); //x_bound =3

    Expr check = em.mkExpr(kind::EQUAL, bound_var, four); //x_bound=4

    //forall x_bound, x_bound=3, the constraint I want to declare as true
    Expr expr = em.mkExpr(kind::FORALL, bound_var_list, declare); 

    smt.assertFormula(expr);
    smt.push();

    // expect to be INVALID
    // I want to check that given forall x_bound, x_bound = 3
    // then I ask CVC4: is it true that x_bound=4, or is it false?
    std::cout << "Quantifier " << smt.query(check) << std::endl;

    return 0;
}

相反，我只是收到一条错误消息：

Bound variables test
Quantifier unknown (INCOMPLETE)

但我将量词定义为forall. 我做错了什么？

编辑（问https://www.andrew.cmu.edu/user/liminjia/）：

语法错误。我们想知道是否

(forall x, x=3) IMPLIES (forall x, x=4)

是真是假。但如果上述公式有效与否，CVC4 则不会，因为 SMT 求解器不是成熟的一阶逻辑定理证明器。

如果您想尝试一些可行的方法，请尝试使用 CVC4 语言：

QUERY (FORALL (x:INT): x =4);

在 C++ 中，我们有

// check that forall x, x=3 is INVALID
void cvc4BoundVar() {
    std::cout << "Bound variables test" << std::endl;
    SmtEngine smt(&em);
    smt.setLogic("AUFLIRA"); // Set the logic

    Expr three = em.mkConst(Rational(3));

    Expr v_expr = em.mkBoundVar("x_bound",  em.integerType());
    vector<Expr> bound_vars;
    bound_vars.push_back(v_expr);
    Expr bound_var_list = em.mkExpr(kind::BOUND_VAR_LIST, bound_vars);

    Expr declare = em.mkExpr(kind::EQUAL, v_expr, three); //x=3

    Expr check = em.mkExpr(kind::EQUAL, v_expr, three);

    Expr expr = em.mkExpr(kind::FORALL, bound_var_list, declare); //forall x, x=3

    std::cout << "Quantifier " << smt.query(expr) << std::endl;
}
4

0 回答 0