Skip to content

GitLab

Commit 9f892d0a authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.102 Mon, 07 Oct 2002 17:53:39 +0200 by jahier 

Parent-Version:      0.101
Version-Log:

Add cuddaux and mlcuddidl to the project.

Also clean-up Makefiles etc in order to make the installation
process as automatic as possible.

Project-Description: Lurette
parent 47cf1f46
Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ 9f892d0a
......@@ -6,96 +6,134 @@
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
(test/passerelle.luc 984 1032789516 b/17_passerelle 1.8)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(bin/Makefile 1282 1033738731 c/20_Makefile 1.3)
(bin/Makefile.gen_stubs 472 1030532285 b/42_Makefile.g 1.2)
(test/temp_float.luc 728 1032789516 b/51_temp_float 1.3)
(test/ControleurPorte.rif.exp 4756 1032789516 b/29_Controleur 1.9)
(test/ControleurPorte.rif.exp 4756 1034006019 b/29_Controleur 1.10)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(mlcuddidl/Makefile 7150 1034006019 d/9_Makefile 1.1)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(mlcuddidl/session.ml 603 1034006019 c/37_session.ml 1.1)
(cuddaux/cuddauxGenCof.c 12011 1034006019 c/29_cuddauxGen 1.1)
(mlcuddidl/rdd.idl 14806 1034006019 c/42_rdd.idl 1.1)
(source/constraint.mli 1478 1033732198 c/18_constraint 1.4)
(cuddaux/cuddauxMisc.c 13842 1034006019 c/27_cuddauxMis 1.1)
(mlcuddidl/sedscript 203 1034006019 c/38_sedscript 1.1)
(source/automata.mli 3396 1033738731 b/46_automata.m 1.3)
(test/heater_int.rif.exp 860 1033397911 b/28_heater_int 1.8)
(test/heater_int.rif.exp 860 1034006019 b/28_heater_int 1.9)
(source/ne.ml 9140 1033723811 c/21_ne.ml 1.1)
(bin/Makefile.lurette_lib 1976 1033397911 c/2_Makefile.l 1.4)
(source/value.mli 1101 1033723811 c/24_value.mli 1.1)
(user-rules.skel 973 1034006019 c/25_user-rules 1.1)
(source/Makefile.gen_stubs 333 1034006019 b/42_Makefile.g 1.3)
(test/temp_int.luc 685 1033723811 b/50_temp_int.e 1.3)
(source/luc_exe.ml 12114 1033738731 b/32_ima_exe.ml 1.20)
(test/heater_float.rif.exp 1459 1033397911 b/30_heater_flo 1.9)
(test/heater_float.rif.exp 1459 1034006019 b/30_heater_flo 1.10)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7)
(ihm/xlurette/makefile 783 1032355637 c/16_makefile 1.1)
(ihm/xlurette/makefile 1283 1034006019 c/16_makefile 1.2)
(test/usager.luc 495 1032789516 b/14_usager.env 1.9)
(mlcuddidl/manager.ml 8017 1034006019 c/47_manager.ml 1.1)
(cuddaux/cuddauxInt.h 2058 1034006019 c/28_cuddauxInt 1.1)
(cuddaux/cuddauxTDGenCof.c 15712 1034006019 c/26_cuddauxTDG 1.1)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/env.ml 8013 1027349504 16_env.ml 1.29)
(demo/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1)
(source/Makefile.show_luc 976 1034006019 b/40_Makefile.s 1.6)
(source/env_state.mli 6734 1033125605 50_env_state. 1.24)
(mlcuddidl/idd.ml 7061 1034006019 d/0_idd.ml 1.1)
(source/print.mli 1145 1033397911 46_print.mli 1.12)
(test/Makefile 105 1031732392 c/0_Makefile 1.4)
(mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1)
(test/Makefile 99 1034006019 c/0_Makefile 1.5)
(source/parse_env.ml 24584 1033723811 41_parse_env. 1.29)
(ihm/xlurette/xlurette_glade_main.ml 16705 1032789516 c/12_xlurette_g 1.6)
(demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(source/solver.ml 31802 1033732198 39_solver.ml 1.32)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(source/lurette.ml 13532 1033738731 12_lurette.ml 1.54)
(source/Makefile 1021 1034006019 c/20_Makefile 1.4)
(source/util.ml 15664 1033723811 35_util.ml 1.27)
(test/time.res 5580 1033738731 b/49_time.res 1.14)
(mlcuddidl/manager.mli 7912 1034006019 c/46_manager.ml 1.1)
(test/time.res 5580 1034006019 b/49_time.res 1.15)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5)
(source/command_line_luc_exe.mli 1082 1033738731 b/34_command_li 1.4)
(source/command_line_luc_exe.mli 1082 1034006019 b/34_command_li 1.5)
(source/Makefile.lucky 2303 1034006019 b/41_Makefile.i 1.5)
(TAGS 9825 1007379917 21_TAGS 1.6)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(mlcuddidl/rdd.ml 8746 1034006019 c/41_rdd.ml 1.1)
(source/Makefile.lurette_lib 2052 1034006019 c/2_Makefile.l 1.5)
(source/parse_env.mli 1025 1033738731 40_parse_env. 1.10)
(source/gen_stubs.ml 34560 1033734088 24_generate_l 1.37)
(OcamlMakefile 22581 1033397911 17_OcamlMakef 1.42)
(OcamlMakefile 22584 1034006019 17_OcamlMakef 1.43)
(source/command_line.ml 4625 1031053030 b/20_command_li 1.8)
(mlcuddidl/bdd.ml 10889 1034006019 d/6_bdd.ml 1.1)
(mlcuddidl/idd_caml.c 15964 1034006019 c/50_idd_caml.c 1.1)
(cuddaux/cuddauxCompose.c 13638 1034006019 c/30_cuddauxCom 1.1)
(test/porte.luc 1050 1032789516 b/16_porte.env 1.8)
(make_lurette 1303 1032940601 27_make_luret 1.16)
(make_lurette 1306 1034006019 27_make_luret 1.17)
(source/control.ml 4416 1030975996 c/4_control.ml 1.3)
(source/lurettetop.ml 24884 1033738731 c/1_lurettetop 1.12)
(ihm/xlurette/xlurette_glade_interface.ml 28245 1032531447 c/15_xlurette_g 1.3)
(source/lurettetop.ml 24884 1033738731 c/1_lurettetop 1.12)
(mlcuddidl/README 1574 1034006019 d/8_README 1.1)
(cuddaux/README 1427 1034006019 c/34_README 1.1)
(source/ne.mli 2376 1033723811 c/22_ne.mli 1.1)
(README 74 1011881677 10_README 1.2)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(source/env_state.ml 20707 1033125605 51_env_state. 1.29)
(mlcuddidl/manager_caml.c 39233 1034006019 c/45_manager_ca 1.1)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
(source/env.mli 2027 1033738731 15_env.mli 1.16)
(mlcuddidl/rdd_caml.c 41613 1034006019 c/39_rdd_caml.c 1.1)
(user-rules 13974 1034006019 c/14_myrules 1.9)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/gne.mli 1552 1033397911 b/36_gne.mli 1.4)
(myrules 10701 1033738731 c/14_myrules 1.8)
(bin/Makefile.lucky 2225 1033738731 b/41_Makefile.i 1.4)
(test/giro/giro.luc 2755 1033738731 c/6_giro.ima 1.4)
(source/show_env.mli 1091 1033738731 42_show_env.m 1.8)
(Makefile.lurette 698 1032940601 b/38_Makefile.l 1.11)
(Makefile.lurette 753 1034006019 b/38_Makefile.l 1.12)
(source/luc_exe.mli 447 1033738731 b/31_ima_exe.ml 1.2)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(mlcuddidl/bdd.idl 18233 1034006019 d/7_bdd.idl 1.1)
(source/constraint.ml 2418 1033732198 c/19_constraint 1.4)
(mlcuddidl/manager.idl 11024 1034006019 c/48_manager.id 1.1)
(test/vrai_tram.c 3060 1027066799 b/8_vrai_tram. 1.3)
(source/command_line.mli 1442 1031053030 b/21_command_li 1.7)
(demo/chaudiere/chaudiere.luc 446 1032789516 c/11_chaudiere. 1.5)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(ihm/xlurette/xlurette.glade 43485 1032531447 c/13_xlurette.g 1.4)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(demo/chaudiere/chaudiere.luc 446 1032789516 c/11_chaudiere. 1.5)
(mlcuddidl/bdd_caml.c 57199 1034006019 d/4_bdd_caml.c 1.1)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(cuddaux/Changes 42 1034006019 c/36_Changes 1.1)
(test/vrai_tram.h 2468 1027066799 b/7_vrai_tram. 1.3)
(test/tram.luc 1079 1032789516 b/15_tram.env 1.8)
(source/eval.mli 1395 1027066799 48_eval.mli 1.10)
(mlcuddidl/mtbdd.ml 10185 1034006019 c/44_mtbdd.ml 1.1)
(demo/chaudiere/chaudiere_ctrl.lus 177 1031732392 c/9_chaudiere_ 1.1)
(source/control.mli 3202 1030975671 c/3_control.ml 1.2)
(source/formula.ml 5765 1033397911 45_formula.ml 1.21)
(cuddaux/Makefile 3091 1034006019 c/35_Makefile 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(mlcuddidl/idd.idl 10595 1034006019 d/1_idd.idl 1.1)
(source/gne.ml 2767 1033397911 b/37_gne.ml 1.4)
(cuddaux/cuddaux.h 2381 1034006019 c/33_cuddaux.h 1.1)
(mlcuddidl/macros.m4 11290 1034006019 c/49_macros.m4 1.1)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(mlcuddidl/bdd.mli 8573 1034006019 d/5_bdd.mli 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/rnumsolver.ml 20636 1033732198 b/27_rnumsolver 1.13)
(mlcuddidl/cudd_caml.c 22890 1034006019 d/3_cudd_caml. 1.1)
(source/print.ml 5807 1033723811 47_print.ml 1.21)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(cuddaux/cuddauxBridge.c 6099 1034006019 c/31_cuddauxBri 1.1)
(source/show_env.ml 3603 1033738731 43_show_env.m 1.13)
(mlcuddidl/Changes 64 1034006019 d/10_Changes 1.1)
(cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1)
(source/rnumsolver.mli 2198 1033732198 b/26_rnumsolver 1.9)
(source/sim2chro.ml 2721 1033397911 b/24_sim2chro.m 1.14)
(source/command_line_luc_exe.ml 2794 1033738731 b/33_command_li 1.6)
(source/command_line_luc_exe.ml 2786 1034006019 b/33_command_li 1.7)
(mlcuddidl/cudd_caml.h 1210 1034006019 d/2_cudd_caml. 1.1)
(source/value.ml 2355 1033723811 c/23_value.ml 1.1)
(test/time.exp 5580 1033738731 b/48_time.exp 1.11)
(test/time.exp 5580 1034006019 b/48_time.exp 1.12)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(bin/Makefile.show_luc 1109 1033738731 b/40_Makefile.s 1.5)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(mlcuddidl/idd.mli 5470 1034006019 c/51_idd.mli 1.1)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
Makefile.lurette
View file @ 9f892d0a
#
# Makefile for lurette based on OcamlMakefile
#
LURETTE_PATH=/home/jahier/lurette
ifndef LURETTE_PATH
LURETTE_PATH := /home/jahier/lurette
endif
export LURETTE_PATH
OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile
OCAMLNCFLAGS = -inline 10 -noassert -unsafe
......@@ -10,7 +16,7 @@ ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe
endif
LIBS = str $(LURETTE_PATH)/bin/lurette_lib # mlpoly
LIBS = str $(LURETTE_PATH)/lib/lurette_lib # mlpoly
INCDIRS = /home/jahier/include
LIBDIRS = /home/jahier/lib
......
OcamlMakefile
View file @ 9f892d0a
......@@ -5,7 +5,7 @@
# For updates see:
# http://www.oefai.at/~markus/ocaml_sources
#
# $Id: OcamlMakefile 1.42 Mon, 30 Sep 2002 16:58:31 +0200 jahier $
# $Id: OcamlMakefile 1.43 Mon, 07 Oct 2002 17:53:39 +0200 jahier $
#
###########################################################################
......@@ -692,7 +692,7 @@ pdfdoc: doc/latex/doc.pdf
doc: htdoc ladoc psdoc pdfdoc
-include $(LURETTE_PATH)/myrules
-include $(LURETTE_PATH)/user-rules
###########################################################################
# LOW LEVEL RULES
......
cuddaux/Changes 0 → 100644
View file @ 9f892d0a
Cuddaux 0.9:
============
First release.
cuddaux/Makefile 0 → 100644
View file @ 9f892d0a
#=======================================
# Configuration Section
#=======================================
#---------------------------------------
# Directories
#---------------------------------------
SRCDIR = $(shell pwd)
#
#
#
# XXX autoconf
CUDD_INSTALL = /home/jahier
ifndef BIN_INSTALL_DIR
BIN_INSTALL_DIR := ../bin
endif
ifndef INC_INSTALL_DIR
INC_INSTALL_DIR := ../include
endif
ifndef LIB_INSTALL_DIR
LIB_INSTALL_DIR := ../lib
endif
#---------------------------------------
# C part
#---------------------------------------
CC = gcc
ICFLAGS = \
-I$(CUDD_INSTALL)/include \
-Winline -Wimplicit-function-declaration \
-Wall
#
# XCFLAGS should be the same than the one with which CUDD is compiled
#
XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100
CFLAGS = $(ICFLAGS) $(XCFLAGS) -O3 -DNDEBUG
CFLAGS_DEBUG = $(ICFLAGS) $(XCFLAGS) -O1 -g -UNDEBUG
CFLAGS_PROF = $(ICFLAGS) $(XCFLAGS) -O3 -DNDEBUG -g -pg
#=======================================
# End of Configuration Section
#=======================================
#---------------------------------------
# Files
#---------------------------------------
CCMODULES = \
cuddauxAddIte cuddauxBridge cuddauxCompose \
cuddauxGenCof cuddauxMisc cuddauxTDGenCof
CCSRC = cuddaux.h cuddauxInt.h $(CCMODULES:%=%.c)
CCLIB_TOINSTALL = libcuddaux.a libcuddaux_debug.a libcuddaux_prof.a
CCINC_TOINSTALL = cuddaux.h
#---------------------------------------
# Rules
#---------------------------------------
# Global rules
all: $(CCLIB_TOINSTALL)
debug: libcuddaux_debug.a
prof: libcuddaux_prof.a
install: all
cp -f $(CCLIB_TOINSTALL) $(LIB_INSTALL_DIR)
cp -f $(CCINC_TOINSTALL) $(INC_INSTALL_DIR)
distclean: mostlyclean
(cd $(LIB_INSTALL_DIR); /bin/rm -f $(CCLIB_TOINSTALL))
(cd $(INC_INSTALL_DIR); /bin/rm -f $(CCINC_TOINSTALL))
mostlyclean:
/bin/rm -f cuddaux.?? cuddaux.??? cuddaux.info
/bin/rm -fr html
clean:
/bin/rm -f *.[ao]
tar: $(CCSRC) Makefile README Changes cuddaux.texi texinfo.tex
(cd ..; tar zcvf $(HOME)/cuddaux.tgz $(^:%=cuddaux/%))
dist: $(CCSRC) Makefile README Changes cuddaux.texi texinfo.tex cuddaux.dvi cuddaux.info html
(cd ..; tar zcvf $(HOME)/cuddaux.tgz $(^:%=cuddaux/%))
# TEX rules
cuddaux.dvi: cuddaux.texi
texi2dvi $<
cuddaux.ps: cuddaux.dvi
dvips -o $@ $<
cuddaux.info: cuddaux.texi
makeinfo --no-split $<
cuddaux.html: cuddaux.texi
texi2html -split=chapter -nosec_nav -subdir=html $<
#--------------------------------------------------------------
# IMPLICIT RULES AND DEPENDENCIES
#--------------------------------------------------------------
.SUFFIXES: .c .h .o .a
#-----------------------------------
# C
#-----------------------------------
libcuddaux.a: $(CCMODULES:%=%.o)
ar rcs libcuddaux.a $^
libcuddaux_debug.a: $(CCMODULES:%=%_debug.o)
ar rcs $@ $^
libcuddaux_prof.a: $(CCMODULES:%=%_prof.o)
ar rcs $@ $^
%.o: %.c cuddaux.h
$(CC) $(CFLAGS) -c -o $@ $<
%_debug.o: %.c cuddaux.h
$(CC) $(CFLAGS_DEBUG) -c -o $@ $<
%_prof.o: %.c cuddaux.h
$(CC) $(CFLAGS_PROF) -c -o $@ $<
cuddaux/README 0 → 100644
View file @ 9f892d0a
* Files
The basic distribution contain the following files:
README
Makefile
Changes
cuddaux.h cuddauxInt.h
cuddauxAddIte.c cuddauxBridge.c cuddauxCompose.c
cuddauxGenCof.c cuddauxMisc.c cuddauxTDGenCof.c
* What's needed :
- An ANSI C compiler (gcc is the only tested compiler)
- GNU make
- The CUDD BDDs library (http://vlsi.colorado.edu/software.html)
* This code provides additional functions to the CUDD library. Many of
them allows to replace 0-1 ADDs by BDDs, some offers equivalent
functions for ADDs than the functions implemented for BDDs, others
offers a different interface, and last new functions are implemented.
* IMPORTANT REMARK: Some functions relies on the distinghuished
"background" ADD node of CUDD. This node can be modified by
Cudd_SetBackground(). However this last function doesn't empty the
cache, which can lead to erroneous results. So be cautious, call
Cudd_SetBackground() before using such functions, or otherwise call
the function Cudd_ReduceHeap(man,CUDD_REORDER_NONE)
to clear the cache.
* To build,
Inspect Makefile and set properly variables.
make all: build the bytecode version of the interface
make install: installs the two versions of the interface
* Documentation:
Available in DVI (cuddaux.dvi), INFO (cuddaux.info), and HTML (html/*)
formats
IMPORTANT REMARK: The C compilation flags (processor, alignement)
should be the same than those with which CUDD is compiled.
cuddaux/cuddaux.h 0 → 100644
View file @ 9f892d0a
/* $Id: cuddaux.h 1.1 Mon, 07 Oct 2002 17:53:39 +0200 jahier $ */
#ifndef __CUDDAUX_H__
#define __CUDDAUX_H__
#include "cudd.h"
struct list_t {
struct list_t* next;
DdNode* node;
};
typedef struct list_t list_t;
/* File cuddauxAddIte.c */
/* f is a BDD, g and h are ADDs */
DdNode* Cuddaux_addIte(DdManager* dd, DdNode* f, DdNode* g, DdNode* h);
DdNode* Cuddaux_addBddAnd(DdManager* dd, DdNode* f, DdNode* g);
DdNode* Cuddaux_addIteConstant(DdManager* dd, DdNode* f, DdNode* g, DdNode* h);
DdNode* Cuddaux_addEvalConst(DdManager* dd, DdNode* f, DdNode* g);
/* File cuddauxBridge.c */
/* f is an ADD */
DdNode* Cuddaux_addTransfer(DdManager* ddS, DdManager* ddD, DdNode* f);
/* File cuddauxGenCof.c */
/* f and c are BDDs */
DdNode* Cuddaux_bddRestrict(DdManager * dd, DdNode * f, DdNode * c);
/* f is an ADD, c a BDD */
DdNode* Cuddaux_addRestrict(DdManager * dd, DdNode * f, DdNode * c);
DdNode* Cuddaux_addConstrain(DdManager * dd, DdNode * f, DdNode * c);
/* File cuddauxTDGenCof.c */
/* f and c are BDDs */
DdNode* Cuddaux_bddTDRestrict(DdManager* dd, DdNode* f, DdNode* c);
DdNode* Cuddaux_bddTDConstrain(DdManager* dd, DdNode* f, DdNode* c);
/* f is an ADD, c a BDD */
DdNode* Cuddaux_addTDRestrict(DdManager* dd, DdNode* f, DdNode* c);
DdNode* Cuddaux_addTDConstrain(DdManager* dd, DdNode* f, DdNode* c);
/* inf and sup are BDDs */
DdNode* Cuddaux_bddTDSimplify(DdManager* dd, DdNode* inf, DdNode* sup);
/* phi,f,g are ADDs with the distinguished background value */
DdNode* Cuddaux_addTDSimplify(DdManager* dd, DdNode* phi);
/* File cuddauxCompose.c */
/* f is an ADD, g a BDD */
DdNode* Cuddaux_addCompose(DdManager* dd, DdNode* f, DdNode* g, int v);
DdNode* Cuddaux_addVarMap(DdManager* dd, DdNode* f);
int Cuddaux_SetVarMap(DdManager *manager, int* array);
/* f is an ADD, vector an array of BDDs */
DdNode* Cuddaux_addVectorCompose(DdManager* dd, DdNode* f, DdNode** vector);
/* File cuddauxMisc.c */
/* f is a BDD/ADD node and var a projection function */
int Cuddaux_IsVarIn(DdManager* dd, DdNode* f, DdNode* var);
/* f and g are BDD cubes */
DdNode* Cuddaux_bddCubeUnion(DdManager* dd, DdNode* f, DdNode* g);
/* f is a BDD/ADD node and level a level. */
list_t* Cuddaux_NodesBelowLevel(DdManager* dd, DdNode* f, int level);
void list_free(list_t* l);
/* f and h are ADDs */
DdNode* Cuddaux_addGuardOfNode(DdManager* dd, DdNode* f, DdNode* h);
#endif
cuddaux/cuddauxAddIte.c 0 → 100644
View file @ 9f892d0a
/* $Id: cuddauxAddIte.c 1.1 Mon, 07 Oct 2002 17:53:39 +0200 jahier $ */
/**CFile***********************************************************************
FileName [cuddauxAddIte.c]
PackageName [cuddaux]
Synopsis [ADD ITE function and satellites, taking BDDs as arguments (instead of a 0-1 ADD as in cuddAddIte.c)]
Description [External procedures included in this module:
<ul>
<li> Cuddaux_addIte()
<li> Cuddaux_addBddAnd()
<li> Cuddaux_addIteConstant()
<li> Cuddaux_addEvalConst()
</ul>
Internal procedures included in this module:
<ul>
<li> cuddauxAddIteRecur()
<li> cuddauxAddBddAndRecur()
</ul>
Static procedures included in this module:
<ul>
</ul>]
Author [Bertrand Jeannet]
Copyright []
******************************************************************************/
#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include <limits.h>
#include "cuddInt.h"
#include "util.h"
#include "st.h"
#include "cuddauxInt.h"
/*---------------------------------------------------------------------------*/
/* Definition of exported functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Implements ITE(f,g,h).]
Description [Implements ITE(f,g,h). This procedure assumes that f is
a BDD. Returns a pointer to the resulting ADD if successful; NULL
otherwise.]
SideEffects [None]
SeeAlso [Cudd_addIte Cudaux_addBddAnd]
******************************************************************************/
DdNode*
Cuddaux_addIte(
DdManager* dd,
DdNode* f,
DdNode* g,
DdNode* h)
{
DdNode *res;
do {
dd->reordered = 0;
res = cuddauxAddIteRecur(dd,f,g,h);
} while (dd->reordered == 1);
return(res);
} /* end of Cuddaux_addIte */
/**Function********************************************************************
Synopsis [Implements ITE(f,g,background).]
Description [Implements ITE(f,g,background). This procedure assumes that f is
a BDD. Returns a pointer to the resulting ADD if successful; NULL
otherwise.]
SideEffects [None]
SeeAlso [Cuddaux_addIte]
******************************************************************************/
DdNode *
Cuddaux_addBddAnd(
DdManager * dd,
DdNode * f,
DdNode * g)
{
DdNode *res;
do {
dd->reordered = 0;
res = cuddauxAddBddAndRecur(dd,f,g);
} while (dd->reordered == 1);
return(res);
} /* end of Cudd_addBddAnd */
/**Function********************************************************************
Synopsis [Implements ITEconstant for ADDs.]
Description [Implements ITEconstant for ADDs. f must be a BDD.
Returns a pointer to the resulting ADD (which may or may not be
constant) or DD_NON_CONSTANT. No new nodes are created. This function
can be used, for instance, to check that g has a constant value
(specified by h) whenever f is 1. If the constant value is unknown,
then one should use Cudd_addEvalConst.]
SideEffects [None]
SeeAlso [Cudd_addIteConstant]
******************************************************************************/
DdNode *
Cuddaux_addIteConstant(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h)
{
DdNode *one,*zero;
DdNode *Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*r,*t,*e;
unsigned int topf,topg,toph,top;
/* Trivial cases. */
one = DD_ONE(dd);
zero = Cudd_Not(one);
if (f == one) { /* ITE(1,G,H) = G */
return(g);
}
if (f == zero){ /* ITE(0,G,H) = H */
return(h);
}
/* Check remaining one variable cases. */
if (g == h) { /* ITE(F,G,G) = G */
return(g);
}
if (cuddIsConstant(g) && cuddIsConstant(h)) {
return(DD_NON_CONSTANT);
}
/* Put into canonical form */
if (Cudd_IsComplement(f)){
DdNode* t = g; g = h; h = t;
f = Cudd_Not(f);
}
topf = cuddI(dd,f->index);
topg = cuddI(dd,g->index);
toph = cuddI(dd,h->index);
top = ddMin(topg,toph);
/* ITE(F,G,H) = (x,G,H) (non constant) if F = (x,1,0), x < top(G,H). */
if (topf < top && cuddT(f) == one && cuddE(f) == zero) {
return(DD_NON_CONSTANT);
}
/* Check cache. */
r = cuddConstantLookup(dd,DDAUX_ADD_ITE_CONSTANT_TAG,f,g,h);
if (r != NULL) {
return(r);
}
/* Compute cofactors. */
top = ddMin(topf,top);
if (topf == top) {
Fv = cuddT(f); Fnv = cuddE(f);
} else {
Fv = Fnv = f;
}
if (topg == top) {
Gv = cuddT(g); Gnv = cuddE(g);
} else {
Gv = Gnv = g;
}
if (toph == top) {
Hv = cuddT(h); Hnv = cuddE(h);
} else {
Hv = Hnv = h;
}
/* Recursive step. */
t = Cuddaux_addIteConstant(dd,Fv,Gv,Hv);
if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
cuddCacheInsert(dd, DDAUX_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
return(DD_NON_CONSTANT);
}
e = Cuddaux_addIteConstant(dd,Fnv,Gnv,Hnv);
if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {