mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
10048 commits 49 branches 53 tags 182 MiB
Commit graph

10048 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
33fc56f686 fix debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 18:36:43 -07:00
Nikolaj Bjorner
f1d27cd487 workaround non-deterministic behavior of is_irrational_numeral test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 18:16:32 -07:00
Lev Nachmanson
16d4e2f5d1 regression fix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 16:10:15 -07:00
Lev Nachmanson
4d88818560 fixes in get_lower,get_upper of theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 14:38:10 -07:00
Lev Nachmanson
342feeff03 implement get_lower, get_upper in theory_lra.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 14:17:13 -07:00
Lev Nachmanson
da44ad7e6f added stubs for get_lower/get_upper required by theory_seq 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 13:43:23 -07:00
Lev Nachmanson
f2e878047d avoid a crash in maximize_term when the term var has not been used 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 13:33:31 -07:00
Nikolaj Bjorner
481b177d47 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-29 10:39:25 -07:00
Nikolaj Bjorner
c0694ae33a deal with memory leak during shutdown 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 10:39:07 -07:00
Nuno Lopes
bc8cd7ff55 remove a few random mem allocs 2018-06-29 18:34:17 +01:00
Lev Nachmanson
d80f6e3222 regression failures fixes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 09:57:29 -07:00
Nikolaj Bjorner
cbc5aaad2c strengthen simplification of to_int such that #1608 is handled during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 09:44:54 -07:00
Nikolaj Bjorner
1e67717d75 log with unsigned characters to avoid malformed strings as in #1712 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 09:11:44 -07:00
Nikolaj Bjorner
7e29cc0b12 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-29 08:52:44 -07:00
Nikolaj Bjorner
c429455f10 visit parameters during occurs count 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 08:52:25 -07:00
Lev Nachmanson
4641d5f32d fixes to get z3test.py back on track etc 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 21:30:41 -07:00
Nikolaj Bjorner
3da8fe4136
Merge pull request #1710 from agurfinkel/deep_space 
Deep space
 2018-06-28 16:57:02 -07:00
Lev Nachmanson
40a363d249 Nikolaj's changes in rationals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 16:22:40 -07:00
Lev Nachmanson
c2f3428373 name change 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 15:02:23 -07:00
Lev Nachmanson
fd8f972cac grammar 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 13:53:38 -07:00
Arie Gurfinkel
9b578083f5 Avoid non-linear arithmetic in qgen 2018-06-28 16:50:43 -04:00
Lev Nachmanson
c986dfe97b change in an SASSERT 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 13:41:59 -07:00
Arie Gurfinkel
5e87d7c4a3 Formatting: move q3 parameters closer together 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
bd63458778 Shuffle assumptions on every call 
Order of assumptions appears to make a huge difference on what lemmas
are discovered. Shuffling the assumptions ensures that the solver
is never stuck with any bad order.
 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
6422fa3739 Fix arithmetic equality solver in qgen 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
41a05e9d58 Add methods to print pob 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
a63e4b48ca Fix order of arguments when normalizing a conjunction 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
a8c9e3a837 Bug fix in qgen 2018-06-28 15:38:50 -04:00
Arie Gurfinkel
e8e27f0daf Don't simplify bounds when normalizing a lemma 2018-06-28 15:38:50 -04:00
Lev Nachmanson
2087ee3fb0 restore some code that was removed during the rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 11:59:01 -07:00
Nikolaj Bjorner
f7512d6d5c
Merge pull request #1709 from nunoplopes/master 
MAM: check soft limits before calling the interpreter
 2018-06-28 10:31:00 -07:00
Nuno Lopes
46799cb3f0 MAM: check soft limits before calling the interpreter 2018-06-28 18:25:22 +01:00
Nikolaj Bjorner
18121e5241
Merge pull request #1707 from agurfinkel/deep_space 
Deep space
 2018-06-28 05:38:25 -07:00
Nuno Lopes
5de6628a5d remove spurious copies and inc_refs around ref_vector 2018-06-28 10:31:38 +01:00
Arie Gurfinkel
4abab8aaf5 Fix bug in qe_term_graph 
In merge, parents of A instead of parents of B were traversed.
Among other things, it created stale marks that caused an
infinite loop in to_lits()
 2018-06-27 22:54:55 -04:00
Arie Gurfinkel
0e5434ce0c Debug prints 2018-06-27 22:49:36 -04:00
Arie Gurfinkel
7c924c49f6 Do not evaluate quantified formulas in a model 2018-06-27 22:49:36 -04:00
Arie Gurfinkel
704c19920d Only 10 levels of weakness 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
4339722e98 Fix segfaults in qgen 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
49e9480928 Fix lemma_as_cti option 
Use negation of a lemma as a proof obligation. This speeds up discovering
bad lemmas that do not contain some reachable states.
 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
bc6604441b Helpers in model_core 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
d7234dc039 Inactive debug code 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
2b4d92821a Avoid crashing on cancel 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
f6dcc6fc72 API to find pob in pob_manager 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
5bc57238a6 Track whether pob is in pob_queue 
pob_queue is a priority queue. Changing a pob while it is in the queue might change
the priority. This is a source of subtle bugs. The flag is ment to help defend
against this issues in the future.

As a side-effect, a pob that is already in the queue will be silently not added
to it, and a new version of a pob might be created if a version being looked
for is already in the queue.
 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
c00c6b4285 Pobs are always managed 
Removed options to allow unmanaged pobs.
Other minor cleanups.
 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
1910b4c87c Rename pobs into pob_manager 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
176c0a97f7 Gracefully handle absence of a proof 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
d9100437ce Weakness of the lemma independent of the pob 
Lemma inherits its weakness score from the pob. However,
pob's weakness might be reset or changed for some other reason.

To avoid affecting the lemma, the weakness is copied on
construction.
 2018-06-27 22:49:35 -04:00
Nikolaj Bjorner
eabe91cdef Merge branch 'master' of https://github.com/z3prover/z3 2018-06-27 17:05:52 -07:00