рекурсия — преобразование логической формулы в конъюнктивную нормальную форму в переполнении стека

Я собираюсь реализовать генератор CNF в C ++, используя Boots / Spirit. но после финиша «порядок старшинства» и «устранение эквивалентности» & последствия «эти две части, я не могу понять, как реализовать» перемещать НЕ внутрь «и» распределить ИЛИ внутрь по И «.

Желаемый результат документирован здесь:
https://en.wikipedia.org/wiki/Conjunctive_normal_form

Вот более подробное описание ниже:

Порядок старшинства:

NOT > AND > OR > IMP > IFF

Пример ввода:

A iff B imp C

Теперь вывод:

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

И код (я реализую вывод на части принтера):

#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;
}

Команда компиляции:

clang++ -std=c++11 -stdlib=libc++ -Weverything CNF_generator.cpp

3

Решение

Движение НЕ внутрь должно быть сделано перед распределением ИЛИ по AND:

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

не забудьте отменить любое !!X что происходит при этом.

Также сбрасывать лишние ( )

ИЛИ распределяет по AND:

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

Возможно, вам нужно уменьшить некоторые другие избыточности, которые будут появляться, как вы делаете все это, например (X ИЛИ 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)

Может быть, я неправильно понял ваш вопрос, и вы уже поняли все вышеупомянутые преобразования, и у вас возникли проблемы с механикой выполнения этого внутри структуры, которую вы создали.

Вы, конечно, усложнили себе задачу (возможно, невозможную), пытаясь выполнить все преобразования внутри рутины печати. Я бы разобрал, потом трансформировал, потом распечатал.

Если вы настаиваете на преобразовании в процедуре печати, то, скорее всего, вы упускаете некоторые упрощения и вам нужно печатать, чтобы быть в курсе правил CNF. Узел AND может просто распечатать свои две стороны рекурсивно с AND между ними. Но любой другой узел сначала проверяет свои дочерние элементы и условно преобразует их достаточно, чтобы вытащить И до вершины перед рекурсивным вызовом.

Ты имел:

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 << ")";
}

Но вы не можете пройти весь путь до l или же r от ифф, и вы не можете напрямую генерировать какие-либо "not" или же "or" текст, пока вы не достигли рекурсивного дна. Таким образом, при неправильном дизайне преобразования во время печати подпрограмме iff потребуется сгенерировать временный объект, представляющий (l или нет r), а затем позвоните or подпрограмма обработки, чтобы обработать это, затем вывести "AND" затем создайте временный объект, представляющий (не l или же r) и позвонить or рутина обработки, чтобы справиться с этим.

Точно так же or рутина обработки должна была бы смотреть на каждый операнд. Если каждый просто конечная переменная или not окончательной переменной, or может просто излучать себя в поток. Но если любой операнд более сложный, or должен сделать что-то более сложное.

Помимо преобразования перед началом печати, есть несколько других вещей, которые вы можете изменить, чтобы сделать код проще:

Во-первых, вы можете избежать многих неприятностей, имея or а также and каждый объект содержит std::set любого количества операндов, а не пары операндов. Большая стоимость этого в том, что вам нужна приличная функция сравнения для объектов. Но окупаемость стоит того, чтобы иметь функцию сравнения.
Далее вы можете рассматривать иметь единый тип для всех подвыражений, а не иметь тип для каждого оператора. Таким образом, каждый объект должен хранить оператор и std::set операндов. У этого выбора дизайна есть довольно большие и очевидные недостатки, но есть одно большое преимущество: Подвыражение может трансформироваться в другой вид.

Более распространенная схема преобразования подвыражений (которая все еще может быть лучшей, просто рассмотрите альтернативы) заключается в том, что владелец подвыражения должен запросить подвыражение для условной генерации преобразованного клона самого себя. Это более эффективно, чем наличие объектов, способных непосредственно трансформироваться. Но для правильного определения деталей кодирования нужно больше думать.

Другим хорошим выбором для этой грамматики является выполнение всех преобразований при разборе. Более сложные проблемы действительно заслуживают полного разделения: разбора, преобразования, печати. Но в этом случае преобразование прекрасно вписывается в разбор, если вы продумываете заводские функции:

Фабрика берет оператора и один (для NOT) или два подвыражения, которые уже CNF. Это производит новое выражение CNF:

  • AND:

    • а) оба входа ANDs, образуют объединение своих множеств.
    • б) один вход является ANDвставьте другой вход в этот набор.
    • в) ни один из входных AND, создать новый AND с этими двумя входами.
  • OR:

    • а) оба входа ORs, образуют объединение своих множеств.
    • б) один вход является OR а другой примитив или NOTвставьте другой вход в ORустановлено.
    • в) по крайней мере один вход AND, распределите другой вклад через это AND (функция распределения должна обрабатывать ужасные подслучаи).
  • NOT:

    • Инверсия примитива тривиальна. Инверсия NOT тривиально. Инверсия OR это довольно тривиально. Инверсия AND это самая уродливая вещь во всем этом дизайне (вам нужно вывернуть все это наизнанку), но она выполнима. Чтобы сохранить здоровье, вы можете забыть об эффективности и рекурсивно использовать фабрику для NOT а также OR операции, которые NOT AND тривиально превращается в (но которые нуждаются в дальнейшем преобразовании, чтобы вернуться к CNF).
  • IFF а также IMPПросто сделайте несколько звонков на основные фабрики.
4

Другие решения

Вдохновленный тем, что я мало знаю о Boost.Proto, я попытался изменить ваш код, чтобы сделать возможными независимые преобразования. Этот подход использует 4 прохода (устранение_ффайса, устранение_импульса, распространение_ответов и распространение_ордина) и в каждом из них он перестраивает ast. Может быть способ сделать то же самое за один проход, возможно, с лучшей производительностью, но я думаю, что такой подход будет (даже) сложнее понять.

Объяснение изменений:

Первое изменение немного безвозмездно, но я действительно думаю, что все phx::construct...делает грамматику труднее читать. Я использую грамматику:

    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;

Для того, чтобы использовать это, вам нужно адаптировать unop а также binop с помощью BOOST_FUSION_ADAPT_TPL_STRUCT и объявить as_xxx как:

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

Если вам не нравится это изменение, ваша оригинальная грамматика также должна работать (если вы добавляете using namespace ast;).


Я положил все, что связано с АСТ внутри namespace ast и сделал несколько дополнений:

  • enum class expr_type: порядок его перечислителей должен быть синхронизирован с параметрами в варианте. Он используется для проверки того, имеет ли один из потомков узла определенный тип.
  • get_expr_type: просто возвращает тип выражения.
  • printer: теперь он просто печатает переданное выражение, без каких-либо преобразований. Может быть, это может быть изменено, чтобы быть умнее в размещении скобок.
  • операторы !, && а также ||: они используются для облегчения восстановления AST.

И наконец преобразования. Каждое преобразование использует ast_helper<Transformation> в качестве своей базы. Эта структура имеет несколько повторно используемых функций-членов:

  • pass_through: создает узел того же типа, который имеет в качестве членов, результат преобразования исходных элементов.
  • recurse: применяет преобразование к текущему узлу.
  • left: получает первый член узла независимо от типа узла. Используется в более сложных преобразованиях, чтобы немного помочь с удобочитаемостью.
  • child0: точно так же, как left, но имя имеет больше смысла в унарных узлах.
  • right: получает второго члена узла.

eliminate_imp :
Это действительно легко:

  • Если вы получите binop<op_imp> вернуть !p || q, куда p а также q являются результатом применения преобразования к первому и второму операндам соответственно.
  • Если вы получили что-то еще, верните узел того же типа, применяя преобразование к его операндам (pass_through).

eliminate_iff :
Это в основном то же самое, меняя binop<op_iff> с (p || !q)&&(!p || q),

distribute_nots :

  • Если вы получаете что-то, что не является unop<op_not> просто pass_through.
  • Если вы получите unop<op_not>Сначала проверьте тип своего операнда:

    • Если это и, заменить !p || !q,
    • Если это или, заменить !p && !q,
    • Если это не так, заменить p,

distribute_ors :

  • Если это что-то, кроме или, pass_through.
  • Если это или:
    • Проверьте, является ли его первый операнд and, Если это распространять ors и применить преобразование снова в случае, если другое or->and есть.
    • Проверьте, является ли его второй операнд and, Сделайте аналогичную работу.
    • Если ни один прямой ребенок не является andпроверить рекурсивно, если есть and в поддереве, начиная с этого узла. Если это произойдет, то все закончится плавающим наверху, поэтому нам нужно вернуться к pass_through.
    • Если нет and в поддереве это уже в CNF и просто pass_through.

Бег на Идеоне

Полный код:

#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;
}
3