mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity
10845 commits 49 branches 53 tags 182 MiB
Commit graph

10845 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
f5bba63674
Merge pull request #1431 from waywardmonkeys/typo-fixes 
Typo fixes.
 2018-01-02 07:56:31 -08:00
Nikolaj Bjorner
a302832917
Merge pull request #1430 from waywardmonkeys/double-promotion-fix 
print_stat_f: Remove implicit conversion of float to double.
 2018-01-02 07:55:13 -08:00
Nikolaj Bjorner
a875d3e491 fix #1429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-02 07:54:31 -08:00
Bruce Mitchener
a3ad0aff8b print_stat_f: Remove implicit conversion of float to double. 2018-01-02 22:50:50 +07:00
Bruce Mitchener
73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07:00
Nikolaj Bjorner
e8a9e1a58b set default rewriter behavior in incremental mode to distribute multiplication over addition #1373 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 20:04:55 -08:00
Nikolaj Bjorner
c1c1b7378c removing axiom exposing unsoundness, replace by weaker axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 19:44:16 -08:00
Nikolaj Bjorner
f0a30ded7d add shorthand for translating models #1407 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 19:25:09 -08:00
Nikolaj Bjorner
8dadd30db5 add __copy__, __deepcopy__ as alias to translate on same context #1427. Add generalized Gaussian elimination as an option to first-pass NL solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 17:11:43 -08:00
Nikolaj Bjorner
b78c538e02 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-30 22:58:41 -08:00
Nikolaj Bjorner
c7d534160e Merge branch 'master' of https://github.com/z3prover/z3 2017-12-30 20:35:48 -08:00
Nikolaj Bjorner
79a9dfd8fd adding pre-processing to nlsat for equations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-30 20:35:33 -08:00
Nikolaj Bjorner
69879322d8 fix up convertion and printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-29 10:26:32 -08:00
Nikolaj Bjorner
444e178a01 fix up convertion and printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-29 10:24:48 -08:00
Nikolaj Bjorner
c80f34102f adding ad-hoc method for converting models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-28 17:29:31 -08:00
Nikolaj Bjorner
b1724b2f62 fix update to variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-28 14:39:16 -08:00
Nikolaj Bjorner
4c949cdbac Merge branch 'master' of https://github.com/z3prover/z3 2017-12-27 10:10:26 -08:00
Nikolaj Bjorner
d86e8f02d7 fix get-objectives error #1419 message (get-objectives) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-27 10:09:22 -08:00
Simon Cruanes
cfcff78754 validate unsat cores in recfun 2017-12-25 23:35:54 +01:00
Simon Cruanes
f7e5977b9e fix memleak 2017-12-25 22:51:40 +01:00
Simon Cruanes
35c802d869 simplify and strenghten some code 2017-12-25 22:51:39 +01:00
Simon Cruanes
0c753aa86a fix bugs related to backtracking and restarts 2017-12-25 22:51:39 +01:00
Simon Cruanes
b877bd8286 debug messages and gating 2017-12-25 22:51:39 +01:00
Simon Cruanes
3b4718b99a simpler conflicts when reaching unrolling limit (just add a clause) 2017-12-25 22:51:39 +01:00
Simon Cruanes
7b1e1d52e7 wip: conflicts for pruning branches with too many unrollings 
use the local assumption on depth to ensure the conflict clause is valid
 2017-12-25 22:51:39 +01:00
Simon Cruanes
06e0b12700 add a predicate for depth limit assumptions 2017-12-25 22:51:39 +01:00
Simon Cruanes
d5e134dd94 wip: add recursive functions 2017-12-25 22:51:39 +01:00
Simon Cruanes
fba22d2fac design document for handling recursive functions 2017-12-25 22:51:39 +01:00
Nikolaj Bjorner
5bc4c9809e initialize additional assumptions after setup_context is called the first time 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-25 12:50:11 -08:00
Nikolaj Bjorner
0b424942ab bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-23 14:42:21 -08:00
Nikolaj Bjorner
8198a8ce7b bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-23 14:41:16 -08:00
Murphy Berzish
0ac7082c80 add upper bound refinement (WIP) 2017-12-21 17:13:39 -05:00
Nikolaj Bjorner
36204fafa0 alternate strategies for QF_NIA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-19 20:27:08 -08:00
Nikolaj Bjorner
517b081202 remove custom exception, perhaps this handles exception issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-18 21:13:03 -08:00
Nikolaj Bjorner
d80c4307a6
Merge pull request #1410 from bannsec/assertion_slices 
Allowing slices and negative index in assertions
 2017-12-18 17:07:09 -08:00
Nikolaj Bjorner
13ee8da659 add virtual destructor to see if this helps ASan error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-18 15:57:16 -08:00
bannsec
d695767f61 Allowing slices and negative index in assertions 2017-12-18 21:48:54 +00:00
Nikolaj Bjorner
94d1695b01 Merge branch 'master' of https://github.com/z3prover/z3 2017-12-18 12:20:53 -08:00
Nikolaj Bjorner
399b27fda3 add Python facility for int2bv, fix #1398 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-18 12:20:44 -08:00
Christoph M. Wintersteiger
c3c06d756c Documentation fixes. 2017-12-18 20:12:19 +00:00
Nikolaj Bjorner
c199344bbf fix sat model converter to work with incrementality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-18 11:12:27 -08:00
Christoph M. Wintersteiger
63951b815d Bumped version number. 2017-12-18 18:58:21 +00:00
Christoph M. Wintersteiger
b0aaa4c6d7 Updated release notes 2017-12-18 14:18:30 +00:00
Nikolaj Bjorner
a5b663c52d add unit walk engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-17 16:09:07 -08:00
trinhmt
57845d4809
Merge pull request #4 from Z3Prover/master 
merge from z3prover/z3
 2017-12-16 20:46:42 +08:00
Thai Trinh
07afce6a64 pass vectors by reference 2017-12-16 20:44:07 +08:00
Nikolaj Bjorner
5adfae0fa8
Merge pull request #12 from TheRealNebus/opt 
Opt
 2017-12-15 14:12:02 -08:00
Miguel Angelo Da Terra Neves
a52fd4c6f2 merge 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-12-15 14:01:50 -08:00
Miguel Angelo Da Terra Neves
0f1286adae restored commented out code 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-12-15 14:00:20 -08:00
Miguel Angelo Da Terra Neves
b731d02adc fixes 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-12-15 13:56:59 -08:00