3

I'm going to implement a CNF generator in C++, using Boots/Spirit. but after finish "the order of precedence" and "eliminating equivalences & implications" these two parts, I can't figure out how to implement "move NOTs inwards" and "distribute ORs inwards over ANDs".

Desired output is documented here: https://en.wikipedia.org/wiki/Conjunctive_normal_form

Here are more detail description below:

The order of precedence:

NOT > AND > OR > IMP > IFF

Input example:

A iff B imp C

Now the output is:

(A or not ( not B or C)) and ( not A or ( not B or C))

And the code( I implement output at printer part ):

#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix.hpp>
#include <boost/spirit/include/phoenix_operator.hpp>
#include <boost/variant/recursive_wrapper.hpp>

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 <typename tag> struct binop;
template <typename tag> struct unop;

typedef boost::variant<var,
        boost::recursive_wrapper<unop <op_not> >,
        boost::recursive_wrapper<binop<op_and> >,
        boost::recursive_wrapper<binop<op_or> >,
        boost::recursive_wrapper<binop<op_imp> >,
        boost::recursive_wrapper<binop<op_iff> >
        > expr;

template <typename tag> struct binop
{
  explicit binop(const expr& l, const expr& r) : oper1(l), oper2(r) { }
  expr oper1, oper2;
};

template <typename tag> struct unop
{
  explicit unop(const expr& o) : oper1(o) { }
  expr oper1;
};



// Operating on the syntax tree

struct printer : boost::static_visitor<void>
{
  printer(std::ostream& os) : _os(os) {}
  std::ostream& _os;

  //
  void operator()(const var& v) const { _os << v; }

  void operator()(const binop<op_and>& b) const { print(" and ", b.oper1, b.oper2); }
  void operator()(const binop<op_or >& b) const { print(" or ", b.oper1, b.oper2); }
  void operator()(const binop<op_iff>& b) const { eliminate_iff(b.oper1, b.oper2); }
  void operator()(const binop<op_imp>& b) const { eliminate_imp(b.oper1, b.oper2); }

  void print(const std::string& op, const expr& l, const expr& r) const
  {
    _os << "(";
    boost::apply_visitor(*this, l);
    _os << op;
    boost::apply_visitor(*this, r);
    _os << ")";
  }

  void operator()(const unop<op_not>& u) const
  {
    _os << "( not ";
    boost::apply_visitor(*this, u.oper1);
    _os << ")";
  }

  void eliminate_iff(const expr& l, const expr& r) const
  {
    _os << "(";
    boost::apply_visitor(*this, l);
    _os << " or not ";
    boost::apply_visitor(*this, r);
    _os << ") and ( not ";
    boost::apply_visitor(*this, l);
    _os << " or ";
    boost::apply_visitor(*this, r);
    _os << ")";
  }

  void eliminate_imp(const expr& l, const expr& r) const
  {
    _os << "( not ";
    boost::apply_visitor(*this, l);
    _os << " or ";
    boost::apply_visitor(*this, r);
    _os << ")";
  }
};

std::ostream& operator<<(std::ostream& os, const expr& e)
{ boost::apply_visitor(printer(os), e); return os; }



// Grammar rules

