<commit_before>/* Copyright (c) 2010, <NAME> <<EMAIL>>
 * All rights reserved.
 *
 * This software is open-source under the BSD license; see "license.txt"
 * for a description.
 */
package modalLogic.tableau;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Comparator;
import java.util.Iterator;
import java.util.List;
import modalLogic.formula.Formula;
import org.apache.commons.collections15.iterators.IteratorChain;
import util.Pair;

/**
 * The currently investigated branch of the tableau.
 * 
 * @author <NAME> <<EMAIL>>
 */
public class Branch<P> {

  private Tableau<P> tableau;
  private Comparator<P> propositionComparator;
  private List<LabelledFormula<P>> unexpanded;

  /**
   * Constructor of class Branch.
   *
   * @param tableau the tableau
   * @param propositionComparator a comparator for propositions
   */
  public Branch(Tableau<P> tableau, Comparator<P> propositionComparator) {
    this.tableau = tableau;
    this.propositionComparator = propositionComparator;
    unexpanded = new ArrayList<LabelledFormula<P>>();
  }

  /**
   * Returns a list of unexpanded subformulas.
   *
   * @return a list of unexpanded subformulas
   */
  public List<LabelledFormula<P>> getUnexpanded() {
    return unexpanded;
  }

  /**
   * Clears the list of unexpanded subformulas.
   */
  public void clear() {
    unexpanded.clear();
  }

  /**
   * Add a subformula to the branch.
   *
   * @param f the subformula
   */
  public void add(LabelledFormula<P> f) {
    if (f.getFormula().getType() == Formula.LITERAL) {
      f.getWorld().addLiteral(f);
    }
    unexpanded.add(f);
  }

  /**
   * Returns an iterator over all clashes in the branch.
   *
   * @return the iterator
   */
  public Iterator<Pair<LabelledFormula<P>>> clashes() {
    IteratorChain<Pair<LabelledFormula<P>>> ites = new IteratorChain<Pair<LabelledFormula<P>>>();
    for(World<P> w : tableau.getWorlds()) {
      if(w.isClashing())
        ites.addIterator(w.clashes());
    }
    return ites;
  }

  /**
   * Add subformula to the unexpanded ones.
   *
   * @param lf the subformula
   */
  public void unexpand(LabelledFormula<P> lf) {
    unexpanded.add(lf);
  }

  /**
   * Return the last unexpanded formula.
   * 
   * @return the last unexpanded formula
   */
  public LabelledFormula<P> unexpanded() {
    if(unexpanded.isEmpty()) {
      return null;
    }
    return unexpanded.remove(unexpanded.size()-1);
  }

  /**
   * Remove subformula from current branch and world.
   *
   * @param lf the subformula
   */
  public void remove(LabelledFormula<P> lf) {
    unexpanded.remove(lf);
    lf.getWorld().removeLiteral(lf);
  }

  /**
   * Remove all subformulas of given collection.
   *
   * @param lfs the subformulas
   */
  public void removeAll(Collection<LabelledFormula<P>> lfs) {
    for (LabelledFormula<P> lf : lfs) {
      remove(lf);
    }
  }

  /**
   * Return number of unexpanded subformulas.
   *<commit_msg>Minor fix for backtracking non-literal disjuncts<commit_after>/* Copyright (c) 2010, <NAME> <<EMAIL>>
 * All rights reserved.
 *
 * This software is open-source under the BSD license; see "license.txt"
 * for a description.
 */
package modalLogic.tableau;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Comparator;
import java.util.Iterator;
import java.util.List;
import modalLogic.formula.Formula;
import modalLogic.formula.Literal;
import org.apache.commons.collections15.iterators.IteratorChain;
import util.Pair;

/**
 * The currently investigated branch of the tableau.
 * 
 * @author <NAME> <<EMAIL>>
 */
public class Branch<P> {

  private Tableau<P> tableau;
  private Comparator<P> propositionComparator;
  private List<LabelledFormula<P>> unexpanded;

  /**
   * Constructor of class Branch.
   *
   * @param tableau the tableau
   * @param propositionComparator a comparator for propositions
   */
  public Branch(Tableau<P> tableau, Comparator<P> propositionComparator) {
    this.tableau = tableau;
    this.propositionComparator = propositionComparator;
    unexpanded = new ArrayList<LabelledFormula<P>>();
  }

  /**
   * Returns a list of unexpanded subformulas.
   *
   * @return a list of unexpanded subformulas
   */
  public List<LabelledFormula<P>> getUnexpanded() {
    return unexpanded;
  }

  /**
   * Clears the list of unexpanded subformulas.
   */
  public void clear() {
    unexpanded.clear();
  }

  /**
   * Add a subformula to the branch.
   *
   * @param f the subformula
   */
  public void add(LabelledFormula<P> f) {
    if (f.getFormula().getType() == Formula.LITERAL) {
      f.getWorld().addLiteral(f);
    }
    unexpanded.add(f);
  }

  /**
   * Returns an iterator over all clashes in the branch.
   *
   * @return the iterator
   */
  public Iterator<Pair<LabelledFormula<P>>> clashes() {
    IteratorChain<Pair<LabelledFormula<P>>> ites = new IteratorChain<Pair<LabelledFormula<P>>>();
    for(World<P> w : tableau.getWorlds()) {
      if(w.isClashing())
        ites.addIterator(w.clashes());
    }
    return ites;
  }

  /**
   * Add subformula to the unexpanded ones.
   *
   * @param lf the subformula
   */
  public void unexpand(LabelledFormula<P> lf) {
    unexpanded.add(lf);
  }

  /**
   * Return the last unexpanded formula.
   * 
   * @return the last unexpanded formula
   */
  public LabelledFormula<P> unexpanded() {
    if(unexpanded.isEmpty()) {
      return null;
    }
    return unexpanded.remove(unexpanded.size()-1);
  }

  /**
   * Remove subformula from current branch and world.
   *
   * @param lf the subformula
   */
  public void remove(LabelledFormula<P> lf) {
    unexpanded.remove(lf);
    if(lf.getFormula() instanceof Literal)
      lf.getWorld().removeLiteral(lf);
  }

  /**
   * Remove all subformulas of given collection.
   *
   * @param lfs the subformulas
   */
  public void removeAll(Collection<LabelledFormula<P>> lfs) {
    for (LabelledFormula<P> lf : lfs) {
      remove(lf);
    }
  }

  /**
   * Return number of unexpanded subformulas.
   *
{'fraction_non_alphanumeric': 0.12315107196277214, 'fraction_numerical': 0.00232674090078112, 'mean_word_length': 3.1704781704781704, 'pattern_counts': {'":': 0, '<': 71, '<?xml version=': 0, '>': 71, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4662130', 'n_tokens_mistral': 2074, 'n_tokens_neox': 1992, 'n_words': 478}