packages: p9m4/p9m4-64bit.patch (NEW) - make it work on 64bit system (from ...

baggins baggins at pld-linux.org
Wed May 6 17:54:04 CEST 2009


Author: baggins                      Date: Wed May  6 15:54:04 2009 GMT
Module: packages                      Tag: HEAD
---- Log message:
- make it work on 64bit system (from debian)

---- Files affected:
packages/p9m4:
   p9m4-64bit.patch (NONE -> 1.1)  (NEW)

---- Diffs:

================================================================
Index: packages/p9m4/p9m4-64bit.patch
diff -u /dev/null packages/p9m4/p9m4-64bit.patch:1.1
--- /dev/null	Wed May  6 17:54:04 2009
+++ packages/p9m4/p9m4-64bit.patch	Wed May  6 17:53:59 2009
@@ -0,0 +1,300 @@
+diff -ur p9m4-0.5.dfsg/control.py p9m4-0.5.dfsg.new/control.py
+--- p9m4-0.5.dfsg/control.py	2007-12-15 15:26:42.000000000 +0000
++++ p9m4-0.5.dfsg.new/control.py	2009-05-03 02:35:56.000000000 +0100
+@@ -566,7 +566,7 @@
+             self.time_ctrl.SetValue(opt[Default])
+         else:
+             error_dialog('error sharing max_second option (%s)' % program.name)
+-            self.time_ctrl = wx.SpinCtrl(self, id, min=-1, max=sys.maxint,
++            self.time_ctrl = wx.SpinCtrl(self, id, min=-1, max=utilities.INT_MAX,
+                                          size=(75,-1))
+             self.time_ctrl.SetValue(60)
+ 
+diff -ur p9m4-0.5.dfsg/options.py p9m4-0.5.dfsg.new/options.py
+--- p9m4-0.5.dfsg/options.py	2007-12-13 02:26:48.000000000 +0000
++++ p9m4-0.5.dfsg.new/options.py	2009-05-03 02:39:28.000000000 +0100
+@@ -320,15 +320,15 @@
+     options = [
+ 
+         [None, None, None, None, Group, 'Basic Options', 'left'],
+-        [None, None, None, None, Parm, 'domain_size', None, 0, [0,sys.maxint], 'Look for structures of this size only.'],
+-        [None, None, None, None, Parm, 'start_size', None, 2, [2,sys.maxint], 'Initial (smallest) domain size.'],
+-        [None, None, None, None, Parm, 'end_size', None, -1, [-1,sys.maxint], 'Final (largest) domain size (-1 means infinity).'],
+-        # [None, None, None, None, Parm, 'iterate_up_to', None, 10, [-1,sys.maxint], 'Final domain size.'],
+-        [None, None, None, None, Parm, 'increment', None, 1, [1,sys.maxint], 'Increment for next domain size (when end_size > start_size).'],
++        [None, None, None, None, Parm, 'domain_size', None, 0, [0,utilities.INT_MAX], 'Look for structures of this size only.'],
++        [None, None, None, None, Parm, 'start_size', None, 2, [2,utilities.INT_MAX], 'Initial (smallest) domain size.'],
++        [None, None, None, None, Parm, 'end_size', None, -1, [-1,utilities.INT_MAX], 'Final (largest) domain size (-1 means infinity).'],
++        # [None, None, None, None, Parm, 'iterate_up_to', None, 10, [-1,utilities.INT_MAX], 'Final domain size.'],
++        [None, None, None, None, Parm, 'increment', None, 1, [1,utilities.INT_MAX], 'Increment for next domain size (when end_size > start_size).'],
+         [None, None, None, None, Stringparm, 'iterate', None, 'all', ['all', 'evens', 'odds', 'primes', 'nonprimes'], 'Domain sizes must satisfy this property.'],
+-        [None, None, None, None, Parm, 'max_models', None, 1, [-1,sys.maxint], 'Stop search at this number of models (-1 means no limit).'],
+-        [None, None, None, None, Parm, 'max_seconds', None, 60, [-1,sys.maxint], 'Overall time limit.'],
+-        [None, None, None, None, Parm, 'max_seconds_per', None, -1, [-1,sys.maxint], 'Time limit for each domain size.'],
++        [None, None, None, None, Parm, 'max_models', None, 1, [-1,utilities.INT_MAX], 'Stop search at this number of models (-1 means no limit).'],
++        [None, None, None, None, Parm, 'max_seconds', None, 60, [-1,utilities.INT_MAX], 'Overall time limit.'],
++        [None, None, None, None, Parm, 'max_seconds_per', None, -1, [-1,utilities.INT_MAX], 'Time limit for each domain size.'],
+         [None, None, None, None, Flag, 'prolog_style_variables', None, 0, None, 'Variables start with upper case instead of starting with u,v,w,x,y,z.'],
+ 
+ #        [None, None, None, None, Group, 'Output Options', 'left'],
+@@ -342,7 +342,7 @@
+         # [None, None, None, None, Flag, 'iterate_primes', None, 0, None, 'Search structures of prime size only.'],
+         # [None, None, None, None, Flag, 'iterate_nonprimes', None, 0, None, 'Search structures of nonprime size only.'],
+         [None, None, None, None, Flag, 'skolems_last', None, 0, None, 'Decide Skolem symbols last.'],
+-        [None, None, None, None, Parm, 'max_megs', None, 200, [-1,sys.maxint], 'Memory limit for Mace4 process (approximate).'],
++        [None, None, None, None, Parm, 'max_megs', None, 200, [-1,utilities.INT_MAX], 'Memory limit for Mace4 process (approximate).'],
+         [None, None, None, None, Flag, 'print_models', None, 1, None, 'Output models that are found.'],
+ 
+         [None, None, None, None, Group, 'Experimental Options', 'right'],
+@@ -436,13 +436,13 @@
+ 
+         ('Basic Options', 
+         [
+-        [None, None, None, None, Parm, 'max_weight', None, 100, [-sys.maxint,sys.maxint], 'Discard inferred clauses with weight greater than this.'],
+-        [None, None, None, None, Parm, 'pick_given_ratio', None, -1, [-1,sys.maxint], 'Selection by (Weight : Age) ratio  (except for hints).'],
++        [None, None, None, None, Parm, 'max_weight', None, 100, [utilities.INT_MIN,utilities.INT_MAX], 'Discard inferred clauses with weight greater than this.'],
++        [None, None, None, None, Parm, 'pick_given_ratio', None, -1, [-1,utilities.INT_MAX], 'Selection by (Weight : Age) ratio  (except for hints).'],
+         [None, None, None, None, Stringparm, 'order', None, 'lpo', ['lpo', 'rpo', 'kbo'], 'Overall term ordering: Lexicographic Path Ordering (LPO), Recursive Path Ordering (RPO), Knuth-Bendix Ordering (KBO).  If the search fails with LPO, try KBO.'],
+         [None, None, None, None, Stringparm, 'eq_defs', None, 'unfold', ['unfold', 'fold', 'pass'], 'Adjustment of term ordering, based on equational definitions in the input.\nUnfold: eliminate defined operations at the start of the search;\nFold: introduce the defined operation whenever possible;\nPass: let equational definitions be oriented by the term ordering.'],
+         [None, None, None, None, Flag, 'expand_relational_defs', None, 0, None, 'Use relational definitions in the input to immediately expand occurrences of the defined relations in the input.'],
+         [None, None, None, None, Flag, 'restrict_denials', None, 0, None, 'This flag restricts the application of inference rules when negative clauses are involved, with the goal of producing more direct (forward) proofs.  WARNING: this flag can block proofs.'],
+-        [None, None, None, None, Parm, 'max_seconds', None, 60, [-1,sys.maxint], 'Stop the search at this number of seconds (CPU, not wall clock).'],
++        [None, None, None, None, Parm, 'max_seconds', None, 60, [-1,utilities.INT_MAX], 'Stop the search at this number of seconds (CPU, not wall clock).'],
+         [None, None, None, None, Flag, 'prolog_style_variables', None, 0, None, 'Variables start with upper case instead of starting with u,v,w,x,y,z.'],
+         ]),
+ 
+@@ -469,26 +469,26 @@
+         [
+ 
+         [None, None, None, None, Group, 'Search Limits', 'left'],
+-        [None, None, None, None, Parm, 'max_given', None, -1, [-1,sys.maxint], 'Stop the search at this number of given clauses.'],
+-        [None, None, None, None, Parm, 'max_kept', None, -1, [-1,sys.maxint], 'Stop the search at this number of kept clauses.'],
+-        [None, None, None, None, Parm, 'max_proofs', None, 1, [-1,sys.maxint], 'Stop the search at this number of proofs.'],
+-        [None, None, None, None, Parm, 'max_megs', None, 200, [-1,sys.maxint], 'Stop the search when the process has used about this amount of memory.'],
+-        [None, None, None, None, Parm, 'max_seconds', None, 60, [-1,sys.maxint], 'Stop the search at this number of seconds (CPU, not wall clock).'],
+-        [None, None, None, None, Parm, 'max_minutes', None, -1, [-1,sys.maxint], ''],
+-        [None, None, None, None, Parm, 'max_hours', None, -1, [-1,sys.maxint], ''],
+-        [None, None, None, None, Parm, 'max_days', None, -1, [-1,sys.maxint], ''],
++        [None, None, None, None, Parm, 'max_given', None, -1, [-1,utilities.INT_MAX], 'Stop the search at this number of given clauses.'],
++        [None, None, None, None, Parm, 'max_kept', None, -1, [-1,utilities.INT_MAX], 'Stop the search at this number of kept clauses.'],
++        [None, None, None, None, Parm, 'max_proofs', None, 1, [-1,utilities.INT_MAX], 'Stop the search at this number of proofs.'],
++        [None, None, None, None, Parm, 'max_megs', None, 200, [-1,utilities.INT_MAX], 'Stop the search when the process has used about this amount of memory.'],
++        [None, None, None, None, Parm, 'max_seconds', None, 60, [-1,utilities.INT_MAX], 'Stop the search at this number of seconds (CPU, not wall clock).'],
++        [None, None, None, None, Parm, 'max_minutes', None, -1, [-1,utilities.INT_MAX], ''],
++        [None, None, None, None, Parm, 'max_hours', None, -1, [-1,utilities.INT_MAX], ''],
++        [None, None, None, None, Parm, 'max_days', None, -1, [-1,utilities.INT_MAX], ''],
+ 
+         [None, None, None, None, Group, 'Limits on Kept Clauses', 'right'],
+-        [None, None, None, None, Parm, 'max_weight', None, 100, [-sys.maxint,sys.maxint], 'Discard inferred clauses with weight greater than this.'],
+-        [None, None, None, None, Parm, 'max_depth', None, -1, [-1,sys.maxint], 'Discard inferred clauses with depth greater than this.'],
+-        [None, None, None, None, Parm, 'max_literals', None, -1, [-1,sys.maxint], 'Discard inferred clauses with more literals than this.'],
+-        [None, None, None, None, Parm, 'max_vars', None, -1, [-1,sys.maxint], 'Discard inferred clauses with more variables than this.'],
++        [None, None, None, None, Parm, 'max_weight', None, 100, [utilities.INT_MIN,utilities.INT_MAX], 'Discard inferred clauses with weight greater than this.'],
++        [None, None, None, None, Parm, 'max_depth', None, -1, [-1,utilities.INT_MAX], 'Discard inferred clauses with depth greater than this.'],
++        [None, None, None, None, Parm, 'max_literals', None, -1, [-1,utilities.INT_MAX], 'Discard inferred clauses with more literals than this.'],
++        [None, None, None, None, Parm, 'max_vars', None, -1, [-1,utilities.INT_MAX], 'Discard inferred clauses with more variables than this.'],
+ 
+         [None, None, None, None, Group, 'Sos Control', 'right'],
+-        [None, None, None, None, Parm, 'sos_limit', None, 20000, [-1,sys.maxint], 'Limit on the size of the SOS list (the list of clauses that have been kept, but not yet selected as given clauses).  As the SOS fills up, a heuristic is used to discards new clauses that are unlikely to be used due to this limit.'],
+-#       [None, None, None, None, Parm, 'min_sos_limit', None, 0, [0,sys.maxint], 'Unused'],
+-#       [None, None, None, None, Parm, 'lrs_interval', None, 50, [1,sys.maxint], 'Limited resource heuristic: '],
+-#       [None, None, None, None, Parm, 'lrs_ticks', None, -1, [-1,sys.maxint], 'Limited resource heuristic: '],
++        [None, None, None, None, Parm, 'sos_limit', None, 20000, [-1,utilities.INT_MAX], 'Limit on the size of the SOS list (the list of clauses that have been kept, but not yet selected as given clauses).  As the SOS fills up, a heuristic is used to discards new clauses that are unlikely to be used due to this limit.'],
++#       [None, None, None, None, Parm, 'min_sos_limit', None, 0, [0,utilities.INT_MAX], 'Unused'],
++#       [None, None, None, None, Parm, 'lrs_interval', None, 50, [1,utilities.INT_MAX], 'Limited resource heuristic: '],
++#       [None, None, None, None, Parm, 'lrs_ticks', None, -1, [-1,utilities.INT_MAX], 'Limited resource heuristic: '],
+         ]),
+ 
+         ('Search Prep', 
+@@ -498,7 +498,7 @@
+         [None, None, None, None, Flag, 'process_initial_sos', None, 1, None, 'Treat input clauses as if they were inferred; exceptions are the application of max_weight, max_level, max_vars, and max_literals.'],
+         [None, None, None, None, Flag, 'sort_initial_sos', None, 0, None, 'Sort the initial assumptions.  The order is largely  arbitrary.'],
+         [None, None, None, None, Flag, 'predicate_elim', None, 1, None, 'Try to eliminate predicate (relation) symbols before the search starts.'],
+-        [None, None, None, None, Parm, 'fold_denial_max', None, 0, [-1,sys.maxint], ''],
++        [None, None, None, None, Parm, 'fold_denial_max', None, 0, [-1,utilities.INT_MAX], ''],
+         ]),
+ 
+         ('Goals/Denials', 
+@@ -511,15 +511,15 @@
+         [
+ 
+         [None, None, None, None, Group, 'Selection Ratio', 'left'],
+-        [None, None, None, None, Parm, 'hints_part', None, sys.maxint, [0,sys.maxint], 'Component for clauses that match hint.'],
+-        [None, None, None, None, Parm, 'age_part', None, 1, [0,sys.maxint], 'Component for the oldest clauses.'],
+-        [None, None, None, None, Parm, 'weight_part', None, 0, [0,sys.maxint], 'Component for the lightest clauses.'],
+-        [None, None, None, None, Parm, 'false_part', None, 4, [0,sys.maxint], 'Component for the lightest false (w.r.t. an interpretation) clauses.'],
+-        [None, None, None, None, Parm, 'true_part', None, 4, [0,sys.maxint], 'Component for the lightest true (w.r.t. an interpretation) clauses.'],
+-        [None, None, None, None, Parm, 'random_part', None, 0, [0,sys.maxint], 'Component for random clauses.'],
++        [None, None, None, None, Parm, 'hints_part', None, utilities.INT_MAX, [0,utilities.INT_MAX], 'Component for clauses that match hint.'],
++        [None, None, None, None, Parm, 'age_part', None, 1, [0,utilities.INT_MAX], 'Component for the oldest clauses.'],
++        [None, None, None, None, Parm, 'weight_part', None, 0, [0,utilities.INT_MAX], 'Component for the lightest clauses.'],
++        [None, None, None, None, Parm, 'false_part', None, 4, [0,utilities.INT_MAX], 'Component for the lightest false (w.r.t. an interpretation) clauses.'],
++        [None, None, None, None, Parm, 'true_part', None, 4, [0,utilities.INT_MAX], 'Component for the lightest true (w.r.t. an interpretation) clauses.'],
++        [None, None, None, None, Parm, 'random_part', None, 0, [0,utilities.INT_MAX], 'Component for random clauses.'],
+ 
+         [None, None, None, None, Group, 'Meta Options', 'right'],
+-        [None, None, None, None, Parm, 'pick_given_ratio', None, -1, [-1,sys.maxint], 'Selection by (Weight : Age) ratio  (except for hints).'],
++        [None, None, None, None, Parm, 'pick_given_ratio', None, -1, [-1,utilities.INT_MAX], 'Selection by (Weight : Age) ratio  (except for hints).'],
+         [None, None, None, None, Flag, 'breadth_first', None, 0, None, 'Selection by age only (except for hints).'],
+         [None, None, None, None, Flag, 'lightest_first', None, 0, None, 'Selection by weight only (except for hints).'],
+         [None, None, None, None, Flag, 'random_given', None, 0, None, 'Random selection (except for hints).'],
+@@ -527,7 +527,7 @@
+ 
+         [None, None, None, None, Group, 'Semantic Guidance', 'left'],
+         [None, None, None, None, Stringparm, 'multiple_interps', None, 'false_in_all', ['false_in_all', 'false_in_some'], 'Semantics with multiple interpretaions: determines how clauses are marked as "false".'],
+-        [None, None, None, None, Parm, 'eval_limit', None, 1024, [-1,sys.maxint], 'Limit on the number of ground instances for evaluation in an explicit interpretation (for semantic guidance).'],
++        [None, None, None, None, Parm, 'eval_limit', None, 1024, [-1,utilities.INT_MAX], 'Limit on the number of ground instances for evaluation in an explicit interpretation (for semantic guidance).'],
+ 
+         [None, None, None, None, Group, 'Others', 'right'],
+         [None, None, None, None, Flag, 'input_sos_first', None, 1, None, 'Before starting with selection ratio, select input clauses.'],
+@@ -549,7 +549,7 @@
+         [None, None, None, None, Flag, 'paramodulation', None, 0, None, 'The inference rule for equality.'],
+ 
+         [None, None, None, None, Group, 'Other Rules', 'left'],
+-        [None, None, None, None, Parm, 'new_constants', None, 0, [-1,sys.maxint], 'If > 0, introduce new constants when equations such as x*x\'=y*y\' are derived.  The value of this parameter is a limit on the number of times the rule will be applied.'],
++        [None, None, None, None, Parm, 'new_constants', None, 0, [-1,utilities.INT_MAX], 'If > 0, introduce new constants when equations such as x*x\'=y*y\' are derived.  The value of this parameter is a limit on the number of times the rule will be applied.'],
+         [None, None, None, None, Flag, 'factor', None, 0, None, ''],
+ 
+         [None, None, None, None, Group, 'General Restrictions', 'right'],
+@@ -559,7 +559,7 @@
+         [None, None, None, None, Flag, 'ordered_res', None, 1, None, 'Resolved literals in one or more parents must be maximal in the clause.  (Does not apply to UR resolution.)'],
+         [None, None, None, None, Flag, 'check_res_instances', None, 0, None, 'The maximality checks are done after the application of the unifier for the inference.'],
+         [None, None, None, None, Flag, 'initial_nuclei', None, 0, None, 'For hyperresolution and UR resolution the nucleus for the inference must be an initial clause (this restriction can block all proofs).'],
+-        [None, None, None, None, Parm, 'ur_nucleus_limit', None, -1, [-1,sys.maxint], 'The nucleus for each UR-resolution inference can have at most this many  literals.'],
++        [None, None, None, None, Parm, 'ur_nucleus_limit', None, -1, [-1,utilities.INT_MAX], 'The nucleus for each UR-resolution inference can have at most this many  literals.'],
+ 
+         [None, None, None, None, Group, 'Paramodulation Restrictions', 'right'],
+         [None, None, None, None, Flag, 'ordered_para', None, 1, None, 'For paramodulation inferences, one or both parents must be maximal in the clause.'],
+@@ -567,20 +567,20 @@
+         [None, None, None, None, Flag, 'para_from_vars', None, 1, None, 'Paramodulation is allowed from variables (not allowing can block all proofs)..'],
+         [None, None, None, None, Flag, 'para_units_only', None, 0, None, 'Paramodulation is applied to unit clauses only (this restriction can block all proofs).'],
+ #       [None, None, None, None, Flag, 'basic_paramodulation', None, 0, None, ''],
+-        [None, None, None, None, Parm, 'para_lit_limit', None, -1, [-1,sys.maxint], 'Paramodulation is not applied to clauses with more than this number of literals (using this restriction can block all proofs).'],
++        [None, None, None, None, Parm, 'para_lit_limit', None, -1, [-1,utilities.INT_MAX], 'Paramodulation is not applied to clauses with more than this number of literals (using this restriction can block all proofs).'],
+         ]),
+ 
+         ('Rewriting', 
+         [
+ 
+         [None, None, None, None, Group, 'Term Rewriting Limits', 'left'],
+-        [None, None, None, None, Parm, 'demod_step_limit', None, 1000, [-1,sys.maxint], 'When rewriting derived clauses, apply at most this many rewrite steps.  Under most settings, rewriting is guaranteed to terminate, but it can be intractable.'],
+-        [None, None, None, None, Parm, 'demod_size_limit', None, 1000, [-1,sys.maxint], 'When rewriting derived clauses, stop if the term being rewritten has more than this many symbols.'],
++        [None, None, None, None, Parm, 'demod_step_limit', None, 1000, [-1,utilities.INT_MAX], 'When rewriting derived clauses, apply at most this many rewrite steps.  Under most settings, rewriting is guaranteed to terminate, but it can be intractable.'],
++        [None, None, None, None, Parm, 'demod_size_limit', None, 1000, [-1,utilities.INT_MAX], 'When rewriting derived clauses, stop if the term being rewritten has more than this many symbols.'],
+ 
+         [None, None, None, None, Group, 'Lex-Dependent Rewriting', 'right'],
+         [None, None, None, None, Flag, 'lex_dep_demod', None, 1, None, 'Apply non-orientable equations as rewrite rules if the instance used for the rewrite is orientable.'],
+         [None, None, None, None, Flag, 'lex_dep_demod_sane', None, 1, None, 'This is a restriction on lex_dep_demod.  A non-orientable equation can be used for rewriting only if the two sides have the same number of symbols.'],
+-        [None, None, None, None, Parm, 'lex_dep_demod_lim', None, 11, [-1,sys.maxint], 'This is a restriction on lex_dep_demod.  A non-orientable equation can be used for rewriting only if it has fewer than this number of symbols.'],
++        [None, None, None, None, Parm, 'lex_dep_demod_lim', None, 11, [-1,utilities.INT_MAX], 'This is a restriction on lex_dep_demod.  A non-orientable equation can be used for rewriting only if it has fewer than this number of symbols.'],
+         [None, None, None, None, Flag, 'lex_order_vars', None, 0, None, 'Incorporate (uninstantiated) variables into the term ordering, treating them as constants.  For example, x*y < y*x.  This cuts down the search, but it can block all proofs.'],
+ 
+         [None, None, None, None, Group, 'Others', 'left'],
+@@ -593,28 +593,28 @@
+         [
+ 
+         [None, None, None, None, Group, 'Symbol Weights', 'left'],
+-        [None, None, None, None, Parm, 'variable_weight', None, 1, [-sys.maxint,sys.maxint], 'Weight of variables .'],
+-        [None, None, None, None, Parm, 'constant_weight', None, 1, [-sys.maxint,sys.maxint], 'Default weight of constants.'],
+-        [None, None, None, None, Parm, 'not_weight', None, 0, [-sys.maxint,sys.maxint], 'Weight of the negation symbol.'],
+-        [None, None, None, None, Parm, 'or_weight', None, 0, [-sys.maxint,sys.maxint], 'Weight of the disjunction symbol.'],
+-        [None, None, None, None, Parm, 'sk_constant_weight', None, 1, [-sys.maxint,sys.maxint], 'Weight of Skolem constants.  This option can be useful, because Skolem constants cannot appear in weighting rules.'],
+-        [None, None, None, None, Parm, 'prop_atom_weight', None, 1, [-sys.maxint,sys.maxint], 'Weight of propositional atoms.'],
++        [None, None, None, None, Parm, 'variable_weight', None, 1, [utilities.INT_MIN,utilities.INT_MAX], 'Weight of variables .'],
++        [None, None, None, None, Parm, 'constant_weight', None, 1, [utilities.INT_MIN,utilities.INT_MAX], 'Default weight of constants.'],
++        [None, None, None, None, Parm, 'not_weight', None, 0, [utilities.INT_MIN,utilities.INT_MAX], 'Weight of the negation symbol.'],
++        [None, None, None, None, Parm, 'or_weight', None, 0, [utilities.INT_MIN,utilities.INT_MAX], 'Weight of the disjunction symbol.'],
++        [None, None, None, None, Parm, 'sk_constant_weight', None, 1, [utilities.INT_MIN,utilities.INT_MAX], 'Weight of Skolem constants.  This option can be useful, because Skolem constants cannot appear in weighting rules.'],
++        [None, None, None, None, Parm, 'prop_atom_weight', None, 1, [utilities.INT_MIN,utilities.INT_MAX], 'Weight of propositional atoms.'],
+ 
+         [None, None, None, None, Group, 'Penalties', 'right'],
+-        [None, None, None, None, Parm, 'skolem_penalty', None, 1, [0,sys.maxint], 'If a term contains a (non-constant) Skolem function, its weight is multiplied by this value.'],
+-        [None, None, None, None, Parm, 'nest_penalty', None, 0, [0,sys.maxint], 'For each nest of two identical function symbols, e.g., f(f(x,y),z), this value is added tot he weight of the term.'],
+-        [None, None, None, None, Parm, 'depth_penalty', None, 0, [-sys.maxint,sys.maxint], 'After the weight of clause C is calculated, its weight is increased by depth(C) * this_value.'],
+-        [None, None, None, None, Parm, 'var_penalty', None, 0, [-sys.maxint,sys.maxint], 'After the weight of clause C is calculated, its weight is increased by number_of_vars(C) * this_value.'],
++        [None, None, None, None, Parm, 'skolem_penalty', None, 1, [0,utilities.INT_MAX], 'If a term contains a (non-constant) Skolem function, its weight is multiplied by this value.'],
++        [None, None, None, None, Parm, 'nest_penalty', None, 0, [0,utilities.INT_MAX], 'For each nest of two identical function symbols, e.g., f(f(x,y),z), this value is added tot he weight of the term.'],
++        [None, None, None, None, Parm, 'depth_penalty', None, 0, [utilities.INT_MIN,utilities.INT_MAX], 'After the weight of clause C is calculated, its weight is increased by depth(C) * this_value.'],
++        [None, None, None, None, Parm, 'var_penalty', None, 0, [utilities.INT_MIN,utilities.INT_MAX], 'After the weight of clause C is calculated, its weight is increased by number_of_vars(C) * this_value.'],
+ 
+         [None, None, None, None, Group, 'Others', 'right'],
+-        [None, None, None, None, Parm, 'default_weight', None, sys.maxint, [-sys.maxint,sys.maxint], ''],
++        [None, None, None, None, Parm, 'default_weight', None, utilities.INT_MAX, [utilities.INT_MIN,utilities.INT_MAX], ''],
+         ]),
+ 
+         ('Process Inferred', 
+         [
+         [None, None, None, None, Flag, 'safe_unit_conflict', None, 0, None, 'In some cases, a proof may be missed because a newly-derived clause is deleted by a limit such as max_weight.  This flag eliminates some of those cases.'],
+         [None, None, None, None, Flag, 'back_subsume', None, 1, None, 'When a newly-derived clause C is kept, discard all old clauses that are subsumed by C.'],
+-        [None, None, None, None, Parm, 'backsub_check', None, 500, [-1,sys.maxint], 'At this number of given clauses, disable back subsumption if less than 5% of kept clauses have been back subsumed.'],
++        [None, None, None, None, Parm, 'backsub_check', None, 500, [-1,utilities.INT_MAX], 'At this number of given clauses, disable back subsumption if less than 5% of kept clauses have been back subsumed.'],
+         ]),
+ 
+         ('Input/Output', 
+@@ -631,8 +631,8 @@
+ #       [None, None, None, None, Flag, 'default_output', None, 1, None, ''],
+         [None, None, None, None, Flag, 'print_clause_properties', None, 0, None, 'When a clause is printed, show some if its syntactic properties (mostly for debugging).'],
+         [None, None, None, None, Stringparm, 'stats', None, 'lots', ['none', 'some', 'lots', 'all'], 'How many statistics should be printed at the end of the search and in "reports".'],
+-        [None, None, None, None, Parm, 'report', None, -1, [-1,sys.maxint], 'Output a statistics report every n seconds.'],
+-#       [None, None, None, None, Parm, 'report_stderr', None, -1, [-1,sys.maxint], ''],
++        [None, None, None, None, Parm, 'report', None, -1, [-1,utilities.INT_MAX], 'Output a statistics report every n seconds.'],
++#       [None, None, None, None, Parm, 'report_stderr', None, -1, [-1,utilities.INT_MAX], ''],
+         [None, None, None, None, Flag, 'prolog_style_variables', None, 0, None, 'Variables start with upper case instead of starting with u,v,w,x,y,z.'],
+         ]),
+ 
+@@ -646,7 +646,7 @@
+ 
+         ('Other Options', 
+         [
+-        [None, None, None, None, Parm, 'random_seed', None, 0, [-1,sys.maxint], 'Seed for random number generation.'],
++        [None, None, None, None, Parm, 'random_seed', None, 0, [-1,utilities.INT_MAX], 'Seed for random number generation.'],
+         ]),
+         ]
+ 
+@@ -683,7 +683,7 @@
+         (('breadth_first', True), ('false_part', 0)),
+         (('breadth_first', True), ('true_part', 0)),
+         (('breadth_first', True), ('random_part', 0)),
+-#        (('default_parts', True), ('hints_part', sys.maxint)),
++#        (('default_parts', True), ('hints_part', utilities.INT_MAX)),
+ #        (('default_parts', True), ('age_part', 1)),
+ #        (('default_parts', True), ('weight_part', 0)),
+ #        (('default_parts', True), ('false_part', 4)),
+@@ -709,7 +709,7 @@
+         (('auto_setup', False), ('eq_defs', 'pass')),
+         (('auto_limits', True), ('max_weight', 100)),
+         (('auto_limits', True), ('sos_limit', 20000)),
+-        (('auto_limits', False), ('max_weight', sys.maxint)),
++        (('auto_limits', False), ('max_weight', utilities.INT_MAX)),
+         (('auto_limits', False), ('sos_limit', -1)),
+         (('auto', True), ('auto_inference', True)),
+         (('auto', True), ('auto_setup', True)),
+@@ -743,7 +743,7 @@
+         (('raw', True), ('ordered_res', False)),
+         (('raw', True), ('ordered_para', False)),
+         (('raw', True), ('literal_selection', 'none')),
+-        (('raw', True), ('backsub_check', sys.maxint)),
++        (('raw', True), ('backsub_check', utilities.INT_MAX)),
+         (('raw', True), ('lightest_first', True)),
+         (('raw', True), ('cac_redundancy', False)),
+ 
+diff -ur p9m4-0.5.dfsg/utilities.py p9m4-0.5.dfsg.new/utilities.py
+--- p9m4-0.5.dfsg/utilities.py	2007-11-16 22:31:26.000000000 +0000
++++ p9m4-0.5.dfsg.new/utilities.py	2009-05-03 02:31:48.000000000 +0100
+@@ -17,7 +17,7 @@
+ #     Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ #
+ 
+-import re
++import re, struct
+ 
+ def grep(pattern, lines):
+     result = []
+@@ -86,5 +86,7 @@
+     str = r.sub('', str)
+     return str
+ 
++INT_MIN = -256**struct.calcsize("i")/2
++INT_MAX = 256**struct.calcsize("i")/2 - 1
+     
+         
================================================================


More information about the pld-cvs-commit mailing list