Playing with propositional logic / first-order logic in C++ with boost::variant.

formula.cpp

#include <iostream>
#include <string>
#include <memory>
#include <set>
#include <boost/variant.hpp>
#include <format.h>

// Selection of symbols

/** A set of symbols for printing / parsing formula. */
struct Symbols { // Well, clang-format couldn't save this mess:
  const std::string true_s, false_s, not_s, and_s, or_s, xor_s, implies_s,
      iff_s;
  Symbols(std::string true_s_, std::string false_s_, std::string not_s_,
          std::string and_s_, std::string or_s_, std::string xor_s_,
          std::string implies_s_, std::string iff_s_)
      : true_s(true_s_), false_s(false_s_), not_s(not_s_), and_s(and_s_),
        or_s(or_s_), xor_s(xor_s_), implies_s(implies_s_), iff_s(iff_s_) {
  }
};

/** Simple representation of logic based on common names. */
auto const LongForm = Symbols("True", "False", "Not", "And", "Or", "Xor", "Implies", "Iff");

/** Symbolic representation of logic (except for true and false). */
auto const Symbolic = Symbols("True", "False", "¬", "∧", "∨", "⊕", "⇒", "⇔");

/** LaTeX representation of logic. */
auto const LaTeX = Symbols("T", "F", "\\lnot", "\\land", "\\lor", "\\oplus", "\\Rightarrow", "\\iff");

// Types et al. for a Formula.

struct True;
struct False;
struct Not;
struct And;
struct Or;
struct Xor;
struct Implies;
struct Iff;

/**
  A formula in propositional logic (is extended to first-order logic in fol.hh).
*/
using Formula = boost::variant<
  std::string,
  True,
  False,
  boost::recursive_wrapper<Not>,
  boost::recursive_wrapper<And>,
  boost::recursive_wrapper<Or>,
  boost::recursive_wrapper<Xor>,
  boost::recursive_wrapper<Implies>,
  boost::recursive_wrapper<Iff>>;

/** True value (top, verum, tautology). */
class True {};

/**
  False value (contradiction, bottom, falsum). Not strictly necessary as False
  is just Not(True).
*/
class False {};

/** The unary negation operator. */
class Not {
  const std::shared_ptr<Formula> p;
public:
  Not(const Formula &p_)
    : p(std::make_shared<Formula>(p_)) {
  }
  auto getFm() const -> Formula { return Formula(*p); }
};

/** Binary 'and' (conjunction) operator. */
struct And {
  const std::shared_ptr<Formula> p, q;
  And(const Formula &p_, const Formula &q_)
    : p(std::make_shared<Formula>(p_)), q(std::make_shared<Formula>(q_)) {
  }
};

/** Binary 'or' (inclusive disjunction) operator. */
struct Or {
  const std::shared_ptr<Formula> p, q;
  Or(const Formula &p_, const Formula &q_)
    : p(std::make_shared<Formula>(p_)), q(std::make_shared<Formula>(q_)) {
  }
};

/** Binary 'xor' (exclusive disjunction) operator. */
struct Xor {
  const std::shared_ptr<Formula> p, q;
  Xor(const Formula &p_, const Formula &q_)
    : p(std::make_shared<Formula>(p_)), q(std::make_shared<Formula>(q_)) {
  }
};

/**
  Binary 'implies' (implication) operator. It's worth repeating: this operator
  is weird. "A implies B" returns false only if A is true and B is false, so
  a sentence like "Obama is a vogon poet *implies* Elvis is alive" is true.
 */
struct Implies {
  const std::shared_ptr<Formula> p, q;
  Implies(const Formula &p_, const Formula &q_)
    : p(std::make_shared<Formula>(p_)), q(std::make_shared<Formula>(q_)) {
  }
};

/** Binary 'if and only if' (equivalence) operator. */
struct Iff {
  const std::shared_ptr<Formula> p, q;
  Iff(const Formula &p_, const Formula &q_)
    : p(std::make_shared<Formula>(p_)), q(std::make_shared<Formula>(q_)) {
  }
};

/** Visitor for logical negation. */
struct VisitNot : public boost::static_visitor<Formula> {
  auto operator()(const True &p) const { return False(); }
  auto operator()(const False &p) const { return True(); }
  auto operator()(const Not &n) const { return n.getFm(); }

