George Karpenkov cheshire
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Configuration config = Configuration.defaultConfiguration(); | |
| Z3FormulaManager mgr = Z3FormulaManager.create(null, config); | |
| // TODO: without type casts?.. | |
| Z3RationalFormulaManager rfmgr = | |
| (Z3RationalFormulaManager) mgr.getRationalFormulaManager(); | |
| Z3TheoremProver prover = new Z3TheoremProver(mgr); |
cheshire
/ gist:49b4f199944d3a891296
Created
September 30, 2014 09:30
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| commit 267746f2542b87447abd2b20f4fc3a658bd41a2a | |
| Author: George Karpenkov <george@metaworld.ru> | |
| Date: Mon Sep 29 21:24:20 2014 +0200 | |
| New interface for CompositeCPA, for easier | |
| strengthening. | |
| diff --git a/src/org/sosy_lab/cpachecker/core/interfaces/ICompositeTransferRelation.java b/src/org/sosy_lab/cpachecker/core/interfaces/ICompositeTransferRelation.java | |
| new file mode 100644 | |
| index 0000000..48d4fda |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| diff --git a/src/org/sosy_lab/common/configuration/OptionCollector.java b/src/org/sosy_lab/common/configuration/OptionCollector.java | |
| index f189adf..d4bb029 100644 | |
| --- a/src/org/sosy_lab/common/configuration/OptionCollector.java | |
| +++ b/src/org/sosy_lab/common/configuration/OptionCollector.java | |
| @@ -188,18 +188,40 @@ public class OptionCollector { | |
| try { | |
| return Iterators.forEnumeration(classLoader.getResources("")); | |
| } catch (IOException e) { | |
| - System.err.println("Could not get recources of classloader."); | |
| + System.err.println("Could not get resources of classloader."); |
cheshire
/ IntegerTheoryFuzzer.java
Last active
July 8, 2016 15:39
Fuzzer over the theory of integers
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| package org.sosy_lab.solver.test; | |
| import org.sosy_lab.common.UniqueIdGenerator; | |
| import org.sosy_lab.solver.api.FormulaManager; | |
| import org.sosy_lab.solver.api.IntegerFormulaManager; | |
| import org.sosy_lab.solver.api.NumeralFormula.IntegerFormula; | |
| import java.util.Random; | |
| import java.util.stream.IntStream; |
cheshire
/ gist:de6331415e4829722effcead954619da
Created
April 14, 2021 18:45
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| hello |
cheshire
/ gist:151ef00fc078ef1e641661437e24774c
Created
April 14, 2021 18:46
This file has been truncated, but you can view the full file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| HloModule Module | |
| ENTRY computation { | |
| tmp_0 = u8[32,224,224,3]{3,2,1,0} parameter(0) | |
| tmp_1 = f32[] constant(1) | |
| tmp_2 = f32[32,7,7,352]{3,2,1,0} broadcast(f32[] tmp_1), dimensions={} | |
| tmp_3 = f32[32,7,7,352]{3,2,1,0} constant({ { /*i0=0*/ { /*i1=0*/ { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 |
cheshire
/ patch.diff
Created
April 28, 2021 03:41
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| diff --git a//tensorflow/compiler/jit/BUILD b//tensorflow/compiler/jit/BUILD | |
| --- a//tensorflow/compiler/jit/BUILD | |
| +++ b//tensorflow/compiler/jit/BUILD | |
| @@ -151,6 +151,7 @@ cc_library( | |
| ":jit_compilation_passes", | |
| ":xla_device", | |
| ":xla_kernel_creator", # buildcleaner: keep | |
| + ":xla_device_no_jit_rewrite_registration", | |
| "//third_party/absl/memory", | |
| "//third_party/absl/strings", |
cheshire
/ cublas.log
Created
May 19, 2021 20:57
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Loading: | |
| Loading: 0 packages loaded | |
| Analyzing: target //third_party/tensorflow/compiler/xla/client/lib:svd_test_gpu (0 packages loaded, 0 targets configured) | |
| INFO: Analyzed target //third_party/tensorflow/compiler/xla/client/lib:svd_test_gpu (0 packages loaded, 0 targets configured). | |
| INFO: Found 1 target... | |
| [0 / 1] [Prepa] action 'BuildInfo build-info.txt' | |
| Target //third_party/tensorflow/compiler/xla/client/lib:svd_test_gpu up-to-date: | |
| blaze-bin/third_party/tensorflow/compiler/xla/client/lib/svd_test_gpu | |
| INFO: Elapsed time: 0.365s, Critical Path: 0.09s, Remote (0.00% of the time): [queue: 0.00%, setup: 0.00%, process: 0.00%] | |
| INFO: Build completed successfully, 1 total action |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| I! CuDNN (v7604) function cudnnSetFilterNdDescriptor() called: | |
| i! dataType: type=cudnnDataType_t; val=CUDNN_DATA_HALF (2); | |
| i! format: type=cudnnTensorFormat_t; val=CUDNN_TENSOR_NHWC (1); | |
| i! nbDims: type=int; val=4; | |
| i! filterDimA: type=int; val=[256,256,3,3]; | |
| i! Time: 2021-05-20T12:38:10.745481 (0d+0h+0m+24s since start) | |
| i! Process=1524391; Thread=1524637; GPU=NULL; Handle=NULL; StreamId=NULL. | |
| I! CuDNN (v7604) function cudnnCreateConvolutionDescriptor() called: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| I! CuDNN (v7604) function cudnnSetFilterNdDescriptor() called: | |
| i! dataType: type=cudnnDataType_t; val=CUDNN_DATA_HALF (2); | |
| i! format: type=cudnnTensorFormat_t; val=CUDNN_TENSOR_NHWC (1); | |
| i! nbDims: type=int; val=4; | |
| i! filterDimA: type=int; val=[256,256,3,3]; | |
| i! Time: 2021-05-20T12:38:10.745481 (0d+0h+0m+24s since start) | |
| i! Process=1524391; Thread=1524637; GPU=NULL; Handle=NULL; StreamId=NULL. | |
| I! CuDNN (v7604) function cudnnCreateConvolutionDescriptor() called: |
OlderNewer