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

15682 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes 1f4a7c5101 logging: don't call the returned function twice (one for log, one for return) 
Z3_simplify() does RETURN_Z3(simplify(...)), hence the function was being called twice
it turns out simplify is not idempotent, so calling it twice can result in different results
thus breaking the log.
 2021-08-29 11:06:19 +01:00
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