CBMC
stack_decision_procedure.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Decision procedure with incremental solving with contexts
4  and assumptions
5 
6 Author: Peter Schrammel
7 
8 \*******************************************************************/
9 
49 
50 #ifndef CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H
51 #define CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H
52 
53 #include <vector>
54 
55 #include "decision_procedure.h"
56 
57 class stack_decision_proceduret : public decision_proceduret
58 {
59 public:
68  virtual void push(const std::vector<exprt> &assumptions) = 0;
69 
72  virtual void push() = 0;
73 
76  virtual void pop() = 0;
77 
78  virtual ~stack_decision_proceduret() = default;
79 };
80 
81 #endif // CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H
decision_proceduret
An interface for a decision procedure for satisfiability problems.
Definition: decision_procedure.h:22
stack_decision_proceduret
Definition: stack_decision_procedure.h:58
stack_decision_proceduret::push
virtual void push()=0
Push a new context on the stack This context becomes a child context nested in the current context.
stack_decision_proceduret::pop
virtual void pop()=0
Pop whatever is on top of the stack.
stack_decision_proceduret::push
virtual void push(const std::vector< exprt > &assumptions)=0
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
stack_decision_proceduret::~stack_decision_proceduret
virtual ~stack_decision_proceduret()=default
decision_procedure.h
Decision Procedure Interface.