Nikolaj Bjorner
6366f8f6b2
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-13 14:05:07 -07:00
Nikolaj Bjorner
9804ba9fd2
Merge branch 'master' of https://github.com/z3prover/z3
2023-08-12 20:34:21 -07:00
Nikolaj Bjorner
41cac5f69e
remove output
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-12 20:34:15 -07:00
Lev Nachmanson
eb817f779d
small change in factor to support TRACE
2023-08-11 12:04:08 -10: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
Lev Nachmanson
a932e596eb
add a constructor from a variable to factor
2023-08-10 08:34:53 -10:00
Nikolaj Bjorner
a6ab0a7d49
formatting hygiene
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-08 13:50:49 -07: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
Lev Nachmanson
a7966dc436
remove an assert
2023-08-07 14:55:13 -10:00
Lev Nachmanson
858eebca82
more efficient column_is_fixed
2023-08-07 14:55:13 -10:00
Lev Nachmanson
0fbf8f92f5
delete remove_fixed_vars_from_base() from
...
int_solver
2023-08-07 14:55:13 -10:00
Nikolaj Bjorner
c3a373e225
format
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-07 14:55:13 -10:00
Lev Nachmanson
0c98c755ba
new equality propagation scheme, etc
2023-08-07 14:55:13 -10:00
Nikolaj Bjorner
125787c458
remove dead code
2023-08-07 11:22:34 -07: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
Jakob Rath
aa81f6c9fb
Propagate value assignments discovered by the slicing e-graph
2023-08-07 15:20:04 +02:00
Jakob Rath
3fe591e5bb
Also print original exprs for polysat unsat core
2023-08-07 14:39:45 +02:00
Hari Govind V K
dd0b0b47b8
fix #5925 ( #6846 )
2023-08-04 15:18:16 -07:00
Nikolaj Bjorner
84520d53ea
remove out
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-04 11:33:39 -07:00
Nikolaj Bjorner
b0055df4ab
revert arithmetic final check to original order
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-04 10:48:44 -07:00
Jakob Rath
2a2015f61d
fix bit width of extract on constants
2023-08-04 11:10:49 +02:00
Jakob Rath
d62aa82762
track pvar_kind
2023-08-04 10:12:50 +02:00
Lev Nachmanson
f58b703ac5
u_set replaced by indexed_uint_set ( #6841 )
...
* replace u_set by indexed_uint_set
* replace u_set by indexed_uint_set
* create insert-fresh and insert for indexed_uint_set to make use cases with non-fresh inserts easier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* update nightly to pull arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* update nightly to pull arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixing the build of lp_tst
* update nightly to pull arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* replace u_set by indexed_uint_set
* replace u_set by indexed_uint_set
* fixing the build of lp_tst
* remove unnecessery call to contains() before
insert to indexed_uint_set
* formatting, no check for contains()
in indexed_uint_set, always init m_touched_rows to nullptr
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-03 16:01:27 -07:00
Nikolaj Bjorner
4637339091
update model validate to include arithmetic
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-03 15:51:29 -07:00
Nikolaj Bjorner
23da36126a
update nightly to pull arm
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-03 11:01:49 -07:00
Nikolaj Bjorner
3df6cd2c5f
update nightly to pull arm
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-03 10:26:12 -07:00
Nikolaj Bjorner
4bfe9a895a
update nightly to pull arm
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-03 10:04:23 -07:00
Nikolaj Bjorner
7b36563196
create insert-fresh and insert for indexed_uint_set to make use cases with non-fresh inserts easier
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-03 09:48:07 -07:00
Jakob Rath
63e81e2bb0
fix zero_ext constraint (2)
2023-08-03 15:16:27 +02:00
Jakob Rath
6e9f07e7c5
temporary fix
2023-08-03 15:03:09 +02:00
Jakob Rath
1d9322b5ae
slicing bugfixes
2023-08-03 14:53:14 +02:00
Jakob Rath
d42d253068
fix
2023-08-03 14:48:42 +02:00
Jakob Rath
13f000942a
fix viable
2023-08-03 11:41:13 +02:00
Jakob Rath
b72a0ed4c8
notes
2023-08-03 10:30:10 +02:00
Jakob Rath
e7e025a2fc
rename to log_start for clarity
2023-08-03 10:25:32 +02:00