template <typename It, typename Skipper = qi::space_type>
struct parser : qi::grammar<It, expr(), Skipper>
{
  parser() : parser::base_type(expr_)
  {
    using namespace qi;

    expr_  = iff_.alias();

    iff_ = (imp_ >> "iff" >> iff_) [ _val = phx::construct<binop<op_iff>>(_1, _2) ] | imp_   [ _val = _1 ];
    imp_ = (or_  >> "imp" >> imp_) [ _val = phx::construct<binop<op_imp>>(_1, _2) ] | or_    [ _val = _1 ];
    or_  = (and_ >> "or"  >> or_ ) [ _val = phx::construct<binop<op_or >>(_1, _2) ] | and_   [ _val = _1 ];
    and_ = (not_ >> "and" >> and_) [ _val = phx::construct<binop<op_and>>(_1, _2) ] | not_   [ _val = _1 ];
    not_ = ("not" > simple       ) [ _val = phx::construct<unop <op_not>>(_1)     ] | simple [ _val = _1 ];

    simple = (('(' > expr_ > ')') | 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<It, var() , Skipper> var_;
  qi::rule<It, expr(), Skipper> not_, and_, or_, imp_, iff_, simple, expr_;
};




// Test some examples in main and check the order of precedence

int main()
{
  for (auto& input : std::list<std::string> {

      // 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<decltype(f)> p;

    try
    {
      expr result;
      bool ok = qi::phrase_parse(f,l,p > ';',qi::space,result);

      if (!ok)
        std::cerr << "invalid input\n";
      else
        std::cout << "result: " << result << "\n";

    } catch (const qi::expectation_failure<decltype(f)>& e)
    {
      std::cerr << "expectation_failure at '" << std::string(e.first, e.last) << "'\n";
    }

    if (f!=l) std::cerr << "unparsed: '" << std::string(f,l) << "'\n";
  }

  return 0;
}

Compiling command:

clang++ -std=c++11 -stdlib=libc++ -Weverything CNF_generator.cpp
JSF
  • 5,281
  • 1
  • 13
  • 20
Eric Tsai
  • 66
  • 1
  • 5
  • @JSF oh so my question is not easy to read? Sorry for my poor English, which part is not clear enough? I'll try to explain it more! – Eric Tsai Dec 23 '15 at 15:56
  • @EricTsai, No I did not think your question was hard to read. I just thought a link to the definition would be more convenient for many people who might read it, so I added that for you. – JSF Dec 23 '15 at 15:59
  • @JSF ah, thank you very much! And also thank for your answer. However I know the rules, it's hard for me to write it down... – Eric Tsai Dec 23 '15 at 16:12
  • 1
    I recognize that code :) – sehe Dec 25 '15 at 00:23
  • @sehe, Yes I take a look at your [old post](http://stackoverflow.com/questions/8706356/boolean-expression-grammar-parser-in-c?answertab=votes#tab-top) and modify it a little bit, trying to make a CNF generator. It gives me a good direction :) – Eric Tsai Dec 25 '15 at 05:29

2 Answers2

4

Moving NOT inward should be done before distributing OR across AND:

!(A AND B) ==> (!A OR !B)
!(A OR B) ==> (!A AND !B)

remember to cancel any !!X that occurs while doing that.

Also drop redundant ( )

OR distributes across AND:

A OR (B AND C) ==> (A OR B) AND (A OR C)

You Probably need to reduce some other redundancies that will creep in as you do all that, such as (X OR X)

(A ornot( not B or C)) and ( not A or ( not B or C)) ==>
(A or (notnot B andnotC)) and ( not A or(not B or C)) ==>
(Aor( B and not C)) and ( not A or not B or C) ==>
((​AorB) and (Aornot C))and ( not A or not B or C) ==>
(A or B) and (A or not C) and ( not A or not B or C)

Maybe I misunderstood your question and you already understood all the above transformations, and you are having trouble with the mechanics of doing that inside the structure you have created.

You certainly have made things hard for yourself (maybe impossible) by trying to accomplish all the transformations inside the print routine. I would have parsed, then transformed, then printed.

If you insist on transforming in the print routine, then you likely miss some simplifications and you need print to be more aware of the rules of CNF. An AND node can simply print its two sides recursively with AND in between. But any other node most first inspect its children and conditionally transform enough to pull an AND up to the top before recursively calling.

You had:

void eliminate_iff(const expr& l, const expr& r) const
{
    _os << "(";
    boost::apply_visitor(*this, l);
    _os << " or not ";
    boost::apply_visitor(*this, r);
    _os << ") and ( not ";
    boost::apply_visitor(*this, l);
    _os << " or ";
    boost::apply_visitor(*this, r);
    _os << ")";
}

But you can't recurse all the way into l or r from iff and you can't directly generate any "not" or "or" text until you have recursively reached the bottom. So with the mis design of transforming while printing, the iff routine would need to generate a temp object representing (l or not r) and then call the or processing routine to handle it, then output "AND" then create a temp object representing (not l or r) and call the or processing routine to handle it.

Similarly, the or processing routine would need to look at each operand. If each is simply a final variable or not of a final variable, or can simply emit itself to the stream. But if any operand is more complicated, or must do something more complicated.

In addition to doing transformation before you start printing, there are a couple other things you might change in order to make the code simpler:

First, you could avoid a lot of trouble by having or and and objects each hold a std::set of any number of operands, rather than a pair of operands. The big cost of that is you need a decent comparison function for the objects. But the pay back is worth the trouble of having a comparison function. Next, you might consider having a single type for all subexpressions, rather than having a type for each operator. So each object must store an operator and a std::set of operands. There are some pretty big and obvious disadvantages to that design choice, but there is one big advantage: A subexpression can transform itself into a different kind.

The more common subexpression transformation scheme (which might still be best, just consider alternatives) is for the owner of a subexpression to ask the subexpression to conditionally generate a transformed clone of itself. That is more efficient than having objects able to directly transform themselves. But getting the coding details right requires more thought.

Another good choice for this grammar is to do all the transformations while parsing. More complicated problems really deserve the full split of parse, transform, print. But in this case transform fits beautifully into parsing if you think through your factory function:

The factory takes an operator and one (for NOT) or two subexpressions that are already CNF. It produces a new CNF expression:

  • AND:

    • a) Both inputs are AND's, form the union of their sets.
    • b) One input is an AND, insert the other input into that one's set.
    • c) Neither input is an AND, create a new AND with those two inputs.
  • OR:

    • a) Both inputs are OR's, form the union of their sets.
    • b) One input is an OR and the other is primitive or NOT, insert the other input into the OR's set.
    • c) At least one input is an AND, distribute the other input across that AND (the distribute function must handle the ugly sub cases).
  • NOT:

    • Inversion of a primitive is trivial. Inversion of a NOT is trivial. Inversion of an OR is pretty trivial. Inversion of an AND is the ugliest thing in this whole design (you need to turn the whole thing inside out) but is doable. To keep your sanity, you could forget about efficiency and use the factory recursively for the NOT and OR operations that a NOT AND trivially transforms to (but which need further transformation to get back to CNF).
  • IFF and IMP: Just make the appropriate several calls to the basic factories.
