mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
129dadba47
* ITE removal fixed to be context-dependent (on UserContext). Resolves incrementality bugs 376 and 396 (which had given wrong answers). * some bugfixes for incrementality that Dejan found (fixes bug 394) * fix for bug in SmtEngine::getValue() where definitions weren't respected (partially resolves bug 411, but get-model is still broken). * change status of microwave21.ec.minimized.smt2 (it's actually unsat, but was labeled sat); re-enable it for "make regress" Also: * --check-model doesn't fail if quantified assertions don't simplify away. * fix some examples, and the Java system test, for the disappearance of the BoolExpr class * add copy constructor to array type enumerator (the type enumerator framework requires copy ctors, and the automatically-generated copy ctor was copying pointers that were then deleted, leaving dangling pointers in the copy and causing segfaults) * --dump=assertions now implies --dump=skolems * --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow you to dump before/after a particular preprocessing pass. E.g., --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning. "--dump=assertions" by itself is after all preprocessing, just before CNF conversion. * minor fixes to dumping output * include Model in language bindings Minor refactoring/misc: * fix compiler warning in src/theory/model.cpp * remove unnecessary SmtEngine::printModel(). * mkoptions script doesn't give progress output if stdout isn't a terminal (e.g., if it's written to a log, or piped through less(1), or whatever). * add some type enumerator unit tests * de-emphasize --parse-only and --preprocess-only (they aren't really "common" options) * fix some exception throw() specifications in SmtEngine * minor documentation clarifications
73 lines
2.3 KiB
Java
73 lines
2.3 KiB
Java
/********************* */
|
|
/*! \file SimpleVC.java
|
|
** \verbatim
|
|
** Original author: mdeters
|
|
** Major contributors: none
|
|
** Minor contributors (to current version): none
|
|
** This file is part of the CVC4 prototype.
|
|
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
|
|
** Courant Institute of Mathematical Sciences
|
|
** New York University
|
|
** See the file COPYING in the top-level source directory for licensing
|
|
** information.\endverbatim
|
|
**
|
|
** \brief A simple demonstration of the Java interface
|
|
**
|
|
** A simple demonstration of the Java interface.
|
|
**
|
|
** To run the resulting class file, you need to do something like the
|
|
** following:
|
|
**
|
|
** java \
|
|
** -classpath path/to/CVC4.jar \
|
|
** -Djava.library.path=/dir/containing/java/CVC4.so \
|
|
** SimpleVC
|
|
**
|
|
** For example, if you are building CVC4 without specifying your own
|
|
** build directory, the build process puts everything in builds/, and
|
|
** you can run this example (after building it with "make") like this:
|
|
**
|
|
** java \
|
|
** -classpath builds/examples:builds/src/bindings/CVC4.jar \
|
|
** -Djava.library.path=builds/src/bindings/java/.libs \
|
|
** SimpleVC
|
|
**/
|
|
|
|
import edu.nyu.acsys.CVC4.*;
|
|
|
|
public class SimpleVC {
|
|
public static void main(String[] args) {
|
|
System.loadLibrary("cvc4jni");
|
|
|
|
ExprManager em = new ExprManager();
|
|
SmtEngine smt = new SmtEngine(em);
|
|
|
|
// Prove that for integers x and y:
|
|
// x > 0 AND y > 0 => 2x + y >= 3
|
|
|
|
Type integer = em.integerType();
|
|
|
|
Expr x = em.mkVar("x", integer);
|
|
Expr y = em.mkVar("y", integer);
|
|
Expr zero = em.mkConst(new Rational(0));
|
|
|
|
Expr x_positive = em.mkExpr(Kind.GT, x, zero);
|
|
Expr y_positive = em.mkExpr(Kind.GT, y, zero);
|
|
|
|
Expr two = em.mkConst(new Rational(2));
|
|
Expr twox = em.mkExpr(Kind.MULT, two, x);
|
|
Expr twox_plus_y = em.mkExpr(Kind.PLUS, twox, y);
|
|
|
|
Expr three = em.mkConst(new Rational(3));
|
|
Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three);
|
|
|
|
Expr formula =
|
|
new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)).
|
|
impExpr(new Expr(twox_plus_y_geq_3));
|
|
|
|
System.out.println("Checking validity of formula " + formula + " with CVC4.");
|
|
System.out.println("CVC4 should report VALID.");
|
|
System.out.println("Result from CVC4 is: " + smt.query(formula));
|
|
}
|
|
}
|