mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-24 16:34:36 +00:00
Code Activity
13811 commits 43 branches 52 tags 176 MiB
Commit graph

13811 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
6321dabe93 fix #2869 fix #2878 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-23 10:59:33 -06:00
Olaf Tomalka
876d7c92fb Added FreshFunction to Python bindings. 
All other declarations can be done use appropriate Fresh*() call,
or FreshConst() with a desired sort, except Functions.

I've added the abillity to do that in Python bindings using already existing APIs
 2020-01-23 10:00:36 -06:00
Nikolaj Bjorner
55f62fcaed fix #2865 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-22 16:16:44 -06:00
Nikolaj Bjorner
0ab107dcb5 revert fix for #2865 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-22 15:06:20 -06:00
Nikolaj Bjorner
ad965ac896 fix #2817 - rows may apparently not be correct (root cause of this tbd), but avoid Gomory on incorrect rows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-22 14:29:02 -06:00
Nikolaj Bjorner
05da2508bf fix #2873 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-22 11:08:44 -06:00
Nikolaj Bjorner
da2f5cc362 remove spurious out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-21 14:18:49 -06:00
Nikolaj Bjorner
3931dd5da0 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-21 11:48:00 -06:00
Nikolaj Bjorner
045448e5b2 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-21 11:47:37 -06:00
Nikolaj Bjorner
683eed0c1e use get_sign 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-21 11:15:13 -06:00
Nikolaj Bjorner
4e81085292 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-21 10:29:42 -06:00
Nikolaj Bjorner
c816d45a7d share some equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-20 16:22:38 -06:00
Nikolaj Bjorner
9179deb746 add get-interpolant command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-20 16:22:38 -06:00
Nikolaj Bjorner
d3b105f9f8 move out sign 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-20 16:22:38 -06:00
Nikolaj Bjorner
89c91765f6 fix 2863 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-20 16:22:37 -06:00
Nikolaj Bjorner
495b88ce99 evaluate with don't cares 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-20 16:22:37 -06:00
Christoph M. Wintersteiger
321bad2c84
Fix for implicit consts in FPA models. Fixes #2865. 2020-01-20 17:06:35 +00:00
Nikolaj Bjorner
22f1c6448a add option to increase thresholds based on simulated equality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-16 22:43:18 -08:00
Nikolaj Bjorner
93d1091ad9 bcd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-16 20:37:22 -08:00
Andrew Helwer
ea3b149575
Script assembly signing & NuGet package creation in Azure Pipelines (#2862) 
Windows x86/x64 builds now parallelized
Windows assemblies now signed
NuGet package created
NuGet package signed
NuGet package published to NuGet.org
 2020-01-16 18:34:01 -08:00
Nikolaj Bjorner
dc5d8819cd add const refs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-15 08:56:46 -08:00
Nikolaj Bjorner
773b27296f translate optimize from c++ API #2859 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-15 04:24:51 -08:00
Nikolaj Bjorner
0d614b8c36 check underflows, aig fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-14 19:46:56 -08:00
Nikolaj Bjorner
82cacdf569 adding stronger filter than connected 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-14 19:46:56 -08:00
Murphy Berzish
509cad9c9a z3str3: refactoring, move legacy model construction code into theory_str_mc 2020-01-14 16:13:25 -08:00
Nikolaj Bjorner
06fb36d648 add comments, rename config to more descriptive names 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-14 10:34:44 -08:00
Nikolaj Bjorner
5f96bf55f4 cleanup, comments, fixes to drat genereration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-14 10:25:10 -08:00
Nikolaj Bjorner
a12fca3105 first pass on extracting binary clauses, ensure that binary clauses used by simplifier are in scope of DRAT, add certification of units 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-14 09:08:40 -08:00
Nikolaj Bjorner
d77ac69015 substitution free 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-13 16:33:46 -08:00
Nikolaj Bjorner
453ef631a0 base working mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-13 15:45:06 -08:00
Christoph M. Wintersteiger
77689ed002
Fix term-ite models in theory_fpa. Fixes #2857. 2020-01-13 19:24:48 +00:00
Nikolaj Bjorner
0e096c55a9 fix how don't cares are handled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-13 09:45:21 -08:00
Nikolaj Bjorner
ba292346ae some more string perf profiling 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-12 22:11:00 -08:00
Nikolaj Bjorner
ab5905cf7f some adjustments for stack use on large strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-12 22:08:24 -08:00
Nikolaj Bjorner
e8cfbb41d3 missing length constraint for at fixes #2852 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-12 17:22:59 -08:00
Nikolaj Bjorner
74f0665a0b add != 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-12 17:06:31 -08:00
Nikolaj Bjorner
9f964be3f4 add don't care option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-12 17:00:05 -08:00
Nikolaj Bjorner
e0a41a18c3 add validation to aig_simplifier, start BIG-based masking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-11 20:47:38 -08:00
Nikolaj Bjorner
41a00707e1 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 13:23:32 -08:00
Nikolaj Bjorner
ab1f2f2e63 reduce use of symbols in gparams 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:54:26 -08:00
Nikolaj Bjorner
8515b304da bdd return 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:20:09 -08:00
Nikolaj Bjorner
e2f5c1f7c8 delay load specrels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:18:56 -08:00
Nikolaj Bjorner
541658fe02 move to abstract symbols 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:14:13 -08:00
Nikolaj Bjorner
78a1736bd2 prepare symbols to be more abstract, update mbi, delay initialize some modules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:02:08 -08:00
Andrew V. Jones
74d3493d74 Ensuring consistency and correctness of exception messages for BV and FP checks within z3.py 
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
 2020-01-10 10:27:05 -08:00
Nuno Lopes
0b14f1b6f6 fix crash when propagating equalities over arrays with lambdas 2020-01-10 16:04:58 +00:00
Nikolaj Bjorner
9064e58665 aig roots 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-09 21:41:00 -08:00
Nikolaj Bjorner
607a1b3f99 cutset updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-09 21:37:25 -08:00
Nikolaj Bjorner
e4cc9e8404 memcpy include 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-09 10:22:19 -08:00
Nikolaj Bjorner
94386a0f6b fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-09 10:07:05 -08:00