Applies simplifications while building up a BooleanFormula. More...

Public Member Functions
	CNFFormulaBuilder (CNFFormula &CNF)

void	addClause (ArrayRef< Literal > Literals)
	Adds the `L1 v ... v Ln` clause to the formula.

bool	isKnownContradictory ()
	Returns true if we observed a contradiction while adding clauses.

Detailed Description

Applies simplifications while building up a BooleanFormula.

We keep track of unit clauses, which tell us variables that must be true/false in any model that satisfies the overall formula. Such variables can be dropped from subsequently-added clauses, which may in turn yield more unit clauses or even a contradiction. The total added complexity of this preprocessing is O(N) where we for every clause, we do a lookup for each unit clauses. The lookup is O(1) on average. This method won't catch all contradictory formulas, more passes can in principle catch more cases but we leave all these and the general case to the proper SAT solver.

Definition at line 192 of file WatchedLiteralsSolver.cpp.

Constructor & Destructor Documentation

◆ CNFFormulaBuilder()

clang::dataflow::CNFFormulaBuilder::CNFFormulaBuilder ( CNFFormula & CNF )

inlineexplicit

Definition at line 194 of file WatchedLiteralsSolver.cpp.

Member Function Documentation

◆ addClause()

void clang::dataflow::CNFFormulaBuilder::addClause ( ArrayRef< Literal > Literals )

inline

Adds the L1 v ... v Ln clause to the formula.

Applies simplifications, based on single-literal clauses.

Requirements:

Li must not be NullLit.

All literals must be distinct.

Definition at line 205 of file WatchedLiteralsSolver.cpp.

References clang::dataflow::isNegLit(), clang::dataflow::isPosLit(), clang::dataflow::NullLit, v, clang::dataflow::var(), and X.

Referenced by clang::dataflow::buildCNF().

◆ isKnownContradictory()

bool clang::dataflow::CNFFormulaBuilder::isKnownContradictory ( )

inline

Returns true if we observed a contradiction while adding clauses.

In this case then the formula is already known to be unsatisfiable.

Definition at line 251 of file WatchedLiteralsSolver.cpp.