rpms/alt-ergo/F-8 README.alt-ergo, NONE, 1.1 alt-ergo.spec, NONE, 1.1 import.log, NONE, 1.1 swap0_why.why, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2

[Alan Dunn]

Author: amdunn

Update of /cvs/pkgs/rpms/alt-ergo/F-8
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv30431/F-8

Modified Files:
	.cvsignore sources 
Added Files:
	README.alt-ergo alt-ergo.spec import.log swap0_why.why 
Log Message:
Initial commit for F-8 branch.



--- NEW FILE README.alt-ergo ---
Fedora alt-ergo package:

Contains the main program alt-ergo.

Consider visiting the main Alt-Ergo site - http://alt-ergo.lri.fr -
for more documentation as it becomes available and a number of
examples of usage. Any current documentation (save the man page) is
generated by the package maintainer.

--- NEW FILE alt-ergo.spec ---
# rpmlint "no-binary" error is not really an error - see:
# https://www.redhat.com/archives/fedora-packaging/2008-August/msg00017.html
# and ocaml-ocamlgraph spec file for a discussion of this issue.

# The following are necessary for alt-ergo to depend on the correct
# version of ocaml-ocamlgraph

%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
%define debug_package %{nil}
%define _use_internal_dependency_generator 0
%define __find_requires /usr/lib/rpm/ocaml-find-requires.sh
%define __find_provides /usr/lib/rpm/ocaml-find-provides.sh

Name:		alt-ergo
Version:	0.8
Release:	3%{?dist}
Summary:	Alt-Ergo automatic theorem prover

# Note: rpmlint invalid-license warning is incorrect - I had the
# CeCILL-C license reviewed by Fedora legal, and it is now present on
# http://fedoraproject.org/wiki/Licensing

Group:		Applications/Engineering
License:	CeCILL-C
URL:		http://alt-ergo.lri.fr
Source0:	http://alt-ergo.lri.fr/http/alt-ergo-0.8.tar.gz
Source1:	swap0_why.why
Source2:	README.alt-ergo
BuildRoot:	%{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)

BuildRequires:	ocaml, ocaml-ocamlgraph-devel, prelink

%if 0%{?fedora} < 9
# There's no ocaml for ppc64 in Fedora <= 8
# bz# (will be changed when exists as a module):
ExcludeArch: ppc64
%endif

%description

Alt-Ergo is an automated theorem prover implemented in OCaml. It is
based on CC(X) - a congruence closure algorithm parameterized by an
equational theory X. This algorithm is reminiscent of the Shostak
algorithm. Currently CC(X) is instantiated by the theory of linear
arithmetics. Alt-Ergo also contains a home made SAT-solver and an
instantiation mechanism by which it fully supports quantifiers.

%prep
%setup -q

cp -p %{SOURCE1} %{SOURCE2} .

%build
# Avoid a Makefile patch by just adding this empty file, and thus autoconf
# doesn't complain (better than ignoring all status from configure)
touch version.sh.in
./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir}

%if ! %{opt}
%define opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLLEX=ocamllex
%else
%define opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
%endif

make %{opt_option}

mv CeCILL-C CeCILL-C.iso8859
iconv -f ISO-8859-1 -t UTF-8 < CeCILL-C.iso8859 > CeCILL-C
rm CeCILL-C.iso8859

%if %{opt}
strip ./alt-ergo.opt
execstack -c ./alt-ergo.opt
%endif

# Test alt-ergo on fairly trivial why file - generated from why example swap0.mlw w/why v2.14
%check
%if %opt
%define altergo ./alt-ergo.opt
%else
%define altergo ./alt-ergo.byte
%endif
%{altergo} swap0_why.why

%install
rm -rf %{buildroot}

mkdir -p %{buildroot}%{_bindir}
make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} install

%clean
rm -rf %{buildroot}

