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

19393 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath d567d3b7f2 rename to try_congruence and add conditions 2023-08-18 17:11:46 +02:00
Jakob Rath 1316e1c881 fix splitting in merge 2023-08-18 17:03:49 +02:00
Jakob Rath 8a8afcdcb8 try_ugt_eq restores 6800 2023-08-18 16:24:06 +02:00
Jakob Rath b4902f374b slicing equivalent vars + explain 2023-08-18 16:21:59 +02:00
Jakob Rath e09636065b don't crash on null_literal 2023-08-18 15:30:39 +02:00
Jakob Rath 5bd35d764f fix collect_fixed 2023-08-18 15:26:09 +02:00
Jakob Rath efe0fa8e15 put add_var on the trail 2023-08-18 15:18:55 +02:00
Jakob Rath 1033c7e536 slicing replay was utterly broken 2023-08-18 15:10:23 +02:00
Jakob Rath d3b5974448 shortcut in add_value 
otherwise, with literal x == a for constant a, we will create unnecessary value nodes.
(because slicing will propagate x := a to the solver, which calls add_value in turn)
 2023-08-18 15:00:00 +02:00
Jakob Rath 2d0120c621 Merge some intermediate slices 
In particular, this ensure propagates of values to extracted variables.
(previously it could happen that x = y[h:l], y is assigned in the
solver, but x is not propagated; because only base slices have been
merged.)
 2023-08-18 14:56:48 +02:00
Jakob Rath 49ca2d983d remove abandoned code 2023-08-18 14:55:40 +02:00
Jakob Rath cb14cb5743 (abandoned) attempt to propagate values upwards 2023-08-18 14:52:48 +02:00
Jakob Rath 9bffb34ce1 helpers 2023-08-18 14:47:29 +02:00
Jakob Rath 93592ea3f2 scoped_set_verbosity_level 2023-08-17 18:02:57 +02:00
Jakob Rath dcb0d27dd7 Use get_bit instead of bitwise_and 2023-08-17 18:02:15 +02:00
Jakob Rath 19c1c7aa73 minor comments, skolem = false 2023-08-17 17:59:40 +02:00
Jakob Rath 3e7f7ef605 egraph comment, remove unneeded check 2023-08-17 17:57:42 +02:00
Jakob Rath f8c9ed1d90 Revisit ule_constraint simplifications and add unit test for this 
If we can be certain of simplification results,
it is easier to recognize patterns for fixed bits and similar.
 2023-08-17 17:46:34 +02:00
Jakob Rath 6593754cd6 enable fixed bits in slicing 2023-08-17 17:37:11 +02:00
Jakob Rath 996012adb1 logging fix 2023-08-17 17:32:08 +02:00
Jakob Rath 0da1d9b218 display actual content of 'inequality' instances 2023-08-17 17:29:51 +02:00
Jakob Rath 9600f812a6 Functions to extract fixed bits for slicing 2023-08-17 17:26:19 +02:00
Jakob Rath c95ff56d2d slicing: change how values are tracked 
Do not eagerly merge equivalence classes with the same constant value.

Reason:
- when we split a value slice, the subslice might already exist in the
  egraph and already have subslices itself, which breaks assumptions in
  split/split_core.
- introduces unnecessary splits

Now:
- wrap constants into fresh function symbol before creating the enode
- check value compatibility in on_merge callback instead
- track pointer to value_node for each enode, and update it in on_merge
 2023-08-17 17:14:18 +02:00
Jakob Rath 08928d041a explain_equal: jumping to root without explanation is wrong 2023-08-17 11:46:09 +02:00
Jakob Rath 53dc31989a relax assertion 2023-08-17 09:32:47 +02:00
Jakob Rath bc6f0729a0 Add lemma: y = x[h:l] & y != 0 ==> x >= 2^l 2023-08-16 09:58:56 +02:00
Jakob Rath afc292e5db Add parameter polysat.max_iterations for debugging 2023-08-16 09:55:21 +02:00
Jakob Rath 062ca92ebe Switch between overflow representations with polysat.bvumulo=1/2 2023-08-16 09:54:04 +02:00
Jakob Rath 11b582cce7 Add rational::next_power_of_two 2023-08-16 09:48:32 +02:00
Jakob Rath 0bfebe3de1 Enable conflict logger with polysat.log_conflicts=true 2023-08-16 09:40:16 +02:00
Jakob Rath 20ab0bc13a Invoke debugger if VERIFY fails in debug mode 2023-08-16 09:36:28 +02:00
Jakob Rath 1f640b96c9 compile unit tests 2023-08-14 14:00:41 +02:00
Jakob Rath 32d66951a8 bugfix 2023-08-11 14:52:26 +02:00
Jakob Rath 81609ed043 viable now takes into account fixed bits from slicing 2023-08-11 14:51:24 +02:00
Jakob Rath 586dcba661 slicing::collect_fixed should start at low-order base slice 2023-08-11 14:49:17 +02:00
Jakob Rath 89f0fb05a5 forgot to commit CMakeLists 2023-08-08 17:54:33 +02:00
Jakob Rath f9cbee3b3d explain_fixed is currently just explain_value for a slice 2023-08-08 17:26:52 +02:00
Jakob Rath 6eb81fbb9d use struct 2023-08-08 17:19:46 +02:00
Jakob Rath 3573305917 no need to keep an enode_pair, since the other is always the root 2023-08-08 17:13:05 +02:00
Jakob Rath 99a078dd69 add note on current example 2023-08-08 16:21:07 +02:00
Jakob Rath 5ec11c591f slicing-conflict debug output 2023-08-08 16:05:36 +02:00
Jakob Rath 46a794ff67 slicing with fixed bits (wip) 2023-08-08 16:04:21 +02:00
Jakob Rath f22ed9002f tab -> space 2023-08-08 15:44:44 +02:00
Jakob Rath 63c41c3e04 Use struct fixed_bits_info instead of separate arguments 
and track sat::literal as justifications rather than viable::entry
(we won't have a viable::entry for fixed bits coming from slicing)
 2023-08-08 15:40:57 +02:00
Jakob Rath e832325a8b viable::entry::refined can be a boolean flag 
because we always copy the 'src' from the original entry to the refined one
 2023-08-08 14:35:26 +02:00
Jakob Rath 036a3f31ca call m_egraph.merge() at a single point 2023-08-07 17:56:43 +02:00
Jakob Rath d36262d731 fix unit tests 2023-08-07 17:38:00 +02:00
Jakob Rath 4b4f0558b4 no need to introduce names for zero_ext/sign_ext arguments 2023-08-07 15:44:06 +02:00
Jakob Rath 5c53f588b7 Additional shortcuts for extract/concat 2023-08-07 15:33:51 +02:00
Jakob Rath bc0119f333 Treat constraints of the form "x = val" more like variable assignments 2023-08-07 15:28:17 +02:00