View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3    *
4    * All rights reserved. This program and the accompanying materials
5    * are made available under the terms of the Eclipse Public License v1.0
6    * which accompanies this distribution, and is available at
7    * http://www.eclipse.org/legal/epl-v10.html
8    *
9    * Alternatively, the contents of this file may be used under the terms of
10   * either the GNU Lesser General Public License Version 2.1 or later (the
11   * "LGPL"), in which case the provisions of the LGPL are applicable instead
12   * of those above. If you wish to allow use of your version of this file only
13   * under the terms of the LGPL, and not to allow others to use your version of
14   * this file under the terms of the EPL, indicate your decision by deleting
15   * the provisions above and replace them with the notice and other provisions
16   * required by the LGPL. If you do not delete the provisions above, a recipient
17   * may use your version of this file under the terms of the EPL or the LGPL.
18   * 
19   * Based on the original MiniSat specification from:
20   * 
21   * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22   * Sixth International Conference on Theory and Applications of Satisfiability
23   * Testing, LNCS 2919, pp 502-518, 2003.
24   *
25   * See www.minisat.se for the original solver in C++.
26   * 
27   *******************************************************************************/
28  package org.sat4j.specs;
29  
30  /**
31   * That enumeration defines the possible truth value for a variable: satisfied,
32   * falsified or unknown/undefined.
33   * 
34   * (that class moved from org.sat4j.minisat.core in earlier version of SAT4J).
35   * 
36   * @author leberre
37   * @since 2.1
38   */
39  public final class Lbool {
40  
41  	public static final Lbool FALSE = new Lbool("F");
42  	public static final Lbool TRUE = new Lbool("T");
43  	public static final Lbool UNDEFINED = new Lbool("U");
44  
45  	static {
46  		// usual boolean rules for negation
47  		FALSE.opposite = TRUE;
48  		TRUE.opposite = FALSE;
49  		UNDEFINED.opposite = UNDEFINED;
50  	}
51  
52  	private Lbool(String symbol) {
53  		this.symbol = symbol;
54  	}
55  
56  	/**
57  	 * boolean negation.
58  	 * 
59  	 * @return Boolean negation. The negation of UNDEFINED is UNDEFINED.
60  	 */
61  	public Lbool not() {
62  		return opposite;
63  	}
64  
65  	/**
66  	 * Textual representation for the truth value.
67  	 * 
68  	 * @return "T","F" or "U"
69  	 */
70  	@Override
71  	public String toString() {
72  		return symbol;
73  	}
74  
75  	/**
76  	 * The symbol representing the truth value.
77  	 */
78  	private final String symbol;
79  
80  	/**
81  	 * the opposite truth value.
82  	 */
83  	private Lbool opposite;
84  
85  }