%files
%defattr(-,root,root,-)
%{_bindir}/*
%{_datadir}/%{name}
%{_mandir}/man1/alt-ergo.1.gz
%doc README.alt-ergo COPYING CeCILL-C CHANGES

%changelog
* Fri Sep 05 2008 Alan Dunn <amdunn at gmail.com> 0.8-3
- Fixed BuildRequires to add prelink (for execstack).
* Tue Aug 26 2008 Alan Dunn <amdunn at gmail.com> 0.8-2
- Fixed BuildRequires to add ocaml-ocamlgraph-devel instead of
  ocaml-ocamlgraph, made other minor changes.
* Mon Aug 25 2008 Alan Dunn <amdunn at gmail.com> 0.8-1
- Initial Fedora RPM version.


--- NEW FILE import.log ---
alt-ergo-0_8-3_fc8:F-8:alt-ergo-0.8-3.fc8.src.rpm:1220666121


--- NEW FILE swap0_why.why ---
logic eq_unit : unit, unit -> prop

logic neq_unit : unit, unit -> prop

logic eq_bool : bool, bool -> prop

logic neq_bool : bool, bool -> prop

logic bool_and : bool, bool -> bool

logic bool_or : bool, bool -> bool

logic bool_xor : bool, bool -> bool

logic bool_not : bool -> bool

axiom bool_and_def:
  (forall a:bool.
    (forall b:bool.
      ((bool_and(a, b) = true) <-> ((a = true) and (b = true)))))

axiom bool_or_def:
  (forall a:bool.
    (forall b:bool. ((bool_or(a, b) = true) <-> ((a = true) or (b = true)))))

axiom bool_xor_def:
  (forall a:bool. (forall b:bool. ((bool_xor(a, b) = true) <-> (a <> b))))

axiom bool_not_def: (forall a:bool. ((bool_not(a) = true) <-> (a = false)))

logic ite : bool, 'a1, 'a1 -> 'a1

axiom ite_true: (forall x:'a1. (forall y:'a1. (ite(true, x, y) = x)))

axiom ite_false: (forall x:'a1. (forall y:'a1. (ite(false, x, y) = y)))

logic add_int : int, int -> int

logic sub_int : int, int -> int

logic mul_int : int, int -> int

logic div_int : int, int -> int

logic mod_int : int, int -> int

logic neg_int : int -> int

logic lt_int : int, int -> prop

logic le_int : int, int -> prop

logic gt_int : int, int -> prop

logic ge_int : int, int -> prop

logic eq_int : int, int -> prop

logic neq_int : int, int -> prop

logic lt_int_bool : int, int -> bool

logic le_int_bool : int, int -> bool

logic gt_int_bool : int, int -> bool

logic ge_int_bool : int, int -> bool

logic eq_int_bool : int, int -> bool

logic neq_int_bool : int, int -> bool

axiom lt_int_bool_axiom:
  (forall x:int. (forall y:int. ((lt_int_bool(x, y) = true) <-> (x < y))))

axiom le_int_bool_axiom:
  (forall x:int. (forall y:int. ((le_int_bool(x, y) = true) <-> (x <= y))))

axiom gt_int_bool_axiom:
  (forall x:int. (forall y:int. ((gt_int_bool(x, y) = true) <-> (x > y))))

axiom ge_int_bool_axiom:
  (forall x:int. (forall y:int. ((ge_int_bool(x, y) = true) <-> (x >= y))))

axiom eq_int_bool_axiom:
  (forall x:int. (forall y:int. ((eq_int_bool(x, y) = true) <-> (x = y))))

axiom neq_int_bool_axiom:
  (forall x:int. (forall y:int. ((neq_int_bool(x, y) = true) <-> (x <> y))))

logic add_real : real, real -> real

logic sub_real : real, real -> real

logic mul_real : real, real -> real

logic div_real : real, real -> real

logic pow_real : real, real -> real

logic neg_real : real -> real

logic abs_real : real -> real

logic sqrt_real : real -> real

logic real_of_int : int -> real

logic int_of_real : real -> int

logic lt_real : real, real -> prop

logic le_real : real, real -> prop

logic gt_real : real, real -> prop

logic ge_real : real, real -> prop

logic eq_real : real, real -> prop

logic neq_real : real, real -> prop

logic lt_real_bool : real, real -> bool

logic le_real_bool : real, real -> bool

logic gt_real_bool : real, real -> bool

logic ge_real_bool : real, real -> bool

logic eq_real_bool : real, real -> bool

logic neq_real_bool : real, real -> bool

axiom lt_real_bool_axiom:
  (forall x:real. (forall y:real. ((lt_real_bool(x, y) = true) <-> (x < y))))

axiom le_real_bool_axiom:
  (forall x:real.
    (forall y:real. ((le_real_bool(x, y) = true) <-> (x <= y))))

axiom gt_real_bool_axiom:
  (forall x:real. (forall y:real. ((gt_real_bool(x, y) = true) <-> (x > y))))

axiom ge_real_bool_axiom:
  (forall x:real.
    (forall y:real. ((ge_real_bool(x, y) = true) <-> (x >= y))))

axiom eq_real_bool_axiom:
  (forall x:real. (forall y:real. ((eq_real_bool(x, y) = true) <-> (x = y))))

axiom neq_real_bool_axiom:
  (forall x:real.
    (forall y:real. ((neq_real_bool(x, y) = true) <-> (x <> y))))

logic int_max : int, int -> int

logic int_min : int, int -> int

logic real_max : real, real -> real

logic real_min : real, real -> real

predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))

type 'a farray

logic access : 'a1 farray, int -> 'a1

logic update : 'a1 farray, int, 'a1 -> 'a1 farray

axiom access_update:
  (forall a:'a1 farray.
    (forall i:int. (forall v:'a1. (access(update(a, i, v), i) = v))))

axiom access_update_neq:
  (forall a:'a1 farray.
    (forall i:int.
      (forall j:int.
        (forall v:'a1.
          ((i <> j) -> (access(update(a, i, v), j) = access(a, j)))))))

logic array_length : 'a1 farray -> int

predicate sorted_array(t: int farray, i: int, j: int) =
  (forall k1:int.
    (forall k2:int.
      ((((i <= k1) and (k1 <= k2)) and (k2 <= j)) -> (access(t,
       k1) <= access(t, k2)))))

predicate exchange(a1: 'a1 farray, a2: 'a1 farray, i: int, j: int) =
  ((array_length(a1) = array_length(a2)) and
   ((access(a1, i) = access(a2, j)) and
    ((access(a2, i) = access(a1, j)) and
     (forall k:int.
       (((k <> i) and (k <> j)) -> (access(a1, k) = access(a2, k)))))))

logic permut : 'a1 farray, 'a1 farray, int, int -> prop

axiom permut_refl:
  (forall t:'a1 farray. (forall l:int. (forall u:int. permut(t, t, l, u))))

axiom permut_sym:
  (forall t1:'a1 farray.
    (forall t2:'a1 farray.
      (forall l:int.
        (forall u:int. (permut(t1, t2, l, u) -> permut(t2, t1, l, u))))))

axiom permut_trans:
  (forall t1:'a1 farray.
    (forall t2:'a1 farray.
      (forall t3:'a1 farray.
        (forall l:int.
          (forall u:int.
            (permut(t1, t2, l, u) ->
             (permut(t2, t3, l, u) -> permut(t1, t3, l, u))))))))

axiom permut_exchange:
  (forall a1:'a1 farray.
    (forall a2:'a1 farray.
      (forall l:int.
        (forall u:int.
          (forall i:int.
            (forall j:int.
              (((l <= i) and (i <= u)) ->
               (((l <= j) and (j <= u)) ->
                (exchange(a1, a2, i, j) -> permut(a1, a2, l, u))))))))))

axiom exchange_upd:
  (forall a:'a1 farray.
    (forall i:int.
      (forall j:int. exchange(a, update(update(a, i, access(a, j)), j,
        access(a, i)), i, j))))

axiom permut_weakening:
  (forall a1:'a1 farray.
    (forall a2:'a1 farray.
      (forall l1:int.
        (forall r1:int.
          (forall l2:int.
            (forall r2:int.
              ((((l1 <= l2) and (l2 <= r2)) and (r2 <= r1)) ->
               (permut(a1, a2, l2, r2) -> permut(a1, a2, l1, r1)))))))))

axiom permut_eq:
  (forall a1:'a1 farray.
    (forall a2:'a1 farray.
      (forall l:int.
        (forall u:int.
          ((l <= u) ->
           (permut(a1, a2, l, u) ->
            (forall i:int.
              (((i < l) or (u < i)) -> (access(a2, i) = access(a1, i))))))))))

predicate permutation(a1: 'a1 farray, a2: 'a1 farray) = permut(a1, a2, 0,
  (array_length(a1) - 1))

axiom array_length_update:
  (forall a:'a1 farray.
    (forall i:int.
      (forall v:'a1. (array_length(update(a, i, v)) = array_length(a)))))

axiom permut_array_length:
  (forall a1:'a1 farray.
    (forall a2:'a1 farray.
      (forall l:int.
        (forall u:int.
          (permut(a1, a2, l, u) -> (array_length(a1) = array_length(a2)))))))

goal swap1_po_1:
  forall x0:int.
  forall y:int.
  forall x:int.
  (x = y) ->
  forall y0:int.
  (y0 = x0) ->
  ((x = y) and (y0 = x0))

goal swap2_po_1:
  forall x0:int.
  forall y:int.
  forall x:int.
  (x = y) ->
  forall y0:int.
  (y0 = x0) ->
  ((x = y) and (y0 = x0))

goal swap3_po_1:
  forall a0:int.
  forall b:int.
  forall a:int.
  (a = b) ->
  forall b0:int.
  (b0 = a0) ->
  ((a = b) and (b0 = a0))

goal call_swap3_y_x_po_1:
  forall x0:int.
  forall y0:int.
  forall x:int.
  forall y:int.
  ((y = x0) and (x = y0)) ->
  ((x = y0) and (y = x0))

goal swap4_po_1:
  forall a:int.
  forall b:int.
  forall tmp:int.
  (tmp = a) ->
  forall a0:int.
  (a0 = b) ->
  forall b0:int.
  (b0 = tmp) ->
  ((a0 = b) and (b0 = a))

goal call_swap4_x_y_po_1:
  forall x:int.
  forall y:int.
  (x = 3) ->
  forall x0:int.
  forall y0:int.
  ((x0 = y) and (y0 = x)) ->
  (y0 = 3)

goal call_swap4_y_x_po_1:
  forall x:int.
  forall y:int.
  (x = 3) ->
  forall x0:int.
  forall y0:int.
  ((y0 = x) and (x0 = y)) ->
  (y0 = 3)



Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/alt-ergo/F-8/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- .cvsignore	5 Sep 2008 21:05:34 -0000	1.1
+++ .cvsignore	6 Sep 2008 01:59:56 -0000	1.2
@@ -0,0 +1 @@
+alt-ergo-0.8.tar.gz


Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/alt-ergo/F-8/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- sources	5 Sep 2008 21:05:34 -0000	1.1
+++ sources	6 Sep 2008 01:59:56 -0000	1.2
@@ -0,0 +1 @@
+ce8e9fbe24c0c2d7328b4b70ac0c2f9e  alt-ergo-0.8.tar.gz