An explanation is either a single clause or a chain of clauses, satisfying the following properties: More...

#include <ClauseChain.h>

Collaboration diagram for smtrat::mcsat::ClauseChain:

[legend]

Data Structures
struct	Link

Public Types
using	const_iterator = typename std::vector< Link >::const_iterator

Public Member Functions
	ClauseChain ()

FormulaT	createTseitinVar (const FormulaT &formula)
	Create a Tseitin variable for the given formula. More...

void	appendPropagating (const FormulaT &&clause, const FormulaT &&impliedTseitinLiteral)
	Append a clause that implies impliedTseitinLiteral under the current assignment. More...

void	appendConflicting (const FormulaT &&clause)
	Append a conflicting clause (regarding the current assignment). More...

void	appendOptional (const FormulaT &&clause)
	Append an additional clause which is neither propagating nor conflicting. More...

const std::vector< Link > &	chain () const

const_iterator	begin () const

const_iterator	end () const

FormulaT	resolve () const
	Performs resolution on the chain. More...

FormulaT	to_formula () const
	Transforms the clause chain into a formula (containing Tseitin variables). More...

Static Public Member Functions
static ClauseChain	from_formula (const FormulaT &f, const Model &model, bool with_equivalence)
	Transforms a given Boolean conjunction over AND and OR to CNF via Tseitin-Transformation so that, if the input formula is conflicting under the current assignment, after all clauses in "implications" have been propagated in the given order, the returned formula evaluates to false. More...

Private Member Functions
bool	isTseitinVar (const FormulaT &var) const

Private Attributes
std::vector< Link >	mClauseChain

std::unordered_set< FormulaT >	mTseitinVars

Friends
std::ostream &	operator<< (std::ostream &stream, const ClauseChain &chain)

Detailed Description

An explanation is either a single clause or a chain of clauses, satisfying the following properties:

If the clauses are inserted and propagated in the chain's order, at least the last clause should be conflicting.
Each conflicting clause is already conflicting after preceding clauses have been inserted and propagated.
Tseitin vars should be used so that a Tseitin variable C is equivalent to its corresponding subformula F (or at least C -> F).

Definition at line 16 of file ClauseChain.h.

Member Typedef Documentation

◆ const_iterator

using smtrat::mcsat::ClauseChain::const_iterator = typename std::vector<Link>::const_iterator

Definition at line 54 of file ClauseChain.h.

Constructor & Destructor Documentation

◆ ClauseChain()

smtrat::mcsat::ClauseChain::ClauseChain ( )

inline

Definition at line 67 of file ClauseChain.h.

Member Function Documentation

◆ appendConflicting()

void smtrat::mcsat::ClauseChain::appendConflicting ( const FormulaT && clause )

inline

Append a conflicting clause (regarding the current assignment).

Definition at line 90 of file ClauseChain.h.

Here is the caller graph for this function:

◆ appendOptional()

void smtrat::mcsat::ClauseChain::appendOptional ( const FormulaT && clause )

inline

Append an additional clause which is neither propagating nor conflicting.

Can be used to pass additional knowledge.

Definition at line 98 of file ClauseChain.h.

Here is the caller graph for this function:

◆ appendPropagating()

void smtrat::mcsat::ClauseChain::appendPropagating	(	const FormulaT &&	clause,
		const FormulaT &&	impliedTseitinLiteral
	)

inline

Append a clause that implies impliedTseitinLiteral under the current assignment.

Note that impliedTseitinLiteral = ~v for a Tseitin variable v obtained via createTseitinVar.

Definition at line 83 of file ClauseChain.h.

Here is the caller graph for this function:

◆ begin()

const_iterator smtrat::mcsat::ClauseChain::begin ( ) const

inline

Returns: A constant iterator to the beginning of this chain.

Definition at line 112 of file ClauseChain.h.

◆ chain()

const std::vector<Link>& smtrat::mcsat::ClauseChain::chain ( ) const

inline

Returns: A vector representing this chain.

Definition at line 105 of file ClauseChain.h.

Here is the caller graph for this function:

◆ createTseitinVar()

FormulaT smtrat::mcsat::ClauseChain::createTseitinVar ( const FormulaT & formula )

inline

Create a Tseitin variable for the given formula.

The returned variable C should be used so that C <-> formula or at least ~formula -> ~C

Definition at line 73 of file ClauseChain.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ end()

const_iterator smtrat::mcsat::ClauseChain::end ( ) const

inline

Returns: A constant iterator to the end of this chain.

Definition at line 119 of file ClauseChain.h.

◆ from_formula()

ClauseChain smtrat::mcsat::ClauseChain::from_formula	(	const FormulaT &	f,
		const Model &	model,
		bool	with_equivalence
	)

static

Transforms a given Boolean conjunction over AND and OR to CNF via Tseitin-Transformation so that, if the input formula is conflicting under the current assignment, after all clauses in "implications" have been propagated in the given order, the returned formula evaluates to false.

Definition at line 160 of file ClauseChain.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isTseitinVar()

bool smtrat::mcsat::ClauseChain::isTseitinVar ( const FormulaT & var ) const

inlineprivate

Definition at line 62 of file ClauseChain.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ resolve()

FormulaT smtrat::mcsat::ClauseChain::resolve ( ) const

Performs resolution on the chain.

Uses the last clause for resolution.

Returns: A single clause conflicting under the current assignment.

Definition at line 5 of file ClauseChain.cpp.

Here is the call graph for this function:

◆ to_formula()

FormulaT smtrat::mcsat::ClauseChain::to_formula ( ) const

Transforms the clause chain into a formula (containing Tseitin variables).

Definition at line 62 of file ClauseChain.cpp.

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<<	(	std::ostream &	stream,
		const ClauseChain &	chain
	)

friend

Definition at line 153 of file ClauseChain.h.

Field Documentation

◆ mClauseChain

std::vector<Link> smtrat::mcsat::ClauseChain::mClauseChain

private

Definition at line 59 of file ClauseChain.h.

◆ mTseitinVars

std::unordered_set<FormulaT> smtrat::mcsat::ClauseChain::mTseitinVars

private

Definition at line 60 of file ClauseChain.h.

The documentation for this class was generated from the following files:

smtrat-mcsat/utils/ClauseChain.h
smtrat-mcsat/utils/ClauseChain.cpp

Data Structures

Public Types

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ const_iterator

Constructor & Destructor Documentation

◆ ClauseChain()

Member Function Documentation

◆ appendConflicting()

◆ appendOptional()

◆ appendPropagating()

◆ begin()

◆ chain()

◆ createTseitinVar()

◆ end()

◆ from_formula()

◆ isTseitinVar()

◆ resolve()

◆ to_formula()

Friends And Related Function Documentation

◆ operator<<

Field Documentation

◆ mClauseChain

◆ mTseitinVars