30 Commits

Author	SHA1	Message	Date
Alexander Arlt	aac7a1e434	Apply modernize-pass-by-value.	2020-04-14 10:32:13 -05:00
Leonardo Alt	5d9dd654cf	[SMTChecker] Add and use tuple sort	2020-04-08 18:26:03 +02:00
Christian Parpart	345f9928ab	Library libdevcore renamed to libsolutil.	2020-01-07 15:51:50 +01:00
Christian Parpart	6b23412fae	C++ namespace cleanup (except tests).	2020-01-07 15:51:50 +01:00
Leonardo Alt	ddc478e3e4	Add CallbackKind and use it for the SMT solver	2019-11-21 22:10:21 +00:00
Leonardo Alt	6b10efff8c	Add CHCSmtLib2Interface	2019-11-07 11:12:11 +01:00
Leonardo Alt	ed9674be8d	[SMTChecker] Add as const function to SMTLib2Interface	2019-09-18 22:57:14 +02:00
Leonardo Alt	a51577facf	Fix Windows build	2019-09-02 22:37:30 +02:00
Leonardo Alt	a774b2d905	[SMTChecker] Zero-initialize arrays	2019-09-02 22:37:30 +02:00
Leonardo Alt	cce377833a	Sort includes in libsolidity/formal	2018-12-17 18:26:10 +01:00
Leonardo Alt	f3c2309c73	Display better error message in SMTLib2	2018-11-23 09:43:49 +01:00
chriseth	bb10be789c	Inject SMTLIB2 queries and responses via standard-json-io.	2018-11-23 09:43:49 +01:00
Leonardo Alt	20accf1a90	[SMTChecker] Add ArraySort and array operations	2018-11-22 14:04:20 +01:00
Leonardo Alt	13a142b039	[SMTChecker] Add FunctionSort and refactors the solver interface to create variables	2018-11-22 10:04:04 +01:00
Christian Parpart	87821c53c3	Isolating files shared between Yul- and Solidity language frontend.	2018-11-21 18:58:12 +00:00
Leonardo Alt	01ce43e51b	[SMTChecker] Refactor smt::Sort and its usage	2018-11-21 15:46:47 +01:00
Leonardo Alt	70bb0eaf95	[SMTChecker] Implement uninterpreted functions and use it for blockhash()	2018-11-15 09:12:42 +01:00
Leonardo Alt	f249f9c86f	[SMTLib2] Fix repeated declarations	2018-07-27 17:34:44 +01:00
Alex Beregszaszi	dea0567e06	Fix unterminated parentheses typo in SMTLib2 ... Found by @leonardoalt	2018-07-27 17:33:53 +01:00
Leonardo Alt	87a38e1abe	[SMTChecker] SMTPortfolio: use all SMT solvers available	2018-07-27 16:15:34 +01:00
Leonardo Alt	06dbcb3afe	Only ask for a model if it's SAT	2018-07-27 14:13:22 +02:00
chriseth	762d591a47	Introduce sorts for smt expressions.	2017-11-22 15:20:26 +01:00
Alex Beregszaszi	18ae0c3d78	SMT enforce variable types	2017-10-05 12:29:20 +01:00
chriseth	cf5e1d6120	Review changes.	2017-08-23 17:37:35 +02:00
chriseth	1e05ebe50e	Refactor Z3 read callback.	2017-08-23 17:37:35 +02:00
chriseth	9ac2ac14c1	Rename read file callback.	2017-08-23 17:37:35 +02:00
chriseth	4cea3d4aa4	Insert abstraction layer.	2017-08-23 17:37:35 +02:00
chriseth	b3f8ed457a	Cleanup.	2017-08-23 14:24:30 +02:00
chriseth	39fc798999	Use file to communicate with z3.	2017-08-23 14:24:05 +02:00
chriseth	df848859da	Rewrite using SMTLIB2 interface.	2017-08-23 14:24:05 +02:00