CBMC
conflict_provider.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Capability to check whether an expression is a reason for
4  the solver returning UNSAT
5 
6 Author: Peter Schrammel
7 
8 \*******************************************************************/
9 
13 
14 #ifndef CPROVER_SOLVERS_CONFLICT_PROVIDER_H
15 #define CPROVER_SOLVERS_CONFLICT_PROVIDER_H
16 
17 class exprt;
18 
19 class conflict_providert
20 {
21 public:
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
conflict_providert
Definition: conflict_provider.h:20
conflict_providert::~conflict_providert
virtual ~conflict_providert()=default
conflict_providert::is_in_conflict
virtual bool is_in_conflict(const exprt &) const =0
Returns true if an expression is in the final conflict leading to UNSAT.
exprt
Base class for all expressions.
Definition: expr.h:56