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 {
7  public:
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 }
std::optional< FormulaT > doEncode(const ConstraintT &constraint)
Rational encodingSize(const ConstraintT &constraint)
bool canEncode(const ConstraintT &constraint)
Base class for a PseudoBoolean Encoder.
Class to create the formulas for axioms.
carl::Constraint< Poly > ConstraintT
Definition: types.h:29
mpq_class Rational
Definition: types.h:19