Skip to content

Instantly share code, notes, and snippets.

Avatar

Masahiro Sakai msakai

View GitHub Profile
View TPPmark2014
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 Jan 8, 2015
Patch for using Cryptominisat4 within open-wbo version 1.3
View open-wbo-1.3-cryptominisat4.diff
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 Aug 29, 2015
fix warnings of LCM 3.0
View README.md
  • lcm_io.cprintfで変数zlong long int なので %d ではなく %lld で受ける必要がある
  • 同個所で引数の数よりも余計に %d があるのを削除
  • lib_e.cexitを使うためにstdlib.hをinclude
  • lib_e.cprintf のフォーマット文字列で、引数が size_t なので %d ではなく %zd で受ける必要がある
View AlphaAlgorithm.hs
-- 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 Aug 29, 2015
Learning of dependency graph and causal net from event logs
View CausalNet.hs
-- | 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 Aug 29, 2015
Learning transition systems from event logs and transforming the transition system into an equivalent Petri net using state-based regions
View MinimalSaturatedNet.hs
{-# 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
Encoding cardinality constraints for CryptoMiniSat from Python interface
View pycryptosat_cardinality.py
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):
View test_lbfgsb.hs
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
View test_ipopt.hs
{-# 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,
View test_chainer.py
#!/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