Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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