SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
LongFormulaEncoder.h
Go to the documentation of this file.
1
#pragma once
2
3
#include "
PseudoBoolEncoder.h
"
4
5
namespace
smtrat
{
6
class
LongFormulaEncoder
:
public
PseudoBoolEncoder
{
7
public
:
8
LongFormulaEncoder
() :
PseudoBoolEncoder
() {}
9
10
bool
canEncode
(
const
ConstraintT
& constraint);
11
Rational
encodingSize
(
const
ConstraintT
& constraint);
12
13
std::string
name
() {
return
"LongFormulaEncoder"
; }
14
15
protected
:
16
std::optional<FormulaT>
doEncode
(
const
ConstraintT
& constraint);
17
18
};
19
}
PseudoBoolEncoder.h
smtrat::LongFormulaEncoder
Definition:
LongFormulaEncoder.h:6
smtrat::LongFormulaEncoder::doEncode
std::optional< FormulaT > doEncode(const ConstraintT &constraint)
Definition:
LongFormulaEncoder.cpp:4
smtrat::LongFormulaEncoder::encodingSize
Rational encodingSize(const ConstraintT &constraint)
Definition:
LongFormulaEncoder.cpp:117
smtrat::LongFormulaEncoder::LongFormulaEncoder
LongFormulaEncoder()
Definition:
LongFormulaEncoder.h:8
smtrat::LongFormulaEncoder::name
std::string name()
Definition:
LongFormulaEncoder.h:13
smtrat::LongFormulaEncoder::canEncode
bool canEncode(const ConstraintT &constraint)
Definition:
LongFormulaEncoder.cpp:96
smtrat::PseudoBoolEncoder
Base class for a PseudoBoolean Encoder.
Definition:
PseudoBoolEncoder.h:13
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
LongFormulaEncoder.h
Generated by
1.9.1