fixed trail class

Author: Udopia

code/src/trail.h

@@ -110,11 +110,14 @@ class Trail {
 
     bool backtrack() {
         if (!trail_lim.empty()) {
-            for (int i = trail.size()-1; i > trail_lim.back(); i--) {
+            if (verb) std::cout << "Backtracking to position " << trail_lim.back() << std::endl;
+            for (int i = trail.size()-1; i >= (int)trail_lim.back(); i--) {
+                if (verb) std::cout << "Unassigning " << trail[i] << " at position " << i << std::endl;
                 val[trail[i].var()] = UNASSIGNED;
             }
             trail.resize(trail_lim.back());
             trail_lim.pop_back();
+            head = trail.size();
             return true;
         }
         return false;

code/tests/trailtest.cc

@@ -26,4 +26,22 @@ TEST_CASE("Trail") {
         CHECK(trail.init(f));
         CHECK(trail.propagate());
     }
+
+    SUBCASE("backtrack") {
+        CNFFormula f;
+        f.readClause({ Lit(1, true), Lit(2) });
+        f.readClause({ Lit(2, true), Lit(3) });
+        Trail trail {};
+        CHECK(trail.init(f));
+        CHECK(trail.push(Lit(1, false)));
+        CHECK(trail.propagate());
+        CHECK(trail[0] == Lit(1, false));
+        CHECK(trail[1] == Lit(2, false));
+        CHECK(trail[2] == Lit(3, false));
+        CHECK(trail.backtrack());
+        CHECK(trail.push(Lit(2, true)));
+        CHECK(trail.propagate());
+        CHECK(trail[0] == Lit(2, true));
+        CHECK(trail[1] == Lit(1, true));
+    }
 }