sehe
  • 374,641
  • 47
  • 450
  • 633
JSF
  • 5,281
  • 1
  • 13
  • 20
  • Yes you're right. OK I'll take your advice and try it tomorrow. Thx again, maybe it's just what I need! – Eric Tsai Dec 23 '15 at 16:18
  • Hi JSF, it’s kind that you point out the mistake I made and give a good advice. Take parsing, transforming and printing apart makes the code more readable(although I still use the old way, not std::set to take any number of operands). The design you give is very clear, thank you for explaining it step by step. – Eric Tsai Dec 25 '15 at 05:31
  • I also wrote a version (because I was curious about something). What kinds of redundancies did you take out and what kinds were you supposed to take out? If you had used `set` that automatically removes a few trivial redundancies. But most remain. See example in next comment. My version uses only single character tokens (to focus on transforming not tokenizing) so I used `=` for `IFF` and other obvious substitutions. – JSF Dec 25 '15 at 11:41
  • 2
    From input `(a=(b=c))` my version generates: `(a|b|!b)&(a|b|c)&(a|!b|!c)&(a|c|!c)&(!a|b|!c)&(!a|!b|c)` which is redundant. A better answer would be`(a|b|c)&(a|!b|!c)&(!a|b|!c)&(!a|!b|c)`. Using `set` and a little extra code, redundancies like that one can be easily dropped. But many others are arbitrarily more difficult. Some cases where the whole expression could be replaced by `false` can't be detected with less work than examining all `2**n` combinations of the primitives. – JSF Dec 25 '15 at 11:47
