cprover
prop_conv_store.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_conv_store.h"
10 
11 #include <cassert>
12 
13 void prop_conv_storet::set_to(const exprt &expr, bool value)
14 {
17  constraint.expr=expr;
18  constraint.value=value;
19 }
20 
22 {
25  constraint.expr=expr;
26  #if 0
27  constraint.literal=prop.new_variable();
28  #endif
29  return constraint.literal;
30 }
31 
33 {
34  for(constraint_listt::const_iterator
35  it=constraint_list.begin();
36  it!=constraint_list.end();
37  it++)
38  it->replay(dest);
39 }
40 
41 void prop_conv_storet::constraintst::print(std::ostream &out) const
42 {
43  for(constraint_listt::const_iterator
44  it=constraint_list.begin();
45  it!=constraint_list.end();
46  it++)
47  it->print(out);
48 }
49 
51 {
52  switch(type)
53  {
54  case typet::SET_TO:
55  dest.set_to(expr, value);
56  break;
57 
58  case typet::CONVERT:
59  // dest.prop.set_equal(dest.convert_rest(expr), literal);
60  break;
61 
62  default:
63  assert(false);
64  }
65 }
66 
67 void prop_conv_storet::constraintt::print(std::ostream &out) const
68 {
69  switch(type)
70  {
71  case typet::SET_TO:
72  out << "SET_TO " << (value?"TRUE":"FALSE") << ": ";
73  out << expr.pretty() << "\n";
74  break;
75 
76  case typet::CONVERT:
77  out << "CONVERT(" << literal.dimacs() << "): ";
78  out << expr.pretty() << "\n";
79  break;
80 
81  default:
82  assert(false);
83  }
84 }
void print(std::ostream &out) const
constraintst constraints
virtual void set_to(const exprt &expr, bool value)
void print(std::ostream &out) const
void replay(prop_convt &dest) const
virtual void set_to(const exprt &expr, bool value)=0
void replay(prop_convt &dest) const
Base class for all expressions.
Definition: expr.h:46
virtual literalt convert(const exprt &expr)