title: Convert logic formula to conjunctive normal form in C++
body: <p>I'm going to implement a CNF generator in C++, using Boots/Spirit. but after finish "the order of precedence" and "eliminating equivalences &amp; implications" these two parts, I can't figure out how to implement "move NOTs inwards" and "distribute ORs inwards over ANDs". </p>
  
  <p>Desired output is documented here:
  <a href="https://en.wikipedia.org/wiki/Conjunctive_normal_form" rel="nofollow">https://en.wikipedia.org/wiki/Conjunctive_normal_form</a></p>
  
  <p>Here are more detail description below:</p>
  
  <p>The order of precedence:</p>
  
  <pre><code>NOT &gt; AND &gt; OR &gt; IMP &gt; IFF
  </code></pre>
  
  <p>Input example:</p>
  
  <pre><code>A iff B imp C
  </code></pre>
  
  <p>Now the output is:</p>
  
  <pre><code>(A or not ( not B or C)) and ( not A or ( not B or C))
  </code></pre>
  
  <p>And the code( I implement output at printer part ):</p>
  
  <pre><code>#include &lt;boost/spirit/include/qi.hpp&gt;
  #include &lt;boost/spirit/include/phoenix.hpp&gt;
  #include &lt;boost/spirit/include/phoenix_operator.hpp&gt;
  #include &lt;boost/variant/recursive_wrapper.hpp&gt;
  
  namespace qi    = boost::spirit::qi;
  namespace phx   = boost::phoenix;
  
  
  
  // Abstract data type
  
  struct op_or  {};
  struct op_and {};
  struct op_imp {};
  struct op_iff {};
  struct op_not {};
  
  typedef std::string var;
  template &lt;typename tag&gt; struct binop;
  template &lt;typename tag&gt; struct unop;
  
  typedef boost::variant&lt;var,
          boost::recursive_wrapper&lt;unop &lt;op_not&gt; &gt;,
          boost::recursive_wrapper&lt;binop&lt;op_and&gt; &gt;,
          boost::recursive_wrapper&lt;binop&lt;op_or&gt; &gt;,
          boost::recursive_wrapper&lt;binop&lt;op_imp&gt; &gt;,
          boost::recursive_wrapper&lt;binop&lt;op_iff&gt; &gt;
          &gt; expr;
  
  template &lt;typename tag&gt; struct binop
  {
    explicit binop(const expr&amp; l, const expr&amp; r) : oper1(l), oper2(r) { }
    expr oper1, oper2;
  };
  
  template &lt;typename tag&gt; struct unop
  {
    explicit unop(const expr&amp; o) : oper1(o) { }
    expr oper1;
  };
  
  
  
  // Operating on the syntax tree
  
  struct printer : boost::static_visitor&lt;void&gt;
  {
    printer(std::ostream&amp; os) : _os(os) {}
    std::ostream&amp; _os;
  
    //
    void operator()(const var&amp; v) const { _os &lt;&lt; v; }
  
    void operator()(const binop&lt;op_and&gt;&amp; b) const { print(" and ", b.oper1, b.oper2); }
    void operator()(const binop&lt;op_or &gt;&amp; b) const { print(" or ", b.oper1, b.oper2); }
    void operator()(const binop&lt;op_iff&gt;&amp; b) const { eliminate_iff(b.oper1, b.oper2); }
    void operator()(const binop&lt;op_imp&gt;&amp; b) const { eliminate_imp(b.oper1, b.oper2); }
  
    void print(const std::string&amp; op, const expr&amp; l, const expr&amp; r) const
    {
      _os &lt;&lt; "(";
      boost::apply_visitor(*this, l);
      _os &lt;&lt; op;
      boost::apply_visitor(*this, r);
      _os &lt;&lt; ")";
    }
  
    void operator()(const unop&lt;op_not&gt;&amp; u) const
    {
      _os &lt;&lt; "( not ";
      boost::apply_visitor(*this, u.oper1);
      _os &lt;&lt; ")";
    }
  
    void eliminate_iff(const expr&amp; l, const expr&amp; r) const
    {
      _os &lt;&lt; "(";
      boost::apply_visitor(*this, l);
      _os &lt;&lt; " or not ";
      boost::apply_visitor(*this, r);
      _os &lt;&lt; ") and ( not ";
      boost::apply_visitor(*this, l);
      _os &lt;&lt; " or ";
      boost::apply_visitor(*this, r);
      _os &lt;&lt; ")";
    }
  
    void eliminate_imp(const expr&amp; l, const expr&amp; r) const
    {
      _os &lt;&lt; "( not ";
      boost::apply_visitor(*this, l);
      _os &lt;&lt; " or ";
      boost::apply_visitor(*this, r);
      _os &lt;&lt; ")";
    }
  };
  
  std::ostream&amp; operator&lt;&lt;(std::ostream&amp; os, const expr&amp; e)
  { boost::apply_visitor(printer(os), e); return os; }
  
  
  
  // Grammar rules
  
  template &lt;typename It, typename Skipper = qi::space_type&gt;
  struct parser : qi::grammar&lt;It, expr(), Skipper&gt;
  {
    parser() : parser::base_type(expr_)
    {
      using namespace qi;
  
      expr_  = iff_.alias();
  
      iff_ = (imp_ &gt;&gt; "iff" &gt;&gt; iff_) [ _val = phx::construct&lt;binop&lt;op_iff&gt;&gt;(_1, _2) ] | imp_   [ _val = _1 ];
      imp_ = (or_  &gt;&gt; "imp" &gt;&gt; imp_) [ _val = phx::construct&lt;binop&lt;op_imp&gt;&gt;(_1, _2) ] | or_    [ _val = _1 ];
      or_  = (and_ &gt;&gt; "or"  &gt;&gt; or_ ) [ _val = phx::construct&lt;binop&lt;op_or &gt;&gt;(_1, _2) ] | and_   [ _val = _1 ];
      and_ = (not_ &gt;&gt; "and" &gt;&gt; and_) [ _val = phx::construct&lt;binop&lt;op_and&gt;&gt;(_1, _2) ] | not_   [ _val = _1 ];
      not_ = ("not" &gt; simple       ) [ _val = phx::construct&lt;unop &lt;op_not&gt;&gt;(_1)     ] | simple [ _val = _1 ];
  
      simple = (('(' &gt; expr_ &gt; ')') | var_);
      var_ = qi::lexeme[ +alpha ];
  
      BOOST_SPIRIT_DEBUG_NODE(expr_);
      BOOST_SPIRIT_DEBUG_NODE(iff_);
      BOOST_SPIRIT_DEBUG_NODE(imp_);
      BOOST_SPIRIT_DEBUG_NODE(or_);
      BOOST_SPIRIT_DEBUG_NODE(and_);
      BOOST_SPIRIT_DEBUG_NODE(not_);
      BOOST_SPIRIT_DEBUG_NODE(simple);
      BOOST_SPIRIT_DEBUG_NODE(var_);
    }
  
    private:
    qi::rule&lt;It, var() , Skipper&gt; var_;
    qi::rule&lt;It, expr(), Skipper&gt; not_, and_, or_, imp_, iff_, simple, expr_;
  };
  
  
  
  
  // Test some examples in main and check the order of precedence
  
  int main()
  {
    for (auto&amp; input : std::list&lt;std::string&gt; {
  
        // Test the order of precedence
        "(a and b) imp ((c and d) or (a and b));",
        "a and b iff (c and d or a and b);",
        "a and b imp (c and d or a and b);",
        "not a or not b;",
        "a or b;",
        "not a and b;",
        "not (a and b);",
        "a or b or c;",
        "aaa imp bbb iff ccc;",
        "aaa iff bbb imp ccc;",
  
  
        // Test elimination of equivalences
        "a iff b;",
        "a iff b or c;",
        "a or b iff b;",
        "a iff b iff c;",
  
        // Test elimination of implications
        "p imp q;",
        "p imp not q;",
        "not p imp not q;",
        "p imp q and r;",
        "p imp q imp r;",
        })
    {
      auto f(std::begin(input)), l(std::end(input));
      parser&lt;decltype(f)&gt; p;
  
      try
      {
        expr result;
        bool ok = qi::phrase_parse(f,l,p &gt; ';',qi::space,result);
  
        if (!ok)
          std::cerr &lt;&lt; "invalid input\n";
        else
          std::cout &lt;&lt; "result: " &lt;&lt; result &lt;&lt; "\n";
  
      } catch (const qi::expectation_failure&lt;decltype(f)&gt;&amp; e)
      {
        std::cerr &lt;&lt; "expectation_failure at '" &lt;&lt; std::string(e.first, e.last) &lt;&lt; "'\n";
      }
  
      if (f!=l) std::cerr &lt;&lt; "unparsed: '" &lt;&lt; std::string(f,l) &lt;&lt; "'\n";
    }
  
    return 0;
  }
  </code></pre>
  
  <p>Compiling command:</p>
  
  <pre><code>clang++ -std=c++11 -stdlib=libc++ -Weverything CNF_generator.cpp
  </code></pre>