Leonardo de Moura
|
91c65178c7
|
fixed compilation bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-24 14:48:45 -07:00 |
|
Leonardo de Moura
|
4cf211acd4
|
moving tactics to tactic folder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-24 14:15:15 -07:00 |
|
Leonardo de Moura
|
4f6b34bc7b
|
removing last refs to assertion_set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-24 14:04:33 -07:00 |
|
Leonardo de Moura
|
96676efeb6
|
had to nuke mip_tactic, it was based on the smt_solver_exp (experimental), that depends on assertion_sets. This change will affect Z3's performance on QF_LIA and QF_LRA benchmarks. The new mcsat should fix that.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-24 13:58:24 -07:00 |
|
Leonardo de Moura
|
361b55edfd
|
Minimizing dependencies to assertion_set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-24 13:33:54 -07:00 |
|
Leonardo de Moura
|
3da69a4f1b
|
Integrated structured branch into unstable branch (the official 'working in progress' branch)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-24 13:19:19 -07:00 |
|
Leonardo de Moura
|
69ce24a6ce
|
checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-24 11:11:07 -07:00 |
|
Leonardo de Moura
|
0a4446ae26
|
reorganizing the code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-23 22:14:35 -07:00 |
|
Leonardo de Moura
|
56ab7a7495
|
checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-21 18:12:34 -07:00 |
|
Leonardo de Moura
|
6bdb009c3e
|
Reorganizing the code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-20 20:42:28 -07:00 |
|
Leonardo de Moura
|
ded42feeb6
|
Reorganizing code base
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-20 16:33:01 -07:00 |
|