Commit 472c46b7 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Plug the lus2lic lib to ldbg and lurettetop. The "v6" rp port now uses lus2lic -exec

(and do not go via ec anymore).

Split the Failure module so that it can be shared with the lus2lic
ldbg plugin without requiring the bdd lib.

+ mv the lus2licRun.ml/mli file to the Lurette git repo.

+ add a copy (in read-only mode) of the source files of the lus2lic compiler

+ Share the comion content of Makefile.lurettetop and Makefile.ldbg via a new
Makefile.comon that is included in both.

+ Merge code of modules that are now shared with the lus2lic repo:
 -  Verbose, Data, Rif_base
parent 888c28a0
......@@ -212,3 +212,5 @@ examples/lutin/socket-from-ocaml/lutin
examples/lutin/adacs/
examples/lutin/alice/
examples/lutin/comon/
test_old/
source/debug/
......@@ -34,8 +34,6 @@ slink:
rm -rf lib && ln -sf pre_release/$(HOSTTYPE)/lib
rm -rf include && ln -sf pre_release/$(HOSTTYPE)/include
cp -rf $(LOCAL_INSTALL)/lib/* $(LIB_INSTALL_DIR)
cp -rf $(LUSTRE_INSTALL)/lib/tcl* $(LIB_INSTALL_DIR)
cp -rf $(LUSTRE_INSTALL)/lib/tk* $(LIB_INSTALL_DIR)
cp -rf $(LOCAL_INSTALL)/include/* $(INC_INSTALL_DIR)
cpcomp:
......@@ -77,10 +75,13 @@ ci:
dif:
git --no-pager diff --color-words
diff:
git diff HEAD -w > diff.diff
diff:dodiff
echo "il y a $(shell grep "+" diff.diff | wc -l) + et $(shell grep "-" diff.diff | wc -l) -"
dodiff:
git diff HEAD -w > diff.diff
# diff of the lastly commited change
cdiff:
git diff -w "HEAD^" HEAD > diff.diff
......
......@@ -290,12 +290,14 @@ LUTIN_SOURCES = \
$(OBJDIR)/util.ml \
$(OBJDIR)/data.ml \
$(OBJDIR)/data.mli \
$(OBJDIR)/expr.ml \
$(OBJDIR)/failure.mli \
$(OBJDIR)/exprUtil.mli \
$(OBJDIR)/expr.ml \
$(OBJDIR)/event.ml \
$(LURETTE_SOURCES_C) \
$(LURETTE_SOURCES) \
$(OBJDIR)/failure.ml \
$(OBJDIR)/exprUtil.ml \
$(OBJDIR)/expEval.mli \
$(OBJDIR)/expEval.ml \
$(OBJDIR)/verbose.ml \
......
......@@ -16,7 +16,7 @@ $(EXPDIR):
# several oracles
test1.rif: heater_control$(EXE) $(EXPDIR)
rm -f test1.rif0 .lurette_rc
$(LURETTETOP) -go --output test1.rif0 \
$(LURETTETOP) -go --output test1.rif0 \
-rp "sut:ec_exe:./heater_control.ec:" \
-rp "oracle:v6:heater_control.lus:not_a_sauna" \
-rp "oracle:v6:heater_control.lus:not_a_fridge" \
......@@ -46,7 +46,8 @@ test2.rif:
grep -v "The execution lasted"| sed -e "s/^M//" > test2.rif
test2:test2.rif $(EXPDIR)
rm -f test2.res diff -u -i $(EXPDIR)/test2.rif.exp test2.rif > test2.res || true
rm -f test2.res
diff -u -i $(EXPDIR)/test2.rif.exp test2.rif > test2.res || true
ifneq (,$(findstring $(HOSTTYPE),win32))
taskkill /F /IM ecexe.exe || true
endif
......@@ -99,7 +100,7 @@ test5.rif: heater_control$(EXE)
test5:test5.rif $(EXPDIR)/
rm -f test5.res
diff -u -i $(EXPDIR)/test4.rif.exp test5.rif > test5.res || true
diff -u -i $(EXPDIR)/test5.rif.exp test5.rif > test5.res || true
ifneq (,$(findstring $(HOSTTYPE),win32))
taskkill /F /IM heater_control.exe || true
endif
......@@ -118,6 +119,9 @@ utest2:test2.rif
utest4:test4.rif
cp test4.rif $(EXPDIR)/test4.rif.exp
utest5:test5.rif
cp test5.rif $(EXPDIR)/test5.rif.exp
# nb : pas de utest5 car je me sert du test4 pour vérifier que je genere bien la meme
# trace en mode ldbg !!
......
......@@ -5,6 +5,7 @@ open Ldbg_utils;;
ltop "set_seed 3";;
add_rp "env:lutin:env.lut:-m:main1";;
add_rp "env:lutin:env.lut:-m:main2";;
(* add_rp "sut:v6:heater_control.lus:heater_control";; *)
add_rp "sut:ec_exe:./heater_control.ec:";;
ltop "set_rif \"test5.rif0\"";;
......
#
# Makefile for lurettetop, a top-level loop/MUI to use lurette.
#
include $(LURETTE_PATH)/Makefile.common.source
include $(LURETTE_PATH)/source/Makefile.ln
OCAMLFLAGS += -I $(OBJDIR) -I $(OCAMLLIB) -I $(PREFIX)/$(HOSTTYPE)/lib
#-I ~/dd/ocamlnat/_build/src/toplevel/
IDLFLAGS=-nocpp
POLKA=polkag
ifdef STATIC
OCAMLLDFLAGS = -cclib -lstdc++ -cclib -lm -cclib -lc -ccopt -static\
-cclib -l$(POLKA)_caml -cclib -l$(POLKA) -cclib -lgmp $(OCAMLOPTFLAG)
else
OCAMLLDFLAGS= -cclib -lstdc++ -cclib -I/usr/lib/w32api \
-cclib -l$(POLKA)_caml \
-cclib -l$(POLKA) -cclib -lgmp $(OCAMLOPTFLAG)
# -cclib ~/dd/ocamlnat/_build/src/libocamlnat.a
endif
CC= $(GCC) $(DWIN32)
LIBS = unix dynlink str nums polka bdd
CLIBS = camlidl $(CLIBS_WIN32) bdd_stubs
#USE_CAMLP4 = yes
ZELANG=lut
USE_CAMLP4 = yes
SOC_SOURCES = \
$(OBJDIR)/soc.ml \
$(OBJDIR)/socUtils.mli \
$(OBJDIR)/socUtils.ml \
$(OBJDIR)/socPredef.mli \
$(OBJDIR)/socPredef.ml \
$(OBJDIR)/toposort.mli \
$(OBJDIR)/toposort.ml \
$(OBJDIR)/actionsDeps.mli \
$(OBJDIR)/actionsDeps.ml \
$(OBJDIR)/lic2soc.mli \
$(OBJDIR)/lic2soc.ml \
$(OBJDIR)/socExecValue.mli \
$(OBJDIR)/socExecValue.ml \
$(OBJDIR)/socExecEvalPredef.mli \
$(OBJDIR)/socExecEvalPredef.ml \
$(OBJDIR)/socExec.mli \
$(OBJDIR)/socExec.ml
LUSTRE_SOURCES = \
$(OBJDIR)/lv6version.ml \
$(OBJDIR)/lv6util.ml \
$(OBJDIR)/lv6MainArgs.ml \
$(OBJDIR)/lv6MainArgs.mli \
$(OBJDIR)/filenameExtras.mli \
$(OBJDIR)/filenameExtras.ml \
$(OBJDIR)/ident.mli \
$(OBJDIR)/ident.ml \
$(OBJDIR)/lxm.mli \
$(OBJDIR)/lxm.ml \
$(OBJDIR)/lv6errors.ml \
$(OBJDIR)/astPredef.ml \
$(OBJDIR)/astCore.ml \
$(OBJDIR)/astV6.ml \
$(OBJDIR)/astV6Dump.mli \
$(OBJDIR)/astV6Dump.ml \
$(OBJDIR)/astRecognizePredef.mli \
$(OBJDIR)/astRecognizePredef.ml \
$(OBJDIR)/lv6parserUtils.ml \
$(OBJDIR)/lv6parser.mly \
$(OBJDIR)/lv6lexer.mll \
$(OBJDIR)/astInstanciateModel.mli \
$(OBJDIR)/astInstanciateModel.ml \
$(OBJDIR)/astTabSymbol.mli \
$(OBJDIR)/astTabSymbol.ml \
$(OBJDIR)/astTab.mli \
$(OBJDIR)/astTab.ml \
$(OBJDIR)/lic.ml \
$(OBJDIR)/idSolver.ml \
$(OBJDIR)/licName.mli \
$(OBJDIR)/licName.ml \
$(OBJDIR)/licDump.ml \
$(OBJDIR)/licPrg.mli \
$(OBJDIR)/licPrg.ml \
$(SOC_SOURCES) \
$(OBJDIR)/unifyType.mli \
$(OBJDIR)/unifyType.ml \
$(OBJDIR)/unifyClock.mli \
$(OBJDIR)/unifyClock.ml \
$(OBJDIR)/licEvalType.mli \
$(OBJDIR)/licEvalType.ml \
$(OBJDIR)/licEvalConst.mli \
$(OBJDIR)/licEvalConst.ml \
$(OBJDIR)/licEvalClock.mli \
$(OBJDIR)/licEvalClock.ml \
$(OBJDIR)/evalConst.mli \
$(OBJDIR)/evalConst.ml \
$(OBJDIR)/evalType.mli \
$(OBJDIR)/evalType.ml \
$(OBJDIR)/evalClock.mli \
$(OBJDIR)/evalClock.ml \
$(OBJDIR)/licMetaOp.mli \
$(OBJDIR)/licMetaOp.ml \
$(OBJDIR)/ast2lic.mli \
$(OBJDIR)/ast2lic.ml \
$(OBJDIR)/misc.ml \
$(OBJDIR)/l2lCheckLoops.mli \
$(OBJDIR)/l2lCheckLoops.ml \
$(OBJDIR)/l2lCheckOutputs.mli \
$(OBJDIR)/l2lCheckOutputs.ml \
$(OBJDIR)/l2lExpandArrays.mli \
$(OBJDIR)/l2lExpandArrays.ml \
$(OBJDIR)/l2lExpandNodes.mli \
$(OBJDIR)/l2lExpandNodes.ml \
$(OBJDIR)/l2lExpandMetaOp.ml \
$(OBJDIR)/l2lExpandMetaOp.mli \
$(OBJDIR)/l2lRmPoly.mli \
$(OBJDIR)/l2lRmPoly.ml \
$(OBJDIR)/l2lAliasType.mli \
$(OBJDIR)/l2lAliasType.ml \
$(OBJDIR)/l2lSplit.mli \
$(OBJDIR)/l2lSplit.ml \
$(OBJDIR)/licTab.ml \
$(OBJDIR)/licTab.mli \
$(OBJDIR)/compile.mli \
$(OBJDIR)/compile.ml \
LTOP_SOURCES = \
$(LUTIN_SOURCES) \
$(LUSTRE_SOURCES) \
$(OBJDIR)/ltopArg.ml \
$(OBJDIR)/lus2licRun.mli \
$(OBJDIR)/lus2licRun.ml \
$(OBJDIR)/lutinRun.mli \
$(OBJDIR)/lutinRun.ml \
$(OBJDIR)/ocamlRM.mli \
$(OBJDIR)/ocamlRM.ml \
$(OBJDIR)/ocamlRun.mli \
$(OBJDIR)/ocamlRun.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
$(OBJDIR)/ocaml.mli \
$(OBJDIR)/ocaml.ml \
$(OBJDIR)/extTools.mli \
$(OBJDIR)/extTools.ml \
$(OBJDIR)/build.mli \
$(OBJDIR)/build.ml \
$(OBJDIR)/runBin.mli \
$(OBJDIR)/runBin.ml \
$(OBJDIR)/runDirect.mli \
$(OBJDIR)/runDirect.ml \
$(OBJDIR)/runPipe.mli \
$(OBJDIR)/runPipe.ml \
$(OBJDIR)/run.mli \
$(OBJDIR)/run.ml \
$(OBJDIR)/cmd.mli \
$(OBJDIR)/cmd.ml \
#
# Makefile for lurettetop, a top-level loop/MUI to use lurette.
#
include $(LURETTE_PATH)/Makefile.common.source
include $(LURETTE_PATH)/source/Makefile.ln
OCAMLFLAGS += -I $(OBJDIR) -I $(OCAMLLIB) -I $(PREFIX)/$(HOSTTYPE)/lib
#-I ~/dd/ocamlnat/_build/src/toplevel/
IDLFLAGS=-nocpp
POLKA=polkag
ifdef STATIC
OCAMLLDFLAGS = -cclib -lstdc++ -cclib -lm -cclib -lc -ccopt -static\
-cclib -l$(POLKA)_caml -cclib -l$(POLKA) -cclib -lgmp $(OCAMLOPTFLAG)
else
OCAMLLDFLAGS= -cclib -lstdc++ -cclib -I/usr/lib/w32api \
-cclib -l$(POLKA)_caml \
-cclib -l$(POLKA) -cclib -lgmp $(OCAMLOPTFLAG)
# -cclib ~/dd/ocamlnat/_build/src/libocamlnat.a
endif
CC= $(GCC) $(DWIN32)
LIBS = unix dynlink str nums polka bdd
CLIBS = camlidl $(CLIBS_WIN32) bdd_stubs
#USE_CAMLP4 = yes
ZELANG=lut
USE_CAMLP4 = yes
include $(LURETTE_PATH)/source/Lurettetop/Makefile.comon
SOURCES = \
$(LUTIN_SOURCES) \
$(OBJDIR)/ltopArg.ml \
$(OBJDIR)/lutinRun.mli \
$(OBJDIR)/lutinRun.ml \
$(OBJDIR)/ocamlRM.mli \
$(OBJDIR)/ocamlRM.ml \
$(OBJDIR)/ocamlRun.mli \
$(OBJDIR)/ocamlRun.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
$(OBJDIR)/ocaml.mli \
$(OBJDIR)/ocaml.ml \
$(OBJDIR)/extTools.mli \
$(OBJDIR)/extTools.ml \
$(OBJDIR)/build.mli \
$(OBJDIR)/build.ml \
$(OBJDIR)/runBin.mli \
$(OBJDIR)/runBin.ml \
$(OBJDIR)/runDirect.mli \
$(OBJDIR)/runDirect.ml \
$(OBJDIR)/runPipe.mli \
$(OBJDIR)/runPipe.ml \
$(OBJDIR)/run.mli \
$(OBJDIR)/run.ml \
$(OBJDIR)/cmd.mli \
$(OBJDIR)/cmd.ml \
$(LTOP_SOURCES) \
$(OBJDIR)/ldbg.mli \
$(OBJDIR)/ldbg.ml \
$(OBJDIR)/ldbg_utils.mli \
......
#
# Makefile for lurettetop, a top-level loop/MUI to use lurette.
#
include $(LURETTE_PATH)/Makefile.common.source
include $(LURETTE_PATH)/source/Makefile.ln
OCAMLFLAGS += -I $(OBJDIR) -I $(OCAMLLIB) -I $(PREFIX)/$(HOSTTYPE)/lib
IDLFLAGS=-nocpp
POLKA=polkag
ifdef STATIC
OCAMLLDFLAGS = -cclib -lstdc++ -cclib -lm -cclib -lc -ccopt -static\
-cclib -l$(POLKA)_caml -cclib -l$(POLKA) -cclib -lgmp $(OCAMLOPTFLAG)
else
OCAMLLDFLAGS= -cclib -lstdc++ -cclib -I/usr/lib/w32api \
-cclib -l$(POLKA)_caml \
-cclib -l$(POLKA) -cclib -lgmp $(OCAMLOPTFLAG)
endif
CC= $(GCC) $(DWIN32)
LIBS = unix dynlink str nums polka bdd
CLIBS = camlidl $(CLIBS_WIN32) bdd_stubs
#USE_CAMLP4 = yes
ZELANG=lut
USE_CAMLP4 = yes
include $(LURETTE_PATH)/source/Lurettetop/Makefile.comon
SOURCES = \
$(LUTIN_SOURCES) \
$(OBJDIR)/ltopArg.ml \
$(OBJDIR)/lutinRun.mli \
$(OBJDIR)/lutinRun.ml \
$(OBJDIR)/ocamlRM.mli \
$(OBJDIR)/ocamlRM.ml \
$(OBJDIR)/ocamlRun.mli \
$(OBJDIR)/ocamlRun.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
$(OBJDIR)/ocaml.mli \
$(OBJDIR)/ocaml.ml \
$(OBJDIR)/extTools.mli \
$(OBJDIR)/extTools.ml \
$(OBJDIR)/build.mli \
$(OBJDIR)/build.ml \
$(OBJDIR)/runBin.mli \
$(OBJDIR)/runBin.ml \
$(OBJDIR)/runDirect.mli \
$(OBJDIR)/runDirect.ml \
$(OBJDIR)/runPipe.mli \
$(OBJDIR)/runPipe.ml \
$(OBJDIR)/run.mli \
$(OBJDIR)/run.ml \
$(OBJDIR)/cmd.mli \
$(OBJDIR)/cmd.ml \
$(LTOP_SOURCES) \
$(OBJDIR)/lurettetop.ml
RESULT = ./lurettetop_exe$(EXE)
......
open Expr
open Constraint
let (index_to_exp : int -> Expr.t * bool) =
fun i ->
let aux ne =
[Ne.to_expr ne; if Ne.is_int ne then Ival (Num.Int 0) else Fval 0.0]
in
match Formula_to_bdd.index_to_linear_constraint i with
| Bv(v) -> Var (Var.name v), false
| EqZ(ne) -> Op (Eq, aux ne), true
| Ineq(GZ(ne)) -> Op (Sup, aux ne), true
| Ineq(GeqZ(ne)) -> Op (SupEq, aux ne), true
let impl a b = not a || b
let (collect : bool -> Bdd.t -> Expr.t) =
fun num bdd ->
(* Collect the set of paths leading to true. If the [num] flag is
true, collect only the numeric constraints. *)
let rec (aux: Bdd.t -> Expr.t list list) =
(* collect the disjunction of conjunction as a list of list *)
fun bdd ->
assert(not(Bdd.is_true bdd));
assert(not(Bdd.is_false bdd));
let t,e = Bdd.dthen bdd, Bdd.delse bdd in
let v,is_num = index_to_exp (Bdd.topvar bdd) in
let not_v = Op(Not,[v]) in
let res_t =
if (Bdd.is_true t) then (if (impl num is_num) then [[v]] else []) else
if (Bdd.is_false t) then [] else
List.map (fun x -> (if (impl num is_num) then v::x else x)) (aux t)
in
let res_e =
if (Bdd.is_true e) then (if (impl num is_num) then [[not_v]] else []) else
if (Bdd.is_false e) then [] else
List.map (fun x -> (if (impl num is_num) then not_v::x else x)) (aux e)
in
List.rev_append res_e res_t
in
let res =
match aux bdd with
| [] -> assert false
| [[e]] -> e
| [l] -> Op(And, l)
| ll -> Op(Or, List.map (fun l -> Op(And, l)) ll)
in
Expr.simplify res
(* substracting list *)
let lminus l1 l2 = List.filter (fun x -> not (List.mem x l2)) l1
(* exported *)
let (get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Failure.info) =
fun bdd bdd1 (expr2,bdd2) ->
assert (not(Bdd.is_false bdd1));
let is_sat = not (Bdd.is_false bdd) in
if is_sat then
Failure.Numeric (collect true bdd)
else if Bdd.is_false bdd2 then
Failure.Boolean expr2
else
(* try to simplify the formula associated to bdd by projet *)
let s1 = Bdd.list_of_support (Bdd.support bdd1)
and s2 = Bdd.list_of_support (Bdd.support bdd2) in
let non_contributing_var = List.rev_append (lminus s1 s2)(lminus s2 s1) in
let non_contributing_var = Bdd.support_of_list non_contributing_var in
let bdd1 = Bdd.exist_local non_contributing_var bdd1
and bdd2 = Bdd.exist_local non_contributing_var bdd2 in
assert (not(Bdd.is_false bdd1));
assert (not(Bdd.is_false bdd2));
assert (Bdd.is_false (Bdd.dand bdd1 bdd2));
Failure.Boolean (Expr.Op(Expr.And, [collect false bdd1; collect false bdd2]))
(* Try to explain why a constraint is not satisfiable. It can be due
to:
- a pure Boolean reason, in which case we provide a (minimal)
expression representing the list of monomes that makes it false);
- Or there do exist Boolean solution, but there do not hold to
satisfiable numeric constraint, in which case we provide an
expression representing the list of monomes that makes its true *)
(* [get_info bdd bdd1 (bdd2,e2)] tries to explain as concisely as
possible why bdd is false
hyp: bdd=bdd1^bdd2=false ; bdd2=to_bdd(e2).
*)
val get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Failure.info
......@@ -6,78 +6,3 @@ type info =
| Boolean of Expr.t
| Numeric of Expr.t
open Expr
open Constraint
let (index_to_exp : int -> Expr.t * bool) =
fun i ->
let aux ne =
[Ne.to_expr ne; if Ne.is_int ne then Ival (Num.Int 0) else Fval 0.0]
in
match Formula_to_bdd.index_to_linear_constraint i with
| Bv(v) -> Var (Var.name v), false
| EqZ(ne) -> Op (Eq, aux ne), true
| Ineq(GZ(ne)) -> Op (Sup, aux ne), true
| Ineq(GeqZ(ne)) -> Op (SupEq, aux ne), true
let impl a b = not a || b
let (collect : bool -> Bdd.t -> Expr.t) =
fun num bdd ->
(* Collect the set of paths leading to true. If the [num] flag is
true, collect only the numeric constraints. *)
let rec (aux: Bdd.t -> Expr.t list list) =
(* collect the disjunction of conjunction as a list of list *)
fun bdd ->
assert(not(Bdd.is_true bdd));
assert(not(Bdd.is_false bdd));
let t,e = Bdd.dthen bdd, Bdd.delse bdd in
let v,is_num = index_to_exp (Bdd.topvar bdd) in
let not_v = Op(Not,[v]) in
let res_t =
if (Bdd.is_true t) then (if (impl num is_num) then [[v]] else []) else
if (Bdd.is_false t) then [] else
List.map (fun x -> (if (impl num is_num) then v::x else x)) (aux t)
in
let res_e =
if (Bdd.is_true e) then (if (impl num is_num) then [[not_v]] else []) else
if (Bdd.is_false e) then [] else
List.map (fun x -> (if (impl num is_num) then not_v::x else x)) (aux e)
in
List.rev_append res_e res_t
in
let res =
match aux bdd with
| [] -> assert false
| [[e]] -> e
| [l] -> Op(And, l)
| ll -> Op(Or, List.map (fun l -> Op(And, l)) ll)
in
Expr.simplify res
(* substracting list *)
let lminus l1 l2 = List.filter (fun x -> not (List.mem x l2)) l1
(* exported *)
let (get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> info) =
fun bdd bdd1 (expr2,bdd2) ->
assert (not(Bdd.is_false bdd1));
let is_sat = not (Bdd.is_false bdd) in
if is_sat then
Numeric (collect true bdd)
else if Bdd.is_false bdd2 then
Boolean expr2
else
(* try to simplify the formula associated to bdd by projet *)
let s1 = Bdd.list_of_support (Bdd.support bdd1)
and s2 = Bdd.list_of_support (Bdd.support bdd2) in
let non_contributing_var = List.rev_append (lminus s1 s2)(lminus s2 s1) in
let non_contributing_var = Bdd.support_of_list non_contributing_var in
let bdd1 = Bdd.exist_local non_contributing_var bdd1
and bdd2 = Bdd.exist_local non_contributing_var bdd2 in
assert (not(Bdd.is_false bdd1));
assert (not(Bdd.is_false bdd2));
assert (Bdd.is_false (Bdd.dand bdd1 bdd2));
Boolean (Expr.Op(Expr.And, [collect false bdd1; collect false bdd2]))
......@@ -8,24 +8,6 @@
** Main author: jahier@imag.fr
*)
type info =
| Boolean of Expr.t
| Numeric of Expr.t
(* Try to explain why a constraint is not satisfiable. It can be due
to:
- a pure Boolean reason, in which case we provide a (minimal)
expression representing the list of monomes that makes it false);
- Or there do exist Boolean solution, but there do not hold to
satisfiable numeric constraint, in which case we provide an
expression representing the list of monomes that makes its true *)
(* [get_info bdd bdd1 (bdd2,e2)] tries to explain as concisely as
possible why bdd is false
hyp: bdd=bdd1^bdd2=false ; bdd2=to_bdd(e2).
*)
val get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> info
......@@ -35,19 +35,21 @@ let on () = LtopArg.args.LtopArg.ldbg <- true
let _ =
LtopArg.args.LtopArg.ldbg <- true
(* Which one should I use??? *)
let my_string_of_float = string_of_float
let my_string_of_float = Util.my_string_of_float