aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SolverInterface.h
Commit message (Collapse)AuthorAgeFilesLines
* Sort includes in libsolidity/formalLeonardo Alt2018-12-181-4/+2
|
* [SMTChecker] Support to mappingLeonardo Alt2018-12-141-3/+12
|
* [SMTChecker] Make smt::Sort::operator== virtualLeonardo Alt2018-11-301-6/+16
|
* Fix move bug.chriseth2018-11-291-1/+2
|
* Inject SMTLIB2 queries and responses via standard-json-io.chriseth2018-11-231-0/+3
|
* Stylechriseth2018-11-231-7/+9
|
* [SMTChecker] Add ArraySort and array operationsLeonardo Alt2018-11-221-2/+49
|
* [SMTChecker] Add FunctionSort and refactors the solver interface to create ↵Leonardo Alt2018-11-221-21/+29
| | | | variables
* Isolating files shared between Yul- and Solidity language frontend.Christian Parpart2018-11-221-1/+1
|
* [SMTChecker] Refactor smt::Sort and its usageLeonardo Alt2018-11-211-60/+48
|
* [SMTChecker] Implement uninterpreted functions and use it for blockhash()Leonardo Alt2018-11-151-13/+14
|
* Retained move/copy semantics; removed const qualifier from Expression's ↵Bhargava Shastry2018-10-171-2/+4
| | | | members name (of type std::string) and arguments (of type std::vector<Expression>)
* Fix compiler warning: clang-8 warns of explicitly-defined op implicitly ↵Bhargava Shastry2018-10-171-2/+0
| | | | deleted for Expression object's copy and move constructors
* [SMTChecker] Add CheckResult::CONFLICTINGLeonardo Alt2018-07-271-1/+1
|
* [SMTChecker] SMTPortfolio: use all SMT solvers availableLeonardo Alt2018-07-271-3/+9
|
* Setting timeout to Z3 and CVC4Leonardo Alt2018-07-271-1/+4
|
* Add virtual destructors on base classes.Alexander Arlt2018-05-021-0/+1
|
* [SMTChecker] Integration with CVC4Leonardo Alt2018-04-171-0/+20
|
* [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests.Leonardo Alt2018-03-131-6/+23
|
* [SMTChecker] Support to Bool variablesLeonardo Alt2018-03-131-5/+10
|
* [SMTChecker] Keep track of current path conditionsLeonardo Alt2017-12-141-0/+5
|
* Unary operators and division.chriseth2017-11-301-0/+4
|
* Explain IntIntFun and merge assertion.chriseth2017-11-241-3/+7
|
* Introduce sorts for smt expressions.chriseth2017-11-221-31/+35
|
* Check for conditions being constant.chriseth2017-11-221-0/+1
|
* Remove parameter names for defaulted functions.chriseth2017-08-311-4/+4
|
* Review changes.chriseth2017-08-231-1/+1
|
* Partial support for if statements.chriseth2017-08-231-0/+7
|
* Refactor Z3 read callback.chriseth2017-08-231-2/+5
|
* Insert abstraction layer.chriseth2017-08-231-0/+168
generated by cgit (git 2.34.1) at 2024-11-18 14:08:04 +0800