Commit: c31969cb1304d7bdab0154b4c0038ca5a017c6ca - IPOGwBDD (git)

IPODwBDD

Commit MetaInfo

• Revision: c31969cb1304d7bdab0154b4c0038ca5a017c6ca (tree)
• Time: 2019-01-07 06:56:03
• Author: Tatsuhiro Tsuchiya <tatsuhiro@ieee...>
• Commiter: Tatsuhiro Tsuchiya

Log Message

Build Boolean expression representing all constraints

Change Summary

• modified: src/v1/Node.java
• modified: src/v1/SATConstraintHandler.java

Incremental Difference

--- a/src/v1/Node.java
+++ b/src/v1/Node.java
@@ -2,6 +2,8 @@
 
 import jdd.bdd.*;
 import bits.*;
+import bits.exceptions.ProblemDenierException;
+
 import java.util.*;
 
 abstract class Node {
@@ -27,8 +29,22 @@ class NotOperator extends BooleanUnaryOperator {
 
 	@Override
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
-		// TODO Auto-generated method stub
-		return null;
+		IProblem res = null;
+		try {
+			IProblem child = Child.buildSAT(restricted, boolenVariables);
+//			if (child == null)
+//				res = Problem.trivialProblem();
+//			else if (child.numberOfClauses() == 0)
+//				res = Problem.unsolvableProblem();
+//			else {
+//				res = new ProblemDenier(child);
+//			}
+			res = new ProblemDenier(child);
+		}
+		catch (Exception e) {
+			e.printStackTrace();
+		}
+		return res;
 	}
 }
 
@@ -49,8 +65,14 @@ class IfOperator extends BooleanBinaryOperator {
 
 	@Override
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
-		// TODO Auto-generated method stub
-		return null;
+		IProblem res = null;
+		try {
+			IProblem tmp = new ProblemDenier(Left.buildSAT(restricted, boolenVariables));
+			res = new Disjunction(tmp, Right.buildSAT(restricted, boolenVariables)); 
+		} catch (Exception e) {
+			e.printStackTrace();
+		}
+		return res;
 	}
 }
 
@@ -67,8 +89,14 @@ class EqualityOperator extends BooleanBinaryOperator {
 
 	@Override
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
-		// TODO Auto-generated method stub
-		return null;
+		IProblem res = null;
+		try {
+			res = new ProblemDenier(new ExclusiveDisjunction(Left.buildSAT(restricted, boolenVariables), 
+					Right.buildSAT(restricted, boolenVariables)));		
+		} catch (Exception e) {
+			e.printStackTrace();
+		}
+		return res;
 	}
 }
 
@@ -85,8 +113,14 @@ class InequalityOperator extends BooleanBinaryOperator {
 
 	@Override
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
-		// TODO Auto-generated method stub
-		return null;
+		IProblem res = null;
+		try {
+			res = new ExclusiveDisjunction(Left.buildSAT(restricted, boolenVariables), 
+					Right.buildSAT(restricted, boolenVariables));		
+		} catch (Exception e) {
+			e.printStackTrace();
+		}
+		return res;
 	}
 }
 
@@ -107,10 +141,22 @@ class IfthenelseOperator extends BooleanTrinaryOperator {
 		return f;
 	}
 
+	
 	@Override
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
-		// TODO Auto-generated method stub
-		return null;
+		// if p then q else r = (!p || q) && (p || r)
+		IProblem res = null;
+		try {
+			IProblem p = Left.buildSAT(restricted, boolenVariables);
+			IProblem q = Middle.buildSAT(restricted, boolenVariables);
+			IProblem r = Right.buildSAT(restricted, boolenVariables);
+			IProblem ifPart = new Disjunction(new ProblemDenier(p), q);
+			IProblem thenPart = new Disjunction(p, r);
+			res = new Conjunction(ifPart, thenPart);		
+		} catch (Exception e) {
+			e.printStackTrace();
+		}
+		return res; 
 	}
 }
 
@@ -140,21 +186,36 @@ class OrOperator extends BooleanMultinaryOperator {
 	}
 
 	@Override
