Skip to content

Instantly share code, notes, and snippets.

View msakai's full-sized avatar

Masahiro Sakai msakai

236 followers · 202 following
View GitHub Profile
@msakai
msakai / TPPmark2014
Last active August 29, 2015 14:11
TPPmark2014のAgda版解説 ref: http://qiita.com/masahiro_sakai/items/ecd83bad7ac8425f22a3
prop3a-step
: ∀ a
→ (∀ a' → (a' <′ a) → ∀ b' c' → (a' ² + b' ² ≡ 3 * c' ²) → a' ≡ 0)
→ ∀ b c → (a ² + b ² ≡ 3 * c ²) → a ≡ 0
prop3a-step zero rec b c P = refl
prop3a-step (suc n) rec b c P = body
where
open ≡-Reasoning
a = suc n
@msakai
msakai / open-wbo-1.3-cryptominisat4.diff
Created January 8, 2015 23:50
Patch for using Cryptominisat4 within open-wbo version 1.3
diff -uprN open-wbo.orig/Makefile open-wbo/Makefile
--- open-wbo.orig/Makefile 2015-01-02 23:11:06.000000000 -0500
+++ open-wbo/Makefile 2015-01-08 08:48:47.418892000 -0500
@@ -10,10 +10,14 @@
# SOLVERDIR = minisat
# NSPACE = Minisat
#
+#VERSION = core
+#SOLVERNAME = "Glucose3.0"
+#SOLVERDIR = glucose3.0
@msakai
msakai / README.md
Last active August 29, 2015 14:13
fix warnings of LCM 3.0
  • lcm_io.cのprintfで変数zは long long int なので %d ではなく %lld で受ける必要がある
  • 同個所で引数の数よりも余計に %d があるのを削除
  • lib_e.cでexitを使うためにstdlib.hをinclude
  • lib_e.c の printf のフォーマット文字列で、引数が size_t なので %d ではなく %zd で受ける必要がある
@msakai
msakai / AlphaAlgorithm.hs
Created April 20, 2015 15:29
-- Naive implementation of alpha algorithm for descovering petri-nets from event logs
import Control.Monad
import Data.Set (Set)
import qualified Data.Set as Set
data Arc p t
= P2T p t
| T2P t p
deriving (Eq, Ord, Show)
@msakai
msakai / CausalNet.hs
Last active August 29, 2015 14:20
Learning of dependency graph and causal net from event logs
-- | Naive implementation of alpha algorithm for descovering petri-nets from event logs
--
-- References:
--
-- * Wil van der Aalst, "Process Mining: Data science in Action", Week 2,
-- https://www.coursera.org/course/procmin
import Control.Monad
import Data.MultiSet (MultiSet) -- http://hackage.haskell.org/package/multiset
import qualified Data.MultiSet as MultiSet
@msakai
msakai / MinimalSaturatedNet.hs
Last active August 29, 2015 14:20
Learning transition systems from event logs and transforming the transition system into an equivalent Petri net using state-based regions
{-# LANGUAGE ScopedTypeVariables, BangPatterns #-}
-- | This module provides two functionality:
--
-- * Learning transition systems from event logs
--
-- * Transforming the transition system into an equivalent Petri net using state-based regions.
--
-- References:
--
-- * Wil van der Aalst, "Process Mining: Data science in Action", Week 3,
@msakai
msakai / pycryptosat_cardinality.py
Created May 9, 2015 02:30
Encoding cardinality constraints for CryptoMiniSat from Python interface
from pycryptosat import Solver
class Encoder():
def __init__(self, solver, n = 1):
self._solver = solver
self._n = n
self._ite_cache = {}
self._true = None
def newvar(self):
@msakai
msakai / test_lbfgsb.hs
Created July 13, 2015 23:14
import Data.List
import qualified Data.Vector as V
import qualified Data.Vector.Storable as VS
import qualified Data.Vector.Generic as VG
import Numeric.AD
-- from http://hackage.haskell.org/package/l-bfgs-b
import qualified Numeric.LBFGSB as LBFGSB
import qualified Numeric.LBFGSB.Result as R
type Weight = Int
@msakai
msakai / test_ipopt.hs
Created July 16, 2015 00:14
{-# LANGUAGE ScopedTypeVariables #-}
import qualified Data.Vector.Storable as VS
import Data.Vector.Generic ((!))
import qualified Data.Vector.Generic as VG
import Ipopt.Raw
( addIpoptNumOption,
addIpoptStrOption,
addIpoptIntOption,
ipoptSolve,
createIpoptProblemAD,
@msakai
msakai / test_chainer.py
Last active August 29, 2015 14:25
#!/usr/bin/env python
import numpy as np
import six
import chainer
from chainer import computational_graph as c
from chainer import cuda
import chainer.functions as F
from chainer import optimizers