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

649 commits

Author SHA1 Message Date
Nikolaj Bjorner 8893913c98 remove internal referenes to set_activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:06:05 -07:00
Nikolaj Bjorner c012f6ea5b fix #2210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-07 03:09:48 +02:00
Nikolaj Bjorner 9cb1a0f094 fix #2253 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 14:24:53 -07:00
Nikolaj Bjorner 9f1b8db870 adjust for SMTLIBification name change of set operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 14:13:23 -07:00
Nikolaj Bjorner 596acf26ce take second suggestion from #2234 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-16 10:39:34 -07:00
Uli Schlachter ebe58f78cf lp_tokenizer: Add missing verbose print 
Three out of two places that call m_tokens.push_back() in
lp_tokenizer::parse_all() were followed by a verbose print. This commit
adds a verbose print to the third such place.

Signed-off-by: Uli Schlachter <psychon@znc.in>
 2019-04-13 15:59:30 +02:00
Nikolaj Bjorner ff6d703c05 add tracing, fix #2214, remove unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-02 12:20:55 -07:00
Nikolaj Bjorner 5c67c9d907 print certificate for #2202, enable CTL-C for API fix #2203 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 17:09:02 -07:00
Nikolaj Bjorner 75b1e8fe27 add tracing for 2157 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-12 20:12:17 -07:00
Nikolaj Bjorner 7aa8b4ac2a restrict idiv-bound checks to bounded terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 19:11:22 -08:00
Nikolaj Bjorner 15d5be66b6 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-25 18:14:47 -08:00
Nikolaj Bjorner 4ff940a29e mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-25 18:14:41 -08:00
Nikolaj Bjorner 8c085f1a18 removing unused and fixing suspect optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 21:26:29 -08:00
Nikolaj Bjorner ea778eefb2 skip optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 20:58:30 -08:00
Nikolaj Bjorner 89bf2d4368 add API for setting variable activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 12:05:24 -08:00
Nikolaj Bjorner 7fa9768c36 improving drat output perf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 09:16:46 -08:00
Nikolaj Bjorner cb94f82f37 fix #2118 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:31:05 -08:00
Nikolaj Bjorner 8d20310758 adding trail/levels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-29 14:45:51 -08:00
Nikolaj Bjorner e22c657811 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-29 10:50:28 -08:00
Nikolaj Bjorner 94dae2da3a fix fourth bug produced by repros by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-27 18:11:18 -08:00
Nikolaj Bjorner d0b2f73c0c change opt.maxlen.enable default to true to prefer this over all other heuristics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-26 13:02:25 -08:00
Nikolaj Bjorner 121211a51c maxlexN 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-25 20:01:38 -08:00
Nikolaj Bjorner 1ed68906fa fix debug assertion code, make maxlex optional 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-25 08:23:41 -08:00
Nikolaj Bjorner d3d392da41 adding maxlex, delay mk_true() calls in goal2sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 21:36:40 -08:00
Nikolaj Bjorner b4f4a1f316 adding maxlex, throttle use of asymmetric literal addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 19:47:50 -08:00
Nikolaj Bjorner ad81fee118 adding maxlex, throttle use of asymmetric literal addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 19:26:44 -08:00
Nikolaj Bjorner 498864c582 adding dump facility for cancelation #2095, easing dimacs in/out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 12:21:23 -08:00
Nikolaj Bjorner 8566d88b99 remove validation assert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 12:49:04 -08:00
Nikolaj Bjorner 9dd41ba554 remove offending assert, disable assembly-info for dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:13:03 -08:00
Nikolaj Bjorner 1efbc25b3b Merge branch 'master' of https://github.com/z3prover/z3 2019-01-18 18:09:22 -08:00
Nikolaj Bjorner 0b7021d2c8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 18:09:19 -08:00
Nikolaj Bjorner c45ab6efed add setting to dump intermediary models #2087 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 15:12:08 -08:00
Nikolaj Bjorner b33f5f879e fix another bug reported by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 17:57:11 -08:00
Nikolaj Bjorner 0b84c60886 fix another bug uncovered by Dunlop, prepare grounds for equality solving within NNFs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 01:25:25 -08:00
Nikolaj Bjorner 4159b987ce purge unused code from theory_pb, fix bug reported by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 03:23:57 -08:00
Nikolaj Bjorner 4b35ef29c9 fix #2081 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 01:18:03 -08:00
Nikolaj Bjorner 63d480fd92 fix cnf check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 21:17:39 -08:00
Nikolaj Bjorner 2dcf36e96c fix #2044 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:32:38 -08:00
Nikolaj Bjorner 2aa7ccc4a9 hide bit-vector dependencies under seq_util 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-03 08:45:17 -08:00
Bruce Mitchener e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07:00
Nikolaj Bjorner 141cd687ff disable validation in builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-17 15:37:36 -08:00
Nikolaj Bjorner d45b8a3ac8 fix debug build, add access to numerics from model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-17 15:24:54 -08:00
Nikolaj Bjorner 9ec59fdb93 fix #1934 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-17 15:04:25 -08:00
Nikolaj Bjorner 28a5a515a8 fix #1889 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-18 09:20:12 -07:00
Michał Janiszewski cfd0486582 Catch exceptions by const-reference 
Exceptions caught by value incur needless cost in C++, most of them can
be caught by const-reference, especially as nearly none are actually
used. This could allow compiler generate a slightly more efficient code.
 2018-10-16 19:16:07 +02:00
Nikolaj Bjorner c4829dfa22 fix #1577 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 09:01:01 -07:00
Nikolaj Bjorner 44a0dbbc61 fix #1864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 08:06:51 -07:00
Nikolaj Bjorner b540868cd7 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-04 13:43:04 -07:00
Nikolaj Bjorner a549e73b86 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-04 13:43:01 -07:00
Nikolaj Bjorner 3bc2213d54 fix #1577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 17:43:42 -07:00