13 Commits

Author	SHA1	Message	Date
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	a51577facf	Fix Windows build	2019-09-02 22:37:30 +02:00
Leonardo Alt	ed275fd760	[SMTChecker] Collect assertions in EncodingContext	2019-06-24 15:03:00 +02:00
Leonardo Alt	31ef421fff	[SMTChecker] Keep a copy of assertions that are added to the solvers	2019-06-04 17:09:04 +02:00
Leonardo Alt	c8a017ccd6	[SMTChecker] Use unique_ptr instead of shared_ptr where applicable.	2019-05-09 16:34:22 +02:00
Leonardo Alt	9a33367bc6	[SMTChecker] Warn when no solver was found and there are unhandled queries.	2019-01-29 14:29:07 +01:00
Leonardo Alt	cce377833a	Sort includes in libsolidity/formal	2018-12-17 18:26:10 +01:00
chriseth	bb10be789c	Inject SMTLIB2 queries and responses via standard-json-io.	2018-11-23 09:43:49 +01:00
Leonardo Alt	13a142b039	[SMTChecker] Add FunctionSort and refactors the solver interface to create variables	2018-11-22 10:04:04 +01: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	87a38e1abe	[SMTChecker] SMTPortfolio: use all SMT solvers available	2018-07-27 16:15:34 +01:00