Commit 8e032dba authored by Erwan Jahier's avatar Erwan Jahier
Browse files

minor changes

parent b475dfba
......@@ -37,7 +37,7 @@ INC_INSTALL_DIR = $(PRE_RELEASE_DIR)/include
CPP=cpp
GCC=gcc
GPP=g++
CFLAGS=-g -O2 -fpic -DPOLKA_NUM=3
CFLAGS=-g -O2 -fpic -DPOLKA_NUM=3
# HOSTTYPE doit etre defini bien sur...
......@@ -184,8 +184,6 @@ else
CAML_INSTALL_DIR=`$(OCAMLC) -where`
CC=gcc -g -O2 -fpic
OCAMLFLAGS =
OCAMLNCFLAGS =
......
......@@ -8,6 +8,7 @@ SRCDIR=.
OBJDIR=./obj
MAIN=foo
MAIN2=bool_utils_au_plus_2_parmi_3
#settings for Linux (and other posix systems ?)
......@@ -36,6 +37,7 @@ ifeq ($(HOSTTYPE),cygwin)
LD=gcc -DWIN32
CC=gcc -DWIN32
MKDLLFLAGS=-Wl,--out-implib,$(OBJDIR)/$(MAIN).a
MKDLL2FLAGS=-Wl,--out-implib,$(OBJDIR)/$(MAIN2).a
LFLAGS=-lm
LD_ARCH=-DWIN32
endif
......@@ -47,7 +49,7 @@ ifeq ($(HOSTTYPE),mac)
LD_ARCH=-DMAC
endif
all: $(OBJDIR)/$(MAIN).$(DLEXT)
all: $(OBJDIR)/$(MAIN).$(DLEXT) $(OBJDIR)/$(MAIN2).$(DLEXT)
$(OBJDIR):
mkdir $(OBJDIR)
......@@ -57,9 +59,20 @@ $(OBJDIR)/$(MAIN).$(DLEXT) : $(OBJDIR)/$(MAIN).o
$(OBJDIR)/$(MAIN).o \
$(MKDLLFLAGS)
$(OBJDIR)/$(MAIN2).$(DLEXT) : $(OBJDIR)/$(MAIN2).o
$(LD) $(LFLAGS) $(SOFLAGS) -o $(OBJDIR)/$(MAIN2).$(DLEXT) \
$(OBJDIR)/$(MAIN2).o \
$(MKDLLFLAGS2)
$(OBJDIR)/%.o : $(OBJDIR) $(SRCDIR)/%.c
$(CC) -c $(CFLAGS) $(SRCDIR)/$*.c -o $(OBJDIR)/$*.o
$(OBJDIR)/bool_utils_au_plus_2_parmi_3.ec : $(SRCDIR)/bool-utils.lus
lus2lic -ec $< -n bool_utils_au_plus_2_parmi_3 -o $@
$(OBJDIR)/bool_utils_au_plus_2_parmi_3.c : $(OBJDIR)/bool_utils_au_plus_2_parmi_3.ec
cd $(OBJDIR) ; ec2c ../$<
run: $(OBJDIR)/$(MAIN).$(DLEXT)
......@@ -80,7 +93,15 @@ test2:
cat test2.res
[ ! -s test2.res ] && make clean
test: test1 test2
test3: $(OBJDIR) $(OBJDIR)/$(MAIN2).$(DLEXT)
echo "1.0 1.0" | ../../../bin/lutin$(EXE) -l 1 -L $(OBJDIR)/$(MAIN2).$(DLEXT) call_lustre.lut \
-seed 1 | grep -v " Version" > test3.rif
rm -f test3.res && diff -u -i -B test3.rif.exp test3.rif > test3.res || true
cat test3.res
[ ! -s test3.res ] && make clean
test: test1 test2
utest1:
......@@ -88,6 +109,9 @@ utest1:
utest2:
cp test2.rif test2.rif.exp
utest3:
cp test3.rif test3.rif.exp
utest: utest1 utest2
clean:
......
......@@ -19,6 +19,17 @@ clean:
test: trace_ivrogne.cmxs
rm -f test.rif0 .lurette_rc
$(NEW_LURETTETOP) -go -v 1 --output test.rif0 -seed 3306566 \
-rp "sut:ocaml:trace_ivrogne.cmxs:" \
-rp 'env:lutin:ivrogne.lut:-main:ivrogne:-L:libm.so:-loc' && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "lurette Version" | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
test2: trace_ivrogne.cmxs
rm -f test.rif0 .lurette_rc
$(NEW_LURETTETOP) -go -v 1 --output test.rif0 -seed 3306566 \
-rp "sut:ocaml:trace_ivrogne.cmxs:" \
......
......@@ -68,7 +68,7 @@ let cross_product(ux,uy,vx,vy) = (ux*.vy-.uy*.vx);;
let image = ref (Graphics.get_image 0 0 (Graphics.size_x ()) (Graphics.size_y ()))
let foi = float_of_int
let cross_product(ux,uy,vx,vy) = (ux*.vy-.uy*.vx)
let is_inside(px,py,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y) =
......@@ -88,10 +88,10 @@ let is_inside(px,py,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y) =
let p4p3_y = p3y-.p4y in
let p3p2_x = p2x-.p3x in
let p3p2_y = p2y-.p3y in
cross_product(p2p1_x, p2p1_y, p2p_x, p2p_y) < 0.0 &&
cross_product(p1p4_x, p1p4_y, p1p_x, p1p_y) < 0.0 &&
cross_product(p4p3_x, p4p3_y, p4p_x, p4p_y) < 0.0 &&
cross_product(p3p2_x, p3p2_y, p3p_x, p3p_y) < 0.0
cross_product(p2p1_x, p2p1_y, p2p_x, p2p_y) > 0.0 &&
cross_product(p1p4_x, p1p4_y, p1p_x, p1p_y) > 0.0 &&
cross_product(p4p3_x, p4p3_y, p4p_x, p4p_y) > 0.0 &&
cross_product(p3p2_x, p3p2_y, p3p_x, p3p_y) > 0.0
let (step : Data.subst list -> Data.subst list)=
fun drunk_outs ->
......@@ -117,16 +117,34 @@ let (step : Data.subst list -> Data.subst list)=
and p4 = truncate p4
in
let max_x, max_y = (Graphics.size_x ()), (Graphics.size_y ()) in
let pc p maxi = p * maxi / 100 in
let point_list = [(pc p1 max_x, max_y);(max_x,pc p2 max_y);
(pc p3 max_x, 0);(0, pc p4 max_y)] in
let pc p maxi = (p * maxi) / 100 in
let [(p1x, p1y);
(p2x, p2y);
(p3x, p3y);
(p4x, p4y);
] = [(pc p1 max_x, max_y);(max_x,pc p2 max_y);
(pc p3 max_x, 0);(0, pc p4 max_y)]
in
let point_list = [(p1x, p1y);
(p2x, p2y);
(p3x, p3y);
(p4x, p4y);
]
in
let poly = Array.of_list point_list in
Graphics.draw_image !image 0 0;
draw x y;
image := Graphics.get_image 0 0 max_x max_y;
Graphics.set_color (Graphics.rgb 0 0 0);
Graphics.draw_poly poly;
if
(is_inside(x,y,foi p1x,foi p1y,foi p2x,foi p2y,foi p3x,foi p3y,foi p4x,foi p4y))
then
(print_string "inside!\n"; flush stdout)
else
(print_string "outside!\n"; flush stdout);
bounds
let _ =
......
......@@ -9,7 +9,7 @@
#CAMLIDL_INSTALL = $(HOME)/$(HOSTTYPE)
#GMP_INSTALL=$(HOME)/$(HOSTTYPE)
# include $(LURETTE_PATH)/Makefile.common.source
#include ../Makefile.common.source
OCAML_BINDIR=$(shell dirname $(OCAMLC))
......@@ -37,7 +37,7 @@ ifeq ($(HOST_TYPE),cross-win32)
GMP_INSTALL=$(LURETTE_PATH)/working/$(HOSTTYPE)
else
CC = gcc
GMP_INSTALL=$(LURETTE_PATH)/$(HOSTTYPE)
GMP_INSTALL=/usr
endif
endif
endif
......@@ -66,8 +66,8 @@ GMP_PREFIX = $(GMP_INSTALL)
CAML_PREFIX = $(CAML_INSTALL)
CAMLIDL_PREFIX = $(CAMLIDL_INSTALL)
CAML_PREFIX = `ocamlc -where`
CAMLIDL_PREFIX = `ocamlc -where`
CAML_PREFIX = `$(OCAMLC) -where`
CAMLIDL_PREFIX = `$(OCAMLC) -where`
#---------------------------------------
# Programs
......@@ -102,12 +102,21 @@ DVIPS = dvips
# Use ICFLAGS to specify machine-independent compilation flags.
ICFLAGS = -I$(GMP_PREFIX)/include -I.. -I$(CAML_PREFIX)\
ICFLAGS = -I$(GMP_PREFIX)/include -I.. -I$(CAML_PREFIX) \
-Wall -Wconversion -Winline -Wimplicit-function-declaration \
-Wswitch -Werror-implicit-function-declaration \
-Wextra -Wundef -Wbad-function-cast -Wstrict-prototypes \
-Wno-unused \
-O3 -g -DNDEBUG
# ICFLAGS = -I$(GMP_PREFIX)/include -I.. \
# -Wswitch -Werror-implicit-function-declaration \
# -Wall -Wextra -Wundef -Wbad-function-cast -Wstrict-prototypes \
# -Wno-unused \
# -std=c99 \
# -O0 -g -UNDEBUG
## xds-O3 -g -DNDEBUG
......
......@@ -57,10 +57,21 @@ runl: polkarunl
rung: polkarung
polkatopg: polka.cma libpolkag_caml_debug.a ../C/libpolkag.a
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
polkatopi: polka.cma libpolkai_caml_debug.a ../C/libpolkai.a
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
polkatopl: polka.cma libpolkal_caml_debug.a ../C/libpolkal.a
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
polkatop%: polka.cma libpolka%_caml_debug.a ../C/libpolka%_debug.a
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom $^ -cclib "-L$(CAMLIDL_PREFIX)/lib/ocaml -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
polkarun%: polka.cma libpolka%_caml.a ../C/libpolka%.a
$(OCAMLC) $(MLFLAGS) -o $@ -make-runtime $^ -cclib "-L$(CAMLIDL_PREFIX)/lib/ocaml -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
$(OCAMLC) $(MLFLAGS) -o $@ -make-runtime $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
install: $(CCINC_TO_INSTALL) $(MLLIB_TO_INSTALL) $(INSTALL) mk_incl_dirs $(LIBDIR) $(BINDIR)
......@@ -137,23 +148,23 @@ libpolkag_caml_prof.a: $(CCFILES_CAML:%=%g_caml_prof.o)
ar rcs $@ $^
%i_caml.o: %_caml.c
$(CC) $(ICFLAGS) $(XCFLAGS) -DPOLKA_NUM=1 -I../C -I$(CAML_PREFIX)/lib/ocaml -I$(CAMLIDL_PREFIX)/lib/ocaml -c -o $@ $<
$(CC) $(ICFLAGS) $(XCFLAGS) -DPOLKA_NUM=1 -I../C -I$(CAML_PREFIX) -I$(CAMLIDL_PREFIX) -c -o $@ $<
%l_caml.o: %_caml.c
$(CC) $(ICFLAGS) $(XCFLAGS) -DPOLKA_NUM=2 -I../C -I$(CAML_PREFIX)/lib/ocaml -I$(CAMLIDL_PREFIX)/lib/ocaml -c -o $@ $<
$(CC) $(ICFLAGS) $(XCFLAGS) -DPOLKA_NUM=2 -I../C -I$(CAML_PREFIX) -I$(CAMLIDL_PREFIX) -c -o $@ $<
%g_caml.o: %_caml.c
$(CC) $(ICFLAGS) $(XCFLAGS) -DPOLKA_NUM=3 -I$(GMP_PREFIX)/include -I../C -I$(CAML_PREFIX)/lib/ocaml -I$(CAMLIDL_PREFIX)/lib/ocaml -c -o $@ $<
$(CC) $(ICFLAGS) $(XCFLAGS) -DPOLKA_NUM=3 -I$(GMP_PREFIX)/include -I../C -I$(CAML_PREFIX) -I$(CAMLIDL_PREFIX) -c -o $@ $<
%i_caml_debug.o: %_caml.c
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_DEBUG) -DPOLKA_NUM=1 -I../C -I$(CAML_PREFIX)/lib/ocaml -I$(CAMLIDL_PREFIX)/lib/ocaml -c -o $@ $<
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_DEBUG) -DPOLKA_NUM=1 -I../C -I$(CAML_PREFIX) -I$(CAMLIDL_PREFIX) -c -o $@ $<
%l_caml_debug.o: %_caml.c
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_DEBUG) -DPOLKA_NUM=2 -I../C -I$(CAML_PREFIX)/lib/ocaml -I$(CAMLIDL_PREFIX)/lib/ocaml -c -o $@ $<
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_DEBUG) -DPOLKA_NUM=2 -I../C -I$(CAML_PREFIX) -I$(CAMLIDL_PREFIX) -c -o $@ $<
%g_caml_debug.o: %_caml.c
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_DEBUG) -DPOLKA_NUM=3 -I$(GMP_PREFIX)/include -I../C -I$(CAML_PREFIX)/lib/ocaml -I$(CAMLIDL_PREFIX)/lib/ocaml -c -o $@ $<
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_DEBUG) -DPOLKA_NUM=3 -I$(GMP_PREFIX)/include -I../C -I$(CAML_PREFIX) -I$(CAMLIDL_PREFIX) -c -o $@ $<
%i_caml_prof.o: %_caml.c
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_PROF) -DPOLKA_NUM=1 -I../C -I$(CAML_PREFIX)/lib/ocaml -I$(CAMLIDL_PREFIX)/lib/ocaml -c -o $@ $<
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_PROF) -DPOLKA_NUM=1 -I../C -I$(CAML_PREFIX) -I$(CAMLIDL_PREFIX) -c -o $@ $<
%l_caml_prof.o: %_caml.c
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_PROF) -DPOLKA_NUM=2 -I../C -I$(CAML_PREFIX)/lib/ocaml -I$(CAMLIDL_PREFIX)/lib/ocaml -c -o $@ $<
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_PROF) -DPOLKA_NUM=2 -I../C -I$(CAML_PREFIX) -I$(CAMLIDL_PREFIX) -c -o $@ $<
%g_caml_prof.o: %_caml.c
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_PROF) -DPOLKA_NUM=3 -I$(GMP_PREFIX)/include -I../C -I$(CAML_PREFIX)/lib/ocaml -I$(CAMLIDL_PREFIX)/lib/ocaml -c -o $@ $<
$(CC) $(ICFLAGS) $(XCFLAGS) $(CAML_CFLAGS_PROF) -DPOLKA_NUM=3 -I$(GMP_PREFIX)/include -I../C -I$(CAML_PREFIX) -I$(CAMLIDL_PREFIX) -c -o $@ $<
#-----------------------------------
# CAML part
......
......@@ -405,48 +405,48 @@ let find_some_sols
(g : guard)
= match g.g_sol with
| Some s -> s
| None -> let zesol = (
(* clean everything in case ? *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
(* HERE : dont't know exactly why but it seems to be
necessary to call Solver.is_satisfiable first
*)
let solver_vl = ref 0 in
Verbose.exe ~flag:dbg (fun _ -> solver_vl := 3);
let is_bool_sat = Solver.is_satisfiable
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl *)
(Verbose.level())
"LutExe.is_bool_sat" (* ctx_msg: string *)
g.g_form
"LutExe.is_bool_sat" (* msg: string (?) *)
in
if not is_bool_sat then (
[]
) else (
let sols = Solver.solve_formula
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl (* vl: int *) *)
(Verbose.level())
"LutExe.solve_guard" (* msg: string *)
[it.out_var_names] (* output_var_names: Var.name list list *)
tfdn (* p: Thickness.formula_draw_nb *)
tn (* num_thickness Thickness.numeric *)
it.bool_vars_to_gen (* bool_vars_to_gen_f: formula *)
it.num_vars_to_gen (* num_vars_to_gen: var list *)
g.g_form (* f: formula *)
in
sols
)
) in (
g.g_sol <- Some zesol;
zesol
)
| None ->
let zesol = (
(* clean everything in case ? *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
(* HERE : don't know exactly why but it seems to be
necessary to call Solver.is_satisfiable first
*)
let solver_vl = ref 0 in
Verbose.exe ~flag:dbg (fun _ -> solver_vl := 3);
let is_bool_sat = Solver.is_satisfiable
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl *)
(Verbose.level())
"LutExe.is_bool_sat" (* ctx_msg: string *)
g.g_form
"LutExe.is_bool_sat" (* msg: string (?) *)
in
if not is_bool_sat then (
[]
) else (
let sols = Solver.solve_formula
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl (* vl: int *) *)
(Verbose.level())
"LutExe.solve_guard" (* msg: string *)
[it.out_var_names] (* output_var_names: Var.name list list *)
tfdn (* p: Thickness.formula_draw_nb *)
tn (* num_thickness Thickness.numeric *)
it.bool_vars_to_gen (* bool_vars_to_gen_f: formula *)
it.num_vars_to_gen (* num_vars_to_gen: var list *)
g.g_form (* f: formula *)
in
sols
)
) in (
g.g_sol <- Some zesol;
zesol
)
let find_one_sol it g =
let thick = match MainArg.step_mode it.arg_opt with
......@@ -464,8 +464,8 @@ let check_satisfiablity (it:t) (g: guard) = (
try (
Verbose.put ~flag:dbg
"--check satisfiablility of \"%s\"\n"
(* (Exp.formula_to_string g.g_form); *)
(string_of_guard g);
(* (Exp.formula_to_string g.g_form); *)
(string_of_guard g);
let _ = find_one_sol it g in
true
) with Not_found -> false
......
......@@ -262,8 +262,7 @@ and (translate_do : Var.env_in -> Var.env -> string -> int -> Exp.formula ->
try (bdd_global f, false)
with Not_found ->
let (bdd, dep) =
(* output_msg (" >>> " ^ (formula_to_string f) ^ "\n") ; *)
match f with
match f with
Not(f1) ->
let (bdd_not, dep) = (translate_do input memory ctx_msg vl f1) in
(Bdd.dnot bdd_not, dep)
......@@ -352,6 +351,12 @@ and (translate_do : Var.env_in -> Var.env -> string -> int -> Exp.formula ->
let gne = expr_to_gne (Diff(e2, e1)) input memory ctx_msg vl in
(gne_to_bdd gne SupZero)
in
if vl > 1 then (
Printf.eprintf "%s" (" >>> " ^ (formula_to_string f) ^ " " ^
(if Bdd.is_false bdd then " is false " else "") ^
(if Bdd.is_true bdd then " is true " else "") ^"\n") ;
flush stderr
);
if
dep
then
......
......@@ -18,7 +18,7 @@ module StringSet = struct
end
let debug = true
let debug = false
let debug = false
let (get_vars_cl : Constraint.ineq list -> StringSet.t) =
fun cl ->
......@@ -439,7 +439,7 @@ let (matrix_to_vector_list : Matrix.t -> Vector.t list) =
matrix_to_vector_list2 0 []
let my_get r i =
let get_row r i =
let str = Vector.get_str10 r i in
float_of_string str
......@@ -458,49 +458,55 @@ let (get_vertices : Poly.t -> (int -> string) -> point list) =
(* print_string "\n"; *)
(* flush stdout ; *)
(* in *)
match Poly.frames poly with
Some(matrix) ->
let row_list = matrix_to_vector_list matrix in
let generators =
List.map
(fun row ->
let denom = my_get row 1
and line = my_get row 0
in
if
(line = 0.0 || denom = 0.0)
then
(
Poly.print rank_to_name Format.std_formatter poly ;
print_string "\n";
flush stdout ;
failwith ("*** Can not draw fairly in an " ^
"unbounded set of solutions.")
)
else
let rec (vector_to_point : Vector.t -> float -> int -> point) =
fun row denom cpt ->
let p = ( (my_get row cpt)) /. denom in
if
(cpt = (Vector.length row) -1)
then
[p]
else
p::(vector_to_point row denom (cpt+1))
in
vector_to_point row ( denom) 2
)
row_list
in
(* Remove the epsilon dimension *)
List.map
(fun l -> List.tl l)
(List.filter
(fun l -> (List.hd l) = 0.)
generators
)
| None -> assert false
let res =
match Poly.frames poly with
Some(matrix) ->
let row_list = matrix_to_vector_list matrix in
let generators =
List.map
(fun row ->
let denom = get_row row 1
and line = get_row row 0
in
if
(line = 0.0 || denom = 0.0)
then
(
Poly.print rank_to_name Format.std_formatter poly ;
print_string "\n";
flush stdout ;
failwith ("*** Can not draw fairly in an " ^
"unbounded set of solutions.")
)
else
let rec (vector_to_point : Vector.t -> float -> int -> point) =
fun row denom cpt ->
let p = ( (get_row row cpt)) /. denom in
if
(cpt = (Vector.length row) -1)
then
[p]
else
p::(vector_to_point row denom (cpt+1))
in
vector_to_point row ( denom) 2
)
row_list
in
(* Remove the epsilon dimension *)
List.map
(fun l -> List.tl l)
(List.filter
(fun l -> (List.hd l) = 0.)
generators
)
| None -> assert false
in
(* let sop p = "("^ (String.concat "," (List.map string_of_float p)) ^ ")" in *)
(* let str = String.concat "," (List.map sop res) in *)
(* Printf.eprintf "Generators are: %s.\n" str; *)
(* flush stderr; *)
res
(****************************************************************************)
......
......@@ -58,37 +58,37 @@ let (set_fair_mode : unit -> unit) =
(* Exported *)
let (is_satisfiable: Var.env_in -> Var.env -> int -> string -> formula -> string -> bool) =
fun input memory vl ctx_msg f msg ->
let bdd = Formula_to_bdd.f input memory ctx_msg vl f in
let is_sat1 = not (Bdd.is_false bdd)
and is_sat2 =
(* the formula may be false because of numerics. In that case,
the solution number is set to (0,0) (if a draw has been tried).
the solution number is set to (0,0) (if a draw has been tried).
*)
(
try
let (n, m) = !sol_number bdd in
not ((Sol_nb.zero_sol, Sol_nb.zero_sol) = (n, m))
with
Not_found -> true
(* migth be false because of numerics, but we don't know yet *)
| e ->
print_string ((Printexc.to_string e) ^ "\n");
flush stdout;
assert false
try
let (n, m) = !sol_number bdd in
not ((Sol_nb.zero_sol, Sol_nb.zero_sol) = (n, m))
with
Not_found -> true
(* migth be false because of numerics, but we don't know yet *)
| e ->
print_string ((Printexc.to_string e) ^ "\n");
flush stdout;
assert false
)
in
if vl > 2 then
(
print_string ("\n[" ^ msg^ "] -> ");
print_string (formula_to_string f);
if is_sat1 && is_sat2
then print_string "\n is satisfiable (for the Boolean part).\n"
else if is_sat1
then print_string "\n is not satisfiable.\n"
else print_string "\n is not satisfiable (because of Booleans).\n";
flush stdout
);
(
print_string ("\n[" ^ msg^ "] -> ");
print_string (formula_to_string f);
if is_sat1 && is_sat2
then print_string "\n is satisfiable (for the Boolean part).\n"
else if is_sat1
then print_string "\n is not satisfiable (because of numerics).\n"
else print_string "\n is not satisfiable (because of Booleans).\n";
flush stdout
);
is_sat1 && is_sat2
(****************************************************************************)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment