From 705b1078461b4d4680ab4080fda9221a92b4846a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 28 Sep 2017 20:05:46 -0700
Subject: [PATCH] fixed encoding for order constraints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/dimacs.cpp         |  9 +++++++--
 src/util/sorting_network.h | 15 ++++++++-------
 2 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/sat/dimacs.cpp b/src/sat/dimacs.cpp
index 512be5f4b..463418b23 100644
--- a/src/sat/dimacs.cpp
+++ b/src/sat/dimacs.cpp
@@ -24,10 +24,12 @@ Revision History:
 class stream_buffer {
     std::istream & m_stream;
     int            m_val;
+    unsigned       m_line;
 public:
     
     stream_buffer(std::istream & s):
-        m_stream(s) {
+        m_stream(s),
+        m_line(0) {
         m_val = m_stream.get();
     }
 
@@ -37,7 +39,10 @@ public:
 
     void operator ++() { 
         m_val = m_stream.get();
+        if (m_val == '\n') ++m_line;
     }
+
+    unsigned line() const { return m_line; }
 };
 
 template<typename Buffer>
@@ -76,7 +81,7 @@ int parse_int(Buffer & in) {
     }
 
     if (*in < '0' || *in > '9') {
-        std::cerr << "(error, \"unexpected char: " << *in << "\")\n";
+        std::cerr << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n";
         exit(3);
         exit(ERR_PARSER);
     }
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index 9a1d064d4..ade66403d 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -328,15 +328,15 @@ Notes:
         }
 
         void add_implies_and(literal l, literal_vector const& xs) {
-            for (unsigned j = 0; j < xs.size(); ++j) {
-                add_clause(ctx.mk_not(l), xs[j]);
+            for (literal const& x : xs) {
+                add_clause(ctx.mk_not(l), x);
             }
         }
 
         void add_and_implies(literal l, literal_vector const& xs) {
             literal_vector lits;
-            for (unsigned j = 0; j < xs.size(); ++j) {
-                lits.push_back(ctx.mk_not(xs[j]));
+            for (literal const& x : xs) {
+                lits.push_back(ctx.mk_not(x));
             }
             lits.push_back(l);
             add_clause(lits);
@@ -513,8 +513,9 @@ Notes:
                 add_clause(ctx.mk_not(r), ctx.mk_not(ys[i]), ctx.mk_not(xs[i + 1]));
             }
 
-            add_clause(ctx.mk_not(r), ys[n-2], xs[n-1]);
-            add_clause(ctx.mk_not(r), ctx.mk_not(ys[n-2]), ctx.mk_not(xs[n-1]));
+            if (is_eq) {
+                add_clause(ctx.mk_not(r), ys[n-2], xs[n-1]);
+            }
             for (unsigned i = 1; i < n - 1; ++i) {
                 add_clause(ctx.mk_not(ys[i]), xs[i], ys[i-1]);
             }
@@ -583,7 +584,7 @@ Notes:
         }
 
         std::ostream& pp(std::ostream& out, literal_vector const& lits) {
-            for (unsigned i = 0; i < lits.size(); ++i) ctx.pp(out, lits[i]) << " ";
+            for (literal const& l : lits) ctx.pp(out, l) << " ";
             return out;
         }