mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity
12732 commits 23 branches 48 tags 156 MiB
Commit graph

12732 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson c562a1f883 remove debug code and improve printing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-04 16:08:24 -08:00
Lev Nachmanson 0d95c780d1 remove an unnecessary check 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-04 14:51:15 -08:00
Nikolaj Bjorner fd808dd98b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-04 14:10:16 -08:00
Nikolaj Bjorner 876bd80bea fix model generation for underspecified operators in theory_lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-04 14:07:24 -08:00
Nikolaj Bjorner 283aa04d68 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-04 13:50:10 -08:00
Nikolaj Bjorner cc5971ceaf fix #2936 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-04 13:50:10 -08:00
Lev Nachmanson 06173aa4d7 do not use nl variables in random_update() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-04 11:51:37 -08:00
Nikolaj Bjorner 3ab7477663 fix #2920 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-04 10:20:44 -08:00
Nikolaj Bjorner d4d3971ecd add LUT finder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-04 09:59:01 -08:00
Nuno Lopes 506fbf9672 fix #2933: soundness issue in dom-simplify with (or foo true) 2020-02-04 14:05:12 +00:00
Nikolaj Bjorner 32968fa41c fix #2935 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-03 19:57:20 -08:00
Nikolaj Bjorner 7a946fd9d0 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-03 18:56:20 -08:00
Lev Nachmanson a05dec99cf do not random_update int vars 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-03 16:01:56 -08:00
Nikolaj Bjorner 47cdb5f46e fix #2913 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-03 09:14:23 -08:00
Nikolaj Bjorner fc4c1dac25 skip debug test for macos build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-03 09:10:03 -08:00
Nikolaj Bjorner 18280a9737 fix #2928 - test case is actually abuse of qe2. It is reasonable for qe2 to assume that simplify was applied first 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-03 08:43:45 -08:00
Nikolaj Bjorner 2398834206 fix #2929 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-03 08:36:37 -08:00
Nikolaj Bjorner d418467089 can't validate when benchmarks use strict bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-03 08:26:13 -08:00
Nikolaj Bjorner 18df6ce1fe remove stdout print 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-03 08:19:34 -08:00
Nuno Lopes e920648c1e reduce boilerplate in qe_lite 2020-02-03 12:01:05 +00:00
Nikolaj Bjorner 3760107bb8 fix #2930 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-02 20:03:55 -08:00
Nikolaj Bjorner 28c827fb69 fix #2919 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-02 14:49:35 -08:00
Lev Nachmanson d77a2ed567 fix the lp pretty printer 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-02 10:57:27 -08:00
Nikolaj Bjorner b0a28160f7 fix #2921 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-02 10:35:06 -08:00
Nikolaj Bjorner 805ac745e9 fix #2902 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 18:51:17 -08:00
Nikolaj Bjorner 3dc822c127 fix #2903 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 18:48:27 -08:00
Nikolaj Bjorner be95ea121b fix #2912 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 17:32:19 -08:00
Nikolaj Bjorner 321329d77c fix #2910 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 14:31:13 -08:00
Nikolaj Bjorner a9d22d7409 fix #2918 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 14:09:40 -08:00
Nikolaj Bjorner abbee32ddc fixup use of SYNC/SYNCH for mpz 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 11:18:36 -08:00
Nikolaj Bjorner 7df8d17639 move in assumptions to loop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 10:59:48 -08:00
Nikolaj Bjorner 75fb25a06c add randomization to lookahead selection' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 10:48:43 -08:00
Nikolaj Bjorner 615da0e3fb move remove thread unsafe increment to num_iterations, use num_rounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 10:38:24 -08:00
Nikolaj Bjorner ece041baf8 randomize branch direction (outside of int_solver for now) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 10:32:49 -08:00
Nikolaj Bjorner 1e92165690 branch selection updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 10:19:27 -08:00
Nikolaj Bjorner 74fc8cfde7 combine PS_THEORY with cache on/off mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 09:50:00 -08:00
Nuno Lopes 3ec7146ec8 attempt to fix build 2020-02-01 10:52:16 +00:00
Nikolaj Bjorner 9fab72b3ef fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-31 22:20:25 -08:00
Nikolaj Bjorner 5f89ead54b adding t-smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-31 17:08:53 -08:00
Nikolaj Bjorner 5f2720562b adding threads to smt core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-31 17:08:53 -08:00
Nikolaj Bjorner d4a24aff1e local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-31 17:08:52 -08:00
Lev Nachmanson abb13f8c76 randomise branches in int_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-31 14:38:28 -08:00
Nuno Lopes d2fc88d675 fix debug build 2020-01-31 17:30:13 +00:00
Nuno Lopes d79692b185 remove unused file & hide a few symbols 2020-01-31 17:13:28 +00:00
Lev Nachmanson 35aa98436f fix term columns after rounding in cube() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-30 14:29:36 -08:00
Lev Nachmanson 41a4dcf90c do not increment m_number_of_calls twice in check() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-30 10:10:15 -08:00
Nuno Lopes eece2f4d49 remove unused vars 2020-01-30 15:30:14 +00:00
Nuno Lopes bb5edb7c65 qe_lite: fix crash when formula has var def with concat, e.g. 
(assert (forall ((a (_ BitVec 4)) (b (_ BitVec 4)))
  (not (and (= a (bvshl #x1 b))
            (= ((_ extract 3 2) b) #b00)))))
 2020-01-30 14:07:47 +00:00
Nuno Lopes 1f0bd04e50 qe_lite: privatize classes & fix some compiler warnings 2020-01-30 11:36:50 +00:00
Lev Nachmanson 9694dc0c74 change in the test lp.cpp and in a trace statement 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-29 11:03:18 -08:00