mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
cfeaf40ed6
This renames api::Solver::checkValidAssuming to checkEntailed and removes api::Solver::checkValid. Internally, SmtEngine::query is renamed to SmtEngine::checkEntailed, and these changes are further propagated to the Result class.
36 lines
1.3 KiB
Java
36 lines
1.3 KiB
Java
/********************* */
|
|
/*! \file HelloWorld.java
|
|
** \verbatim
|
|
** Top contributors (to current version):
|
|
** Morgan Deters, Tim King
|
|
** This file is part of the CVC4 project.
|
|
** Copyright (c) 2009-2019 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.\endverbatim
|
|
**
|
|
** This file is part of the CVC4 project.
|
|
** Copyright (c) 2009-2018 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.\endverbatim
|
|
**
|
|
** \brief A very simple CVC4 example
|
|
**
|
|
** A very simple CVC4 tutorial example.
|
|
**/
|
|
|
|
import edu.stanford.CVC4.*;
|
|
|
|
public class HelloWorld {
|
|
public static void main(String[] args) {
|
|
System.loadLibrary("cvc4jni");
|
|
|
|
ExprManager em = new ExprManager();
|
|
Expr helloworld = em.mkVar("Hello World!", em.booleanType());
|
|
SmtEngine smt = new SmtEngine(em);
|
|
|
|
System.out.println(helloworld + " is " + smt.checkEntailed(helloworld));
|
|
}
|
|
}
|