mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity
4941 commits 23 branches 48 tags 157 MiB
Commit graph

4941 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes
9c620376c2 simplify ast::are_equal(), since pointer equality is sufficient 2016-03-07 13:15:12 +00:00
Christoph M. Wintersteiger
4423447029 Merge pull request #486 from 4tXJ7f/patch-1 
[Z3py] Add examples for fpToFP
 2016-03-07 11:31:12 +00:00
Christoph M. Wintersteiger
eccf03aaac build fix for non-windows platforms 2016-03-07 11:21:06 +00:00
Andres Nötzli
d6ece7e8a5 [Z3py] Add examples for fpToFP 2016-03-07 00:21:26 -08:00
Nikolaj Bjorner
4cd1efc50e address unused variable warnings from OSX build log 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-05 15:33:33 -08:00
Nikolaj Bjorner
aa1ddd169a fix bug in offset for shift amount for free bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-05 15:25:14 -08:00
Nikolaj Bjorner
5c276d8bf1 Merge pull request #484 from NikolajBjorner/master 
Replacing legacy evaluator from proto_model, fix scope-related bugs in rewriter
 2016-03-05 10:36:52 -08:00
Nikolaj Bjorner
640308b546 make proto-model evaluation use model_evaluator instead of legacy evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-05 10:27:19 -08:00
Nikolaj Bjorner
70f13ced33 make proto-model evaluation use model_evaluator instead of legacy evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-05 10:14:15 -08:00
Christoph M. Wintersteiger
a2ecb19d03 Added hash-consing remarks to mk_context and mk_context_rc. 
Fixes #452
 2016-03-05 17:58:32 +00:00
Christoph M. Wintersteiger
8abedbf389 whitespace 2016-03-05 17:55:27 +00:00
Christoph M. Wintersteiger
03a8ef2795 Fixed non-Windows preprocessor options. 
Fixes #463
 2016-03-05 17:14:19 +00:00
Christoph M. Wintersteiger
f34e15f289 whitespace 2016-03-05 16:47:39 +00:00
Christoph M. Wintersteiger
9dfc2bc61e Fixed memory leaks in fpa2bv converter. 
Fixes #480
 2016-03-05 16:47:08 +00:00
Christoph M. Wintersteiger
09832ca807 Fixed static Windows binary build. 2016-03-05 13:58:28 +00:00
Christoph M. Wintersteiger
fedc6d4754 Fixed memory leak in fpa2bv tactic. 2016-03-05 12:54:36 +00:00
Nikolaj Bjorner
f54c430756 Merge pull request #483 from zv/fix_arith_div 
Bugfix for arith_rewriter single operand division
 2016-03-04 18:51:14 -08:00
Zephyr Pellerin
b13db1e82e Bugfix for arith_rewriter single operand division 2016-03-04 18:26:00 -08:00
Christoph M. Wintersteiger
40c5152075 Added --staticbin option. 
Relates to #456
 2016-03-04 18:32:45 +00:00
Christoph M. Wintersteiger
cf5910e041 typos 2016-03-04 15:08:03 +00:00
Christoph M. Wintersteiger
a51201298c Bugfix for assumptions in inc_sat_solver 2016-03-04 14:42:38 +00:00
Christoph M. Wintersteiger
b2eb5b7170 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-04 13:09:50 +00:00
Christoph M. Wintersteiger
8cc3ba5a8b fixed FP Python doctest examples 2016-03-04 13:09:42 +00:00
Nikolaj Bjorner
6fef24edb4 recursive function definitions; combine model-building functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-03 08:07:06 -08:00
Nikolaj Bjorner
50b2389e7f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-03 07:59:13 -08:00
Nikolaj Bjorner
7c6540e18f recursive function definitions; combine model-building functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-03 07:59:03 -08:00
Christoph M. Wintersteiger
1aeea763ff Assertion fix in inc_sat_solver 2016-03-02 18:39:28 +00:00
Christoph M. Wintersteiger
bf40bb8005 Bugfix for inc_sat_solver 2016-03-02 18:27:01 +00:00
Christoph M. Wintersteiger
68416bf6bc whitespace 2016-03-02 18:25:56 +00:00
Christoph M. Wintersteiger
bddf416064 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-02 18:06:22 +00:00
Christoph M. Wintersteiger
dbf9609b4c added assertion 2016-03-02 18:06:14 +00:00
Christoph M. Wintersteiger
f128c76f23 whitespace 2016-03-02 18:05:14 +00:00
Christoph M. Wintersteiger
6fa2338edc Merge pull request #471 from 4tXJ7f/patch-1 
[Z3py] Fix documentation in FPSortRef
 2016-03-02 14:14:54 +00:00
Nikolaj Bjorner
1a081936ac Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 22:31:53 -08:00
Nikolaj Bjorner
a25336a899 fix test build, working on rec-functions and automata complementation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 22:31:44 -08:00
Andres Nötzli
18b9cd1948 [Z3py] Fix documentation in FPSortRef 2016-03-01 18:56:20 -08:00
Christoph M. Wintersteiger
1e86175c03 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 21:21:32 +00:00
Christoph M. Wintersteiger
59e695f2be Bugfixes for FP numerals in Python 
Relates to #464, #470
 2016-03-01 21:21:25 +00:00
Nikolaj Bjorner
9b6963d112 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 09:48:53 -08:00
Nikolaj Bjorner
67397bf71e enable logic parameter update to configure SMTLIB logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 09:48:24 -08:00
Christoph M. Wintersteiger
0cb8193cdd logic fix 2016-03-01 17:42:33 +00:00
Christoph M. Wintersteiger
4fe4db6657 build fix for static libray on Windows 2016-03-01 17:34:45 +00:00
Nikolaj Bjorner
7f51ecab37 enable logic parameter update to configure SMTLIB logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 09:26:14 -08:00
Nikolaj Bjorner
31c58b0999 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 08:46:51 -08:00
Nikolaj Bjorner
908f09a9df update logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 08:46:43 -08:00
Christoph M. Wintersteiger
c171170bed Fixed FP string input conversions. 
Fixes #464
 2016-03-01 15:31:33 +00:00
Christoph M. Wintersteiger
b6e43b6d7b Merge pull request #468 from 4tXJ7f/fix_fp_neq 
[Z3py] Consistent behavior of eq and ne for FP
 2016-03-01 14:07:28 +00:00
Christoph M. Wintersteiger
ad9127690d Merge branch '4tXJ7f-fix_build' 2016-03-01 14:05:30 +00:00
Christoph M. Wintersteiger
5c35a07a46 Merge branch 'master' of https://github.com/Z3Prover/z3 into 4tXJ7f-fix_build 
# Conflicts:
#	src/math/automata/symbolic_automata_def.h
 2016-03-01 14:05:19 +00:00
Nuno Lopes
62e46aacd9 bv_bounds: make may_simplify more precise to skip exprs with just 1 bound expr 
speedups up to 3x in selected benchmarks
 2016-03-01 11:31:08 +00:00