+++ /dev/null
-(********************* **
-**! \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 ()
-;;
+++ /dev/null
-#! /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";
-
+++ /dev/null
-#! /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";
-
+++ /dev/null
-#! /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
-
+++ /dev/null
-#! /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]]"
-
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) {
projects / cvc5.git / commitdiff