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

11426 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
5e5f46f0f8 handle cancelation from nra_solver gracefully 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 17:34:45 -07:00
Nikolaj Bjorner
0170a9772a expose methods for dumping T-lemmas from theory_lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 16:44:48 -07:00
Lev Nachmanson
61cc3d1250
Merge pull request #1747 from levnach/master 
remove an assert
 2018-07-10 12:08:13 -07:00
Lev
a4a468660d remove an assert 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-10 12:05:23 -07:00
Nikolaj Bjorner
b59fa3ebd7 fix #1746 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 09:05:24 -07:00
Nikolaj Bjorner
30a30e76f9
Merge pull request #1744 from levnach/master 
enable printing from Release
 2018-07-10 01:24:55 -07:00
Lev
c4c52ad104 enable printing in Release 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson
5c712d471f create hnf cuts too, when gomory_cut_period is 2 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson
c518ddac6f rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson
fd980952ea rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson
367fff618d setting smt.arith.solver=6 by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Nikolaj Bjorner
390f77ee69
Merge pull request #1743 from rainoftime/master 
Add example of using z3's model construction C++ API
 2018-07-09 20:20:03 -07:00
rainoftime
bb534f6103 Add example of using z3's model construction C++ API 2018-07-10 11:16:20 +08:00
Nikolaj Bjorner
fc4627a24f force the new arithmetic solver for QF_LIA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 16:33:48 -07:00
Nikolaj Bjorner
567fbac27f add back old multiplication for comparison 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 14:33:32 -07:00
Nikolaj Bjorner
de454db58c guard expensive ite rewrites under configuration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 14:17:39 -07:00
Nikolaj Bjorner
8373bec6ad only assign, if there isn't already a true literal incube/clause mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 10:33:56 -07:00
Nikolaj Bjorner
efe440839e Merge branch 'master' of https://github.com/z3prover/z3 2018-07-09 09:19:37 -07:00
Nikolaj Bjorner
605dcc40a3 fix #1741 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 09:19:13 -07:00
Nikolaj Bjorner
4b802fd5cd
Merge pull request #1740 from alexanderjsummers/master 
Added return value to bool-typed function
 2018-07-09 09:05:52 -07:00
Nuno Lopes
009708ed07 remove unneeded creation of tmp mpz_manager 2018-07-09 10:52:27 +01:00
Nuno Lopes
6f7271a5e8 remove virtual destructor from api::pmanager 2018-07-09 10:37:26 +01:00
alexanderjsummers
d6a3afd2a1
Added return value to bool-typed function 
It seems that without this, the build fails with a default Visual C++ on Windows; see https://docs.microsoft.com/en-gb/cpp/error-messages/compiler-warnings/compiler-warning-level-1-c4716 

Another option would be to add the #pragma directive mentioned there.
 2018-07-09 11:30:24 +02:00
Nuno Lopes
c5a282dadb sat_allocator: align allocation size with page boundary to reduce memory consumption 2018-07-08 18:04:32 +01:00
Nuno Lopes
a85a4f41c7 ast_exception: remove str copies 2018-07-08 15:32:01 +01:00
Nuno Lopes
fd75eccfec don't even bother allocating traces in release mode 2018-07-08 13:21:16 +01:00
Nikolaj Bjorner
a2d078f6f5
Merge pull request #1737 from Nils-Becker/master 
Equality Explanation Logging
 2018-07-07 15:39:08 -07:00
Nikolaj Bjorner
290302dca8
Merge pull request #1738 from agurfinkel/deep_space 
Fix bug in proof checking
 2018-07-07 15:36:39 -07:00
Nuno Lopes
d2b77b1170 remove dead code 2018-07-07 19:07:13 +01:00
Arie Gurfinkel
1de0f8fe5e Fix bug in proof checking 2018-07-07 19:10:16 +03:00
Nikolaj Bjorner
dfbd285dae avoid rewriting if reduces to tautology 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 22:02:48 -07:00
Nikolaj Bjorner
dc932a93e2 fix #1736 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 21:44:16 -07:00
Nikolaj Bjorner
ecb5c45d6f Merge branch 'master' of https://github.com/z3prover/z3 2018-07-06 21:33:58 -07:00
Nikolaj Bjorner
c4e4139ab6 fix clause check in goal2dimacs, redo rewriting of mod to avoid deeply nested mod 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 21:33:53 -07:00
Nikolaj Bjorner
e4ae80b3f2 update documentation for renamed parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 21:25:38 -07:00
Nikolaj Bjorner
3ae0ea8246 add circuit and unate encoding besides sorting option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 21:09:13 -07:00
nilsbecker
820c14ed06 synchronize fork 2018-07-06 16:19:13 +02:00
nilsbecker
a405742037 Adding comments 2018-07-06 12:43:46 +02:00
Nikolaj Bjorner
0b30ddb769 fix #1733 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 02:09:47 -07:00
Nikolaj Bjorner
a0124a079e Merge branch 'master' of https://github.com/z3prover/z3 2018-07-06 01:49:19 -07:00
Nikolaj Bjorner
c3035de44e logging in sorting network 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 01:49:13 -07:00
Nikolaj Bjorner
ca8183da33
Merge pull request #1732 from levnach/upbranch 
fix in theory_lra.cpp get_value
 2018-07-05 19:37:59 -07:00
Lev Nachmanson
852df6f7d9 reshufle var_register to faster access 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-05 16:35:05 -07:00
Lev Nachmanson
905282ffe4 fix in theory_lra.cpp get_value 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-05 14:47:05 -07:00
Nikolaj Bjorner
1918395f0e fix bug in sat-solver where frozen clauses get re-attached 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-05 12:19:03 -07:00
Nikolaj Bjorner
eceb92f5ef add utilities for purification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-05 09:50:39 -07:00
Nikolaj Bjorner
f96133f4d9 fix #1729 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-05 07:17:08 -07:00
Nikolaj Bjorner
adb9a1c797 fix c 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-04 17:31:26 -07:00
Nikolaj Bjorner
f4abb7eb48 fix c++ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-04 16:26:05 -07:00
Nikolaj Bjorner
a74f2ed9dc Merge branch 'master' of https://github.com/z3prover/z3 2018-07-04 16:05:02 -07:00