mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-29 02:39:24 +00:00
Code Activity
10693 commits 46 branches 52 tags 179 MiB
Commit graph

10693 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
774fa33bfe fix parameter lookup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 08:49:46 -07:00
Nikolaj Bjorner
1d408c1955 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-13 07:52:40 -07:00
Nikolaj Bjorner
167969d6c2 remove debug/non-debug difference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 07:52:36 -07:00
Nikolaj Bjorner
ca12a8482f fix to closure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-12 22:50:24 -07:00
Nikolaj Bjorner
4915fb080b fix #1749 by rejecting non-well-founded use of datatype in array 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-12 22:45:52 -07:00
Nuno Lopes
b7ea90c12b bv_decl_plugin: remove some mem allocs of parameters 2018-07-12 18:36:09 +01:00
Lev Nachmanson
5314ae60cc
Merge pull request #1750 from levnach/master 
fix in hnf by using signed terms
 2018-07-11 15:40:51 -07:00
Lev Nachmanson
e0e893b791 fix in hnf for the lower bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 12:29:09 -07:00
Lev Nachmanson
2dfb8f53b6 do not add term to hnf if one of the vars has v.y value 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Lev Nachmanson
5cfc3591d2 create hnf cuts too, when gomory_cut_period is 2 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Lev Nachmanson
3c230727bb rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Lev Nachmanson
adf0d745c1 rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Lev Nachmanson
bc17b18ed0 setting smt.arith.solver=6 by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Nikolaj Bjorner
f09f1a7524 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-11 08:53:00 -07:00
Nikolaj Bjorner
3a5aebd1d3 tidy model generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-11 08:52:57 -07:00
Nikolaj Bjorner
9f2bafbf10 tidy model generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-11 08:52:13 -07:00
Nikolaj Bjorner
e39107c682 turn lemma-id into an attribute on the cotext 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 21:26:51 -07:00
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