mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity
17718 commits 23 branches 48 tags 157 MiB
Commit graph

17718 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson 25f103db1a rm_lp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson 527f0d1242 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson a38be43264 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson 97c1ba4641 rm get_column_in_lu_mode 2023-03-08 10:27:05 -08:00
Lev Nachmanson ea16f6608c before rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Hari Govind V K f7c9c9ef72
fix unsound slice criteria (#6625) 
* rename for readability

* bug fix #6617. Don't slice op args that are values
 2023-03-06 19:28:22 -08:00
Nikolaj Bjorner 42076a3c13 bug fixes to new core, elim_predicates and elim_unconstrained 2023-03-05 22:26:37 -08:00
Nuno Lopes b9a87e493b minor code simplifications 2023-03-05 19:08:41 +00:00
Lev Nachmanson 92fe8c5968 restore the previous state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-03 18:30:17 -08:00
Lev Nachmanson ff1dc0424c rm lp_solver 2023-03-03 16:32:49 -08:00
Lev Nachmanson 5e4bca3d26 small removals 2023-03-03 15:58:25 -08:00
Lev Nachmanson 2dd30fa350 rm lp_primal_simplex 2023-03-03 15:44:50 -08:00
Lev Nachmanson 8989e10e71 rm lp_dual_simplex 2023-03-03 15:41:30 -08:00
Lev Nachmanson d2e8297d41 remove includes of lp_dual_simplex 2023-03-03 15:38:47 -08:00
Lev Nachmanson 2ec09944d7 removals 2023-03-03 15:32:44 -08:00
Lev Nachmanson a44772424c more removals 2023-03-03 15:30:15 -08:00
Lev Nachmanson 8db2f1409b lp_dual_simplex.cpp removed from CMakeLists.txt 2023-03-03 15:27:57 -08:00
Lev Nachmanson cd24c99739 remove a lp_primal_simplex.cpp from CMakeLists 2023-03-03 15:26:06 -08:00
Lev Nachmanson f986ac6a75 remove mps_reader 2023-03-03 14:50:10 -08:00
Hari Govind V K 55d45e0c0c
bug fix. Prevent resetting gg stats #6062 (#6618) 2023-03-03 12:32:23 -08:00
Nikolaj Bjorner b82d177276 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-03 11:26:13 -08:00
Nikolaj Bjorner aa75ba8a6b remove parenthesis 2023-03-01 21:03:41 -08:00
Nikolaj Bjorner fd97be0e3e move sat.smt.proof.check_rup into solver.proof.check_rup #6616 2023-03-01 21:03:27 -08:00
Nikolaj Bjorner 94b79eefea add back max_occs parameter dependency to solve-eqs 2023-03-01 20:40:22 -08:00
Nikolaj Bjorner acd2eaa390 add (disabled) code path to enable nested conjunctions 
for experiments with disabling flat-and-or dependency
 2023-03-01 20:39:39 -08:00
Nikolaj Bjorner 46d37b6e30 fix #6615 
make rewriting exception safe (for cancelation).
The state during restart in smt_context is not exception safe.
 2023-03-01 17:30:07 -08:00
Nikolaj Bjorner 027770930e fix bug in quasi macro identification: require quantifiers 2023-03-01 17:03:15 -08:00
Nikolaj Bjorner 25d45a3500 fixes and tests for arith-sls 2023-02-28 17:40:09 -08:00
Nikolaj Bjorner e87fa1c299 remove stale file 2023-02-28 17:40:08 -08:00
Nikolaj Bjorner 79d47eb302 add preprocessor parameter whether to use bound simplifier 2023-02-28 17:40:08 -08:00
Nikolaj Bjorner 76aad689c6 Update smt_context_pp.cpp 
print units in statistics
 2023-02-28 17:40:08 -08:00
Nikolaj Bjorner 5974a2dc58 remove m_b from lar_core_solver 
the column vector is pure overhead for the way the lar solver uses lp.
Some other solver modules use column vectors b and integrate with the lp_core_solver_base. The interaction model should be reviewed.
Unused solvers should be removed to make it easier to maintain this code.
 2023-02-28 17:40:08 -08:00
Kevin Phoenix 1a9990a92f
Use sys.getdefaultencoding() instead of sys.stdout.encoding (#6612) 2023-02-28 11:46:10 -08:00
Julian Parsert 6e7d80633d
Documentation on how to add z3 to CMake project using FetchContent and documentation to recdef function. (#6613) 
* Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort*

* added documentation to recdef function

* added a section in the README-CMake.md that explains how z3 can be added to a CMake project as a dependency

---------

Co-authored-by: Julian Parsert <julian.parsert@uibk.ac.at>
 2023-02-28 11:44:21 -08:00
Arie Gurfinkel 358caa85e2
Merge pull request #6608 from hgvk94/bugfix 
fix #6543. don't assume order on bindings
 2023-02-24 10:23:57 -05:00
hgvk94 828fff9684 fix #6543. don't assume order on bindings 2023-02-23 17:35:55 -05:00
Nikolaj Bjorner 146f0eae06 wip - arith local search 2023-02-20 12:17:14 -08:00
Nikolaj Bjorner 4aa05b2b57 remove limiting error mode #6600 2023-02-20 12:16:43 -08:00
Nikolaj Bjorner 755b517001 fix #6600 
ensure that semantics of last-indexof(t,"") = len(t)
 2023-02-19 14:02:37 -08:00
Nikolaj Bjorner 0758c93086 fix #6591 
- add check for lambdas similar to as-array in context of quantifiers. MBQI is not a decision procedure for this combination and can then incorrectly conclude satisfiabiltiy.

Scenario

The formula contains assertions
 - bv = (map or (lambda ..) t)
 - forall y (not (select bv (pair s y)))

Since bv is extensionally equal to a term that depends on a lambda, MBQI cannot just take the current finite approximation of bv when checking the quantifier for satisfiability.
 2023-02-19 11:09:52 -08:00
Nikolaj Bjorner 6454e7fa3f apply rewriting if result of destructive equality resolution is simplified 2023-02-19 11:03:04 -08:00
Nikolaj Bjorner bc6037464d clean up build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-19 10:08:31 -08:00
Nikolaj Bjorner 9b6ac45e02 compile warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-19 10:03:38 -08:00
Nikolaj Bjorner 6352340478 update do logging 2023-02-19 09:59:33 -08:00
Nikolaj Bjorner a6eed9f00c Update api.cpp 
fix test
 2023-02-18 18:43:20 -08:00
Nikolaj Bjorner cb81473260 add destructive equality resolution to the main simplifier. 2023-02-18 17:54:26 -08:00
Nikolaj Bjorner c0f80f92ba deal with compiler warnings (unused variables etc) 2023-02-18 17:53:37 -08:00
Nikolaj Bjorner 6092bf534c fix #6599 2023-02-18 14:18:02 -08:00
Nikolaj Bjorner daeaed1e82 revert debug only changes to sat-solver 2023-02-18 14:13:40 -08:00
Nikolaj Bjorner c5e33b79b5 wip - arith sls 
overhaul to tier inequalities with Boolean variables instead of literals
 2023-02-18 14:11:48 -08:00