Remove CVC3 compatibility layer (#2418)

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;
-}