37 dynamic_cast<dimacs_cnft &>(
prop).write_dimacs_cnf(out);
42 if(s.second.is_constant())
43 out <<
"c " << s.first <<
" " << (s.second.is_true() ?
"TRUE" :
"FALSE")
46 out <<
"c " << s.first <<
" " << s.second.dimacs() <<
"\n";
50 for(
const auto &m :
get_map().mapping)
54 if(literal_map.empty())
57 out <<
"c " << m.first;
59 for(
const auto &lit : literal_map)
63 else if(lit.l.is_constant())
64 out <<
" " << (lit.l.is_true() ?
"TRUE" :
"FALSE");
66 out <<
" " << lit.l.dimacs();
const symbolst & get_symbols() const
bool write_dimacs(const std::string &filename)
std::vector< map_bitt > literal_mapt
const boolbv_mapt & get_map() const