mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 10:51:50 +00:00
Code Activity
12618 commits 23 branches 48 tags 156 MiB
Commit graph

12618 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner eefb685fa9 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-28 18:49:25 -08:00
Nikolaj Bjorner ff5bdd6f1f speed up freedom interval computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-28 15:21:39 -08:00
Lev Nachmanson 75d1e8e929 return l_undef in get_phase() if lpvar is not available 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 12:06:56 -08:00
Nikolaj Bjorner 8b7426f5ad add filter to gcd test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-28 11:30:16 -08:00
Nikolaj Bjorner f161bdaf8f fix #2898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-28 10:30:57 -08:00
Lev Nachmanson d3a4b7c44b correct handling of int terms in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 8ebeaf03b4 rebase with Z3Prover/z3/master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 90f14ec0b3 rebase with Z3Prover/master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 19120bee81 fix the debug build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 80245f05ad rebase with Z3Prover and Nikolaj's changes in lp bound propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 8388868c27 fix the make build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 3bc67d1804 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 696c95e1cf remove duplicate lines 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00