在 C++ 中将逻辑公式转换为合取范式
Posted
技术标签:
【中文标题】在 C++ 中将逻辑公式转换为合取范式【英文标题】：Convert logic formula to conjunctive normal form in C++ 【发布时间】：2016-03-30 00:13:15 【问题描述】：我将使用 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
【问题讨论】：
@JSF 哦，所以我的问题不容易阅读？对不起我的英语不好，哪一部分不够清楚？我会尽力解释的！ @EricTsai，不，我不认为你的问题很难阅读。我只是认为定义的链接对于可能阅读它的许多人来说会更方便，所以我为您添加了。 @JSF 啊，非常感谢！也感谢您的回答。但是我知道规则，我很难写下来...... 我认识那个代码 :) @sehe，是的，我看看你的old post 并稍作修改，尝试制作一个 CNF 生成器。它给了我一个很好的方向:) 【参考方案1】：在将 OR 分配给 AND 之前，应该先将 NOT 向内移动：
!(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 andnot@987654333 @(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 << ")";
但是你不能从 iff 一直递归到 l 或 r 并且你不能直接生成任何 "not" 或 "or" 文本，直到你递归到达底部。因此，由于打印时转换的错误设计，iff例程需要生成一个表示（l或不是r）的临时对象，然后调用or处理例程来处理它，然后输出"AND"创建一个表示（不是l 或r）的临时对象并调用or 处理例程来处理它。
同样，or 处理例程需要查看每个操作数。如果每个都只是一个最终变量或最终变量的not，则or 可以简单地将自身发射到流中。但是如果任何操作数更复杂，or 必须做一些更复杂的事情。
除了在开始打印之前进行转换之外，您还可以更改其他几项以使代码更简单：
首先，您可以通过让or 和and 对象各自拥有任意数量的操作数的std::set 而不是一对操作数来避免很多麻烦。这样做的最大代价是您需要一个体面的对象比较功能。但回报是值得拥有比较功能的麻烦。
接下来，您可能考虑为所有子表达式设置一个类型，而不是为每个运算符设置一个类型。所以每个对象都必须存储一个运算符和一个std::set 的操作数。这种设计选择有一些相当大且明显的缺点，但有一个很大的优点：子表达式可以将自己转换为另一种类型。
更常见的子表达式转换方案（这可能仍然是最好的，只是考虑替代方案）是子表达式的所有者要求子表达式有条件地生成其自身的转换克隆。这比让对象能够直接转换自己更有效。但是要正确地编写编码细节需要更多的思考。
此语法的另一个不错的选择是在解析时进行所有转换。更复杂的问题确实值得完全拆分解析、转换、打印。但是在这种情况下，如果您仔细考虑工厂函数，则 transform 非常适合解析：
工厂接受一个运算符和一个（用于NOT）或两个已经是CNF的子表达式。它产生一个新的 CNF 表达式：
AND：
AND 的，形成它们集合的并集。
b) 一个输入是AND，将另一个输入插入到该集合中。
c) 两个输入都不是AND，使用这两个输入创建一个新的AND。
OR：
OR 的，形成它们集合的并集。
b) 一个输入是OR，另一个是原始输入或NOT，将另一个输入插入OR 的集合中。
c) 至少一个输入是AND，将另一个输入分配给AND（distribute 函数必须处理丑陋的子情况）。
NOT：
NOT 的反转是微不足道的。 OR 的反转非常简单。 AND 的反转是整个设计中最丑陋的事情（你需要把整个事情从里到外翻过来），但它是可行的。为了保持理智，您可以忘记效率并递归地使用工厂进行 NOT 和 OR 操作，NOT AND 可以简单地转换为（但需要进一步转换才能回到 CNF）。
IFF 和 IMP：只需对基本工厂进行适当的几次调用即可。
【讨论】：
是的，你是对的。好的，我会接受你的建议，明天试试。再次感谢，也许这正是我所需要的！ 您好 JSF，很高兴您指出我犯的错误并给出了很好的建议。将解析、转换和打印分开使代码更具可读性（尽管我仍然使用旧方法，而不是 std::set 来获取任意数量的操作数）。你给的设计很清楚，谢谢你一步一步的解释。 我还写了一个版本（因为我对某事感到好奇）。你去掉了什么样的冗余，你应该去掉什么样的冗余？如果您使用过set，它会自动删除一些琐碎的冗余。但大多数仍然存在。请参阅下一条评论中的示例。我的版本只使用单个字符标记（专注于转换而不是标记化）所以我使用= 代替IFF 和其他明显的替换。
从输入 (a=(b=c)) 我的版本生成：(a|b|!b)&(a|b|c)&(a|!b|!c)&(a|c|!c)&(!a|b|!c)&(!a|!b|c) 这是多余的。更好的答案是(a|b|c)&(a|!b|!c)&(!a|b|!c)&(!a|!b|c)。使用set 和一些额外的代码，可以轻松删除像这样的冗余。但是许多其他的则更加困难。与检查基元的所有 2**n 组合相比，无法检测到整个表达式可以被 false 替换的某些情况。【参考方案2】：
受我对 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;
为了能够使用它，您需要使用 BOOST_FUSION_ADAPT_TPL_STRUCT 调整 unop 和 binop 并将 as_xxx 声明为：
const as<binop<op_xxx>> as_xxx=;
如果您不喜欢这种更改，您的原始语法也应该可以使用（如果您添加 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：获取节点的第二个成员。
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。
Running on 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;
【讨论】：
我检查了输出“原始：公式”，它们显然是正确的。然后我查看输出“CNF：公式”，它们在删除多余的括号之后是合取范式（也就是说，这个程序给出了正确的解决方案）。我稍微修改了打印机以使最终输出为 CNF（也许有更多更好的方法）。感谢您的帮助，非常感谢您的明确解释！ Here 是一个尝试在括号打印上更智能的版本。它依赖于变体上的元素按优先级排序的事实（因此，如果您更改变体的定义，它将中断）。 顺便说一句，imps（我猜iffs）应该保持关联吗？还是this 正确？
@JSF 和他提供的解析器，一切都是正确的关联。我认为这对and 和or 来说不是问题，但我想这可能是imp 和iff 的问题。我的评论是为了确保他意识到可能存在的问题。
@EricTsai 我不是 100% 确定，但我认为 fix_associativity 转换 here 解决了问题。以上是关于在 C++ 中将逻辑公式转换为合取范式的主要内容，如果未能解决你的问题，请参考以下文章
数理逻辑命题逻辑的等值演算与推理演算 ( 命题逻辑 | 等值演算 | 主合取 ( 析取 ) 范式 | 推理演算 ) ★★