  template <class P>
  auto operator()(const P &p) const { return Not(p); }
};

/** Visitor for conjunction. */
struct VisitAnd : public boost::static_visitor<Formula> {
  auto operator()(const True &p, const True &q) const { return True(); }
  auto operator()(const True &p, const False &q) const { return False(); }
  auto operator()(const False &p, const True &q) const { return False(); }
  auto operator()(const False &p, const False &q) const { return False(); }

  template <class P>
  auto operator()(const P &p, const True &q) const { return p; }

  template <class Q>
  auto operator()(const True &p, const Q &q) const { return q; }

  template <class P>
  auto operator()(const P &p, const False &q) const { return False(); }

  template <class Q>
  auto operator()(const False &p, const Q &q) const { return False(); }

  template <class P, class Q>
  auto operator()(const P &p, const Q &q) const { return And(p, q); }
};

/** Visitor for disjunction. */
struct VisitOr : public boost::static_visitor<Formula> {
  auto operator()(const True &p, const True &q) const { return True(); }
  auto operator()(const True &p, const False &q) const { return True(); }
  auto operator()(const False &p, const True &q) const { return True(); }
  auto operator()(const False &p, const False &q) const { return False(); }

  template <class P>
  auto operator()(const P &p, const True &q) const { return True(); }

  template <class Q>
  auto operator()(const True &p, const Q &q) const { return True(); }

  template <class P>
  auto operator()(const P &p, const False &q) const { return p; }

  template <class Q>
  auto operator()(const False &p, const Q &q) const { return q; }

  template <class P, class Q>
  auto operator()(const P &p, const Q &q) const { return Or(p, q); }
};

/** Visitor for exclusive disjunction. */
struct VisitXor : public boost::static_visitor<Formula> {
  auto operator()(const True &p, const True &q) const { return False(); }
  auto operator()(const True &p, const False &q) const { return True(); }
  auto operator()(const False &p, const True &q) const { return True(); }
  auto operator()(const False &p, const False &q) const { return False(); }

  template <class P>
  auto operator()(const P &p, const True &q) const { return Not(p); }

  template <class Q>
  auto operator()(const True &p, const Q &q) const { return Not(q); }

  template <class P>
  auto operator()(const P &p, const False &q) const { return p; }

  template <class Q>
  auto operator()(const False &p, const Q &q) const { return q; }

  template <class P, class Q>
  auto operator()(const P &p, const Q &q) const { return Xor(p, q); }
};

/** Visitor for the messed up implication. */
struct VisitImplies : public boost::static_visitor<Formula> {
  auto operator()(const True &p, const True &q) const { return True(); }
  auto operator()(const True &p, const False &q) const { return False(); }
  auto operator()(const False &p, const True &q) const { return True(); }
  auto operator()(const False &p, const False &q) const { return True(); }

  template <class P>
  auto operator()(const P &p, const True &q) const { return True(); }

  template <class Q>
  auto operator()(const True &p, const Q &q) const { return q; }

  template <class P>
  auto operator()(const P &p, const False &q) const { return Not(p); }

  template <class Q>
  auto operator()(const False &p, const Q &q) const { return True(); }

  template <class P, class Q>
  auto operator()(const P &p, const Q &q) const { return Implies(p, q); }
};

/** Visitor for equivalence. */
struct VisitIff : public boost::static_visitor<Formula> {
  auto operator()(const True &p, const True &q) const { return True(); }
  auto operator()(const True &p, const False &q) const { return False(); }
  auto operator()(const False &p, const True &q) const { return False(); }
  auto operator()(const False &p, const False &q) const { return True(); }

  template <class P>
  auto operator()(const P &p, const True &q) const { return p; }

  template <class Q>
  auto operator()(const True &p, const Q &q) const { return q; }

  template <class P>
  auto operator()(const P &p, const False &q) const { return Not(p); }

  template <class Q>
  auto operator()(const False &p, const Q &q) const { return Not(q); }

  template <class P, class Q>
  auto operator()(const P &p, const Q &q) const { return Iff(p, q); }
};

