1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 dimacs.h 7 8 Abstract: 9 10 Dimacs CNF parser 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2011-07-26. 15 16 Revision History: 17 18 Nikolaj Bjorner (nbjorner) 2020-09-07 19 Add parser to consume extended DRAT format. 20 21 --*/ 22 #pragma once 23 24 #include "sat/sat_types.h" 25 26 bool parse_dimacs(std::istream & s, std::ostream& err, sat::solver & solver); 27 28 namespace dimacs { 29 struct lex_error {}; 30 31 class stream_buffer { 32 std::istream & m_stream; 33 int m_val; 34 unsigned m_line; 35 public: 36 37 stream_buffer(std::istream & s): 38 m_stream(s), 39 m_line(0) { 40 m_val = m_stream.get(); 41 } 42 43 int operator *() const { 44 return m_val; 45 } 46 47 void operator ++() { 48 m_val = m_stream.get(); 49 if (m_val == '\n') ++m_line; 50 } 51 52 unsigned line() const { return m_line; } 53 }; 54 55 struct drat_record { 56 enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def }; 57 tag_t m_tag{ tag_t::is_clause }; 58 // a clause populates m_lits and m_status 59 // a node populates m_node_id, m_name, m_args 60 // a bool def populates m_node_id and one element in m_args 61 sat::literal_vector m_lits; 62 sat::status m_status{ sat::status::redundant() }; 63 unsigned m_node_id{ 0 }; 64 std::string m_name; 65 unsigned_vector m_args; 66 drat_record() {} 67 }; 68 69 struct drat_pp { 70 drat_record const& r; 71 std::function<symbol(int)>& th; 72 drat_pp(drat_record const& r, std::function<symbol(int)>& th) : r(r), th(th) {} 73 }; 74 75 std::ostream& operator<<(std::ostream& out, drat_record const& r); 76 std::ostream& operator<<(std::ostream& out, drat_pp const& r); 77 78 class drat_parser { 79 dimacs::stream_buffer in; 80 std::ostream& err; 81 drat_record m_record; 82 std::function<int(char const*)> m_read_theory_id; 83 svector<char> m_buffer; 84 85 char const* parse_sexpr(); 86 char const* parse_identifier(); 87 int read_theory_id(); 88 bool next(); 89 90 public: 91 drat_parser(std::istream & _in, std::ostream& err): 92 in(_in), err(err) 93 {} 94 95 class iterator { 96 drat_parser& p; 97 bool m_eof; 98 public: 99 iterator(drat_parser& p, bool is_eof):p(p), m_eof(is_eof) { if (!m_eof) m_eof = !p.next(); } 100 drat_record const& operator*() { return p.m_record; } 101 iterator& operator++() { if (!p.next()) m_eof = true; return *this;} 102 bool operator==(iterator const& other) const { return m_eof == other.m_eof; } 103 bool operator!=(iterator const& other) const { return m_eof != other.m_eof; } 104 }; 105 106 iterator begin() { return iterator(*this, false); }; 107 iterator end() { return iterator(*this, true); } 108 109 void set_read_theory(std::function<int(char const*)>& r) { m_read_theory_id = r; } 110 111 }; 112 }; 113 114 115 116