mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
18923 commits 49 branches 53 tags 182 MiB
Commit graph

18923 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
483508d257 move all saturation functionality into saturation.cpp, differentiate basic multiplication by -1, 1 from other powers of 2. 2023-12-31 14:42:10 -08:00
Nikolaj Bjorner
7bd7faa722 add proof checker plugin 
fixes to monomials
 2023-12-31 05:30:21 -08:00
Nikolaj Bjorner
32825a26cb Update hints to carry premises 2023-12-30 17:29:36 -08:00
Nikolaj Bjorner
f328ddf88e Add monomials container to keep track of non-linear multipliers 
Refine constraints to include an unfolded version of them where multiplier definitions are expanded.
 2023-12-30 14:14:12 -08:00
Nikolaj Bjorner
78f32401ac bugfixes 2023-12-29 18:11:40 -08:00
Nikolaj Bjorner
03e012c1d8 bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-29 15:13:11 -08:00
Bruce Mitchener
d66df2616f
Fix some typos. (#7075) 2023-12-29 15:20:06 +00:00
Nikolaj Bjorner
97225b7d8f bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-28 21:02:09 -08:00
Nikolaj Bjorner
15f36f95a4 use constraint_id type within viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-28 18:00:11 -08:00
Nikolaj Bjorner
91b9d78cd3 bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-28 17:36:42 -08:00
Nikolaj Bjorner
bd93379346 add validation to polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-28 15:52:30 -08:00
Nikolaj Bjorner
20afc55b41 misc bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-28 14:24:52 -08: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
Nikolaj Bjorner
c0da732cea more proof hint information 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-27 22:48:11 -08:00
Nikolaj Bjorner
20958f1468 add qed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-27 22:26:20 -08:00
Nikolaj Bjorner
25863d4682 tidy a bit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-27 22:21:30 -08:00
Nikolaj Bjorner
47b2113260 track proof hints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-27 16:34:00 -08:00
Nikolaj Bjorner
ac8efad7e1 bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-27 16:06:27 -08:00
Nikolaj Bjorner
737913b67e bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-27 14:00:28 -08:00
Nikolaj Bjorner
6103c9d718 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-27 11:29:42 -08:00
Nikolaj Bjorner
9cce1ff836 finish explanation code for viable 2023-12-26 14:17:24 -08:00
Nikolaj Bjorner
6466345755 viable revisit v1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-26 14:10:43 -08: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
9cd838f705 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-25 17:38:16 -08:00
Nikolaj Bjorner
b82d4c352b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-25 16:38:45 -08:00
Nikolaj Bjorner
f51e200dd8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-25 16:37:25 -08:00
Nikolaj Bjorner
4f60dd7f3a remove v1 code 2023-12-25 11:32:39 -08:00
Nikolaj Bjorner
f0c23f9b7b make offset_claim structured similar to fixed_claim 2023-12-25 11:19:37 -08:00
Nikolaj Bjorner
b1072d0a1c hoist out fixed-bits reasoning into self-contained module 
without dependencies on viable entries
 2023-12-25 10:59:27 -08:00
Nikolaj Bjorner
658f079efd remove literal polarity from dependencies 2023-12-25 09:39:51 -08:00
Nikolaj Bjorner
5398429c21 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-25 09:27:51 -08:00
Nikolaj Bjorner
071836d5ed na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-25 09:23:57 -08:00
Nikolaj Bjorner
cf6d7d2c4b move extract saturation as an axiom 2023-12-24 05:15:59 -08:00
Nikolaj Bjorner
50358e43ed updates to saturation 2023-12-23 16:59:17 -08:00
Nikolaj Bjorner
ebe5ebf0ae Add branch and bound solver, for fun 2023-12-23 11:58:29 -08:00
Nikolaj Bjorner
fbbad72c29 use lazy explanation function for slices, use euf-bv-plugin to extract slices 2023-12-23 11:10:18 -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
5bbec43235 working on sub/super slices 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 17:45:23 -08:00
Nikolaj Bjorner
9a7e50c1e8 separate egraph functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 16:17:53 -08:00
Nikolaj Bjorner
8eea2488e2 separate egraph functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 15:57:28 -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
Nikolaj Bjorner
d183ac23d0 don't rely on initializer list implementations, there are no constructors in the standard 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 10:48:37 -08:00