CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
conflict_provider.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Capability to check whether an expression is a reason for
4 the solver returning UNSAT
5
6Author: Peter Schrammel
7
8\*******************************************************************/
9
13
14#ifndef CPROVER_SOLVERS_CONFLICT_PROVIDER_H
15#define CPROVER_SOLVERS_CONFLICT_PROVIDER_H
16
17class exprt;
18
20{
21public:
25 virtual bool is_in_conflict(const exprt &) const = 0;
26
27 virtual ~conflict_providert() = default;
28};
29
30#endif // CPROVER_SOLVERS_CONFLICT_PROVIDER_H
virtual ~conflict_providert()=default
virtual bool is_in_conflict(const exprt &) const =0
Returns true if an expression is in the final conflict leading to UNSAT.
Base class for all expressions.
Definition expr.h:56