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

10416 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 5cdbb1f7be this is still used 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:25:34 -08:00
Nikolaj Bjorner 9dd41ba554 remove offending assert, disable assembly-info for dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:13:03 -08:00
Nikolaj Bjorner cabe0ee447 integrating additional changes from @yatli pull request #1815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 10:51:44 -08:00
Nikolaj Bjorner 37d9e6d811 incrementally adding files from dotnet core pull request from @yatli 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 10:40:11 -08:00
Nikolaj Bjorner 1efbc25b3b Merge branch 'master' of https://github.com/z3prover/z3 2019-01-18 18:09:22 -08:00
Nikolaj Bjorner 0b7021d2c8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 18:09:19 -08:00
Nikolaj Bjorner dc5af2d969
Merge pull request #2088 from barik/patch-1 
PYTHON_PATH should say PYTHONPATH.
 2019-01-18 18:07:46 -08:00
Titus Barik 2f0d2ec385
PYTHON_PATH should say PYTHONPATH. 2019-01-18 16:18:16 -08:00
Nikolaj Bjorner c45ab6efed add setting to dump intermediary models #2087 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 15:12:08 -08:00
Nikolaj Bjorner 4caadc6519 add note about libgomp dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 10:13:04 -08:00
Nikolaj Bjorner 947fe2ff9c fix datatype occurs check bug reported by Gerhard Schellhorn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-17 16:35:07 -08:00
Nikolaj Bjorner 442e47dfce fix datatype occurs check bug reported by Gerhard Schellhorn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-17 16:34:26 -08:00
Nikolaj Bjorner f2e636c598 record simplified input clauses as lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 16:37:21 -08:00
Nikolaj Bjorner 247980c5a2 don't assign already assigned literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 11:41:32 -08:00
Nikolaj Bjorner e94aa5bb1d
Merge pull request #2084 from Z3Prover/revert-1815-master 
Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration."
 2019-01-16 10:22:14 -08:00
Nikolaj Bjorner 038971c029
Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration." 2019-01-16 10:21:56 -08:00
Nikolaj Bjorner 16c15d53a9
Merge pull request #1815 from yatli/master 
api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration.
 2019-01-16 10:16:26 -08:00
Nikolaj Bjorner e01a668da0 coordinate drat with clause removal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 02:29:33 -08:00
Nikolaj Bjorner b33f5f879e fix another bug reported by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 17:57:11 -08:00
Nikolaj Bjorner 3298486136 don't reach max conflicts if state is inconsistent 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:40:38 -08:00
Nikolaj Bjorner 5328454c77 const 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:37:23 -08:00
Nikolaj Bjorner 161c83795f remember inconsistent states when cloning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:34:55 -08:00
Nikolaj Bjorner 65bd427e46 neatify statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:48:48 -08:00
Nikolaj Bjorner f238460597 neatify statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:45:04 -08:00
Nikolaj Bjorner ed7cac8cc0 neatify logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:42:13 -08:00
Nikolaj Bjorner b11ec3bfbf merge sat_tactic from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:17:42 -08:00
Nikolaj Bjorner ee07008fb9 import files from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:04:46 -08:00
Nikolaj Bjorner 54a125063b remove produce interpolants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:00:25 -08:00
Nikolaj Bjorner e954f59052 ensure that solver objects have timeout/rlimit/ctrl-c exposed as possible parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 13:50:17 -08:00
Nikolaj Bjorner a686aa7f56 produce binary clauses for DRAT for units produced by probing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 10:56:10 -08:00
Yatao Li 43ee345f01 dotnet deps hack for test 2019-01-15 03:06:36 +09:00
Nikolaj Bjorner 0b84c60886 fix another bug uncovered by Dunlop, prepare grounds for equality solving within NNFs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 01:25:25 -08:00
Yatao Li 58e8b2b8d5 Dockerfile: update ubuntu 14.04 image with cmake 3.12 2019-01-14 14:02:58 +08:00
Nikolaj Bjorner eaa80d5b02 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 11:33:23 -08:00
Yatao Li 209ebecb86 cmake: dotnet: example: dotnet.csproj is NETCOREAPP 2019-01-14 00:51:44 +08:00
Yatao Li f0f9a16f85 cmake: dotnet: example: program -> Program 2019-01-14 00:22:51 +08:00
Yatao Li 08adc1bf97 ... 2019-01-13 23:15:40 +08:00
Yatao Li 8ebde41f35 dotnet: example: copy to binary dir before build 2019-01-13 22:45:05 +08:00
Nikolaj Bjorner 46bfcbd4f8 fix #2082 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 03:46:11 -08:00
Nikolaj Bjorner 4159b987ce purge unused code from theory_pb, fix bug reported by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 03:23:57 -08:00
Nikolaj Bjorner 4b35ef29c9 fix #2081 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 01:18:03 -08:00
Nikolaj Bjorner dc5e4ca1c5 fix drat generation in asymmetric branch simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 13:19:09 -08:00
Nikolaj Bjorner f835a3c2b2 revert assumption tracking choice in unit literals inferred from binary clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 11:08:35 -08:00
Nikolaj Bjorner e4d6aa07dc use vectors instead of hash-tables in dimacs serialization to avoid hash-table contention 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 11:05:00 -08:00
Yatao Li 0a6a76734a docker: ubuntu 14.04 dotnet source fix 2019-01-13 00:08:32 +08:00
Yatao Li 5e79dba3d6 dotnet: move example project build to cmake 2019-01-13 00:03:37 +08:00
Yatao Li 55f92f3658 dotnet: remove stale packages before pack; relay cmake config generator expression into msbuild property.. 2019-01-12 21:33:09 +08:00
Yatao Li 4b3189f3e2 dotnet: identifies arch-specific native libraries 2019-01-12 20:04:44 +08:00
Yatao Li 3767c311aa FindDotnet: generator expression IF is not available for older cmake versions 2019-01-12 19:35:08 +08:00
Yatao Li e5f65263bb dotnet: reigster local repo for nupkg 2019-01-12 19:22:38 +08:00