feat(verifier): unknot some deps and call into the fast solver (#5662)

kythe/cxx/verifier/BUILD

@@ -61,7 +61,6 @@ cc_library(
     deps = [
         ":assertions_to_souffle",
         ":lexparse",
-        ":lib",
         "//third_party/souffle:parse_transform",
         "@com_github_google_glog//:glog",
         "@com_google_absl//absl/strings",
@@ -93,7 +92,6 @@ cc_library(
     ],
     deps = [
         ":lexparse",
-        ":lib",
         "@com_google_absl//absl/strings",
     ],
 )
@@ -106,6 +104,7 @@ cc_test(
     deps = [
         ":assertions_to_souffle",
         ":lexparse",
+        ":lib",
         ":pretty_printer",
         "//third_party:gtest",
         "//third_party:gtest_main",
@@ -164,6 +163,7 @@ cc_library(
     deps = [
         ":lexparse",
         ":pretty_printer",
+        ":souffle_interpreter",
         "//kythe/cxx/common:file_utils",
         "//kythe/cxx/common:kythe_uri",
         "//kythe/cxx/common:scope_guard",

kythe/cxx/verifier/assertion_ast.h

@@ -352,6 +352,25 @@ struct GoalGroup {
   std::vector<AstNode*> goals;    ///< Grouped goals, implicitly conjoined.
 };
 
+/// \brief A database of fact-shaped AstNodes.
+using Database = std::vector<AstNode*>;
+
+/// \brief Multimap from anchor offsets to anchor VName tuples.
+using AnchorMap = std::multimap<std::pair<size_t, size_t>, AstNode*>;
+
+/// An EVar whose assignment is interesting to display.
+struct Inspection {
+  enum class Kind {
+    EXPLICIT,  ///< The user requested this inspection (with "?").
+    IMPLICIT   ///< This inspection was added by default.
+  };
+  std::string label;  ///< A label for user reference.
+  EVar* evar;         ///< The EVar to inspect.
+  Kind kind;          ///< Whether this inspection was added by default.
+  Inspection(const std::string& label, EVar* evar, Kind kind)
+      : label(label), evar(evar), kind(kind) {}
+};
+
 }  // namespace verifier
 }  // namespace kythe
 

kythe/cxx/verifier/assertions.h

@@ -32,9 +32,6 @@ class AssertionParserImpl;
 namespace kythe {
 namespace verifier {
 
-/// \brief A database of fact-shaped AstNodes.
-using Database = std::vector<AstNode*>;
-
 class Verifier;
 
 /// \brief Parses logic programs.
@@ -80,19 +77,6 @@ class AssertionParser {
   /// \brief All of the goal groups in this `AssertionParser`.
   std::vector<GoalGroup>& groups() { return groups_; }
 
-  /// An EVar whose assignment is interesting to display.
-  struct Inspection {
-    enum class Kind {
-      EXPLICIT,  ///< The user requested this inspection (with "?").
-      IMPLICIT   ///< This inspection was added by default.
-    };
-    std::string label;  ///< A label for user reference.
-    EVar* evar;         ///< The EVar to inspect.
-    Kind kind;          ///< Whether this inspection was added by default.
-    Inspection(const std::string& label, EVar* evar, Kind kind)
-        : label(label), evar(evar), kind(kind) {}
-  };
-
   /// \brief All of the inspections in this `AssertionParser`.
   std::vector<Inspection>& inspections() { return inspections_; }
 
@@ -333,9 +317,6 @@ class AssertionParser {
   /// The current file's corpus.
   Symbol corpus_;
 };
-
-/// Multimap from anchor offsets to anchor VName tuples.
-using AnchorMap = std::multimap<std::pair<size_t, size_t>, AstNode*>;
 }  // namespace verifier
 }  // namespace kythe
 

kythe/cxx/verifier/assertions_to_souffle.cc

@@ -37,7 +37,7 @@ result() :- true
 bool SouffleProgram::Lower(const SymbolTable& symbol_table,
                            const std::vector<GoalGroup>& goal_groups) {
   code_ = emit_prelude_ ? std::string(kGlobalDecls) : "";
-  CHECK_EQ(0, goal_groups.size()) << "(unimplemented)";
+  CHECK_LE(goal_groups.size(), 1) << "(unimplemented)";
   absl::StrAppend(&code_, ".\n");
   return true;
 }

kythe/cxx/verifier/souffle_interpreter.cc

@@ -24,7 +24,6 @@
 #include "glog/logging.h"
 #include "interpreter/Engine.h"
 #include "kythe/cxx/verifier/assertions_to_souffle.h"
-#include "kythe/cxx/verifier/verifier.h"
 #include "souffle/RamTypes.h"
 #include "souffle/io/IOSystem.h"
 #include "third_party/souffle/parse_transform.h"
@@ -176,11 +175,11 @@ class KytheWriteStreamFactory : public souffle::WriteStreamFactory {
 };
 }  // anonymous namespace
 
-SouffleResult RunSouffle(
-    const SymbolTable& symbol_table, const std::vector<GoalGroup>& goal_groups,
-    const Database& database, const AnchorMap& anchors,
-    const std::vector<AssertionParser::Inspection>& inspections,
-    std::function<bool(const AssertionParser::Inspection&)> inspect) {
+SouffleResult RunSouffle(const SymbolTable& symbol_table,
+                         const std::vector<GoalGroup>& goal_groups,
+                         const Database& database, const AnchorMap& anchors,
+                         const std::vector<Inspection>& inspections,
+                         std::function<bool(const Inspection&)> inspect) {
   SouffleResult result{};
   SouffleProgram program;
   if (!program.Lower(symbol_table, goal_groups)) {

kythe/cxx/verifier/souffle_interpreter.h

@@ -17,7 +17,7 @@
 #ifndef KYTHE_CXX_VERIFIER_SOUFFLE_INTERPRETER_H_
 #define KYTHE_CXX_VERIFIER_SOUFFLE_INTERPRETER_H_
 
-#include "kythe/cxx/verifier/assertions.h"
+#include "kythe/cxx/verifier/assertion_ast.h"
 
 namespace kythe::verifier {
 struct SouffleResult {
@@ -37,11 +37,11 @@ struct SouffleResult {
 /// provided list of inspections; a false return value stops iterating through
 /// inspection results and fails the solution, while a true result continues.
 /// \return a `SouffleResult` describing how the run went.
-SouffleResult RunSouffle(
-    const SymbolTable& symbol_table, const std::vector<GoalGroup>& goal_groups,
-    const Database& database, const AnchorMap& anchors,
-    const std::vector<AssertionParser::Inspection>& inspections,
-    std::function<bool(const AssertionParser::Inspection&)> inspect);
+SouffleResult RunSouffle(const SymbolTable& symbol_table,
+                         const std::vector<GoalGroup>& goal_groups,
+                         const Database& database, const AnchorMap& anchors,
+                         const std::vector<Inspection>& inspections,
+                         std::function<bool(const Inspection&)> inspect);
 }  // namespace kythe::verifier
 
 #endif  // defined(KYTHE_CXX_VERIFIER_SOUFFLE_INTERPRETER_H_)

kythe/cxx/verifier/souffle_interpreter_test.cc

@@ -25,10 +25,9 @@ TEST(SouffleInterpreterTest, SmokeTest) {
   Database db;
   AnchorMap anchors;
   std::vector<GoalGroup> groups;
-  std::vector<AssertionParser::Inspection> inspections;
-  auto result =
-      RunSouffle(symbols, groups, db, anchors, inspections,
-                 [](const AssertionParser::Inspection&) { return true; });
+  std::vector<Inspection> inspections;
+  auto result = RunSouffle(symbols, groups, db, anchors, inspections,
+                           [](const Inspection&) { return true; });
   ASSERT_TRUE(result.success);
 }
 }  // namespace kythe::verifier

kythe/cxx/verifier/verifier.cc

@@ -30,6 +30,7 @@
 #include "google/protobuf/util/json_util.h"
 #include "kythe/cxx/common/kythe_uri.h"
 #include "kythe/cxx/common/scope_guard.h"
+#include "kythe/cxx/verifier/souffle_interpreter.h"
 #include "kythe/proto/common.pb.h"
 #include "kythe/proto/storage.pb.h"
 
@@ -336,8 +337,6 @@ static bool FastLookupFactLessThan(AstNode* a, AstNode* b) {
 // look at deferring to a pre-existing system.
 class Solver {
  public:
-  using Inspection = AssertionParser::Inspection;
-
   Solver(Verifier* context, Database& database, AnchorMap& anchors,
          std::function<bool(Verifier*, const Inspection&)>& inspect)
       : context_(*context),
@@ -960,24 +959,31 @@ void Verifier::DumpErrorGoal(size_t group, size_t index) {
 }
 
 bool Verifier::VerifyAllGoals(
-    std::function<bool(Verifier*, const Solver::Inspection&)> inspect) {
+    std::function<bool(Verifier*, const Inspection&)> inspect) {
   if (use_fast_solver_) {
-    return true;
-  }
-  if (!PrepareDatabase()) {
-    return false;
+    auto result = RunSouffle(symbol_table_, parser_.groups(), facts_, anchors_,
+                             parser_.inspections(), [&](const Inspection& i) {
+                               return inspect(this, i);
+                             });
+    highest_goal_reached_ = result.highest_goal_reached;
+    highest_group_reached_ = result.highest_group_reached;
+    return result.success;
+  } else {
+    if (!PrepareDatabase()) {
+      return false;
+    }
+    Solver solver(this, facts_, anchors_, inspect);
+    bool result = solver.Solve();
+    highest_goal_reached_ = solver.highest_goal_reached();
+    highest_group_reached_ = solver.highest_group_reached();
+    return result;
   }
-  Solver solver(this, facts_, anchors_, inspect);
-  bool result = solver.Solve();
-  highest_goal_reached_ = solver.highest_goal_reached();
-  highest_group_reached_ = solver.highest_group_reached();
-  return result;
 }
 
 bool Verifier::VerifyAllGoals() {
   return VerifyAllGoals([this](Verifier* context,
-                               const Solver::Inspection& inspection) {
-    if (inspection.kind == Solver::Inspection::Kind::EXPLICIT) {
+                               const Inspection& inspection) {
+    if (inspection.kind == Inspection::Kind::EXPLICIT) {
       FileHandlePrettyPrinter printer(saving_assignments_ ? stderr : stdout);
       printer.Print(inspection.label);
       printer.Print(": ");

kythe/cxx/verifier/verifier.h

@@ -89,8 +89,7 @@ class Verifier {
   /// \param inspect function to call on any inspection request
   /// \return true if all goals could be satisfied.
   bool VerifyAllGoals(
-      std::function<bool(Verifier* context, const AssertionParser::Inspection&)>
-          inspect);
+      std::function<bool(Verifier* context, const Inspection&)> inspect);
 
   /// \brief Attempts to satisfy all goals from all loaded rule files and facts.
   /// \return true if all goals could be satisfied.