Trail Access

.travis.yml

@@ -1,26 +1,18 @@
-# Use container-based distribution
 sudo: false
 language: c++
 matrix:
   include:
     - os: linux
+      dist: bionic
       compiler: gcc
       addons:
         apt:
-          sources:
-            - ubuntu-toolchain-r-test
           packages:
-            - g++-5
             - re2c
-            - liblua5.1-0-dev
+            - bison
+            - liblua5.3-dev
             - zsh
-      env:
-        - MY_CC=gcc-5
-        - MY_CXX=g++-5
     - os: osx
-      env:
-        - MY_CC=clang
-        - MY_CXX=clang++
 
 script:
   - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then
@@ -29,11 +21,6 @@ script:
       brew install lua bison re2c;
       export PATH="/usr/local/opt/bison/bin:$PATH";
     fi
-  - if [[ "${TRAVIS_OS_NAME}" == "linux" ]]; then
-      CMAKE_URL="http://www.cmake.org/files/v3.3/cmake-3.3.2-Linux-x86_64.tar.gz";
-      mkdir cmake-bin && wget --quiet --no-check-certificate -O - ${CMAKE_URL} | tar --strip-components=1 -xz -C cmake-bin;
-      export PATH=${PWD}/cmake-bin/bin:${PATH};
-    fi
   - mkdir build &&
     cd build &&
     cmake
@@ -42,8 +29,6 @@ script:
       -DCLASP_BUILD_TESTS=True
       -DLIB_POTASSCO_BUILD_TESTS=True
       -DCLINGO_BUILD_EXAMPLES=True
-      -DCMAKE_C_COMPILER=${MY_CC}
-      -DCMAKE_CXX_COMPILER=${MY_CXX}
       .. &&
     make -j3 &&
     make test CTEST_OUTPUT_ON_FAILURE=True

app/clingo/tests/lua/assignment.lp

@@ -0,0 +1,96 @@
+#script (lua)
+
+require("clingo")
+
+Propagator = { }
+Propagator.__index = Propagator
+
+function Propagator.new()
+    local self = setmetatable({}, Propagator)
+    return self
+end
+
+function check_lit(assignment, l)
+    local trail = assignment.trail
+    local t = assignment:value(l)
+    if t ~= nil then
+        local s = 1
+        if not t then
+            s = -1
+        end
+        local n = 0
+        for k in trail:iter() do
+            if k == s * l then
+                n = n + 1
+            end
+        end
+        assert(n == 1)
+    end
+end
+
+function check_trail(assignment)
+    local trail = assignment.trail
+    local n = 0
+    for i = 0, assignment.decision_level do
+        check = false
+        for j = trail:first(i), trail:last(i) do
+            check = true
+            assert(assignment:is_true(trail[j]))
+            n = n + 1
+        end
+        assert(check)
+    end
+    assert(n == #trail)
+    n = 0
+    for l in assignment:iter() do
+        n = n + 1
+        check_lit(assignment, l)
+    end
+    assert(n == #assignment)
+    n = 0
+    for i, l in assignment:__pairs() do
+        n = n + 1
+        assert(assignment[i] == l)
+    end
+    assert(n == #assignment)
+    n = 0
+    for i, l in assignment:__ipairs() do
+        n = n + 1
+        assert(assignment[i] == l)
+    end
+    assert(n == #assignment)
+    n = 0
+    for i, k in trail:__pairs() do
+        assert(trail[i] == k)
+        n = n + 1
+    end
+    assert(n == #trail)
+    n = 0
+    for i, k in trail:__ipairs() do
+        assert(trail[i] == k)
+        n = n + 1
+    end
+    assert(n == #trail)
+end
+
+
+function Propagator:init(init)
+    check_trail(init.assignment)
+
+    init.check_mode = clingo.PropagatorCheckMode.Fixpoint
+end
+
+function Propagator:check(control)
+    check_trail(control.assignment)
+end
+
+function main(prg)
+    local p = Propagator.new()
+    prg:register_propagator(p)
+    prg:ground({{"base", {}}})
+    prg:solve()
+end
+
+#end.
+
+{ a; b; c }.

app/clingo/tests/lua/assignment.sol

@@ -0,0 +1,10 @@
+Step: 1
+
+a
+a b
+a b c
+a c
+b
+b c
+c
+SAT

app/clingo/tests/python/assignment.lp

@@ -0,0 +1,79 @@
+#script (python)
+
+import clingo
+from itertools import chain
+
+def check_lit(assignment, l):
+    trail = assignment.trail
+    t = assignment.value(l)
+    if t is not None:
+        s = 1
+        if not t:
+            s = -1
+        n = 0
+        for k in trail:
+            if k == s * l:
+                n = n + 1
+        assert n == 1
+
+def check_trail(assignment):
+    trail = assignment.trail
+
+    n = 0
+    for i in range(0, assignment.decision_level + 1):
+        check = False
+        for j in range(trail.begin(i), trail.end(i)):
+            check = True
+            assert assignment.is_true(trail[j])
+            n = n + 1
+        assert check
+    assert n == len(trail)
+
+    n = 0
+    for l in assignment:
+        n = n + 1
+        check_lit(assignment, l)
+    assert n == len(assignment)
+
+    n = 0
+    for l in chain(assignment[0::2], assignment[1::2]):
+        n = n + 1
+    assert n == len(assignment)
+
+    n = 0
+    for l in chain(trail[0::2], trail[1::2]):
+        n = n + 1
+    assert n == len(trail)
+
+    n = 1
+    for l in trail[0:-1]:
+        n = n + 1
+    assert n == len(trail)
+
+    n = 0
+    for l in trail[-1:-1-len(trail):-1]:
+        n = n + 1
+    assert n == len(trail)
+
+    n = 0
+    for l in chain(trail[-1:-1-len(trail):-2], trail[-2:-1-len(trail):-2]):
+        n = n + 1
+    assert n == len(trail)
+
+class Propagator:
+    def init(self, init):
+        check_trail(init.assignment)
+
+        init.check_mode = clingo.PropagatorCheckMode.Fixpoint
+
+    def check(self, control):
+        check_trail(control.assignment)
+
+def main(prg):
+    prg.register_propagator(Propagator())
+    prg.ground([("base", [])])
+    prg.solve()
+
+#end.
+
+{ a; b; c }.

app/clingo/tests/python/assignment.sol

@@ -0,0 +1,10 @@
+Step: 1
+
+a
+a b
+a b c
+a c
+b
+b c
+c
+SAT

libclingo/clingo.h

@@ -996,21 +996,59 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_false(clingo_assignment_t co
 //! @param[out] value the resulting truth value
 //! @return whether the call was successful
 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_truth_value(clingo_assignment_t const *assignment, clingo_literal_t literal, clingo_truth_value_t *value);
-//! The number of assigned literals in the assignment.
+//! The number of (positive) literals in the assignment.
 //!
 //! @param[in] assignment the target
 //! @return the number of literals
 CLINGO_VISIBILITY_DEFAULT size_t clingo_assignment_size(clingo_assignment_t const *assignment);
-//! The maximum size of the assignment (if all literals are assigned).
+//! The (positive) literal at the given offset in the assignment.
 //!
 //! @param[in] assignment the target
+//! @param[in] offset the offset of the literal
+//! @param[out] literal the literal
 //! @return the maximum size
-CLINGO_VISIBILITY_DEFAULT size_t clingo_assignment_max_size(clingo_assignment_t const *assignment);
-//! Check if the assignmen is total, i.e. - size == max_size.
+CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_at(clingo_assignment_t const *assignment, size_t offset, clingo_literal_t *literal);
+//! Check if the assignment is total, i.e. there are no free literal.
 //!
 //! @param[in] assignment the target
 //! @return wheather the assignment is total
 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_total(clingo_assignment_t const *assignment);
+//! Returns the number of literals in the trail, i.e., the number of assigned literals.
+//!
+//! @param[in] assignment the target
+//! @param[out] size the number of literals in the trail
+//! @return whether the call was successful
+CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_size(clingo_assignment_t const *assignment, uint32_t *size);
+//! Returns the offset of the decision literal with the given decision level in
+//! the trail.
+//!
+//! @note Literals in the trail are ordered by decision levels, where the first
+//! literal with a larger level than the previous literals is a decision; the
+//! following literals with same level are implied by this decision literal.
+//! Each decision level up to and including the current decision level has a
+//! valid offset in the trail.
+//!
+//! @param[in] assignment the target
+//! @param[in] level the decision level
+//! @param[out] offset the offset of the decision literal
+//! @return whether the call was successful
+CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_begin(clingo_assignment_t const *assignment, uint32_t level, uint32_t *offset);
+//! Returns the offset following the last literal with the given decision level.
+//!
+//! @note This function is the counter part to clingo_assignment_trail_begin().
+//!
+//! @param[in] assignment the target
+//! @param[in] level the decision level
+//! @param[out] offset the offset
+//! @return whether the call was successful
+CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_end(clingo_assignment_t const *assignment, uint32_t level, uint32_t *offset);
+//! Returns the literal at the given position in the trail.
+//!
+//! @param[in] assignment the target
+//! @param[in] offset the offset of the literal
+//! @param[out] literal the literal
+//! @return whether the call was successful
+CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_at(clingo_assignment_t const *assignment, uint32_t offset, clingo_literal_t *literal);
 
 //! @}