Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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;
- }
- Quantifier not defined.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement