smtrat::RNSEncoder Class Reference

#include <RNSEncoder.h>

Inheritance diagram for smtrat::RNSEncoder:

Collaboration diagram for smtrat::RNSEncoder:

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

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
bool	isNonRedundant (const std::vector< Integer > &base, const ConstraintT &formula)
std::vector< Integer >	integerFactorization (const Integer &coeff)
std::vector< std::vector< Integer > >	primesTable ()
std::vector< Integer >	calculateRNSBase (const ConstraintT &formula)
FormulaT	rnsTransformation (const ConstraintT &formula, const Integer &prime)
ConstraintT	normalizeLessConstraint (const ConstraintT &constraint)

Private Attributes
const std::vector< std::vector< Integer > >	mPrimesTable

Detailed Description

Definition at line 9 of file RNSEncoder.h.

Constructor & Destructor Documentation

RNSEncoder()

smtrat::RNSEncoder::RNSEncoder ( )

inline

Definition at line 11 of file RNSEncoder.h.

Member Function Documentation

calculateRNSBase()

std::vector< Integer > smtrat::RNSEncoder::calculateRNSBase ( const ConstraintT &  formula )

private

Definition at line 94 of file RNSEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

canEncode()

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

virtual

Implements smtrat::PseudoBoolEncoder.

Definition at line 230 of file RNSEncoder.cpp.

doEncode()

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

protectedvirtual

Implements smtrat::PseudoBoolEncoder.

Definition at line 7 of file RNSEncoder.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::PseudoBoolEncoder::encodingSize ( const ConstraintT &  constraint )

virtualinherited

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  )

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:

integerFactorization()

std::vector< Integer > smtrat::RNSEncoder::integerFactorization ( const Integer &  coeff )

private

Definition at line 158 of file RNSEncoder.cpp.

Here is the caller graph for this function:

isNonRedundant()

bool smtrat::RNSEncoder::isNonRedundant ( const std::vector< Integer > &  base, const ConstraintT &  formula  )

private

Definition at line 22 of file RNSEncoder.cpp.

Here is the caller graph for this function:

name()

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

inlinevirtualinherited

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 )

privateinherited

Definition at line 25 of file PseudoBoolEncoder.cpp.

Here is the caller graph for this function:

primesTable()

std::vector< std::vector< Integer > > smtrat::RNSEncoder::primesTable ( )

private

Definition at line 234 of file RNSEncoder.cpp.

rnsTransformation()

FormulaT smtrat::RNSEncoder::rnsTransformation ( const ConstraintT &  formula, const Integer &  prime  )

private

Definition at line 54 of file RNSEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

mPrimesTable

const std::vector<std::vector<Integer> > smtrat::RNSEncoder::mPrimesTable

private

Definition at line 19 of file RNSEncoder.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:

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