indent

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

scripts/nightly.yaml

@@ -100,7 +100,7 @@ stages:
     displayName: "$(name) build"
     pool:
       vmImage: "Ubuntu-18.04"
-    container: $(image)
+      container: $(image)
     variables:
       python: $(python)
     steps:

src/sat/dimacs.cpp

@@ -113,8 +113,9 @@ static void read_clause(Buffer & in, std::ostream& err, sat::literal_vector & li
 }
 
 template<typename Buffer>
-static void read_pragma(Buffer & in, std::ostream& err, std::string& p) {
+static void read_pragma(Buffer & in, std::ostream& err, std::string& p, sat::proof_hint& h) {
     skip_whitespace(in);
+    h.reset();
     if (*in != 'p')
         return;
     ++in;
@@ -122,14 +123,16 @@ static void read_pragma(Buffer & in, std::ostream& err, std::string& p) {
         ++in;
     while (true) {
         if (*in == EOF)
-            return;
+            break;
         if (*in == '\n') {
             ++in;
-            return;
+            break;
         }
         p.push_back(*in);
         ++in;
     }
+    if (!p.empty()) 
+        h.from_string(p);
 }
 
 
@@ -328,7 +331,7 @@ namespace dimacs {
                 theory_id = read_theory_id();
                 skip_whitespace(in);
                 read_clause(in, err, m_record.m_lits);
-                read_pragma(in, err, m_record.m_pragma);
+                read_pragma(in, err, m_record.m_pragma, m_record.m_hint);
                 m_record.m_tag = drat_record::tag_t::is_clause;
                 m_record.m_status = sat::status::th(false, theory_id);
                 break;

src/sat/dimacs.h

@@ -64,6 +64,7 @@ namespace dimacs {
         std::string     m_name;
         unsigned_vector m_args;
         std::string     m_pragma;
+        sat::proof_hint m_hint;
     };
 
     struct drat_pp {

src/sat/sat_drat.cpp

@@ -932,11 +932,12 @@ namespace sat {
         return ous.str();
     }
 
-    proof_hint proof_hint::from_string(char const* s) {
+    void proof_hint::from_string(char const* s) {
-        proof_hint h;
+        proof_hint& h = *this;
+        h.reset();
         h.m_ty = hint_type::null_h;
         if (!s)
-            return h;
+            return;
         auto ws = [&]() {
             while (*s == ' ' || *s == '\n' || *s == '\t')
                 ++s;
@@ -999,14 +1000,14 @@ namespace sat {
 
         ws();
         if (!parse_type())
-            return h;
+            return;
         ws();
         while (*s) {
             if (!parse_coeff_literal())
-                return h;
+                return;
             ws();            
         }
-        return h;
+        return;
     }
 
 }

src/sat/sat_types.h

@@ -102,11 +102,13 @@ namespace sat {
     };
 
     struct proof_hint {
-        hint_type                                   m_ty;
+        hint_type                                        m_ty = hint_type::null_h;
         vector<std::pair<rational, literal>>             m_literals;
         vector<std::tuple<rational, unsigned, unsigned>> m_eqs;
+        void reset() { m_ty = hint_type::null_h; m_literals.reset(); m_eqs.reset(); }
         std::string to_string() const;
-        static proof_hint from_string(char const* s);
+        void from_string(char const* s);
+        void from_string(std::string const& s) { from_string(s.c_str()); }
     };
 
     class status {