smtrat::PseudoBoolEncoder Class Reference

Base class for a PseudoBoolean Encoder. More...

#include <PseudoBoolEncoder.h>

Inheritance diagram for smtrat::PseudoBoolEncoder:

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

Data Fields
std::size_t	problem_size

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

Private Member Functions
ConstraintT	normalizeLessConstraint (const ConstraintT &constraint)

Detailed Description

Base class for a PseudoBoolean Encoder.

It takes a arithmetic constraint and converts it to a boolean Formula

Definition at line 13 of file PseudoBoolEncoder.h.

Member Function Documentation

canEncode()

virtual bool smtrat::PseudoBoolEncoder::canEncode ( const ConstraintT &  constraint )

pure virtual

Implemented in smtrat::TotalizerEncoder, smtrat::ShortFormulaEncoder, smtrat::RNSEncoder, smtrat::MixedSignEncoder, smtrat::LongFormulaEncoder, smtrat::ExactlyOneCommanderEncoder, and smtrat::CardinalityEncoder.

Here is the caller graph for this function:

doEncode()

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

protectedpure virtual

Implemented in smtrat::TotalizerEncoder, smtrat::ShortFormulaEncoder, smtrat::RNSEncoder, smtrat::MixedSignEncoder, smtrat::LongFormulaEncoder, smtrat::ExactlyOneCommanderEncoder, and smtrat::CardinalityEncoder.

Here is the caller graph for this function:

encode()

std::optional< FormulaT > smtrat::PseudoBoolEncoder::encode

(

const ConstraintT &

constraint

)

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:

encodingSize()

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

virtual

Reimplemented in smtrat::TotalizerEncoder, smtrat::ShortFormulaEncoder, smtrat::MixedSignEncoder, smtrat::LongFormulaEncoder, smtrat::ExactlyOneCommanderEncoder, and smtrat::CardinalityEncoder.

Definition at line 33 of file PseudoBoolEncoder.cpp.

Here is the caller graph for this function:

generateVarChain()

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

protected

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()

virtual std::string smtrat::PseudoBoolEncoder::name ( )

inlinevirtual

Reimplemented in smtrat::TotalizerEncoder, smtrat::ShortFormulaEncoder, smtrat::MixedSignEncoder, smtrat::LongFormulaEncoder, smtrat::ExactlyOneCommanderEncoder, and smtrat::CardinalityEncoder.

Definition at line 25 of file PseudoBoolEncoder.h.

normalizeLessConstraint()

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

private

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

Definition at line 20 of file PseudoBoolEncoder.h.

---

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

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