diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-04 14:59:19 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-04 16:59:19 -0500 |
commit | 747a9a248da073911e1c0da34c38f0648421a087 (patch) | |
tree | 98449a71c66d0ad427b8c8dc6f0ed1b9fbccdfbe /examples | |
parent | 29bf7d6a937ab50c4dd92a30d7beb36a4001ead6 (diff) |
Remove CVC3 compatibility layer (#2418)
Diffstat (limited to 'examples')
-rw-r--r-- | examples/Makefile.am | 34 | ||||
-rw-r--r-- | examples/SimpleVCCompat.java | 68 | ||||
-rw-r--r-- | examples/simple_vc_compat_c.c | 60 | ||||
-rw-r--r-- | examples/simple_vc_compat_cxx.cpp | 62 |
4 files changed, 0 insertions, 224 deletions
diff --git a/examples/Makefile.am b/examples/Makefile.am index 0f5c7db98..a39a51382 100644 --- a/examples/Makefile.am +++ b/examples/Makefile.am @@ -10,25 +10,11 @@ noinst_PROGRAMS = \ simple_vc_cxx \ translator - -if CVC4_BUILD_LIBCOMPAT -noinst_PROGRAMS += \ - simple_vc_compat_cxx -if CVC4_LANGUAGE_BINDING_C -noinst_PROGRAMS += \ - simple_vc_compat_c -endif -endif - noinst_DATA = if CVC4_LANGUAGE_BINDING_JAVA noinst_DATA += \ SimpleVC.class -if CVC4_BUILD_LIBCOMPAT -noinst_DATA += \ - SimpleVCCompat.class -endif endif @@ -38,18 +24,6 @@ simple_vc_cxx_LDADD = \ @builddir@/../src/parser/libcvc4parser.la \ @builddir@/../src/libcvc4.la -simple_vc_compat_cxx_SOURCES = \ - simple_vc_compat_cxx.cpp -simple_vc_compat_cxx_LDADD = \ - @builddir@/../src/compat/libcvc4compat.la \ - @builddir@/../src/parser/libcvc4parser.la \ - @builddir@/../src/libcvc4.la - -simple_vc_compat_c_SOURCES = \ - simple_vc_compat_c.c -simple_vc_compat_c_LDADD = \ - @builddir@/../src/bindings/compat/c/libcvc4bindings_c_compat.la - translator_SOURCES = \ translator.cpp translator_LDADD = \ @@ -58,12 +32,9 @@ translator_LDADD = \ SimpleVC.class: SimpleVC.java $(AM_V_JAVAC)$(JAVAC) -classpath "@builddir@/../src/bindings/CVC4.jar" -d "@builddir@" $< -SimpleVCCompat.class: SimpleVCCompat.java - $(AM_V_JAVAC)$(JAVAC) -classpath "@builddir@/../src/bindings/compat/java/CVC4compat.jar" -d "@builddir@" $< EXTRA_DIST = \ SimpleVC.java \ - SimpleVCCompat.java \ SimpleVC.ml \ SimpleVC.php \ SimpleVC.pl \ @@ -74,12 +45,8 @@ EXTRA_DIST = \ if STATIC_BINARY simple_vc_cxx_LINK = $(CXXLINK) -all-static -simple_vc_compat_cxx_LINK = $(CXXLINK) -all-static -simple_vc_compat_c_LINK = $(LINK) -all-static else simple_vc_cxx_LINK = $(CXXLINK) -simple_vc_compat_cxx_LINK = $(CXXLINK) -simple_vc_compat_c_LINK = $(LINK) endif # for installation @@ -92,4 +59,3 @@ MOSTLYCLEANFILES = $(noinst_DATA) AM_V_JAVAC = $(am__v_JAVAC_$(V)) am__v_JAVAC_ = $(am__v_JAVAC_$(AM_DEFAULT_VERBOSITY)) am__v_JAVAC_0 = @echo " JAVAC " $@; - diff --git a/examples/SimpleVCCompat.java b/examples/SimpleVCCompat.java deleted file mode 100644 index 160b24a14..000000000 --- a/examples/SimpleVCCompat.java +++ /dev/null @@ -1,68 +0,0 @@ -/********************* */ -/*! \file SimpleVCCompat.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** 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 simple demonstration of the Java compatibility interface - ** (quite similar to the old CVC3 Java interface) - ** - ** A simple demonstration of the Java compatibility interface - ** (quite similar to the old CVC3 Java interface). - ** - ** To run the resulting class file, you need to do something like the - ** following: - ** - ** java \ - ** -classpath path/to/CVC4compat.jar \ - ** -Djava.library.path=/dir/containing/libcvc4bindings_java_compat.so \ - ** SimpleVCCompat - ** - ** 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/compat/java/CVC4compat.jar \ - ** -Djava.library.path=builds/src/bindings/compat/java/.libs \ - ** SimpleVCCompat - **/ - -import cvc3.*; - -public class SimpleVCCompat { - public static void main(String[] args) { - ValidityChecker vc = ValidityChecker.create(); - - // Prove that for integers x and y: - // x > 0 AND y > 0 => 2x + y >= 3 - - Type integer = vc.intType(); - - Expr x = vc.varExpr("x", integer); - Expr y = vc.varExpr("y", integer); - Expr zero = vc.ratExpr(0); - - Expr x_positive = vc.gtExpr(x, zero); - Expr y_positive = vc.gtExpr(y, zero); - - Expr two = vc.ratExpr(2); - Expr twox = vc.multExpr(two, x); - Expr twox_plus_y = vc.plusExpr(twox, y); - - Expr three = vc.ratExpr(3); - Expr twox_plus_y_geq_3 = vc.geExpr(twox_plus_y, three); - - Expr formula = vc.impliesExpr(vc.andExpr(x_positive, y_positive), - 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: " + vc.query(formula)); - } -} diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c deleted file mode 100644 index ff913dd83..000000000 --- a/examples/simple_vc_compat_c.c +++ /dev/null @@ -1,60 +0,0 @@ -/********************* */ -/*! \file simple_vc_compat_c.c - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** 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 simple demonstration of the C compatibility interface - ** (quite similar to the old CVC3 C interface) - ** - ** A simple demonstration of the C compatibility interface - ** (quite similar to the old CVC3 C interface). - **/ - -#include <stdio.h> -#include <stdlib.h> - -// Use this after CVC4 is properly installed. -// #include <cvc4/bindings/compat/c/c_interface.h> -#include "bindings/compat/c/c_interface.h" - -int main() { - VC vc = vc_createValidityChecker(NULL); - - /* Prove that for integers x and y: - * x > 0 AND y > 0 => 2x + y >= 3 */ - - Type integer = vc_intType(vc); - - Expr x = vc_varExpr(vc, "x", integer); - Expr y = vc_varExpr(vc, "y", integer); - Expr zero = vc_ratExpr(vc, 0, 1); - - Expr x_positive = vc_gtExpr(vc, x, zero); - Expr y_positive = vc_gtExpr(vc, y, zero); - - Expr two = vc_ratExpr(vc, 2, 1); - Expr twox = vc_multExpr(vc, two, x); - Expr twox_plus_y = vc_plusExpr(vc, twox, y); - - Expr three = vc_ratExpr(vc, 3, 1); - Expr twox_plus_y_geq_3 = vc_geExpr(vc, twox_plus_y, three); - - Expr formula = vc_impliesExpr(vc, vc_andExpr(vc, x_positive, y_positive), - twox_plus_y_geq_3); - - char* formulaString = vc_printExprString(vc, formula); - - printf("Checking validity of formula %s with CVC4.\n", formulaString); - printf("CVC4 should return 1 (meaning VALID).\n"); - printf("Result from CVC4 is: %d\n", vc_query(vc, formula)); - - free(formulaString); - - return 0; -} diff --git a/examples/simple_vc_compat_cxx.cpp b/examples/simple_vc_compat_cxx.cpp deleted file mode 100644 index 8986aaeca..000000000 --- a/examples/simple_vc_compat_cxx.cpp +++ /dev/null @@ -1,62 +0,0 @@ -/********************* */ -/*! \file simple_vc_compat_cxx.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** 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 simple demonstration of the C++ compatibility interface - ** (quite similar to the old CVC3 C++ interface) - ** - ** A simple demonstration of the C++ compatibility interface (quite - ** similar to the old CVC3 C++ interface). Note that the library is - ** named "libcvc4compat," to mark it as being part of CVC4, but the - ** header file is "cvc3_compat.h" to indicate the similarity to the - ** CVC3 interface, and the namespace is "CVC3". CVC3::Expr and - ** CVC4::Expr are incompatible; to avoid confusion, it is best to not - ** include both the CVC3 and CVC4 interface headers. - **/ - -#include <iostream> - -// #include <cvc4/compat/cvc3_compat.h> // use this after CVC4 is properly installed -#include "compat/cvc3_compat.h" - -using namespace std; -using namespace CVC3; - -int main() { - ValidityChecker* vc = ValidityChecker::create(); - - // Prove that for integers x and y: - // x > 0 AND y > 0 => 2x + y >= 3 - - Type integer = vc->intType(); - - Expr x = vc->varExpr("x", integer); - Expr y = vc->varExpr("y", integer); - Expr zero = vc->ratExpr(0); - - Expr x_positive = vc->gtExpr(x, zero); - Expr y_positive = vc->gtExpr(y, zero); - - Expr two = vc->ratExpr(2); - Expr twox = vc->multExpr(two, x); - Expr twox_plus_y = vc->plusExpr(twox, y); - - Expr three = vc->ratExpr(3); - Expr twox_plus_y_geq_3 = vc->geExpr(twox_plus_y, three); - - Expr formula = vc->impliesExpr(vc->andExpr(x_positive, y_positive), - twox_plus_y_geq_3); - - cout << "Checking validity of formula " << formula << " with CVC4." << endl; - cout << "CVC4 should report VALID." << endl; - cout << "Result from CVC4 is: " << vc->query(formula) << endl; - - return 0; -} |