Nikolaj Bjorner
|
f20e95184e
|
remove old_simplify dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-28 13:29:51 -07:00 |
|
Nikolaj Bjorner
|
9e4b2a6795
|
port simplifications on bv2int
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-28 02:55:50 -07:00 |
|
Nikolaj Bjorner
|
0ebb917268
|
complement regular expressions when used in negated membership constraints #1224
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-28 01:40:15 -07:00 |
|
Nikolaj Bjorner
|
974eaab01c
|
complement regular expressions when used in negated membership constraints #1224
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-28 01:38:23 -07:00 |
|
Nikolaj Bjorner
|
8542e4ae3d
|
add pre-processing simplificaiton of power to the legacy simplifier Fixes #1237
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-28 00:05:53 -07:00 |
|
Nikolaj Bjorner
|
5db349f6fa
|
raise an exception if trying proof generation for the SAT solver. Stackoverflow question https://stackoverflow.com/questions/45885321/check-function-while-qf-fd-logic-is-set-throws-accessviolationexception
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 23:52:27 -07:00 |
|
Nikolaj Bjorner
|
03f263b974
|
update names
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 13:02:59 -07:00 |
|
Nikolaj Bjorner
|
623cd5ded2
|
fix naming for functions #1223
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 13:00:43 -07:00 |
|
Nikolaj Bjorner
|
f76815a009
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 12:55:55 -07:00 |
|
Nikolaj Bjorner
|
f9dc6385b2
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 12:19:24 -07:00 |
|
Nikolaj Bjorner
|
ce8443581d
|
add API methods for creating and modifying models, #1223
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 12:15:27 -07:00 |
|
Nikolaj Bjorner
|
3bfc3437f1
|
purify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 11:57:13 -07:00 |
|
Nikolaj Bjorner
|
d940516df3
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 11:01:45 -07:00 |
|
Nikolaj Bjorner
|
2ede4b2c80
|
fixes based on regression tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 09:31:16 -07:00 |
|
Nikolaj Bjorner
|
809a4efc6b
|
removing dependencies on simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 11:24:19 -07:00 |
|
Nikolaj Bjorner
|
bcf229dcfd
|
removing dependencies on simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 11:23:41 -07:00 |
|
Nikolaj Bjorner
|
82a937d1af
|
enforce arithmetic normalization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 10:41:25 -07:00 |
|
Nikolaj Bjorner
|
0d5cfe9292
|
separate out, add copy constructor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 09:23:15 -07:00 |
|
Nikolaj Bjorner
|
2955b0c2ef
|
removing more dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 03:05:34 -07:00 |
|
Nikolaj Bjorner
|
ce3ab6b170
|
mising files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 02:04:59 -07:00 |
|
Nikolaj Bjorner
|
e3e965883f
|
mising files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 01:55:03 -07:00 |
|
Nikolaj Bjorner
|
9b53646a34
|
mising files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 01:43:06 -07:00 |
|
Nikolaj Bjorner
|
14e6b5b500
|
mising files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 01:38:55 -07:00 |
|
Nikolaj Bjorner
|
c03be16039
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 01:33:19 -07:00 |
|
Nikolaj Bjorner
|
5371315f4c
|
remove simplify dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 00:57:44 -07:00 |
|
Nikolaj Bjorner
|
881f90d17d
|
remove simplify dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 00:48:49 -07:00 |
|
Nikolaj Bjorner
|
2897b98ed2
|
remove simplify dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 00:37:22 -07:00 |
|
Nikolaj Bjorner
|
b16a4ac452
|
remove simplify dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-25 23:57:10 -07:00 |
|
Nikolaj Bjorner
|
d3c00181ba
|
remove simplify dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-25 23:56:31 -07:00 |
|
Nikolaj Bjorner
|
ac0bb6a3d0
|
remove simplify dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-25 23:56:09 -07:00 |
|
Nikolaj Bjorner
|
9438ff848f
|
moved files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-25 17:44:57 -07:00 |
|
Nikolaj Bjorner
|
ebcacaa26d
|
update new assertions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-25 17:44:33 -07:00 |
|
Christoph M. Wintersteiger
|
b8a81bcb09
|
Added unsat core support to the macro-finder.
|
2017-08-25 20:21:57 +01:00 |
|
Christoph M. Wintersteiger
|
31496b6625
|
Whitespace
|
2017-08-25 15:29:29 +01:00 |
|
Christoph M. Wintersteiger
|
3e0926fb82
|
Whitespace
|
2017-08-25 15:23:25 +01:00 |
|
Christoph M. Wintersteiger
|
36dd2b6530
|
Re-enabled macro-related options for the smt_context
|
2017-08-25 15:01:54 +01:00 |
|
Christoph M. Wintersteiger
|
799fb4a0d1
|
Revert "Eliminated the dependency of the macro-finder on the simplifier."
This reverts commit 8310b24c52.
|
2017-08-24 21:26:09 +01:00 |
|
Christoph M. Wintersteiger
|
8310b24c52
|
Eliminated the dependency of the macro-finder on the simplifier.
|
2017-08-24 20:34:11 +01:00 |
|
Christoph M. Wintersteiger
|
ed8c11ff76
|
Whitespace
|
2017-08-24 19:59:38 +01:00 |
|
Nikolaj Bjorner
|
5141477809
|
remove dead code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-24 11:16:48 -07:00 |
|
Nikolaj Bjorner
|
23d1c0a9a8
|
move pull/push files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-24 11:13:01 -07:00 |
|
Christoph M. Wintersteiger
|
227e6801c2
|
Whitespace
|
2017-08-24 18:33:21 +01:00 |
|
Christoph M. Wintersteiger
|
ed4477c9e4
|
Whitespace
|
2017-08-24 18:32:50 +01:00 |
|
Nikolaj Bjorner
|
a7bb41fd49
|
fix build issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-24 09:19:35 -07:00 |
|
Christoph M. Wintersteiger
|
4252d7f5f9
|
Merge pull request #1232 from johnduck/master
Bugfix: get_objectives in ML API
|
2017-08-24 12:24:44 +01:00 |
|
Sangwoo Joh
|
5845958986
|
Bugfix: get_objectives in ML API
|
2017-08-24 18:17:47 +09:00 |
|
Nikolaj Bjorner
|
8b2d60e3ca
|
using rewrite in push_app_ite
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-23 17:57:03 -07:00 |
|
Nikolaj Bjorner
|
f91496f5ff
|
pruning simplifier dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-23 16:56:55 -07:00 |
|
Nikolaj Bjorner
|
8ff8470809
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2017-08-23 16:33:54 -07:00 |
|
Nikolaj Bjorner
|
7dd28781ab
|
remove simplifier dependencies from cmakelist.txt files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-23 16:33:36 -07:00 |
|