cprover
qdimacs_cnf.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "qdimacs_cnf.h"
10 
11 #include <iostream>
12 #include <cassert>
13 
14 void qdimacs_cnft::write_qdimacs_cnf(std::ostream &out)
15 {
16  write_problem_line(out);
17  write_prefix(out);
18  write_clauses(out);
19 }
20 
21 void qdimacs_cnft::write_prefix(std::ostream &out) const
22 {
23  std::vector<bool> quantified;
24 
25  quantified.resize(no_variables(), false);
26 
27  for(quantifierst::const_iterator
28  it=quantifiers.begin();
29  it!=quantifiers.end();
30  it++)
31  {
32  const quantifiert &quantifier=*it;
33 
34  assert(quantifier.var_no<no_variables());
35  // double quantification?
36  assert(!quantified[quantifier.var_no]);
37  quantified[quantifier.var_no]=true;
38 
39  switch(quantifier.type)
40  {
42  out << "a";
43  break;
44 
46  out << "e";
47  break;
48 
49  default:
50  assert(false);
51  }
52 
53  out << " " << quantifier.var_no << " 0\n";
54  }
55 
56  // variables that are not quantified
57  // will be quantified existentially in the innermost scope
58 
59  for(std::size_t i=1; i<no_variables(); i++)
60  if(!quantified[i])
61  out << "e " << i << " 0\n";
62 }
63 
64 bool qdimacs_cnft::operator==(const qdimacs_cnft &other) const
65 {
66  return quantifiers==other.quantifiers && clauses==other.clauses;
67 }
68 
70  const quantifiert::typet type,
71  const literalt l)
72 {
73  for(quantifierst::iterator it=quantifiers.begin();
74  it!=quantifiers.end();
75  it++)
76  if(it->var_no==l.var_no())
77  {
78  it->type=type;
79  return;
80  }
81 
82  // variable not found - let's add a new quantifier.
83  add_quantifier(type, l);
84 }
85 
87 {
89 
90  for(quantifierst::const_iterator
91  it=quantifiers.begin();
92  it!=quantifiers.end();
93  it++)
94  cnf.add_quantifier(*it);
95 
96  for(clausest::const_iterator
97  it=clauses.begin();
98  it!=clauses.end();
99  it++)
100  cnf.lcnf(*it);
101 }
102 
103 size_t qdimacs_cnft::hash() const
104 {
105  size_t result=0;
106 
107  for(quantifierst::const_iterator it=quantifiers.begin();
108  it!=quantifiers.end();
109  it++)
110  result=((result<<1)^it->hash())-result;
111 
112  return result^cnf_clause_listt::hash();
113 }
114 
116 {
117  for(quantifierst::const_iterator it=quantifiers.begin();
118  it!=quantifiers.end();
119  it++)
120  if(it->var_no==l.var_no())
121  return true;
122 
123  return false;
124 }
125 
127 {
128  for(quantifierst::const_iterator it=quantifiers.begin();
129  it!=quantifiers.end();
130  it++)
131  if(it->var_no==l.var_no())
132  {
133  q=*it;
134  return true;
135  }
136 
137  return false;
138 }
mstreamt & result()
Definition: message.h:233
void write_prefix(std::ostream &out) const
Definition: qdimacs_cnf.cpp:21
size_t _no_variables
Definition: cnf.h:53
size_t hash() const
bool is_quantified(const literalt l) const
void write_clauses(std::ostream &out)
Definition: dimacs_cnf.cpp:61
virtual void add_quantifier(const quantifiert &quantifier)
Definition: qdimacs_cnf.h:63
bool operator==(const qdimacs_cnft &other) const
Definition: qdimacs_cnf.cpp:64
size_t hash() const
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
Definition: qdimacs_cnf.cpp:69
var_not var_no() const
Definition: literal.h:82
virtual void lcnf(const bvt &bv)
bool find_quantifier(const literalt l, quantifiert &q) const
virtual void set_no_variables(size_t no)
Definition: cnf.h:39
quantifierst quantifiers
Definition: qdimacs_cnf.h:61
void write_problem_line(std::ostream &out)
Definition: dimacs_cnf.cpp:28
void copy_to(qdimacs_cnft &cnf) const
Definition: qdimacs_cnf.cpp:86
virtual size_t no_variables() const override
Definition: cnf.h:38
virtual void write_qdimacs_cnf(std::ostream &out)
Definition: qdimacs_cnf.cpp:14