February 2004 - PPL-devel - BUGSENG Mailman

Bignums
by Roberto Bagnara 14 May '04

14 May '04

Hi there, I believe the following behavior of the CVS version of YAP witnesses a bug (or, quite possible, a misunderstanding on my part): $ yap [ Restoring file /usr/local/lib/Yap/startup ] [ YAP version Yap-4.3.23 ] ?- current_prolog_flag(bounded,X). X = false ? ?- X is 333333333333333, integer(X). no ?- X is 33333333, integer(X). X = 33333333 ? ?- X is 333333333333333, float(X). no ?- X is 333333333333333, number_chars(X,L). X = 333333333333333, L = [51,51,51,51,51,51,51,51,51,51,51,51,51,51,51] ? In words, the Prolog engine first declares it is employing unbounded integers, then it silently converts an integer numeral to... to what? Is this a bug? Am I missing something? All the best Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

2 5

ppl TODO
by Roberto Bagnara 25 Feb '04

25 Feb '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-02-25 17:59:16 Modified files: . : TODO Log message: Added a (monster) configure command line to compile with Comeau C/C++ compiler. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/TODO.diff?cvsroot=ppl&r1=1.65…

1 0

ppl TODO
by Roberto Bagnara 25 Feb '04

25 Feb '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-02-25 14:11:28 Modified files: . : TODO Log message: Started adding instructions on how to compile with other C++ compilers. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/TODO.diff?cvsroot=ppl&r1=1.64…

1 0

ppl/interfaces/C ppl_c.h.in
by Roberto Bagnara 24 Feb '04

24 Feb '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-02-24 19:02:28 Modified files: interfaces/C : ppl_c.h.in Log message: Fixed the comments for ppl_Polyhedron_minimize() and ppl_Polyhedron_maximize(). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/interfaces/C/ppl_c.h.in.diff?…

1 0

Poliedri convessi per l'analisi e la verifica di sistemi hardware e software
by Roberto Bagnara 23 Feb '04

23 Feb '04

[Con preghiera di diffusione e scuse per l'eventuale ricezione di copie multiple. RB] POLIEDRI CONVESSI PER L'ANALISI E LA VERIFICA DI SISTEMI HARDWARE E SOFTWARE ============================================================================ CICLO DI SEMINARI ----------------- http://www.cs.unipr.it/ppl/seminars_2003_2004 --------------------------------------------- Come annunciato in precedenza, il giorno 26 febbraio 2004 si terra`, presso il Dipartimento di Matematica dell'Universita` di Parma, il terzo e ultimo gruppo di seminari nell'ambito del ciclo sui poliedri convessi e le loro applicazioni nel campo dell'analisi e della verifica di sistemi hardware e software. I seminari avranno luogo secondo il seguente calendario (i primi 6 seminari si sono tenuti il 18 e 19 novembre e il 10 e 11 dicembre 2003). Per ulteriori informazioni e aggiornamenti si rimanda alla pagina http://www.cs.unipr.it/ppl/seminars_2003_2004 7) February 26th, 2004, 14:30 Roberto Bagnara, Dipartimento di Matematica, University of Parma, Italy Representation and Manipulation of Not Necessarily Closed Convex Polyhedra 8) February 26th, 2004, 15:45 Enea Zaffanella, Dipartimento di Matematica, University of Parma, Italy Widenings for Powerset Domains with Applications to Finite Sets of Polyhedra ---------------------------------------------------------------------- Date: Thursday, February 26, 2004 Time: 14:30 Speaker: Roberto Bagnara Dipartimento di Matematica, University of Parma, Italy Title: Representation and Manipulation of Not Necessarily Closed Convex Polyhedra Abstract: Convex polyhedra, commonly employed for the analysis and verification of both hardware and software, may be defined either by a finite set of linear inequality constraints or by finite sets of generating points and rays of the polyhedron. Although most implementations of the polyhedral operations assume that the polyhedra are topologically closed (i.e., all the constraints defining them are non-strict), several analyzers and verifiers need to compute on a domain of convex polyhedra that are not necessarily closed (NNC). We propose a generalization of the well-known theorems by Minkowski and Weyl, where the concept of generator of an NNC polyhedron is extended to also account for the closure points of the polyhedron. In particular, we show that any NNC polyhedron can be defined directly by means of an extended generator system, namely, a triple of finite sets containing rays, points and closure points of the polyhedron. We propose two alternative implementations for NNC polyhedra, discussing the relative benefits and how the choice of representation can affect the efficiency of the polyhedral operations. We also provide a novel solution to the issue of providing a non-redundant description of NNC polyhedra. Place: Sala Riunioni Department of Mathematics University of Parma Via D'Azeglio, 85/A Parma, Italy ====================================================================== Date: Thursday, February 26, 2004 Time: 15:45 Speaker: Enea Zaffanella Dipartimento di Matematica, University of Parma, Italy Title: Widenings for Powerset Domains with Applications to Finite Sets of Polyhedra Abstract: The finite powerset construction upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. In this talk we present three generic widening operators for the finite powerset abstract domain. All widenings are obtained by lifting any widening operator defined on the base-level abstract domain and are parametric with respect to the specification of a few additional operators. We illustrate the proposed techniques by instantiating our widenings on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known. Place: Sala Riunioni Department of Mathematics University of Parma Via D'Azeglio, 85/A Parma, Italy ---------------------------------------------------------------------- -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

ppl/src AskTell.defs.hh AskTell.inlines.hh
by Roberto Bagnara 22 Feb '04

22 Feb '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-02-22 18:06:18 Modified files: src : AskTell.defs.hh AskTell.inlines.hh Log message: AskTell<CS>::add_constraints() now takes a ConSys by const reference. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/AskTell.defs.hh.diff?cvsr… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/AskTell.inlines.hh.diff?c…

1 0

ppl/src Polyhedra_PowerSet.inlines.hh
by Roberto Bagnara 22 Feb '04

22 Feb '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-02-22 18:02:15 Modified files: src : Polyhedra_PowerSet.inlines.hh Log message: Avoid making unnecessary copies. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedra_PowerSet.inline…

1 0

ppl/src Polyhedron_public.cc Polyhedron_wideni ...
by Roberto Bagnara 22 Feb '04

22 Feb '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-02-22 17:59:29 Modified files: src : Polyhedron_public.cc Polyhedron_widenings.cc Log message: Use the add_recycled_*() methods whenever necessary or desirable. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedron_public.cc.diff… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedron_widenings.cc.d…

1 0

ppl/src C_Polyhedron.cc NNC_Polyhedron.cc Poly ...
by Roberto Bagnara 22 Feb '04

22 Feb '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-02-22 17:55:23 Modified files: src : C_Polyhedron.cc NNC_Polyhedron.cc Polyhedra_PowerSet.inlines.hh Polyhedron_public.cc Polyhedron_widenings.cc Log message: Use the add_recycled_*() methods whenever necessary or desirable. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/C_Polyhedron.cc.diff?cvsr… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/NNC_Polyhedron.cc.diff?cv… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedra_PowerSet.inline… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedron_public.cc.diff… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedron_widenings.cc.d…

1 0

ppl/interfaces/C/lpenum lpenum.c
by Roberto Bagnara 22 Feb '04

22 Feb '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-02-22 17:36:22 Modified files: interfaces/C/lpenum: lpenum.c Log message: Error message improved. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/interfaces/C/lpenum/lpenum.c.…

1 0