conflict_providert Class Referenceabstract
#include <conflict_provider.h>
Inheritance diagram for conflict_providert:Public Member Functions | |
| virtual bool | is_in_conflict (const exprt &) const =0 |
| Returns true if an expression is in the final conflict leading to UNSAT. More... | |
| virtual | ~conflict_providert ()=default |
Detailed Description
Definition at line 19 of file conflict_provider.h.
Constructor & Destructor Documentation
◆ ~conflict_providert()
|
virtualdefault |
Member Function Documentation
◆ is_in_conflict()
|
pure virtual |
Returns true if an expression is in the final conflict leading to UNSAT.
The argument can be a Boolean expression or something more solver-specific, e.g. a literal_exprt.
Implemented in prop_conv_solvert.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/solvers/conflict_provider.h
