mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
7a4a17b193
This introduces a general way to use public enums both in the C++ and the (upcoming) C API. For the C++ case, we now use enum classes rather than enums for public enums. This also includes definitions for C API to_string conversions for public enums. C API definitions in cvc5_types.h are only included from the C API, guarded via a macro (thus, for now, not included yet when the header is included).
81 lines
2.2 KiB
C++
81 lines
2.2 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Abdalrhman Mohamed, Mathias Preiner, Mudathir Mohamed
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
|
|
* in the top-level source directory and their institutional affiliations.
|
|
* All rights reserved. See the file COPYING in the top-level source
|
|
* directory for licensing information.
|
|
* ****************************************************************************
|
|
*
|
|
* A simple demonstration of the Sygus API.
|
|
*
|
|
* A simple demonstration of how to use the Sygus API to synthesize a simple
|
|
* invariant.
|
|
*/
|
|
|
|
#include <cvc5/cvc5.h>
|
|
|
|
#include <iostream>
|
|
|
|
#include "utils.h"
|
|
|
|
using namespace cvc5;
|
|
|
|
int main()
|
|
{
|
|
Solver slv;
|
|
|
|
// required options
|
|
slv.setOption("sygus", "true");
|
|
slv.setOption("incremental", "false");
|
|
|
|
// set the logic
|
|
slv.setLogic("LIA");
|
|
|
|
Sort integer = slv.getIntegerSort();
|
|
Sort boolean = slv.getBooleanSort();
|
|
|
|
Term zero = slv.mkInteger(0);
|
|
Term one = slv.mkInteger(1);
|
|
Term ten = slv.mkInteger(10);
|
|
|
|
// declare input variables for functions
|
|
Term x = slv.mkVar(integer, "x");
|
|
Term xp = slv.mkVar(integer, "xp");
|
|
|
|
// (ite (< x 10) (= xp (+ x 1)) (= xp x))
|
|
Term ite = slv.mkTerm(
|
|
Kind::ITE,
|
|
{slv.mkTerm(Kind::LT, {x, ten}),
|
|
slv.mkTerm(Kind::EQUAL, {xp, slv.mkTerm(Kind::ADD, {x, one})}),
|
|
slv.mkTerm(Kind::EQUAL, {xp, x})});
|
|
|
|
// define the pre-conditions, transition relations, and post-conditions
|
|
Term pre_f =
|
|
slv.defineFun("pre-f", {x}, boolean, slv.mkTerm(Kind::EQUAL, {x, zero}));
|
|
Term trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite);
|
|
Term post_f =
|
|
slv.defineFun("post-f", {x}, boolean, slv.mkTerm(Kind::LEQ, {x, ten}));
|
|
|
|
// declare the invariant-to-synthesize
|
|
Term inv_f = slv.synthFun("inv-f", {x}, boolean);
|
|
|
|
slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f);
|
|
|
|
// print solutions if available
|
|
if (slv.checkSynth().hasSolution())
|
|
{
|
|
// Output should be equivalent to:
|
|
// (
|
|
// (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
|
|
// )
|
|
std::vector<Term> terms = {inv_f};
|
|
utils::printSynthSolutions(terms, slv.getSynthSolutions(terms));
|
|
}
|
|
|
|
return 0;
|
|
}
|