1372 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Denis Merigoux	777f194178	.mlis and ocamldoc [skip-ci]	2022-01-18 15:13:16 +01:00
Aymeric Fromherz	661b30f638	Add bad tests for date_get_year	2022-01-17 15:05:06 +01:00
Aymeric Fromherz	c7fd00702a	Fix good get year test + reset [skip ci]	2022-01-17 15:04:05 +01:00
Aymeric Fromherz	400a777891	Support common case for getYear: Comparison against a literal [skip ci]	2022-01-17 15:02:56 +01:00
Aymeric Fromherz	cf63e4f3d3	Restore pretty-printing of enum model [skip ci]	2022-01-14 21:10:34 +01:00
Aymeric Fromherz	2548b4ad5e	Pretty-print structs, temporarily disable pretty-printing of enum model during refactoring [skip ci]	2022-01-14 21:02:34 +01:00
Aymeric Fromherz	271d20dcaf	todo outputs for bad struct tests [skip ci]	2022-01-14 20:42:06 +01:00
Aymeric Fromherz	ede73501d6	Add bad struct tests [skip ci]	2022-01-14 20:41:03 +01:00
Aymeric Fromherz	8b1c2d0891	reset test [skip ci]	2022-01-14 20:38:11 +01:00
Aymeric Fromherz	0b011a5e3a	Support TTuple type [skip ci]	2022-01-14 20:37:45 +01:00
Aymeric Fromherz	7fa271b9f4	Construct Z3 sort corresponding to a struct [skip ci]	2022-01-14 20:35:22 +01:00
Aymeric Fromherz	89e41b3a33	Encode ETupleAccess node [skip ci]	2022-01-14 20:17:27 +01:00
Aymeric Fromherz	850718be17	Add support for structs in the Z3 encoding context [skip ci]	2022-01-14 20:08:42 +01:00
Aymeric Fromherz	9684e14b1b	reset tests [skip ci]	2022-01-14 19:24:20 +01:00
Aymeric Fromherz	6c749fdbfe	Pretty-print enums in Z3 model [skip ci]	2022-01-14 19:23:26 +01:00
Aymeric Fromherz	a128a188ee	reset [skip ci]	2022-01-14 19:05:58 +01:00
Aymeric Fromherz	9727acc788	more tests [skip ci]	2022-01-14 19:04:23 +01:00
Aymeric Fromherz	38b4912161	Reset test [skip ci]	2022-01-14 19:02:59 +01:00
Aymeric Fromherz	06b845316d	Allow match bodies in VCs to refer to the value corresponding to the destructed enum [skip ci]	2022-01-14 19:01:54 +01:00
Aymeric Fromherz	867fc46515	Add more complex enum test [skip ci]	2022-01-14 19:01:23 +01:00
Aymeric Fromherz	cc026e35b3	Add negative tests for enums	2022-01-14 18:37:32 +01:00
Aymeric Fromherz	d7563c229e	Reset test [skip ci]	2022-01-14 18:34:58 +01:00
Aymeric Fromherz	3c21182dea	Finish encoding arms of EMatch in VCs [skip ci]	2022-01-14 18:33:56 +01:00
Aymeric Fromherz	a7abe630e7	More progress towards encoding arms of EMatch in VCs [skip ci]	2022-01-14 18:24:32 +01:00
Aymeric Fromherz	ffee0d815d	Wrap up the find_or_create_enum function [skip ci]	2022-01-14 17:42:12 +01:00
Aymeric Fromherz	7c1e808880	Translate the type TEnum to Z3	2022-01-14 17:42:12 +01:00
Aymeric Fromherz	a1e12a22b1	Create or retrieve Z3 enum types [skip ci]	2022-01-14 17:42:12 +01:00
Aymeric Fromherz	ae0935f035	Z3 encoding: Add a map from enumnames to Z3 sorts to the context [skip ci]	2022-01-14 17:42:12 +01:00
Denis Merigoux	08591fd178	Add link to demo	2022-01-14 16:52:30 +01:00
Aymeric Fromherz	1932277c80	Fix printing of negative money amounts [skip ci]	2022-01-14 11:45:47 +01:00
Aymeric Fromherz	abba635047	Add build_dev Makefile target to avoid reformatting during development cycles [skip ci]	2022-01-14 11:25:37 +01:00
Aymeric Fromherz	7ca0ca4012	Reset bad dates examples with expected outputs [skip ci]	2022-01-14 02:09:20 +01:00
Aymeric Fromherz	951e50637f	Actually plug date pretty printing into Z3 encoding [skip ci]	2022-01-14 02:08:04 +01:00
Aymeric Fromherz	50ad5e3044	Print dates generated by Z3 model [skip ci]	2022-01-14 02:04:55 +01:00
Aymeric Fromherz	59e36d2750	Reset good dates simple test [skip ci]	2022-01-14 01:56:07 +01:00
Aymeric Fromherz	977e985e4c	Encode dates to Z3 [skip ci]	2022-01-14 01:54:33 +01:00
Aymeric Fromherz	c8be75ca75	Z3encoding: Add bad tests related to dates [skip ci]	2022-01-13 20:28:28 +01:00
Aymeric Fromherz	52f33aa1ae	Fix good date example [skip ci]	2022-01-13 20:25:16 +01:00
Aymeric Fromherz	a6c88b103f	Reset bad money tests [skip ci]	2022-01-13 20:13:12 +01:00
Aymeric Fromherz	28935c689d	Reset good money test [skip ci]	2022-01-13 20:12:28 +01:00
Aymeric Fromherz	a15fb872ef	Fix money tests [skip ci]	2022-01-13 20:11:42 +01:00
Aymeric Fromherz	d89eea0481	Encode comparison operators on money [skip ci]	2022-01-13 20:11:28 +01:00
Aymeric Fromherz	827f5cb916	encode money to Z3 [skip ci]	2022-01-13 20:02:14 +01:00
Aymeric Fromherz	50d0ee0909	Start printing z3 model results according to their type [skip ci]	2022-01-13 19:52:58 +01:00
Aymeric Fromherz	69e34b4ae7	Negative tests for money [skip ci]	2022-01-13 19:34:34 +01:00
Denis Merigoux	428ae95c62	[skip ci] Added a walkthrough example for ProLaLa + tweaked tests output order of vcs	2022-01-13 16:58:43 +01:00
Denis Merigoux	496775b148	Dates and money tests	2022-01-13 16:20:43 +01:00
Denis Merigoux	5a6f4485e7	Matching subscope variables also [skip ci]	2022-01-13 16:00:09 +01:00
Denis Merigoux	a9454a0aac	Correctly match ignored part of expressions in VC generation [skip ci]	2022-01-13 12:15:37 +01:00
Denis Merigoux	bf444f548f	Error message pretty-printing and sat solving example [skip ci]	2022-01-13 10:46:23 +01:00