SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Data Fields | Protected Member Functions | Private Member Functions | Private Attributes
smtrat::MixedSignEncoder Class Reference

#include <MixedSignEncoder.h>

Inheritance diagram for smtrat::MixedSignEncoder:
Inheritance graph
[legend]
Collaboration diagram for smtrat::MixedSignEncoder:
Collaboration graph
[legend]

Public Member Functions

 MixedSignEncoder ()
 
bool canEncode (const ConstraintT &constraint)
 
Rational encodingSize (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

FormulaT findSubEncoding (const ConstraintT &constraint)
 
std::vector< Rational > calculateSubsetsums (const std::vector< TermT > &terms)
 
void calculateSubsetsums (const std::vector< TermT > &terms, size_t leftIndex, std::set< Rational > &result, Rational sum=0)
 
ConstraintT normalizeLessConstraint (const ConstraintT &constraint)
 

Private Attributes

LongFormulaEncoder mLongFormulaEncoder
 
ShortFormulaEncoder mShortFormulaEncoder
 
CardinalityEncoder mCardinalityEncoder
 
PseudoBoolNormalizer mNormalizer
 

Detailed Description

Definition at line 10 of file MixedSignEncoder.h.

Constructor & Destructor Documentation

◆ MixedSignEncoder()

smtrat::MixedSignEncoder::MixedSignEncoder ( )
inline

Definition at line 12 of file MixedSignEncoder.h.

Member Function Documentation

◆ calculateSubsetsums() [1/2]

std::vector< Rational > smtrat::MixedSignEncoder::calculateSubsetsums ( const std::vector< TermT > &  terms)
private

Definition at line 145 of file MixedSignEncoder.cpp.

Here is the caller graph for this function:

◆ calculateSubsetsums() [2/2]

void smtrat::MixedSignEncoder::calculateSubsetsums ( const std::vector< TermT > &  terms,
size_t  leftIndex,
std::set< Rational > &  result,
Rational  sum = 0 
)
private

Definition at line 154 of file MixedSignEncoder.cpp.

Here is the call graph for this function:

◆ canEncode()

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

Implements smtrat::PseudoBoolEncoder.

Definition at line 99 of file MixedSignEncoder.cpp.

Here is the caller graph for this function:

◆ doEncode()

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

Implements smtrat::PseudoBoolEncoder.

Definition at line 4 of file MixedSignEncoder.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:

◆ encodingSize()

Rational smtrat::MixedSignEncoder::encodingSize ( const ConstraintT &  constraint)
virtual

Reimplemented from smtrat::PseudoBoolEncoder.

Definition at line 118 of file MixedSignEncoder.cpp.

Here is the call graph for this function:

◆ findSubEncoding()

FormulaT smtrat::MixedSignEncoder::findSubEncoding ( const ConstraintT &  constraint)
private

Definition at line 165 of file MixedSignEncoder.cpp.

Here is the call graph for this function:
Here is the caller 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::MixedSignEncoder::name ( )
inlinevirtual

Reimplemented from smtrat::PseudoBoolEncoder.

Definition at line 17 of file MixedSignEncoder.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

◆ mCardinalityEncoder

CardinalityEncoder smtrat::MixedSignEncoder::mCardinalityEncoder
private

Definition at line 26 of file MixedSignEncoder.h.

◆ mLongFormulaEncoder

LongFormulaEncoder smtrat::MixedSignEncoder::mLongFormulaEncoder
private

Definition at line 24 of file MixedSignEncoder.h.

◆ mNormalizer

PseudoBoolNormalizer smtrat::MixedSignEncoder::mNormalizer
private

Definition at line 27 of file MixedSignEncoder.h.

◆ mShortFormulaEncoder

ShortFormulaEncoder smtrat::MixedSignEncoder::mShortFormulaEncoder
private

Definition at line 25 of file MixedSignEncoder.h.

◆ 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: