mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity
14107 commits 23 branches 48 tags 157 MiB
Commit graph

11916 commits

Author SHA1 Message Date
Lev Nachmanson
80467f1400 cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
431bb36cf5 cheap_eqs tree 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
f7f9c15676 cheap_eqs tree 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Nikolaj Bjorner
274323b818 fix reset order for #4533 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-19 16:07:45 -07:00
Nikolaj Bjorner
1204671595 fix #4534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-19 14:10:49 -07:00
Arie Gurfinkel
07a1aea689 fix(spacer): bug in assign_bounds to Farkas conversion 
The fix is to remove a hack that used a theory rewriter to simplify
the conversion. Now the conversion happens less often than possible.
Will need more thinking to fix properly.

The unsoundness at this point would cause SPACER to generate lemmas
that do not block a proof obligation and then get stuck in an infinite loop
blocking and generating the same lemma.
 2020-06-18 21:19:53 -04:00
Nuno Lopes
38d4418f94 simplify string_buffer::append 2020-06-18 19:55:34 +01:00
Nuno Lopes
fdeba2102c fix deref of free'd memory in mk_fresh_const 2020-06-18 19:25:32 +01:00
Nikolaj Bjorner
3b1149330d enable theory propagation of regex accept condition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-17 13:42:40 -07:00
Nikolaj Bjorner
be36a8fd80 fix for SPACER models using bit2bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-16 10:45:11 -07:00
Nikolaj Bjorner
48d4d8d7af fix tracking of bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-15 17:36:20 -07:00
Lev Nachmanson
f882219081 fix a bug in cheap_eqs with table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-15 13:30:45 -07:00
Lev Nachmanson
09516d74f6 change the default for cheap eqs to table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-15 13:30:45 -07:00
Lev Nachmanson
d13e584706 simplify the fixed var table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-15 13:30:45 -07:00
Nikolaj Bjorner
d09e6eccf0 re-enable proofs for qe-lite #3153 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-15 12:03:15 -07:00
Nikolaj Bjorner
395a304262 add optional feature to bound search within ranges 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-14 21:34:54 -07:00
Nikolaj Bjorner
180fb3abf6 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-14 11:36:09 -07:00
Nikolaj Bjorner
7387fc9dec avoid some bignum overhead in addmul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-14 11:20:05 -07:00
Nikolaj Bjorner
53e49eb428 neatify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-13 15:20:21 -07:00
Nikolaj Bjorner
5ee9edf46b fix incorrect bound in order-lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-13 14:28:42 -07:00
Lev Nachmanson
23c12b75af remove a duplicate option gb==grobner 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-13 10:03:19 -07:00
Lev Nachmanson
e5632736d2 review comments 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
fbfcc6796a fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
66701de157 fix the test build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
06826adec3 fix the race in add_var_bound and add_def_constraint 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
fe0e042e40 move m_fixed_var_table to lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
3b87cdfd0f remove the debug output 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
67eaff4490 testing cheap equalities 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
6c115bf896 cheap eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
94263167ec cheap eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
50b9915c57 avoid big nums in is_offset_row in cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
713eb6319d fix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
1587497562 cheap equalities 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
ccc8651800 cheap eqs on table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
b3bdce7837 make lp_bound_propagator a field of theory_lra::imp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
dd30b5e3af some simplifications in cheap eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
4de38d09e2 cheap eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
4f0bd93124 debug cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
110ab5e6ef debug cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
9c078c6d59 relaxing asserts in column_to_reported_index 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
6a678fd5be rename in lar_solver and memory corruption bug in cheap_eq 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
4936ace7cd more guards on cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
0ff18dd5a7 a small example passing with cheap eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
54921d08dc cheap_eq debug 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
4a9f031502 cheap_eqs progress 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
62bd19242e replace graph by a tree in cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
5d3070bc2d implement graph integrality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
1e4e887221 propagate cheap eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Nikolaj Bjorner
865dfe0590 own refs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-12 17:07:06 -07:00
Jack Yao
55cd1e996c
add sat option for doing a global simplification before the bounded search and the main CDCL search loop. The option is also used for the sat-preprocess tacitc (#4514) 
Co-authored-by: rainoftime <rainoftime@gmail.com>
 2020-06-12 16:45:50 -07:00