mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
18017 commits 24 branches 48 tags 158 MiB
Commit graph

1451 commits

Author SHA1 Message Date
Nikolaj Bjorner
85db8163fa move allocator to memory_manager and std_vector to vector 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-19 13:57:28 -07:00
Lev Nachmanson
c5cfd62e0a remove dead code related to nla unit propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-19 10:56:09 -07:00
Lev Nachmanson
cf63e75898 using structures from util in lp_bound_propagator 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-18 13:25:24 -07:00
Lev Nachmanson
af8d192392 add an include 2023-09-17 13:14:36 -07:00
Lev Nachmanson
10095a30b7 add an include file 2023-09-17 12:25:11 -07:00
Lev Nachmanson
66f6a0327f change type of m_ibounds to std::vector 2023-09-17 11:00:48 -07:00
Lev Nachmanson
30b743d7b3 refactor propagat_monic 2023-09-17 10:45:54 -07:00
Lev Nachmanson
7353d7fb4d fix dep calculations in lp_bound_propagator 2023-09-17 06:48:12 -07:00
Lev Nachmanson
77e56b0a69 debug 2023-09-16 13:54:14 -07:00
Lev Nachmanson
c240f62ca8 is_linear does not check for is_big 2023-09-15 17:44:10 -07:00
Lev Nachmanson
4cfba9787b debug lp_bound_propagator 2023-09-15 17:41:10 -07:00
Lev Nachmanson
a55aa1a648 add a comment 2023-09-14 19:29:48 -07:00
Lev Nachmanson
b3673d491e fix the build for gcc 2023-09-14 19:20:47 -07:00
Lev Nachmanson
cbad61ba2e propagate monics with lp_bound_propagator 2023-09-13 14:27:34 -07:00
Lev Nachmanson
c309d52283 runs a simple test 2023-09-13 08:12:00 -07:00
Lev Nachmanson
c050af922f fixing the bugs 2023-09-07 15:59:20 -07:00
Lev Nachmanson
c43b99daae renaming 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-07 11:57:20 -07:00
Lev Nachmanson
47b64e689c restore the lemma scheme 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-07 11:33:14 -07:00
Lev Nachmanson
288e66de59 restore m_crossed* and create lemmas 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-06 09:27:30 -07:00
Lev Nachmanson
41f59cb1ed propagate monomial is nla 2023-09-05 18:49:59 -07:00
Lev Nachmanson
318d7d7564 fixes a bug 2023-09-01 11:32:26 -07:00
Lev Nachmanson
d3258e7084 propagate lineal monomial 2023-09-01 11:18:03 -07:00
Lev Nachmanson
5509b468e9 handle monomial_bounds::unit_propagate() 2023-08-31 17:35:41 -07:00
Nikolaj Bjorner
ff3268e636 move unit propagation into monomial_bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-31 14:32:05 -07:00
Nikolaj Bjorner
c2cbe72b64 sketch linear monomial propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-31 11:49:05 -07:00
Nikolaj Bjorner
38b131386d add stubs for monomial unit propagation 2023-08-30 17:21:48 -07:00
Nikolaj Bjorner
e8929041b8 fixing calls, signs 2023-08-22 09:29:12 -07:00
Lev Nachmanson
61a7c6b28d init m_literal_vec 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-08-21 17:11:55 -07:00
Lev Nachmanson
9aeaed8f53
Merge branch 'master' into nl_branches 2023-08-21 16:15:20 -07:00
Lev Nachmanson
9b672bc5cc remove tracking of bounds 2023-08-20 10:10:48 -07: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
Lev Nachmanson
610313946d split free vars in nla 2023-08-18 12:36:14 -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
51df7b75ce fix 6800 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 15:18:22 -07:00
Nikolaj Bjorner
33c35b0c31 fix #6851 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-13 14:49:25 -07:00
Nikolaj Bjorner
6366f8f6b2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-13 14:05:07 -07:00
Lev Nachmanson
eb817f779d small change in factor to support TRACE 2023-08-11 12:04:08 -10: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
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
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
403340498c format 2023-07-31 19:41:11 -07:00
Nikolaj Bjorner
f0184c3fde update format and checker for implied-eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-27 13:21:45 -07:00
Lev Nachmanson
bfc37bd266 add to m_touched_rows only when bound 
propagation is required
 2023-07-17 08:00:01 -10:00
Lev Nachmanson
fd5902f76e relax an assertion in int_solver::patcher 2023-07-16 11:55:42 -10:00