Created
March 9, 2020 02:10
-
-
Save jkoppel/1b884d6654194bf9e68ecf5998a3c622 to your computer and use it in GitHub Desktop.
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
generator int exp([int nvars, int nconsts], int bnd, int[nvars] vars, int[nconsts] consts){ | |
//In this generator, nvars is the number of variables and nconsts is the number of constants. | |
//the array vars contains the values of all the variables and the array consts of all the constants. | |
//Note that unlike problem 1, where you were generating ASTs, here you are synthesizing the actual function. | |
//Also note that you will probably need a separate generator for the boolean expressions. | |
if (bnd == 0) { | |
return {| vars[??] | consts[??] |}; | |
} | |
int t = ??; | |
if (t == 0) return vars[??]; | |
if (t == 1) return consts[??]; | |
int a = exp(bnd-1, vars, consts); | |
int b = exp(bnd-1, vars, consts); | |
if (t == 2) return a + b; | |
if (t == 3) { | |
assert a < 1000; | |
assert b < 1000; | |
return a * b; | |
} | |
bit c = boolExp(bnd-1, vars, consts); | |
return c ? a : b; | |
} | |
generator bit boolExp([int nvars, int nconsts], int bnd, int[nvars] vars, int[nconsts] consts) { | |
if (bnd == 0) { | |
return false; | |
} | |
int t = ??; | |
if (t == 0) return false; | |
bit a = boolExp(bnd-1, vars, consts); | |
if (t == 1) return !a; | |
bit b = boolExp(bnd-1, vars, consts); | |
if (t == 2) return a && b; | |
return exp(bnd-1, vars, consts) < exp(bnd-1, vars, consts); | |
} | |
// Seems to suffer a worse blowup in speed than the randomized generator, and is not | |
// biased towards small expressions. | |
harness void experiment2(){ | |
//Use this harness for the example from 1.e | |
//Assume that x is the first variable and y is the second variable, so the | |
//input x=10 and y=7, for example will correspond to an array {10,7}. | |
int g(int x, int y) { | |
return exp(3, {x, y}, {-1}); | |
}; | |
assert g(10,7) == 17; | |
assert g(4,7) == -7; | |
assert g(10,3) == 13; | |
assert g(1, -7)== -6; | |
assert g(1, 8) == -8; | |
} | |
// Seems to suffer a worse blowup in speed than the randomized generator, and is not | |
// biased towards small expressions. | |
harness void experiment1(){ | |
//Use this harness for the example from 1.b | |
//Assume that x is the first variable and y is the second variable, so the | |
//input x=8 and y=3, for example will correspond to an array {8,3}. | |
int f(int x, int y) { | |
return exp(3, {x, y}, {}); | |
}; | |
assert f(5,5) == 15; | |
assert f(8,3) == 14; | |
assert f(1234,227) == 1688; | |
} | |
generator int exp2([int nvars, int nconsts], int bnd, int[nvars] vars, int[nconsts] consts){ | |
int t = ??; | |
if (t == 0 || bnd == 0) return nonAdditionExp(bnd, vars, consts); | |
// Addition restrictions | |
return nonAdditionExp(bnd-1, vars, consts) + nonAdditionExp(bnd-1, vars, consts); | |
} | |
generator int nonAdditionExp([int nvars, int nconsts], int bnd, int[nvars] vars, int[nconsts] consts){ | |
if (bnd == 0) { | |
return {| vars[??] | consts[??] |}; | |
} | |
int t = ??; | |
if (t == 0) return vars[??]; | |
if (t == 1) return consts[??]; | |
// Multiplication restrictions | |
if (t == 2) return vars[??] * vars[??]; | |
if (t == 3) return consts[??] * vars[??]; | |
bit c = boolExp(bnd-1, vars, consts); | |
int a = exp2(bnd-1, vars, consts); | |
int b = exp2(bnd-1, vars, consts); | |
return c ? a : b; | |
} | |
generator bit atomicBoolExp([int nvars, int nconsts], int bnd, int[nvars] vars, int[nconsts] consts) { | |
int t = ??; | |
if (t == 0 || bnd == 0) return false; | |
bit a = atomicBoolExp(bnd-1, vars, consts); | |
if (t == 1) return !a; | |
return exp2(bnd-1, vars, consts) < exp2(bnd-1, vars, consts); | |
} | |
generator bit boolExp2([int nvars, int nconsts], int bnd, int[nvars] vars, int[nconsts] consts) { | |
if (bnd == 0) { | |
return false; | |
} | |
int t = ??; | |
// Boolean restriction | |
if (t == 0) return atomicBoolExp(bnd, vars, consts); | |
bit a = boolExp(bnd-1, vars, consts); | |
bit b = boolExp(bnd-1, vars, consts); | |
return a && b; | |
} | |
// Seems to suffer a worse blowup in speed than the randomized generator, and is not | |
// biased towards small expressions. | |
harness void experiment2_2(){ | |
//Use this harness for the example from 1.e | |
//Assume that x is the first variable and y is the second variable, so the | |
//input x=10 and y=7, for example will correspond to an array {10,7}. | |
int g2(int x, int y) { | |
return exp2(3, {x, y}, {-1}); | |
}; | |
assert g2(10,7) == 17; | |
assert g2(4,7) == -7; | |
assert g2(10,3) == 13; | |
assert g2(1, -7)== -6; | |
assert g2(1, 8) == -8; | |
} | |
// Seems to suffer a worse blowup in speed than the randomized generator, and is not | |
// biased towards small expressions. | |
harness void experiment1_2(){ | |
//Use this harness for the example from 1.b | |
//Assume that x is the first variable and y is the second variable, so the | |
//input x=8 and y=3, for example will correspond to an array {8,3}. | |
int f2(int x, int y) { | |
return exp2(3, {x, y}, {2}); | |
}; | |
assert f2(5,5) == 15; | |
assert f2(8,3) == 14; | |
assert f2(1234,227) == 1688; | |
} | |
/* | |
* I am continually getting errors of the following form: | |
* -------------------------------------------------------------------------------- | |
* Error: NotesToSolver::processArith: This should not happen here 262551 262550 | |
* | |
* ERROR WAS IN THE FOLLOWING NODE: name_8438__TIMES | |
* | |
* | |
* ** Rejected | |
* [1425055485.9130 - ERROR] [SKETCH] Sketch Not Resolved Error: Error: NotesToSolver::processArith: This should not happen here 262551 262550 | |
* | |
* -------------------------------------------------------------------------------- | |
* | |
* I have only found two classes of functions: Those that synthesize quickly, and those that produce this error. I have not been | |
* able to find a satisfiable sketch which times out and does not produce this error. I have thus failed to complete question 3d | |
*/ | |
/* | |
* One failed attempt: Triangle classification function (processArith error) | |
* | |
* (z < x * x + y *y) ? 0 : (x * x + y * y < z) ? 2 : 1 | |
*/ | |
/* | |
harness void large_1() { | |
int l1(int x, int y, int z) { | |
return exp(5, {x, y, z}, {0,1,2}); | |
}; | |
assert l1(3,4,5) == 1; | |
assert l1(3,4,4) == 0; | |
assert l1(3,4,6) == 2; | |
assert l1(5,12,13) == 1; | |
assert l1(5,12,12) == 0; | |
assert l1(5,12,14) == 2; | |
assert l1(16,30,34) == 1; | |
assert l1(16,30,33) == 0; | |
assert l1(16,30,35) == 2; | |
} | |
*/ | |
/* | |
* Another failed attempt: x == 7 (again, processArith error) | |
* | |
* (!(x < 7) && !(7 < x)) ? 1 : 0 | |
*/ | |
/*harness void large_1() { | |
int l1(int x) { | |
return exp(5, {x}, {0,1,7}); | |
}; | |
assert l1(0) == 0; | |
assert l1(1) == 0; | |
assert l1(2) == 0; | |
assert l1(3) == 0; | |
assert l1(4) == 0; | |
assert l1(5) == 0; | |
assert l1(6) == 0; | |
assert l1(7) == 1; | |
assert l1(8) == 0; | |
assert l1(9) == 0; | |
assert l1(10) == 0; | |
assert l1(11) == 0; | |
} | |
*/ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment