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
33
void
cnf_clause_list_assignmentt::copy_assignment_from
(
const
propt
&prop)
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
}
cnf_clause_list_assignmentt::print_assignment
void print_assignment(std::ostream &out) const
Definition:
cnf_clause_list.cpp:27
cnft::process_clause
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses ...
Definition:
cnf.cpp:416
cnf_clause_list.h
CNF Generation.
cnf_clause_list_assignmentt::copy_assignment_from
virtual void copy_assignment_from(const propt &prop)
Definition:
cnf_clause_list.cpp:33
cnf_clause_listt::clauses
clausest clauses
Definition:
cnf_clause_list.h:76
literalt
Definition:
literal.h:24
cnf_clause_listt::lcnf
virtual void lcnf(const bvt &bv)
Definition:
cnf_clause_list.cpp:17
literalt::set
void set(var_not _l)
Definition:
literal.h:92
propt
TO_BE_DOCUMENTED.
Definition:
prop.h:22
cnf_clause_list_assignmentt::assignment
assignmentt assignment
Definition:
cnf_clause_list.h:112
propt::l_get
virtual tvt l_get(literalt a) const =0
cnft::no_variables
virtual size_t no_variables() const override
Definition:
cnf.h:38
bvt
std::vector< literalt > bvt
Definition:
literal.h:197
solvers
sat
cnf_clause_list.cpp
Generated by
1.8.14