Skip to content

Commit 89507b4

Browse files
Add contexts capability interface
1 parent 3d1da60 commit 89507b4

File tree

1 file changed

+28
-0
lines changed

1 file changed

+28
-0
lines changed

src/solvers/prop/prop_context.h

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
/*******************************************************************\
2+
3+
Module: Context-based Incremental Solver Interface
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Context-based interface for incremental solvers
11+
12+
#ifndef CPROVER_SOLVERS_PROP_PROP_CONTEXT_H
13+
#define CPROVER_SOLVERS_PROP_PROP_CONTEXT_H
14+
15+
class prop_contextt
16+
{
17+
public:
18+
/// Push a new context on the stack
19+
/// This context becomes a child context nested in the current context.
20+
virtual void push_context() = 0;
21+
22+
/// Pop the current context
23+
virtual void pop_context() = 0;
24+
25+
virtual ~prop_contextt() = default;
26+
};
27+
28+
#endif // CPROVER_SOLVERS_PROP_PROP_CONTEXT_H

0 commit comments

Comments
 (0)