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

15449 commits

Author SHA1 Message Date
Jakob Rath
4dc05447ad verify model also in release mode 2023-01-25 11:42:34 +01:00
Jakob Rath
b460150f98 tried logic ALL for univariate solver 
Allows us to solve bench25 but some others turn into unknown
 2023-01-25 11:42:02 +01:00
Jakob Rath
7fbf27309b rename 2023-01-25 11:42:02 +01:00
Nikolaj Bjorner
cf1ce4cea2 promote assertion to verify so it triggers in release mode, triggers for bench15 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 20:15:40 -08:00
Jakob Rath
a2ff185187 Put (arbitrary) bound on number of refinements 2023-01-23 16:33:07 +01:00
Jakob Rath
3dc8ef6337 parity edge case 2023-01-23 15:07:35 +01:00
Jakob Rath
07de75cd12 fix and-propagation 2023-01-23 15:04:13 +01:00
Jakob Rath
58ab342029 Add missing and-lemma; fix condition on existing one 2023-01-23 14:56:46 +01:00
Jakob Rath
46147c2fc3 Fix unsoundness in ule_constraint lemma 2023-01-23 13:59:00 +01:00
Jakob Rath
c6cd35508b fix 2023-01-19 19:09:46 +01:00
Jakob Rath
2056d392ba Detect gap in has_max_forbidden 2023-01-19 13:48:06 +01:00
Jakob Rath
d1ef8029a9 simpler condition 2023-01-19 13:43:50 +01:00
Jakob Rath
f9f61249e1 debug output 2023-01-19 13:42:33 +01:00
Jakob Rath
a7ad1f0bfb fix build 2023-01-18 19:29:22 +01:00
Jakob Rath
85a8d8b005 debug output 2023-01-18 18:46:40 +01:00
Jakob Rath
905144cdbb assert 2023-01-18 18:43:41 +01:00
Jakob Rath
8385452d91 simplify interval 2023-01-18 18:40:48 +01:00
Jakob Rath
c62ba26cf4 simplify 2023-01-18 18:38:44 +01:00
Jakob Rath
3e42dbe591 Fix assertions 2023-01-18 18:30:25 +01:00
Jakob Rath
b23c1b4016 Update viable tests 2023-01-18 18:23:47 +01:00
Jakob Rath
c954e82503 assertion should hold now after recent fix 2023-01-16 16:51:16 +01:00
Jakob Rath
015fcb457c avoid warnings 2023-01-16 16:50:36 +01:00
Jakob Rath
b6f8538d20 Update parity lemmas 
p != 0  ==>  odd(r)
... added premise p != 0

parity(p) < k    ==>  r <= 2^(N - k) - 1
... do this also in the other branch
    (otherwise we hit the UNREACHABLE in bench3)
 2023-01-16 16:46:12 +01:00
Jakob Rath
26e7d0d35a We need to use expr_ref when storing expressions across add calls 
Without this, bench3 created a constraint 2^parity == x * parity which
should have been 2^parity == x * x_inv.
 2023-01-16 15:41:04 +01:00
Clemens Eisenhofer
b33911de13 Added missing minimality lemma for pseudo_inverse 2023-01-15 12:11:15 +01:00
Jakob Rath
caf624589e Accelerate interval widening in refine_equal_lin 2023-01-13 15:41:28 +01:00
Jakob Rath
057e115bbc Update op_constraint simplifications 2023-01-12 13:31:16 +01:00
Jakob Rath
0a2c69332d disable try_add_overflow_bound, add note on possible rewrite 2023-01-11 13:39:41 +01:00
Jakob Rath
fa036ae486 track clause name for debugging 2023-01-11 10:50:14 +01:00
Jakob Rath
1d349fb0e6 compile 2023-01-11 10:50:14 +01:00
Clemens Eisenhofer
7aeabe39a3 Removed remaining debug output 2023-01-11 10:32:38 +01:00
Clemens Eisenhofer
2581754c3e Forward propagation for op_constraints + optimization for left/right shift 2023-01-11 10:29:26 +01:00
Jakob Rath
1d0ad1ccc0 fix build (add conversion operator) 2023-01-10 17:18:56 +01:00
Jakob Rath
0c799524e8 try splitting x-intervals 2023-01-10 16:25:28 +01:00
Jakob Rath
49848a4298 extract function update_bounds_for_xs 2023-01-10 15:16:24 +01:00
Jakob Rath
abbe139abb Use M for 2^N 2023-01-10 14:50:11 +01:00
Jakob Rath
913aa9f43e debugging output 2023-01-10 14:33:48 +01:00
Jakob Rath
0f43c1c71d adjust_bound fails if [min,max] contains a multiple of N 2023-01-10 13:32:36 +01:00
Nikolaj Bjorner
eda25e0ebb get-assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-09 10:14:19 -08:00
Jakob Rath
b6ea9e31e5 output 2023-01-09 17:20:40 +01:00
Jakob Rath
181995a4fb extend invariant check 2023-01-09 17:16:56 +01:00
Jakob Rath
c55d316c6a Rename to get_assignment to prevent clash with class name 2023-01-09 17:15:40 +01:00
Jakob Rath
3f5e6a4bfa bugfix: don't intersect forbidden intervals if variable is already assigned 2023-01-09 17:10:18 +01:00
Clemens Eisenhofer
aafd9039db Bugfix 2023-01-09 14:14:19 +01:00
Nikolaj Bjorner
991acb0d72 add diagnostics for assertion violations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-06 13:29:24 -08:00
Clemens Eisenhofer
b1239d5276 Missing file 2023-01-05 18:05:08 +01:00
Clemens Eisenhofer
0c1c9c64eb Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2023-01-05 18:03:43 +01:00
Clemens Eisenhofer
4a6053b289 Missing univariate for pseudo-inverse 2023-01-05 18:02:21 +01:00
Jakob Rath
1002538565 insert_eval? 2023-01-05 17:41:08 +01:00
Jakob Rath
aeb6138c25 No result if there is no other interval 2023-01-05 17:21:25 +01:00