+//	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
+//		IProblem res = null;
+//		try {
+//			res = new Disjunction(ChildList.get(0).buildSAT(restricted, boolenVariables), 
+//				ChildList.get(1).buildSAT(restricted, boolenVariables));
+//			for (int i = 2; i < ChildList.size(); i++) {
+//				res = new Disjunction(res, ChildList.get(i).buildSAT(restricted, boolenVariables));
+//			}
+//			
+//		}
+//		catch (Exception e) {
+//			e.printStackTrace();
+//		}
+//		return res;
+//	}
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
 		IProblem res = null;
 		try {
-			res = new Disjunction(ChildList.get(0).buildSAT(restricted, boolenVariables), 
-				ChildList.get(1).buildSAT(restricted, boolenVariables));
-			for (int i = 2; i < ChildList.size(); i++) {
-				res = new Disjunction(res, ChildList.get(i).buildSAT(restricted, boolenVariables));
+			IProblem[] problemArray = new IProblem[ChildList.size()];
+			for (int i = 0; i < ChildList.size(); i++) {
+				problemArray[i] = ChildList.get(i).buildSAT(restricted, boolenVariables);
 			}
-			
+			res = new Disjunction(problemArray);
 		}
 		catch (Exception e) {
 			e.printStackTrace();
 		}
 		return res;
 	}
