smtrat::CardinalityEncoder Class Reference

#include <CardinalityEncoder.h>

Inheritance diagram for smtrat::CardinalityEncoder:

Collaboration diagram for smtrat::CardinalityEncoder:

Public Member Functions
	CardinalityEncoder ()
Rational	encodingSize (const ConstraintT &constraint)
bool	canEncode (const ConstraintT &constraint)
std::string	name ()
std::optional< FormulaT >	encode (const ConstraintT &constraint)
	Encodes an arbitrary constraint. More...

Data Fields
std::size_t	problem_size

Protected Member Functions
std::optional< FormulaT >	doEncode (const ConstraintT &constraint)
FormulaT	generateVarChain (const std::set< carl::Variable > &vars, carl::FormulaType type)

Private Member Functions
std::optional< FormulaT >	encodeExactly (const ConstraintT &constraint)
FormulaT	encodeExactly (const std::vector< carl::Variable > &variables, const Rational constant)
std::optional< FormulaT >	encodeAtLeast (const ConstraintT &constraint)
std::optional< FormulaT >	encodeAtMost (const ConstraintT &constraint)
ConstraintT	normalizeLessConstraint (const ConstraintT &constraint)

Detailed Description

Definition at line 6 of file CardinalityEncoder.h.

Constructor & Destructor Documentation

CardinalityEncoder()

smtrat::CardinalityEncoder::CardinalityEncoder ( )

inline

Definition at line 8 of file CardinalityEncoder.h.

Member Function Documentation

canEncode()

bool smtrat::CardinalityEncoder::canEncode ( const ConstraintT &  constraint )

virtual

Implements smtrat::PseudoBoolEncoder.

Definition at line 157 of file CardinalityEncoder.cpp.

Here is the caller graph for this function:

doEncode()

std::optional< FormulaT > smtrat::CardinalityEncoder::doEncode ( const ConstraintT &  constraint )

protectedvirtual

Implements smtrat::PseudoBoolEncoder.

Definition at line 8 of file CardinalityEncoder.cpp.

Here is the call graph for this function:

encode()

std::optional< FormulaT > smtrat::PseudoBoolEncoder::encode ( const ConstraintT &  constraint )

inherited

Encodes an arbitrary constraint.

Returns

encoded formula

Definition at line 5 of file PseudoBoolEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

encodeAtLeast()

std::optional< FormulaT > smtrat::CardinalityEncoder::encodeAtLeast ( const ConstraintT &  constraint )

private

Definition at line 111 of file CardinalityEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

encodeAtMost()

std::optional< FormulaT > smtrat::CardinalityEncoder::encodeAtMost ( const ConstraintT &  constraint )

private

Definition at line 137 of file CardinalityEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

encodeExactly() [1/2]

std::optional< FormulaT > smtrat::CardinalityEncoder::encodeExactly ( const ConstraintT &  constraint )

private

Definition at line 73 of file CardinalityEncoder.cpp.

Here is the caller graph for this function:

encodeExactly() [2/2]

FormulaT smtrat::CardinalityEncoder::encodeExactly ( const std::vector< carl::Variable > &  variables, const Rational  constant  )

private

Definition at line 79 of file CardinalityEncoder.cpp.

encodingSize()

Rational smtrat::CardinalityEncoder::encodingSize ( const ConstraintT &  constraint )

virtual

Reimplemented from smtrat::PseudoBoolEncoder.

Definition at line 178 of file CardinalityEncoder.cpp.

Here is the call graph for this function:

generateVarChain()

FormulaT smtrat::PseudoBoolEncoder::generateVarChain ( const std::set< carl::Variable > &  vars, carl::FormulaType  type  )

protectedinherited

Definition at line 38 of file PseudoBoolEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

name()

std::string smtrat::CardinalityEncoder::name ( )

inlinevirtual

Reimplemented from smtrat::PseudoBoolEncoder.

Definition at line 14 of file CardinalityEncoder.h.

normalizeLessConstraint()

ConstraintT smtrat::PseudoBoolEncoder::normalizeLessConstraint ( const ConstraintT &  constraint )

privateinherited

Definition at line 25 of file PseudoBoolEncoder.cpp.

Here is the caller graph for this function:

Field Documentation

problem_size

std::size_t smtrat::PseudoBoolEncoder::problem_size

inherited

Definition at line 20 of file PseudoBoolEncoder.h.

---

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

• smtrat-modules/PBPPModule/Encoders/CardinalityEncoder.h
• smtrat-modules/PBPPModule/Encoders/CardinalityEncoder.cpp