214 Commits

Author	SHA1	Message	Date
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	6c749fdbfe	Pretty-print enums in Z3 model [skip ci]	2022-01-14 19:23:26 +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	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
Aymeric Fromherz	1932277c80	Fix printing of negative money amounts [skip ci]	2022-01-14 11:45:47 +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	977e985e4c	Encode dates to Z3 [skip ci]	2022-01-14 01:54:33 +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
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	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
Aymeric Fromherz	f342c89482	[skip ci] Z3encoding: proper error message for ill-formed unary operators	2022-01-12 19:15:51 +01:00
Aymeric Fromherz	29ed4ff696	[skip ci] Z3encoding: refer to Catala source code variable names when printing a model	2022-01-12 19:09:20 +01:00
Aymeric Fromherz	297b7ec604	[skip ci] Z3encoding: documenting the function style for the context	2022-01-12 19:02:56 +01:00
Aymeric Fromherz	83e83507ed	[skip ci] Z3encoding: Passing the context around to preserve dynamic updates throughout the VC encoding	2022-01-12 18:59:01 +01:00
Aymeric Fromherz	e66730bdd5	[skip ci] Start improving model prettyprinting	2022-01-12 18:35:36 +01:00
Aymeric Fromherz	a7ad86233e	[skip ci] document Z3encoding context type	2022-01-12 18:23:50 +01:00
Aymeric Fromherz	862af7a3d8	[skip ci] Pretty-print simple Z3 models when a VC is not satisfied	2022-01-12 18:15:09 +01:00
Aymeric Fromherz	45dc3faeed	[skip ci] minor refactor: prepare to parse Z3 model	2022-01-12 17:55:32 +01:00
Aymeric Fromherz	0e59cff1ed	[skip ci] print Z3 model when verification is failing	2022-01-12 17:51:28 +01:00
Aymeric Fromherz	9995837564	[skip ci] Z3encoding: support function calls	2022-01-12 17:38:12 +01:00
Denis Merigoux	78b1fe08f4	[skip ci] Always name of the variable on the left	2022-01-12 16:56:05 +01:00
Denis Merigoux	6d06f9c81c	Prettified error messages	2022-01-12 16:50:10 +01:00
Aymeric Fromherz	2a8f7f7c07	[skip ci] remove all logs before encoding query to z3	2022-01-12 16:30:00 +01:00
Aymeric Fromherz	d455e29978	[skip ci] Z3encoding: obtain type of bound variables	2022-01-12 15:58:19 +01:00
Denis Merigoux	c7b225bad5	Add types of free variables in VC [skip ci]	2022-01-12 15:52:44 +01:00
Aymeric Fromherz	7f3e59f7b0	[skip ci] Z3encoding: more debug information when encoding fails	2022-01-12 15:21:13 +01:00
Aymeric Fromherz	8bb8053580	[skip ci] Z3 encoding: Better split output between debug and non-debug information	2022-01-12 14:43:17 +01:00
Aymeric Fromherz	3c6f9d9174	[skip ci] formatting + slight refactor for better error messages during Z3 verification	2022-01-12 14:20:52 +01:00
Aymeric Fromherz	b11c76404f	[skip ci] Spawn one query per VC and correctly encode VC by negating it	2022-01-12 14:08:35 +01:00
Aymeric Fromherz	e10a25876f	[skip ci] Print Z3 encoding information as debug information only	2022-01-12 13:58:38 +01:00
Aymeric Fromherz	1c8f9c31f5	Z3 encoding: Add missing Lte for integers	2022-01-12 12:16:54 +01:00
Denis Merigoux	260959b088	Formatting + correct expected tests output	2022-01-11 18:33:45 +01:00
Aymeric Fromherz	20cc0795f9	Arithmetic binary operators	2022-01-11 17:54:02 +01:00
Aymeric Fromherz	f642bfe4be	Z3 encoding: More binary operators, pass more tests	2022-01-11 17:49:02 +01:00
Denis Merigoux	83bdd0b632	Test base for verification conditions encoding	2022-01-11 16:13:34 +01:00
Denis Merigoux	d705334d9e	Merge branch 'master' into proof_platform	2022-01-11 15:43:33 +01:00
Alain	5c5bc77c87	formatting (sorry, problem with the makefile)	2022-01-10 17:53:48 +01:00
Alain	5bc9a36308	vc generation for conflict errors	2022-01-10 17:30:19 +01:00
Alain	e8dbaaec47	add not to z3encoding	2022-01-10 17:30:08 +01:00
Alain	0c2dbdddd1	correct typo in vc generation for conflict error ... add some debug in comments	2022-01-10 17:29:53 +01:00
Alain	8a0a4c7603	naive verification condition for conflicts	2022-01-10 16:25:20 +01:00
Aymeric Fromherz	4b47f7fd9a	More binary operators encoding, some boolean examples now passing	2022-01-10 14:53:58 +01:00
Aymeric Fromherz	b9b593a361	Encode some basic types to Z3	2022-01-10 14:51:36 +01:00
Aymeric Fromherz	0455029951	Z3: Start encoding Catala types as Z3 sorts	2022-01-10 14:50:50 +01:00
Aymeric Fromherz	bc4608755a	Z3: Encode EVar node	2022-01-10 14:46:41 +01:00
Aymeric Fromherz	2d036f9925	Add ctx_var to z3encoding context	2022-01-10 14:37:17 +01:00
Aymeric Fromherz	a9ebfaed38	Pass program to z3encoder	2022-01-10 14:36:15 +01:00
Denis Merigoux	50719911f8	Added TODOs	2022-01-10 13:48:00 +01:00
Denis Merigoux	04cc274d3e	Print term for error message	2022-01-10 11:52:48 +01:00
Denis Merigoux	4082e5056e	More prettier things	2022-01-10 10:59:30 +01:00
Denis Merigoux	3a864b6160	Aesthetic improvements	2022-01-10 10:28:14 +01:00
Denis Merigoux	ad4218285d	Working partial evaluation for Dcalc using ugly but correct style	2022-01-09 19:16:34 +01:00
Denis Merigoux	743a1b74c9	Renamed and grouped modules cleanly	2022-01-08 18:37:04 +01:00