3

Inspired by what little I know about Boost.Proto I've tried to modify your code to allow for independent ast transformations. This approach uses 4 passes (eliminate_iff, eliminate_imp, distribute_nots and distribute_ors) and in each one it rebuilds the ast. There may be a way to do the same in a single pass, probably with better performance, but I think that approach would be (even) harder to understand.

Explanation of the changes:

The first change is a little gratuitous but I really think that all the phx::construct...s make the grammar harder to read. The grammar I use is:

    iff_ = as_iff[imp_ >> "iff" >> iff_] | imp_;
    imp_ = as_imp[or_ >> "imp" >> imp_] | or_;
    or_ = as_or[and_ >> "or" >> or_] | and_;
    and_ = as_and[not_ >> "and" >> and_] | not_;
    not_ = as_not["not" > simple] | simple;

In order to be able to use this you need to adapt unop and binop using BOOST_FUSION_ADAPT_TPL_STRUCT and declare as_xxx as:

const as<binop<op_xxx>> as_xxx={};

If you don't like this change your original grammar should also work (if you add a using namespace ast;).


I've put everything related to the AST inside namespace ast and made a few additions:

  • enum class expr_type: the order of its enumerators needs to be kept in synch with the parameters in the variant. It is used to check whether one of a node's children has a particular type.
  • get_expr_type: simply returns what is the type of the expression.
  • printer: now it just prints the expression passed, without making any transformation. Maybe it could be changed to be smarter about the placing of parentheses.
  • operators !, && and ||: they are used to make the rebuilding of the AST easier.

And finally the transformations. Every transformation uses ast_helper<Transformation> as its base. This struct has several reused member functions:

  • pass_through: creates a node of the same type that has as members, the result of transforming the original members.
  • recurse: applies the transformation to the current node.
  • left: gets the first member of a node independently of the type of the node. Gets used in the more complex transformations to slightly help with readability.
  • child0: exactly the same as left, but the name makes more sense in unary nodes.
  • right: gets the second member of a node.

eliminate_imp :
This one is really easy:

  • If you get a binop<op_imp> return !p || q. Where p and q are the result of applying the transformation to the first and second operands respectively.
  • If you get anything else return a node of the same kind applying the transformation to its operands(pass_through).

eliminate_iff :
It's basically the same, changing binop<op_iff> with (p || !q)&&(!p || q).

distribute_nots :

  • If you get anything that is not a unop<op_not> simply pass_through.
  • If you get a unop<op_not>, first check the type of its operand:

    • If it's an and, substitute with !p || !q.
    • If it's an or, substitute with !p && !q.
    • If it's a not, substitute with p.

distribute_ors :

  • If it's anything but an or, pass_through.
  • If it's an or:
    • Check whether its first operand is an and. If it is distribute the ors and apply the transformation again in case another or->and is there.
    • Check whether its second operand is an and. Do the analogous work.
    • If neither direct child is an and, check recursively if there is any and in the subtree starting with this node. If there is it'll end up floating to the top so we'll need to recurse on the pass_through.
    • If there isn't any and in the subtree, it is already in CNF and simply pass_through.

Running on Ideone

Full Code:

#include <boost/spirit/include/qi.hpp>
#include <boost/fusion/include/adapt_struct.hpp>

#include <boost/variant/recursive_wrapper.hpp>

namespace qi = boost::spirit::qi;



// Abstract data type

struct op_or {};
struct op_and {};
struct op_imp {};
struct op_iff {};
struct op_not {};

namespace ast
{
    typedef std::string var;
    template <typename tag> struct binop;
    template <typename tag> struct unop;

    enum class expr_type { var = 0, not_, and_, or_, imp, iff };
    typedef boost::variant<var,
        boost::recursive_wrapper<unop <op_not> >,
        boost::recursive_wrapper<binop<op_and> >,
        boost::recursive_wrapper<binop<op_or> >,
        boost::recursive_wrapper<binop<op_imp> >,
        boost::recursive_wrapper<binop<op_iff> >
    > expr;

