mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-05 01:27:41 +00:00
Code Activity
10659 commits 67 branches 52 tags 179 MiB
Commit graph

978 commits

Author SHA1 Message Date
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
nilsbecker
6d2cf4f464 smt-like logging of theory specific meaning of constants 2018-12-10 22:49:08 +01:00
Bruce Mitchener
51a947b73d Change how 64 bit builds are detected. 
Instead of doing this at configure time, we look at the actual
compile time status. This also avoids hardcoding checks based on
what CPU architecture is present, which doesn't work when Z3 is
being built on non-x86_64 platforms.
 2018-12-09 16:16:20 +07:00
Bruce Mitchener
4bc1b0b8c8 Fix typos. 2018-12-05 21:07:34 +07:00