Joel Burget joelburget
joelburget
/ seaninterview.py
Created
June 5, 2019 15:18
This file contains hidden or 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
| # given an amount and coin denominations, | |
| # compute the number of ways to make amount with coins of the given denoms | |
| # 4, [1,2,3] -> 4 | |
| def ways_to_make(amount, denoms): | |
| # ways to make 4 | |
| # ~ ways(4 - 3) + ways(4 - 2) + ways(4 - 1) ~ | |
| # ways(1, largest=1) + ways(2, largest=1) | |
| # dim 1: amount |
joelburget
/ hdocset-dtruss
Created
May 12, 2019 13:10
This file has been truncated, but you can view the full file.
This file contains hidden or 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
| dtrace: system integrity protection is on, some features will not be available | |
| PID/THRD ELAPSD CPU SYSCALL(args) = return | |
| 27547/0x5b150b: 4 0 ulock_wake(0x1000002, 0x102F5A000, 0x0) = 0 0 | |
| 27547/0x5b13b5: 4 0 ulock_wake(0x1000002, 0x102F5A000, 0x0) = 0 0 | |
| 27547/0x5b1513: 4 1 ulock_wait(0x1010002, 0x102F5A000, 0x1102) = 1 0 | |
| 27547/0x5b1513: 2 0 ulock_wake(0x1000002, 0x102F5A000, 0x0) = 0 0 | |
| 27547/0x5b13b5: 2 0 ulock_wait(0x1010002, 0x102F5A000, 0x7C02) = 1 0 | |
| 27547/0x5b150b: 2 0 ulock_wake(0x1000002, 0x102F5A000, 0x0) = 0 0 | |
| 27547/0x5b150b: 1 0 ulock_wake(0x1000002, 0x102F5A000, 0x0) = 0 0 | |
| 27547/0x5b13b5: 2 0 ulock_wait(0x1010002, 0x102F5A000, 0x7C02) = 1 0 |
joelburget
/ Generic.hs
Last active
February 5, 2019 00:54
This file contains hidden or 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
| {-# LANGUAGE DefaultSignatures #-} | |
| {-# LANGUAGE DeriveAnyClass #-} | |
| {-# LANGUAGE DeriveGeneric #-} | |
| {-# LANGUAGE FlexibleContexts #-} | |
| {-# LANGUAGE LambdaCase #-} | |
| {-# LANGUAGE PolyKinds #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE TypeApplications #-} | |
| {-# LANGUAGE TypeOperators #-} |
joelburget
/ gist:4c5e4a6594ea4aa7f48e5b6093f951fa
Created
January 7, 2019 22:59
This file contains hidden or 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
| λ> :r | |
| *** Chasing dependencies: | |
| Chasing modules from: *Pact.Compile,*Pact.Eval,*Pact.Gas,*Pact.Native,*Pact.Native.Db,*Pact.Native.Internal,*Pact.Native.Time,*Pact.Native.Ops,*Pact.Native.Keysets,*Pact.Parse,*Pact.PersistPactDb,*Pact.Persist,*Pact.Persist.Pure,*Pact.Repl,*Pact.Repl.Lib,*Pact.Repl.Types,*Pact.Types.Exp,*Pact.Types.ExpParser,*Pact.Types.Gas,*Pact.Types.Hash,*Pact.Types.Info,*Pact.Types.Lang,*Pact.Types.Logger,*Pact.Types.Native,*Pact.Types.Parser,*Pact.Types.Persistence,*Pact.Types.Runtime,*Pact.Types.Orphans,*Pact.Types.Term,*Pact.Types.Type,*Pact.Types.Util,*Pact.Types.Version,*Crypto.Hash.Blake2Native,*Pact.Types.Typecheck,*Pact.Typechecker,*Pact.Analyze.Alloc,*Pact.Analyze.Eval,*Pact.Analyze.Eval.Invariant,*Pact.Analyze.Eval.Numerical,*Pact.Analyze.Eval.Prop,*Pact.Analyze.Eval.Core,*Pact.Analyze.Eval.Term,*Pact.Analyze.Check,*Pact.Analyze.Errors,*Pact.Analyze.Feature,*Pact.Analyze.LegacySFunArray,*Pact.Analyze.Model,*Pact.Analyze.Model.Dot,*Pact.Analyze.Model.Graph,*Pact.Analyze.Model.Tags, |
joelburget
/ test.smt2
Created
September 23, 2018 00:39
This file contains hidden or 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
| (set-logic ALL) | |
| ; define List | |
| (declare-datatypes (T) | |
| ((List | |
| (nil) | |
| (cons (head T) (tail List))))) | |
| ; define len | |
| (declare-fun len ((List Int)) Int) |
joelburget
/ len.z3
Created
September 21, 2018 21:24
This file contains hidden or 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
| (declare-fun len ((List Int)) Int) | |
| (declare-fun append ((List Int) (List Int)) (List Int)) | |
| (declare-const xs (List Int)) | |
| (declare-const ys (List Int)) | |
| ; len defining equations | |
| (assert (forall ((xs (List Int))) | |
| (= (len xs) | |
| (ite (= xs nil) 0 (+ 1 (len (tail xs))))))) |
joelburget
/ test2.z3
Created
September 16, 2018 19:12
This file contains hidden or 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
| (set-option :global-declarations true) | |
| (set-option :smtlib2_compliant true) | |
| (set-option :diagnostic-output-channel "stdout") | |
| (set-option :produce-models true) | |
| (set-logic ALL) | |
| ; --- literal constants --- | |
| (define-fun two-digits () Real 100.0) | |
| ; --- skolem constants --- |
joelburget
/ -
Created
September 11, 2018 16:10
This file contains hidden or 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
| ** Calling: z3 -nw -in -smt2 | |
| [GOOD] ; Automatically generated by SBV. Do not edit. | |
| [GOOD] (set-option :print-success true) | |
| [GOOD] (set-option :global-declarations true) | |
| [GOOD] (set-option :smtlib2_compliant true) | |
| [GOOD] (set-option :diagnostic-output-channel "stdout") | |
| [GOOD] (set-option :produce-models true) | |
| [GOOD] (set-logic ALL) | |
| [GOOD] ; --- uninterpreted sorts --- | |
| [GOOD] ; --- literal constants --- |
joelburget
/ test.z3
Last active
September 10, 2018 17:26
This file contains hidden or 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
| (set-option :global-declarations true) | |
| (set-option :smtlib2_compliant true) | |
| (set-option :diagnostic-output-channel "stdout") | |
| (set-option :produce-models true) | |
| (set-logic ALL) | |
| ; --- literal constants --- | |
| (define-fun two-digits () Real 100.0) | |
| ; --- skolem constants --- |
joelburget
/ test.z3
Created
September 10, 2018 16:00
This file contains hidden or 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
| (set-option :global-declarations true) | |
| (set-option :smtlib2_compliant true) | |
| (set-option :diagnostic-output-channel "stdout") | |
| (set-option :produce-models true) | |
| (set-logic ALL) | |
| ; --- uninterpreted sorts --- | |
| ; --- literal constants --- | |
| (define-fun s3 () Real (/ 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0 1.0)) | |
| (define-fun s57 () Real 0.0) | |
| (define-fun s82 () Real (/ 1.0 2.0)) |