mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
12781 commits 49 branches 53 tags 182 MiB
Commit graph

12781 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Jerry James
1dfe1a975b Add explicit instantiation of update_inf_cost_for_column_tableau. 2020-01-28 21:30:24 -08:00