Commit 31d1ddb8 authored by Andrei Paskevich's avatar Andrei Paskevich

trywhy3: update for Alt-Ergo 1.30

parent fd3cdc28
......@@ -1470,7 +1470,7 @@ else
JS_MAPS=
endif
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
ALTERGODIR=src/trywhy3/alt-ergo
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3 \
......@@ -1483,27 +1483,25 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.syntax \
-I $(ALTERGODIR)/src/sat \
-I $(ALTERGODIR)/src/main
ALTERGOMODS=util/numsNumbers util/numbers \
util/version util/myUnix util/config util/options \
util/hashcons util/hstring util/lists util/loc \
ALTERGOMODS=util/config util/version util/emap util/myUnix util/myDynlink \
util/myZip util/util util/lists util/numsNumbers util/numbers \
util/timers util/options util/gc_debug util/loc util/hashcons \
util/hstring \
structures/exception structures/symbols structures/ty \
structures/parsed structures/typed structures/term structures/literal \
structures/formula structures/explanation structures/errors \
util/profiling_default util/profiling \
util/util \
structures/parsed structures/symbols \
structures/ty structures/errors \
structures/term structures/literal structures/formula \
structures/explanation structures/exception \
parsing/why_parser parsing/why_lexer \
preprocess/existantial preprocess/triggers \
preprocess/why_typing preprocess/cnf \
theories/polynome theories/ac \
theories/intervals theories/inequalities \
theories/intervalCalculus \
theories/arith theories/records theories/bitv \
theories/arrays theories/sum theories/uf theories/use \
theories/combine theories/ccx theories/theory \
instances/matching \
preprocess/existantial preprocess/triggers preprocess/why_typing \
preprocess/cnf \
instances/matching instances/instances \
theories/polynome theories/ac theories/uf theories/use \
theories/intervals theories/inequalities theories/intervalCalculus \
theories/arith theories/records theories/bitv theories/arrays \
theories/sum theories/combine theories/ccx theories/theory \
sat/sat_solvers \
main/frontend
ALTERGOCMO=$(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
TRYWHY3CMO=lib/why3/why3.cma
TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \
......@@ -1512,7 +1510,7 @@ TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \
fontawesome/fonts/FontAwesome.otf fontawesome/fonts/fontawesome-webfont.svg \
fontawesome/fonts/fontawesome-webfont.woff fontawesome/fonts/fontawesome-webfont.eot \
fontawesome/fonts/fontawesome-webfont.ttf fontawesome/fonts/fontawesome-webfont.woff2 \
ace-builds/src-min-noconflict/ace.js ace-builds/src-min-noconflict/mode-why3.js \
ace-builds/src-min-noconflict/ace.js ace-builds/src-min-noconflict/mode-why3.js \
ace-builds/src-min-noconflict/theme-chrome.js $(JS_MAPS)
trywhy3_package: trywhy3
......@@ -1546,7 +1544,7 @@ src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
js_of_ocaml $(JSOO_DEBUG) +weak.js +nat.js +dynlink.js +toplevel.js $<
src/trywhy3/alt_ergo_worker.byte: $(ALTERGOCMO) src/trywhy3/worker_proto.cmo src/trywhy3/alt_ergo_worker.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
$(JSOCAMLC) -I +ocplib-simplex $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) ocplibSimplex.cma $^
src/trywhy3/alt_ergo_worker.cmo: src/trywhy3/worker_proto.cmo
src/trywhy3/why3_worker.cmo: src/trywhy3/worker_proto.cmo
......
......@@ -20,7 +20,7 @@ Instructions to build TryWhy3
- get sources of Alt-Ergo and put them in directory src/trywhy3/ e.g. in
src/trywhy3/alt-ergo-1.00-private-2015-01-29/
src/trywhy3/alt-ergo/
- apply the patch alt-ergo.patch
......@@ -38,7 +38,7 @@ Instructions to build TryWhy3
** if necessary, change the following line of Makefile.in to point
to Alt-Ergo sources
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
ALTERGODIR=src/trywhy3/alt-ergo
** [optional] If you want to build a standalone trywhy3 that can be
run without a Webserver, the example files must be present at
......@@ -90,4 +90,4 @@ Instructions to build TryWhy3
trywhy3.html.
Note that this is the default behaviour when trywhy3.html is opened from
a file:// URL rather than an http(s):// URL, regardless of the value of
the load_embedded_files variable.
\ No newline at end of file
the load_embedded_files variable.
Only in alt-ergo-1.00-private-2015-01-29/: autom4te.cache
Only in alt-ergo-1.00-private-2015-01-29/: config.status
Only in alt-ergo-1.00-private-2015-01-29/: .depend
Only in alt-ergo-1.00-private-2015-01-29/: Makefile.configurable
diff -c -r /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml
*** /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml 2016-04-07 16:01:57.449020746 +0200
--- alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml 2016-04-08 10:26:05.485174395 +0200
***************
*** 23,28 ****
--- 23,30 ----
open Options
open Format
+ exception StepsLimitReached
+
module type S = sig
type t
***************
*** 492,499 ****
--- 494,504 ----
if steps_bound () <> -1
&& Int64.compare !steps (Int64.of_int (steps_bound ())) > 0 then
begin
+ raise StepsLimitReached;
+ (*
printf "Steps limit reached: %Ld@." !steps;
exit 1
+ *)
end;
{ env with tbox = tbox; unit_tbox = utbox; inst = inst }
diff -c -r /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli
*** /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli 2016-04-07 16:01:57.449020746 +0200
--- alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli 2016-04-08 10:26:05.485174395 +0200
***************
*** 20,25 ****
--- 20,27 ----
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
+ exception StepsLimitReached
+
module type S = sig
type t
diff -c -r /tmp/alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml
*** /tmp/alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml 2016-04-07 16:01:57.453020790 +0200
--- alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml 2016-04-08 10:41:51.037337014 +0200
***************
*** 20,28 ****
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
! module MyZarith = ZarithNumbers
module MyNums = NumsNumbers
! include MyZarith
--- 20,29 ----
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
! (* module MyZarith = ZarithNumbers *)
module MyNums = NumsNumbers
! include MyNums
!
diff --git a/src/sat/sat_solvers.ml b/src/sat/sat_solvers.ml
index 97e384e..5213df7 100644
--- a/src/sat/sat_solvers.ml
+++ b/src/sat/sat_solvers.ml
@@ -23,6 +23,8 @@
open Options
open Format
+exception StepsLimitReached
+
module type S = sig
type t
@@ -580,8 +582,11 @@ module Dfs_sat : S = struct
if steps_bound () <> -1
&& Int64.compare !steps (Int64.of_int (steps_bound ())) > 0 then
begin
+ raise StepsLimitReached;
+(*
printf "Steps limit reached: %Ld@." !steps;
exit 1
+ *)
end;
{ env with tbox = tbox; unit_tbox = utbox; inst = inst }
diff --git a/src/sat/sat_solvers.mli b/src/sat/sat_solvers.mli
index f4f9f60..4da53d1 100644
--- a/src/sat/sat_solvers.mli
+++ b/src/sat/sat_solvers.mli
@@ -22,6 +22,8 @@
open Options
+exception StepsLimitReached
+
module type S = sig
type t
diff --git a/src/util/numbers.ml b/src/util/numbers.ml
index ebf8f95..f172a03 100644
--- a/src/util/numbers.ml
+++ b/src/util/numbers.ml
@@ -20,8 +20,8 @@
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
-module MyZarith = ZarithNumbers
-module MyNums = NumsNumbers
+module MyZarith = (*ZarithNumbers
+module MyNums =*) NumsNumbers
module Z = MyZarith.Z
......@@ -40,7 +40,7 @@ let run_alt_ergo_on_task text =
match Why_typing.split_goals ltd with
| [d] ->
let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
SAT.reset_steps ();
SAT.reset_refs ();
let stat = ref (Invalid "no answer from Alt-Ergo") in
let f s = stat := s in
begin
......
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