cprover
cnf_clause_list.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CNF Generation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "cnf_clause_list.h"
13 
14 #include <cassert>
15 #include <ostream>
16 
17 void cnf_clause_listt::lcnf(const bvt &bv)
18 {
19  bvt new_bv;
20 
21  if(process_clause(bv, new_bv))
22  return;
23 
24  clauses.push_back(new_bv);
25 }
26 
27 void cnf_clause_list_assignmentt::print_assignment(std::ostream &out) const
28 {
29  for(unsigned v=1; v<assignment.size(); v++)
30  out << "v" << v << "=" << assignment[v] << "\n";
31 }
32 
34 {
35  assignment.resize(no_variables());
36 
37  // we don't use index 0, start with 1
38  for(unsigned v=1; v<assignment.size(); v++)
39  {
40  literalt l;
41  l.set(v, false);
42  assignment[v]=prop.l_get(l);
43  }
44 }
void print_assignment(std::ostream &out) const
bool process_clause(const bvt &bv, bvt &dest)
filter &#39;true&#39; from clause, eliminate duplicates, recognise trivially satisfied clauses ...
Definition: cnf.cpp:416
CNF Generation.
virtual void copy_assignment_from(const propt &prop)
virtual void lcnf(const bvt &bv)
void set(var_not _l)
Definition: literal.h:92
TO_BE_DOCUMENTED.
Definition: prop.h:22
virtual tvt l_get(literalt a) const =0
virtual size_t no_variables() const override
Definition: cnf.h:38
std::vector< literalt > bvt
Definition: literal.h:197