ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
lri-master
why3/drivers
History
Paul Bonnot 8d15db6d7b Removed propositions that confuse the prover
2023-01-05 15:17:03 +01:00
..
alt_ergo_2_2_0.drv
Resolve "Add support for Alt-Ergo 2.4.0"
2021-02-05 14:46:11 +01:00
alt_ergo_2_3.drv
Resolve "Add support for Alt-Ergo 2.4.0"
2021-02-05 14:46:11 +01:00
alt_ergo_common.drv
Fix step detection regexp of Alt-Ergo
2022-08-03 12:45:21 +00:00
alt_ergo_fp.drv
Add an alternative "FPA" to Alt-Ergo, supporting dedicated reasoning on floating-point and real numbers
2022-11-03 08:47:46 +00:00
alt_ergo_model.drv
cosmetic changes in drivers
2016-03-08 17:03:35 +01:00
alt_ergo_smt2.drv
cosmetic changes in drivers
2016-03-08 17:03:35 +01:00
alt_ergo.drv
more renaming
2022-07-07 08:51:40 +02:00
beagle.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
colibri2.drv
Remove simplify_trivial_quantification from colibri drivers
2022-10-04 09:29:13 +02:00
colibri.drv
Remove simplify_trivial_quantification from colibri drivers
2022-10-04 09:29:13 +02:00
coq-common.gen
Use plain identifiers whenever possible in the Coq printer.
2019-03-05 06:35:41 +01:00
coq-realize.drv
[Realization] The realizations ask to prove that the coq driver is correct
2013-01-29 14:25:13 +01:00
coq-ssreflect.drv
Support for multi-line strings. Drivers updated accordingly.
2019-10-21 14:13:59 +02:00
coq.drv
Remove support for Coq 8.3.
2014-03-13 08:39:17 +01:00
cvc3.drv
Merge branch 'master' into new_system
2017-04-14 17:45:25 +02:00
cvc4_14.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
cvc4_15_counterexample.drv
support for CVC4 1.6 finalized
2018-07-05 16:52:29 +02:00
cvc4_15.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
cvc4_16_counterexample.drv
support for CVC4 1.6 finalized
2018-07-05 16:52:29 +02:00
cvc4_16.drv
Drivers updated - string theory is not mapped to CVC4 1.6
2019-11-06 13:55:34 +01:00
cvc4_16.gen
more renaming
2022-07-07 08:51:40 +02:00
cvc4_17_counterexample.drv
CVC4 strings-counterexample prover
2020-04-01 17:09:06 +01:00
cvc4_17.drv
For CVC4 1.7 do not use --string-exp flag by default
2020-03-26 15:42:33 +01:00
cvc4_18_strings_counterexample.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
cvc4_18_strings.drv
Resolve "Fix drivers for SMT-LIB strings"
2022-04-06 14:29:41 +00:00
cvc4_bv.gen
Add new drivers for z3 and cvc4 to support bitvectors of size 128 and 256
2021-07-12 13:08:49 +02:00
cvc4-realize.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
cvc4.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
cvc5_counterexample.drv
Support for CVC5
2022-06-03 16:30:54 +00:00
cvc5_strings_counterexample.drv
Add support for strings theory with cvc5
2022-08-22 15:58:14 +02:00
cvc5_strings.drv
Add support for strings theory with cvc5
2022-08-22 15:58:14 +02:00
cvc5.drv
Add outofmemory pattern for CVC5
2022-06-07 09:36:41 +02:00
discrimination.gen
Repair discriminate2
2021-04-08 12:26:07 +00:00
dreal.drv
Delete quantifier instantiation transformation
2022-10-25 14:42:29 +02:00
eprover.drv
Properly detect an "unknown" result from eprover.
2016-06-09 13:47:06 +02:00
gappa.drv
Removed propositions that confuse the prover
2023-01-05 15:17:03 +01:00
iprover.drv
change default polymorphism encoding methods
2013-08-06 17:25:04 +02:00
isabelle-common.gen
Adapted to Isabelle2019
2020-03-03 09:58:48 +01:00
isabelle-realize.drv
Use a single Isabelle driver for realizations.
2021-06-29 07:27:35 +02:00
isabelle.drv
Use a single Isabelle driver for realizations.
2021-06-29 07:27:35 +02:00
mathematica.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
mathsat.drv
Merge branch 'master' into new_system
2017-10-03 17:49:58 +02:00
metis.drv
Support for Metis (seems to work) and MetiTarski (does not work)
2013-08-21 13:36:26 +02:00
metitarski.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
no-bv.gen
- Add nth_bv_def and eq_sub_bv_def axioms to bv.BV_Gen and remove nth_bv
2016-01-26 21:35:58 +01:00
polypaver.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
princess.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
psyche.drv
Merge branch 'master' into new_system
2017-10-03 17:49:58 +02:00
pvs-common.gen
fixed 'make bench'
2019-03-07 11:37:41 +01:00
pvs-realize.drv
PVS output revamped (in preparation of forthcoming PVS realizations)
2012-07-11 20:51:49 +02:00
pvs.drv
PVS output revamped (in preparation of forthcoming PVS realizations)
2012-07-11 20:51:49 +02:00
safeprover.drv
fix the newly added theories and drivers
2016-03-07 19:29:07 +01:00
simplify.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
smt-libv2-bv-realization.gen
Add new drivers for z3 and cvc4 to support bitvectors of size 128 and 256
2021-07-12 13:08:49 +02:00
smt-libv2-bv.gen
convert to 128 bit for checks
2021-07-13 16:40:34 +02:00
smt-libv2-floats-gnatprove.gen
minor update of smtlib reserved words
2017-11-22 14:58:42 +01:00
smt-libv2-floats-int_via_bv.gen
Q817-011 proof - use cvc4 for floats
2018-06-01 13:48:34 +02:00
smt-libv2-floats-int_via_real.gen
Q817-011 proof - use cvc4 for floats
2018-06-01 13:48:34 +02:00
smt-libv2-floats.gen
In SMTLIB, "abs" is *not* the absolute value on reals
2020-03-04 09:54:27 +01:00
smt-libv2-gnatprove.gen
Q817-011 proof - use cvc4 for floats
2018-06-01 13:48:34 +02:00
smt-libv2.gen
Remove properties in int.MinMax only for Z3
2020-12-01 15:19:29 +01:00
smtlib-strings.gen
Resolve "Fix drivers for SMT-LIB strings"
2022-04-06 14:29:41 +00:00
spass_types.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
spass.drv
change default polymorphism encoding methods
2013-08-06 17:25:04 +02:00
tptp-tff0.drv
Merge branch 'master' into new_system
2017-10-03 17:49:58 +02:00
tptp-tff1.drv
Merge branch 'master' into new_system
2017-10-03 17:49:58 +02:00
tptp.gen
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
vampire-smt.drv
make transf eliminate_definition aware of the meta for CE tracing
2021-07-15 11:18:57 +02:00
vampire.drv
change default polymorphism encoding methods
2013-08-06 17:25:04 +02:00
verit.drv
make driver mst-libv2 generique since it does not contains printer anymore
2018-07-05 18:45:10 +02:00
why3_smt.drv
make transf eliminate_definition aware of the meta for CE tracing
2021-07-15 11:18:57 +02:00
why3_tptp.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
why3.drv
why3 driver should ignore polymorphism of equality
2016-06-10 15:12:58 +02:00
yices-smt2.drv
make driver mst-libv2 generique since it does not contains printer anymore
2018-07-05 18:45:10 +02:00
yices.drv
Merge branch 'master' into new_system
2017-10-03 17:49:58 +02:00
z3_432.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
z3_440_counterexample.drv
New setting for counterexample generation
2018-05-04 13:39:55 +02:00
z3_440.drv
Resolve "z3 driver should not unfold definitions"
2022-07-09 09:12:15 +00:00
z3_471_counterexample.drv
Drivers updated so strings are only used with solvers that support them
2019-11-05 16:19:09 +01:00
z3_471_nobv.drv
Drivers updated so strings are only used with solvers that support them
2019-11-05 16:19:09 +01:00
z3_471.drv
Drivers updated so strings are only used with solvers that support them
2019-11-05 16:19:09 +01:00
z3_bv.gen
Add new drivers for z3 and cvc4 to support bitvectors of size 128 and 256
2021-07-12 13:08:49 +02:00
z3_smtv1.drv
Merge branch 'master' into new_system
2017-10-03 17:49:58 +02:00
z3.drv
Add comment prelude and outofmemory error for z3 driver
2019-04-15 15:01:09 +02:00
zenon_modulo.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00
zenon.drv
hybrid eliminate_if
2019-01-17 14:09:53 +01:00