Networks of Automata fixes and visualization, and MCTS search improvements

Dockerfile

@@ -1,4 +1,23 @@
-FROM ubuntu:16.04
+FROM ubuntu
 MAINTAINER Soonho Kong <[email protected]>
-COPY bin/dReal /usr/local/bin/dReal
-#ENTRYPOINT dReal
+COPY bin/dReal /usr/local/bin/
+COPY bin/dReach /usr/local/bin/
+COPY bin/bmc /usr/local/bin/
+RUN apt-get update
+RUN apt-get -y install -qq build-essential
+RUN apt-get -y install -qq autoconf automake bison flex git libtool make pkg-config python-software-properties texinfo
+ADD https://cmake.org/files/v3.7/cmake-3.7.2-Linux-x86_64.sh /cmake-3.7.2-Linux-x86_64.sh
+RUN mkdir /opt/cmake
+RUN sh /cmake-3.7.2-Linux-x86_64.sh --prefix=/opt/cmake --skip-license
+RUN ln -s /opt/cmake/bin/cmake /usr/local/bin/cmake
+RUN apt-get -y install -qq libbz2-dev coinor-libclp-dev clang-format glpk-utils libglpk-dev glpk-doc python-glpk
+RUN apt-get -y install software-properties-common python-software-properties && \
+    add-apt-repository ppa:jonathonf/gcc-7.1 && \
+    apt-get update && \
+    apt-get -y install gcc-7 g++-7
+RUN update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-7 60 && \
+    update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-7 60
+RUN apt-get -y install python-dev   # for python2.x installs && \
+    apt-get -y install python3-dev  # for python3.x installs
+
+ENTRYPOINT dReal

bin/dReach

@@ -247,11 +247,12 @@ do
         #echo SMT: ${SMT}
 
         #Solve
-        echo "${SOLVER} ${MY_SOLVER_OPT} ${SMT} --short_sat --delta_heuristic --delta --sat-prep-bool 2>&1 | tee $OUT"
-        ${SOLVER} ${MY_SOLVER_OPT} ${SMT} --short_sat --delta_heuristic --delta --sat-prep-bool 2>&1 | tee $OUT
+        echo "${SOLVER} ${MY_SOLVER_OPT} ${SMT} --short_sat --delta_heuristic --delta  2>&1 | tee $OUT"
+
+        ${SOLVER} ${MY_SOLVER_OPT} ${SMT} --short_sat --delta_heuristic --delta  2>&1 | tee $OUT
         #        ${SOLVER} ${MY_SOLVER_OPT} ${SMT} --short_sat --delta_heuristic --delta  2>&1 | tee $OUT
         RESULT=`tail -n 1 $OUT`
-        if [[ $RESULT == delta-sat* ]]
+        if [[ $RESULT == delta-sat* || $RESULT == sat* ]]
         then
             echo "For k = $K, $P -- SAT"
             if [ $Z_OPT == TRUE ];      # (edited: FS)
@@ -294,7 +295,7 @@ do
                     ${SOLVER} ${SOLVER_OPT} ${SMT} 2>&1 | tee $OUT
                 fi
                 RESULT=`tail -n 1 $OUT`
-                if [[ $RESULT == delta-sat* ]]
+                if [[ $RESULT == delta-sat* || $RESULT == sat* ]]
                 then
                     echo "For k = $K, $P -- SAT"
                     if [ $Z_OPT == TRUE ];      # (edited: FS)

build-all-docker.sh

@@ -0,0 +1,9 @@
+cd tools
+make dist-clean
+docker build . -t dreal3-tools
+docker run -v `pwd`/../bin:/usr/local/src/dreal/bin -v `pwd`:/usr/local/src/dreal/tools   dreal3-tools 
+cd ../dockerbuild
+docker build . -t dreal3-build
+docker run -v `pwd`/../src:/usr/local/src/dreal/src -v `pwd`/../bin:/usr/local/src/dreal/bin   dreal3-build
+cd ..
+docker build . -t dreal3

dockerbuild/Dockerfile

@@ -5,9 +5,21 @@ VOLUME /usr/local/src/dreal/bin
 RUN apt-get update
 RUN apt-get -y install -qq build-essential
 RUN apt-get -y install -qq autoconf automake bison flex git libtool make pkg-config python-software-properties texinfo
-RUN apt-get -y install -qq cmake
+ADD https://cmake.org/files/v3.7/cmake-3.7.2-Linux-x86_64.sh /cmake-3.7.2-Linux-x86_64.sh
+RUN mkdir /opt/cmake
+RUN sh /cmake-3.7.2-Linux-x86_64.sh --prefix=/opt/cmake --skip-license
+RUN ln -s /opt/cmake/bin/cmake /usr/local/bin/cmake
+RUN apt-get -y install -qq libbz2-dev coinor-libclp-dev clang-format glpk-utils libglpk-dev glpk-doc python-glpk
+RUN apt-get -y install software-properties-common python-software-properties && \
+    add-apt-repository ppa:jonathonf/gcc-7.1 && \
+    apt-get update && \
+    apt-get -y install gcc-7 g++-7
+RUN update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-7 60 && \
+    update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-7 60
+RUN apt-get -y install python-dev   # for python2.x installs && \
+    apt-get -y install python3-dev  # for python3.x installs
+
 RUN mkdir -p /usr/local/src/dreal/build/release
 WORKDIR /usr/local/src/dreal/build/release
 COPY build.sh .
 ENTRYPOINT /bin/bash build.sh
-

dockerbuild/build.sh

@@ -1,3 +1,4 @@
 #!/bin/bash
 cmake -DCMAKE_BUILD_TYPE=RELEASE ../../src
 make
+#cp /usr/local/src/dreal/build/release/dReal /usr/local/src/dreal/bin/dReal-docker

src/contractor/contractor_capd4.cpp

@@ -981,6 +981,9 @@ json generate_trace_core(integral_constraint const & ic, vector<Enode *> const &
     for (auto const & var : pars_0) {
         json entry;
         string const name = var->getCar()->getNameFull();
+
+        if (name.find("gamma_") == 0) continue;
+
         entry["key"] = name;
         entry["mode"] = ic.get_flow_id();
         entry["step"] = extract_step(name);

src/contractor/contractor_fixpoint.cpp

@@ -136,6 +136,13 @@ void contractor_fixpoint::prune(contractor_status & cs) {
         worklist_fixpoint_alg(cs);
         DREAL_LOG_DEBUG << "contractor_fix::prune -- end";
         return;
+    } else if (cs.m_config.nra_gac) {
+        if (m_dep_map.size() == 0) {
+            build_deps_map();
+        }
+        worklist_gac_alg(cs);
+        DREAL_LOG_DEBUG << "contractor_fix::prune -- end";
+        return;
     } else {
         naive_fixpoint_alg(cs);
         DREAL_LOG_DEBUG << "contractor_fix::prune -- end";
@@ -236,4 +243,92 @@ void contractor_fixpoint::worklist_fixpoint_alg(contractor_status & cs) {
              !m_term_cond(m_old_box, cs.m_box));
     return;
 }
+
+void contractor_fixpoint::worklist_gac_alg(contractor_status & cs) {
+    queue<int> q;
+    ibex::BitSet ctc_bitset(m_clist.size());
+    // Add all contractors to the queue.
+    DREAL_LOG_DEBUG << " --- fp first pass --- ";
+
+    for (unsigned i = 0; i < m_clist.size(); ++i) {
+        contractor & c_i = m_clist[i];
+        contractor_status_guard csg(cs);
+        c_i.prune(cs);
+        if (cs.m_box.is_empty()) {
+            return;
+        }
+        // ibex::BitSet const & output_i = cs.m_output;
+        // if (!output_i.empty()) {
+        //     assert(!ctc_bitset.contain(i));
+        //     q.push(i);
+        //     ctc_bitset.add(i);
+        // }
+        auto const & c_output = cs.m_output;
+        if (!c_output.empty()) {
+            // j-th dimension is changed as a result of pruning
+            // need to add a contractor which takes j-th dim as an input
+            int j = c_output.min();
+            do {
+                if (!c_output.contain(j)) {
+                    continue;
+                }
+                for (unsigned int const dependent_ctc_id : m_dep_map[j]) {
+                    if (!ctc_bitset.contain(dependent_ctc_id) && dependent_ctc_id != i) {
+                        q.push(dependent_ctc_id);
+                        ctc_bitset.add(dependent_ctc_id);
+                    }
+                }
+                j = c_output.next(j);
+            } while (j < c_output.max());
+        }
+    }
+
+    if (q.size() == 0) {
+        return;
+    }
+    // Fixed Point Loop
+    do {
+        DREAL_LOG_DEBUG << " --- start fp loop --- |q| = " << q.size();
+        interruption_point();
+        int const idx = q.front();
+        q.pop();
+        ctc_bitset.remove(idx);
+        assert(!ctc_bitset.contain(idx));
+        assert(idx >= 0 && static_cast<size_t>(idx) < m_clist.size());
+        contractor & c = m_clist[idx];
+        m_old_box = cs.m_box;
+        contractor_status_guard csg(cs);
+        c.prune(cs);
+        if (cs.m_box.is_empty()) {
+            return;
+        }
+        auto const & c_output = cs.m_output;
+        if (!c_output.empty()) {
+            // j-th dimension is changed as a result of pruning
+            // need to add a contractor which takes j-th dim as an input
+            int j = c_output.min();
+            do {
+                if (!c_output.contain(j)) {
+                    continue;
+                }
+                //                DREAL_LOG_DEBUG << "adding deps for " << cs.m_box.get_vars()[j];
+                for (int const dependent_ctc_id : m_dep_map[j]) {
+                    if (!ctc_bitset.contain(dependent_ctc_id) && dependent_ctc_id != idx) {
+                        // DREAL_LOG_DEBUG << "adding dep " << m_clist[dependent_ctc_id];
+                        q.push(dependent_ctc_id);
+                        ctc_bitset.add(dependent_ctc_id);
+                    }
+                }
+                j = c_output.next(j);
+            } while (j < c_output.max());
+        }
+
+        DREAL_LOG_DEBUG << (q.size() > 0) << " " << (m_old_box != cs.m_box) << " "
+                        << cs.m_box.is_bisectable(cs.m_config.nra_precision) << " "
+                        << !m_term_cond(m_old_box, cs.m_box);
+    } while (q.size() > 0 && cs.m_box.is_bisectable(cs.m_config.nra_precision));
+    DREAL_LOG_DEBUG << " --- exit fp loop --- ";
+
+    return;
+}
 }  // namespace dreal

src/contractor/contractor_fixpoint.h

@@ -56,6 +56,8 @@ class contractor_fixpoint : public contractor_cell {
     void naive_fixpoint_alg(contractor_status & cs);
     // Worklist fixedpoint algorithm
     void worklist_fixpoint_alg(contractor_status & cs);
+    // Worklist GAC algorithm
+    void worklist_gac_alg(contractor_status & cs);
     void build_deps_map();
 };
 }  // namespace dreal

src/dsolvers/nra_solver.cpp

@@ -54,6 +54,7 @@ along with dReal. If not, see <http://www.gnu.org/licenses/>.
 #include "interval/interval.icc"
 #include "json/json.hpp"
 #include "smtsolvers/SMTConfig.h"
+#include "smtsolvers/SimpSMTSolver.h"
 #include "tsolvers/TSolver.h"
 #include "util/box.h"
 #include "util/logging.h"
@@ -458,6 +459,8 @@ void nra_solver::handle_sat_case(box const & b) const {
     if (config.logic == QF_NRA_ODE && config.nra_json) {
         try {
             json traces = {};
+            json modes = egraph.getSolver()->visualizeModes();
+
             // Need to run ODE pruning operator once again to generate a trace
             for (shared_ptr<constraint> const ctr : m_stack) {
                 if (ctr->get_type() == constraint_type::ODE) {
@@ -469,6 +472,7 @@ void nra_solver::handle_sat_case(box const & b) const {
             }
             json vis_json;
             vis_json["traces"] = traces;
+            vis_json["modes"] = modes;
             config.nra_json_out << vis_json.dump() << endl;
         } catch (contractor_exception const & e) {
             DREAL_LOG_FATAL << "The following exception is generated while computing "

src/icp/icp.cpp

@@ -495,61 +495,98 @@ void mcts_icp::solve(contractor & ctc, contractor_status & cs,
     DREAL_THREAD_LOCAL static vector<box> solns;
     solns.clear();
 
+    ctc.prune(cs);
+    if (cs.m_box.is_empty()) return;
+
     icp_mcts_expander expander(ctc, cs, ctrs, brancher);
-    icp_mcts_node * root = new icp_mcts_node(cs.m_box, &expander);
+    shared_ptr<icp_mcts_node> root(new icp_mcts_node(cs.m_box, &expander));
+    root->set_sp(root);
 
     do {
         DREAL_LOG_INFO << "mcts_icp::solve - loop"
                        << "\t"
                        << "graph Size = " << root->size();
 
-        mcts_node * current = root;
-        mcts_node * last = current;
+        // ofstream mcts_out;
+        // mcts_out.open("mcts.dot");
+        // root->draw_dot(mcts_out);
+        // mcts_out.close();
+        // sleep(1);
 
-        // Get leaf node
-        while (!current->children()->empty()) {  // the node is an interior node
+        shared_ptr<mcts_node> current = root;
+        shared_ptr<mcts_node> last = current;
+
+        // Get expandable node
+        while (!current->has_unexplored_children() && !current->terminal()) {
             last = current;
             current = current->select();
             // DREAL_LOG_INFO << "mcts_icp::solve() selected node " << current->id();
         }
 
-        // DREAL_LOG_INFO << "mcts_icp::solve() expand";
+        DREAL_LOG_INFO << "mcts_icp::solve() expand";
 
         // generate leaf nodes and pick one
         last = current->expand();
 
-        if (last != NULL) {
-            // DREAL_LOG_INFO << "mcts_icp::solve() simulate";
+        if (last) {
+            DREAL_LOG_INFO << "mcts_icp::solve() simulate";
             // simulate to end: sat or unsat
             last->simulate();
 
             if (last->is_solution()) {
                 cs.m_config.nra_found_soln++;
-                DREAL_LOG_INFO << "mcts_icp::solve() found solution";
+                DREAL_LOG_INFO << "mcts_icp::solve() found solution, used #nodes = "
+                               << root->size();
+                icp_mcts_node * inode = NULL;
+                if ((inode = dynamic_cast<icp_mcts_node *>(&*last))) {
+                    cs.m_box = inode->get_sat_simulation_boxes().back();
+                }
                 if (cs.m_config.nra_multiple_soln > 1) {
                     // If --multiple_soln is used
                     output_solution(cs.m_box, cs.m_config, cs.m_config.nra_found_soln);
                 }
                 if (cs.m_config.nra_found_soln >= cs.m_config.nra_multiple_soln) {
                     break;
                 }
-                solns.push_back(cs.m_box);
             }
         } else {
             DREAL_LOG_INFO << "mcts_icp::solve() end state";
+
+            if (current == root) {
+                // root has no children, so unsat
+                return;
+            } else if (current->is_solution()) {
+                current->simulate();
+            } else {
+                // current is an unsat box
+                // delete current;
+                // current.reset();
+                //  current = NULL;
+                DREAL_LOG_DEBUG << "Removing unsat node " << current->id();
+
+                // remove current
+                // remove pointer to it from its parent
+                vector<shared_ptr<mcts_node>> * parent_children =
+                    current->parent().lock()->children();
+                auto it = std::find(parent_children->begin(), parent_children->end(), current);
+                parent_children->erase(it);
+            }
+
             last = current;
         }
 
-        // DREAL_LOG_INFO << "mcts_icp::solve() backpropagate";
+        DREAL_LOG_INFO << "mcts_icp::solve() backpropagate";
 
         // backpropagate value
         current = last;
-        while (current != NULL) {  // the node is in the graph
+        while (current) {  // the node is in the graph
             current->backpropagate();
-            current = current->parent();
+            current = current->parent().lock();
         }
-    } while (true);
+    } while (!root->children()->empty());
+
+    DREAL_LOG_INFO << "mcts_icp::solve() exit";
 
-    delete root;
+    // delete root;
 }
 }  // namespace dreal