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
(declare-const n Int) | |
(declare-datatypes () ((Jug Big Small))) | |
(declare-datatypes () ((Act FillBig FillSmall EmptyBig EmptySmall BigToSmall SmallToBig))) | |
(declare-fun vol (Jug Int) Int) | |
(declare-fun act (Int) Act) | |
(assert (= n 6)) | |
(assert (= (act 0) EmptyBig)) | |
(assert (= (vol Big 0) 0)) | |
(assert (= (vol Small 0) 0)) |
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
from z3 import * | |
Jug, (Big, Small) = EnumSort( | |
'Jug', ['Big', 'Small']) | |
Act, (FillBig, FillSmall, EmptyBig, EmptySmall, BigToSmall, SmallToBig) = EnumSort( | |
'Act', ['FillBig', 'FillSmall', 'EmptyBig', 'EmptySmall', 'BigToSmall', 'SmallToBig']) | |
#m = 10 | |
for n in range(5, 10): | |
print("n = {}".format(n)) |
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
1> c("jug_statem.erl"). | |
{ok,jug_statem} | |
2> jug_statem:test(100). | |
.................................................................................................... | |
OK: Passed 100 test(s). | |
18% {jug_statem,fill_big,0} | |
17% {jug_statem,big_to_small,0} |
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
// recursive | |
const hanoi0 = (n, a, b, c) => { | |
if (n > 0) { | |
hanoi0(n - 1, a, c, b); | |
console.log(`${a} ==> ${c}`); | |
hanoi0(n - 1, b, a, c); | |
} | |
} | |
hanoi0(3, "a", "b", "c"); |
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
let fact0 = (n) => { | |
if (n > 0) { | |
return n * fact0(n - 1); | |
} else | |
return 1; | |
} | |
console.log(fact0(5, (x) => x)) | |
let fact1 = (n, k) => { |
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
/* | |
How many different ways can we make change of $ 1.00, given half-dollars, quarters, dimes, nickels, and pennies? More generally, can we write a procedure to compute the number of ways to change any given amount of money? | |
This problem has a simple solution as a recursive procedure. | |
Suppose we think of the types of coins available as arranged in some order. Then the following relation holds: | |
The number of ways to change amount a using n kinds of coins equals | |
the number of ways to change amount a using all but the first kind of coin, plus | |
the number of ways to change amount a - d using all n kinds of coins, where d is the denomination of the first kind of coin. |
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
module Date | |
-- leap year ? | |
leap : Integer -> Bool | |
leap year = (mod year 4 == 0) && ((mod year 400 == 0) || not (mod year 100 == 0)) | |
-- number of days in month/year | |
days : Integer -> Integer -> Integer | |
days 2 year = if leap year then 29 else 28 | |
days month _ = if month `List.elem` [4,6,9,11] then 30 else 31 |
OlderNewer