# HG changeset patch # User Mike Pavone # Date 1376198749 25200 # Node ID b00904b36acaf0a308a4da15117ac67a95907d50 # Parent 2b5357b13e2df95f2411f35ca0d1a5b8c4df2974 More solver work diff -r 2b5357b13e2d -r b00904b36aca src/bv.tp --- a/src/bv.tp Sat Aug 10 19:54:20 2013 -0700 +++ b/src/bv.tp Sat Aug 10 22:25:49 2013 -0700 @@ -4,13 +4,17 @@ _input <- 0u64 _acc <- 0u64 _val <- 0u64 + _zero <- #{ string <- { "0" } eval <- { 0u64 } operators <- { 0 } isTfold? <- { false } isTerminal? <- { true } + constant? <- { true } } + _accInputNode <- _zero + _foldInputNode <- _zero _one <- #{ string <- { "1" } @@ -18,6 +22,7 @@ operators <- { 0 } isTfold? <- { false } isTerminal? <- { true } + constant? <- { true } } _inputNode <- #{ @@ -26,6 +31,7 @@ operators <- { 0 } isTfold? <- { false } isTerminal? <- { true } + constant? <- { false } } _accNode <- #{ string <- { "acc" } @@ -33,6 +39,7 @@ operators <- { 0 } isTfold? <- { false } isTerminal? <- { true } + constant? <- { _accInputNode constant? } } _valNode <- #{ string <- { "val" } @@ -40,6 +47,7 @@ operators <- { 0 } isTfold? <- { false } isTerminal? <- { true } + constant? <- { _foldInputNode constant? } } _opPlus <- 1 _opAnd <- 2 @@ -78,6 +86,7 @@ operators <- { _opPlus or (left operators) or (right operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { (left constant?) && (right constant?) } } } zero <- { @@ -95,6 +104,29 @@ operators <- { _opAnd or (left operators) or (right operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { + if: (left constant?) { + if: (right constant?) { + true + } else: { + if: (string: left) = "0" { + true + } else: { + false + } + } + } else: { + if: (right constant?) { + if: (string: right) = "0" { + true + } else: { + false + } + } else: { + false + } + } + } } } @@ -105,6 +137,7 @@ operators <- { _opOr or (left operators) or (right operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { (left constant?) && (right constant?) } } } @@ -115,6 +148,13 @@ operators <- { _opXor or (left operators) or (right operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { + if: (left constant?) && (right constant?) { + true + } else: { + (string: left) = (string: right) + } + } } } @@ -125,6 +165,7 @@ operators <- { _opNot or (exp operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { exp constant? } } } @@ -135,6 +176,7 @@ operators <- { _opShl1 or (exp operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { exp constant? } } } @@ -145,6 +187,7 @@ operators <- { _opShr1 or (exp operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { exp constant? } } } @@ -155,6 +198,7 @@ operators <- { _opShr4 or (exp operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { exp constant? } } } @@ -165,6 +209,7 @@ operators <- { _opShr16 or (exp operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { exp constant? } } } @@ -185,6 +230,7 @@ operators <- { _opIf0 or (exp operators) or (ifzero operators) or (ifnotzero operators)} isTfold? <- { false } isTerminal? <- { false } + constant? <- { (exp constant?) && (ifzero constant?) && (ifnotzero constant?) } } } @@ -210,6 +256,11 @@ (toFold isTerminal?) && (startAcc isTerminal?) && (toFold string) = "input" && (startAcc string) = "0" } isTerminal? <- { false } + constant? <- { + _accInputNode <- startAcc + _foldInputNode <- toFold + fun constant? + } } } diff -r 2b5357b13e2d -r b00904b36aca src/solver.tp --- a/src/solver.tp Sat Aug 10 19:54:20 2013 -0700 +++ b/src/solver.tp Sat Aug 10 22:25:49 2013 -0700 @@ -1,43 +1,129 @@ -#{ - classify <- :prog trees { - testvals <- #[] - i <- 0 - (os srand: (os time)) - while: {i < 256} do: { - i <- i + 1 - testvals append: (uint64: (os rand64)) - } - root <- dict linear - foreach: trees :idx tree { - prog root!: tree - res <- prog run: (testvals get: 0) - arr <- root get: res withDefault: #[] - arr append: tree - if: (arr length) = 1 { - root set: res arr +{ + _classifNode <- :vals prog startIdx child? { + if: startIdx < (vals length) { + _dict <- dict linear + _const <- #[] + _first <- false + _hasFirst? <- false + _val <- vals get: startIdx + #{ + input <- { _val } + valmap <- { _dict } + constantProgs <- { _const } + append <- :tree { + if: child? && (tree constant?) { + _const append: tree + } else: { + if: (_dict length) > 0 { + prog root!: tree + res <- prog run: _val + node <- _dict get: res elseSet: { + _classifNode: vals prog startIdx + 1 true + } + node append: tree + } else: { + if: _hasFirst? { + prog root!: _first + res <- prog run: _val + node <- _classifNode: vals prog startIdx + 1 true + _dict set: res node + node append: _first + append: tree + } else: { + _first <- tree + _hasFirst? <- true + } + } + } + } + length <- { + len <- _dict length + if: len = 0 && _hasFirst? { + len <- 1 + } + len + _const length + } + printwithIndent <- :indent { + print: indent . "Input: " . (hex: _val) . "\n" + nextindent <- indent . " " + if: (_const length) > 0 { + print: indent . "Constants:\n" + foreach: _const :idx val { + print: nextindent . (string: val) . "\n" + } + } + if: (_dict length) > 0 { + foreach: _dict :key val { + print: indent . (hex: key) . " ->\n" + val printwithIndent: nextindent + } + } else: { + if: _hasFirst? { + print: nextindent . (string: _first) . "\n" + } + } + } + print <- { + printwithIndent: "" + } + } + } else: { + _arr <- #[] + #{ + append <- :tree { + _arr append: tree + } + length <- { _arr length } + printwithIndent <- :indent { + print: indent . "No more values for these:\n" + indent <- indent . " " + foreach: _arr :idx val { + print: indent . (string: val) . "\n" + } + } + print <- { + printwithIndent: "" + } } } - #{ - inputs <- { testvals } - valmap <- { root } - } } - - main <- :args { - size <- 3 - if: (args length) > 1 { - size <- int32: (args get: 1) + #{ + classify <- :prog trees numTests { + testvals <- #[] + i <- 0 + (os srand: (os time)) + while: {i < numTests} do: { + i <- i + 1 + testvals append: (uint64: (os rand64)) + } + root <- _classifNode: testvals prog 0 false + foreach: trees :idx tree { + root append: tree + } + root } - prog <- bv program - if: size >= 2 { - trees <- (prog allOfSize: size) - if: (args length) > 2 { - ops <- (args get: 2) splitOn: "," - trees <- prog filterTrees: trees ops + + main <- :args { + size <- 3 + if: (args length) > 1 { + size <- int32: (args get: 1) } - info <- classify: prog trees - foreach: (info valmap) :val arr { - print: "Value: 0x" . (hex: val) ." produced by " . (string: (arr length)) . "programs\n" + prog <- bv program + if: size >= 2 { + trees <- (prog allOfSize: size) + numTests <- 0 + if: (args length) > 2 { + numTests <- int32: (args get: 2) + } + if: numTests <= 0 { + numTests <- 16 + } + if: (args length) > 3 { + ops <- (args get: 3) splitOn: "," + trees <- prog filterTrees: trees ops + } + info <- classify: prog trees numTests + print: info } } }