Skip to content

Commit 901a296

Browse files
authored
Merge pull request #21 from dhendriks/18-release-2.0
#18 Prepare for release 2.0
2 parents ec32097 + 13807d7 commit 901a296

File tree

5 files changed

+205
-42
lines changed

5 files changed

+205
-42
lines changed

pom.xml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
2-
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
1+
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
32

43
<modelVersion>4.0.0</modelVersion>
54

src/main/java/com/github/javabdd/BDD.java

Lines changed: 29 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -163,6 +163,7 @@ public BDD and(BDD that) {
163163
* </p>
164164
*
165165
* @param that the BDD to 'and' with
166+
* @return the logical 'and' of the two BDDs
166167
*/
167168
public BDD andWith(BDD that) {
168169
return this.applyWith(that, BDDFactory.and);
@@ -191,6 +192,7 @@ public BDD or(BDD that) {
191192
* </p>
192193
*
193194
* @param that the BDD to 'or' with
195+
* @return the logical 'or' of the two BDDs
194196
*/
195197
public BDD orWith(BDD that) {
196198
return this.applyWith(that, BDDFactory.or);
@@ -219,6 +221,7 @@ public BDD xor(BDD that) {
219221
* </p>
220222
*
221223
* @param that the BDD to 'xor' with
224+
* @return the logical 'xor' of the two BDDs
222225
*/
223226
public BDD xorWith(BDD that) {
224227
return this.applyWith(that, BDDFactory.xor);
@@ -247,6 +250,7 @@ public BDD imp(BDD that) {
247250
* </p>
248251
*
249252
* @param that the BDD to 'implication' with
253+
* @return the logical 'implication' of the two BDDs
250254
*/
251255
public BDD impWith(BDD that) {
252256
return this.applyWith(that, BDDFactory.imp);
@@ -276,6 +280,7 @@ public BDD biimp(BDD that) {
276280
* </p>
277281
*
278282
* @param that the BDD to 'bi-implication' with
283+
* @return the logical 'bi-implication' of two BDDs
279284
*/
280285
public BDD biimpWith(BDD that) {
281286
return this.applyWith(that, BDDFactory.biimp);
@@ -426,6 +431,7 @@ public BDD relprod(BDD that, BDDVarSet var) {
426431
* </p>
427432
*
428433
* @param var BDD containing the variables to be restricted
434+
* @return the result of the restrict operation
429435
* @see com.github.javabdd.BDDDomain#set()
430436
*/
431437
public abstract BDD restrictWith(BDD var);
@@ -456,7 +462,7 @@ public BDD relprod(BDD that, BDDVarSet var) {
456462
public abstract BDDVarSet support();
457463

458464
/**
459-
* Returns the result of applying the binary operator <tt>opr</tt> to the two BDDs.
465+
* Returns the result of applying the binary operator {@code opr} to the two BDDs.
460466
*
461467
* <p>
462468
* Compare to bdd_apply.
@@ -469,7 +475,7 @@ public BDD relprod(BDD that, BDDVarSet var) {
469475
public abstract BDD apply(BDD that, BDDFactory.BDDOp opr);
470476

471477
/**
472-
* Makes this BDD be the result of the binary operator <tt>opr</tt> of two BDDs. The "that" BDD is consumed, and can
478+
* Makes this BDD be the result of the binary operator {@code opr} of two BDDs. The "that" BDD is consumed, and can
473479
* no longer be used. Attempting to use the passed in BDD again will result in an exception being thrown.
474480
*
475481
* <p>
@@ -478,12 +484,13 @@ public BDD relprod(BDD that, BDDVarSet var) {
478484
*
479485
* @param that the BDD to apply the operator on
480486
* @param opr the operator to apply
487+
* @return the result of applying the operator
481488
*/
482489
public abstract BDD applyWith(BDD that, BDDFactory.BDDOp opr);
483490

484491
/**
485-
* Applies the binary operator <tt>opr</tt> to two BDDs and then performs a universal quantification of the
486-
* variables from the variable set <tt>var</tt>.
492+
* Applies the binary operator {@code opr} to two BDDs and then performs a universal quantification of the variables
493+
* from the variable set {@code var}.
487494
*
488495
* <p>
489496
* Compare to bdd_appall.
@@ -498,8 +505,8 @@ public BDD relprod(BDD that, BDDVarSet var) {
498505
public abstract BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var);
499506

500507
/**
501-
* Applies the binary operator <tt>opr</tt> to two BDDs and then performs an existential quantification of the
502-
* variables from the variable set <tt>var</tt>.
508+
* Applies the binary operator {@code opr} to two BDDs and then performs an existential quantification of the
509+
* variables from the variable set {@code var}.
503510
*
504511
* <p>
505512
* Compare to bdd_appex.
@@ -514,8 +521,8 @@ public BDD relprod(BDD that, BDDVarSet var) {
514521
public abstract BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var);
515522

516523
/**
517-
* Applies the binary operator <tt>opr</tt> to two BDDs and then performs a unique quantification of the variables
518-
* from the variable set <tt>var</tt>.
524+
* Applies the binary operator {@code opr} to two BDDs and then performs a unique quantification of the variables
525+
* from the variable set {@code var}.
519526
*
520527
* <p>
521528
* Compare to bdd_appuni.
@@ -554,9 +561,9 @@ public BDD relprod(BDD that, BDDVarSet var) {
554561
public abstract BDD fullSatOne();
555562

556563
/**
557-
* Finds one satisfying variable assignment. Finds a minterm in this BDD. The <tt>var</tt> argument is a set of
564+
* Finds one satisfying variable assignment. Finds a minterm in this BDD. The {@code var} argument is a set of
558565
* variables that must be mentioned in the result. The polarity of these variables in the result - in case they are
559-
* undefined in this BDD - are defined by the <tt>pol</tt> parameter. If <tt>pol</tt> is false, then all variables
566+
* undefined in this BDD - are defined by the {@code pol} parameter. If {@code pol} is false, then all variables
560567
* will be in negative form. Otherwise they will be in positive form.
561568
*
562569
* <p>
@@ -723,7 +730,7 @@ public void remove() {
723730
}
724731

725732
/**
726-
* Finds one satisfying assignment of the domain <tt>d</tt> in this BDD and returns that value.
733+
* Finds one satisfying assignment of the domain {@code d} in this BDD and returns that value.
727734
*
728735
* <p>
729736
* Compare to fdd_scanvar.
@@ -817,8 +824,8 @@ public BigInteger[] scanAllVar() {
817824
*/
818825

819826
/**
820-
* Returns an iteration of the satisfying assignments of this BDD. Returns an iteration of minterms. The
821-
* <tt>var</tt> argument is the set of variables that will be mentioned in the result.
827+
* Returns an iteration of the satisfying assignments of this BDD. Returns an iteration of minterms. The {@code var}
828+
* argument is the set of variables that will be mentioned in the result.
822829
*
823830
* @param var set of variables to mention in result
824831
* @return an iteration of minterms
@@ -1053,8 +1060,8 @@ public void remove() {
10531060
}
10541061

10551062
/**
1056-
* Returns true if the given BDD variable number is a dont-care. <tt>var</tt> must be a variable in the
1057-
* iteration set.
1063+
* Returns true if the given BDD variable number is a dont-care. {@code var} must be a variable in the iteration
1064+
* set.
10581065
*
10591066
* @param var variable number to check
10601067
* @return if the given variable is a dont-care
@@ -1116,7 +1123,7 @@ public void fastForward(int[] vars) {
11161123
}
11171124

11181125
/**
1119-
* Assuming <tt>d</tt> is a dont-care, skip to the end of the iteration for <tt>d</tt>.
1126+
* Assuming {@code d} is a dont-care, skip to the end of the iteration for {@code d}.
11201127
*
11211128
* @param d BDD domain to fast-forward past
11221129
*/
@@ -1153,6 +1160,7 @@ public void skipDontCare(BDDDomain d) {
11531160
* </p>
11541161
*
11551162
* @param pair pairing of variables to the BDDs that replace those variables
1163+
* @return result of replace
11561164
*/
11571165
public abstract BDD replaceWith(BDDPairing pair);
11581166

@@ -1285,6 +1293,7 @@ protected int printdot_rec(PrintStream out, int current, boolean[] visited, Hash
12851293
* Compare to bdd_satcountset.
12861294
* </p>
12871295
*
1296+
* @param varset the given varset
12881297
* @return the number of satisfying variable assignments
12891298
*/
12901299
public double satCount(BDDVarSet varset) {
@@ -1321,6 +1330,7 @@ public double logSatCount() {
13211330
* Compare to bdd_satcountset.
13221331
* </p>
13231332
*
1333+
* @param varset the given varset
13241334
* @return the logarithm of the number of satisfying variable assignments
13251335
*/
13261336
public double logSatCount(BDDVarSet varset) {
@@ -1334,6 +1344,8 @@ public double logSatCount(BDDVarSet varset) {
13341344
* <p>
13351345
* Compare to bdd_varprofile.
13361346
* </p>
1347+
*
1348+
* @return the variable profile
13371349
*/
13381350
public abstract int[] varProfile();
13391351

@@ -1434,8 +1446,8 @@ public String toStringWithDomains() {
14341446
/**
14351447
* Returns a string representation of this BDD on the defined domains, using the given BDDToString converter.
14361448
*
1449+
* @param ts the given BDDToString converter
14371450
* @return string representation of this BDD using the given BDDToString converter
1438-
*
14391451
* @see com.github.javabdd.BDD.BDDToString
14401452
*/
14411453
public String toStringWithDomains(BDDToString ts) {

src/main/java/com/github/javabdd/BDDDomain.java

Lines changed: 30 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
* </p>
1818
*
1919
* <p>
20-
* Use <tt>BDDFactory.extDomain()</tt> to create one or more domains with a specified list of sizes.
20+
* Use {@code BDDFactory.extDomain()} to create one or more domains with a specified list of sizes.
2121
* </p>
2222
*
2323
* @see com.github.javabdd.BDDFactory#extDomain(int[])
@@ -63,25 +63,33 @@ protected BDDDomain(int index, BigInteger range) {
6363

6464
/**
6565
* Returns the factory that created this domain.
66+
*
67+
* @return the BDD factory
6668
*/
6769
public abstract BDDFactory getFactory();
6870

6971
/**
7072
* Sets the name of this domain.
73+
*
74+
* @param name the name
7175
*/
7276
public void setName(String name) {
7377
this.name = name;
7478
}
7579

7680
/**
7781
* Gets the name of this domain.
82+
*
83+
* @return the name
7884
*/
7985
public String getName() {
8086
return name;
8187
}
8288

8389
/**
8490
* Returns the index of this domain.
91+
*
92+
* @return the index
8593
*/
8694
public int getIndex() {
8795
return index;
@@ -94,6 +102,8 @@ public int getIndex() {
94102
* <p>
95103
* Compare to fdd_domain.
96104
* </p>
105+
*
106+
* @return BDD representing the possible values of this domain
97107
*/
98108
public BDD domain() {
99109
BDDFactory factory = getFactory();
@@ -119,6 +129,8 @@ public BDD domain() {
119129
* <p>
120130
* Compare to fdd_domainsize.
121131
* </p>
132+
*
133+
* @return the size
122134
*/
123135
public BigInteger size() {
124136
return this.realsize;
@@ -189,6 +201,7 @@ public BDD buildAdd(BDDDomain that, int bits, long value) {
189201
* Compare to fdd_equals/fdd_equ.
190202
* </p>
191203
*
204+
* @param that the other BDD domain
192205
* @return BDD
193206
*/
194207
public BDD buildEquals(BDDDomain that) {
@@ -233,6 +246,7 @@ public BDDVarSet set() {
233246
* Compare to fdd_ithvar.
234247
* </p>
235248
*
249+
* @param val the given value
236250
* @return BDD
237251
*/
238252
public BDD ithVar(long val) {
@@ -262,6 +276,8 @@ public BDD ithVar(BigInteger val) {
262276
/**
263277
* Returns the BDD that defines the given range of values, inclusive, for this finite domain block.
264278
*
279+
* @param lo low value (inclusive)
280+
* @param hi high value (inclusive)
265281
* @return BDD
266282
*/
267283
public BDD varRange(long lo, long hi) {
@@ -352,39 +368,40 @@ public String toString() {
352368
}
353369

354370
/**
355-
* Convert a BDD that to a list of indices of this domain. This method assumes that the BDD passed is a disjunction
356-
* of ithVar(i_1) to ithVar(i_k). It returns an array of length 'k' with elements [i_1,...,i_k].
371+
* Convert a BDD {@code that} to a list of indices of this domain. This method assumes that the BDD passed is a
372+
* disjunction of ithVar(i_1) to ithVar(i_k). It returns an array of length 'k' with elements [i_1,...,i_k].
357373
*
358374
* <p>
359375
* Be careful when using this method for BDDs with a large number of entries, as it allocates a BigInteger[] array
360376
* of dimension k.
361377
* </p>
362378
*
363-
* @param bdd bdd that is the disjunction of domain indices
379+
* @param that bdd that is the disjunction of domain indices
380+
* @return list of indices in this domain
364381
* @see #getVarIndices(BDD,int)
365382
* @see #ithVar(BigInteger)
366383
*/
367-
public BigInteger[] getVarIndices(BDD bdd) {
368-
return getVarIndices(bdd, -1);
384+
public BigInteger[] getVarIndices(BDD that) {
385+
return getVarIndices(that, -1);
369386
}
370387

371388
/**
372-
* Convert a BDD that to a list of indices of this domain. Same as getVarIndices(BDD), except only 'max' indices are
373-
* extracted.
389+
* Convert a BDD {@code that} to a list of indices of this domain. Same as getVarIndices(BDD), except only 'max'
390+
* indices are extracted.
374391
*
375-
* @param bdd bdd that is the disjunction of domain indices
392+
* @param that bdd that is the disjunction of domain indices
376393
* @param max maximum number of entries to be returned
377-
*
394+
* @return list of indices of this domain
378395
* @see #ithVar(long)
379396
*/
380-
public BigInteger[] getVarIndices(BDD bdd, int max) {
397+
public BigInteger[] getVarIndices(BDD that, int max) {
381398
BDDVarSet myvarset = set(); // can't use var here, must respect subclass a factory may provide
382-
int n = (int)bdd.satCount(myvarset);
399+
int n = (int)that.satCount(myvarset);
383400
if (max != -1 && n > max) {
384401
n = max;
385402
}
386403
BigInteger[] res = new BigInteger[n];
387-
BDDIterator it = bdd.iterator(myvarset);
404+
BDDIterator it = that.iterator(myvarset);
388405
myvarset.free();
389406
for (int i = 0; i < n; i++) {
390407
res[i] = it.nextValue(this);

0 commit comments

Comments
 (0)