/**
  Simplify a formula without assignments to atoms.
*/
struct SimplifyFormula : public boost::static_visitor<Formula> {
  auto operator()(const Not &n) const {
    auto fm(n.getFm());
    auto p = boost::apply_visitor(SimplifyFormula(), fm);
    return boost::apply_visitor(VisitNot(), p);
  }

  auto operator()(const And &a) const {
    auto p = boost::apply_visitor(SimplifyFormula(), *a.p);
    auto q = boost::apply_visitor(SimplifyFormula(), *a.q);
    return boost::apply_visitor(VisitAnd(), p, q);
  }

  auto operator()(const Or &o) const {
    auto p = boost::apply_visitor(SimplifyFormula(), *o.p);
    auto q = boost::apply_visitor(SimplifyFormula(), *o.q);
    return boost::apply_visitor(VisitOr(), p, q);
  }

  auto operator()(const Xor &x) const {
    auto p = boost::apply_visitor(SimplifyFormula(), *x.p);
    auto q = boost::apply_visitor(SimplifyFormula(), *x.q);
    return boost::apply_visitor(VisitXor(), p, q);
  }

  auto operator()(const Implies &i) const {
    auto p = boost::apply_visitor(SimplifyFormula(), *i.p);
    auto q = boost::apply_visitor(SimplifyFormula(), *i.q);
    return boost::apply_visitor(VisitImplies(), p, q);
  }

  auto operator()(const Iff &i) const {
    auto p = boost::apply_visitor(SimplifyFormula(), *i.p);
    auto q = boost::apply_visitor(SimplifyFormula(), *i.q);
    return boost::apply_visitor(VisitIff(), p, q);
  }

  template <class P> auto
  operator()(const P &p) const { return Formula(p); }
};

/**
  Surrounds a string with parens if a condition is true, returns unmodified
  otherwise.
*/
auto surroundIf(bool b, const std::string &s) {
  return b ? fmt::format("({0})", s) : s;
}

/** Helper function to handle infix operators. */
auto showInfix(bool b, int pr, const std::string &sym, const Formula &p,
               const Formula &q) -> std::string;

/** Generates a string for formula. */
struct FormulaStr : public boost::static_visitor<std::string> {
  const int pr; // Used to decide whether to add a parenthesis.

  FormulaStr(int pr_ = 0) : pr(pr_) {
  }

  auto operator()(const std::string &s) const { return s; }

  auto operator()(const True &t) const { return Symbolic.true_s; }

  auto operator()(const False &f) const { return Symbolic.false_s; }

  auto operator()(const Not &n) const {
    auto fm(n.getFm());
    auto s0 = boost::apply_visitor(FormulaStr(pr + 1), fm);
    return surroundIf((pr > 10), fmt::format("{0} {1}", Symbolic.not_s, s0));
  }

  auto operator()(const And &a) const {
    return showInfix((pr > 8), 8, Symbolic.and_s, *a.p, *a.q);
  }

  auto operator()(const Or &o) const {
    return showInfix((pr > 6), 6, Symbolic.or_s, *o.p, *o.q);
  }

  auto operator()(const Xor &x) const {
    return showInfix((pr > 6), 6, Symbolic.xor_s, *x.p, *x.q);
  }

  auto operator()(const Implies &i) const {
    return showInfix((pr > 4), 4, Symbolic.implies_s, *i.p, *i.q);
  }

  auto operator()(const Iff &i) const {
    return showInfix((pr > 4), 4, Symbolic.iff_s, *i.p, *i.q);
  }
};

auto showInfix(bool b, int pr, const std::string &sym, const Formula &p, const Formula &q) -> std::string {
  auto s0 = boost::apply_visitor(FormulaStr(pr + 1), p);
  auto s1 = boost::apply_visitor(FormulaStr(pr), q);
  return surroundIf(b, fmt::format("{0} {1} {2}", s0, sym, s1));
}

auto operator<<(std::ostream &oss, const Formula &f) -> std::ostream& {
  oss << boost::apply_visitor(FormulaStr(), f);
  return oss;
}

/**
  Simple solver (without a mapping between atoms and values).
 */
