conjunctive_normal_form.h File Reference

Conversion of conditions to conjunctive normal form (CNF). More...

#include <vector>
#include "sdfg/symbolic/assumptions.h"
#include "sdfg/symbolic/symbolic.h"

Go to the source code of this file.

Classes
class	sdfg::symbolic::CNFException
	Exception thrown when CNF conversion fails. More...

Namespaces
namespace	sdfg
namespace	sdfg::symbolic

Typedefs
typedef std::vector< std::vector< Condition > >	sdfg::symbolic::CNF
	Conjunctive Normal Form representation.

Functions
CNF	sdfg::symbolic::conjunctive_normal_form (const Condition cond)
	Convert a condition to conjunctive normal form.
bool	sdfg::symbolic::is_tautology (const std::vector< symbolic::Condition > &clause)
	Check if a disjunctive clause is a tautology.

Detailed Description

Conversion of conditions to conjunctive normal form (CNF).

This file provides functionality for converting boolean conditions into conjunctive normal form.

Conjunctive Normal Form

CNF is a standardized format for boolean expressions where the expression is represented as a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals. For example: (A OR B) AND (C OR D OR E) AND (F)

Example Usage

auto x = symbolic::symbol("x");
auto y = symbolic::symbol("y");
 
// Create a complex condition: (x > 0 AND y < 10) OR (x < 0 AND y > 10)
auto cond = symbolic::Or(
    symbolic::And(symbolic::Gt(x, zero()), symbolic::Lt(y, integer(10))),
    symbolic::And(symbolic::Lt(x, zero()), symbolic::Gt(y, integer(10)))
);
 
// Convert to CNF
auto cnf = conjunctive_normal_form(cond);
// Result is a vector of clauses, each clause being a vector of conditions

See also

symbolic.h for building boolean conditions