javabdd-checkins Mailing List for JavaBDD (Page 5)
Brought to you by:
joewhaley
Menu
▾
▴
javabdd-checkins — CVS updates. High traffic.
You can subscribe to this list here.
| 2003 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
(4) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2004 |
Jan
|
Feb
|
Mar
(6) |
Apr
(6) |
May
(4) |
Jun
(31) |
Jul
(64) |
Aug
(19) |
Sep
(28) |
Oct
(50) |
Nov
(25) |
Dec
|
| 2005 |
Jan
(44) |
Feb
(8) |
Mar
(2) |
Apr
(15) |
May
(48) |
Jun
(8) |
Jul
(7) |
Aug
|
Sep
(1) |
Oct
(3) |
Nov
|
Dec
|
| 2006 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(1) |
Jun
(2) |
Jul
(14) |
Aug
|
Sep
|
Oct
|
Nov
(6) |
Dec
(4) |
| 2007 |
Jan
|
Feb
|
Mar
(2) |
Apr
|
May
|
Jun
(1) |
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2010 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
(1) |
Nov
(1) |
Dec
|
| 2011 |
Jan
|
Feb
(2) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(1) |
Dec
|
| 2019 |
Jan
|
Feb
|
Mar
|
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: John W. <joe...@us...> - 2005-05-04 22:31:46
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv8676/net/sf/javabdd Modified Files: BuDDyFactory.java BDDFactory.java Added Files: CUDDFactory$1.class CALFactory$1.class TestBDDFactory$1.class BuDDyFactory$1.class JDDFactory$1.class BDDFactory$1.class Log Message: Don't use finalizer() on bdd factory objects by default. Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.10 retrieving revision 1.11 diff -C2 -d -r1.10 -r1.11 *** BuDDyFactory.java 4 May 2005 22:23:12 -0000 1.10 --- BuDDyFactory.java 4 May 2005 22:31:35 -0000 1.11 *************** *** 40,44 **** public static BDDFactory init(int nodenum, int cachesize) { ! BuDDyFactory f = new BuDDyFactory(); f.initialize(nodenum, cachesize); return f; --- 40,48 ---- public static BDDFactory init(int nodenum, int cachesize) { ! BuDDyFactory f; ! if (USE_FINALIZER) ! f = new BuDDyFactoryWithFinalizer(); ! else ! f = new BuDDyFactory(); f.initialize(nodenum, cachesize); return f; *************** *** 98,101 **** --- 102,117 ---- private static final boolean USE_FINALIZER = false; + private static class BuDDyFactoryWithFinalizer extends BuDDyFactory { + + /** + * @see java.lang.Object#finalize() + */ + protected void finalize() throws Throwable { + super.finalize(); + this.done(); + } + + } + private static BuDDyBDD makeBDD(int id) { BuDDyBDD b; --- NEW FILE: BDDFactory$1.class --- (This appears to be a binary file; contents omitted.) --- NEW FILE: TestBDDFactory$1.class --- (This appears to be a binary file; contents omitted.) --- NEW FILE: BuDDyFactory$1.class --- (This appears to be a binary file; contents omitted.) Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.10 retrieving revision 1.11 diff -C2 -d -r1.10 -r1.11 *** BDDFactory.java 29 Apr 2005 02:25:28 -0000 1.10 --- BDDFactory.java 4 May 2005 22:31:35 -0000 1.11 *************** *** 294,305 **** /** - * @see java.lang.Object#finalize() - */ - protected void finalize() throws Throwable { - super.finalize(); - this.done(); - } - - /** * <p>Sets the error condition. This will cause the BDD package to throw an * exception at the next garbage collection.</p> --- 294,297 ---- --- NEW FILE: JDDFactory$1.class --- (This appears to be a binary file; contents omitted.) --- NEW FILE: CUDDFactory$1.class --- (This appears to be a binary file; contents omitted.) --- NEW FILE: CALFactory$1.class --- (This appears to be a binary file; contents omitted.) |
|
From: John W. <joe...@us...> - 2005-05-04 22:23:21
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6129/net/sf/javabdd Modified Files: BuDDyFactory.java Log Message: Don't use finalizer() on bddpairs by default. Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.9 retrieving revision 1.10 diff -C2 -d -r1.9 -r1.10 *** BuDDyFactory.java 29 Apr 2005 02:25:28 -0000 1.9 --- BuDDyFactory.java 4 May 2005 22:23:12 -0000 1.10 *************** *** 345,349 **** public BDDPairing makePair() { long ptr = makePair0(); ! return new BuDDyBDDPairing(ptr); } private static native long makePair0(); --- 345,353 ---- public BDDPairing makePair() { long ptr = makePair0(); ! if (USE_FINALIZER) { ! return new BuDDyBDDPairingWithFinalizer(ptr); ! } else { ! return new BuDDyBDDPairing(ptr); ! } } private static native long makePair0(); *************** *** 1101,1104 **** --- 1105,1125 ---- private static native void reset0(long ptr); + /** + * Free the memory allocated for this pair. + */ + public void free() { + if (_ptr != 0) free0(_ptr); + _ptr = 0; + } + private static native void free0(long p); + + } + + private static class BuDDyBDDPairingWithFinalizer extends BuDDyBDDPairing { + + private BuDDyBDDPairingWithFinalizer(long ptr) { + super(ptr); + } + /* (non-Javadoc) * @see java.lang.Object#finalize() *************** *** 1106,1118 **** protected void finalize() throws Throwable { super.finalize(); ! if (_ptr != 0) free0(_ptr); ! _ptr = 0; } - /** - * Free the memory allocated for this pair. - */ - private static native void free0(long p); - } --- 1127,1133 ---- protected void finalize() throws Throwable { super.finalize(); ! free(); } } |
|
From: John W. <joe...@us...> - 2005-05-04 22:14:21
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4063/buddy/src Modified Files: pairs.c Log Message: Set pairs to null when calling bdd_done() so that we can reinitialize safely. Index: pairs.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/pairs.c,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** pairs.c 17 Apr 2005 10:21:27 -0000 1.4 --- pairs.c 4 May 2005 22:14:12 -0000 1.5 *************** *** 69,72 **** --- 69,73 ---- p = next; } + pairs = NULL; } |
|
From: John W. <joe...@us...> - 2005-04-29 06:44:14
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv23255/bdd Modified Files: BasicTests.java Log Message: Fixed imports. Index: BasicTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/BasicTests.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** BasicTests.java 17 Apr 2005 10:22:23 -0000 1.4 --- BasicTests.java 29 Apr 2005 06:44:03 -0000 1.5 *************** *** 10,16 **** import java.util.List; import java.util.Random; - import java.io.BufferedWriter; import java.io.IOException; - import java.io.PrintWriter; import java.math.BigInteger; import junit.framework.Assert; --- 10,14 ---- |
|
From: John W. <joe...@us...> - 2005-04-29 06:43:40
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22679/net/sf/javabdd Modified Files: JFactory.java MicroFactory.java BDDException.java Log Message: Added UID for serialization. Index: BDDException.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDException.java,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** BDDException.java 16 Oct 2004 02:58:57 -0000 1.1 --- BDDException.java 29 Apr 2005 06:43:31 -0000 1.2 *************** *** 11,14 **** --- 11,19 ---- */ public class BDDException extends RuntimeException { + /** + * Version ID for serialization. + */ + private static final long serialVersionUID = 3761969363112243251L; + public BDDException() { super(); Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.20 retrieving revision 1.21 diff -C2 -d -r1.20 -r1.21 *** JFactory.java 17 Apr 2005 10:21:46 -0000 1.20 --- JFactory.java 29 Apr 2005 06:43:31 -0000 1.21 *************** *** 607,610 **** --- 607,615 ---- private static class JavaBDDException extends BDDException { + /** + * Version ID for serialization. + */ + private static final long serialVersionUID = 3257289144995952950L; + public JavaBDDException(int x) { super(errorstrings[-x]); *************** *** 612,616 **** } ! private static class ReorderException extends RuntimeException {} static final int bddtrue = 1; --- 617,626 ---- } ! private static class ReorderException extends RuntimeException { ! /** ! * Version ID for serialization. ! */ ! private static final long serialVersionUID = 3256727264505772345L; ! } static final int bddtrue = 1; Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.9 retrieving revision 1.10 diff -C2 -d -r1.9 -r1.10 *** MicroFactory.java 17 Apr 2005 10:21:46 -0000 1.9 --- MicroFactory.java 29 Apr 2005 06:43:31 -0000 1.10 *************** *** 1225,1228 **** --- 1225,1233 ---- private static class JavaBDDException extends BDDException { + /** + * Version ID for serialization. + */ + private static final long serialVersionUID = 3257289123604607538L; + public JavaBDDException(int x) { super(errorstrings[-x]); |
|
From: John W. <joe...@us...> - 2005-04-29 02:25:38
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9291/net/sf/javabdd Modified Files: CALFactory.java TestBDDFactory.java BuDDyFactory.java CUDDFactory.java BDDFactory.java TypedBDDFactory.java Log Message: Many updates to support applet version. Index: TestBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TestBDDFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** TestBDDFactory.java 8 Apr 2005 05:27:52 -0000 1.6 --- TestBDDFactory.java 29 Apr 2005 02:25:28 -0000 1.7 *************** *** 30,35 **** public static BDDFactory init(int nodenum, int cachesize) { ! String bdd1 = System.getProperty("bdd1", "j"); ! String bdd2 = System.getProperty("bdd2", "micro"); BDDFactory a = BDDFactory.init(bdd1, nodenum, cachesize); BDDFactory b = BDDFactory.init(bdd2, nodenum, cachesize); --- 30,35 ---- public static BDDFactory init(int nodenum, int cachesize) { ! String bdd1 = getProperty("bdd1", "j"); ! String bdd2 = getProperty("bdd2", "micro"); BDDFactory a = BDDFactory.init(bdd1, nodenum, cachesize); BDDFactory b = BDDFactory.init(bdd2, nodenum, cachesize); Index: CALFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/CALFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** CALFactory.java 8 Apr 2005 05:27:52 -0000 1.5 --- CALFactory.java 29 Apr 2005 02:25:28 -0000 1.6 *************** *** 53,58 **** // Cannot find library, try loading it from the current directory... libname = System.mapLibraryName(libname); ! String currentdir = System.getProperty("user.dir"); ! String sep = System.getProperty("file.separator"); System.load(currentdir+sep+libname); } --- 53,58 ---- // Cannot find library, try loading it from the current directory... libname = System.mapLibraryName(libname); ! String currentdir = getProperty("user.dir", "."); ! String sep = getProperty("file.separator", "/"); System.load(currentdir+sep+libname); } Index: TypedBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TypedBDDFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** TypedBDDFactory.java 8 Apr 2005 05:27:52 -0000 1.6 --- TypedBDDFactory.java 29 Apr 2005 02:25:28 -0000 1.7 *************** *** 39,43 **** public static BDDFactory init(int nodenum, int cachesize) { BDDFactory a; ! String factoryName = System.getProperty("bdd"); if (factoryName != null && factoryName.equals("typed")) a = BuDDyFactory.init(nodenum, cachesize); --- 39,43 ---- public static BDDFactory init(int nodenum, int cachesize) { BDDFactory a; ! String factoryName = getProperty("bdd", null); if (factoryName != null && factoryName.equals("typed")) a = BuDDyFactory.init(nodenum, cachesize); Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.8 retrieving revision 1.9 diff -C2 -d -r1.8 -r1.9 *** BuDDyFactory.java 8 Apr 2005 05:27:52 -0000 1.8 --- BuDDyFactory.java 29 Apr 2005 02:25:28 -0000 1.9 *************** *** 51,55 **** static { ! String libname = System.getProperty("buddylib", "buddy"); try { System.loadLibrary(libname); --- 51,55 ---- static { ! String libname = getProperty("buddylib", "buddy"); try { System.loadLibrary(libname); *************** *** 57,62 **** // Cannot find library, try loading it from the current directory... libname = System.mapLibraryName(libname); ! String currentdir = System.getProperty("user.dir"); ! String sep = System.getProperty("file.separator"); String filename = currentdir+sep+libname; try { --- 57,62 ---- // Cannot find library, try loading it from the current directory... libname = System.mapLibraryName(libname); ! String currentdir = getProperty("user.dir", "."); ! String sep = getProperty("file.separator", "/"); String filename = currentdir+sep+libname; try { Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.9 retrieving revision 1.10 diff -C2 -d -r1.9 -r1.10 *** BDDFactory.java 17 Apr 2005 10:21:47 -0000 1.9 --- BDDFactory.java 29 Apr 2005 02:25:28 -0000 1.10 *************** *** 21,24 **** --- 21,25 ---- import java.lang.reflect.Modifier; import java.math.BigInteger; + import java.security.AccessControlException; /** *************** *** 32,35 **** --- 33,44 ---- public abstract class BDDFactory { + public static final String getProperty(String key, String def) { + try { + return System.getProperty(key, def); + } catch (AccessControlException _) { + return def; + } + } + /** * <p>Initializes a BDD factory with the given initial node table size *************** *** 42,46 **** */ public static BDDFactory init(int nodenum, int cachesize) { ! String bddpackage = System.getProperty("bdd", "buddy"); return init(bddpackage, nodenum, cachesize); } --- 51,55 ---- */ public static BDDFactory init(int nodenum, int cachesize) { ! String bddpackage = getProperty("bdd", "buddy"); return init(bddpackage, nodenum, cachesize); } *************** *** 1157,1161 **** public String toString() { StringBuffer sb = new StringBuffer(); ! String newLine = System.getProperty("line.separator"); sb.append(newLine); sb.append("Cache statistics"); --- 1166,1170 ---- public String toString() { StringBuffer sb = new StringBuffer(); ! String newLine = getProperty("line.separator", "\n"); sb.append(newLine); sb.append("Cache statistics"); Index: CUDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/CUDDFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** CUDDFactory.java 8 Apr 2005 05:27:52 -0000 1.5 --- CUDDFactory.java 29 Apr 2005 02:25:28 -0000 1.6 *************** *** 53,58 **** // Cannot find library, try loading it from the current directory... libname = System.mapLibraryName(libname); ! String currentdir = System.getProperty("user.dir"); ! String sep = System.getProperty("file.separator"); System.load(currentdir+sep+libname); } --- 53,58 ---- // Cannot find library, try loading it from the current directory... libname = System.mapLibraryName(libname); ! String currentdir = getProperty("user.dir", "."); ! String sep = getProperty("file.separator", "/"); System.load(currentdir+sep+libname); } |
|
From: John W. <joe...@us...> - 2005-04-19 08:51:09
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4600 Modified Files: NQueens.java Log Message: Print out cache stats if they are available. Index: NQueens.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/NQueens.java,v retrieving revision 1.16 retrieving revision 1.17 diff -C2 -d -r1.16 -r1.17 *** NQueens.java 19 Oct 2004 11:11:54 -0000 1.16 --- NQueens.java 19 Apr 2005 08:50:55 -0000 1.17 *************** *** 30,33 **** --- 30,37 ---- time = System.currentTimeMillis() - time; System.out.println("Time: "+time/1000.+" seconds"); + BDDFactory.CacheStats cachestats = B.getCacheStats(); + if (cachestats != null && cachestats.uniqueAccess > 0) { + System.out.println(cachestats); + } B.done(); B = null; |
|
From: John W. <joe...@us...> - 2005-04-19 08:49:29
|
Update of /cvsroot/javabdd/JavaBDD/.settings In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3365/.settings Modified Files: org.eclipse.jdt.ui.prefs org.eclipse.jdt.core.prefs Log Message: Update to latest eclipse version. Index: org.eclipse.jdt.core.prefs =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/.settings/org.eclipse.jdt.core.prefs,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** org.eclipse.jdt.core.prefs 4 Jan 2005 02:01:53 -0000 1.1 --- org.eclipse.jdt.core.prefs 19 Apr 2005 08:49:16 -0000 1.2 *************** *** 1,229 **** ! #Mon Jan 03 18:00:48 PST 2005 ! org.eclipse.jdt.core.formatter.brace_position_for_enum_constant=end_of_line ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_method_invocation=do not insert ! org.eclipse.jdt.core.formatter.format_guardian_clause_on_one_line=false ! org.eclipse.jdt.core.formatter.number_of_blank_lines_at_beginning_of_method_body=0 ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_synchronized=insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_switch=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_for_inits=insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_method_invocation=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_annotation_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_brace_in_array_initializer=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_before_catch_in_try_statement=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_bracket_in_array_allocation_expression=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_brackets_in_array_type_reference=do not insert ! org.eclipse.jdt.core.formatter.brace_position_for_switch=end_of_line ! org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_parameters=insert ! org.eclipse.jdt.core.formatter.insert_space_before_postfix_operator=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_enum_constant=insert ! org.eclipse.jdt.core.formatter.insert_new_line_at_end_of_file_if_missing=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_catch=insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_method_declaration=do not insert ! org.eclipse.jdt.core.formatter.brace_position_for_enum_declaration=end_of_line org.eclipse.jdt.core.formatter.alignment_for_arguments_in_allocation_expression=16 ! org.eclipse.jdt.core.formatter.continuation_indentation_for_array_initializer=1 ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_constructor_declaration_throws=insert ! org.eclipse.jdt.core.formatter.blank_lines_before_method=1 ! org.eclipse.jdt.core.formatter.insert_space_after_assignment_operator=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_anonymous_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_array_initializer=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_method_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_annotation_type_member_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_explicitconstructorcall_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_parameterized_type_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_annotation=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_enum_declarations=insert ! org.eclipse.jdt.core.formatter.number_of_empty_lines_to_preserve=0 ! org.eclipse.jdt.core.formatter.insert_new_line_before_while_in_do_statement=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_parameters=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_enum_constant=do not insert ! org.eclipse.jdt.core.formatter.alignment_for_selector_in_method_invocation=16 ! org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation_type_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_question_in_conditional=insert ! org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_constant=insert ! org.eclipse.jdt.core.formatter.tabulation.size=4 ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_catch=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_method_invocation=do not insert ! org.eclipse.jdt.core.formatter.indent_statements_compare_to_body=true ! org.eclipse.jdt.core.formatter.insert_space_before_colon_in_conditional=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_method_declaration=insert ! org.eclipse.jdt.core.formatter.keep_then_statement_on_same_line=true ! org.eclipse.jdt.core.formatter.tabulation.char=space ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_for=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_empty_brackets_in_array_allocation_expression=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_synchronized=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_array_initializer=insert ! org.eclipse.jdt.core.formatter.insert_space_after_colon_in_labeled_statement=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_constructor_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_if=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_bracket_in_array_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_for_increments=insert org.eclipse.jdt.core.formatter.alignment_for_parameters_in_method_declaration=16 ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_switch=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_enum_constant_arguments=do not insert org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_type_declaration=64 ! org.eclipse.jdt.core.formatter.insert_space_before_at_in_annotation_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_before_unary_operator=do not insert ! org.eclipse.jdt.core.formatter.brace_position_for_block_in_case=end_of_line ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_constructor_declaration_parameters=insert ! org.eclipse.jdt.core.formatter.brace_position_for_block=end_of_line ! org.eclipse.jdt.core.formatter.insert_space_before_opening_bracket_in_array_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_and_in_type_parameter=insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_multiple_field_declarations=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_assignment_operator=insert ! org.eclipse.jdt.core.formatter.insert_space_after_ellipsis=insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_parameters=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_superinterfaces=insert ! org.eclipse.jdt.core.formatter.insert_space_before_colon_in_default=insert org.eclipse.jdt.core.formatter.blank_lines_before_imports=0 - org.eclipse.jdt.core.formatter.insert_space_after_colon_in_conditional=insert - org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_for=do not insert - org.eclipse.jdt.core.formatter.indent_switchstatements_compare_to_cases=true - org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_arguments=do not insert - org.eclipse.jdt.core.formatter.insert_space_after_comma_in_allocation_expression=insert - org.eclipse.jdt.core.formatter.alignment_for_compact_if=52 - org.eclipse.jdt.core.formatter.insert_space_after_and_in_type_parameter=insert - org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_if=insert - org.eclipse.jdt.core.formatter.insert_space_between_empty_braces_in_array_initializer=do not insert org.eclipse.jdt.core.formatter.blank_lines_before_member_type=0 ! org.eclipse.jdt.core.formatter.insert_space_before_question_in_wildcard=insert ! org.eclipse.jdt.core.formatter.insert_space_before_colon_in_for=insert ! org.eclipse.jdt.core.formatter.insert_space_after_postfix_operator=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_method_invocation_arguments=insert ! org.eclipse.jdt.core.formatter.insert_space_before_ellipsis=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_multiple_local_declarations=do not insert org.eclipse.jdt.core.formatter.brace_position_for_array_initializer=end_of_line org.eclipse.jdt.core.formatter.indent_body_declarations_compare_to_enum_constant_header=true org.eclipse.jdt.core.formatter.indent_body_declarations_compare_to_type_header=true ! org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_parameters=do not insert ! org.eclipse.jdt.core.formatter.blank_lines_before_field=0 ! org.eclipse.jdt.core.formatter.insert_new_line_in_empty_type_declaration=insert org.eclipse.jdt.core.formatter.indent_statements_compare_to_block=true ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_method_declaration_parameters=do not insert org.eclipse.jdt.core.formatter.insert_space_after_colon_in_case=insert ! org.eclipse.jdt.core.formatter.keep_empty_array_initializer_on_one_line=false ! org.eclipse.jdt.core.formatter.insert_space_before_binary_operator=insert org.eclipse.jdt.core.formatter.insert_space_after_comma_in_annotation=insert ! org.eclipse.jdt.core.formatter.insert_space_after_closing_brace_in_block=insert ! org.eclipse.jdt.core.formatter.put_empty_statement_on_new_line=false ! org.eclipse.jdt.core.formatter.brace_position_for_method_declaration=end_of_line ! org.eclipse.jdt.core.formatter.insert_space_before_prefix_operator=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_superinterfaces=do not insert org.eclipse.jdt.core.formatter.insert_space_after_comma_in_enum_constant_arguments=insert org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_parenthesized_expression=do not insert ! org.eclipse.jdt.core.formatter.blank_lines_before_first_class_body_declaration=0 ! org.eclipse.jdt.core.formatter.lineSplit=80 ! org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_enum_constant=do not insert org.eclipse.jdt.core.formatter.insert_space_after_question_in_conditional=insert - org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_if=do not insert - org.eclipse.jdt.core.formatter.insert_space_after_comma_in_explicitconstructorcall_arguments=insert org.eclipse.jdt.core.formatter.insert_space_after_question_in_wildcard=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_enum_constant=do not insert ! org.eclipse.jdt.core.formatter.blank_lines_after_imports=1 ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_synchronized=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_before_else_in_if_statement=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_block=insert ! org.eclipse.jdt.core.formatter.alignment_for_throws_clause_in_method_declaration=16 org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_cast=do not insert ! org.eclipse.jdt.core.formatter.alignment_for_arguments_in_explicit_constructor_call=16 org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_method_invocation=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_comma_in_constructor_declaration_throws=do not insert - org.eclipse.jdt.core.formatter.alignment_for_arguments_in_qualified_allocation_expression=16 - org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_enum_declaration=insert - org.eclipse.jdt.core.formatter.insert_space_before_closing_brace_in_array_initializer=do not insert - org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_constructor_declaration=do not insert - org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_for=insert - org.eclipse.jdt.core.formatter.insert_space_before_opening_bracket_in_array_allocation_expression=do not insert - org.eclipse.jdt.core.formatter.blank_lines_before_package=0 - org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_arguments=insert - org.eclipse.jdt.core.formatter.brace_position_for_anonymous_type_declaration=end_of_line - org.eclipse.jdt.core.formatter.brace_position_for_type_declaration=end_of_line - org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_parameters=do not insert - org.eclipse.jdt.core.formatter.insert_space_after_closing_paren_in_cast=insert - org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_while=do not insert - org.eclipse.jdt.core.formatter.insert_new_line_in_empty_method_body=insert - org.eclipse.jdt.core.formatter.keep_else_statement_on_same_line=true - org.eclipse.jdt.core.formatter.align_type_members_on_columns=false - org.eclipse.jdt.core.formatter.insert_space_after_opening_bracket_in_array_allocation_expression=do not insert - org.eclipse.jdt.core.formatter.blank_lines_between_type_declarations=1 - org.eclipse.jdt.core.formatter.insert_new_line_after_opening_brace_in_array_initializer=do not insert - org.eclipse.jdt.core.formatter.insert_space_after_binary_operator=insert - org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_annotation_type_member_declaration=do not insert - org.eclipse.jdt.core.formatter.insert_new_line_before_closing_brace_in_array_initializer=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_comma_in_constructor_declaration_parameters=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_parameterized_type_reference=do not insert - org.eclipse.jdt.core.formatter.insert_space_after_prefix_operator=do not insert - org.eclipse.jdt.core.formatter.brace_position_for_constructor_declaration=end_of_line - org.eclipse.jdt.core.formatter.insert_space_before_comma_in_annotation=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_comma_in_parameterized_type_reference=do not insert org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_parenthesized_expression=do not insert ! org.eclipse.jdt.core.formatter.indent_switchstatements_compare_to_switch=true ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_cast=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_for=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_bracket_in_array_type_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_in_empty_block=insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_parameterized_type_reference=do not insert ! eclipse.preferences.version=1 ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_method_invocation_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_allocation_expression=do not insert ! org.eclipse.jdt.core.formatter.alignment_for_superclass_in_type_declaration=64 org.eclipse.jdt.core.formatter.insert_space_before_colon_in_assert=insert - org.eclipse.jdt.core.formatter.insert_new_line_in_empty_anonymous_type_declaration=insert - org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_enum_declaration=16 - org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_method_declaration=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_comma_in_enum_declarations=do not insert - org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation=do not insert - org.eclipse.jdt.core.formatter.blank_lines_before_new_chunk=0 - org.eclipse.jdt.core.formatter.alignment_for_conditional_expression=48 - org.eclipse.jdt.core.formatter.brace_position_for_annotation_type_declaration=end_of_line - org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_annotation=do not insert - org.eclipse.jdt.core.formatter.alignment_for_multiple_fields=16 - org.eclipse.jdt.core.formatter.insert_space_before_closing_bracket_in_array_reference=do not insert - org.eclipse.jdt.core.formatter.alignment_for_arguments_in_method_invocation=16 - org.eclipse.jdt.core.formatter.insert_space_before_comma_in_for_inits=do not insert - org.eclipse.jdt.core.formatter.alignment_for_expressions_in_array_initializer=16 - org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_arguments=insert - org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_constructor_declaration=do not insert - org.eclipse.jdt.core.formatter.keep_imple_if_on_one_line=false - org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_while=insert - org.eclipse.jdt.core.formatter.alignment_for_arguments_in_enum_constant=16 - org.eclipse.jdt.core.formatter.insert_space_after_comma_in_parameterized_type_reference=insert - org.eclipse.jdt.core.formatter.blank_lines_after_package=1 - org.eclipse.jdt.core.formatter.insert_space_after_comma_in_method_declaration_parameters=insert - org.eclipse.jdt.core.formatter.insert_space_after_comma_in_method_declaration_throws=insert org.eclipse.jdt.core.formatter.insert_space_before_colon_in_case=insert org.eclipse.jdt.core.formatter.insert_space_before_colon_in_labeled_statement=insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_multiple_field_declarations=insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_parameters=insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_enum_constant=do not insert org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_switch=insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_catch=do not insert org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_parenthesized_expression=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_semicolon=do not insert - org.eclipse.jdt.core.formatter.alignment_for_parameters_in_constructor_declaration=16 - org.eclipse.jdt.core.formatter.alignment_for_binary_expression=16 - org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_declaration=insert - org.eclipse.jdt.core.formatter.alignment_for_throws_clause_in_constructor_declaration=16 - org.eclipse.jdt.core.formatter.insert_new_line_before_finally_in_try_statement=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_constructor_declaration=insert - org.eclipse.jdt.core.formatter.compact_else_if=true - org.eclipse.jdt.core.formatter.indent_breaks_compare_to_cases=true - org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_for=do not insert - org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_while=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_comma_in_method_declaration_throws=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_comma_in_for_increments=do not insert - org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_method_declaration=do not insert - org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_constructor_declaration=do not insert org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_switch=insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_array_initializer=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_colon_in_for=insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_annotation=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_unary_operator=do not insert ! org.eclipse.jdt.core.formatter.continuation_indentation=1 ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_multiple_local_declarations=insert ! org.eclipse.jdt.core.formatter.indent_body_declarations_compare_to_enum_declaration_header=true ! org.eclipse.jdt.core.formatter.insert_space_after_colon_in_assert=insert --- 1,241 ---- ! #Wed Apr 06 09:10:10 PDT 2005 ! eclipse.preferences.version=1 ! org.eclipse.jdt.core.formatter.align_type_members_on_columns=false org.eclipse.jdt.core.formatter.alignment_for_arguments_in_allocation_expression=16 ! org.eclipse.jdt.core.formatter.alignment_for_arguments_in_enum_constant=16 ! org.eclipse.jdt.core.formatter.alignment_for_arguments_in_explicit_constructor_call=16 ! org.eclipse.jdt.core.formatter.alignment_for_arguments_in_method_invocation=16 ! org.eclipse.jdt.core.formatter.alignment_for_arguments_in_qualified_allocation_expression=16 ! org.eclipse.jdt.core.formatter.alignment_for_binary_expression=16 ! org.eclipse.jdt.core.formatter.alignment_for_compact_if=52 ! org.eclipse.jdt.core.formatter.alignment_for_conditional_expression=48 ! org.eclipse.jdt.core.formatter.alignment_for_expressions_in_array_initializer=16 ! org.eclipse.jdt.core.formatter.alignment_for_multiple_fields=16 ! org.eclipse.jdt.core.formatter.alignment_for_parameters_in_constructor_declaration=16 org.eclipse.jdt.core.formatter.alignment_for_parameters_in_method_declaration=16 ! org.eclipse.jdt.core.formatter.alignment_for_selector_in_method_invocation=16 ! org.eclipse.jdt.core.formatter.alignment_for_superclass_in_type_declaration=64 ! org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_enum_declaration=16 org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_type_declaration=64 ! org.eclipse.jdt.core.formatter.alignment_for_throws_clause_in_constructor_declaration=16 ! org.eclipse.jdt.core.formatter.alignment_for_throws_clause_in_method_declaration=16 ! org.eclipse.jdt.core.formatter.blank_lines_after_imports=1 ! org.eclipse.jdt.core.formatter.blank_lines_after_package=1 ! org.eclipse.jdt.core.formatter.blank_lines_before_field=0 ! org.eclipse.jdt.core.formatter.blank_lines_before_first_class_body_declaration=0 org.eclipse.jdt.core.formatter.blank_lines_before_imports=0 org.eclipse.jdt.core.formatter.blank_lines_before_member_type=0 ! org.eclipse.jdt.core.formatter.blank_lines_before_method=1 ! org.eclipse.jdt.core.formatter.blank_lines_before_new_chunk=0 ! org.eclipse.jdt.core.formatter.blank_lines_before_package=0 ! org.eclipse.jdt.core.formatter.blank_lines_between_type_declarations=1 ! org.eclipse.jdt.core.formatter.brace_position_for_annotation_type_declaration=end_of_line ! org.eclipse.jdt.core.formatter.brace_position_for_anonymous_type_declaration=end_of_line org.eclipse.jdt.core.formatter.brace_position_for_array_initializer=end_of_line + org.eclipse.jdt.core.formatter.brace_position_for_block=end_of_line + org.eclipse.jdt.core.formatter.brace_position_for_block_in_case=end_of_line + org.eclipse.jdt.core.formatter.brace_position_for_constructor_declaration=end_of_line + org.eclipse.jdt.core.formatter.brace_position_for_enum_constant=end_of_line + org.eclipse.jdt.core.formatter.brace_position_for_enum_declaration=end_of_line + org.eclipse.jdt.core.formatter.brace_position_for_method_declaration=end_of_line + org.eclipse.jdt.core.formatter.brace_position_for_switch=end_of_line + org.eclipse.jdt.core.formatter.brace_position_for_type_declaration=end_of_line + org.eclipse.jdt.core.formatter.comment.clear_blank_lines=false + org.eclipse.jdt.core.formatter.comment.format_comments=true + org.eclipse.jdt.core.formatter.comment.format_header=true + org.eclipse.jdt.core.formatter.comment.format_html=true + org.eclipse.jdt.core.formatter.comment.format_source_code=true + org.eclipse.jdt.core.formatter.comment.indent_parameter_description=true + org.eclipse.jdt.core.formatter.comment.indent_root_tags=true + org.eclipse.jdt.core.formatter.comment.insert_new_line_before_root_tags=insert + org.eclipse.jdt.core.formatter.comment.insert_new_line_for_parameter=insert + org.eclipse.jdt.core.formatter.comment.line_length=80 + org.eclipse.jdt.core.formatter.compact_else_if=true + org.eclipse.jdt.core.formatter.continuation_indentation=1 + org.eclipse.jdt.core.formatter.continuation_indentation_for_array_initializer=1 + org.eclipse.jdt.core.formatter.format_guardian_clause_on_one_line=false org.eclipse.jdt.core.formatter.indent_body_declarations_compare_to_enum_constant_header=true + org.eclipse.jdt.core.formatter.indent_body_declarations_compare_to_enum_declaration_header=true org.eclipse.jdt.core.formatter.indent_body_declarations_compare_to_type_header=true ! org.eclipse.jdt.core.formatter.indent_breaks_compare_to_cases=true org.eclipse.jdt.core.formatter.indent_statements_compare_to_block=true ! org.eclipse.jdt.core.formatter.indent_statements_compare_to_body=true ! org.eclipse.jdt.core.formatter.indent_switchstatements_compare_to_cases=true ! org.eclipse.jdt.core.formatter.indent_switchstatements_compare_to_switch=true ! org.eclipse.jdt.core.formatter.indentation.size=4 ! org.eclipse.jdt.core.formatter.insert_new_line_after_annotation=insert ! org.eclipse.jdt.core.formatter.insert_new_line_after_opening_brace_in_array_initializer=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_at_end_of_file_if_missing=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_before_catch_in_try_statement=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_before_closing_brace_in_array_initializer=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_before_else_in_if_statement=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_before_finally_in_try_statement=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_before_while_in_do_statement=do not insert ! org.eclipse.jdt.core.formatter.insert_new_line_in_empty_anonymous_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_new_line_in_empty_block=insert ! org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_constant=insert ! org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_declaration=insert ! org.eclipse.jdt.core.formatter.insert_new_line_in_empty_method_body=insert ! org.eclipse.jdt.core.formatter.insert_new_line_in_empty_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_after_and_in_type_parameter=insert ! org.eclipse.jdt.core.formatter.insert_space_after_assignment_operator=insert ! org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation_type_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_binary_operator=insert ! org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_arguments=insert ! org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_parameters=insert ! org.eclipse.jdt.core.formatter.insert_space_after_closing_brace_in_block=insert ! org.eclipse.jdt.core.formatter.insert_space_after_closing_paren_in_cast=insert ! org.eclipse.jdt.core.formatter.insert_space_after_colon_in_assert=insert org.eclipse.jdt.core.formatter.insert_space_after_colon_in_case=insert ! org.eclipse.jdt.core.formatter.insert_space_after_colon_in_conditional=insert ! org.eclipse.jdt.core.formatter.insert_space_after_colon_in_for=insert ! org.eclipse.jdt.core.formatter.insert_space_after_colon_in_labeled_statement=insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_allocation_expression=insert org.eclipse.jdt.core.formatter.insert_space_after_comma_in_annotation=insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_array_initializer=insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_constructor_declaration_parameters=insert ! org.eclipse.jdt.core.formatter.insert_space_after_comma_in_constructor_declaration_throws=insert org.eclipse.jdt.core.formatter.insert_space_after_comma_in_enum_constant_arguments=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_enum_declarations=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_explicitconstructorcall_arguments=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_for_increments=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_for_inits=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_method_declaration_parameters=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_method_declaration_throws=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_method_invocation_arguments=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_multiple_field_declarations=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_multiple_local_declarations=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_parameterized_type_reference=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_superinterfaces=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_arguments=insert + org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_parameters=insert + org.eclipse.jdt.core.formatter.insert_space_after_ellipsis=insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_parameterized_type_reference=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_arguments=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_parameters=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_brace_in_array_initializer=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_bracket_in_array_allocation_expression=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_bracket_in_array_reference=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_annotation=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_cast=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_catch=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_constructor_declaration=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_enum_constant=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_for=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_if=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_method_declaration=do not insert + org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_method_invocation=do not insert org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_parenthesized_expression=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_switch=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_synchronized=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_opening_paren_in_while=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_postfix_operator=do not insert ! org.eclipse.jdt.core.formatter.insert_space_after_prefix_operator=do not insert org.eclipse.jdt.core.formatter.insert_space_after_question_in_conditional=insert org.eclipse.jdt.core.formatter.insert_space_after_question_in_wildcard=insert ! org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_for=insert ! org.eclipse.jdt.core.formatter.insert_space_after_unary_operator=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_and_in_type_parameter=insert ! org.eclipse.jdt.core.formatter.insert_space_before_assignment_operator=insert ! org.eclipse.jdt.core.formatter.insert_space_before_at_in_annotation_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_before_binary_operator=insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_parameterized_type_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_parameters=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_brace_in_array_initializer=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_bracket_in_array_allocation_expression=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_bracket_in_array_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_annotation=do not insert org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_cast=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_catch=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_constructor_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_enum_constant=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_for=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_if=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_method_declaration=do not insert org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_method_invocation=do not insert org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_parenthesized_expression=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_switch=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_synchronized=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_closing_paren_in_while=do not insert org.eclipse.jdt.core.formatter.insert_space_before_colon_in_assert=insert org.eclipse.jdt.core.formatter.insert_space_before_colon_in_case=insert + org.eclipse.jdt.core.formatter.insert_space_before_colon_in_conditional=insert + org.eclipse.jdt.core.formatter.insert_space_before_colon_in_default=insert + org.eclipse.jdt.core.formatter.insert_space_before_colon_in_for=insert org.eclipse.jdt.core.formatter.insert_space_before_colon_in_labeled_statement=insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_allocation_expression=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_annotation=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_array_initializer=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_constructor_declaration_parameters=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_constructor_declaration_throws=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_enum_constant_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_enum_declarations=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_explicitconstructorcall_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_for_increments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_for_inits=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_method_declaration_parameters=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_method_declaration_throws=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_method_invocation_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_multiple_field_declarations=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_multiple_local_declarations=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_parameterized_type_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_superinterfaces=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_parameters=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_ellipsis=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_parameterized_type_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_arguments=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_parameters=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_annotation_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_anonymous_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_array_initializer=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_block=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_constructor_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_enum_constant=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_enum_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_method_declaration=insert org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_switch=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_brace_in_type_declaration=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_bracket_in_array_allocation_expression=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_bracket_in_array_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_bracket_in_array_type_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_annotation=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_annotation_type_member_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_catch=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_constructor_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_enum_constant=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_for=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_if=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_method_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_method_invocation=do not insert org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_parenthesized_expression=do not insert org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_switch=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_synchronized=insert ! org.eclipse.jdt.core.formatter.insert_space_before_opening_paren_in_while=insert ! org.eclipse.jdt.core.formatter.insert_space_before_postfix_operator=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_prefix_operator=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_question_in_conditional=insert ! org.eclipse.jdt.core.formatter.insert_space_before_question_in_wildcard=insert ! org.eclipse.jdt.core.formatter.insert_space_before_semicolon=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_for=do not insert ! org.eclipse.jdt.core.formatter.insert_space_before_unary_operator=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_brackets_in_array_type_reference=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_empty_braces_in_array_initializer=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_empty_brackets_in_array_allocation_expression=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_annotation_type_member_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_constructor_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_enum_constant=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_method_declaration=do not insert ! org.eclipse.jdt.core.formatter.insert_space_between_empty_parens_in_method_invocation=do not insert ! org.eclipse.jdt.core.formatter.keep_else_statement_on_same_line=true ! org.eclipse.jdt.core.formatter.keep_empty_array_initializer_on_one_line=false ! org.eclipse.jdt.core.formatter.keep_imple_if_on_one_line=false ! org.eclipse.jdt.core.formatter.keep_then_statement_on_same_line=true ! org.eclipse.jdt.core.formatter.lineSplit=80 ! org.eclipse.jdt.core.formatter.number_of_blank_lines_at_beginning_of_method_body=0 ! org.eclipse.jdt.core.formatter.number_of_empty_lines_to_preserve=0 ! org.eclipse.jdt.core.formatter.put_empty_statement_on_new_line=false ! org.eclipse.jdt.core.formatter.tabulation.char=space ! org.eclipse.jdt.core.formatter.tabulation.size=4 Index: org.eclipse.jdt.ui.prefs =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/.settings/org.eclipse.jdt.ui.prefs,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** org.eclipse.jdt.ui.prefs 4 Jan 2005 02:01:53 -0000 1.1 --- org.eclipse.jdt.ui.prefs 19 Apr 2005 08:49:16 -0000 1.2 *************** *** 1,12 **** ! #Mon Jan 03 18:00:48 PST 2005 ! comment_format_source_code=true ! comment_new_line_for_parameter=true ! comment_format_html=true ! comment_line_length=80 comment_format_header=true ! eclipse.preferences.version=1 comment_indent_parameter_description=true - comment_format_comments=true - comment_separate_root_tags=true - comment_clear_blank_lines=false comment_indent_root_tags=true --- 1,13 ---- ! #Wed Apr 06 09:10:13 PDT 2005 ! comment_clear_blank_lines=false ! comment_format_comments=true comment_format_header=true ! comment_format_html=true ! comment_format_source_code=true comment_indent_parameter_description=true comment_indent_root_tags=true + comment_line_length=80 + comment_new_line_for_parameter=true + comment_separate_root_tags=true + eclipse.preferences.version=1 + formatter_settings_version=8 |
|
From: John W. <joe...@us...> - 2005-04-18 23:10:30
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv26353/buddy/src Modified Files: kernel.h Log Message: Changed default max node increment. Index: kernel.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.h,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** kernel.h 17 Apr 2005 10:21:27 -0000 1.5 --- kernel.h 18 Apr 2005 23:10:21 -0000 1.6 *************** *** 370,374 **** #endif ! #define DEFAULTMAXNODEINC 50000 #define MIN(a,b) ((a) < (b) ? (a) : (b)) --- 370,374 ---- #endif ! #define DEFAULTMAXNODEINC 10000000 #define MIN(a,b) ((a) < (b) ? (a) : (b)) |
|
From: John W. <joe...@us...> - 2005-04-18 12:00:53
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32123/bdd Modified Files: CallbackTests.java Log Message: More bits by default. Index: CallbackTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/CallbackTests.java,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** CallbackTests.java 29 Jan 2005 11:32:25 -0000 1.1 --- CallbackTests.java 18 Apr 2005 12:00:41 -0000 1.2 *************** *** 48,52 **** bdd.registerGCCallback(this, m); gc_called = 0; ! final int numBits = 16; final int max = (1 << numBits) - 1; if (bdd.varNum() < numBits) bdd.setVarNum(numBits); --- 48,52 ---- bdd.registerGCCallback(this, m); gc_called = 0; ! final int numBits = 20; final int max = (1 << numBits) - 1; if (bdd.varNum() < numBits) bdd.setVarNum(numBits); |
|
From: John W. <joe...@us...> - 2005-04-18 12:00:10
|
Update of /cvsroot/javabdd/JavaBDD_tests/regression In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31824/regression Modified Files: R3.java Log Message: rename method. Index: R3.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/regression/R3.java,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** R3.java 29 Jan 2005 01:02:46 -0000 1.1 --- R3.java 18 Apr 2005 12:00:00 -0000 1.2 *************** *** 20,24 **** } ! public void testR2() { Assert.assertTrue(hasNext()); while (hasNext()) { --- 20,24 ---- } ! public void testR3() { Assert.assertTrue(hasNext()); while (hasNext()) { |
|
From: John W. <joe...@us...> - 2005-04-17 10:22:35
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv21364/bdd Modified Files: BasicTests.java Log Message: New test case for ensureCapacity Index: BasicTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/BasicTests.java,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** BasicTests.java 31 Jan 2005 00:08:33 -0000 1.3 --- BasicTests.java 17 Apr 2005 10:22:23 -0000 1.4 *************** *** 4,9 **** --- 4,20 ---- package bdd; + import java.util.ArrayList; + import java.util.Arrays; + import java.util.Iterator; + import java.util.LinkedList; + import java.util.List; + import java.util.Random; + import java.io.BufferedWriter; + import java.io.IOException; + import java.io.PrintWriter; + import java.math.BigInteger; import junit.framework.Assert; import net.sf.javabdd.BDD; + import net.sf.javabdd.BDDDomain; import net.sf.javabdd.BDDException; import net.sf.javabdd.BDDFactory; *************** *** 386,388 **** --- 397,539 ---- } } + + public void testEnsureCapacity() { + reset(); + Assert.assertTrue(hasNext()); + while (hasNext()) { + BDDFactory bdd = nextFactory(); + long[] domains = new long[] { 127, 17, 31, 4 }; + BDDDomain[] d = bdd.extDomain(domains); + BDD q = d[0].ithVar(7); + BDD r = d[1].ithVar(9); + BDD s = d[2].ithVar(4); + BDD t = d[3].ithVar(2); + BDD u = r.and(s); + BDD v = q.and(t); + BDD w = u.and(t); + //BDD x = d[1].set(); + for (int i = 0; i < d.length; ++i) { + d[i].ensureCapacity(BigInteger.valueOf(150)); + Assert.assertEquals(BigInteger.valueOf(7), q.scanVar(d[0])); + Assert.assertEquals(BigInteger.valueOf(9), r.scanVar(d[1])); + Assert.assertEquals(BigInteger.valueOf(4), s.scanVar(d[2])); + Assert.assertEquals(BigInteger.valueOf(2), t.scanVar(d[3])); + Assert.assertEquals(BigInteger.valueOf(9), u.scanVar(d[1])); + Assert.assertEquals(BigInteger.valueOf(4), u.scanVar(d[2])); + Assert.assertEquals(BigInteger.valueOf(7), v.scanVar(d[0])); + Assert.assertEquals(BigInteger.valueOf(2), v.scanVar(d[3])); + Assert.assertEquals(BigInteger.valueOf(9), w.scanVar(d[1])); + Assert.assertEquals(BigInteger.valueOf(4), w.scanVar(d[2])); + Assert.assertEquals(BigInteger.valueOf(2), w.scanVar(d[3])); + //BDD y = d[1].set(); + //Assert.assertEquals(x, y); + //y.free(); + } + //x.free(); + w.free(); v.free(); u.free(); t.free(); s.free(); r.free(); q.free(); + } + } + + public void testEnsureCapacity2() throws IOException { + reset(); + Assert.assertTrue(hasNext()); + while (hasNext()) { + BDDFactory bdd = nextFactory(); + System.out.println("Factory "+bdd); + int n = bdd.numberOfDomains(); + long[] domainSizes = new long[] { 127, 17, 31, 4, 256, 87, 42, 666, 3405, 18 }; + while (bdd.numberOfDomains() < domainSizes.length) { + bdd.extDomain(domainSizes[bdd.numberOfDomains()]); + } + BDDDomain[] d = new BDDDomain[domainSizes.length]; + for (int i = 0; i < domainSizes.length; ++i) { + d[i] = bdd.getDomain(i); + domainSizes[i] = d[i].size().longValue(); + } + for (int i = 0; i < d.length; ++i) { + d[i].setName(Integer.toString(i)); + } + final int count = 100; + final int num = 10; + for (int i = 0; i < count; ++i) { + String order = randomOrder(d); + //System.out.println("Random order: "+order); + bdd.setVarOrder(bdd.makeVarOrdering(false, order)); + List bdds = new LinkedList(); + for (int j = 0; j < num; ++j) { + BDD b = randomBDD(bdd); + bdds.add(b); + } + StringBuffer sb = new StringBuffer(); + for (Iterator j = bdds.iterator(); j.hasNext(); ) { + BDD b = (BDD) j.next(); + sb.append(b.toStringWithDomains()); + //bdd.save(new BufferedWriter(new PrintWriter(System.out)), b); + } + String before = sb.toString(); + int which = random.nextInt(d.length); + int amount = random.nextInt(d[which].size().intValue() * 3); + //System.out.println(" Ensure capacity "+d[which]+" = "+amount); + d[which].ensureCapacity(amount); + sb = new StringBuffer(); + for (Iterator j = bdds.iterator(); j.hasNext(); ) { + BDD b = (BDD) j.next(); + sb.append(b.toStringWithDomains()); + //bdd.save(new BufferedWriter(new PrintWriter(System.out)), b); + } + String after = sb.toString(); + Assert.assertEquals(before, after); + for (Iterator j = bdds.iterator(); j.hasNext(); ) { + BDD b = (BDD) j.next(); + b.free(); + } + } + } + } + + private static BDD randomBDD(BDDFactory f) { + Assert.assertTrue(f.numberOfDomains() > 0); + List list = new ArrayList(f.numberOfDomains()); + int k = random.nextInt(f.numberOfDomains()); + for (int i = 0; i < f.numberOfDomains(); ++i) { + list.add(f.getDomain(i)); + } + BDD result = f.one(); + for (int i = 0; i < k; ++i) { + int x = random.nextInt(f.numberOfDomains()-i); + BDDDomain d = (BDDDomain) list.remove(x); + int y = random.nextInt(d.size().intValue()); + result.andWith(d.ithVar(y)); + } + if (k == 0 && random.nextBoolean()) + result.andWith(f.zero()); + return result; + } + + private static String randomOrder(BDDDomain[] domains) { + domains = (BDDDomain[]) randomShuffle(domains); + StringBuffer sb = new StringBuffer(); + for (int i = 0; i < domains.length; ++i) { + if (i > 0) { + boolean x = random.nextBoolean(); + if (x) sb.append('x'); + else sb.append('_'); + } + sb.append(domains[i].toString()); + } + return sb.toString(); + } + + private static Random random = new Random(System.currentTimeMillis()); + private static Object[] randomShuffle(Object[] a) { + int n = a.length; + List list = new ArrayList(Arrays.asList(a)); + Object[] result = (Object[]) a.clone(); + for (int i = 0; i < n; ++i) { + int k = random.nextInt(n-i); + result[i] = list.remove(k); + } + Assert.assertTrue(list.isEmpty()); + return result; + } } |
|
From: John W. <joe...@us...> - 2005-04-17 10:22:00
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20956/net/sf/javabdd Modified Files: JFactory.java BDDDomain.java MicroFactory.java BDDFactory.java Log Message: Updates to duplicateVar. Seems to actually work now. Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.8 retrieving revision 1.9 diff -C2 -d -r1.8 -r1.9 *** BDDFactory.java 14 Apr 2005 23:58:41 -0000 1.8 --- BDDFactory.java 17 Apr 2005 10:21:47 -0000 1.9 *************** *** 268,271 **** --- 268,274 ---- int nodes = getNodeTableSize(); int cache = getCacheSize(); + domain = null; + fdvarnum = 0; + firstbddvar = 0; done(); initialize(nodes, cache); Index: BDDDomain.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDDomain.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** BDDDomain.java 14 Apr 2005 23:58:41 -0000 1.6 --- BDDDomain.java 17 Apr 2005 10:21:46 -0000 1.7 *************** *** 320,328 **** --- 320,331 ---- BDDFactory factory = getFactory(); for (int i = ivar.length; i < new_ivar.length; ++i) { + //System.out.println("Domain "+this+" Duplicating var#"+new_ivar[i-1]); int newVar = factory.duplicateVar(new_ivar[i-1]); factory.firstbddvar++; new_ivar[i] = newVar; + //System.out.println("Domain "+this+" var#"+i+" = "+newVar); } this.ivar = new_ivar; + //System.out.println("Domain "+this+" old var = "+var); this.var.free(); BDD nvar = factory.one(); *************** *** 331,334 **** --- 334,338 ---- } this.var = nvar; + //System.out.println("Domain "+this+" new var = "+var); return binsize; } Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.19 retrieving revision 1.20 diff -C2 -d -r1.19 -r1.20 *** JFactory.java 14 Apr 2005 23:58:41 -0000 1.19 --- JFactory.java 17 Apr 2005 10:21:46 -0000 1.20 *************** *** 4470,4473 **** --- 4470,4475 ---- bddrefstack = null; bddvarset = null; + bddvar2level = null; + bddlevel2var = null; bdd_operator_done(); *************** *** 4610,4614 **** bdd_setvarnum(bddvarnum+1); // Actually duplicate the var in all BDDs. ! insert_level(lev, true, 0); // Fix up bddvar2level for (int i = 0; i < bddvarnum; ++i) { --- 4612,4617 ---- bdd_setvarnum(bddvarnum+1); // Actually duplicate the var in all BDDs. ! insert_level(lev); ! dup_level(lev, 0); // Fix up bddvar2level for (int i = 0; i < bddvarnum; ++i) { *************** *** 4629,4633 **** SETMAXREF(bddvarset[bdv * 2]); ! SETMAXREF(bddvarset[bdv * 2] + 1); } // Fix up pairs --- 4632,4636 ---- SETMAXREF(bddvarset[bdv * 2]); ! SETMAXREF(bddvarset[bdv * 2 + 1]); } // Fix up pairs *************** *** 4707,4711 **** SETMAXREF(bddvarset[bddvarnum * 2]); ! SETMAXREF(bddvarset[bddvarnum * 2] + 1); bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; --- 4710,4714 ---- SETMAXREF(bddvarset[bddvarnum * 2]); ! SETMAXREF(bddvarset[bddvarnum * 2 + 1]); bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; *************** *** 5465,5496 **** } ! void insert_level(int levToInsert, boolean dupLevel, int val) { for (int n = 2; n < bddnodesize; n++) { if (LOW(n) == INVALID_BDD) continue; int lev = LEVEL(n); ! if (lev < levToInsert || lev == bddvarnum-1) { // Stays the same. continue; } int lo, hi, newLev; ! if (dupLevel && lev == levToInsert) { ! // Duplicate this node. ! int n_low, n_high; ! bdd_addref(n); ! // 0 = var is zero, 1 = var is one, -1 = var equals other ! n_low = bdd_makenode(levToInsert+1, val<=0 ? LOW(n) : 0, val<=0 ? 0 : LOW(n)); ! n_high = bdd_makenode(levToInsert+1, val==0 ? HIGH(n) : 0, val==0 ? 0 : HIGH(n)); ! bdd_delref(n); ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev; ! SETLOW(n, n_low); ! SETHIGH(n, n_high); } else { ! // Need to increase level by one. ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev+1; } // Find this node in its hash chain. --- 5468,5538 ---- } ! void insert_level(int levToInsert) { for (int n = 2; n < bddnodesize; n++) { if (LOW(n) == INVALID_BDD) continue; int lev = LEVEL(n); ! if (lev <= levToInsert || lev == bddvarnum-1) { // Stays the same. continue; } int lo, hi, newLev; ! lo = LOW(n); ! hi = HIGH(n); ! // Need to increase level by one. ! newLev = lev+1; ! ! // Find this node in its hash chain. ! int hash = NODEHASH(lev, lo, hi); ! int r = HASH(hash), r2 = 0; ! while (r != n && r != 0) { ! r2 = r; ! r = NEXT(r); ! } ! if (r == 0) { ! // Cannot find node in the hash chain ?! ! throw new InternalError(); ! } ! // Remove from this hash chain. ! int NEXT_r = NEXT(r); ! if (r2 == 0) { ! SETHASH(hash, NEXT_r); } else { ! SETNEXT(r2, NEXT_r); ! } ! // Set level of this node. ! SETLEVEL(n, newLev); ! lo = LOW(n); hi = HIGH(n); ! // Add to new hash chain. ! hash = NODEHASH(newLev, lo, hi); ! r = HASH(hash); ! SETHASH(hash, n); ! SETNEXT(n, r); ! } ! } ! ! void dup_level(int levToInsert, int val) { ! for (int n = 2; n < bddnodesize; n++) { ! if (LOW(n) == INVALID_BDD) continue; ! int lev = LEVEL(n); ! if (lev != levToInsert || lev == bddvarnum-1) { ! // Stays the same. ! continue; } + int lo, hi, newLev; + lo = LOW(n); + hi = HIGH(n); + // Duplicate this node. + _assert(LEVEL(lo) > levToInsert + 1); + _assert(LEVEL(hi) > levToInsert + 1); + int n_low, n_high; + bdd_addref(n); + // 0 = var is zero, 1 = var is one, -1 = var equals other + n_low = bdd_makenode(levToInsert+1, val<=0 ? lo : 0, val<=0 ? 0 : lo); + n_high = bdd_makenode(levToInsert+1, val==0 ? hi : 0, val==0 ? 0 : hi); + bdd_delref(n); + //System.out.println("Lev = "+lev+" old low = "+lo+" old high = "+hi+" new low = "+n_low+" ("+new bdd(n_low)+") new high = "+n_high+" ("+new bdd(n_high)+")"); + newLev = lev; + SETLOW(n, n_low); + SETHIGH(n, n_high); // Find this node in its hash chain. *************** *** 5522,5526 **** } } ! int mark_roots() { boolean[] dep = new boolean[bddvarnum]; --- 5564,5568 ---- } } ! int mark_roots() { boolean[] dep = new boolean[bddvarnum]; *************** *** 6016,6019 **** --- 6058,6062 ---- bdd_unmark(r); + out.flush(); return; } Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.8 retrieving revision 1.9 diff -C2 -d -r1.8 -r1.9 *** MicroFactory.java 8 Apr 2005 05:27:52 -0000 1.8 --- MicroFactory.java 17 Apr 2005 10:21:46 -0000 1.9 *************** *** 4955,4969 **** int newVar = bddvarnum; int lev = bddvar2level[var]; bdd_setvarnum(bddvarnum+1); ! insert_level(lev, true, 0); ! for (int i = 0; i < bddvar2level.length; ++i) { if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) ++bddvar2level[i]; } bddvar2level[newVar] = lev+1; for (int i = bddvarnum-2; i > lev; --i) { bddlevel2var[i+1] = bddlevel2var[i]; } bddlevel2var[lev+1] = newVar; bdd_enable_reorder(); --- 4955,4995 ---- int newVar = bddvarnum; int lev = bddvar2level[var]; + // Increase the size of the various data structures. bdd_setvarnum(bddvarnum+1); ! // Actually duplicate the var in all BDDs. ! insert_level(lev); ! dup_level(lev, 0); ! // Fix up bddvar2level ! for (int i = 0; i < bddvarnum; ++i) { if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) ++bddvar2level[i]; } bddvar2level[newVar] = lev+1; + // Fix up bddlevel2var for (int i = bddvarnum-2; i > lev; --i) { bddlevel2var[i+1] = bddlevel2var[i]; } bddlevel2var[lev+1] = newVar; + // Fix up bddvarset + for (int bdv = 0; bdv < bddvarnum; bdv++) { + bddvarset[bdv * 2] = PUSHREF(bdd_makenode(bddvar2level[bdv], 0, 1)); + bddvarset[bdv * 2 + 1] = bdd_makenode(bddvar2level[bdv], 1, 0); + POPREF(1); + + SETMAXREF(bddvarset[bdv * 2]); + SETMAXREF(bddvarset[bdv * 2 + 1]); + } + // Fix up pairs + for (bddPair pair = pairs; pair != null; pair = pair.next) { + bdd_delref(pair.result[bddvarnum-1]); + for (int i = bddvarnum-1; i > lev+1; --i) { + pair.result[i] = pair.result[i-1]; + if (i != LEVEL(pair.result[i]) && i > pair.last) { + pair.last = i; + } + } + pair.result[lev+1] = bdd_ithvar(newVar); + //System.out.println("Pair "+pair); + } bdd_enable_reorder(); *************** *** 5028,5032 **** SETMAXREF(bddvarset[bddvarnum * 2]); ! SETMAXREF(bddvarset[bddvarnum * 2] + 1); bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; --- 5054,5058 ---- SETMAXREF(bddvarset[bddvarnum * 2]); ! SETMAXREF(bddvarset[bddvarnum * 2 + 1]); bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; *************** *** 5779,5810 **** } ! void insert_level(int levToInsert, boolean dupLevel, int val) { for (int n = 2; n < bddnodesize; n++) { if (LOW(n) == INVALID_BDD) continue; int lev = LEVEL(n); ! if (lev < levToInsert || lev == bddvarnum-1) { // Stays the same. continue; } int lo, hi, newLev; ! if (dupLevel && lev == levToInsert) { ! // Duplicate this node. ! int n_low, n_high; ! bdd_addref(n); ! // 0 = var is zero, 1 = var is one, -1 = var equals other ! n_low = bdd_makenode(levToInsert+1, val<=0 ? LOW(n) : 0, val<=0 ? 0 : LOW(n)); ! n_high = bdd_makenode(levToInsert+1, val==0 ? HIGH(n) : 0, val==0 ? 0 : HIGH(n)); ! bdd_delref(n); ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev; ! SETLOW(n, n_low); ! SETHIGH(n, n_high); } else { ! // Need to increase level by one. ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev+1; } // Find this node in its hash chain. --- 5805,5874 ---- } ! void insert_level(int levToInsert) { for (int n = 2; n < bddnodesize; n++) { if (LOW(n) == INVALID_BDD) continue; int lev = LEVEL(n); ! if (lev <= levToInsert || lev == bddvarnum-1) { // Stays the same. continue; } int lo, hi, newLev; ! lo = LOW(n); ! hi = HIGH(n); ! // Need to increase level by one. ! newLev = lev+1; ! ! // Find this node in its hash chain. ! int hash = NODEHASH(lev, lo, hi); ! int r = HASH(hash), r2 = 0; ! while (r != n && r != 0) { ! r2 = r; ! r = NEXT(r); ! } ! if (r == 0) { ! // Cannot find node in the hash chain ?! ! throw new InternalError(); ! } ! // Remove from this hash chain. ! int NEXT_r = NEXT(r); ! if (r2 == 0) { ! SETHASH(hash, NEXT_r); } else { ! SETNEXT(r2, NEXT_r); ! } ! // Set level of this node. ! SETLEVEL(n, newLev); ! lo = LOW(n); hi = HIGH(n); ! // Add to new hash chain. ! hash = NODEHASH(newLev, lo, hi); ! r = HASH(hash); ! SETHASH(hash, n); ! SETNEXT(n, r); ! } ! } ! ! void dup_level(int levToInsert, int val) { ! for (int n = 2; n < bddnodesize; n++) { ! if (LOW(n) == INVALID_BDD) continue; ! int lev = LEVEL(n); ! if (lev != levToInsert || lev == bddvarnum-1) { ! // Stays the same. ! continue; } + int lo, hi, newLev; + lo = LOW(n); + hi = HIGH(n); + // Duplicate this node. + _assert(LEVEL(lo) > levToInsert + 1); + _assert(LEVEL(hi) > levToInsert + 1); + int n_low, n_high; + bdd_addref(n); + // 0 = var is zero, 1 = var is one, -1 = var equals other + n_low = bdd_makenode(levToInsert+1, val<=0 ? lo : 0, val<=0 ? 0 : lo); + n_high = bdd_makenode(levToInsert+1, val==0 ? hi : 0, val==0 ? 0 : hi); + bdd_delref(n); + newLev = lev; + SETLOW(n, n_low); + SETHIGH(n, n_high); // Find this node in its hash chain. |
|
From: John W. <joe...@us...> - 2005-04-17 10:21:45
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20708/buddy/src Modified Files: kernel.h kernel.c pairs.c Log Message: Updates to duplicateVar. Seems to actually work now. Index: kernel.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.h,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** kernel.h 31 Jan 2005 10:04:59 -0000 1.4 --- kernel.h 17 Apr 2005 10:21:27 -0000 1.5 *************** *** 450,453 **** --- 450,455 ---- extern void bdd_cpp_init(void); + extern void fixup_pairs(int,int); + #ifdef CPLUSPLUS } Index: kernel.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v retrieving revision 1.9 retrieving revision 1.10 diff -C2 -d -r1.9 -r1.10 *** kernel.c 8 Apr 2005 05:28:05 -0000 1.9 --- kernel.c 17 Apr 2005 10:21:27 -0000 1.10 *************** *** 1659,1701 **** } ! static void insert_level(int levToInsert, int dupLevel, int val) ! { ! int n, lev; for (n = 2; n < bddnodesize; n++) { ! int lo, hi, newLev, hash, r, r2, NEXT_r; if (LOW(n) == INVALID_BDD) continue; lev = LEVEL(n); ! if (lev < levToInsert || lev == bddvarnum-1) { ! // Stays the same. continue; } ! if (dupLevel && lev == levToInsert) { ! // Duplicate this node. ! int n_low, n_high; ! bdd_addref(n); ! // 0 = var is zero, 1 = var is one, -1 = var equals other ! n_low = bdd_makenode(levToInsert+1, val<=0 ? LOW(n) : 0, val<=0 ? 0 : LOW(n)); ! n_high = bdd_makenode(levToInsert+1, val==0 ? HIGH(n) : 0, val==0 ? 0 : HIGH(n)); ! bdd_delref(n); ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev; ! SETLOW(n, n_low); ! SETHIGH(n, n_high); } else { ! // Need to increase level by one. ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev+1; } ! ! // Find this node in its hash chain. hash = NODEHASH(lev, lo, hi); ! r = HASH(hash), r2 = 0; ! while (r != n) { r2 = r; r = NEXT(r); } - // Remove from this hash chain. NEXT_r = NEXT(r); if (r2 == 0) { --- 1659,1723 ---- } ! static void insert_level(int levToInsert) { ! int n; for (n = 2; n < bddnodesize; n++) { ! int lev, lo, hi, newLev, hash, r, r2, NEXT_r; if (LOW(n) == INVALID_BDD) continue; lev = LEVEL(n); ! if (lev <= levToInsert || lev == bddvarnum-1) { continue; } ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev+1; ! hash = NODEHASH(lev, lo, hi); ! r = HASH(hash); ! r2 = 0; ! while (r != n && r != 0) { ! r2 = r; ! r = NEXT(r); ! } ! NEXT_r = NEXT(r); ! if (r2 == 0) { ! SETHASH(hash, NEXT_r); } else { ! SETNEXT(r2, NEXT_r); } ! SETLEVEL(n, newLev); ! lo = LOW(n); hi = HIGH(n); ! hash = NODEHASH(newLev, lo, hi); ! r = HASH(hash); ! SETHASH(hash, n); ! SETNEXT(n, r); ! } ! } ! ! static void dup_level(int levToInsert, int val) { ! int n; ! for (n = 2; n < bddnodesize; n++) { ! int lev, lo, hi, newLev; ! int n_low, n_high; ! int hash, r, r2, NEXT_r; ! if (LOW(n) == INVALID_BDD) continue; ! lev = LEVEL(n); ! if (lev != levToInsert || lev == bddvarnum-1) { ! continue; ! } ! lo = LOW(n); ! hi = HIGH(n); ! bdd_addref(n); ! n_low = bdd_makenode(levToInsert+1, val<=0 ? lo : 0, val<=0 ? 0 : lo); ! n_high = bdd_makenode(levToInsert+1, val==0 ? hi : 0, val==0 ? 0 : hi); ! bdd_delref(n); ! newLev = lev; ! SETLOW(n, n_low); ! SETHIGH(n, n_high); hash = NODEHASH(lev, lo, hi); ! r = HASH(hash); ! r2 = 0; ! while (r != n && r != 0) { r2 = r; r = NEXT(r); } NEXT_r = NEXT(r); if (r2 == 0) { *************** *** 1704,1711 **** SETNEXT(r2, NEXT_r); } - // Set level of this node. SETLEVEL(n, newLev); lo = LOW(n); hi = HIGH(n); - // Add to new hash chain. hash = NODEHASH(newLev, lo, hi); r = HASH(hash); --- 1726,1731 ---- *************** *** 1716,1732 **** int bdd_duplicatevar(int var) { ! int newVar, lev, i; if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); return bddfalse; } - bdd_disable_reorder(); - newVar = bddvarnum; lev = bddvar2level[var]; bdd_setvarnum(bddvarnum+1); ! insert_level(lev, 1, 0); ! for (i = 0; i <= bddvarnum; ++i) { if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) ++bddvar2level[i]; --- 1736,1751 ---- int bdd_duplicatevar(int var) { ! int newVar, lev, i, bdv; if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); return bddfalse; } bdd_disable_reorder(); newVar = bddvarnum; lev = bddvar2level[var]; bdd_setvarnum(bddvarnum+1); ! insert_level(lev); ! dup_level(lev, 0); ! for (i = 0; i < bddvarnum; ++i) { if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) ++bddvar2level[i]; *************** *** 1737,1743 **** } bddlevel2var[lev+1] = newVar; ! bdd_enable_reorder(); - return newVar; } --- 1756,1768 ---- } bddlevel2var[lev+1] = newVar; ! for (bdv = 0; bdv < bddvarnum; bdv++) { ! bddvarset[bdv * 2] = PUSHREF(bdd_makenode(bddvar2level[bdv], 0, 1)); ! bddvarset[bdv * 2 + 1] = bdd_makenode(bddvar2level[bdv], 1, 0); ! POPREF(1); ! SETMAXREF(bddvarset[bdv * 2]); ! SETMAXREF(bddvarset[bdv * 2 + 1]); ! } ! fixup_pairs(lev, newVar); bdd_enable_reorder(); return newVar; } Index: pairs.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/pairs.c,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** pairs.c 30 Jan 2005 14:43:02 -0000 1.3 --- pairs.c 17 Apr 2005 10:21:27 -0000 1.4 *************** *** 360,363 **** --- 360,379 ---- } + void fixup_pairs(int lev, int newVar) + { + bddPair* pair; + for (pair = pairs; pair != NULL; pair = pair->next) { + int i; + bdd_delref(pair->result[bddvarnum-1]); + for (i = bddvarnum-1; i > lev+1; --i) { + pair->result[i] = pair->result[i-1]; + if (i != LEVEL(pair->result[i]) && i > pair->last) { + pair->last = i; + } + } + pair->result[lev+1] = bdd_ithvar(newVar); + } + } + /* EOF */ |
|
From: John W. <joe...@us...> - 2005-04-14 23:58:50
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4104/net/sf/javabdd Modified Files: JFactory.java BDDDomain.java BDDFactory.java Log Message: More updates. Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** BDDFactory.java 8 Apr 2005 05:27:52 -0000 1.7 --- BDDFactory.java 14 Apr 2005 23:58:41 -0000 1.8 *************** *** 1525,1528 **** --- 1525,1534 ---- int di = d.getIndex(); int local = localOrders[di][bitNumber]; + if (local >= d.vars().length) { + System.out.println("bug!"); + } + if (bitIndex >= varorder.length) { + System.out.println("bug2!"); + } varorder[bitIndex++] = d.vars()[local]; } Index: BDDDomain.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDDomain.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** BDDDomain.java 8 Apr 2005 05:27:52 -0000 1.5 --- BDDDomain.java 14 Apr 2005 23:58:41 -0000 1.6 *************** *** 308,314 **** if (range.compareTo(realsize) < 0) return ivar.length; ! this.realsize = range; int binsize = 1; ! while (calcsize.compareTo(range) < 0) { binsize++; calcsize = calcsize.shiftLeft(1); --- 308,314 ---- if (range.compareTo(realsize) < 0) return ivar.length; ! this.realsize = range.add(BigInteger.ONE); int binsize = 1; ! while (calcsize.compareTo(range) <= 0) { binsize++; calcsize = calcsize.shiftLeft(1); *************** *** 321,324 **** --- 321,325 ---- for (int i = ivar.length; i < new_ivar.length; ++i) { int newVar = factory.duplicateVar(new_ivar[i-1]); + factory.firstbddvar++; new_ivar[i] = newVar; } Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.18 retrieving revision 1.19 diff -C2 -d -r1.18 -r1.19 *** JFactory.java 8 Apr 2005 05:27:52 -0000 1.18 --- JFactory.java 14 Apr 2005 23:58:41 -0000 1.19 *************** *** 3571,3575 **** for (n = 0; n < bddvarnum; n++) ! p.result[n] = bdd_ithvar(n); p.last = 0; } --- 3571,3575 ---- for (n = 0; n < bddvarnum; n++) ! p.result[n] = bdd_ithvar(bddlevel2var[n]); p.last = 0; } *************** *** 3603,3609 **** StringBuffer sb = new StringBuffer(); sb.append('{'); for (int i = 0; i < result.length; ++i) { if (result[i] != bdd_ithvar(bddlevel2var[i])) { ! if (i > 0) sb.append(", "); sb.append(bddlevel2var[i]); sb.append('='); --- 3603,3611 ---- StringBuffer sb = new StringBuffer(); sb.append('{'); + boolean any = false; for (int i = 0; i < result.length; ++i) { if (result[i] != bdd_ithvar(bddlevel2var[i])) { ! if (any) sb.append(", "); ! any = true; sb.append(bddlevel2var[i]); sb.append('='); |
|
From: John W. <joe...@us...> - 2005-04-08 05:28:16
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15852/buddy/src Modified Files: kernel.c bdd.h reorder.c Log Message: Support for dynamic resizing domains. Index: kernel.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v retrieving revision 1.8 retrieving revision 1.9 diff -C2 -d -r1.8 -r1.9 *** kernel.c 15 Mar 2005 09:22:24 -0000 1.8 --- kernel.c 8 Apr 2005 05:28:05 -0000 1.9 *************** *** 1378,1382 **** int bdd_makenode(unsigned int level, int low, int high) { - register BddNode *node; register unsigned int hash; register int res; --- 1378,1381 ---- *************** *** 1528,1532 **** int oldsize = bddnodesize; int newsize; - int n; if (bddnodesize >= bddmaxnodesize && bddmaxnodesize > 0) --- 1527,1530 ---- *************** *** 1661,1664 **** --- 1659,1745 ---- } + static void insert_level(int levToInsert, int dupLevel, int val) + { + int n, lev; + for (n = 2; n < bddnodesize; n++) { + int lo, hi, newLev, hash, r, r2, NEXT_r; + if (LOW(n) == INVALID_BDD) continue; + lev = LEVEL(n); + if (lev < levToInsert || lev == bddvarnum-1) { + // Stays the same. + continue; + } + if (dupLevel && lev == levToInsert) { + // Duplicate this node. + int n_low, n_high; + bdd_addref(n); + // 0 = var is zero, 1 = var is one, -1 = var equals other + n_low = bdd_makenode(levToInsert+1, val<=0 ? LOW(n) : 0, val<=0 ? 0 : LOW(n)); + n_high = bdd_makenode(levToInsert+1, val==0 ? HIGH(n) : 0, val==0 ? 0 : HIGH(n)); + bdd_delref(n); + lo = LOW(n); + hi = HIGH(n); + newLev = lev; + SETLOW(n, n_low); + SETHIGH(n, n_high); + } else { + // Need to increase level by one. + lo = LOW(n); + hi = HIGH(n); + newLev = lev+1; + } + + // Find this node in its hash chain. + hash = NODEHASH(lev, lo, hi); + r = HASH(hash), r2 = 0; + while (r != n) { + r2 = r; + r = NEXT(r); + } + // Remove from this hash chain. + NEXT_r = NEXT(r); + if (r2 == 0) { + SETHASH(hash, NEXT_r); + } else { + SETNEXT(r2, NEXT_r); + } + // Set level of this node. + SETLEVEL(n, newLev); + lo = LOW(n); hi = HIGH(n); + // Add to new hash chain. + hash = NODEHASH(newLev, lo, hi); + r = HASH(hash); + SETHASH(hash, n); + SETNEXT(n, r); + } + } + + int bdd_duplicatevar(int var) { + int newVar, lev, i; + if (var < 0 || var >= bddvarnum) { + bdd_error(BDD_VAR); + return bddfalse; + } + + bdd_disable_reorder(); + + newVar = bddvarnum; + lev = bddvar2level[var]; + bdd_setvarnum(bddvarnum+1); + insert_level(lev, 1, 0); + for (i = 0; i <= bddvarnum; ++i) { + if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) + ++bddvar2level[i]; + } + bddvar2level[newVar] = lev+1; + for (i = bddvarnum-2; i > lev; --i) { + bddlevel2var[i+1] = bddlevel2var[i]; + } + bddlevel2var[lev+1] = newVar; + + bdd_enable_reorder(); + + return newVar; + } /* EOF */ Index: reorder.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/reorder.c,v retrieving revision 1.8 retrieving revision 1.9 diff -C2 -d -r1.8 -r1.9 *** reorder.c 31 Jan 2005 12:04:16 -0000 1.8 --- reorder.c 8 Apr 2005 05:28:05 -0000 1.9 *************** *** 1665,1669 **** } - static int reorder_init(void) { --- 1665,1668 ---- Index: bdd.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bdd.h,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** bdd.h 17 Nov 2004 23:05:02 -0000 1.4 --- bdd.h 8 Apr 2005 05:28:05 -0000 1.5 *************** *** 235,238 **** --- 235,239 ---- extern int bdd_setmaxincrease(int); extern int bdd_setminfreenodes(int); + extern double bdd_setincreasefactor(double); extern int bdd_getnodenum(void); extern int bdd_setallocnum(int); *************** *** 262,265 **** --- 263,267 ---- extern BDD bdd_delref(BDD); extern void bdd_gbc(void); + extern int bdd_duplicatevar(int); extern int bdd_scanset(BDD, int**, int*); extern BDD bdd_makeset(int *, int); |
|
From: John W. <joe...@us...> - 2005-04-08 05:28:05
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15724/net/sf/javabdd Modified Files: CALFactory.java TestBDDFactory.java JFactory.java JDDFactory.java BuDDyFactory.java BDDDomain.java MicroFactory.java CUDDFactory.java BDDFactory.java TypedBDDFactory.java Log Message: Support for dynamic resizing domains. Index: TestBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TestBDDFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** TestBDDFactory.java 31 Jan 2005 00:08:05 -0000 1.5 --- TestBDDFactory.java 8 Apr 2005 05:27:52 -0000 1.6 *************** *** 640,643 **** --- 640,653 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + int r1 = f1.duplicateVar(var); + int r2 = f2.duplicateVar(var); + assertSame(r1 == r2, "duplicateVar"); + return r1; + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#ithVar(int) */ Index: BDDDomain.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDDomain.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** BDDDomain.java 1 Nov 2004 09:41:50 -0000 1.4 --- BDDDomain.java 8 Apr 2005 05:27:52 -0000 1.5 *************** *** 299,302 **** --- 299,336 ---- } + public int ensureCapacity(long range) { + return ensureCapacity(BigInteger.valueOf(range)); + } + public int ensureCapacity(BigInteger range) { + BigInteger calcsize = BigInteger.valueOf(2L); + if (range.signum() < 0) + throw new BDDException(); + if (range.compareTo(realsize) < 0) + return ivar.length; + this.realsize = range; + int binsize = 1; + while (calcsize.compareTo(range) < 0) { + binsize++; + calcsize = calcsize.shiftLeft(1); + } + if (ivar.length == binsize) return binsize; + + int[] new_ivar = new int[binsize]; + System.arraycopy(ivar, 0, new_ivar, 0, ivar.length); + BDDFactory factory = getFactory(); + for (int i = ivar.length; i < new_ivar.length; ++i) { + int newVar = factory.duplicateVar(new_ivar[i-1]); + new_ivar[i] = newVar; + } + this.ivar = new_ivar; + this.var.free(); + BDD nvar = factory.one(); + for (int i = 0; i < ivar.length; ++i) { + nvar.andWith(factory.ithVar(ivar[i])); + } + this.var = nvar; + return binsize; + } + /* (non-Javadoc) * @see java.lang.Object#toString() *************** *** 313,321 **** * <p> * Be careful when using this method for BDDs with a large number ! * of entries, as it allocates a long[] array of dimension k. * * @param bdd bdd that is the disjunction of domain indices * @see #getVarIndices(BDD,int) ! * @see #ithVar(long) */ public BigInteger[] getVarIndices(BDD bdd) { --- 347,355 ---- * <p> * Be careful when using this method for BDDs with a large number ! * of entries, as it allocates a BigInteger[] array of dimension k. * * @param bdd bdd that is the disjunction of domain indices * @see #getVarIndices(BDD,int) ! * @see #ithVar(BigInteger) */ public BigInteger[] getVarIndices(BDD bdd) { Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.17 retrieving revision 1.18 diff -C2 -d -r1.17 -r1.18 *** JFactory.java 26 Feb 2005 21:41:40 -0000 1.17 --- JFactory.java 8 Apr 2005 05:27:52 -0000 1.18 *************** *** 612,615 **** --- 612,617 ---- } + private static class ReorderException extends RuntimeException {} + static final int bddtrue = 1; static final int bddfalse = 0; *************** *** 793,797 **** CHECK(root); if (root < 2) ! throw new JavaBDDException(BDD_ILLBDD); return (bddlevel2var[LEVEL(root)]); --- 795,799 ---- CHECK(root); if (root < 2) ! bdd_error(BDD_ILLBDD); return (bddlevel2var[LEVEL(root)]); *************** *** 900,904 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); if (firstReorder-- == 1) --- 902,906 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); if (firstReorder-- == 1) *************** *** 965,969 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 967,971 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1078,1082 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1080,1084 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1183,1187 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1185,1189 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1466,1470 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1468,1472 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1817,1821 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1819,1823 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1916,1920 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1918,1922 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1997,2001 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1999,2003 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2067,2071 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2069,2073 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2108,2112 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2110,2114 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2147,2151 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2149,2153 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2186,2190 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2188,2192 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2256,2260 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2258,2262 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2430,2434 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2432,2436 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2478,2484 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); - if (firstReorder-- == 1) continue again; --- 2480,2485 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); if (firstReorder-- == 1) continue again; *************** *** 3056,3066 **** bdd_gbc(); - /* if ((bddnodesize-bddfreenum) >= usednodes_nextreorder && ! bdd_reorder_ready()) { ! longjmp(bddexception,1); } - */ if ((bddfreenum * 100) / bddnodesize <= minfreenodes) { --- 3057,3065 ---- bdd_gbc(); if ((bddnodesize-bddfreenum) >= usednodes_nextreorder && ! bdd_reorder_ready()) { ! throw new ReorderException(); } if ((bddfreenum * 100) / bddnodesize <= minfreenodes) { *************** *** 3176,3180 **** if (bddrunning) ! throw new JavaBDDException(BDD_RUNNING); bddnodesize = bdd_prime_gte(initnodesize); --- 3175,3179 ---- if (bddrunning) ! bdd_error(BDD_RUNNING); bddnodesize = bdd_prime_gte(initnodesize); *************** *** 3600,3603 **** --- 3599,3619 ---- bdd_resetpair(this); } + + public String toString() { + StringBuffer sb = new StringBuffer(); + sb.append('{'); + for (int i = 0; i < result.length; ++i) { + if (result[i] != bdd_ithvar(bddlevel2var[i])) { + if (i > 0) sb.append(", "); + sb.append(bddlevel2var[i]); + sb.append('='); + bdd b = new bdd(result[i]); + sb.append(b); + b.free(); + } + } + sb.append('}'); + return sb.toString(); + } } *************** *** 4575,4584 **** } int bdd_setvarnum(int num) { int bdv; int oldbddvarnum = bddvarnum; - bdd_disable_reorder(); - if (num < 1 || num > MAXVAR) { bdd_error(BDD_RANGE); --- 4591,4654 ---- } + /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + if (var < 0 || var >= bddvarnum) { + bdd_error(BDD_VAR); + return bddfalse; + } + + bdd_disable_reorder(); + + int newVar = bddvarnum; + int lev = bddvar2level[var]; + //System.out.println("Adding new variable "+newVar+" at level "+(lev+1)); + // Increase the size of the various data structures. + bdd_setvarnum(bddvarnum+1); + // Actually duplicate the var in all BDDs. + insert_level(lev, true, 0); + // Fix up bddvar2level + for (int i = 0; i < bddvarnum; ++i) { + if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) + ++bddvar2level[i]; + } + bddvar2level[newVar] = lev+1; + // Fix up bddlevel2var + for (int i = bddvarnum-2; i > lev; --i) { + bddlevel2var[i+1] = bddlevel2var[i]; + } + bddlevel2var[lev+1] = newVar; + // Fix up bddvarset + for (int bdv = 0; bdv < bddvarnum; bdv++) { + bddvarset[bdv * 2] = PUSHREF(bdd_makenode(bddvar2level[bdv], 0, 1)); + bddvarset[bdv * 2 + 1] = bdd_makenode(bddvar2level[bdv], 1, 0); + POPREF(1); + + SETMAXREF(bddvarset[bdv * 2]); + SETMAXREF(bddvarset[bdv * 2] + 1); + } + // Fix up pairs + for (bddPair pair = pairs; pair != null; pair = pair.next) { + bdd_delref(pair.result[bddvarnum-1]); + for (int i = bddvarnum-1; i > lev+1; --i) { + pair.result[i] = pair.result[i-1]; + if (i != LEVEL(pair.result[i]) && i > pair.last) { + pair.last = i; + } + } + pair.result[lev+1] = bdd_ithvar(newVar); + //System.out.println("Pair "+pair); + } + + bdd_enable_reorder(); + + return newVar; + } + int bdd_setvarnum(int num) { int bdv; int oldbddvarnum = bddvarnum; if (num < 1 || num > MAXVAR) { bdd_error(BDD_RANGE); *************** *** 4591,4594 **** --- 4661,4666 ---- return 0; + bdd_disable_reorder(); + if (bddvarset == null) { bddvarset = new int[num * 2]; *************** *** 5391,5394 **** --- 5463,5524 ---- } + void insert_level(int levToInsert, boolean dupLevel, int val) { + for (int n = 2; n < bddnodesize; n++) { + if (LOW(n) == INVALID_BDD) continue; + int lev = LEVEL(n); + if (lev < levToInsert || lev == bddvarnum-1) { + // Stays the same. + continue; + } + int lo, hi, newLev; + if (dupLevel && lev == levToInsert) { + // Duplicate this node. + int n_low, n_high; + bdd_addref(n); + // 0 = var is zero, 1 = var is one, -1 = var equals other + n_low = bdd_makenode(levToInsert+1, val<=0 ? LOW(n) : 0, val<=0 ? 0 : LOW(n)); + n_high = bdd_makenode(levToInsert+1, val==0 ? HIGH(n) : 0, val==0 ? 0 : HIGH(n)); + bdd_delref(n); + lo = LOW(n); + hi = HIGH(n); + newLev = lev; + SETLOW(n, n_low); + SETHIGH(n, n_high); + } else { + // Need to increase level by one. + lo = LOW(n); + hi = HIGH(n); + newLev = lev+1; + } + + // Find this node in its hash chain. + int hash = NODEHASH(lev, lo, hi); + int r = HASH(hash), r2 = 0; + while (r != n && r != 0) { + r2 = r; + r = NEXT(r); + } + if (r == 0) { + // Cannot find node in the hash chain ?! + throw new InternalError(); + } + // Remove from this hash chain. + int NEXT_r = NEXT(r); + if (r2 == 0) { + SETHASH(hash, NEXT_r); + } else { + SETNEXT(r2, NEXT_r); + } + // Set level of this node. + SETLEVEL(n, newLev); + lo = LOW(n); hi = HIGH(n); + // Add to new hash chain. + hash = NODEHASH(newLev, lo, hi); + r = HASH(hash); + SETHASH(hash, n); + SETNEXT(n, r); + } + } + int mark_roots() { boolean[] dep = new boolean[bddvarnum]; Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** BDDFactory.java 30 Jan 2005 14:42:23 -0000 1.6 --- BDDFactory.java 8 Apr 2005 05:27:52 -0000 1.7 *************** *** 897,901 **** public abstract void swapVar(int v1, int v2); ! /**** VARIABLE BLOCKS ****/ --- 897,907 ---- public abstract void swapVar(int v1, int v2); ! /** ! * Duplicate a BDD variable. ! * ! * @param var var to duplicate ! * @return index of new variable ! */ ! public abstract int duplicateVar(int var); /**** VARIABLE BLOCKS ****/ Index: TypedBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TypedBDDFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** TypedBDDFactory.java 19 Oct 2004 21:47:05 -0000 1.5 --- TypedBDDFactory.java 8 Apr 2005 05:27:52 -0000 1.6 *************** *** 161,164 **** --- 161,171 ---- } + /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + return factory.duplicateVar(var); + } + public BDDDomain whichDomain(int var) { for (int i = 0; i < numberOfDomains(); ++i) { Index: JDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JDDFactory.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** JDDFactory.java 19 Oct 2004 11:11:35 -0000 1.4 --- JDDFactory.java 8 Apr 2005 05:27:52 -0000 1.5 *************** *** 667,670 **** --- 667,678 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + // TODO Implement this. + throw new UnsupportedOperationException(); + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#ithVar(int) */ Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** BuDDyFactory.java 29 Jan 2005 11:37:20 -0000 1.7 --- BuDDyFactory.java 8 Apr 2005 05:27:52 -0000 1.8 *************** *** 299,302 **** --- 299,310 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + return duplicateVar0(var); + } + private static native int duplicateVar0(int var); + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#extVarNum(int) */ Index: CUDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/CUDDFactory.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** CUDDFactory.java 19 Oct 2004 11:11:35 -0000 1.4 --- CUDDFactory.java 8 Apr 2005 05:27:52 -0000 1.5 *************** *** 204,207 **** --- 204,215 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + // TODO Implement this. + throw new UnsupportedOperationException(); + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#ithVar(int) */ Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** MicroFactory.java 26 Feb 2005 21:19:12 -0000 1.7 --- MicroFactory.java 8 Apr 2005 05:27:52 -0000 1.8 *************** *** 4942,4945 **** --- 4942,4975 ---- } + /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + if (var < 0 || var >= bddvarnum) { + bdd_error(BDD_VAR); + return bddfalse; + } + + bdd_disable_reorder(); + + int newVar = bddvarnum; + int lev = bddvar2level[var]; + bdd_setvarnum(bddvarnum+1); + insert_level(lev, true, 0); + for (int i = 0; i < bddvar2level.length; ++i) { + if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) + ++bddvar2level[i]; + } + bddvar2level[newVar] = lev+1; + for (int i = bddvarnum-2; i > lev; --i) { + bddlevel2var[i+1] = bddlevel2var[i]; + } + bddlevel2var[lev+1] = newVar; + + bdd_enable_reorder(); + + return newVar; + } + int bdd_setvarnum(int num) { int bdv; *************** *** 5749,5752 **** --- 5779,5840 ---- } + void insert_level(int levToInsert, boolean dupLevel, int val) { + for (int n = 2; n < bddnodesize; n++) { + if (LOW(n) == INVALID_BDD) continue; + int lev = LEVEL(n); + if (lev < levToInsert || lev == bddvarnum-1) { + // Stays the same. + continue; + } + int lo, hi, newLev; + if (dupLevel && lev == levToInsert) { + // Duplicate this node. + int n_low, n_high; + bdd_addref(n); + // 0 = var is zero, 1 = var is one, -1 = var equals other + n_low = bdd_makenode(levToInsert+1, val<=0 ? LOW(n) : 0, val<=0 ? 0 : LOW(n)); + n_high = bdd_makenode(levToInsert+1, val==0 ? HIGH(n) : 0, val==0 ? 0 : HIGH(n)); + bdd_delref(n); + lo = LOW(n); + hi = HIGH(n); + newLev = lev; + SETLOW(n, n_low); + SETHIGH(n, n_high); + } else { + // Need to increase level by one. + lo = LOW(n); + hi = HIGH(n); + newLev = lev+1; + } + + // Find this node in its hash chain. + int hash = NODEHASH(lev, lo, hi); + int r = HASH(hash), r2 = 0; + while (r != n && r != 0) { + r2 = r; + r = NEXT(r); + } + if (r == 0) { + // Cannot find node in the hash chain ?! + throw new InternalError(); + } + // Remove from this hash chain. + int NEXT_r = NEXT(r); + if (r2 == 0) { + SETHASH(hash, NEXT_r); + } else { + SETNEXT(r2, NEXT_r); + } + // Set level of this node. + SETLEVEL(n, newLev); + lo = LOW(n); hi = HIGH(n); + // Add to new hash chain. + hash = NODEHASH(newLev, lo, hi); + r = HASH(hash); + SETHASH(hash, n); + SETNEXT(n, r); + } + } + int mark_roots() { boolean[] dep = new boolean[bddvarnum]; Index: CALFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/CALFactory.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** CALFactory.java 19 Oct 2004 11:11:34 -0000 1.4 --- CALFactory.java 8 Apr 2005 05:27:52 -0000 1.5 *************** *** 177,180 **** --- 177,188 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + // TODO Implement this. + throw new UnsupportedOperationException(); + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#ithVar(int) */ |
|
From: John W. <joe...@us...> - 2005-04-08 05:28:04
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15724 Modified Files: buddy_jni.c Log Message: Support for dynamic resizing domains. Index: buddy_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy_jni.c,v retrieving revision 1.29 retrieving revision 1.30 diff -C2 -d -r1.29 -r1.30 *** buddy_jni.c 15 Mar 2005 09:22:13 -0000 1.29 --- buddy_jni.c 8 Apr 2005 05:27:52 -0000 1.30 *************** *** 42,46 **** printf("bdd_errstring(%d)\n", errcode); #endif ! printf("BuDDy error: %s\n", bdd_errstring(errcode)); bdd_error = errcode; #if defined(TRACE_BUDDYLIB) --- 42,46 ---- printf("bdd_errstring(%d)\n", errcode); #endif ! //printf("BuDDy error: %s\n", bdd_errstring(errcode)); bdd_error = errcode; #if defined(TRACE_BUDDYLIB) *************** *** 511,514 **** --- 511,532 ---- /* * Class: net_sf_javabdd_BuDDyFactory + * Method: duplicateVar0 + * Signature: (I)I + */ + JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_duplicateVar0 + (JNIEnv *env, jclass cl, jint var) + { + int result; + jnienv = env; + #if defined(TRACE_BUDDYLIB) + printf("bdd_duplicatevar(%d)\n", var); + #endif + result = bdd_duplicatevar(var); + check_error(env); + return result; + } + + /* + * Class: net_sf_javabdd_BuDDyFactory * Method: extVarNum0 * Signature: (I)I |
|
From: John W. <joe...@us...> - 2005-03-15 09:22:41
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2986 Modified Files: buddy_jni.c Log Message: Added setIncreaseFactor() Index: buddy_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy_jni.c,v retrieving revision 1.28 retrieving revision 1.29 diff -C2 -d -r1.28 -r1.29 *** buddy_jni.c 31 Jan 2005 12:17:46 -0000 1.28 --- buddy_jni.c 15 Mar 2005 09:22:13 -0000 1.29 *************** *** 439,442 **** --- 439,460 ---- /* * Class: net_sf_javabdd_BuDDyFactory + * Method: setIncreaseFactor0 + * Signature: (D)D + */ + JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_setIncreaseFactor0 + (JNIEnv *env, jclass cl, jdouble r) + { + jdouble result; + jnienv = env; + #if defined(TRACE_BUDDYLIB) + printf("bdd_setincreasefactor(%lf)\n", r); + #endif + result = bdd_setincreasefactor(r); + check_error(env); + return result; + } + + /* + * Class: net_sf_javabdd_BuDDyFactory * Method: setCacheRatio0 * Signature: (I)I |
|
From: John W. <joe...@us...> - 2005-03-15 09:22:41
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2986/buddy/src Modified Files: kernel.c Log Message: Added setIncreaseFactor() Index: kernel.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** kernel.c 31 Jan 2005 10:23:39 -0000 1.7 --- kernel.c 15 Mar 2005 09:22:24 -0000 1.8 *************** *** 91,94 **** --- 91,95 ---- int bddmaxnodesize; /* Maximum allowed number of nodes */ int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ + double bddincreasefactor; /* Increase factor when growing table. */ BddNode* bddnodes; /* All of the bdd nodes */ int bddfreepos; /* First free node */ *************** *** 236,239 **** --- 237,241 ---- usednodes_nextreorder = bddnodesize; bddmaxnodeincrease = DEFAULTMAXNODEINC; + bddincreasefactor = 2; bdderrorcond = 0; *************** *** 573,577 **** DESCR {* The node table is expanded by doubling the size of the table when no more free nodes can be found, but a maximum for the ! number of new nodes added can be set with {\tt bdd\_maxincrease} to {\tt size} nodes. The default is 50000 nodes (1 Mb). *} RETURN {* The old threshold on succes, otherwise a negative error code. *} --- 575,579 ---- DESCR {* The node table is expanded by doubling the size of the table when no more free nodes can be found, but a maximum for the ! number of new nodes added can be set with {\tt bdd\_setmaxincrease} to {\tt size} nodes. The default is 50000 nodes (1 Mb). *} RETURN {* The old threshold on succes, otherwise a negative error code. *} *************** *** 593,596 **** --- 595,624 ---- /* + NAME {* bdd\_increasefactor *} + SECTION {* kernel *} + SHORT {* set factor used to increase node table *} + PROTO {* double bdd_setincreasefactor(double size) *} + DESCR {* The node table is expanded by multiplying the size by this factor + when no more free nodes can be found, but a maximum for the + number of new nodes added can be set with {\tt bdd\_setmaxincrease} + to {\tt size} nodes. The default is 2. *} + RETURN {* The old threshold on success, otherwise a negative error code. *} + ALSO {* bdd\_setmaxnodenum, bdd\_setminfreenodes, bdd\_setmaxincrease *} + */ + double bdd_setincreasefactor(double size) + { + double old = bddincreasefactor; + + BUDDY_PROLOGUE; + ADD_ARG1(T_DOUBLE,size); + + if (size <= 1) + RETURN(bdd_error(BDD_SIZE)); + + bddincreasefactor = size; + RETURN(old); + } + + /* NAME {* bdd\_setmaxnodenum *} SECTION {* kernel *} *************** *** 1505,1509 **** return -1; ! newsize = bddnodesize << 1; if (newsize > oldsize + bddmaxnodeincrease) --- 1533,1537 ---- return -1; ! newsize = (int) bddnodesize * bddincreasefactor; if (newsize > oldsize + bddmaxnodeincrease) |
|
From: John W. <joe...@us...> - 2005-02-26 21:42:12
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3324/net/sf/javabdd Modified Files: JFactory.java Log Message: Fix stupid bug with OpCacheData. Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.16 retrieving revision 1.17 diff -C2 -d -r1.16 -r1.17 *** JFactory.java 26 Feb 2005 21:32:40 -0000 1.16 --- JFactory.java 26 Feb 2005 21:41:40 -0000 1.17 *************** *** 3436,3439 **** --- 3436,3441 ---- int n; + boolean is_d = cache.table instanceof BddCacheDataD[]; + free(cache.table); cache.table = null; *************** *** 3441,3446 **** newsize = bdd_prime_gte(newsize); - boolean is_d = cache.table instanceof BddCacheDataD[]; - if (is_d) cache.table = new BddCacheDataD[newsize]; --- 3443,3446 ---- |
|
From: John W. <joe...@us...> - 2005-02-26 21:33:05
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv745/net/sf/javabdd Modified Files: JFactory.java Log Message: Fix stupid bug with OpCacheData. Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.15 retrieving revision 1.16 diff -C2 -d -r1.15 -r1.16 *** JFactory.java 26 Feb 2005 21:18:20 -0000 1.15 --- JFactory.java 26 Feb 2005 21:32:40 -0000 1.16 *************** *** 592,596 **** BddCache copy() { BddCache that = new BddCache(); ! that.table = new BddCacheData[this.table.length]; that.tablesize = this.tablesize; for (int i = 0; i < table.length; ++i) { --- 592,601 ---- BddCache copy() { BddCache that = new BddCache(); ! boolean is_d = this.table instanceof BddCacheDataD[]; ! if (is_d) { ! that.table = new BddCacheDataD[this.table.length]; ! } else { ! that.table = new BddCacheDataI[this.table.length]; ! } that.tablesize = this.tablesize; for (int i = 0; i < table.length; ++i) { |
|
From: John W. <joe...@us...> - 2005-02-26 21:19:21
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv29743/net/sf/javabdd Modified Files: MicroFactory.java Log Message: Fix when OutOfMemoryError occurs. Also better cache stats. Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** MicroFactory.java 3 Feb 2005 02:12:27 -0000 1.6 --- MicroFactory.java 26 Feb 2005 21:19:12 -0000 1.7 *************** *** 55,61 **** --- 55,70 ---- BDDFactory f = new MicroFactory(); f.initialize(nodenum, cachesize); + if (CACHESTATS > 0) addShutdownHook(f); return f; } + static void addShutdownHook(final BDDFactory f) { + Runtime.getRuntime().addShutdownHook(new Thread() { + public void run() { + System.out.println(f.getCacheStats().toString()); + } + }); + } + private int[] bddnodes; *************** *** 291,295 **** * Wrapper for the BDD index number used internally in the representation. */ ! private class bdd extends BDD { int _index; --- 300,304 ---- * Wrapper for the BDD index number used internally in the representation. */ ! public class bdd extends BDD { int _index; *************** *** 375,378 **** --- 384,395 ---- } + public BDD relprod(BDD t1, BDD t2, BDD var) { + int x = _index; + int y1 = ((bdd) t1)._index; + int y2 = ((bdd) t2)._index; + int z = ((bdd) var)._index; + return makeBDD(bdd_relprod3(x, y1, y2, z)); + } + /* (non-Javadoc) * @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int) *************** *** 687,690 **** --- 704,711 ---- ++compulsoryMiss; } + void checkCompulsory(int a, int b, int c, int d) { + if (!cache.contains(new QuadOfInts(a, b, c, d))) + ++compulsoryMiss; + } void addCompulsory(int a) { cache.add(new Integer(a)); *************** *** 696,699 **** --- 717,723 ---- cache.add(new TripleOfInts(a, b, c)); } + void addCompulsory(int a, int b, int c, int d) { + cache.add(new QuadOfInts(a, b, c, d)); + } void removeCompulsory(int a) { cache.remove(new Integer(a)); *************** *** 705,708 **** --- 729,753 ---- cache.remove(new TripleOfInts(a, b, c)); } + void removeCompulsory(int a, int b, int c, int d) { + cache.remove(new QuadOfInts(a, b, c, d)); + } + void removeAll(int n) { + for (Iterator i = cache.iterator(); i.hasNext(); ) { + Object o = i.next(); + if (o instanceof Integer) { + Integer a = (Integer) o; + if (n == a.intValue()) i.remove(); + } else if (o instanceof PairOfInts) { + PairOfInts a = (PairOfInts) o; + if (n == a.a || n == a.b) i.remove(); + } else if (o instanceof TripleOfInts) { + TripleOfInts a = (TripleOfInts) o; + if (n == a.a || n == a.b || n == a.c) i.remove(); + } else if (o instanceof QuadOfInts) { + QuadOfInts a = (QuadOfInts) o; + if (n == a.a || n == a.b || n == a.c || n == a.d) i.remove(); + } + } + } } *************** *** 735,738 **** --- 780,797 ---- } + public static class QuadOfInts { + int a, b, c, d; + public QuadOfInts(int x, int y, int z, int q) { a = x; b = y; c = z; d = q; } + public boolean equals(QuadOfInts o) { + return a == o.a && b == o.b && c == o.c && d == o.d; + } + public boolean equals(Object o) { + if (o instanceof QuadOfInts) + return equals((QuadOfInts) o); + return false; + } + public int hashCode() { return a ^ b ^ c ^ d; } + } + private class OpCache1 extends OpCache { OpCache1Entry table[]; *************** *** 1014,1017 **** --- 1073,1152 ---- } + private class OpCache4 extends OpCache { + OpCache4Entry table[]; + + OpCache4(int size) { alloc(size); } + final void alloc(int size) { + table = new OpCache4Entry[size]; + for (int i = 0; i < table.length; ++i) { + table[i] = new OpCache4Entry(); + } + } + final OpCache4Entry lookup(int hash) { + return (OpCache4Entry) table[Math.abs(hash % table.length)]; + } + final void reset() { + for (int i = 0; i < table.length; ++i) { + table[i].a = -1; + } + if (CACHESTATS > 1) cache.clear(); + } + final void clean() { + for (int i = 0; i < table.length; ++i) { + int a = table[i].a; + if (a == -1) continue; + if (LOW(a & NODE_MASK) == INVALID_BDD || + LOW(table[i].b) == INVALID_BDD || + LOW(table[i].c) == INVALID_BDD || + LOW(table[i].d) == INVALID_BDD || + LOW(table[i].res) == INVALID_BDD) { + if (CACHESTATS > 1) removeCompulsory(table[i].a, table[i].b, table[i].c, table[i].d); + table[i].a = -1; + } + } + } + final OpCache4 copy() { + OpCache4 that = new OpCache4(this.table.length); + for (int i = 0; i < this.table.length; ++i) { + that.table[i].a = this.table[i].a; + that.table[i].b = this.table[i].b; + that.table[i].c = this.table[i].c; + that.table[i].d = this.table[i].d; + that.table[i].res = this.table[i].res; + } + if (CACHESTATS > 0) { + that.cacheHit = this.cacheHit; + that.cacheMiss = this.cacheMiss; + if (CACHESTATS > 1) + that.cache.addAll(this.cache); + } + return that; + } + + final int get(OpCache4Entry e, int node1, int node2, int node3, int node4) { + if (e.a != node1 || e.b != node2 || e.c != node3 || e.d != node4) { + if (CACHESTATS > 0) cacheMiss++; + if (CACHESTATS > 1) checkCompulsory(node1, node2, node3, node4); + return -1; + } + if (CACHESTATS > 0) cacheHit++; + return e.res; + } + + final void set(OpCache4Entry e, int node1, int node2, int node3, int node4, int r) { + e.a = node1; + e.b = node2; + e.c = node3; + e.d = node4; + e.res = r; + if (CACHESTATS > 1) addCompulsory(e.a, e.b, e.c, e.d); + } + } + + private static class OpCache4Entry { + int a, b, c, d; + int res; + } + private class OpCacheD extends OpCache { OpCacheDEntry table[]; *************** *** 1306,1313 **** } static final int ANDHASH(int l, int r) { ! return PAIR(l, r); } static final int ORHASH(int l, int r) { ! return PAIR(l, r); } static final int APPLYHASH(int l, int r, int op) { --- 1441,1450 ---- } static final int ANDHASH(int l, int r) { ! //return PAIR(l, r); ! return (l ^ r); } static final int ORHASH(int l, int r) { ! //return PAIR(l, r); ! return (l ^ r); } static final int APPLYHASH(int l, int r, int op) { *************** *** 1342,1346 **** } static final int APPEXHASH(int l, int r, int op) { ! return PAIR(l, r); } --- 1479,1488 ---- } static final int APPEXHASH(int l, int r, int op) { ! //return PAIR(l, r); ! return (l ^ r ^ op); ! } ! static final int APPEX3HASH(int a, int b, int c, int op) { ! //return PAIR(l, r); ! return (a ^ b ^ c ^ op); } *************** *** 1719,1722 **** --- 1861,1866 ---- if (ISONE(r)) return l; + if (l < r) { int t = l; l = r; r = t; } + entry = andcache.lookup(ANDHASH(l, r)); if ((res = andcache.get(entry, l, r)) >= 0) { *************** *** 1755,1758 **** --- 1899,1905 ---- if (ISZERO(l)) return r; if (ISZERO(r)) return l; + + if (l < r) { int t = l; l = r; r = t; } + entry = orcache.lookup(ORHASH(l, r)); if ((res = orcache.get(entry, l, r)) >= 0) { *************** *** 1787,1790 **** --- 1934,1982 ---- } + int bdd_relprod3(int a, int b, int c, int var) { + int res; + int numReorder = 1; + + CHECKa(a, bddfalse); + CHECKa(b, bddfalse); + CHECKa(c, bddfalse); + CHECKa(var, bddfalse); + + if (ISCONST(var)) { + /* Empty set */ + res = bdd_apply(a, b, bddop_and); + return bdd_apply(res, c, bddop_and); + } + + if (andcache == null) andcache = new OpCache2(cachesize); + if (appexcache == null) appexcache = new OpCache3(cachesize); + if (appex3cache == null) appex3cache = new OpCache4(cachesize); + if (orcache == null) orcache = new OpCache2(cachesize); // or_rec() + if (quantcache == null) quantcache = new OpCache2(cachesize); // quant_rec() + + again : for (;;) { + if (varset2vartable(var) < 0) + return bddfalse; + try { + INITREF(); + applyop = bddop_or; + appexop = bddop_and; + appexid = (var << 7) | (appexop << 3) | CACHEID_APPEX; + quantid = appexid; + if (numReorder == 0) bdd_disable_reorder(); + res = relprod3_rec(a, b, c); + if (numReorder == 0) bdd_enable_reorder(); + } catch (BDDException x) { + bdd_checkreorder(); + numReorder--; + continue again; + } + break; + } + + checkresize(); + return res; + } + int bdd_appex(int l, int r, int opr, int var) { int res; *************** *** 2085,2088 **** --- 2277,2282 ---- if (r == 1) return quant_rec(l); + if (l < r) { int t = l; l = r; r = t; } + int LEVEL_l = LEVEL(l); int LEVEL_r = LEVEL(r); *************** *** 2093,2096 **** --- 2287,2291 ---- return res; } + entry = appexcache.lookup(APPEXHASH(l, r, appexop)); if ((res = appexcache.get(entry, l, r, appexid)) >= 0) { *************** *** 2124,2127 **** --- 2319,2399 ---- } + int relprod3_rec(int a, int b, int c) { + OpCache4Entry entry; + int res; + + if (a == 0 || b == 0 || c == 0) return 0; + if (a == b || a == 1) return relprod_rec(b, c); + if (b == c || b == 1) return relprod_rec(a, c); + if (c == a || c == 1) return relprod_rec(a, b); + + int LEVEL_a = LEVEL(a); + int LEVEL_b = LEVEL(b); + int LEVEL_c = LEVEL(c); + if (LEVEL_a > quantlast && LEVEL_b > quantlast && LEVEL_c > quantlast) { + applyop = bddop_and; + res = and_rec(a, b); + res = and_rec(res, c); + applyop = bddop_or; + return res; + } + + entry = appex3cache.lookup(APPEX3HASH(a, b, c, appexop)); + if ((res = appex3cache.get(entry, a, b, c, appexid)) >= 0) { + return res; + } + + int x1, x2, x3, y1, y2, y3, lev; + x1 = y1 = a; + x2 = y2 = b; + x3 = y3 = c; + if (LEVEL_b < LEVEL_c) { + if (LEVEL_a < LEVEL_b) { + // a b c + x1 = LOW(a); y1 = HIGH(a); lev = LEVEL_a; + } else { + x2 = LOW(b); y2 = HIGH(b); lev = LEVEL_b; + if (LEVEL_a == LEVEL_b) { + // ab c + x1 = LOW(a); y1 = HIGH(a); + } + } + } else if (LEVEL_b == LEVEL_c) { + if (LEVEL_a < LEVEL_b) { + // a bc + x1 = LOW(a); y1 = HIGH(a); lev = LEVEL_a; + } else { + x2 = LOW(b); y2 = HIGH(b); lev = LEVEL_b; + x3 = LOW(c); y3 = HIGH(c); + if (LEVEL_a == LEVEL_b) { + // abc + x1 = LOW(a); y1 = HIGH(a); + } + } + } else if (LEVEL_a < LEVEL_c) { + // a c b + x1 = LOW(a); y1 = HIGH(a); lev = LEVEL_a; + } else { + x3 = LOW(c); y3 = HIGH(c); lev = LEVEL_c; + if (LEVEL_a == LEVEL_c) { + x1 = LOW(a); y1 = HIGH(a); + } + } + + PUSHREF(relprod3_rec(x1, x2, x3)); + PUSHREF(relprod3_rec(y1, y2, y3)); + if (INVARSET(lev)) { + res = or_rec(READREF(2), READREF(1)); + } else { + res = bdd_makenode(lev, READREF(2), READREF(1)); + } + + POPREF(2); + + appex3cache.set(entry, a, b, c, appexid, res); + + return res; + } + int appuni_rec(int l, int r, int var) { OpCache3Entry entry; *************** *** 3388,3399 **** if (newsize >= NODE_MASK) newsize = NODE_MASK-1; ! bddnodesize = newsize; ! resize_handler(oldsize, bddnodesize); int[] newnodes; int n; ! newnodes = new int[bddnodesize*__node_size]; System.arraycopy(bddnodes, 0, newnodes, 0, bddnodes.length); bddnodes = newnodes; if (doRehash) --- 3660,3671 ---- if (newsize >= NODE_MASK) newsize = NODE_MASK-1; ! resize_handler(oldsize, newsize); int[] newnodes; int n; ! newnodes = new int[newsize*__node_size]; System.arraycopy(bddnodes, 0, newnodes, 0, bddnodes.length); bddnodes = newnodes; + bddnodesize = newsize; if (doRehash) *************** *** 3524,3527 **** --- 3796,3800 ---- OpCache2 quantcache; /* exist(), forall(), unique(), restrict() */ OpCache3 appexcache; /* appex(), appall(), appuni(), constrain(), compose() */ + OpCache4 appex3cache; /* relprod3() */ OpCache3 itecache; /* ite() */ OpCache2 misccache; /* other functions */ *************** *** 3546,3549 **** --- 3819,3823 ---- quantcache = null; appexcache = null; + appex3cache = null; itecache = null; countcache = null; *************** *** 3566,3569 **** --- 3840,3845 ---- if (appexcache != null) appexcache.reset(); + if (appex3cache != null) + appex3cache.reset(); if (itecache != null) itecache.reset(); *************** *** 3589,3592 **** --- 3865,3870 ---- if (appexcache != null) appexcache.clean(); + if (appex3cache != null) + appex3cache.reset(); if (itecache != null) itecache.clean(); *************** *** 3613,3616 **** --- 3891,3895 ---- quantcache = null; appexcache = null; + appex3cache = null; itecache = null; countcache = null; *************** *** 3629,3632 **** --- 3908,3912 ---- quantcache = null; appexcache = null; + appex3cache = null; itecache = null; countcache = null; *************** *** 3738,3742 **** if (pairsid >= MAX_PAIRSID) throw new BDDException("Too many pairs!"); ! replacecache.reset(); } --- 4018,4022 ---- if (pairsid >= MAX_PAIRSID) throw new BDDException("Too many pairs!"); ! if (replacecache != null) replacecache.reset(); } *************** *** 6387,6397 **** public MicroFactory cloneFactory() { MicroFactory INSTANCE = new MicroFactory(); ! INSTANCE.applycache = this.applycache.copy(); ! INSTANCE.itecache = this.itecache.copy(); ! INSTANCE.quantcache = this.quantcache.copy(); ! INSTANCE.appexcache = this.appexcache.copy(); ! INSTANCE.replacecache = this.replacecache.copy(); ! INSTANCE.misccache = this.misccache.copy(); ! INSTANCE.countcache = this.countcache.copy(); // TODO: potential difference here (!) INSTANCE.rng = new Random(); --- 6667,6686 ---- public MicroFactory cloneFactory() { MicroFactory INSTANCE = new MicroFactory(); ! if (applycache != null) ! INSTANCE.applycache = this.applycache.copy(); ! if (itecache != null) ! INSTANCE.itecache = this.itecache.copy(); ! if (quantcache != null) ! INSTANCE.quantcache = this.quantcache.copy(); ! if (appexcache != null) ! INSTANCE.appexcache = this.appexcache.copy(); ! if (appex3cache != null) ! INSTANCE.appex3cache = this.appex3cache.copy(); ! if (replacecache != null) ! INSTANCE.replacecache = this.replacecache.copy(); ! if (misccache != null) ! INSTANCE.misccache = this.misccache.copy(); ! if (countcache != null) ! INSTANCE.countcache = this.countcache.copy(); // TODO: potential difference here (!) INSTANCE.rng = new Random(); *************** *** 6489,6492 **** --- 6778,6786 ---- cachestats.opMiss += appexcache.cacheMiss; } + if (appex3cache != null) { + System.out.println("Appex3 cache: "+appex3cache); + cachestats.opHit += appex3cache.cacheHit; + cachestats.opMiss += appex3cache.cacheMiss; + } if (itecache != null) { System.out.println("ITE cache: "+itecache); |
|
From: John W. <joe...@us...> - 2005-02-26 21:18:29
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv29553/net/sf/javabdd Modified Files: JFactory.java Log Message: Fix when OutOfMemoryError occurs. Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.14 retrieving revision 1.15 diff -C2 -d -r1.14 -r1.15 *** JFactory.java 31 Jan 2005 10:08:59 -0000 1.14 --- JFactory.java 26 Feb 2005 21:18:20 -0000 1.15 *************** *** 3132,3143 **** if (oldsize > newsize) return 0; ! bddnodesize = newsize; ! resize_handler(oldsize, bddnodesize); int[] newnodes; int n; ! newnodes = new int[bddnodesize*__node_size]; System.arraycopy(bddnodes, 0, newnodes, 0, bddnodes.length); bddnodes = newnodes; if (doRehash) --- 3132,3143 ---- if (oldsize > newsize) return 0; ! resize_handler(oldsize, newsize); int[] newnodes; int n; ! newnodes = new int[newsize*__node_size]; System.arraycopy(bddnodes, 0, newnodes, 0, bddnodes.length); bddnodes = newnodes; + bddnodesize = newsize; if (doRehash) |
|
From: John W. <joe...@us...> - 2005-02-05 00:33:28
|
Update of /cvsroot/javabdd/JavaBDD/xdocs In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4224/xdocs Modified Files: links.xml Log Message: Fix xml Index: links.xml =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/xdocs/links.xml,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** links.xml 4 Feb 2005 11:06:59 -0000 1.2 --- links.xml 5 Feb 2005 00:33:18 -0000 1.3 *************** *** 40,43 **** --- 40,44 ---- </li> </ul> + </section> <section name="Related Links"> <ul> |
