001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.pa.generic;
004    
005    import javafe.util.*;
006    
007    /* Represents a clause (disjunction of literals) over up to 64 variables.
008       Clause represented by low bits in "stars" and "bits".
009       "stars" has a 1 in bit n if variable n is not mentioned in clause.
010       If "stars" has a 0 in bit n then variable n is mentioned in clause, and
011       its sign is given by bit n of "bits".   
012     */   
013    public class Disjunction {
014        public long stars;
015        public long bits;
016    
017        public  Disjunction(long stars, long bits) {
018            Assert.notFalse( (stars & bits) == 0 );
019            this.stars = stars;
020            this.bits = bits;
021        }
022        public Disjunction(/*@ non_null @*/ Disjunction d) {
023            this( d.stars, d.bits);
024        }
025        // Yields Disjunction for false
026        public Disjunction() {
027            this( -1L, 0L);
028        }
029        public /*@ non_null @*/ String toString() {
030            return "("+Long.toBinaryString(stars)+","+Long.toBinaryString(bits)+")";
031        }
032        public boolean equals(Object o) {
033            if( o instanceof Disjunction ) {
034                Disjunction d = (Disjunction)o;
035                return d.stars == stars && d.bits == bits;
036            } else {
037                return false;
038            }
039        }
040    }