code: ///////////////////////////////////////////////////////////////////////////
  //                   __                _      _   ________               //
  //                  / /   ____  ____ _(_)____/ | / / ____/               //
  //                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
  //                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
  //               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
  //                           /____/                                      //
  //                                                                       //
  //               The Next Generation Logic Library                       //
  //                                                                       //
  ///////////////////////////////////////////////////////////////////////////
  //                                                                       //
  //  Copyright 2015-20xx Christoph Zengler                                //
  //                                                                       //
  //  Licensed under the Apache License, Version 2.0 (the "License");      //
  //  you may not use this file except in compliance with the License.     //
  //  You may obtain a copy of the License at                              //
  //                                                                       //
  //  http://www.apache.org/licenses/LICENSE-2.0                           //
  //                                                                       //
  //  Unless required by applicable law or agreed to in writing, software  //
  //  distributed under the License is distributed on an "AS IS" BASIS,    //
  //  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or      //
  //  implied.  See the License for the specific language governing        //
  //  permissions and limitations under the License.                       //
  //                                                                       //
  ///////////////////////////////////////////////////////////////////////////
  
  package org.logicng.formulas;
  
  import static org.assertj.core.api.Assertions.assertThat;
  import static org.logicng.formulas.cache.PredicateCacheEntry.IS_CNF;
  import static org.logicng.formulas.cache.PredicateCacheEntry.IS_DNF;
  import static org.logicng.formulas.cache.TransformationCacheEntry.FACTORIZED_CNF;
  
  import org.junit.jupiter.api.Test;
  import org.logicng.datastructures.Tristate;
  import org.logicng.formulas.cache.CacheEntry;
  import org.logicng.io.parsers.ParserException;
  import org.logicng.transformations.cnf.BDDCNFTransformation;
  
  import java.util.Arrays;
  
  /**
   * Test some common formula functionality.
   * @version 2.0.0
   * @since 1.0
   */
  public class FormulaTest {
  
      private enum MyOwnCacheKey implements CacheEntry {
          MYKEY1("My Key 1"),
          MYKEY2("My Key 2");
  
          private final String description;
  
          MyOwnCacheKey(final String description) {
              this.description = description;
          }
  
          @Override
          public String description() {
              return "MyOwnCacheKey{description=" + this.description + "}";
          }
      }
  
      @Test
      public void testStringContains() {
          final FormulaFactory f = new FormulaFactory();
          final Formula formula = f.not(f.and(f.variable("a"), f.variable("b")));
          assertThat(formula.containsVariable("a")).isTrue();
          assertThat(formula.containsVariable("b")).isTrue();
          assertThat(formula.containsVariable("x")).isFalse();
          assertThat(formula.containsVariable("y")).isFalse();
      }
  
      @Test
      public void testTransformationCache() {
          final FormulaFactory f = new FormulaFactory();
          final Formula formula = f.not(f.and(f.variable("a"), f.variable("b")));
          formula.setTransformationCacheEntry(FACTORIZED_CNF, f.or(f.literal("a", false), f.literal("b", false)));
          assertThat(formula.transformationCacheEntry(FACTORIZED_CNF)).isEqualTo(f.or(f.literal("a", false), f.literal("b", false)));
      }
  
      @Test
      public void testPredicateCache() {
          final FormulaFactory f = new FormulaFactory();
          final Formula formula = f.not(f.and(f.variable("a"), f.variable("b")));
          formula.setPredicateCacheEntry(IS_CNF, false);
          formula.setPredicateCacheEntry(IS_DNF, Tristate.UNDEF);
          assertThat(formula.predicateCacheEntry(IS_CNF)).isEqualTo(Tristate.FALSE);
          assertThat(formula.predicateCacheEntry(IS_DNF)).isEqualTo(Tristate.UNDEF);
      }
  
      @Test
      public void testFunctionCache() {
          final FormulaFactory f = new FormulaFactory();
          final Formula formula = f.not(f.and(f.variable("a"), f.variable("b")));
          formula.setFunctionCacheEntry(MyOwnCacheKey.MYKEY1, "key1");
          formula.setFunctionCacheEntry(MyOwnCacheKey.MYKEY2, "key2");
          assertThat(MyOwnCacheKey.MYKEY1.description).isEqualTo("My Key 1");
          assertThat(formula.functionCacheEntry(MyOwnCacheKey.MYKEY1)).isEqualTo("key1");
          assertThat(formula.functionCacheEntry(MyOwnCacheKey.MYKEY2)).isEqualTo("key2");
      }
  
      @Test
      public void testFType() {
          assertThat(FType.valueOf("AND")).isEqualTo(FType.AND);
          assertThat(Arrays.asList(FType.values()).contains(FType.valueOf("PBC"))).isTrue();
          assertThat(FType.values().length).isEqualTo(9);
      }
  
      @Test
      public void testCType() {
          assertThat(CType.valueOf("EQ")).isEqualTo(CType.EQ);
          assertThat(CType.valueOf("LE")).isEqualTo(CType.LE);
          assertThat(Arrays.asList(CType.values()).contains(CType.valueOf("GT"))).isTrue();
          assertThat(CType.values().length).isEqualTo(5);
      }
  
      @Test
      public void testIsSatisfiable() throws ParserException {
          final FormulaFactory f = new FormulaFactory();
          final Formula f1 = f.parse("(a | b) & (c | ~d)");
          final Formula f2 = f.parse("~a & ~b & (a | b)");
          assertThat(f.falsum().isSatisfiable()).isFalse();
          assertThat(f.verum().isSatisfiable()).isTrue();
          assertThat(f1.isSatisfiable()).isTrue();
          assertThat(f2.isSatisfiable()).isFalse();
      }
  
      @Test
      public void testIsTautology() throws ParserException {
          final FormulaFactory f = new FormulaFactory();
          final Formula f1 = f.parse("(a | b) & (c | ~d)");
          final Formula f2 = f.parse("(a & b) | (~a & b) | (a & ~b) | (~a & ~b)");
          assertThat(f.falsum().isTautology()).isFalse();
          assertThat(f.verum().isTautology()).isTrue();
          assertThat(f1.isTautology()).isFalse();
          assertThat(f2.isTautology()).isTrue();
      }
  
      @Test
      public void testIsContradiction() throws ParserException {
          final FormulaFactory f = new FormulaFactory();
          final Formula f1 = f.parse("(a | b) & (c | ~d)");
          final Formula f2 = f.parse("~a & ~b & (a | b)");
          assertThat(f.falsum().isContradiction()).isTrue();
          assertThat(f.verum().isContradiction()).isFalse();
          assertThat(f1.isContradiction()).isFalse();
          assertThat(f2.isContradiction()).isTrue();
      }
  
      @Test
      public void testImplies() throws ParserException {
          final FormulaFactory f = new FormulaFactory();
          final Formula f1 = f.parse("(a | b) & (c | ~d)");
          final Formula f2 = f.parse("(a | b) & (c | ~d) & (e | ~f)");
          final Formula f3 = f.parse("(a | b) & (c | d)");
          assertThat(f1.implies(f2)).isFalse();
          assertThat(f2.implies(f1)).isTrue();
          assertThat(f1.implies(f3)).isFalse();
          assertThat(f2.implies(f3)).isFalse();
          assertThat(f2.implies(f2)).isTrue();
      }
  
      @Test
      public void testIsImpliedBy() throws ParserException {
          final FormulaFactory f = new FormulaFactory();
          final Formula f1 = f.parse("(a | b) & (c | ~d)");
          final Formula f2 = f.parse("(a | b) & (c | ~d) & (e | ~f)");
          final Formula f3 = f.parse("(a | b) & (c | d)");
          assertThat(f1.isImpliedBy(f2)).isTrue();
          assertThat(f2.isImpliedBy(f1)).isFalse();
          assertThat(f1.isImpliedBy(f3)).isFalse();
          assertThat(f2.isImpliedBy(f3)).isFalse();
          assertThat(f2.isImpliedBy(f2)).isTrue();
      }
  
      @Test
      public void testIsEquivalentTo() throws ParserException {
          final FormulaFactory f = new FormulaFactory();
          final Formula f1 = f.parse("(a | b) & (c | ~d)");
          final Formula f2 = f.parse("(a | b) & (c | ~d) & (e | ~f)");
          final Formula f3 = f.parse("(a & c) | (a & ~d) | (b & c) | (b & ~d)");
          assertThat(f1.isEquivalentTo(f2)).isFalse();
          assertThat(f2.isEquivalentTo(f1)).isFalse();
          assertThat(f1.isEquivalentTo(f3)).isTrue();
          assertThat(f3.isEquivalentTo(f1)).isTrue();
          assertThat(f2.isEquivalentTo(f3)).isFalse();
          assertThat(f2.isEquivalentTo(f2.transform(new BDDCNFTransformation()))).isTrue();
      }
  }
  