struct SameFormula : public boost::static_visitor<bool> {
  auto operator()(const std::string &a0, const std::string &a1) const { return a0 == a1; }
  auto operator()(const True &t0, const True &t1) const { return true; }
  auto operator()(const False &f0, const False &f1) const { return true; }

  auto operator()(const Not &n0, const Not &n1) const {
    auto fm0(n0.getFm());
    auto fm1(n1.getFm());
    return boost::apply_visitor(SameFormula(), fm0, fm1);
  }

  auto operator()(const And &a0, const And &a1) const {
    auto p = boost::apply_visitor(SameFormula(), *a0.p, *a1.p);
    auto q = boost::apply_visitor(SameFormula(), *a0.q, *a1.q);
    return p && q;
  }

  auto operator()(const Or &o0, const Or &o1) const {
    auto p = boost::apply_visitor(SameFormula(), *o0.p, *o1.p);
    auto q = boost::apply_visitor(SameFormula(), *o0.q, *o1.q);
    return p && q;
  }

  auto operator()(const Xor &x0, const Xor &x1) const {
    auto p = boost::apply_visitor(SameFormula(), *x0.p, *x1.p);
    auto q = boost::apply_visitor(SameFormula(), *x0.q, *x1.q);
    return p && q;
  }

  auto operator()(const Implies &i0, const Implies &i1) const {
    auto p = boost::apply_visitor(SameFormula(), *i0.p, *i1.p);
    auto q = boost::apply_visitor(SameFormula(), *i0.q, *i1.q);
    return p && q;
  }

  auto operator()(const Iff &i0, const Iff &i1) const {
    auto p = boost::apply_visitor(SameFormula(), *i0.p, *i1.p);
    auto q = boost::apply_visitor(SameFormula(), *i0.q, *i1.q);
    return p && q;
  }

  template <class P, class Q> auto
  operator()(const P &p, const Q &q) const { return false; }
};

auto same(const Formula &fm0, const Formula &fm1) -> bool {
  return boost::apply_visitor(SameFormula(), fm0, fm1);
}

/** Get the names of all the atoms present in the formula. */
struct GatherAtoms : public boost::static_visitor<std::set<std::string>> {
  auto operator()(const std::string &s) const { return std::set<std::string>{s}; }

  auto operator()(const True &t) const { return std::set<std::string>(); }

  auto operator()(const False &f) const { return std::set<std::string>(); }

  auto operator()(const Not &n) const {
    auto fm(n.getFm());
    return boost::apply_visitor(GatherAtoms(), fm);
  }

  auto operator()(const And &x) const {
    auto s = std::set<std::string>();
    auto sp = boost::apply_visitor(GatherAtoms(), *x.p);
    auto sq = boost::apply_visitor(GatherAtoms(), *x.q);
    for (auto const &i : sp) s.insert(i);
    for (auto const &i : sq) s.insert(i);
    return s;
  }

  auto operator()(const Or &x) const {
    auto s = std::set<std::string>();
    auto sp = boost::apply_visitor(GatherAtoms(), *x.p);
    auto sq = boost::apply_visitor(GatherAtoms(), *x.q);
    for (auto const &i : sp) s.insert(i);
    for (auto const &i : sq) s.insert(i);
    return s;
  }

  auto operator()(const Xor &x) const {
    auto s = std::set<std::string>();
    auto sp = boost::apply_visitor(GatherAtoms(), *x.p);
    auto sq = boost::apply_visitor(GatherAtoms(), *x.q);
    for (auto const &i : sp) s.insert(i);
    for (auto const &i : sq) s.insert(i);
    return s;
  }

  auto operator()(const Implies &x) const {
    auto s = std::set<std::string>();
    auto sp = boost::apply_visitor(GatherAtoms(), *x.p);
    auto sq = boost::apply_visitor(GatherAtoms(), *x.q);
    for (auto const &i : sp) s.insert(i);
    for (auto const &i : sq) s.insert(i);
    return s;
  }

  auto operator()(const Iff &x) const {
    auto s = std::set<std::string>();
    auto sp = boost::apply_visitor(GatherAtoms(), *x.p);
    auto sq = boost::apply_visitor(GatherAtoms(), *x.q);
    for (auto const &i : sp) s.insert(i);
    for (auto const &i : sq) s.insert(i);
    return s;
  }
};