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:
21  explicit qdimacs_cnft(message_handlert &message_handler)
22  : dimacs_cnft(message_handler)
23  {
24  }
25  virtual ~qdimacs_cnft() { }
26 
27  virtual void write_qdimacs_cnf(std::ostream &out);
28 
29  // dummy functions
30 
31  virtual const std::string solver_text()
32  {
33  return "QDIMACS CNF";
34  }
35 
37  {
38  public:
39  enum class typet { NONE, EXISTENTIAL, UNIVERSAL };
41  unsigned var_no;
42 
44  {
45  }
46 
47  quantifiert(typet _type, literalt _l):type(_type), var_no(_l.var_no())
48  {
49  }
50 
51  bool operator==(const quantifiert &other) const
52  {
53  return type==other.type && var_no==other.var_no;
54  }
55 
56  size_t hash() const
57  {
58  return var_no^(static_cast<int>(type)<<24);
59  }
60  };
61 
62  // quantifiers
63  typedef std::vector<quantifiert> quantifierst;
65 
66  virtual void add_quantifier(const quantifiert &quantifier)
67  {
68  quantifiers.push_back(quantifier);
69  }
70 
71  void add_quantifier(const quantifiert::typet type, const literalt l)
72  {
73  add_quantifier(quantifiert(type, l));
74  }
75 
77  {
79  }
80 
82  {
84  }
85 
86  bool is_quantified(const literalt l) const;
87  bool find_quantifier(const literalt l, quantifiert &q) const;
88 
89  virtual void set_quantifier(const quantifiert::typet type, const literalt l);
90  void copy_to(qdimacs_cnft &cnf) const;
91 
92  bool operator==(const qdimacs_cnft &other) const;
93 
94  size_t hash() const;
95 
96 protected:
97  void write_prefix(std::ostream &out) const;
98 };
99 
100 #endif // CPROVER_SOLVERS_QBF_QDIMACS_CNF_H
complexity_violationt::NONE
@ NONE
qdimacs_cnft::copy_to
void copy_to(qdimacs_cnft &cnf) const
Definition: qdimacs_cnf.cpp:90
qdimacs_cnft::hash
size_t hash() const
Definition: qdimacs_cnf.cpp:107
qdimacs_cnft::quantifierst
std::vector< quantifiert > quantifierst
Definition: qdimacs_cnf.h:63
qdimacs_cnft::~qdimacs_cnft
virtual ~qdimacs_cnft()
Definition: qdimacs_cnf.h:25
qdimacs_cnft::write_qdimacs_cnf
virtual void write_qdimacs_cnf(std::ostream &out)
Definition: qdimacs_cnf.cpp:15
typet
The type of an expression, extends irept.
Definition: type.h:29
qdimacs_cnft::is_quantified
bool is_quantified(const literalt l) const
Definition: qdimacs_cnf.cpp:119
qdimacs_cnft::write_prefix
void write_prefix(std::ostream &out) const
Definition: qdimacs_cnf.cpp:22
qdimacs_cnft::add_quantifier
void add_quantifier(const quantifiert::typet type, const literalt l)
Definition: qdimacs_cnf.h:71
qdimacs_cnft::add_existential_quantifier
void add_existential_quantifier(const literalt l)
Definition: qdimacs_cnf.h:76
qdimacs_cnft::find_quantifier
bool find_quantifier(const literalt l, quantifiert &q) const
Definition: qdimacs_cnf.cpp:130
qdimacs_cnft::quantifiert::typet::UNIVERSAL
@ UNIVERSAL
qdimacs_cnft::quantifiert::typet
typet
Definition: qdimacs_cnf.h:39
qdimacs_cnft::quantifiert::typet::NONE
@ NONE
qdimacs_cnft::solver_text
virtual const std::string solver_text()
Definition: qdimacs_cnf.h:31
qdimacs_cnft::quantifiert::type
typet type
Definition: qdimacs_cnf.h:40
qdimacs_cnft::set_quantifier
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
Definition: qdimacs_cnf.cpp:73
message_handlert
Definition: message.h:28
qdimacs_cnft::quantifiert::quantifiert
quantifiert(typet _type, literalt _l)
Definition: qdimacs_cnf.h:47
qdimacs_cnft::quantifiert::typet::EXISTENTIAL
@ EXISTENTIAL
qdimacs_cnft::quantifiert::quantifiert
quantifiert()
Definition: qdimacs_cnf.h:43
qdimacs_cnft::quantifiert::hash
size_t hash() const
Definition: qdimacs_cnf.h:56
qdimacs_cnft::add_universal_quantifier
void add_universal_quantifier(const literalt l)
Definition: qdimacs_cnf.h:81
dimacs_cnf.h
qdimacs_cnft::quantifiers
quantifierst quantifiers
Definition: qdimacs_cnf.h:64
qdimacs_cnft
Definition: qdimacs_cnf.h:19
qdimacs_cnft::operator==
bool operator==(const qdimacs_cnft &other) const
Definition: qdimacs_cnf.cpp:68
qdimacs_cnft::qdimacs_cnft
qdimacs_cnft(message_handlert &message_handler)
Definition: qdimacs_cnf.h:21
literalt
Definition: literal.h:26
qdimacs_cnft::quantifiert::operator==
bool operator==(const quantifiert &other) const
Definition: qdimacs_cnf.h:51
qdimacs_cnft::quantifiert::var_no
unsigned var_no
Definition: qdimacs_cnf.h:41
qdimacs_cnft::quantifiert
Definition: qdimacs_cnf.h:37
dimacs_cnft
Definition: dimacs_cnf.h:18
qdimacs_cnft::add_quantifier
virtual void add_quantifier(const quantifiert &quantifier)
Definition: qdimacs_cnf.h:66