cprover
prop.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 "
prop.h
"
10
12
void
propt::set_equal
(
literalt
a,
literalt
b)
13
{
14
lcnf
(a, !b);
15
lcnf
(!a, b);
16
}
17
20
bvt
propt::new_variables
(std::size_t width)
21
{
22
bvt
result
;
23
result
.resize(width);
24
for
(std::size_t i=0; i<width; i++)
25
result
[i]=
new_variable
();
26
return
result
;
27
}
propt::new_variables
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition:
prop.cpp:20
bvt
std::vector< literalt > bvt
Definition:
literal.h:200
propt::set_equal
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition:
prop.cpp:12
propt::new_variable
virtual literalt new_variable()=0
messaget::result
mstreamt & result() const
Definition:
message.h:396
prop.h
literalt
Definition:
literal.h:24
propt::lcnf
void lcnf(literalt l0, literalt l1)
Definition:
prop.h:55
solvers
prop
prop.cpp
Generated by
1.8.17