stack_decision_procedure.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Decision procedure with incremental solving with contexts
        and assumptions
 
Author: Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H
#define CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H
 
#include <vector>
 
#include "decision_procedure.h"
 
class stack_decision_proceduret : public decision_proceduret
{
public:
  virtual void push(const std::vector<exprt> &assumptions) = 0;
 
  virtual void push() = 0;
 
  virtual void pop() = 0;
 
  virtual ~stack_decision_proceduret() = default;
};
class stack_decision_proceduret : public decision_proceduret {…};
 
#endif // CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H