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

20005 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes
dda0c8ff42 array theory: use expr_ref for mk_default() so it doesnt leak if internalize throws 
like on timeout/memout
 2023-08-20 22:28:57 +01:00
Lev Nachmanson
9b672bc5cc remove tracking of bounds 2023-08-20 10:10:48 -07:00
Nuno Lopes
57c667e355 remove unused code 2023-08-20 15:16:47 +01:00
Nuno Lopes
a694d27557 revert removal of virtual destructor of relevancy_eh since clang doesnt play along 2023-08-20 14:20:20 +01:00
Nuno Lopes
8210aafb69 ast compare_nodes: fail faster when comparing quantifier expressions 2023-08-20 14:09:04 +01:00
Nuno Lopes
c469c6e1d5 attempt to fix clang buildbots 2023-08-20 13:39:15 +01:00
Nuno Lopes
28884b398c remove unneeded virtual destructor (optimization) 2023-08-20 12:57:47 +01:00
Nuno Lopes
3b546b2348 smt_context: we can't assert that the resource limits were exceeded on cancel_exception 
It happens sometimes that e.g. the internalizer goes above the soft memory limit
But since it's only by a small amount, when the exception propagates back to the context, some stuff
has been freed already and we are not longer above the memory threshold
Just delete these asserts
 2023-08-20 10:34:28 +01:00
Nuno Lopes
5d33805c8b optimize ~relevancy_propagator_imp() so it just dec refs the exprs in the trail 
It avoid doing all the funky watch stuff
One extreme Alive2 test case goes from 40s to 28s :)
 2023-08-20 10:07:56 +01:00
Nikolaj Bjorner
5e3df9ee77
Arith min max (#6864) 
* prepare for dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* snapshot

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* pass in u_dependency_manager

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* address NYIs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactoring names

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* eq_explanation update

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add outline of bounds improvement functionality

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix unit tests

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove unused structs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* convert more internals to use u_dependency instead of constraint_index

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* convert more internals to use u_dependency instead of constraint_index

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remember to push/pop scopes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use the main function for updating bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove reset of shared dep manager

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disable improve-bounds, add statistics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-19 17:44:09 -07:00
Nikolaj Bjorner
c3b344ec47 fix #6865 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-18 16:51:58 -07:00
Lev Nachmanson
610313946d split free vars in nla 2023-08-18 12:36:14 -07:00
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
Nikolaj Bjorner
a8c4384536 download 20.04 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-18 07:58:48 -07: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
Nikolaj Bjorner
59b56f2ce7 update unit test to be compatible with C++ vs C exception semantics #6537 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 19:13:50 -07:00
Nikolaj Bjorner
8aa35f7fdb remove package lock 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 18:54:00 -07:00
Nikolaj Bjorner
63f18a1d99 #6822 - change to 2.31 for nuget packaging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 18:47:05 -07:00
Nikolaj Bjorner
73724f9cab lines that go away 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 18:45:49 -07:00
Lev Nachmanson
252a30e727
use param_ref in nla_solver (#6862) 
* use param_ref in nla_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add parameters

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add parameters

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* replace nla_setting by command line parameters

* delete nla_setting.h

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 18:44:27 -07:00
Nikolaj Bjorner
63ea8efcfb remove output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 15:20:12 -07:00
Nikolaj Bjorner
2dbf9bcab2 Merge branch 'master' of https://github.com/z3prover/z3 2023-08-17 15:18:36 -07:00
Nikolaj Bjorner
51df7b75ce fix 6800 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 15:18:22 -07: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
Hari Govind V K
1be692002d
split on all ite terms. fix #6852 (#6859) 2023-08-16 10:07:30 -07: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