conflict_provider.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Capability to check whether an expression is a reason for
        the solver returning UNSAT
 
Author: Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_SOLVERS_CONFLICT_PROVIDER_H
#define CPROVER_SOLVERS_CONFLICT_PROVIDER_H
 
class exprt;
 
class conflict_providert
{
public:
  virtual bool is_in_conflict(const exprt &) const = 0;
 
  virtual ~conflict_providert() = default;
};
class conflict_providert {…};
 
#endif // CPROVER_SOLVERS_CONFLICT_PROVIDER_H