symbolic.h

 
#pragma once
 
#include <functional>
#include <ostream>
#include <set>
#include <string>
#include <vector>
 
// From drake
// IWYU pragma: begin_exports
#include "dlinear/symbolic/symbolic_environment.h"
#include "dlinear/symbolic/symbolic_expression.h"
#include "dlinear/symbolic/symbolic_expression_cell.h"
#include "dlinear/symbolic/symbolic_expression_visitor.h"
#include "dlinear/symbolic/symbolic_formula.h"
#include "dlinear/symbolic/symbolic_formula_visitor.h"
#include "dlinear/symbolic/symbolic_variables.h"
// IWYU pragma: end_exports
 
// From dlinear
#include "dlinear/symbolic/hash.h"
#include "dlinear/symbolic/literal.h"
 
namespace dlinear {
 
using drake::symbolic::Environment;
using drake::symbolic::Expression;
using drake::symbolic::ExpressionAddFactory;
using drake::symbolic::ExpressionKind;
using drake::symbolic::Formula;
using drake::symbolic::FormulaKind;
using drake::symbolic::Variables;
using drake::symbolic::VisitExpression;
using drake::symbolic::VisitFormula;
 
FormulaKind operator-(FormulaKind kind);
 
Formula imply(const Formula &f1, const Formula &f2);
Formula imply(const Variable &v, const Formula &f);
Formula imply(const Formula &f, const Variable &v);
Formula imply(const Variable &v1, const Variable &v2);
 
Formula iff(const Formula &f1, const Formula &f2);
Formula iff(const Variable &v, const Formula &f);
Formula iff(const Formula &f, const Variable &v);
Formula iff(const Variable &v1, const Variable &v2);
 
std::set<Formula> map(const std::set<Formula> &formulas, const std::function<Formula(const Formula &)> &func);
 
bool is_atomic(const Formula &f);
 
bool is_clause(const Formula &f);
 
std::set<Formula> get_clauses(const Formula &f);
 
bool is_cnf(const Formula &f);
 
bool HaveIntersection(const Variables &variables1, const Variables &variables2);
 
Formula DeltaStrengthen(const Formula &f, double delta);
 
Formula DeltaWeaken(const Formula &f, double delta);
 
bool IsDifferentiable(const Formula &f);
 
bool IsDifferentiable(const Expression &e);
 
Formula make_conjunction(const std::vector<Formula> &formulas);
 
Formula make_disjunction(const std::vector<Formula> &formulas);
 
std::vector<Variable> CreateVector(const std::string &prefix, int size,
                                   Variable::Type type = Variable::Type::CONTINUOUS);
 
enum class RelationalOperator {
  EQ,   
  NEQ,  
  GT,   
  GEQ,  
  LT,   
  LEQ,  
};
 
RelationalOperator operator!(RelationalOperator op);
 
std::ostream &operator<<(std::ostream &os, RelationalOperator op);
 
std::ostream &operator<<(std::ostream &os, const FormulaKind &kind);
 
std::ostream &operator<<(std::ostream &os, const ExpressionKind &kind);
 
}  // namespace dlinear
 
#ifdef DLINEAR_INCLUDE_FMT
 
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::Expression)
OSTREAM_FORMATTER(dlinear::Formula)
OSTREAM_FORMATTER(dlinear::Variables)
OSTREAM_FORMATTER(dlinear::RelationalOperator)
OSTREAM_FORMATTER(dlinear::FormulaKind)
OSTREAM_FORMATTER(dlinear::ExpressionKind)
 
#endif