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

981 commits

Author SHA1 Message Date
Lev Nachmanson e59d60fbbe Remove unnecessary null pointer checks 2019-03-22 10:47:11 -07:00
Lev Nachmanson 61ac006cbe Remove unnecessary null pointer checks 2019-03-22 10:32:33 -07:00
Lev Nachmanson 6e5d0b7594 Remove unnecessary null pointer checks 2019-03-22 09:43:34 -07:00
Lev Nachmanson 885d640301 make explicit rational(double)constructor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-19 19:45:33 -07:00
Nikolaj Bjorner 90b78eb64a use random_next instead of library random 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-13 19:59:05 -07:00
Lev Nachmanson f336039da3 snap variables to bounds when maximizing terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-13 15:28:50 -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
Nuno Lopes 9736c46375 constify is_threaded if MT is disabled 2019-03-08 11:16:10 +00:00
Nuno Lopes cd4b53500c avoid a few str copies + symbol hiding 2019-03-08 10:13:46 +00:00
Nikolaj Bjorner 5c13acbf9f remove print directive that doesn't compile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 20:48:13 -08:00
Nikolaj Bjorner 0c0e79a937 add logging to lar-solver to capture state for unbounded optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 20:33:12 -08:00
Nikolaj Bjorner 19e7b75536 set status optimal also on object 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 19:31:51 -08: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 3723c1af0a
Merge pull request #2166 from levnach/Prover 
fixes in indices in lar_solver::maximize_term()
 2019-03-03 13:00:51 -08:00
Lev Nachmanson 06725de477 fixes in indices in lar_solver::maximize_term() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-03 10:57:25 -10:00
Nikolaj Bjorner 7399f78dfd disable model compression for regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 12:40:59 -08:00
Nikolaj Bjorner 3ee5c0e7d9 fix #2164 address some of simplification shortcommings from #2151 #2152 #2153 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 11:33:44 -08:00
Lev Nachmanson 69f03952a7 enable lar_solver::constraint_holds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-02-28 12:11:34 -10:00
Nikolaj Bjorner b632c08fe0 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-28 08:35:26 -08:00
Nikolaj Bjorner 4c76d43670 add binary_merge encoding option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 08:35:22 -08:00
Nuno Lopes 6a0c409b0f move a few strings instead of copying 2019-02-28 10:53:27 +00:00
Nikolaj Bjorner e79f7ca1fd
Merge pull request #2150 from Nils-Becker/master 
Logging Support for Theory Solvers
 2019-02-27 17:06:31 +01:00
Nikolaj Bjorner 6ef3e5e363 integrate some self-contained fixes from #2147 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-24 14:21:34 -08:00
nilsbecker 960708e99e Merge branch 'master' of https://github.com/Z3Prover/z3 2019-02-23 12:34:40 +01:00
nilsbecker 6ee3941523 more cleanup 2019-02-23 12:08:08 +01:00
Nikolaj Bjorner c0d20f8ea8 add cr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-23 10:59:10 +01:00
Nikolaj Bjorner 28c675f56e
Merge pull request #2146 from danielschemmel/buffer-1 
Buffer and Vector Modernization Part 1
 2019-02-23 10:55:08 +01:00
nilsbecker a8586746be cleanup for pull request 2019-02-23 02:47:33 +01:00
nilsbecker ec76efedbe synchronizing with main repository 2019-02-22 00:19:43 +01:00
Nuno Lopes bb7aa16223 stopwatch: fix debug build crash in sat solver 2019-02-21 16:38:48 +00:00
Nuno Lopes 6598aedbb2 fix VS build, take 2 2019-02-21 15:52:52 +00:00
Nuno Lopes 3d7878bafc hopefully fix build with VS 2012 2019-02-21 15:25:26 +00:00
Nuno Lopes 2f33bafd5a stopwatches: fix a few places that would call start/stop multiple times 2019-02-21 14:59:31 +00:00
Daniel Schemmel 721ea2a8d3
Move vector.h to old_vector.h and add a shim vector.h 
To do so, one instance of the class keyword needs to be removed.
 2019-02-21 15:38:08 +01:00
Nuno Lopes 85162d90d1 simplify timer.h 2019-02-21 13:57:38 +00:00
Nuno Lopes 3a7c467822 fix debug build.. 2019-02-21 13:33:52 +00:00
Nuno Lopes 3a5263be95 modernize stopwatch 2019-02-21 13:30:27 +00:00
Daniel Schemmel 2ff2e77739
Move buffer.h to old_buffer.h and add a shim buffer.h 2019-02-21 13:05:58 +01:00
Nuno Lopes a76c0fbbfb simplify timeout mechanism and fix race conditions there 2019-02-21 11:49:41 +00:00
Nuno Lopes f3cd7d646d further simplifications to scoped_timer 2019-02-21 10:42:42 +00:00
Nuno Lopes edf0df634d simplifications to refs 2019-02-19 13:18:20 +00:00
Nuno Lopes 73f6806371 rewrite scoped_timer in C++11 way 
the code is much smaller and reused across platforms
I see a small speedup on linux as well
 2019-02-04 17:42:27 +00: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 ee07008fb9 import files from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:04:46 -08:00
Nikolaj Bjorner e954f59052 ensure that solver objects have timeout/rlimit/ctrl-c exposed as possible parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 13:50:17 -08:00
Bruce Mitchener d757c342d5 Define NO_Z3_DEBUGGER for emscripten builds. 2019-01-07 23:13:09 +07:00
Nikolaj Bjorner 2486971094
Merge pull request #2065 from waywardmonkeys/improve-ios-support 
Define NO_Z3_DEBUGGER for iOS builds.
 2019-01-06 18:56:03 -08:00
Bruce Mitchener 7e1ce2a16c Define NO_Z3_DEBUGGER for iOS builds. 
This is defined because we can't call `system` (via `invoke_gdb`)
on iOS and related platforms.
 2019-01-06 12:16:33 +07:00
Bruce Mitchener a06bc49710 Let str_hashtable store const char*. 
This removes some boilerplate const casting.
 2019-01-06 12:15:31 +07:00
Bruce Mitchener 877df0f1cc If NO_Z3_DEBUGGER, also drop defining invoke_gdb. 2018-12-27 09:21:45 -05:00