+	
 }
 
 class AndOperator extends BooleanMultinaryOperator {
@@ -178,22 +239,39 @@ class AndOperator extends BooleanMultinaryOperator {
 		return f;
 	}
 
+//	@Override
+//	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
+//		IProblem res = null;
+//		try {
+//			res = new Conjunction(ChildList.get(0).buildSAT(restricted, boolenVariables), 
+//				ChildList.get(1).buildSAT(restricted, boolenVariables));
+//			for (int i = 2; i < ChildList.size(); i++) {
+//				res = new Conjunction(res, ChildList.get(i).buildSAT(restricted, boolenVariables));
+//			}
+//			
+//		}
+//		catch (Exception e) {
+//			e.printStackTrace();
+//		}
+//		return res;
+//	}
+
 	@Override
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
 		IProblem res = null;
 		try {
-			res = new Conjunction(ChildList.get(0).buildSAT(restricted, boolenVariables), 
-				ChildList.get(1).buildSAT(restricted, boolenVariables));
-			for (int i = 2; i < ChildList.size(); i++) {
-				res = new Conjunction(res, ChildList.get(i).buildSAT(restricted, boolenVariables));
+			IProblem[] problemArray = new IProblem[ChildList.size()];
+			for (int i = 0; i < ChildList.size(); i++) {
+				problemArray[i] = ChildList.get(i).buildSAT(restricted, boolenVariables);
 			}
-			
+			res = new Conjunction(problemArray);
 		}
 		catch (Exception e) {
 			e.printStackTrace();
 		}
 		return res;
 	}
+
 }
 
 abstract class AtomicExpression extends Node {
@@ -214,13 +292,21 @@ class TrueValue extends Constant {
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
 		IProblem res = null;
 		try {
-			IBooleanVariable dum = BooleanVariable.getBooleanVariable("dum");
-			res = new Problem(new IClause[]	{ new Clause().or(dum),	new Clause().orNot(dum) });		
+			res = Problem.trivialProblem();
 		} catch (Exception e) {
 			e.printStackTrace();
 		}
 		return res;
 	}
+//		IProblem res = null;
+//		try {
+//			IBooleanVariable dum = BooleanVariable.getBooleanVariable("dum");
+//			res = new Problem(new IClause[]	{ new Clause().or(dum),	new Clause().orNot(dum) });		
+//		} catch (Exception e) {
+//			e.printStackTrace();
+//		}
+//		return res;
+//	}
 }
 
 class FalseValue extends Constant {
@@ -236,13 +322,23 @@ class FalseValue extends Constant {
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
 		IProblem res = null;
 		try {
-			IBooleanVariable dum = BooleanVariable.getBooleanVariable("dum");
-			res = new Problem(new IClause[]	{ new Clause().or(dum),	new Clause().orNot(dum) });		
+			res = Problem.unsolvableProblem();
 		} catch (Exception e) {
 			e.printStackTrace();
 		}
 		return res;
 	}
+	
+//	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
+//		IProblem res = null;
+//		try {
+//			IBooleanVariable dum = BooleanVariable.getBooleanVariable("dum");
+//			res = new Problem(new IClause[]	{ new Clause().or(dum),	new Clause().orNot(dum) });		
+//		} catch (Exception e) {
+//			e.printStackTrace();
+//		}
+//		return res;
+//	}
 }
 
 abstract class ComparisonOfValueAndValue extends AtomicExpression {
@@ -298,15 +394,21 @@ class EqualityOfParameterAndValue extends ComparisonOfParameterAndValue {
 
 	@Override
 	IProblem buildSAT(ArrayList<ParaIDAndNumLevels> restricted, IBooleanVariable[][] boolenVariables) {
-		// TODO Auto-generated method stub
 		// System.out.println("[" + p +"] = " + v);
+		// pは（絶対値で）パラメータの番号が既にはいっている
+		int num = 0;
+		for (ParaIDAndNumLevels i: restricted) {
+			if (i.getID() == p)  {
+				break;
+			}
+			num++;
+		}
 		
 		IProblem res = null;
 		try {
-			res = new BitFixer(boolenVariables[p][v], true);
-			System.out.println(res);		
+			res = new BitFixer(boolenVariables[num][v], true);
+			// System.out.println(res);		
 		} catch (Exception e) {
-			// TODO Auto-generated catch block
 			e.printStackTrace();
 		}
 		return res;

--- a/src/v1/SATConstraintHandler.java
+++ b/src/v1/SATConstraintHandler.java
@@ -14,6 +14,9 @@ class SATConstraintHandler implements ConstraintHandler {
 	// BooleanVariables
 	private IBooleanVariable[][] booleanVariables = null;
 	
+	// Constraints 
+	private IProblem booleanConstraint = null;
+	
 	SATConstraintHandler(PList parameterList, List<Node> constraintList,
 			TreeSet<Integer> constrainedParametersArg) {
 		// set -> arrayList
@@ -34,31 +37,40 @@ class SATConstraintHandler implements ConstraintHandler {
 				for (int j = 0; j < pidlevels.getNumLevels(); j++) {
 					String str = "p" + pidlevels.getID() + "_" + j;
 					booleanVariables[i][j] = BooleanVariable.getBooleanVariable(str);
-					System.err.println(str);
+					// System.err.println(str);
 				}
+				i++;
 			}
 
-			IBooleanVariable x = BooleanVariable.getBooleanVariable("x");
-			IBooleanVariable y = BooleanVariable.getBooleanVariable("y");
-			IBooleanVariable z = BooleanVariable.getBooleanVariable("z");
-			// Construct the object that implements the constraint x & y = z :
-			IProblem bitAnder1 = new BitAnder(x, y, z);
-			System.out.println(bitAnder1);
-			System.out.println(bitAnder1.solve(Problem.defaultSolver()));
+//			IBooleanVariable x = BooleanVariable.getBooleanVariable("x");
+//			IBooleanVariable y = BooleanVariable.getBooleanVariable("y");
+//			IBooleanVariable z = BooleanVariable.getBooleanVariable("z");
+//			// Construct the object that implements the constraint x & y = z :
+//			IProblem bitAnder1 = new BitAnder(x, y, z);
+//			System.out.println(bitAnder1);
+//			System.out.println(bitAnder1.solve(Problem.defaultSolver()));
 		} catch (Exception e) {
 			// TODO Auto-generated catch block
 			e.printStackTrace();
 		}
 		
-		setSATConstraint(constraintList);
+		booleanConstraint = setSATConstraint(constraintList);
 	}
 
-	private int setSATConstraint(List<Node> constraintList) {	
+	private IProblem setSATConstraint(List<Node> constraintList) {	
 		// 制約式の論理積をとる
-		for (Node n : constraintList) {		
-			IProblem g = n.buildSAT(parameterToIDAndNumLevels, booleanVariables);
+		IProblem[] problemArray = new IProblem[constraintList.size()];
+		for (int i = 0; i < constraintList.size(); i++) {
+			problemArray[i] = constraintList.get(i).buildSAT(parameterToIDAndNumLevels, booleanVariables);
+		}
+		IProblem res = null;
+		try {
+			res = new Conjunction(problemArray);
+		}
+		catch (Exception e) {
+			e.printStackTrace();
 		}
-		return 0;
+		return res;
 	}
 	
 	@Override