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