OSDN > Developer > tallman > Chamber > cit_bach > Commit

CIT-BACH
Fork

Commit

Version 1.10
- Support arithmetic comparators: ===, !==, <, >, <=, >=.
- Memory usage reduction in BDD construction

--- a/src/v1/ConstraintHandler.java

+++ b/src/v1/ConstraintHandler.java

		@@ -169,6 +169,7 @@ class ConstraintHandler {
169	169
170	170	private int extendBddConstraint(int constraint) {
171	171	int f = constraint;
	172	+
172	173	for (VariableAndBDD p : parameters) {
173	174	int cube = p.var[0];
174	175	bdd.ref(cube);

		@@ -179,12 +180,13 @@ class ConstraintHandler {
179	180	}
180	181	int tmp0 = bdd.ref(bdd.exists(f, cube));
181	182	int tmp = bdd.ref(bdd.and(tmp0, cube));
182		- int newf = bdd.ref(bdd.or(f, tmp));
183		-
184		- bdd.deref(cube);
	183	+ bdd.deref(cube);
185	184	bdd.deref(tmp0);
	185	+
	186	+ int newf = bdd.ref(bdd.or(f, tmp));
186	187	bdd.deref(tmp);
187	188	bdd.deref(f);
	189	+
188	190	f = newf;
189	191	}
190	192	return f;

		@@ -289,7 +291,6 @@ class ConstraintHandler {
289	291	i++;
290	292	}
291	293
292		-
293	294	/* for debug
294	295	test.print(); for (int k = 0; k < res.length; k++)
295	296	System.err.print(res[k] ? 1 : 0); System.err.println("<*");

--- a/src/v1/Generator.java

+++ b/src/v1/Generator.java

		@@ -233,6 +233,8 @@ class Generator2 extends Generator {
233	233
234	234	boolean isSeedUsed = false;
235	235
	236	+ // debug: System.err.print("seedrownum: " + seedrownum + "-> ");
	237	+
236	238	// seedのコピー　制約を満たさなかったらエラー
237	239	if (seed.size() > 0 && seedrownum < seed.size()) {
238	240	isSeedUsed = true;

		@@ -284,8 +286,12 @@ class Generator2 extends Generator {
284	286	res.numOfCoveredTuples = newtuples;
285	287	if (isSeedUsed) {
286	288	res.nextSeedRow = seedrownum + 1;
287		- } else
	289	+ } else {
288	290	res.nextSeedRow = seedrownum;
	291	+ }
	292	+
	293	+ // debug: System.err.println("next seed row:" + res.nextSeedRow);
	294	+
289	295	return res;
290	296	}
291	297

		@@ -431,6 +437,9 @@ class Generator2 extends Generator {
431	437	for (int j = i + 1; j < numOfParameters; j++) {
432	438	if (tab.get(i, test.get(i), j, test.get(j)) == false) {
433	439	tab.set(i, test.get(i), j, test.get(j));
	440	+
	441	+ // debug: System.err.println(i + ":" + test.get(i)+", " + j + ":" + test.get(j));
	442	+
434	443	numOfNewlyCoveredTuples++;
435	444	}
436	445	}