пользовательский ввод — CVC4: использование квантификаторов в интерфейсе C ++

Я пытаюсь понять, как кодировать квантификаторы в CVC4, используя интерфейс C ++. Вот пример, который я пытаюсь запустить, но не могу.

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;
}