    expr_type get_expr_type(const expr& expression)
    {
        return static_cast<expr_type>(expression.which());
    }

    template <typename tag> struct binop
    {
        expr oper1, oper2;
    };

    template <typename tag> struct unop
    {
        expr oper1;
    };

    struct printer : boost::static_visitor<void>
    {
        printer(std::ostream& os) : _os(os) {}
        std::ostream& _os;
        mutable bool first{ true };

        //
        void operator()(const ast::var& v) const { _os << v; }


        void operator()(const ast::binop<op_and>& b) const { print(" and ", b.oper1, b.oper2); }
        void operator()(const ast::binop<op_or>& b) const { print(" or ", b.oper1, b.oper2); }
        void operator()(const ast::binop<op_iff>& b) const { print(" iff ", b.oper1, b.oper2); }
        void operator()(const ast::binop<op_imp>& b) const { print(" imp ", b.oper1, b.oper2); }

        void print(const std::string& op, const ast::expr& l, const ast::expr& r) const
        {
            _os << "(";
            boost::apply_visitor(*this, l);
            _os << op;
            boost::apply_visitor(*this, r);
            _os << ")";
        }

        void operator()(const ast::unop<op_not>& u) const
        {
            _os << "not(";
            boost::apply_visitor(*this, u.oper1);
            _os << ")";
        }
    };

    std::ostream& operator<<(std::ostream& os, const expr& e)
    {
        boost::apply_visitor(printer(os), e); return os;
    }

    expr operator!(const expr& e)
    {
        return unop<op_not>{e};
    }

    expr operator||(const expr& l, const expr& r)
    {
        return binop<op_or>{l, r};
    }

    expr operator&&(const expr& l, const expr& r)
    {
        return binop<op_and>{l, r};
    }

}

BOOST_FUSION_ADAPT_TPL_STRUCT(
    (Tag),
    (ast::binop) (Tag),
    (ast::expr, oper1)
    (ast::expr, oper2)
)

BOOST_FUSION_ADAPT_TPL_STRUCT(
    (Tag),
    (ast::unop) (Tag),
    (ast::expr, oper1)
)


// Grammar rules

