Commit aa611eed authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into claude

Conflicts:
	drivers/cvc4_bare.drv
	drivers/smt-libv2.drv
	examples/logic/lagrange_inequality/why3session.xml
	examples/logic/triangle_inequality/why3session.xml
parents 364795f2 39b53c76
......@@ -794,12 +794,12 @@ src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
$(if $(QUIET),@echo 'Camlp5 $<' &&) \
$(CAMLP5O) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cma
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
touch src/coq-tactic/.why3-vo-byte
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cmxs
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
touch src/coq-tactic/.why3-vo-opt
......@@ -830,6 +830,8 @@ endif
# Coq realizations
####################
ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes)
COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
......@@ -865,18 +867,6 @@ endif
COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
%.vo: %.v
$(if $(QUIET),@echo 'Coqc $<' &&) \
$(COQC) -R lib/coq Why3 $<
%.vd: %.v
$(if $(QUIET),@echo 'Coqdep $<' &&) \
$(COQDEP) -R lib/coq Why3 $< > $@
drivers/coq-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
......@@ -901,8 +891,6 @@ drivers/coq-realizations.aux: Makefile
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
opt byte: $(COQVO)
install_no_local::
mkdir -p $(LIBDIR)/why3/coq
cp lib/coq/BuiltIn.vo $(LIBDIR)/why3/coq/
......@@ -926,22 +914,6 @@ ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
endif
cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
install_local:: $(COQVO) drivers/coq-realizations.aux
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
include $(COQVD)
endif
endif
depend: $(COQVD)
clean-coq:
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
clean:: clean-coq
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp
......@@ -977,11 +949,49 @@ else
drivers/coq-realizations.aux:
echo "(* generated automatically at compilation time *)" > $@
install_no_local::
cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
COQLIBS_FILES = lib/coq/BuiltIn
endif
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
%.vo: %.v
$(if $(QUIET),@echo 'Coqc $<' &&) \
$(COQC) -R lib/coq Why3 $<
%.vd: %.v
$(if $(QUIET),@echo 'Coqdep $<' &&) \
$(COQDEP) -R lib/coq Why3 $< > $@
opt byte: $(COQVO)
install_local:: $(COQVO) drivers/coq-realizations.aux
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
include $(COQVD)
endif
endif
depend: $(COQVD)
clean-coq:
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
clean:: clean-coq
else
drivers/coq-realizations.aux:
echo "(* generated automatically at compilation time *)" > $@
endif
install_no_local::
cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
opt byte: drivers/coq-realizations.aux
clean::
......
......@@ -516,6 +516,12 @@ else
;;
esac
fi
AC_CHECK_PROG(COQDEP,coqdep,coqdep,no)
if test "$COQDEP" = no ; then
enable_coq_support=no
AC_MSG_WARN(Cannot find coqdep.)
reason_coq_support=" (coqdep not found)"
fi
fi
if test "$enable_coq_support" = no; then
......@@ -538,15 +544,6 @@ if test "$enable_coq_tactic" = yes -a "$CAMLP5O" = no; then
reason_coq_tactic=" (camlp5o not found)"
fi
if test "$enable_coq_libs" = yes; then
AC_CHECK_PROG(COQDEP,coqdep,coqdep,no)
if test "$COQDEP" = no ; then
enable_coq_libs=no
AC_MSG_WARN(Cannot find coqdep.)
reason_coq_libs=" (coqdep not found)"
fi
fi
if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq])
AS_IF(
......@@ -756,6 +753,7 @@ AC_SUBST(MENHIRLIB)
AC_SUBST(enable_coq_tactic)
AC_SUBST(enable_coq_libs)
AC_SUBST(enable_coq_support)
AC_SUBST(enable_coq_fp_libs)
AC_SUBST(coq_compat_version)
......
......@@ -344,6 +344,7 @@ depending on whether the index is meaningful or not.
\begin{whycode}
module SearchingALinkedList
use import int.Int
use import option.Option
use export list.List
use export list.Length
use export list.Nth
......@@ -795,6 +796,7 @@ operations we will require: length, reversal, and concatenation.
\begin{whycode}
module AmortizedQueue
use import int.Int
use import option.Option
use export list.ListRich
\end{whycode}
The queue data type is naturally introduced as a polymorphic record type.
......
......@@ -182,15 +182,7 @@ theory bv.BV32
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
(* syntax function to_uint "(bv2nat %1)" *)
(* syntax function to_int "(bv2int %1)" (* Z3 vb2nat *)*)
(* syntax function to_int "(ite (= ((_ extract 31 31) %1) #b0) *)
(* (bv2nat %1) *)
(* (- (bv2nat %1) 4294967296))" *)
(* syntax function of_int "((_ int2bv 32) %1)" *)
syntax function of_int_const "((_ int2bv 32) %1)"
(* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *)
(* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *)
syntax converter of_int_const "((_ int2bv 32) %1)"
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
......@@ -202,26 +194,6 @@ theory bv.BV32
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
(* remove prop Nth_zero *)
(* remove prop Nth_ones *)
(* remove prop Nth_bw_and *)
(* remove prop Nth_bw_or *)
(* remove prop Nth_bw_xor *)
(* remove prop Nth_bw_not *)
(* remove prop Add_is_add *)
(* remove prop Min_is_min *)
(* remove prop Neg_is_neg *)
(* remove prop Mul_is_mul *)
(* remove prop Udiv_is_udiv *)
(* remove prop Lsr_nth_low *)
(* remove prop Lsr_nth_high *)
(* remove prop Lsl_nth_low *)
(* remove prop Lsl_nth_high *)
(* remove prop Asr_nth_low *)
(* remove prop Asr_nth_high *)
end
theory bv.BV32Ax
......@@ -253,14 +225,7 @@ theory bv.BV32Ax
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
(* syntax function to_uint "(bv2nat %1)" *)
(* syntax function to_int "(ite (= ((_ extract 31 31) %1) #b0) *)
(* (bv2nat %1) *)
(* (- (bv2nat %1) 4294967296))" *)
(* syntax function of_int "((_ int2bv 32) %1)" *)
syntax function of_int_const "((_ int2bv 32) %1)"
(* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *)
(* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *)
syntax converter of_int_const "((_ int2bv 32) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
......@@ -272,25 +237,11 @@ theory bv.BV32Ax
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
(* remove prop Nth_zero *)
(* remove prop Nth_ones *)
(* remove prop Nth_bw_and *)
(* remove prop Nth_bw_or *)
(* remove prop Nth_bw_xor *)
(* remove prop Nth_bw_not *)
remove prop Add_is_add
remove prop Min_is_min
remove prop Neg_is_neg
remove prop Mul_is_mul
remove prop Udiv_is_udiv
(* remove prop Lsr_nth_low *)
(* remove prop Lsr_nth_high *)
(* remove prop Lsl_nth_low *)
(* remove prop Lsl_nth_high *)
(* remove prop Asr_nth_low *)
(* remove prop Asr_nth_high *)
end
theory bv.BV64
......@@ -322,7 +273,7 @@ theory bv.BV64
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax function of_int_const "((_ int2bv 64) %1)"
syntax converter of_int_const "((_ int2bv 64) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
......@@ -364,7 +315,7 @@ theory bv.BV16
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax function of_int_const "((_ int2bv 16) %1)"
syntax converter of_int_const "((_ int2bv 16) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
......@@ -406,7 +357,7 @@ theory bv.BV8
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax function of_int_const "((_ int2bv 8) %1)"
syntax converter of_int_const "((_ int2bv 8) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
......
......@@ -2,103 +2,109 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="10" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<file name="../bag.mlw" expanded="true">
<theory name="Bag" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Bag" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="BagSpec" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="BagSpec" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ResizableArraySpec" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="ResizableArraySpec" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="BagImpl" sum="e5c247f3bba7104c0837200325f56fbc" expanded="true">
<goal name="WP_parameter create" expl="VC for create">
<proof prover="2"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter clear" expl="VC for clear">
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="1"><result status="valid" time="2.76"/></proof>
<proof prover="2"><result status="valid" time="2.76"/></proof>
</goal>
<goal name="WP_parameter get" expl="VC for get">
<proof prover="2"><result status="valid" time="0.00" steps="11"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter remove" expl="VC for remove" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter remove" expl="VC for remove">
<transf name="split_goal_wp">
<goal name="WP_parameter remove.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.04" steps="4"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="4"/></proof>
</goal>
<goal name="WP_parameter remove.2" expl="2. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove.3" expl="3. precondition">
<proof prover="2"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter remove.4" expl="4. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove.5" expl="5. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter remove.6" expl="6. assertion">
<proof prover="0"><result status="valid" time="1.75"/></proof>
<proof prover="1"><result status="valid" time="1.75"/></proof>
</goal>
<goal name="WP_parameter remove.7" expl="7. assertion" expanded="true">
<proof prover="0" timelimit="76"><result status="valid" time="8.94"/></proof>
<goal name="WP_parameter remove.7" expl="7. assertion">
<proof prover="1" timelimit="76"><result status="valid" time="8.94"/></proof>
</goal>
<goal name="WP_parameter remove.8" expl="8. type invariant">
<proof prover="2"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter remove.9" expl="9. type invariant">
<proof prover="2"><result status="valid" time="0.02" steps="37"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
<goal name="WP_parameter remove.10" expl="10. type invariant">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter remove.11" expl="11. postcondition">
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter remove.12" expl="12. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter remove.13" expl="13. precondition">
<proof prover="2"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter remove.14" expl="14. assertion">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.64"/></proof>
</goal>
<goal name="WP_parameter remove.15" expl="15. assertion">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter remove.16" expl="16. type invariant">
<proof prover="2"><result status="valid" time="0.01" steps="12"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter remove.17" expl="17. type invariant">
<proof prover="2"><result status="valid" time="0.03" steps="33"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="33"/></proof>
</goal>
<goal name="WP_parameter remove.18" expl="18. type invariant">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter remove.19" expl="19. postcondition">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter remove.20" expl="20. postcondition">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Harness" sum="528e93ede1770450354a9703428c111b">
<theory name="Harness" sum="528e93ede1770450354a9703428c111b" expanded="true">
<goal name="WP_parameter test1" expl="VC for test1">
<transf name="split_goal_wp">
<goal name="WP_parameter test1.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="1.52" steps="249"/></proof>
<proof prover="0"><result status="valid" time="0.39" steps="195"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="0.18"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="1.52" steps="249"/></proof>
</goal>
<goal name="WP_parameter test1.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="4.99"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......
......@@ -509,6 +509,6 @@ end
(*
Local Variables:
compile-command: "why3ide -L . bitvector.why"
compile-command: "why3 ide -L . bitvector.why"
End:
*)
......@@ -278,6 +278,6 @@ end
(*
Local Variables:
compile-command: "why3ide -L . double_of_int.why"
compile-command: "why3 ide -L . double_of_int.why"
End:
*)
......@@ -40,6 +40,6 @@ end
(*
Local Variables:
compile-command: "why3ide -L . neg_as_xor.why"
compile-command: "why3 ide -L . neg_as_xor.why"
End:
*)
......@@ -3,80 +3,105 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="2.19" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="10" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="10" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../neg_as_xor.why" expanded="true">
<theory name="TestNegAsXOR" sum="6138fee1d9542841b21ad746cad9a930" expanded="true">
<goal name="Nth_j" expanded="true">
<proof prover="5" timelimit="3"><result status="valid" time="0.35" steps="107"/></proof>
<goal name="Nth_j">
<proof prover="1"><result status="valid" time="0.56" steps="114"/></proof>
<proof prover="6" timelimit="3"><result status="valid" time="0.35" steps="107"/></proof>
</goal>
<goal name="sign_of_j" expanded="true">
<proof prover="5"><result status="valid" time="0.09" steps="100"/></proof>
<goal name="sign_of_j">
<proof prover="1"><result status="valid" time="0.15" steps="108"/></proof>
<proof prover="3"><result status="valid" time="0.86"/></proof>
<proof prover="6"><result status="valid" time="0.09" steps="100"/></proof>
</goal>
<goal name="mantissa_of_j" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="2"><result status="valid" time="0.61"/></proof>
<proof prover="3"><result status="valid" time="0.67"/></proof>
<proof prover="4"><result status="valid" time="3.22"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="104"/></proof>
<goal name="mantissa_of_j">
<proof prover="1"><result status="valid" time="0.16" steps="123"/></proof>
<proof prover="2"><result status="valid" time="0.78"/></proof>
<proof prover="3"><result status="valid" time="0.61"/></proof>
<proof prover="4"><result status="valid" time="0.85"/></proof>
<proof prover="5"><result status="valid" time="3.73"/></proof>
<proof prover="6"><result status="valid" time="0.06" steps="104"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="exp_of_j" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<goal name="exp_of_j">
<proof prover="1"><result status="valid" time="0.17" steps="124"/></proof>
<proof prover="2"><result status="valid" time="0.62"/></proof>
<proof prover="3"><result status="valid" time="0.70"/></proof>
<proof prover="4" timelimit="11"><result status="valid" time="2.67"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="3"><result status="valid" time="0.59"/></proof>
<proof prover="4"><result status="valid" time="0.92"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.13"/></proof>
<proof prover="6"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="7"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="int_of_bv" expanded="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<goal name="int_of_bv">
<proof prover="1"><result status="valid" time="0.06" steps="94"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
<proof prover="3"><result status="valid" time="0.13"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="93"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.13"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.10"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="93"/></proof>
<proof prover="7"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="MainResultBits" expanded="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.16" steps="128"/></proof>
<goal name="MainResultBits">
<proof prover="1"><result status="valid" time="0.15" steps="132"/></proof>
<proof prover="3"><result status="valid" time="0.55"/></proof>
<proof prover="6"><result status="valid" time="0.16" steps="128"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="MainResultSign" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="104"/></proof>
<goal name="MainResultSign">
<proof prover="1"><result status="valid" time="0.04" steps="102"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.03" steps="104"/></proof>
<proof prover="7"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="Sign_of_xor_j" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<goal name="Sign_of_xor_j">
<proof prover="1"><result status="valid" time="0.04" steps="85"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="96"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.03" steps="96"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="Exp_of_xor_j" expanded="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<goal name="Exp_of_xor_j">
<proof prover="1"><result status="valid" time="1.53" steps="498"/></proof>
<proof prover="2"><result status="valid" time="0.63"/></proof>
<proof prover="3"><result status="valid" time="0.69"/></proof>
<proof prover="4"><result status="valid" time="2.62"/></proof>
<proof prover="3"><result status="valid" time="0.65"/></proof>
<proof prover="4"><result status="valid" time="0.87"/></proof>
<proof prover="5"><result status="valid" time="3.00"/></proof>
<proof prover="7"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="Mantissa_of_xor_j" expanded="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<goal name="Mantissa_of_xor_j">
<proof prover="2"><result status="valid" time="0.67"/></proof>
<proof prover="3"><result status="valid" time="0.72"/></proof>
<proof prover="4"><result status="valid" time="2.69"/></proof>
<proof prover="3"><result status="valid" time="0.66"/></proof>
<proof prover="4"><result status="valid" time="0.72"/></proof>
<proof prover="5"><result status="valid" time="2.69"/></proof>
<proof prover="7"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="MainResultZero" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<goal name="MainResultZero">
<proof prover="1"><result status="valid" time="0.07" steps="104"/></proof>
<proof prover="2"><result status="valid" time="1.36"/></proof>
<proof prover="3"><result status="valid" time="0.94"/></proof>
<proof prover="4"><result status="valid" time="3.15"/></proof>
<proof prover="5" timelimit="6"><result status="valid" time="1.20" steps="142"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.94"/></proof>
<proof prover="5"><result status="valid" time="3.57"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="1.20" steps="142"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="sign_neg" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="5" timelimit="9"><result status="valid" time="0.07" steps="124"/></proof>
<goal name="sign_neg">
<proof prover="1"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="6" timelimit="9"><result status="valid" time="0.07" steps="124"/></proof>
<proof prover="7"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="MainResult" expanded="true">
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="1.44"/></proof>
<goal name="MainResult">
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="2.42"/></proof>
<proof prover="1"><result status="valid" time="2.27" steps="326"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
theory TestBV
use import int.Int
use import bv.BV32
constant b0000 : t = of_int 0b0000
constant b0001 : t = of_int 0b0001
constant b0010 : t = of_int 0b0010
constant b0011 : t = of_int 0b0011
constant b0110 : t = of_int 0b0110
constant b0101 : t = of_int 0b0101
constant b0111 : t = of_int 0b0111
constant b1100 : t = of_int 0b1100
constant b11100 : t = of_int 0b11100
constant b0000 : t = of_int_const 0b0000
constant b0001 : t = of_int_const 0b0001
constant b0010 : t = of_int_const 0b0010
constant b0011 : t = of_int_const 0b0011
constant b0110 : t = of_int_const 0b0110
constant b0101 : t = of_int_const 0b0101
constant b0111 : t = of_int_const 0b0111
constant b1100 : t = of_int_const 0b1100
constant b11100 : t = of_int_const 0b11100
goal g1 : bw_and b0011 b0110 = b0010
goal f1 : bw_and b0011 b0110 = b0011
......@@ -21,14 +20,14 @@ theory TestBV
goal f2 : bw_or b0011 b0110 = b0110
goal g3 : bw_xor b0011 b0110 = b0101
goal g4 : bw_not b0011 = (of_int 0xFFFFFFFC)
goal g4 : bw_not b0011 = (of_int_const 0xFFFFFFFC)
goal g3a : lsr b0111 2 = b0001
goal g3b : lsr ones 31 = b0001
goal g3c : lsr ones 0x100000001 = (of_int 0x7FFFFFFF)
goal g3c : lsr ones 0x100000001 = (of_int_const 0x7FFFFFFF)