From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 19 Jun 2020 16:09:45 +0000 (-0700)
Subject: Cleanup examples (#4634)
X-Git-Tag: cvc5-1.0.0~3199
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=039a642610f570f3367a73a3a29082152a2736f2;p=cvc5.git

Cleanup examples (#4634)

This commit removes examples from unsupported programming languages and
fixes a compilation issue in the sets-translate example. The issue
arised due to changes to the `DefineFunctionCommand` in commit
fd60da4a22f02f6f5b82cef3585240c1b33595e9 and wasn't detected by our CI
because the sets-translate example requires Boost.
---

diff --git a/examples/SimpleVC.ml b/examples/SimpleVC.ml
deleted file mode 100644
index d9d78586b..000000000
--- a/examples/SimpleVC.ml
+++ /dev/null
@@ -1,91 +0,0 @@
-(*********************                                                        **
-**! \file SimpleVC.ml
-*** \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 OCaml interface
-***
-*** A simple demonstration of the OCaml interface.  Compare to the
-*** C++ interface in simple_vc_cxx.cpp; they are quite similar.
-***
-*** To run, use something like:
-***
-***   LD_LIBRARY_PATH=../builds/src/bindings/ocaml/.libs \
-***     ../builds/src/bindings/cvc4_ocaml_top -I ../builds/src/bindings/ocaml \
-***     SimpleVC.ml
-***
-*** After you "make install" CVC4, it's much easier; the cvc4_ocaml_top goes in
-*** $prefix/bin, and it's automatically set up the load the .cmo and .cmi files
-*** from $prefix/lib/ocaml/cvc4, in which they get installed.  Then you just
-*** have to: cvc4_ocaml_top -I $prefix/lib/ocaml/cvc4
-***)
-
-open Swig
-open CVC4
-
-let em = new_ExprManager '()
-let smt = new_SmtEngine(em)
-
-(* Prove that for integers x and y:
- *   x > 0 AND y > 0  =>  2x + y >= 3 *)
-
-let integer = em->integerType()
-
-let x = em->mkVar(integer) (* em->mkVar("x", integer) *)
-let y = em->mkVar(integer) (* em->mkVar("y", integer) *)
-let integerZero = new_Integer '("0", 10)
-let zero = em->mkConst(integerZero)
-
-(* OK, this is really strange.  We can call mkExpr(36, ...) for
- * example, with the int value of the operator Kind we want,
- * or we can compute it.  But if we compute it, we have to rip
- * it out of its C_int, then wrap it again a C_int, in order
- * for the parser to make it go through. *)
-let geq = C_int (get_int (enum_to_int `Kind_t (``GEQ)))
-let gt = C_int (get_int (enum_to_int `Kind_t (``GT)))
-let mult = C_int (get_int (enum_to_int `Kind_t (``MULT)))
-let plus = C_int (get_int (enum_to_int `Kind_t (``PLUS)))
-let and_kind = C_int (get_int (enum_to_int `Kind_t (``AND)))
-let implies = C_int (get_int (enum_to_int `Kind_t (``IMPLIES)))
-
-(* gt = 35, but the parser screws up if we put "geq" what follows *)
-let x_positive = em->mkExpr(gt, x, zero)
-let y_positive = em->mkExpr(gt, y, zero)
-
-let integerTwo = new_Integer '("2", 10)
-let two = em->mkConst(integerTwo)
-let twox = em->mkExpr(mult, two, x)
-let twox_plus_y = em->mkExpr(plus, twox, y)
-
-let integerThree = new_Integer '("3", 10)
-let three = em->mkConst(integerThree)
-let twox_plus_y_geq_3 = em->mkExpr(geq, twox_plus_y, three)
-
-let lhs = em->mkExpr(and_kind, x_positive, y_positive)
-
-(* This fails for some reason. *)
-(* let rhs = new_Expr(twox_plus_y_geq_3)
-   let formula = new_Expr(lhs)->impExpr(rhs) *)
-
-let formula = em->mkExpr(implies, lhs, twox_plus_y_geq_3)
-
-let bformula = new_Expr(formula) in
-
-print_string "Checking entailment of formula " ;
-print_string (get_string (formula->toString ())) ;
-print_string " with CVC4." ;
-print_newline () ;
-print_string "CVC4 should report ENTAILED." ;
-print_newline () ;
-print_string "Result from CVC4 is: " ;
-print_string (get_string (smt->checkEntailed(bformula)->toString ())) ;
-print_newline ()
-;;
diff --git a/examples/SimpleVC.php b/examples/SimpleVC.php
deleted file mode 100755
index 031c0a1c5..000000000
--- a/examples/SimpleVC.php
+++ /dev/null
@@ -1,56 +0,0 @@
-#! /usr/bin/php
-##! \file SimpleVC.php
-### \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 PHP interface
-###
-### A simple demonstration of the PHP interface.  Compare to the
-### C++ interface in simple_vc_cxx.cpp; they are quite similar.
-###
-### To run, use something like:
-###
-###   ln -s ../builds/src/bindings/php/.libs/CVC4.so CVC4.so
-###   ln -s ../builds/src/bindings/php/CVC4.php CVC4.php
-###   ./SimpleVC.php
-####
-
-use strict;
-use CVC4;
-
-my $em = new CVC4::ExprManager();
-my $smt = new CVC4::SmtEngine($em);
-
-# Prove that for integers x and y:
-#   x > 0 AND y > 0  =>  2x + y >= 3
-
-my $integer = $em->integerType();
-
-my $x = $em->mkVar("x", $integer);
-my $y = $em->mkVar("y", $integer);
-my $zero = $em->mkConst(new CVC4::Integer(0));
-
-my $x_positive = $em->mkExpr($CVC4::GT, $x, $zero);
-my $y_positive = $em->mkExpr($CVC4::GT, $y, $zero);
-
-my $two = $em->mkConst(new CVC4::Integer(2));
-my $twox = $em->mkExpr($CVC4::MULT, $two, $x);
-my $twox_plus_y = $em->mkExpr($CVC4::PLUS, $twox, $y);
-
-my $three = $em->mkConst(new CVC4::Integer(3));
-my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three);
-
-my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3));
-
-print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n";
-print "CVC4 should report ENTAILED.\n";
-print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n";
-
diff --git a/examples/SimpleVC.pl b/examples/SimpleVC.pl
deleted file mode 100755
index 20ad6c737..000000000
--- a/examples/SimpleVC.pl
+++ /dev/null
@@ -1,56 +0,0 @@
-#! /usr/bin/perl -w
-##! \file SimpleVC.pl
-### \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 Perl interface
-###
-### A simple demonstration of the Perl interface.  Compare to the
-### C++ interface in simple_vc_cxx.cpp; they are quite similar.
-###
-### To run, use something like:
-###
-###   ln -s ../builds/src/bindings/perl/.libs/CVC4.so CVC4.so
-###   ln -s ../builds/src/bindings/perl/CVC4.pm CVC4.pm
-###   ./SimpleVC.pl
-####
-
-use strict;
-use CVC4;
-
-my $em = new CVC4::ExprManager();
-my $smt = new CVC4::SmtEngine($em);
-
-# Prove that for integers x and y:
-#   x > 0 AND y > 0  =>  2x + y >= 3
-
-my $integer = $em->integerType();
-
-my $x = $em->mkVar("x", $integer);
-my $y = $em->mkVar("y", $integer);
-my $zero = $em->mkConst(new CVC4::Integer(0));
-
-my $x_positive = $em->mkExpr($CVC4::GT, $x, $zero);
-my $y_positive = $em->mkExpr($CVC4::GT, $y, $zero);
-
-my $two = $em->mkConst(new CVC4::Integer(2));
-my $twox = $em->mkExpr($CVC4::MULT, $two, $x);
-my $twox_plus_y = $em->mkExpr($CVC4::PLUS, $twox, $y);
-
-my $three = $em->mkConst(new CVC4::Integer(3));
-my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three);
-
-my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3));
-
-print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n";
-print "CVC4 should report ENTAILED.\n";
-print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n";
-
diff --git a/examples/SimpleVC.rb b/examples/SimpleVC.rb
deleted file mode 100755
index 4f289d34f..000000000
--- a/examples/SimpleVC.rb
+++ /dev/null
@@ -1,57 +0,0 @@
-#! /usr/bin/ruby
-##! \file SimpleVC.rb
-### \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 Ruby interface
-###
-### A simple demonstration of the Ruby interface.  Compare to the
-### C++ interface in simple_vc_cxx.cpp; they are quite similar.
-###
-### To run, use something like:
-###
-###   ln -s ../builds/src/bindings/ruby/.libs/CVC4.so CVC4.so
-###   ./SimpleVC.rb
-####
-
-require 'CVC4'
-include CVC4 # CVC4::Integer still has to be qualified
-
-em = ExprManager.new
-smt = SmtEngine.new(em)
-
-# Prove that for integers x and y:
-#   x > 0 AND y > 0  =>  2x + y >= 3
-
-integer = em.integerType
-
-x = em.mkVar("x", integer)
-y = em.mkVar("y", integer)
-zero = em.mkConst(CVC4::Integer.new(0))
-
-x_positive = em.mkExpr(GT, x, zero)
-y_positive = em.mkExpr(GT, y, zero)
-
-two = em.mkConst(CVC4::Integer.new(2))
-twox = em.mkExpr(MULT, two, x)
-twox_plus_y = em.mkExpr(PLUS, twox, y)
-
-three = em.mkConst(CVC4::Integer.new(3))
-twox_plus_y_geq_3 = em.mkExpr(GEQ, twox_plus_y, three)
-
-formula = Expr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(Expr.new(twox_plus_y_geq_3))
-
-puts "Checking entailment of formula " + formula.toString + " with CVC4."
-puts "CVC4 should report ENTAILED."
-puts "Result from CVC4 is: " + smt.checkEntailed(formula).toString
-
-exit
-
diff --git a/examples/SimpleVC.tcl b/examples/SimpleVC.tcl
deleted file mode 100755
index 4e1c76c5a..000000000
--- a/examples/SimpleVC.tcl
+++ /dev/null
@@ -1,54 +0,0 @@
-#! /usr/bin/tclsh
-##! \file SimpleVC.tcl
-### \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 Tcl interface
-###
-### A simple demonstration of the Tcl interface.  Compare to the
-### C++ interface in simple_vc_cxx.cpp; they are quite similar.
-###
-### To run, use something like:
-###
-###   ln -s ../builds/src/bindings/tcl/.libs/CVC4.so CVC4.so
-###   ./SimpleVC.tcl
-####
-
-load CVC4.so CVC4
-
-ExprManager em
-SmtEngine smt em
-
-# Prove that for integers x and y:
-#   x > 0 AND y > 0  =>  2x + y >= 3
-
-set integer [ExprManager_integerType em]
-
-set x [ExprManager_mkVar em "x" $integer]
-set y [ExprManager_mkVar em "y" $integer]
-set zero [ExprManager_mkConst em [Integer _ 0]]
-
-set x_positive [ExprManager_mkExpr em $GT $x $zero]
-set y_positive [ExprManager_mkExpr em $GT $y $zero]
-
-set two [ExprManager_mkConst em [Integer _ 2]]
-set twox [ExprManager_mkExpr em $MULT $two $x]
-set twox_plus_y [ExprManager_mkExpr em $PLUS $twox $y]
-
-set three [ExprManager_mkConst em [Integer _ 3]]
-set twox_plus_y_geq_3 [ExprManager_mkExpr em $GEQ $twox_plus_y $three]
-
-set formula [Expr_impExpr [Expr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [Expr _2 $twox_plus_y_geq_3]]
-
-puts "Checking entailment of formula [Expr_toString $formula] with CVC4."
-puts "CVC4 should report ENTAILED."
-puts "Result from CVC4 is: [Result_toString [SmtEngine_checkEntailed smt $formula]]"
-
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 0b02288d0..5db33892f 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -341,16 +341,26 @@ int main(int argc, char* argv[])
       DefineFunctionCommand* definefun = dynamic_cast<DefineFunctionCommand*>(cmd);
 
       Command* new_cmd = NULL;
-      if(assert) {
+      if (assert)
+      {
         Expr newexpr = m.collectSortsExpr(assert->getExpr());
         new_cmd = new AssertCommand(newexpr);
-      } else if(declarefun) {
+      }
+      else if (declarefun)
+      {
         Expr newfunc = m.collectSortsExpr(declarefun->getFunction());
-        new_cmd = new DeclareFunctionCommand(declarefun->getSymbol(), newfunc, declarefun->getType());
-      } else if(definefun) {
+        new_cmd = new DeclareFunctionCommand(
+            declarefun->getSymbol(), newfunc, declarefun->getType());
+      }
+      else if (definefun)
+      {
         Expr newfunc = m.collectSortsExpr(definefun->getFunction());
         Expr newformula = m.collectSortsExpr(definefun->getFormula());
-        new_cmd = new DefineFunctionCommand(definefun->getSymbol(), newfunc, definefun->getFormals(), newformula);
+        new_cmd = new DefineFunctionCommand(definefun->getSymbol(),
+                                            newfunc,
+                                            definefun->getFormals(),
+                                            newformula,
+                                            false);
       }
 
       if(new_cmd == NULL) {