mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 11:12:28 +00:00
Code Activity
19398 commits 49 branches 53 tags 181 MiB
Commit graph

19398 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
f66a082de9 fix #6595 2023-02-18 14:11:48 -08:00
Ding Fei
828ff98c77
fix tpl instantiation issue for mingw (#6597) 2023-02-17 09:26:45 -08:00
Nikolaj Bjorner
bd10ddf6ae wip - local search - use dispatch model from bool local search instead of separate phases. 2023-02-16 09:17:11 -08:00
Nikolaj Bjorner
ac068888e7 add trichotomy for sequence comparison. #6586 2023-02-16 08:59:55 -08:00
Nikolaj Bjorner
554a9e8efe fix #6346 2023-02-16 08:53:08 -08:00
Nikolaj Bjorner
7c08e53e94 fixes for #6590 2023-02-15 15:11:44 -08:00
Nikolaj Bjorner
c1ecc49021 wip - local search - move to plugin model 2023-02-15 13:32:30 -08:00
Nikolaj Bjorner
a1f73d3805 wip - local search - fix build 2023-02-15 08:48:37 -08:00
Nikolaj Bjorner
4f20b8e2ba wip - local search 2023-02-15 08:36:10 -08:00
Nikolaj Bjorner
8ce0c56ff5 fix #6590 2023-02-15 08:36:01 -08:00
Nikolaj Bjorner
c2fe76569f remove dependency on bool-rewriter in hoist rewriter 
deal with regression reported in
cac5052685 (commitcomment-100606067)
and unit tests doc.cpp
 2023-02-14 17:48:02 -08:00
Nikolaj Bjorner
a976b781a0 fix #6585 2023-02-14 15:33:17 -08:00
Nikolaj Bjorner
44fcf60a72 wip experiments with sls 2023-02-14 15:06:26 -08:00
Nikolaj Bjorner
9ce5fe707d track assumptions when parsing into a solver. This enables solver.from_file/solver.from_string to support assumptions/cores #6587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-14 11:09:11 -08:00
Nikolaj Bjorner
3dc91de531 fix #6582 2023-02-13 13:21:30 -08:00
Nikolaj Bjorner
2b77012993 fix build 2023-02-13 08:36:12 -08:00
Nikolaj Bjorner
52804b5c8f save on dtt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-13 08:29:32 -08:00
Nikolaj Bjorner
7956cf1201 annotate arith_sls 2023-02-12 20:55:44 -08:00
Nikolaj Bjorner
bb81bc5452 fix #6580 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-12 20:21:53 -08:00
Nikolaj Bjorner
102eee77dc patch regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-12 20:12:01 -08:00