    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    }