Skip to content

GitLab

Commit c6673f68 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Make trywhy3 compatible with alt-ergo 2.0.

parent 4dd0cc57
Hide whitespace changes
Inline Side-by-side
Showing with 137 additions and 100 deletions
Makefile.in
View file @ c6673f68
......@@ -1664,36 +1664,79 @@ endif
ALTERGODIR=src/trywhy3/alt-ergo
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.syntax \
-package ocplib-simplex -syntax camlp4o -I src/trywhy3 \
-I $(ALTERGODIR)/src/util \
-I $(ALTERGODIR)/src/structures \
-I $(ALTERGODIR)/src/parsing \
-I $(ALTERGODIR)/src/preprocess \
-I $(ALTERGODIR)/src/theories \
-I $(ALTERGODIR)/src/instances \
-I $(ALTERGODIR)/src/sat \
-I $(ALTERGODIR)/src/main
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 \
-package ocplib-simplex -I src/trywhy3 \
-I $(ALTERGODIR)/lib/util \
-I $(ALTERGODIR)/lib/structures \
-I $(ALTERGODIR)/lib/parsing \
-I $(ALTERGODIR)/lib/frontend \
-I $(ALTERGODIR)/lib/reasoners \
-I $(ALTERGODIR)/parsers/why
ALTERGOLIBS = \
util/config \
util/version \
util/emap \
util/myUnix \
util/myDynlink \
util/myZip \
util/util \
util/lists \
util/numsNumbers \
util/numbers \
util/options \
util/cmdline_parser \
util/timers \
util/gc_debug \
util/loc \
util/hconsing \
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 \
parsing/why_parser parsing/why_lexer \
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)))
structures/exception \
structures/symbols \
structures/ty \
structures/parsed \
structures/errors \
structures/typed \
structures/term \
structures/fpa_rounding \
structures/literal \
structures/formula \
structures/explanation \
structures/commands \
structures/profiling \
reasoners/matching \
reasoners/instances \
reasoners/polynome \
reasoners/ac \
reasoners/uf \
reasoners/use \
reasoners/intervals \
reasoners/inequalities \
reasoners/intervalCalculus \
reasoners/arith \
reasoners/records \
reasoners/bitv \
reasoners/arrays \
reasoners/sum \
reasoners/combine \
reasoners/ccx \
reasoners/theory \
reasoners/fun_sat \
reasoners/sat_solver \
frontend/triggers \
frontend/typechecker \
frontend/cnf \
frontend/parsed_interface \
frontend/frontend \
frontend/parsers
ALTERGOPARSERS = \
why/why_parser \
why/why_lexer
ALTERGOCMO = \
$(addprefix $(ALTERGODIR)/lib/, $(addsuffix .cmo,$(ALTERGOLIBS))) \
$(addprefix $(ALTERGODIR)/parsers/, $(addsuffix .cmo,$(ALTERGOPARSERS)))
TRYWHY3CMO=lib/why3/why3.cma
TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \
README examples/ \
......@@ -1720,7 +1763,7 @@ src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/why3_worker.js src/
src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte src/trywhy3/try_alt_ergo.drv
js_of_ocaml $(JSOO_DEBUG) --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
`find stdlib \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/%p"` \
......@@ -1745,6 +1788,10 @@ src/trywhy3/%.cmo: src/trywhy3/%.ml
src/trywhy3/%.cmi: src/trywhy3/%.mli
$(JSOCAMLC) $(BFLAGS) -c $<
src/trywhy3/%.cmo: BFLAGS += -w -48
src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo: BFLAGS += -syntax camlp4o
clean::
rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte src/trywhy3/trywhy3.cm* \
src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte src/trywhy3/why3_worker.cm* \
......
src/trywhy3/alt-ergo.patch
View file @ c6673f68
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 @@
diff -r -u alt-ergo-2.0.0/lib/reasoners/fun_sat.ml alt-ergo/lib/reasoners/fun_sat.ml
--- alt-ergo-2.0.0/lib/reasoners/fun_sat.ml 2017-11-14 18:01:38.000000000 +0100
+++ alt-ergo/lib/reasoners/fun_sat.ml 2018-05-24 16:10:10.418194590 +0200
@@ -29,6 +29,7 @@
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
module Th = Theory.Main
open Sig
@@ -691,8 +692,7 @@
if steps_bound () <> -1
&& Int64.compare !steps (Int64.of_int (steps_bound ())) > 0 then
begin
- printf "Steps limit reached: %Ld@." !steps;
- exit 1
+ raise StepsLimitReached
end;
{ env with tbox = tbox; unit_tbox = utbox; inst = inst }
diff -r -u alt-ergo-2.0.0/lib/reasoners/fun_sat.mli alt-ergo/lib/reasoners/fun_sat.mli
--- alt-ergo-2.0.0/lib/reasoners/fun_sat.mli 2017-11-14 18:01:38.000000000 +0100
+++ alt-ergo/lib/reasoners/fun_sat.mli 2018-05-24 16:10:45.622082786 +0200
@@ -27,3 +27,5 @@
(******************************************************************************)
+exception StepsLimitReached
include Sat_solver_sig.S
+
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 *)
+exception StepsLimitReached
diff -r -u alt-ergo-2.0.0/lib/util/numbers.ml alt-ergo/lib/util/numbers.ml
--- alt-ergo-2.0.0/lib/util/numbers.ml 2017-11-14 18:01:38.000000000 +0100
+++ alt-ergo/lib/util/numbers.ml 2018-05-24 16:12:31.849745671 +0200
@@ -26,7 +26,7 @@
(* *)
(******************************************************************************)
-module MyZarith = ZarithNumbers
-module MyNums = NumsNumbers
+module MyZarith = (*ZarithNumbers
+module MyNums =*) NumsNumbers
+module MyZarith = NumsNumbers
module MyNums = NumsNumbers
module Z = MyZarith.Z
src/trywhy3/alt_ergo_worker.ml
View file @ c6673f68
......@@ -12,7 +12,7 @@
open Format
open Worker_proto
module SAT = (val (Sat_solvers.get_current ()) : Sat_solvers.S)
module SAT = (val (Sat_solver.get_current ()) : Sat_solver_sig.S)
module FE = Frontend.Make (SAT)
let print_status fmt _d status steps =
......@@ -34,10 +34,10 @@ let report_status report _d status _steps =
let run_alt_ergo_on_task text =
let lb = Lexing.from_string text in
(* from Alt-Ergo, src/main/frontend.ml *)
let a = Why_parser.file Why_lexer.token lb in
let a = Why_parser.file_parser Why_lexer.parse_token lb in
Parsing.clear_parser ();
let ltd, _typ_env = Why_typing.file false Why_typing.empty_env a in
match Why_typing.split_goals ltd with
let ltd, _typ_env = Typechecker.file false Typechecker.empty_env a in
match Typechecker.split_goals ltd with
| [d] ->
let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
SAT.reset_refs ();
......@@ -49,7 +49,7 @@ let run_alt_ergo_on_task text =
(SAT.empty (), true, Explanation.empty) d
in
!stat
with Sat_solvers.StepsLimitReached -> Unknown "steps limit reached"
with Fun_sat.StepsLimitReached -> Unknown "steps limit reached"
end
| _ -> Invalid "zero or more than 1 goal to solve"
......@@ -58,6 +58,7 @@ let run_alt_ergo_on_task text =
let () =
Options.set_steps_bound 100;
Options.set_is_gui false;
Worker.set_onmessage (fun msg ->
match unmarshal msg with
Goal (id, text, steps) ->
......
src/trywhy3/try_alt_ergo.drv
View file @ c6673f68
......@@ -74,16 +74,16 @@ theory int.Int
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
remove prop Unit_def_l
remove prop Unit_def_r
remove prop Inv_def_l
remove prop Inv_def_r
remove prop Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
......@@ -140,16 +140,16 @@ theory real.Real
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
remove prop Unit_def_l
remove prop Unit_def_r
remove prop Inv_def_l
remove prop Inv_def_r
remove prop Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
......@@ -195,16 +195,16 @@ end
theory algebra.AC
meta AC function op
remove prop Comm.Comm
remove prop Comm
remove prop Assoc
end
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
theory HighOrd
syntax type (->) "(%1,%2) farray"
syntax function (@) "(%1[%2])"
end
remove prop Select_eq
remove prop Select_neq
theory map.Map
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
end
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