<commit_before>// vim:filetype=cpp:textwidth=120:shiftwidth=2:softtabstop=2:expandtab
// Copyright 2014-2017 <NAME>
// Licensed under the MIT license. See LICENSE file in the project root.
//
// Basic first-order formulas without any syntactic sugar. The atomic entities
// here are clauses, and the connectives are negation, disjunction, and
// existential quantifier.
//
// NF() rectifies a formula (that is, renames variables to make sure no variable
// occurs freely and bound or bound by two different quantifiers).

#ifndef LIMBO_FORMULA_H_
#define LIMBO_FORMULA_H_

#include <cassert>

#include <algorithm>
#include <list>
#include <memory>
#include <utility>
#include <unordered_set>
#include <unordered_map>
#include <vector>

#include <limbo/clause.h>

#include <limbo/internal/iter.h>
#include <limbo/internal/intmap.h>
#include <limbo/internal/ints.h>
#include <limbo/internal/maybe.h>

namespace limbo {

class Formula {
 public:
  typedef internal::size_t size_t;
  typedef std::unique_ptr<Formula> Ref;
  struct SortOf { Symbol::Sort operator()(Term t) const { return t.sort(); } };
  typedef internal::IntMultiSet<Term, SortOf> SortedTermSet;
  typedef SortedTermSet::Bucket TermSet;
  typedef internal::IntMap<Symbol::Sort, size_t> SortCount;
  typedef unsigned int belief_level;
  enum Type { kAtomic, kNot, kOr, kExists, kKnow, kCons, kBel, kGuarantee };

  class Factory {
   public:
    Factory() = delete;
    Factory(const Factory&) = delete;
    Factory& operator=(const Factory&) = delete;
    Factory(Factory&&) = delete;
    Factory& operator=(Factory&&) = delete;

    inline static Ref Atomic(const Clause& c);
    inline static Ref Not(Ref alpha);
    inline static Ref Or(Ref lhs, Ref rhs);
    inline static Ref Exists(Term lhs, Ref rhs);
    inline static Ref Know(belief_level k, Ref alpha);
    inline static Ref Cons(belief_level k, Ref alpha);
    inline static Ref Bel(belief_level k, belief_level l, Ref alpha, Ref beta);
    inline static Ref Bel(belief_level k, belief_level l, Ref alpha, Ref beta, Ref not_alpha_or_beta);
    inline static Ref Guarantee(Ref alpha);
  };

  class Atomic;
  class Not;
  class Or;
  class Exists;
  class Know;
  class Cons;
  class Bel;
  class Guarantee;

  Formula(const Formula&) = delete;
  Formula& operator=(const Formula&) = delete;
  Formula(Formula&&) = default;
  Formula& operator=(Formula&&) = default;

  virtual ~Formula() {}

  virtual bool operator==(const Formula&) const = 0;
  bool operator!=(const Formula& that) const { return !(*this == that); }

  virtual Ref Clone() const = 0;

  Type type() const { return type_; }

  inline const Atomic&    as_atomic() const;
  inline const Not&       as_not() const;
  inline const Or&        as_or() const;
  inline const Exists&    as_exists() const;
  inline const Know&      as_know() const;
  inline const Cons&      as_cons() const;
  inline const Bel&       as_bel() const;
  inline const Guarantee& as_guarantee() const;

  const SortedTermSet& free_vars() const {
    if (!free_vars_) {
      free_vars_ = internal::Just(FreeVars());
    }
    return free_vars_.val;
  }

  virtual SortCount n_vars() const = 0;

  template<typename UnaryFunction>
  void SubstituteFree(UnaryFunction theta, Term::Factory* tf) {
    class FreeSubstitution : public ISubstitution {
     public:
      explicit FreeSubstitution(UnaryFunction func) : func_(func) {}
      internal::Maybe<Term> operator()(Term t) const override { return !bound(t) ? func_(t) : internal::Nothing; }
     private:
      UnaryFunction func_;
    };
    ISubstitute(FreeSubstitution(theta), tf);
  }

  template<typename UnaryFunction>
  void Traverse(UnaryFunction f) const {
    typedef typename internal::remove_const_ref<typename internal::arg<UnaryFunction>::template type<0>>::type arg_type;
    class Traversal : public ITraversal<arg_type> {
     public:
      explicit Traversal(UnaryFunction func) : func_(func) {}
      bool operator()(const arg_type& t) const override { return func_(t); }
     private:
      UnaryFunction func_;
    };
    ITraverse(Traversal(f));
  }

  Ref NF(Symbol::Factory* sf, Term::Factory* tf, bool distribute = true) const {
    Formula::Ref c = Clone();
    c->Rectify(sf, tf);
    c = c->Normalize(distribute);
    c = c->Flatten(0, sf, tf);
    return Ref(std::move(c));
  }

  internal::Maybe<Clause> AsUnivClause() const { return AsUnivClause(0); }

  virtual bool objective() const = 0;
  virtual bool subjective() const = 0;
  virtual bool quantified_in() const = 0;
  virtual bool trivially_valid() const = 0;
  virtual bool trivially_invalid() const = 0;

