@@ -46,21 +46,21 @@ public class Clause {
4646 //
4747 private static StandardizeApartIndexical _saIndexical = StandardizeApartIndexicalFactory
4848 .newStandardizeApartIndexical ('c' );
49+ private static Unifier _unifier = new Unifier ();
50+ private static SubstVisitor _substVisitor = new SubstVisitor ();
51+ private static VariableCollector _variableCollector = new VariableCollector ();
52+ private static StandardizeApart _standardizeApart = new StandardizeApart ();
53+ private static LiteralsSorter _literalSorter = new LiteralsSorter ();
4954 //
5055 private final Set <Literal > literals = new LinkedHashSet <Literal >();
5156 private final List <Literal > positiveLiterals = new ArrayList <Literal >();
5257 private final List <Literal > negativeLiterals = new ArrayList <Literal >();
5358 private boolean immutable = false ;
5459 private boolean saCheckRequired = true ;
5560 private String equalityIdentity = "" ;
56- private Unifier unifier = new Unifier ();
57- private SubstVisitor substVisitor = new SubstVisitor ();
58- private VariableCollector variableCollector = new VariableCollector ();
59- private StandardizeApart standardizeApart = new StandardizeApart ();
60- private LiteralsSorter literalSorter = new LiteralsSorter ();
6161 private Set <Clause > factors = null ;
6262 private Set <Clause > nonTrivialFactors = null ;
63- private String stringRep = "{}" ;
63+ private String stringRep = null ;
6464 private ProofStep proofStep = null ;
6565
6666 public Clause () {
@@ -276,7 +276,7 @@ public Set<Clause> binaryResolvents(Clause othC) {
276276 for (Literal pl : trPosLits ) {
277277 for (Literal nl : trNegLits ) {
278278 Map <Variable , Term > copyRBindings = new LinkedHashMap <Variable , Term >();
279- if (null != unifier .unify (pl .getAtomicSentence (), nl
279+ if (null != _unifier .unify (pl .getAtomicSentence (), nl
280280 .getAtomicSentence (), copyRBindings )) {
281281 copyRPosLits .clear ();
282282 copyRNegLits .clear ();
@@ -286,7 +286,7 @@ public Set<Clause> binaryResolvents(Clause othC) {
286286 found = true ;
287287 continue ;
288288 }
289- copyRPosLits .add (substVisitor .subst (
289+ copyRPosLits .add (_substVisitor .subst (
290290 copyRBindings , l ));
291291 }
292292 found = false ;
@@ -295,11 +295,11 @@ public Set<Clause> binaryResolvents(Clause othC) {
295295 found = true ;
296296 continue ;
297297 }
298- copyRNegLits .add (substVisitor .subst (
298+ copyRNegLits .add (_substVisitor .subst (
299299 copyRBindings , l ));
300300 }
301301 // Ensure the resolvents are standardized apart
302- Map <Variable , Term > renameSubstitituon = standardizeApart
302+ Map <Variable , Term > renameSubstitituon = _standardizeApart
303303 .standardizeApart (copyRPosLits ,
304304 copyRNegLits , _saIndexical );
305305 Clause c = new Clause (copyRPosLits , copyRNegLits );
@@ -321,6 +321,12 @@ public Set<Clause> binaryResolvents(Clause othC) {
321321 }
322322
323323 public String toString () {
324+ if (null == stringRep ) {
325+ List <Literal > sortedLiterals = new ArrayList <Literal >(literals );
326+ Collections .sort (sortedLiterals , _literalSorter );
327+
328+ stringRep = sortedLiterals .toString ();
329+ }
324330 return stringRep ;
325331 }
326332
@@ -352,7 +358,7 @@ private void recalculateIdentity() {
352358 // Sort the literals first based on negation, atomic sentence,
353359 // constant, function and variable.
354360 List <Literal > sortedLiterals = new ArrayList <Literal >(literals );
355- Collections .sort (sortedLiterals , literalSorter );
361+ Collections .sort (sortedLiterals , _literalSorter );
356362
357363 stringRep = sortedLiterals .toString ();
358364
@@ -362,7 +368,7 @@ private void recalculateIdentity() {
362368 // the # of unique variables they contain and
363369 // there positions across the clauses
364370 ClauseEqualityIdentityConstructor ceic = new ClauseEqualityIdentityConstructor (
365- sortedLiterals , literalSorter );
371+ sortedLiterals , _literalSorter );
366372
367373 equalityIdentity = ceic .getIdentity ();
368374
@@ -371,6 +377,9 @@ private void recalculateIdentity() {
371377 // access lazily.
372378 factors = null ;
373379 nonTrivialFactors = null ;
380+ // Reset the objects string representation
381+ // until it is requested for.
382+ stringRep = null ;
374383 }
375384 }
376385
@@ -393,31 +402,35 @@ private void calculateFactors(Set<Clause> parentFactors) {
393402 Literal litY = lits .get (y );
394403
395404 theta .clear ();
396- Map <Variable , Term > substitution = unifier .unify (litX
405+ Map <Variable , Term > substitution = _unifier .unify (litX
397406 .getAtomicSentence (), litY .getAtomicSentence (),
398407 theta );
399408 if (null != substitution ) {
400409 List <Literal > posLits = new ArrayList <Literal >();
401410 List <Literal > negLits = new ArrayList <Literal >();
402411 if (i == 0 ) {
403- posLits .add (substVisitor .subst (substitution , litX ));
412+ posLits
413+ .add (_substVisitor
414+ .subst (substitution , litX ));
404415 } else {
405- negLits .add (substVisitor .subst (substitution , litX ));
416+ negLits
417+ .add (_substVisitor
418+ .subst (substitution , litX ));
406419 }
407420 for (Literal pl : positiveLiterals ) {
408421 if (pl == litX || pl == litY ) {
409422 continue ;
410423 }
411- posLits .add (substVisitor .subst (substitution , pl ));
424+ posLits .add (_substVisitor .subst (substitution , pl ));
412425 }
413426 for (Literal nl : negativeLiterals ) {
414427 if (nl == litX || nl == litY ) {
415428 continue ;
416429 }
417- negLits .add (substVisitor .subst (substitution , nl ));
430+ negLits .add (_substVisitor .subst (substitution , nl ));
418431 }
419432 // Ensure the non trivial factor is standardized apart
420- standardizeApart .standardizeApart (posLits , negLits ,
433+ _standardizeApart .standardizeApart (posLits , negLits ,
421434 _saIndexical );
422435 Clause c = new Clause (posLits , negLits );
423436 c .setProofStep (new ProofStepClauseFactor (c , this ));
@@ -457,17 +470,17 @@ private Clause saIfRequired(Clause othClause) {
457470 // then need to standardize apart in
458471 // order to work correctly.
459472 if (isStandardizedApartCheckRequired () || this == othClause ) {
460- Set <Variable > mVariables = variableCollector
473+ Set <Variable > mVariables = _variableCollector
461474 .collectAllVariables (this );
462- Set <Variable > oVariables = variableCollector
475+ Set <Variable > oVariables = _variableCollector
463476 .collectAllVariables (othClause );
464477
465478 Set <Variable > cVariables = new HashSet <Variable >();
466479 cVariables .addAll (mVariables );
467480 cVariables .addAll (oVariables );
468481
469482 if (cVariables .size () < (mVariables .size () + oVariables .size ())) {
470- othClause = standardizeApart .standardizeApart (othClause ,
483+ othClause = _standardizeApart .standardizeApart (othClause ,
471484 _saIndexical );
472485 }
473486 }
0 commit comments