template <typename It, typename Skipper = qi::space_type>
struct parser : qi::grammar<It, ast::expr(), Skipper>
{
    parser() : parser::base_type(expr_)
    {
        using namespace qi;
        const as<ast::binop<op_iff> > as_iff = {};
        const as<ast::binop<op_imp> > as_imp = {};
        const as<ast::binop<op_or> > as_or = {};
        const as<ast::binop<op_and> > as_and = {};
        const as<ast::unop<op_not> > as_not = {};

        expr_ = iff_.alias();

        iff_ = as_iff[imp_ >> "iff" >> iff_] | imp_;
        imp_ = as_imp[or_ >> "imp" >> imp_] | or_;
        or_ = as_or[and_ >> "or" >> or_] | and_;
        and_ = as_and[not_ >> "and" >> and_] | not_;
        not_ = as_not["not" > simple] | simple;

        simple = (('(' > expr_ > ')') | 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<It, ast::var(), Skipper> var_;
    qi::rule<It, ast::expr(), Skipper> not_, and_, or_, imp_, iff_, simple, expr_;
};

template <typename Transform>
struct ast_helper : boost::static_visitor<ast::expr>
{

    template <typename Tag>
    ast::expr pass_through(const ast::binop<Tag>& op) const
    {
        return ast::binop<Tag>{recurse(op.oper1), recurse(op.oper2)};
    }

    template <typename Tag>
    ast::expr pass_through(const ast::unop<Tag>& op) const
    {
        return ast::unop<Tag>{recurse(op.oper1)};
    }

    ast::expr pass_through(const ast::var& variable) const
    {
        return variable;
    }

    ast::expr recurse(const ast::expr& expression) const
    {
        return boost::apply_visitor(Transform{}, expression);
    }

    struct left_getter:boost::static_visitor<ast::expr>
    {
        template< template<class> class Op,typename Tag>
        ast::expr operator()(const Op<Tag>& op) const
        {
            return op.oper1;
        }

        ast::expr operator()(const ast::var&) const
        {
            return{};//throw something?
        }
    };


    ast::expr left(const ast::expr& expression) const
    {
        return boost::apply_visitor(left_getter{}, expression);
    }

    ast::expr child0(const ast::expr& expression) const
    {
        return left(expression);
    }

    struct right_getter :boost::static_visitor<ast::expr>
    {
        template<typename Tag>
        ast::expr operator()(const ast::binop<Tag>& op) const
        {
            return op.oper2;
        }

        template<typename Expr>
        ast::expr operator()(const Expr&) const
        {
            return{};//throw something?
        }
    };

    ast::expr right(const ast::expr& expression) const
    {
        return boost::apply_visitor(right_getter{}, expression);
    }

};

struct eliminate_imp : ast_helper<eliminate_imp>
{
    template <typename Op>
    ast::expr operator()(const Op& op) const
    {
        return pass_through(op);
    }

    ast::expr operator()(const ast::binop<op_imp>& imp) const
    {
        return !recurse(imp.oper1) || recurse(imp.oper2);
    }

    ast::expr operator()(const ast::expr& expression) const
    {
        return recurse(expression);
    }
};

struct eliminate_iff : ast_helper<eliminate_iff>
{
    template <typename Op>
    ast::expr operator()(const Op& op) const
    {
        return pass_through(op);
    }

    ast::expr operator()(const ast::binop<op_iff>& imp) const
    {
        return (recurse(imp.oper1) || !recurse(imp.oper2)) && (!recurse(imp.oper1) || recurse(imp.oper2));
    }

    ast::expr operator()(const ast::expr& expression) const
    {
        return recurse(expression);
    }
};

struct distribute_nots : ast_helper<distribute_nots>
{
    template <typename Op>
    ast::expr operator()(const Op& op) const
    {
        return pass_through(op);
    }

    ast::expr operator()(const ast::unop<op_not>& not_) const
    {
        switch (ast::get_expr_type(not_.oper1)) //There is probably a better solution
        {
        case ast::expr_type::and_:
            return recurse(!recurse(left(not_.oper1))) || recurse(!recurse(right(not_.oper1)));

        case ast::expr_type::or_:
            return recurse(!recurse(left(not_.oper1))) && recurse(!recurse(right(not_.oper1)));

        case ast::expr_type::not_:
            return recurse(child0(not_.oper1));
        default:
            return pass_through(not_);
        }
    }

    ast::expr operator()(const ast::expr& expression) const
    {
        return recurse(expression);
    }
};

struct any_and_inside : boost::static_visitor<bool>
{
    any_and_inside(const ast::expr& expression) :expression(expression) {}
    const ast::expr& expression;

    bool operator()(const ast::var&) const
    {
        return false;
    }

    template <typename Tag>
    bool operator()(const ast::binop<Tag>& op) const
    {
        return boost::apply_visitor(*this, op.oper1) || boost::apply_visitor(*this, op.oper2);
    }

    bool operator()(const ast::binop<op_and>&) const
    {
        return true;
    }

    template<typename Tag>
    bool operator()(const ast::unop<Tag>& op) const
    {
        return boost::apply_visitor(*this, op.oper1);
    }


    explicit operator bool() const
    {
        return boost::apply_visitor(*this, expression);
    }

};

struct distribute_ors : ast_helper<distribute_ors>
{
    template <typename Op>
    ast::expr operator()(const Op& op) const
    {
        return pass_through(op);
    }

    ast::expr operator()(const ast::binop<op_or>& or_) const
    {
        if (ast::get_expr_type(or_.oper1) == ast::expr_type::and_)
        {
            return recurse(recurse(left(or_.oper1)) || recurse(or_.oper2)) 
                && recurse(recurse(right(or_.oper1)) || recurse(or_.oper2));
        }
        else if (ast::get_expr_type(or_.oper2) == ast::expr_type::and_)
        {
            return recurse(recurse(or_.oper1) || recurse(left(or_.oper2)))
                && recurse(recurse(or_.oper1) || recurse(right(or_.oper2)));
        }
        else if (any_and_inside( or_ ))
        {
            return recurse(recurse(or_.oper1) || recurse(or_.oper2));
        }
        else
        {
            return pass_through(or_);
        }
    }

    ast::expr operator()(const ast::expr& expression) const
    {
        return recurse(expression);
    }

};

ast::expr to_CNF(const ast::expr& expression)
{
    return distribute_ors()(distribute_nots()(eliminate_iff()(eliminate_imp()(expression))));
}




// Test some examples in main and check the order of precedence

int main()
{
    for (auto& input : std::list<std::string>{

        // 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<decltype(f)> p;

        try
        {
            ast::expr result;
            bool ok = qi::phrase_parse(f, l, p > ';', qi::space, result);

            if (!ok)
                std::cerr << "invalid input\n";
            else
            {
                std::cout << "original: " << result << "\n";
                std::cout << "CNF: " << to_CNF(result) << "\n";
            }

        }
        catch (const qi::expectation_failure<decltype(f)>& e)
        {
            std::cerr << "expectation_failure at '" << std::string(e.first, e.last) << "'\n";
        }

        if (f != l) std::cerr << "unparsed: '" << std::string(f, l) << "'\n";
    }

    return 0;
}
llonesmiz
  • 155
  • 2
  • 11
  • 20
  • 1
    I check the outputs "original: formula", they are correct obviously. Then I look at the outputs "CNF: formula", they are conjunctive normal form exactly after dropping redundant parentheses(that's mean, this program gives the correct solution). I modify the printer a little bit to make final output as CNF(maybe there are more better way). Thanks for your help, and BIG THANKS for clear explanation! – Eric Tsai Dec 25 '15 at 06:47
  • [Here](http://ideone.com/mY7QSf) is a version that tries to be smarter with the printing of the parentheses. It relies on the fact that the elements on the variant are ordered by priority (so if you change the definition of the variant it will break). – llonesmiz Dec 25 '15 at 07:21
  • 1
    Btw, should `imp`s (and I guess `iff`s) be left associative? Or is [this](http://ideone.com/x9wQMY) correct? – llonesmiz Dec 25 '15 at 07:31
  • @cv_and_he It is convenient for the final output to drop redundant `( )` for `AND` of `AND` or `OR` of `OR`. But having your parsed intermediate output drop non redundant `( )` is inconvenient. If anything was right associative, that should have been specified in the original problem statement. – JSF Dec 25 '15 at 11:58
  • 1
    @JSF with the parser he provided everything IS right associative. I think that is not a problem for `and` and `or`, but I imagine it could be for `imp` and `iff`. My comment was to make sure he was aware of that possible problem. – llonesmiz Dec 25 '15 at 12:04
  • I missed that detail. I didn't look into the behavior of his parser or your parser. I focused on the transformation aspect and foolishly assumed the grammar was simple enough to not have issues. So you make a very important point. The decision of whether IMP and IFF are right or left associative should be by design, not by accident. – JSF Dec 25 '15 at 12:07
  • @cv_and_he No!!! I didn't aware they should be left associative!!! So I guess it's necessary to rewrite the parser, but I can only tell the code in parser part dealing with precedence issue. How to make it left associative? – Eric Tsai Dec 25 '15 at 14:54
  • 1
    @EricTsai I'm not 100% certain, but I think the `fix_associativity` transformation [here](http://ideone.com/nL0zte) solves the problem. – llonesmiz Dec 25 '15 at 23:05
  • I checkout some tests like `a imp b imp c` , `(a iff b) iff c` by hand, the final CNF are as same as outputs `CNF fixed?: formula`. They are left associative now. I'm going to imagining how `fix_associativity` do and then tests more example formulas, but I think your code is already right =) – Eric Tsai Dec 26 '15 at 03:48