 protected:
  class ISubstitution {
   public:
    virtual ~ISubstitution() {}<commit_msg>Formula::NF() now flattens before normalizing.<commit_after>// vim:filetype=cpp:textwidth=120:shiftwidth=2:softtabstop=2:expandtab
// Copyright 2014-2017 <NAME>
// Licensed under the MIT license. See LICENSE file in the project root.
//
// Basic first-order formulas without any syntactic sugar. The atomic entities
// here are clauses, and the connectives are negation, disjunction, and
// existential quantifier.
//
// NF() rectifies a formula (that is, renames variables to make sure no variable
// occurs freely and bound or bound by two different quantifiers).

#ifndef LIMBO_FORMULA_H_
#define LIMBO_FORMULA_H_

#include <cassert>

#include <algorithm>
#include <list>
#include <memory>
#include <utility>
#include <unordered_set>
#include <unordered_map>
#include <vector>

#include <limbo/clause.h>

#include <limbo/internal/iter.h>
#include <limbo/internal/intmap.h>
#include <limbo/internal/ints.h>
#include <limbo/internal/maybe.h>

namespace limbo {

class Formula {
 public:
  typedef internal::size_t size_t;
  typedef std::unique_ptr<Formula> Ref;
  struct SortOf { Symbol::Sort operator()(Term t) const { return t.sort(); } };
  typedef internal::IntMultiSet<Term, SortOf> SortedTermSet;
  typedef SortedTermSet::Bucket TermSet;
  typedef internal::IntMap<Symbol::Sort, size_t> SortCount;
  typedef unsigned int belief_level;
  enum Type { kAtomic, kNot, kOr, kExists, kKnow, kCons, kBel, kGuarantee };

  class Factory {
   public:
    Factory() = delete;
    Factory(const Factory&) = delete;
    Factory& operator=(const Factory&) = delete;
    Factory(Factory&&) = delete;
    Factory& operator=(Factory&&) = delete;

    inline static Ref Atomic(const Clause& c);
    inline static Ref Not(Ref alpha);
    inline static Ref Or(Ref lhs, Ref rhs);
    inline static Ref Exists(Term lhs, Ref rhs);
    inline static Ref Know(belief_level k, Ref alpha);
    inline static Ref Cons(belief_level k, Ref alpha);
    inline static Ref Bel(belief_level k, belief_level l, Ref alpha, Ref beta);
    inline static Ref Bel(belief_level k, belief_level l, Ref alpha, Ref beta, Ref not_alpha_or_beta);
    inline static Ref Guarantee(Ref alpha);
  };

  class Atomic;
  class Not;
  class Or;
  class Exists;
  class Know;
  class Cons;
  class Bel;
  class Guarantee;

  Formula(const Formula&) = delete;
  Formula& operator=(const Formula&) = delete;
  Formula(Formula&&) = default;
  Formula& operator=(Formula&&) = default;

  virtual ~Formula() {}

  virtual bool operator==(const Formula&) const = 0;
  bool operator!=(const Formula& that) const { return !(*this == that); }

  virtual Ref Clone() const = 0;

  Type type() const { return type_; }

  inline const Atomic&    as_atomic() const;
  inline const Not&       as_not() const;
  inline const Or&        as_or() const;
  inline const Exists&    as_exists() const;
  inline const Know&      as_know() const;
  inline const Cons&      as_cons() const;
  inline const Bel&       as_bel() const;
  inline const Guarantee& as_guarantee() const;

  const SortedTermSet& free_vars() const {
    if (!free_vars_) {
      free_vars_ = internal::Just(FreeVars());
    }
    return free_vars_.val;
  }

  virtual SortCount n_vars() const = 0;

  template<typename UnaryFunction>
  void SubstituteFree(UnaryFunction theta, Term::Factory* tf) {
    class FreeSubstitution : public ISubstitution {
     public:
      explicit FreeSubstitution(UnaryFunction func) : func_(func) {}
      internal::Maybe<Term> operator()(Term t) const override { return !bound(t) ? func_(t) : internal::Nothing; }
     private:
      UnaryFunction func_;
    };
    ISubstitute(FreeSubstitution(theta), tf);
  }

  template<typename UnaryFunction>
  void Traverse(UnaryFunction f) const {
    typedef typename internal::remove_const_ref<typename internal::arg<UnaryFunction>::template type<0>>::type arg_type;
    class Traversal : public ITraversal<arg_type> {
     public:
      explicit Traversal(UnaryFunction func) : func_(func) {}
      bool operator()(const arg_type& t) const override { return func_(t); }
     private:
      UnaryFunction func_;
    };
    ITraverse(Traversal(f));
  }

  Ref NF(Symbol::Factory* sf, Term::Factory* tf, bool distribute = true) const {
    Formula::Ref c = Clone();
    c->Rectify(sf, tf);
    c = c->Flatten(0, sf, tf);
    c = c->Normalize(distribute);
    return Ref(std::move(c));
  }

  internal::Maybe<Clause> AsUnivClause() const { return AsUnivClause(0); }

  virtual bool objective() const = 0;
  virtual bool subjective() const = 0;
  virtual bool quantified_in() const = 0;
  virtual bool trivially_valid() const = 0;
  virtual bool trivially_invalid() const = 0;

 protected:
  class ISubstitution {
   public:
    virtual ~ISubstitution() {}
{'fraction_non_alphanumeric': 0.11565779709530372, 'fraction_numerical': 0.005088519028940952, 'mean_word_length': 4.0665950590762625, 'pattern_counts': {'":': 0, '<': 53, '<?xml version=': 0, '>': 59, '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': '3351195', 'n_tokens_mistral': 3040, 'n_tokens_neox': 2914, 'n_words': 906}