cprover
Loading...
Searching...
No Matches
qdimacs_cnf.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 <iosfwd>
14
16
18{
19public:
20 explicit qdimacs_cnft(message_handlert &message_handler)
21 : dimacs_cnft(message_handler)
22 {
23 }
24 virtual ~qdimacs_cnft() { }
25
26 virtual void write_qdimacs_cnf(std::ostream &out);
27
28 // dummy functions
29
30 virtual const std::string solver_text()
31 {
32 return "QDIMACS CNF";
33 }
34
36 {
37 public:
38 enum class typet { NONE, EXISTENTIAL, UNIVERSAL };
40 unsigned var_no;
41
43 {
44 }
45
47 {
48 }
49
50 bool operator==(const quantifiert &other) const
51 {
52 return type==other.type && var_no==other.var_no;
53 }
54
55 size_t hash() const
56 {
57 return var_no^(static_cast<int>(type)<<24);
58 }
59 };
60
61 // quantifiers
62 typedef std::vector<quantifiert> quantifierst;
64
66 {
67 quantifiers.push_back(quantifier);
68 }
69
70 void add_quantifier(const quantifiert::typet type, const literalt l)
71 {
73 }
74
79
84
85 bool is_quantified(const literalt l) const;
86 bool find_quantifier(const literalt l, quantifiert &q) const;
87
88 virtual void set_quantifier(const quantifiert::typet type, const literalt l);
89 void copy_to(qdimacs_cnft &cnf) const;
90
91 bool operator==(const qdimacs_cnft &other) const;
92
93 size_t hash() const;
94
95protected:
96 void write_prefix(std::ostream &out) const;
97};
98
99#endif // CPROVER_SOLVERS_QBF_QDIMACS_CNF_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
quantifiert(typet _type, literalt _l)
Definition qdimacs_cnf.h:46
bool operator==(const quantifiert &other) const
Definition qdimacs_cnf.h:50
virtual const std::string solver_text()
Definition qdimacs_cnf.h:30
virtual void add_quantifier(const quantifiert &quantifier)
Definition qdimacs_cnf.h:65
bool find_quantifier(const literalt l, quantifiert &q) const
virtual ~qdimacs_cnft()
Definition qdimacs_cnf.h:24
void write_prefix(std::ostream &out) const
virtual void write_qdimacs_cnf(std::ostream &out)
void add_universal_quantifier(const literalt l)
Definition qdimacs_cnf.h:80
size_t hash() const
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
std::vector< quantifiert > quantifierst
Definition qdimacs_cnf.h:62
void add_quantifier(const quantifiert::typet type, const literalt l)
Definition qdimacs_cnf.h:70
bool operator==(const qdimacs_cnft &other) const
quantifierst quantifiers
Definition qdimacs_cnf.h:63
void copy_to(qdimacs_cnft &cnf) const
void add_existential_quantifier(const literalt l)
Definition qdimacs_cnf.h:75
qdimacs_cnft(message_handlert &message_handler)
Definition qdimacs_cnf.h:20
bool is_quantified(const literalt l) const
The type of an expression, extends irept.
Definition type.h:29