cprover
qdimacs_core.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_QBF_QDIMACS_CORE_H
11 #define CPROVER_SOLVERS_QBF_QDIMACS_CORE_H
12 
13 #include <map>
14 
15 #include <util/expr.h>
16 
17 #include "qdimacs_cnf.h"
18 
20 {
21 public:
22  virtual tvt l_get(literalt a) const=0;
23  virtual bool is_in_core(literalt l) const=0;
24 
26  virtual modeltypet m_get(literalt a) const=0;
27 
28  typedef std::pair<exprt, unsigned> symbol_mapt;
29  typedef std::map<unsigned, symbol_mapt> variable_mapt;
30  variable_mapt variable_map; // variable -> symbol/index map
31  virtual const exprt f_get(literalt v)=0;
32 
33  void simplify_extractbits(exprt &expr) const;
34 };
35 
36 #endif // CPROVER_SOLVERS_QBF_QDIMACS_CORE_H
variable_mapt variable_map
Definition: qdimacs_core.h:30
void simplify_extractbits(exprt &expr) const
std::map< unsigned, symbol_mapt > variable_mapt
Definition: qdimacs_core.h:29
virtual const exprt f_get(literalt v)=0
Definition: threeval.h:19
virtual modeltypet m_get(literalt a) const =0
virtual bool is_in_core(literalt l) const =0
Base class for all expressions.
Definition: expr.h:54
virtual tvt l_get(literalt a) const =0
std::pair< exprt, unsigned > symbol_mapt
Definition: qdimacs_core.h:28