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