c++ - 在 C++ 中将逻辑公式转换为合取范式

Question

我将使用 Boots/Spirit 在 C++ 中实现一个 CNF 生成器。但是在完成“优先顺序”和“消除等价和含义”这两个部分之后，我无法弄清楚如何实现“向内移动NOT”和“向内分配ORs而不是ANDs”。

所需的输出记录在这里： 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

score 4 · Accepted Answer

将 NOT 向内移动应该在将 OR 分布到 AND 之前完成：

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

请记住取消执行此操作!!X时发生的任何事情。

也丢掉多余的( )

OR 分布于 AND：

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

您可能需要减少其他一些在您执行所有这些操作时会逐渐出现的冗余，例如 (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)

也许我误解了您的问题，并且您已经理解了上述所有转换，并且您在创建的结构内执行此操作的机制遇到了麻烦。

通过尝试完成打印例程中的所有转换，您肯定让事情变得困难（也许是不可能的）。我会解析，然后转换，然后打印。

如果你坚持在 print 例程中进行转换，那么你可能会错过一些简化，你需要 print 来更加了解 CNF 的规则。AND 节点可以简单地用 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 << ")";
}

但是您不能一直递归到iffl或从 iff中递归，并且在递归到达底部之前r，您不能直接生成任何"not"或文本。"or"因此，由于打印时转换的错误设计，iff 例程需要生成一个表示 ( lor not r) 的临时对象，然后调用or处理例程来处理它，然后输出"AND"然后创建一个表示 (not lor r) 的临时对象并调用or处理例程来处理它。

类似地，or处理例程需要查看每个操作数。如果 each 只是一个 final 变量或not一个 final 变量，or则可以简单地将自身发射到流中。但是如果任何操作数更复杂，or就必须做一些更复杂的事情。

除了在开始打印之前进行转换之外，您还可以更改其他几项以使代码更简单：

or首先，您可以通过让和and对象每个都std::set包含任意数量的操作数而不是一对操作数来避免很多麻烦。这样做的最大代价是您需要一个体面的对象比较功能。但回报是值得拥有比较功能的麻烦。接下来，您可能会考虑为所有子表达式设置一个类型，而不是为每个运算符设置一个类型。所以每个对象都必须存储一个操作符和一个std::set操作数。这种设计选择有一些相当大且明显的缺点，但有一个很大的优点：子表达式可以将自己转换为另一种类型。

更常见的子表达式转换方案（可能仍然是最好的，只是考虑替代方案）是子表达式的所有者要求子表达式有条件地生成其自身的转换克隆。这比让对象能够直接转换自己更有效。但是正确地编写编码细节需要更多的思考。

该语法的另一个不错的选择是在解析时进行所有转换。更复杂的问题确实值得完全拆分解析、转换、打印。但是在这种情况下，如果您仔细考虑工厂函数，则 transform 非常适合解析：

工厂接受一个运算符和一个 (for NOT) 或两个已经是 CNF的子表达式。它产生一个新的 CNF 表达式：

AND：
- a) 两个输入都是AND's，形成它们集合的并集。
- b）一个输入是一个AND，将另一个输入插入到那个集合中。
- c）两个输入都不是AND，用这两个输入创建一个新AND的。
OR：
- a) 两个输入都是OR's，形成它们集合的并集。
- b) 一个输入是 anOR而另一个是原始的 or NOT，将另一个输入插入到OR的集合中。
- c）至少一个输入是一个AND，将另一个输入分布在其中AND（分布函数必须处理丑陋的子情况）。
NOT：
- 原语的反转是微不足道的。a 的反转NOT是微不足道的。an 的反转OR非常简单。an 的反转AND是整个设计中最难看的东西（你需要把整个东西翻过来）但是是可行的。为了保持理智，您可以忘记效率并递归地使用工厂进行简单转换为的NOT和OR操作NOT AND（但需要进一步转换才能回到 CNF）。
IFF和IMP：只需对基本工厂进行适当的几次调用。

score 3 · Accepted Answer

受到我对 Boost.Proto 知之甚少的启发，我尝试修改您的代码以允许独立的 ast 转换。这种方法使用 4 次传递（eliminate_iff、消除_imp、distribute_nots 和distribute_ors），并且在每一次中都重建了ast。可能有一种方法可以一次性完成相同的操作，可能性能更好，但我认为这种方法（甚至）更难理解。

变更说明：

第一个更改有点无缘无故，但我真的认为所有的phx::construct...s 都会使语法更难阅读。我使用的语法是：

    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={};

如果您不喜欢这种更改，您的原始语法也应该有效（如果您添加 a using namespace ast;）。

我已将与 AST 相关的所有内容都放入其中namespace ast并添加了一些内容：

enum class expr_type：它的枚举数的顺序需要与变量中的参数保持同步。它用于检查节点的其中一个子节点是否具有特定类型。
get_expr_type: 只返回表达式的类型。
printer: 现在它只打印传递的表达式，而不进行任何转换。也许可以将其更改为更智能地放置括号。
运算符!和&&:||它们用于使 AST 的重建更容易。

最后是转变。每个转换都ast_helper<Transformation>用作其基础。这个结构有几个重用的成员函数：

pass_through：创建一个与成员相同类型的节点，这是转换原始成员的结果。
recurse：将转换应用于当前节点。
left：获取节点的第一个成员，与节点的类型无关。用于更复杂的转换以稍微提高可读性。
child0: 与完全一样left，但名称在一元节点中更有意义。
right: 获取节点的第二个成员。

exclude_imp：
这个真的很简单：

如果你得到binop<op_imp>回报!p || q。其中p和q是分别对第一个和第二个操作数应用变换的结果。
如果你得到其他任何东西，则返回一个相同类型的节点，将转换应用于其操作数（pass_through）。

remove_iff：
基本一样，binop<op_iff>用(p || !q)&&(!p || q).

分发_nots：

如果你得到任何不是unop<op_not>简单的 pass_through 的东西。
如果你得到 a unop<op_not>，首先检查它的操作数的类型：
- 如果它是一个 and，用替换!p || !q。
- 如果是或，则替换为!p && !q。
- 如果不是，请替换为p。

分发器：

如果它不是一个或，pass_through。
如果是或：
- 检查其第一个操作数是否为and. 如果它是分发ors 并再次应用转换，以防另一个or->and存在。
- 检查其第二个操作数是否为and. 做类似的工作。
- 如果两个直接子节点都不是，则递归检查从该节点开始的子树中and是否有任何子树。and如果有，它最终会浮到顶部，所以我们需要在 pass_through 上递归。
- 如果子树中没有任何子and树，则它已经在 CNF 中并且只是 pass_through。

在 Ideone 上运行

完整代码：

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

c++ - 在 C++ 中将逻辑公式转换为合取范式

2 回答 2

变更说明：

Related

Reference