mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 09:56:39 +00:00
Code Activity
13531 commits 43 branches 51 tags 169 MiB
Commit graph

94 commits

Author SHA1 Message Date
Nikolaj Bjorner
98ff388c4e fix #3910 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-11 13:11:47 -07:00
Nikolaj Bjorner
ee9c797822 address #3886 and #3891 by revamping nl_arith decoupling of monomial analysis and access 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-10 01:33:46 -07:00
Nikolaj Bjorner
7a04e52c41 fix ordering of delayed assume eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 16:22:24 -07:00
Lev Nachmanson
96cc58f67c instrument the tableau 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
b6618892d8 fix #3469 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-22 11:02:24 -07:00
Nikolaj Bjorner
611c14844d fix #3194, remove euclidean solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-08 16:05:13 +01:00
Nikolaj Bjorner
cc5971ceaf fix #2936 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-04 13:50:10 -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
d4a24aff1e local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-31 17:08:52 -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
e8b6b870ac port grobner basis functionality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
36380463d7 start porting grobner basis functionality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
35efdc9852 start porting grobner basis functionality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
26b4294bce start porting grobner basis functionality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner
6cf7d8e523 adding div0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-06 11:23:19 +01:00
Nikolaj Bjorner
ca498e20d1 move value factories to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-16 19:48:35 -07:00
Nikolaj Bjorner
0481adb87c fix #2547 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-10 06:38:27 +02:00
Nikolaj Bjorner
a337a51374 fixes for #2513 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-23 23:29:24 +03:00
Nikolaj Bjorner
8e2ad4e461 #2379 and #2380 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-04 07:08:47 +07:00
Nikolaj Bjorner
f699ac0353 fixing bugs uncovered by repro in #1914 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-05 13:54:23 -08:00
Michał Janiszewski
844f400a62 Remove superfluous const from returned types 2018-10-16 19:30:48 +02:00
Nikolaj Bjorner
1a3fe1edd3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-16 13:43:38 -07:00
Lev Nachmanson
c04bcb411d no calling cut_solver when there are bounded columns 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

use special bounds inf find_cube for x+y, x-y

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

bug fixes in column patching, add stats to patching, restructure int_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

comment out m_old_values from int_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

avoid calling pivot_fixed_vars_from_basis() in int_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fix the return value from path_nbasic_columns

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fix the return value from path_nbasic_columns

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work in patch_columns

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on int_solver check()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

exit from find_free_interval() when l >= u

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

experiment with branching on nbasic columns

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

remove m_old_values

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

add rounding to patch_columns

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

qflia

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

patch all columns, round non-patched, branch or basic columns

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

refactor int_solver::check()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

restore  move_non_basic_columns_to_bounds() after a failure in find_cube()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

optimize gomory cuts search

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

produce gomory cuts without moving columns to bounds

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

call find_feasible_solution() after moving columns

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

alway move colums to bounds before gomory cut

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

merge from best branch

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-27 11:38:40 -07:00
Nikolaj Bjorner
50c93d1ad4 merge with 4.7.1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-22 17:10:36 -07:00
Daniel Schemmel
78087483ca
Add missing include 
The code should not have compiled previously, as smt::context was only forward declared at this point.
 2018-05-20 15:34:01 +02:00
Nikolaj Bjorner
c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Bruce Mitchener
73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07:00
Nikolaj Bjorner
4520fafa8c fix #1368 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-26 19:13:35 -08:00
Nikolaj Bjorner
0d15b6abb7 add stubs for converting assertions, consolidate filter_model_converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 14:51:13 -08:00
Nikolaj Bjorner
cf87b6d622 remove simplifier files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-29 09:22:27 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
7e1fae418a fix #1005, disable expansion of regular expression range to union as it degrades performance significantly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-05 10:59:47 -04:00
Nikolaj Bjorner
fa868e058e fix bound bug #991 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 17:39:02 -07:00
Nikolaj Bjorner
b42973152f fix model generation for non-linear expressions, reported by Martin Suda and Giles Reger 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 12:02:32 -05:00
Nikolaj Bjorner
dea3b8ddf7 address warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 13:14:36 +01:00
Nikolaj Bjorner
9c7e5c37d1 add equality propagation based on partial length information to sequence theory. Fix issue #429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-04 08:12:46 -08:00
Nikolaj Bjorner
9a6fe93e6c re-enable feature that lets Z3 solver mixed integer/real constraints with additional information tha texpressions with sort real can only take integer values. Fixes regression on epsilon.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 12:42:18 -08:00
Nikolaj Bjorner
20cfbcd66b dealing with issues #402 #399 #258 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-09 13:29:44 -08:00
Nikolaj Bjorner
af758dea4a tuning for seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 08:23:44 -08:00
Nikolaj Bjorner
071a654a9a seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-27 04:41:25 -08:00
Nikolaj Bjorner
3d993a4ee1 Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-06 17:29:53 -08:00
Nikolaj Bjorner
b4cb51cdb3 working on Forking/Serializing a z3 Solver #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 17:29:24 -08:00
Nikolaj Bjorner
fc592fc856 fix for #291. The root issue is that the set of antecedents is recycled as a fixed object between routines. Antecedents that were already allocated for a Gomory cut got reset by the internalizer. This causes unsound bounds axioms to be created 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-05 15:08:42 -08:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Nikolaj Bjorner
d9522cfd07 fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 12:05:19 +02:00
Nikolaj Bjorner
9734407cde disable throttle on unbounded objectives in shared theories. It may violate an interface equality, to fix issue #120 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 11:14:59 -07:00
Nikolaj Bjorner
534271db08 adding parameters to gomory cut axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 14:48:51 -07:00
Nikolaj Bjorner
e8811748d3 fix regressions in nl/smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-16 19:08:37 +01:00