Commit Graph

19 Commits

Author SHA1 Message Date
Bhargava Shastry
67fd3ca4a7 Retained move/copy semantics; removed const qualifier from Expression's members name (of type std::string) and arguments (of type std::vector<Expression>) 2018-10-17 16:46:18 +02:00
Bhargava Shastry
546b08c158 Fix compiler warning: clang-8 warns of explicitly-defined op implicitly deleted for Expression object's copy and move constructors 2018-10-17 16:42:51 +02:00
Leonardo Alt
55c1fb60b4 [SMTChecker] Add CheckResult::CONFLICTING 2018-07-27 16:16:26 +01:00
Leonardo Alt
87a38e1abe [SMTChecker] SMTPortfolio: use all SMT solvers available 2018-07-27 16:15:34 +01:00
Leonardo Alt
b356f6a7f9 Setting timeout to Z3 and CVC4 2018-07-27 16:01:48 +02:00
Alexander Arlt
f94b793472 Add virtual destructors on base classes. 2018-05-02 13:29:16 +02:00
Leonardo Alt
ae3350ae03 [SMTChecker] Integration with CVC4 2018-04-17 12:26:58 +01:00
Leonardo Alt
c2d26eb6a2 [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests. 2018-03-12 20:16:47 +01:00
Leonardo Alt
6a940f0a99 [SMTChecker] Support to Bool variables 2018-03-12 20:16:47 +01:00
Leonardo Alt
2af4d7c7dd [SMTChecker] Keep track of current path conditions 2017-12-13 17:39:10 +01:00
chriseth
19e067465a Unary operators and division. 2017-11-30 01:20:21 +01:00
chriseth
0e2a9658d2 Explain IntIntFun and merge assertion. 2017-11-23 19:02:47 +01:00
chriseth
762d591a47 Introduce sorts for smt expressions. 2017-11-22 15:20:26 +01:00
chriseth
22c689d516 Check for conditions being constant. 2017-11-22 02:35:34 +00:00
chriseth
9e63710b8e Remove parameter names for defaulted functions. 2017-08-31 12:16:41 +02:00
chriseth
cf5e1d6120 Review changes. 2017-08-23 17:37:35 +02:00
chriseth
75f09f2a84 Partial support for if statements. 2017-08-23 17:37:35 +02:00
chriseth
1e05ebe50e Refactor Z3 read callback. 2017-08-23 17:37:35 +02:00
chriseth
4cea3d4aa4 Insert abstraction layer. 2017-08-23 17:37:35 +02:00