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

17695 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner cac5052685 fixes related to #6577 
- enforce elim-and in bool-rewriter when invoking hoisting.
- make cnf tactic more resilient to non-normalized input.
- enable eliminate predicates on ground formulas
 2023-02-12 13:43:44 -08:00
Walden Yan ede9e5ffc2
[WIP] More TS Binding Features (#6412) 
* feat: basic quantfier support

* feat: added isQuantifier

* feat: expanded functions

* wip: (lambda broken)

* temp fix to LambdaImpl typing issue

* feat: function type inference

* formatting with prettier

* fix: imported from invalid module

* fix isBool bug and dumping to smtlib

* substitution and model.updateValue

* api to add custom func interps to model

* fix: building

* properly handling uint32 -> number conversion in z3 TS wrapper

* added simplify

* remame Add->Sum and Mul->Product

* formatting
 2023-02-11 15:48:29 -08:00
Nikolaj Bjorner 5e30323b1a wip - bounded local search for arithmetic 2023-02-11 15:46:39 -08:00