dReal4
filter_assertion.h
1 #pragma once
2 
3 #include "dreal/symbolic/symbolic.h"
4 #include "dreal/util/box.h"
5 
6 namespace dreal {
7 
8 enum class FilterAssertionResult {
9  NotFiltered,
10  FilteredWithChange,
11  FilteredWithoutChange,
12 };
13 
14 /// If the @p assertion can be applied into the @p box update @p box
15 /// and return true. Otherwise, return false while keeping @p box
16 /// intact.
17 FilterAssertionResult FilterAssertion(const Formula& assertion, Box* box);
18 } // namespace dreal
dreal
Sum type of symbolic::Expression and symbolic::Formula.
Definition: api.cc:9
dreal::FilterAssertion
FilterAssertionResult FilterAssertion(const Formula &assertion, Box *const box)
If the assertion can be applied into the box update box and return true.
Definition: filter_assertion.cc:348
symbolic.h
This is the header file that we consolidate Drake's symbolic classes and expose them inside of dreal ...