cprover
qdimacs_cnf.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_QBF_QDIMACS_CNF_H
11 #define CPROVER_SOLVERS_QBF_QDIMACS_CNF_H
12 
13 #include <set>
14 #include <iosfwd>
15 
16 #include <solvers/sat/dimacs_cnf.h>
17 
19 {
20 public:
22  virtual ~qdimacs_cnft() { }
23 
24  virtual void write_qdimacs_cnf(std::ostream &out);
25 
26  // dummy functions
27 
28  virtual const std::string solver_text()
29  {
30  return "QDIMACS CNF";
31  }
32 
34  {
35  public:
36  enum class typet { NONE, EXISTENTIAL, UNIVERSAL };
38  unsigned var_no;
39 
41  {
42  }
43 
44  quantifiert(typet _type, literalt _l):type(_type), var_no(_l.var_no())
45  {
46  }
47 
48  bool operator==(const quantifiert &other) const
49  {
50  return type==other.type && var_no==other.var_no;
51  }
52 
53  size_t hash() const
54  {
55  return var_no^(static_cast<int>(type)<<24);
56  }
57  };
58 
59  // quantifiers
60  typedef std::vector<quantifiert> quantifierst;
62 
63  virtual void add_quantifier(const quantifiert &quantifier)
64  {
65  quantifiers.push_back(quantifier);
66  }
67 
68  void add_quantifier(const quantifiert::typet type, const literalt l)
69  {
70  add_quantifier(quantifiert(type, l));
71  }
72 
74  {
76  }
77 
79  {
81  }
82 
83  bool is_quantified(const literalt l) const;
84  bool find_quantifier(const literalt l, quantifiert &q) const;
85 
86  virtual void set_quantifier(const quantifiert::typet type, const literalt l);
87  void copy_to(qdimacs_cnft &cnf) const;
88 
89  bool operator==(const qdimacs_cnft &other) const;
90 
91  size_t hash() const;
92 
93 protected:
94  void write_prefix(std::ostream &out) const;
95 };
96 
97 #endif // CPROVER_SOLVERS_QBF_QDIMACS_CNF_H
The type of an expression.
Definition: type.h:22
void write_prefix(std::ostream &out) const
Definition: qdimacs_cnf.cpp:21
size_t hash() const
bool is_quantified(const literalt l) const
virtual void add_quantifier(const quantifiert &quantifier)
Definition: qdimacs_cnf.h:63
bool operator==(const qdimacs_cnft &other) const
Definition: qdimacs_cnf.cpp:64
virtual const std::string solver_text()
Definition: qdimacs_cnf.h:28
quantifiert(typet _type, literalt _l)
Definition: qdimacs_cnf.h:44
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
Definition: qdimacs_cnf.cpp:69
bool find_quantifier(const literalt l, quantifiert &q) const
void add_existential_quantifier(const literalt l)
Definition: qdimacs_cnf.h:73
std::vector< quantifiert > quantifierst
Definition: qdimacs_cnf.h:60
quantifierst quantifiers
Definition: qdimacs_cnf.h:61
void add_quantifier(const quantifiert::typet type, const literalt l)
Definition: qdimacs_cnf.h:68
void copy_to(qdimacs_cnft &cnf) const
Definition: qdimacs_cnf.cpp:86
void add_universal_quantifier(const literalt l)
Definition: qdimacs_cnf.h:78
virtual ~qdimacs_cnft()
Definition: qdimacs_cnf.h:22
bool operator==(const quantifiert &other) const
Definition: qdimacs_cnf.h:48
virtual void write_qdimacs_cnf(std::ostream &out)
Definition: qdimacs_cnf.cpp:14