In Formula.hpp we define classes TrueFormula and FalseFormula:
class TrueFormula : public Formula
{
friend class Formulas;
public:
TrueFormula(std::string label = "") : Formula(label) {}
Type type() const override { return Formula::Type::True; }
std::string toSMTLIB(unsigned indentation = 0) const override;
std::string prettyString(unsigned indentation = 0) const override;
};
class FalseFormula : public Formula
{
friend class Formulas;
public:
FalseFormula(std::string label = "") : Formula(label) {}
Type type() const override { return Formula::Type::False; }
std::string toSMTLIB(unsigned indentation = 0) const override;
std::string prettyString(unsigned indentation = 0) const override;
};
But then never use these elsewhere. Instead the function boolTrue() declared in Theory.hpp creates a predicate formula with name true. We should either remove these two classes or update Theory.hpp to make use of them.
In Formula.hpp we define classes
TrueFormulaandFalseFormula:But then never use these elsewhere. Instead the function
boolTrue()declared inTheory.hppcreates a predicate formula with nametrue. We should either remove these two classes or updateTheory.hppto make use of them.