mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity
18752 commits 23 branches 48 tags 156 MiB
Commit graph

18752 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 2c55aa5466 remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-17 18:04:08 -08:00
Lev Nachmanson d084a19630 take care of strategy undecided, Nikolaj's comments 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-17 14:17:07 -10:00
Lev Nachmanson 6e9a938533 Merge branch 'master' of https://github.com/z3prover/z3 2024-01-17 14:02:38 -10:00
Lev Nachmanson c591a7a3e7 force int bound on int columns, call term_is_int() after subst 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-17 13:53:59 -10:00
Nikolaj Bjorner fef1596c81 pin expression passed to validate_eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-17 15:11:06 -08:00
Nikolaj Bjorner 4f75153186
Update z3_api.h 
Updated doc https://github.com/Z3Prover/z3/discussions/7087
 2024-01-17 13:53:38 -08:00
Nikolaj Bjorner c340233df6 fix #7081 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-16 10:31:31 -08:00
Nikolaj Bjorner afba43a5a7 fix #7085 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-16 10:18:46 -08:00
Nikolaj Bjorner 4ff352fcac fix #7084 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-15 08:49:14 -08:00
Lev Nachmanson 91ca55e5ad change the definition of Gomory row 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-14 13:37:30 -10:00
Lev Nachmanson d8df203622 remove an unused declaration 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-13 19:11:17 -10:00
Lev Nachmanson e2fb4fbd38 fix dependencies for Gomory polarity 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-13 19:01:21 -10:00
Lev Nachmanson 2eadcf0872 avoid duplicate explanations 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-12 15:49:21 -10:00
Lev Nachmanson 7d7fef061f add explanations and fix polarity 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-12 15:28:16 -10:00
Nikolaj Bjorner ddf2eb57d6 deleted parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-12 10:42:08 -08:00
Nikolaj Bjorner 3381fd2b52 spell check from https://github.com/microsoft/z3guide/pull/165 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-12 09:57:46 -08:00
Nikolaj Bjorner 27171591d1
Update sat_params.pyg 
spellcheck from https://github.com/microsoft/z3guide/pull/165
 2024-01-12 09:49:56 -08:00
Nikolaj Bjorner 59b18d4a14 create as_bin as_hex wrappers for display 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-12 09:19:22 -08:00
Lev Nachmanson 999e67df0d address Nikolaj's comments in Gomory cut 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-11 16:49:10 -10:00
Lev Nachmanson 2d24436582 remove a blank line 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-11 13:42:35 -10:00
Lev Nachmanson 2b974a0f1d do not delay update for the polar case 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-11 13:39:37 -10:00
Lev Nachmanson 2ac866a8d0 take the coefficient from cut_result, not lia 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-11 12:10:37 -10:00
Nikolaj Bjorner 1b3929099b try to remove version spec 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-11 13:36:07 -08:00
Nikolaj Bjorner b239371265 try to remove version spec 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-11 13:30:42 -08:00
Nikolaj Bjorner aa4e1b34bb update Julia versions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-11 13:15:45 -08:00
Nikolaj Bjorner 955c80e98b import updates from poly branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-10 19:42:58 -08:00
Lev Nachmanson 2ca1187b3a fix a bug in polarity 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-10 10:50:56 -10:00
Nikolaj Bjorner 75005d9077 add validation option for debugging regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-09 09:18:29 -08:00
Lev Nachmanson 2934618c50 remove simplify_inequality from gomory.cpp 2024-01-04 11:40:57 -10:00
Nikolaj Bjorner 696b70fddb fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-04 11:00:07 -08:00
Lev Nachmanson 239d68ed9c return conflict on an empty term in Gomory cuts 2024-01-03 18:56:35 -10:00
Nikolaj Bjorner b75367ffc7 port improvements to arith rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 13:57:09 -08:00
Nikolaj Bjorner a7bfdcd0ea readd big cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-02 11:17:59 -08:00
Lev Nachmanson 84997f8b21 move a TRACE statement 2024-01-01 05:25:07 -10:00
Lev Nachmanson fd2b6c62d1 bug fix in gomory polarity 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-01 05:25:07 -10:00
Bruce Mitchener d66df2616f
Fix some typos. (#7075) 2023-12-29 15:20:06 +00:00
Jakob Rath ec2b8eb4ca
Merge shared parts from polysat branch (#7063) 
* sat_literal: make constants constexpr

* dlist: rename elem -> list

* tbv: use get_bit

* additional pdd and rational tests

* egraph: callback setters take functions by value

This allows to set callbacks without defining a separate variable for
the callback lambda.

(previous usage does one copy of the function, exactly as before)

* cmake: enable compiler error when non-void function does not return value
 2023-12-28 11:11:53 -08:00
Lev Nachmanson 53c95e3627 cleanup 2023-12-28 06:00:57 -10:00
Lev Nachmanson 0728b81e9e add parameter lp_settings.m_gomory_simplify 2023-12-28 06:00:57 -10:00
Lev Nachmanson 5796e8899f use vector instead of unordered_map in gomory 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-12-28 06:00:57 -10:00
Lev Nachmanson a3529a0046 create bounds for gomory cuts with big numbers 2023-12-28 06:00:57 -10:00
Lev Nachmanson af7691224e adding the polarity bound 2023-12-28 06:00:57 -10:00
dependabot[bot] d7931b9342
Bump microsoft/setup-msbuild from 1.1 to 1.3 (#7071) 
Bumps [microsoft/setup-msbuild](https://github.com/microsoft/setup-msbuild) from 1.1 to 1.3.
- [Release notes](https://github.com/microsoft/setup-msbuild/releases)
- [Changelog](https://github.com/microsoft/setup-msbuild/blob/main/building-release.md)
- [Commits](https://github.com/microsoft/setup-msbuild/compare/v1.1...v1.3)

---
updated-dependencies:
- dependency-name: microsoft/setup-msbuild
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2023-12-26 08:41:33 +00:00
Nikolaj Bjorner ebe5ebf0ae Add branch and bound solver, for fun 2023-12-23 11:58:29 -08:00
Nikolaj Bjorner ad07e0e18d add sub and super-slice functionality directory to euf-bv-plugin 2023-12-23 10:27:54 -08:00
Nikolaj Bjorner cd331b8a56 remove reference to tactic.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 13:17:04 -08:00
Nikolaj Bjorner 7adb402a3f add missing dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 12:06:30 -08:00
Nikolaj Bjorner 5f451182f7 missing cmake list 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 12:02:24 -08:00
Nikolaj Bjorner e321643bf5 move sls core functionality to be independent of tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 12:00:52 -08:00
Nuno Lopes 606a9a7409 fix test build 2023-12-22 16:19:28 +00:00