cprover
prop.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "prop.h"
10
13{
14 lcnf(a, !b);
15 lcnf(!a, b);
16}
17
20bvt propt::new_variables(std::size_t width)
21{
22 bvt result;
23 result.reserve(width);
24 for(std::size_t i=0; i<width; i++)
25 result.push_back(new_variable());
26 return result;
27}
28
30{
32 return do_prop_solve();
33}
34
36{
38}
std::size_t number_of_solver_calls
Definition: prop.h:129
std::size_t get_number_of_solver_calls() const
Definition: prop.cpp:35
void lcnf(literalt l0, literalt l1)
Definition: prop.h:56
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:12
resultt prop_solve()
Definition: prop.cpp:29
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
resultt
Definition: prop.h:97
virtual resultt do_prop_solve()=0
virtual literalt new_variable()=0
std::vector< literalt > bvt
Definition: literal.h:201