mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 17:59:24 +00:00
Code Activity
16181 commits 44 branches 52 tags 177 MiB
Commit graph

16181 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes
9a172939e0 fix logging in Z3_fpa_get_[es]bits 2021-08-29 10:58:54 +01:00
Nikolaj Bjorner
b1bc890992 fix #5515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-28 18:05:51 -07:00
Nikolaj Bjorner
e7fcbd9563 bail on first model validation failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-28 17:08:34 -07:00
Nikolaj Bjorner
4f064ee5d6 simplify based on comment from Jamie Sharp #5512 2021-08-28 17:08:34 -07:00
Nuno Lopes
e5a2f08cc9 fix logging of Z3_mk_lambda and Z3_mk_lambda_const 
In preparation of a bug report just for you @NikolajBjorner
 2021-08-29 00:37:45 +01:00
Nikolaj Bjorner
e3a83dd0dd Integrate fixes from #5512 
Pull request #5512 identifies a in line 1139 where the const-case-multiplier constructor returns false and does useless work.
In this update we also remove mk_const_multiplier because code path is subsumed by mk_const_case_multiplier.
 2021-08-28 10:46:45 -07:00
Nikolaj Bjorner
992daa6d2e #5482 
remove overly permissive filter on select_store axiom
 2021-08-27 21:03:30 -07:00
Nikolaj Bjorner
e9a30385cf remove wtm and booth 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-27 15:32:06 -07:00
Jamey Sharp
cd7a826083
bit_blaster unit tests for adder and multiplier (#5514) 
These tests cover a mix of constant and non-constant input bits.
 2021-08-27 14:19:12 -07:00
Nikolaj Bjorner
8f306c6a8f handle constants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-27 11:59:41 -07:00
Nikolaj Bjorner
09696e989e add missing lambda defs per #5509 
the result is now unknown because the nested expression contains exists, which doesn't get replaced by universal quantifier which is assumed by the legacy core.
The legacy core should not depend on universal quantifiers only, but fixing this is a risk. Workaround is to rewrite goals using forall only (replace exists by de-Morgan dual).
 2021-08-27 11:57:26 -07:00
Nikolaj Bjorner
9790a8aa43 #5507 
can't use auto-config if there are no assertions. Auto-config only works properly for one-shot mode since theories aren't loaded on demand in this solver.
 2021-08-27 09:42:40 -07:00
Nikolaj Bjorner
828fc72754 types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-26 18:55:53 -07:00
Nikolaj Bjorner
d6848175eb re-add API for creating propagator from a context for "fresh" 2021-08-26 18:12:40 -07:00
Nikolaj Bjorner
f7c1ed8273 missing this 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-26 10:41:37 -07:00
Nikolaj Bjorner
4d39af3d7b #5507 missing init 2021-08-26 09:37:06 -07:00
Nikolaj Bjorner
07c26208fa regressions from previous push 2021-08-25 18:30:50 -07:00
Nikolaj Bjorner
2daf569da6 update Bool rewriter to pull negations up 2021-08-25 17:50:49 -07:00
Nikolaj Bjorner
e6264a80ff extend macro detection to negated equivalences #5496 2021-08-25 17:47:30 -07:00
Nikolaj Bjorner
f03d756e08 missing rewrite exposed by #5498 2021-08-25 06:34:27 -07:00
Nikolaj Bjorner
17663acf75 #5482 other relevancy tracking 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner
e75b5e9513 don't copy "true" 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner
037c93b258 #5482 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner
7bae297297 #5482 
add unit propagation
 2021-08-24 11:24:31 -07:00
Nikolaj Bjorner
26db68bf2c #5482 2021-08-24 11:15:52 -07:00
Nikolaj Bjorner
e5b6cd36f0 use datatype name instead of instantiation for cycle detection #5482 2021-08-24 11:14:41 -07:00
Nikolaj Bjorner
e90ec457c3 #5482 
non-termination (stack overflow) bug in recursive comparison
 2021-08-24 09:49:36 -07:00
Nikolaj Bjorner
5fa1b0b09f update project description #5503 2021-08-24 09:48:33 -07:00
Nikolaj Bjorner
23b995d3b5 #5499 
throw exception when dividing by a small 0
 2021-08-24 08:52:20 -07:00
Nikolaj Bjorner
dd91cfb47e #5482 
update temp variables
 2021-08-23 22:21:52 -07:00
Nikolaj Bjorner
592c53e46d char sort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-23 20:45:26 -07:00
Nikolaj Bjorner
170ef1dcca add character sort to Python API and allchar function to API for ease. #5500 2021-08-23 20:02:50 -07:00
Nikolaj Bjorner
4b3b4b95d9 missing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-23 10:03:34 -07:00
Nikolaj Bjorner
2a682e4b13 #5482 
tricky one
 2021-08-23 10:01:53 -07:00
Nikolaj Bjorner
9c7d9f06ed #5497 2021-08-22 17:22:37 -07:00
Nikolaj Bjorner
1975e486ee finally expose some easier to use basics could be used in cases such as #5496 2021-08-21 21:22:54 -07:00
Nikolaj Bjorner
aa05298950 fix #5491 2021-08-19 21:12:27 -07:00
Nikolaj Bjorner
15e3e81cb5 remove likely culprit for #5493 
@zwimer: I had to remove a different move constructor before in the same API due to a different bug that the coverage tool exposed. I was unable to reproduce the bug reported in #5493 in my environment, but the interaction with reference counting and move constructors is sufficiently opaque that I rather not have to fix more bugs introduced with move constructors in the API. I am therefore removing also this use of && and maybe this fixes #5493
 2021-08-19 21:08:20 -07:00
Nikolaj Bjorner
d0e210849f #5454 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-19 03:06:23 -07:00
Nikolaj Bjorner
9122ec9cd6 comment out for now 2021-08-18 14:52:59 -07:00
Nikolaj Bjorner
93c3fc2bda try without semi-colon 2021-08-18 14:52:12 -07:00
Nikolaj Bjorner
adcdd11afc #5454 again 2021-08-18 13:32:51 -07:00
Nikolaj Bjorner
2492278a4b Update test for java 2021-08-18 13:32:51 -07:00
Nikolaj Bjorner
1db9f9a3b5 try vscode from github integration 2021-08-18 11:02:02 -07:00
Nikolaj Bjorner
810b9d003d move examples to python based build 2021-08-18 10:06:02 -07:00
Nikolaj Bjorner
d980ee0533 fix regression in FPNumRef sign 2021-08-18 10:00:22 -07:00
Nikolaj Bjorner
b3db9a1cd5 #5488 2021-08-18 08:30:08 -07:00
Nikolaj Bjorner
5c9f4dc4d7 #5486 - improve type elaboration by epsilon to make common cases parse without type annotation 2021-08-17 16:43:36 -07:00
Nikolaj Bjorner
7f88cfe727 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-17 10:10:20 -07:00
Nikolaj Bjorner
1884ad5b2f expose method for updating python model for constants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-17 09:09:04 -07:00