symbolic_formula_visitor.h

#pragma once
 
#include <utility>
 
#include "dlinear/symbolic/symbolic_formula.h"
 
namespace dlinear::drake::symbolic {
 
template<typename Result, typename Visitor, typename... Args>
Result VisitFormula(Visitor *v, const Formula &f, Args &&... args) {
  switch (f.get_kind()) {
    case FormulaKind::False:return v->VisitFalse(f, std::forward<Args>(args)...);
    case FormulaKind::True:return v->VisitTrue(f, std::forward<Args>(args)...);
    case FormulaKind::Var:return v->VisitVariable(f, std::forward<Args>(args)...);
    case FormulaKind::Eq:return v->VisitEqualTo(f, std::forward<Args>(args)...);
    case FormulaKind::Neq:return v->VisitNotEqualTo(f, std::forward<Args>(args)...);
    case FormulaKind::Gt:return v->VisitGreaterThan(f, std::forward<Args>(args)...);
    case FormulaKind::Geq:return v->VisitGreaterThanOrEqualTo(f, std::forward<Args>(args)...);
    case FormulaKind::Lt:return v->VisitLessThan(f, std::forward<Args>(args)...);
    case FormulaKind::Leq:return v->VisitLessThanOrEqualTo(f, std::forward<Args>(args)...);
    case FormulaKind::And:return v->VisitConjunction(f, std::forward<Args>(args)...);
    case FormulaKind::Or:return v->VisitDisjunction(f, std::forward<Args>(args)...);
    case FormulaKind::Not:return v->VisitNegation(f, std::forward<Args>(args)...);
    case FormulaKind::Forall:return v->VisitForall(f, std::forward<Args>(args)...);
  }
  // Should not be reachable. But we need the following to avoid "control
  // reaches end of non-void function" gcc-warning.
  throw std::runtime_error("Should not be reachable.");
}
 
} // namespace dlinear::drake::symbolic