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 |
|
Lev Nachmanson
|
a38f58e49f
|
simplify tang lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
052814d165
|
NB fix in theory_lra mk_bound
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
fd1e0e4d80
|
fixes for mixed case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
9c8d5ddffb
|
enable test_tangent_lemma_reg
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
30d35488d8
|
get_rid or inf eps
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
0e86c567cc
|
prepare the mixed case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
8980aff7f3
|
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
1b07ad0952
|
fix errors with dependency manager reset
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
6bc5400c5d
|
add deps from fixed vars
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
e17214c1c2
|
return the minimal dependencies for the case of a fixed to zero var in pdd_expr()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
379a1927e6
|
fix a bug in nexvar()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f0b530b0e4
|
experiment with substituting zeros in Horner&Grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
45c0f2225c
|
allow unlimited number of Grobner calls
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
b577544830
|
make grobner quota a parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
06203d227e
|
cleanup the grobner config init
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f2884088cc
|
add quota to Grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
7ad95aa5d2
|
Nikolaj fixes pdd_manager::reduce() to work with the changed order
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
00e1049ff2
|
move some grobner settings to pdd_solver.m_config
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|