Skip to content

Commit 3d1da60

Browse files
Add assumptions capability interface
1 parent 97c1cde commit 3d1da60

File tree

1 file changed

+27
-0
lines changed

1 file changed

+27
-0
lines changed

src/solvers/prop/prop_assumption.h

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
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_ASSUMPTION_H
13+
#define CPROVER_SOLVERS_PROP_PROP_ASSUMPTION_H
14+
15+
class prop_assumptiont
16+
{
17+
public:
18+
virtual void set_frozen(literalt) = 0;
19+
virtual void set_frozen(const bvt &) = 0;
20+
virtual void set_assumptions(const bvt &) = 0;
21+
virtual void set_all_frozen() = 0;
22+
virtual bool is_in_conflict(literalt) const = 0;
23+
24+
virtual ~prop_assumptiont() = default;
25+
};
26+
27+
#endif // CPROVER_SOLVERS_PROP_PROP_ASSUMPTION_H

0 commit comments

Comments
 (0)