SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
ShortFormulaEncoder.h
Go to the documentation of this file.
1
#pragma once
2
3
#include "
PseudoBoolEncoder.h
"
4
5
namespace
smtrat
{
6
class
ShortFormulaEncoder
:
public
PseudoBoolEncoder
{
7
public
:
8
ShortFormulaEncoder
() :
PseudoBoolEncoder
() {}
9
10
bool
canEncode
(
const
ConstraintT
& constraint);
11
12
Rational
encodingSize
(
const
ConstraintT
& constraint);
13
14
std::string
name
() {
return
"ShortFormulaEncoder"
; }
15
16
protected
:
17
std::optional<FormulaT>
doEncode
(
const
ConstraintT
& constraint);
18
19
};
20
}
PseudoBoolEncoder.h
smtrat::PseudoBoolEncoder
Base class for a PseudoBoolean Encoder.
Definition:
PseudoBoolEncoder.h:13
smtrat::ShortFormulaEncoder
Definition:
ShortFormulaEncoder.h:6
smtrat::ShortFormulaEncoder::name
std::string name()
Definition:
ShortFormulaEncoder.h:14
smtrat::ShortFormulaEncoder::ShortFormulaEncoder
ShortFormulaEncoder()
Definition:
ShortFormulaEncoder.h:8
smtrat::ShortFormulaEncoder::canEncode
bool canEncode(const ConstraintT &constraint)
Definition:
ShortFormulaEncoder.cpp:103
smtrat::ShortFormulaEncoder::doEncode
std::optional< FormulaT > doEncode(const ConstraintT &constraint)
Definition:
ShortFormulaEncoder.cpp:4
smtrat::ShortFormulaEncoder::encodingSize
Rational encodingSize(const ConstraintT &constraint)
Definition:
ShortFormulaEncoder.cpp:107
smtrat
Class to create the formulas for axioms.
Definition:
handle_options.h:10
smtrat::ConstraintT
carl::Constraint< Poly > ConstraintT
Definition:
types.h:29
smtrat::Rational
mpq_class Rational
Definition:
types.h:19
smtrat-modules
PBPPModule
Encoders
ShortFormulaEncoder.h
Generated by
1.9.1