Skip to content

Instantly share code, notes, and snippets.

View msakai's full-sized avatar

Masahiro Sakai msakai

237 followers · 202 following
View GitHub Profile
@msakai
msakai / datatypes.smtc
Created December 20, 2011 13:20
Can't Z3 handle datatypes that contains sorts introduced by declare-sort/define-sort?
(declare-sort A)
(define-sort B () Int)
(declare-datatypes ((listA (nilA) (consA (hdA A) (tlA listA)))))
(declare-datatypes ((listB (nilB) (consB (hdB B) (tlB listB)))))
(declare-datatypes ((listInt (nilInt) (consInt (hdInt Int) (tlInt listInt)))))
; =>
; success
; success
; (error "line 3 column 64: could not parse data-type declaration")
; (error "ERROR: line 3 column 47: unknown sort 'A'.")
@msakai
msakai / glpk-mip-sample.c
Created April 22, 2012 04:21
Sample for solving MIP (mixed integer programming) problem with GLPK
#include <stdlib.h>
#include <stdio.h>
#include <glpk.h>
/*
Maximize
obj: x1 + 2 x2 + 3 x3 + x4
Subject To
c1: - x1 + x2 + x3 + 10 x4 <= 20
c2: x1 - 3 x2 + x3 <= 30
@msakai
msakai / problem.lp
Created June 26, 2012 23:09
A bug of SCIP?
MINIMIZE
+ 0 x2746
SUBJECT TO
- 1259712 x3295 - 205379 x3294 - 300763 x3292 - 1000 x3286 - 226981 x3280 - 1367631 x3279 - 941192 x3277 - 79507 x3276 - 166375 x3273 - 1259712 x3225 - 226981 x3224 - 226981 x3217 - 373248 x3216 - 830584 x3213 - 1259712 x3211 - 205379 x3435 - 1367631 x3434 - 2744 x3427 - 1157625 x3423 - 287496 x3421 - 300763 x3405 - 941192 x3404 - 226981 x3400 - 2744 x3399 - 474552 x3396 - 912673 x3393 - 373248 x3391 - 79507 x3389 - 373248 x3385 - 474552 x3382 - 10648 x3378 - 166375 x3344 - 830584 x3340 - 1157625 x3339 - 912673 x3337 - 10648 x3336 - 1000 x3315 - 1259712 x3310 - 287496 x3309 - 373248 x3307 + x3210 + x3209 + x3205 + x3204 + x3202 + x3201 + x3196 - 76800 x2834 - 307200 x2833 - 109443 x2832 - 85683 x2831 - 34992 x2830 - 10443 x2829 - 209088 x2828 - 13467 x2827 - 63075 x2826 - 399675 x2825 - 458643 x2824 - 79707 x2823 - 382347 x2822 - 300 x2821 - 76800 x2820 - 158700 x2818 - 93987 x2817 - 43200 x2816 - 11163 x2815 - 36963 x2814 - 83667 x2813 - 28812 x2812 - 5547 x2811 - 143883 x2810 -
@msakai
msakai / FlightRadar24.hs
Created August 10, 2012 22:56
Sample for fetching JSON data from flightradar24.com
import Control.Concurrent
import Control.Monad
import Data.Maybe
import Data.Time
import Network.Browser
import Network.HTTP
import Network.HTTP.Proxy
import Network.URI
import System.Locale
@msakai
msakai / parse-dimacs-1.2-zero-clauses.patch
Created September 30, 2012 09:34
Patch for accepting .cnf files with zero clauses
--- parse-dimacs-1.2.orig/Language/CNF/Parse/ParseDIMACS.hs 2012-09-30 09:37:00.000000000 +0900
+++ parse-dimacs-1.2/Language/CNF/Parse/ParseDIMACS.hs 2012-09-30 09:52:55.000000000 +0900
@@ -31,7 +31,7 @@ import Text.Parsec( ParseError, SourceNa
import Text.Parsec.ByteString.Lazy
import Text.Parsec.Char
import Text.Parsec.Combinator
-import Text.Parsec.Prim( try, unexpected, runParser )
+import Text.Parsec.Prim( many, try, unexpected, runParser )
import qualified Text.Parsec.Token as T
@msakai
msakai / scip-maxsat.cpp
Last active December 12, 2015 02:48
#include <stdlib.h>
#include <stdio.h>
#include <stdint.h>
#include <inttypes.h>
#include <vector>
#include "scip/scip.h"
#include "scip/scipdefplugins.h"
extern SCIP_RETCODE SCIPincludeEventHdlrBestsol(SCIP* scip);
@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)