mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
10360 commits 49 branches 53 tags 182 MiB
Commit graph

10360 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
e4b595d490 add solver pool abstraction for Spacer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:10:20 -07:00
Murphy Berzish
30f958f291 Merge branch 'upstream-master' into develop 2017-10-28 15:48:04 -04:00
Nikolaj Bjorner
ba53fc1230 fix scc omitting blocked clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-27 17:29:26 -07:00
Nikolaj Bjorner
2a8a28bb59 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-27 15:41:24 -07:00
Nikolaj Bjorner
829c140087 ensure that bca takes also lemmas into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-27 15:40:25 -07:00
Nikolaj Bjorner
5989de1ae3
Merge pull request #8 from TheRealNebus/opt 
Opt
 2017-10-27 12:49:12 -07:00
Miguel Angelo Da Terra Neves
f1bad91609 Clean-up 2017-10-27 12:39:36 -07:00
Miguel Angelo Da Terra Neves
3a05313c67 Python API context fix 2017-10-27 12:36:09 -07:00
Nikolaj Bjorner
c886b6d500 fix #1330. Interpolation transformation needs to handle TRANSITIVITY_STAR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 20:53:10 -07:00
Nikolaj Bjorner
e7aa6455bc fix #1326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 19:25:25 -07:00
Nikolaj Bjorner
0589a20b46 fix #1326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 19:24:45 -07:00
Miguel Angelo Da Terra Neves
8bb2be1fba Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-25 17:08:10 -07:00
Miguel Angelo Da Terra Neves
e1ff6304ed Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-25 17:06:08 -07:00
Nikolaj Bjorner
0919fd4075 fix bca condition for tautology check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 16:46:22 -07:00
Nikolaj Bjorner
ac0202630e fix non-termination bug with retained clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 15:40:11 -07:00
Nikolaj Bjorner
32711790e8 bug fixes reported by Miguel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 13:36:48 -07:00
Nikolaj Bjorner
fc73271b83 more C fixes to model example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 11:20:56 -07:00
Nikolaj Bjorner
7ed32f4315 re-add model example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 10:48:53 -07:00
Nikolaj Bjorner
2c27056283 disable model example pending C compliance or C99 or whatever adjustment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 10:24:49 -07:00
Nikolaj Bjorner
0268f2243e remove ast.h reference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 09:49:53 -07:00
Nikolaj Bjorner
f5f1d019d8 missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 09:00:35 -07:00
Nikolaj Bjorner
7148226823 Merge branch 'master' of https://github.com/z3prover/z3 2017-10-25 08:39:05 -07:00
Nikolaj Bjorner
f2ce68b899 Merge pull request #1324 from delcypher/c_api_construct_model_example 
Add example of using Z3's new model construction C API.
 2017-10-25 08:38:17 -07:00
Dan Liew
de3700e1fd [CMake] Try to unbreak the C example build with older GCC versions 
by forcing the language version to be C99.
 2017-10-25 11:13:25 +01:00
Nikolaj Bjorner
371f0b193c move min_cut, fix #1321 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 02:59:04 -07:00
Nikolaj Bjorner
8acc924c21 ifndef/define match 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 16:34:49 -07:00
Miguel Angelo Da Terra Neves
4d9492176e Removed incremental disabling 2017-10-24 15:19:45 -07:00
Nikolaj Bjorner
b72225d7d0 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 15:16:59 -07:00
Miguel Angelo Da Terra Neves
69c253e8e6 Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-24 14:08:53 -07:00
Miguel Angelo Da Terra Neves
8915d0a21f Tidy 2017-10-24 14:08:44 -07:00
Miguel Angelo Da Terra Neves
80041d7131 Fixed infinite loop bugs in blocked clause retention. Added option to 
disable incremental sat solver
 2017-10-24 13:51:27 -07:00
Nikolaj Bjorner
ee320fa025 fix build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 13:32:40 -07:00
Nikolaj Bjorner
31dfc0c610 fix build, fix #1322 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 13:20:19 -07:00
Nikolaj Bjorner
6300a78b82 more build errors in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 12:57:30 -07:00
Nikolaj Bjorner
48d144a6dd missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 12:51:47 -07:00
Nikolaj Bjorner
db65cc007a move more proof utils 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 10:27:48 -07:00
Nikolaj Bjorner
fc822af707 move proof utils under ast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 09:59:55 -07:00
Nikolaj Bjorner
f6ee6894c7 fix bugs related to reading configuration flags 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 09:59:23 -07:00
Dan Liew
f27ac24fa0 Add example of using Z3's new model construction C API. This API 
was requested in #1223.

This example uses the new `Z3_mk_model()`, `Z3_add_const_interp()`
, `Z3_add_func_interp()`, and `Z3_mk_as_array()` API calls.
 2017-10-24 17:34:47 +01:00
Nikolaj Bjorner
1315c8d7de rename repeated class apart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 09:03:28 -07:00
Nikolaj Bjorner
2c3b56315d Merge branch 'master' of https://github.com/z3prover/z3 2017-10-24 08:49:56 -07:00
Nikolaj Bjorner
637a0fa139 unused warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 08:49:25 -07:00
Christoph M. Wintersteiger
eda3c6258b backward comp 2017-10-24 12:53:24 +01:00
Nikolaj Bjorner
e6e1d94cf9 fix build issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:39:00 -07:00
Nikolaj Bjorner
bce143b2b2 Merge pull request #1323 from c-cube/pp-proof-graphviz 
print proofs in graphviz
 2017-10-24 03:28:04 -07:00
Nikolaj Bjorner
70f7846af5 move spacer_marshal to under parsers/smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:18:59 -07:00
Nikolaj Bjorner
d67f3c1466 create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:08:56 -07:00
Simon Cruanes
607eba1720 account for review 2017-10-24 11:44:28 +02:00
Nikolaj Bjorner
72c9134424 fixing regressions introduced when reducing astm proof dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 02:26:39 -07:00
Simon Cruanes
ed526b808d add parameter to specify the file into which dot proofs are to be printed 2017-10-24 10:16:56 +02:00