Commit e7810d42 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

Merge branch 'ReduceToCNFSAT'

# Conflicts:
#	src/vagabond/reduction/cnfsat/RunSolverCNFSAT.java
parents 2ed4678c cea060c0
......@@ -221,8 +221,20 @@ public class RunSolverCNFSAT implements RunSolver {
return s;
}
public void constraintInfoLeakUb(Circuit c, LessEquals le[], BigAndOr band, Sum s[], int nclientpairs, int ub)
throws Exception {
public void constraintInfoLeakUb(Circuit c, LessEquals le[], BigAndOr band[], Sum s[], int nclientpairs,
int ub, Circuit.Wire wirestoand[], int orignoutputs) throws Exception {
for (int i = 0; i < c.getOutputs().size(); i++)
c.removeAsOutput(c.getOutputs().get(0));
if (band[0] != null) {
c.removeAsOutput(band[0].getOutputs().get(0));
c.gates.removeAll(band[0].gates);
c.wires.removeAll(band[0].wires);
c.inputs.removeAll(band[0].wires);
c.outputs.removeAll(band[0].wires);
}
IntegerAsCircuit midc = new IntegerAsCircuit(ub);
c.union(midc);
for (int j = 0; j < midc.getOutputs().size(); j++) {
......@@ -231,6 +243,7 @@ public class RunSolverCNFSAT implements RunSolver {
for (int i = 0; i < le.length; i++) {
if (le[i] != null) {
c.removeAsOutput(le[i].getOutputs().get(0));
c.gates.removeAll(le[i].gates);
c.wires.removeAll(le[i].wires);
c.inputs.removeAll(le[i].wires);
......@@ -245,38 +258,32 @@ public class RunSolverCNFSAT implements RunSolver {
for (int j = 0; j < midc.getOutputs().size(); j++) {
c.fuse(midc.getOutputs().get(j), le[i].getInputs().get(j + s[i].getOutputs().size()));
}
}
if (band != null) {
c.gates.removeAll(band.gates);
c.wires.removeAll(band.wires);
c.inputs.removeAll(band.wires);
c.outputs.removeAll(band.wires);
wirestoand[orignoutputs + i] = le[i].getOutputs().get(0);
}
band = addBigAnd(c);
band[0] = addBigAnd(c, wirestoand);
}
/**
* Big AND of all the outputs of a circuit
*
* @param c the circuit whose outputs we should AND. This is an in-out param. I.e., c is changed up on return.
* @return the big-and circuit that was created
* @return
*/
public BigAndOr addBigAnd(Circuit c) {
public BigAndOr addBigAnd(Circuit c, Circuit.Wire wirestoand[]) {
BigAndOr band = null;
try {
band = new BigAndOr(false, c.getOutputs().size());
band = new BigAndOr(false, wirestoand.length);
c.union(band);
for (int i = 0; c.getOutputs().size() > 1; i++) {
c.fuse(c.getOutputs().get(0), band.getInputs().get(i));
c.removeAsOutput(c.getOutputs().get(0));
for (int i = 0; i < wirestoand.length; i++) {
c.fuse(wirestoand[i], band.getInputs().get(i));
c.removeAsOutput(wirestoand[i]);
}
} catch (Exception e) {
e.printStackTrace();
}
assert c.getOutputs().size() == 1;
return band;
}
......@@ -322,10 +329,22 @@ public class RunSolverCNFSAT implements RunSolver {
return null;
}
// All the sum circuits whose outputs we want to compare against are now in s[]
// At this point, we know how many output wires to AND with the <= circuit's output that's coming up
Circuit.Wire wirestoand[];
int orignoutputs = c.getOutputs().size();
int hi;
if (VagabondSettings.getInstance().minimizeMaxClientToClientInfoLeak) {
wirestoand = new Circuit.Wire[orignoutputs + nclientpairs];
} else {
wirestoand = new Circuit.Wire[orignoutputs + 1];
}
for (int i = 0; i < orignoutputs; i++) {
wirestoand[i] = c.getOutputs().get(0);
c.removeAsOutput(wirestoand[i]);
}
// All the sum circuits whose outputs we want to compare against are now in s[]
int hi;
if (VagabondSettings.getInstance().minimizeMaxClientToClientInfoLeak) {
int maxclientnv = -1;
for (int i = 0; i < _r.nv.size(); i++) {
......@@ -352,7 +371,8 @@ public class RunSolverCNFSAT implements RunSolver {
le[0] = null;
}
BigAndOr band = null;
BigAndOr band[] = new BigAndOr[1];
band[0] = null;
List<String> cnfcert = null;
// certificate from cnf-sat
......@@ -366,7 +386,7 @@ public class RunSolverCNFSAT implements RunSolver {
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::loopVal::" + searchVal);
// System.out.println("mid = "+mid); System.out.flush();
try {
constraintInfoLeakUb(c, le, band, s, nclientpairs, mid);
constraintInfoLeakUb(c, le, band, s, nclientpairs, mid, wirestoand, orignoutputs);
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::cnfSatToFile::" + searchVal);
// Now convert to cnf, invoke solver and adjust mid as needed.
......
......@@ -21,7 +21,7 @@ public class CNFEverythingTests {
@Test
public void equalSpreadTest() throws Exception {
boolean minMaxCtoCInfoLeak = false;
boolean minMaxCtoCInfoLeak = true;
VagabondSettings vs = VagabondSettings.getInstance();
vs.migrationBudget = new Integer(-1);
......@@ -60,7 +60,7 @@ public class CNFEverythingTests {
@Test
public void equalSpreadBiggerTest() throws Exception {
int testparam = 8;
int migbudget = -1;
int migbudget = 5;
boolean minMaxCtoCInfoLeak = false;
VagabondSettings vs = VagabondSettings.getInstance();
vs.migrationBudget = new Integer(migbudget);
......
......@@ -111,10 +111,15 @@ public class InfoLeakSumTests {
*/
LessEquals le[] = new LessEquals[nclientpairs];
BigAndOr band = null;
for(int i = 0; i < nclientpairs; i++) le[i] = null;
int ub = 4; // Change this as needed. < 3 should result in false. > 2 should result in true
rs.constraintInfoLeakUb(c, le, band, s, nclientpairs, ub);
Circuit.Wire wirestoand[] = new Circuit.Wire[c.getOutputs().size()];
for(int i = 0; i < wirestoand.length; i++) {
wirestoand[i] = c.getOutputs().get(i);
}
BigAndOr band[] = new BigAndOr[1]; band[0] = null;
rs.constraintInfoLeakUb(c, le, band, s, nclientpairs, ub, wirestoand, 0);
assertEquals(c.getOutputs().size(), 1);
......@@ -190,10 +195,14 @@ public class InfoLeakSumTests {
assertEquals(c.getOutputs().size(), 0);
LessEquals le[] = new LessEquals[nclientpairs];
BigAndOr band = null;
for(int i = 0; i < nclientpairs; i++) le[i] = null;
int ub = 5; // Change this as needed. < 8 should result in false. > 7 should result in true
rs.constraintInfoLeakUb(c, le, band, s, nclientpairs, ub);
Circuit.Wire wirestoand[] = new Circuit.Wire[c.getOutputs().size()];
for(int i = 0; i < wirestoand.length; i++) {
wirestoand[i] = c.getOutputs().get(i);
}
BigAndOr band[] = new BigAndOr[1]; band[0] = null;
rs.constraintInfoLeakUb(c, le, band, s, nclientpairs, ub, wirestoand, 0);
assertEquals(c.getOutputs().size(), 1);
......
......@@ -167,9 +167,13 @@ public class MigrationBudgetTests {
SumOfClientVMsPerMachine currp = new SumOfClientVMsPerMachine(PlacementMapExamples.equalSpreadClients());
r.constraintMigrationBudget(c, nc, nv, ns, currp, mig);
Circuit.Wire wirestoand[] = new Circuit.Wire[c.getOutputs().size()];
for(int i = 0; i < wirestoand.length; i++) {
wirestoand[i] = c.getOutputs().get(i);
}
//System.out.println(c.getOutputs().size());
(new RunSolverCNFSAT()).addBigAnd(c);
(new RunSolverCNFSAT()).addBigAnd(c, wirestoand);
System.out.println(c.getOutputs().size());
CircuitUtils.cnfSatToFile(c,"/home/tripunit/Desktop/instance.cnf");
......
......@@ -148,9 +148,14 @@ public class PlacementMapFromCNFSATTests {
Sum s[];
s = rs.constraintSumInfoLeak(c, _r, nclientpairs);
LessEquals le[] = new LessEquals[nclientpairs];
BigAndOr band = null;
for(int i = 0; i < le.length; i++) le[i] = null;
rs.constraintInfoLeakUb(c, le, band, s, nclientpairs, 6);
Circuit.Wire wirestoand[] = new Circuit.Wire[c.getOutputs().size()];
for(int i = 0; i < wirestoand.length; i++) {
wirestoand[i] = c.getOutputs().get(i);
}
BigAndOr band[] = new BigAndOr[1]; band[0] = null;
rs.constraintInfoLeakUb(c, le, band, s, nclientpairs, 6, wirestoand, 0);
CircuitUtils.cnfSatToFile(c, cnfloc);
Process p = Runtime.getRuntime().exec(solverloc+" "+cnfloc);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment