Purge docs references to bmct

peterschrammel · peterschrammel · commit aa3dda90763c · 2019-04-16T18:20:04.000+01:00
diff --git a/src/goto-symex/README.md b/src/goto-symex/README.md
@@ -47,11 +47,11 @@ digraph G {
 
 \subsection symex-overview Overview
 
-The \ref bmct class gets a reference to an \ref symex_target_equationt
+The \ref goto_symext class gets a reference to a \ref symex_target_equationt
 "equation" (initially, an empty list of \ref SSA_stept
 "single-static assignment steps") and a goto-program from the frontend.
-The \ref bmct creates a goto_symext to symbolically execute the
-goto-program, thereby filling the equation, which can then be passed
+\ref multi_path_symex_checkert then calls goto_symext to symbolically execute
+the goto-program, thereby filling the equation, which can then be passed
 along to the SAT solver.
 
 The class \ref goto_symext holds the global state of the symbol executor, while
@@ -131,12 +131,11 @@ representing that path, then continues to execute other paths.
 The 'other paths' that would have been taken when the program branches
 are saved onto a workqueue so that the driver program can continue to execute
 the current path, and then later retrieve saved paths from the workqueue.
-Implementation-wise, \ref bmct passes a worklist to goto_symext in
-\ref bmct::do_language_agnostic_bmc. If path exploration is enabled,
-goto_symext will fill up the worklist whenever it encounters a branch,
-instead of merging the paths on the branch.  After the initial symbolic
-execution (i.e. the first call to \ref bmct::run in
-\ref bmct::do_language_agnostic_bmc), \ref bmct continues popping the
+Implementation-wise, \ref single_path_symex_checkert maintains a worklist
+and passes it to goto_symext. If path exploration is enabled, goto_symext will
+fill up the worklist whenever it encounters a branch, instead of merging the
+paths on the branch. The worklist is initialized with the initial state at the
+entry point. Then \ref single_path_symex_checkert continues popping the
 worklist and executing untaken paths until the worklist empties. Note
 that this means that the default model-checking behaviour is a special
 case of path exploration: when model-checking, the initial symbolic
@@ -261,7 +260,6 @@ In the \ref goto-symex directory.
 **Key classes:**
 * \ref symex_target_equationt
 * \ref prop_convt
-* \ref bmct
 * \ref counterexample_beautificationt
 
 \dot
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
@@ -631,8 +631,8 @@ class goto_symext
   /// The actual number of total and remaining VCCs should be assigned to
   /// the relevant members of goto_symex_statet. The members below are used to
   /// cache the values from goto_symex_statet after symbolic execution has
-  /// ended, so that \ref bmct can read those values even after the state has
-  /// been deallocated.
+  /// ended, so that the user of \ref goto_symext can read those values even
+  /// after the state has been deallocated.
 
   unsigned _total_vccs, _remaining_vccs;
   ///@}
diff --git a/src/solvers/README.md b/src/solvers/README.md
@@ -297,7 +297,6 @@ In the \ref solvers directory.
 **Key classes:**
 * symex_target_equationt
 * \ref propt
-* \ref bmct
 
 \dot
 digraph G {
