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 
11 #include <cassert>
12 
15 {
16  lcnf(a, !b);
17  lcnf(!a, b);
18 }
19 
20 void propt::set_assignment(literalt a, bool value)
21 {
22  assert(false);
23 }
24 
26 {
27  assert(false);
28 }
29 
32 {
33  assert(false);
34  return false;
35 }
36 
39 bvt propt::new_variables(std::size_t width)
40 {
41  bvt result;
42  result.resize(width);
43  for(std::size_t i=0; i<width; i++)
44  result[i]=new_variable();
45  return result;
46 }
mstreamt & result()
Definition: message.h:233
void lcnf(literalt l0, literalt l1)
Definition: prop.h:53
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:39
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:14
virtual literalt new_variable()=0
virtual void set_assignment(literalt a, bool value)
Definition: prop.cpp:20
TO_BE_DOCUMENTED.
Definition: prop.h:22
virtual bool is_in_conflict(literalt l) const
Definition: prop.cpp:31
virtual void copy_assignment_from(const propt &prop)
Definition: prop.cpp:25
std::vector< literalt > bvt
Definition: literal.h:197