User implemented features

DEVELOPING.md

@@ -73,6 +73,12 @@
     source ~/.bashrc
     ```
 
+1. (Optional) Set path to custom files (see `SMTD_CUSTOM.md` for more information)
+    ```bash
+    echo 'export SMTD_CUSTOM_PATH=<PATH_TO_SMTD_CUSTOM>' >> ~/.bashrc
+    source ~/.bashrc
+    ```
+
 1. Run build script
 
     Begin in project root:
@@ -162,6 +168,12 @@
     source ~/.bashrc
     ```
 
+1. (Optional) Set path to custom files (see `SMTD_CUSTOM.md` for more information)
+    ```bash
+    echo 'export SMTD_CUSTOM_PATH=<PATH_TO_SMTD_CUSTOM>' >> ~/.bashrc
+    source ~/.bashrc
+    ```
+
 1. Run build script
     Begin in project root:
     ```bash
@@ -179,10 +191,10 @@
     pip install hatch
     ```
 
-1. Update `.zshrc` (or `.bashrc`)
+1. Update `.bashrc` (or `.zshrc`)
 
     ```bash
-    echo 'export PATH="/opt/homebrew/opt/bison/bin:$PATH"' >> ~/.zshrc
+    echo 'export PATH="/opt/homebrew/opt/bison/bin:$PATH"' >> ~/.bashrc
     ```
 
 3. Use ***Python 3.11*** -- here's one way (other versions of Python may not work)
@@ -238,6 +250,12 @@
     source ~/.bashrc
     ```
 
+1. (Optional) Set path to custom files (see `SMTD_CUSTOM.md` for more information)
+    ```bash
+    echo 'export SMTD_CUSTOM_PATH=<PATH_TO_SMTD_CUSTOM>' >> ~/.bashrc
+    source ~/.bashrc
+    ```
+
 1. Run the build script
 
     Begin in project root:

SMTD_CUSTOM.md

@@ -0,0 +1,41 @@
+This file describes how to implement features that are factored out of the main SMT-D repo. 
+
+#### Prerequistes 
+* Everything from `DEVELOPING.md` 
+* Set `$SMTD_CUSTOM_PATH` to the absolute path to the folder hosting the custom features, called `smtd_custom`. For example, `/home/<username>/smtd_custom`
+#### Custom worker heuristics
+* In the `smtd_custom/custom_worker_heuristics` folder, implement `CustomHeuristics.cpp` and `CustomHeuristics.h`, 
+  which implement the `UserHeuristics.h` interface 
+* Pass argument `--custom_worker` when running `./run_build.sh` (building SMT-D)
+#### Custom proto fields
+* In the `smtd_custom/custom_proto` folder, implement `custom_proto.proto`. A minimal example of `custom_proto.proto` 
+  is as follows (you must use the `SmtD` package and use, at least, the `SmtDWrapperCustomOptions` struct): 
+    ```
+    syntax = "proto3";
+    package SmtD;
+
+    message SmtDWrapperCustomOptions {
+        uint32 custom = 1;
+    }
+    ```
+* Pass argument `--custom_proto` when running `./run_build.sh` (building SMT-D)
+#### Custom stats reporting
+* In the `smtd_custom/custom_stats` folder, implement `custom_stats_handler.py`, which implements the 
+  interface defined in `UserStatsHandler.py` in SMT-D
+* Pass argument `--user_stats` when running SMT-D (e.g., `./smtd -f <file> --user_stats`)
+* Also pass argument `--broker user` when calling SMT-D. (In the future, the user broker will 
+  become the only broker, and all the clause sharing heuristics will be modularly defined, 
+  rather than having a separate parse broker, rate broker, and so on. When this time comes, 
+  it will be possible to, for example, mix the parse time heuristic with user stats handling. 
+  But for now, it is unsupported.)
+#### Custom control loops (clause sharing heuristics)
+* In the `smtd_custom/custom_control_loops` folder, implement `custom_control_loop.py`, which implements 
+  the interface defined in `UserControlLoop.py`
+* Pass argument `--user_control_loop` when running SMT-D
+* Also pass argument `--broker user` when calling SMT-D
+#### Miscellaneous
+* In the build script, when `--custom_worker` or `--custom_proto` is not passed, 
+  a default, dummy value for `custom_proto.proto` and `CustomHeuristics.cpp/h` is 
+  generated by the build script (`./run_build.sh`). Hence, if you ever update the interface for 
+  custom workers or proto files, you will also need to update the build script accordingly. 
+  There is probably a better way of doing this.

run_build.sh

@@ -1,11 +1,15 @@
 #!/usr/bin/env bash
 # Args
-#   --only_broker -> only run broker portions of build script
-#   --only_worker -> only run worker portions of build script
-#   --debug       -> build worker executable in debug mode
+#   --only_broker  -> only run broker portions of build script
+#   --only_worker  -> only run worker portions of build script
+#   --debug        -> build worker executable in debug mode
+#   --custom_proto -> include user-defined .proto file from ${SMTD_CUSTOM_PATH}/custom_proto/custom_proto.proto
+#   --custom_worker -> include user-defined .cpp/.h files from ${SMTD_CUSTOM_PATH}/custom_worker_heuristics/CustomHeuristics.cpp/.h
 #   You can use any combination of the above args, but combining --only_broker with --only_worker
 #   will perform no action.
 
+# TODO: Allow passing filename of custom proto and custom worker files
+
 cd "$(dirname "$0")" || exit 1
 
 if [ -z "${SMTD_CVC5_REPO_PATH}" ]; then
@@ -24,6 +28,49 @@ if ! [[ " $@ " == *" --only_worker "* ]]; then
   find ./src/smtd/proto -maxdepth 1 -type f \( -name "*.py" -o -name "*.pyi" \) -exec rm -f {} +
   touch ./src/smtd/proto/__init__.py
 
+  # Copy custom proto file to proto directory
+  if [[ " $@ " == *" --custom_proto "* ]]; then
+    if [ -z "${SMTD_CUSTOM_PATH}" ]; then
+      echo "Error: SMTD_CUSTOM_PATH is not set. See DEVELOPING.md"  >&2
+      exit 1
+    fi
+
+    cp ${SMTD_CUSTOM_PATH}/custom_proto/custom_proto.proto ./src/smtd/proto/custom_proto.proto
+  else 
+    echo "syntax = \"proto3\";
+          package SmtD;
+
+          message SmtDWrapperCustomOptions {
+            uint32 custom = 1;
+          }" > ./src/smtd/proto/custom_proto.proto
+  fi
+
+  # Copy custom worker heuristics file to worker science directory
+  if [[ " $@ " == *" --custom_worker "* ]]; then
+    if [ -z "${SMTD_CUSTOM_PATH}" ]; then
+      echo "Error: SMTD_CUSTOM_PATH is not set. See DEVELOPING.md"  >&2
+      exit 1
+    fi
+
+    cp ${SMTD_CUSTOM_PATH}/custom_worker_heuristics/CustomHeuristics.cpp ./src/smtd/workers/src/science/CustomHeuristics.cpp
+    cp ${SMTD_CUSTOM_PATH}/custom_worker_heuristics/CustomHeuristics.h ./src/smtd/workers/src/science/CustomHeuristics.h
+  else 
+    echo "#include <iostream>
+          #include \"CustomHeuristics.h\"
+
+          void CustomHeuristics::dummy(SmtD::SmtDStatus &d_stats, std::optional<std::reference_wrapper<const cvc5::Term>> lemma, SemiStructuredContext &ssctx, SmtDWorkerInterface &d_interface) {
+              return;
+          }" > ./src/smtd/workers/src/science/CustomHeuristics.cpp
+    echo "#ifndef CVC5__CUSTOM_HEURISTICS_H
+          #define CVC5__CUSTOM_HEURISTICS_H
+          #include \"UserHeuristics.h\"
+          class CustomHeuristics : public UserHeuristics {
+          public:
+              void dummy(SmtD::SmtDStatus &d_stats, std::optional<std::reference_wrapper<const cvc5::Term>> lemma, SemiStructuredContext &ssctx, SmtDWorkerInterface &d_interface) override;
+              };
+          #endif " > ./src/smtd/workers/src/science/CustomHeuristics.h
+  fi
+
   # Ideally: Put all generated stuff in a top-level build folder
   hatch run python3.11 -m grpc_tools.protoc \
     --python_out=./src \

src/smtd/broker/main.py

@@ -19,6 +19,7 @@
 from smtd.broker.science.brokers.parse_time_broker import parse_time_broker
 from smtd.broker.science.brokers.rate_broker import rate_broker
 from smtd.broker.science.brokers.size_broker import size_broker
+from smtd.broker.science.brokers.user_broker import user_broker
 from smtd.broker.science.ClusterMap import ClusterMap
 from smtd.broker.science.statistics.formatting_helpers import (
     parse_key_value_pairs,
@@ -54,8 +55,9 @@ async def async_entry():
     else:
         cluster_config = {"partitioners": []}
 
+    optional_env_vars = ["SMTD_CUSTOM_PATH"]
     for var, val in config.items():
-        if val is None:
+        if val is None and not var in optional_env_vars:
             # TODO: Update when creating first release -- non-developer users should not be directed to DEVELOPING.md
             logging.error(f"Environment variable {var} is not set. See DEVELOPING.md")
             raise FileNotFoundError
@@ -95,6 +97,7 @@ async def async_entry():
                 "size": size_broker,
                 "rate": rate_broker,
                 "parse": parse_time_broker,
+                "user": user_broker,
             }[args.broker]
             logging.warning(f"Using {broker_implementation}.")
             winner, result, winner_duration = await broker_implementation(

src/smtd/broker/parse_args.py

@@ -30,14 +30,20 @@
 parser.add_argument(
     "--share_theory_lemma", action="store_true", help="Share theory lemmas (default: False)"
 )
+parser.add_argument(
+    "--user_stats", action="store_true", help="Use user-implemented statistics (default: False)"
+)
+parser.add_argument(
+    "--user_control_loop", action="store_true", help="Use user-implemented control loop (default: False)"
+)
 
 # old is now unsupported since it relies heavily on strings, and is not easily portable to atom caching
 # parser.add_argument('--broker', type=str, default='old', choices=['old', 'size', 'rate', 'weighted', 'parse'], help='Broker strategy to use.')
 parser.add_argument(
     "--broker",
     type=str,
     default="parse",
-    choices=["size", "rate", "weighted", "parse"],
+    choices=["size", "rate", "weighted", "parse", "user",],
     help="Broker strategy to use.",
 )
 parser.add_argument(
@@ -181,7 +187,7 @@
     "--scrambler_seed",
     type=int,
     default=100,
-    help="Seed for scrambler (default: 100; DO NOT USE 0!!)",
+    help="Seed for scrambler (default: 100; DO NOT USE 0!)",
 )
 parser.add_argument(
     "--scrambler_shuffle_decls",

src/smtd/broker/parse_config.py

@@ -1,6 +1,6 @@
 import os
 
-env_variables = ["SMTD_CVC5_REPO_PATH", "SMTD_SCRAMBLER_PATH"]
+env_variables = ["SMTD_CVC5_REPO_PATH", "SMTD_SCRAMBLER_PATH", "SMTD_CUSTOM_PATH"]
 
 # Config dictionary is for non-user-configurable relative paths within the project,
 # as well as for external dependencies fetched from environment variables.
@@ -14,4 +14,4 @@
 
 # TODO: move all build artifacts to to top-level 'build' directory
 config["WORKER_EXE_PATH"] = "src/smtd/workers/build-release/smtd-worker"
-config["PROTO_DIR_PATH"] = "src/smtd/proto/"
+config["PROTO_DIR_PATH"] = "src/smtd/proto/"

src/smtd/broker/science/SemiStructuredContext.py

@@ -9,10 +9,10 @@
 from smtd.broker.science.statistics.formatting_helpers import n5
 from smtd.broker.systems.servers.SmtDWorker import SmtDWorker
 from smtd.broker.systems.SmtDBrokerInterface import SmtDBrokerInterface
-from smtd.proto import semi_structured_api_pb2 as soapi
+from smtd.proto import semi_structured_api_pb2 as ssapi
 from smtd.proto import service_api_pb2 as pb
 
-UUID_t = soapi.SmtSemiStructuredDefinitionUUID
+UUID_t = ssapi.SmtSemiStructuredDefinitionUUID
 
 
 def _u2p(uuid):
@@ -50,7 +50,7 @@ def __init__(self):
     def synchronize_definition(
         self,
         sender: SmtDWorker,
-        d: soapi.SmtSemiStructuredDefinition,
+        d: ssapi.SmtSemiStructuredDefinition,
         interface: SmtDBrokerInterface,
     ):
         self.unmapping[_u2p(d.new_uuid)] = d.str
@@ -75,20 +75,20 @@ def synchronize_definition(
             self.unique_atom_stats[sender] += 1
             # for s in interface.workers: self.knows_about[s].add(_u2p(d.uuid))
 
-    def to_string(self, l: soapi.SmtSemiStructuredExpression) -> str:
+    def to_string(self, l: ssapi.SmtSemiStructuredExpression) -> str:
         if l.HasField("connective"):
             prefix = {
-                soapi.OR: "(or ",
-                soapi.AND: "(and ",
-                soapi.NOT: "(not ",
+                ssapi.OR: "(or ",
+                ssapi.AND: "(and ",
+                ssapi.NOT: "(not ",
             }[l.connective.kind]
             infix = " ".join(self.to_string(c) for c in l.connective.children)
             suffix = ")"
             return prefix + infix + suffix
         else:
             return self.unmapping.get(pair := _u2p(l.uuid), f"<< unknown uuid {pair} >>")
 
-    # def remap(self, sender: SmtDWorker, l: soapi.SmtSemiStructuredExpression):
+    # def remap(self, sender: SmtDWorker, l: ssapi.SmtSemiStructuredExpression):
     #     # todo: we can sort the children and maybe do some deduplication here if we want.
     #     if l.HasField('uuid'):
     #         remapped_uuid = self.remapping.get(_u2p(l.uuid))
@@ -99,7 +99,7 @@ def to_string(self, l: soapi.SmtSemiStructuredExpression) -> str:
     #         for c in l.connective.children:
     #             self.remap(sender, c)
 
-    # def safe_to_send(self, l: soapi.SmtSemiStructuredExpression, to: SmtDWorker):
+    # def safe_to_send(self, l: ssapi.SmtSemiStructuredExpression, to: SmtDWorker):
     #     if l.HasField('uuid'):
     #         if _u2p(l.uuid) not in self.knows_about[to]:
     #             logging.error(f"Attempting to send lemma containing UUID {l.uuid} (which was remapped to {self.remapping.get(_u2p(l.uuid))}) to worker {to} which does not know about that UUID.")

src/smtd/broker/science/brokers/parse_time_broker.py

@@ -217,6 +217,7 @@ async def parse_time_broker(
                     interface.export_immediate(req, to_specific_workers={sender})
 
                 if message.HasField("define"):
+                    # print("PROCESSING DEFINE MESSAGE")
                     ssctx.synchronize_definition(sender, message.define, interface)
 
                 if message.HasField("lemma"):
@@ -226,7 +227,7 @@ async def parse_time_broker(
                     if message.lemma.metadata.length == 1:
                         if args.log_unit_clauses:
                             logging.info(
-                                f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.soapi)[:100]}`... was discovered by {sender}"
+                                f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.ssapi)[:100]}`... was discovered by {sender}"
                             )
                         stats.incr("unit_clauses", sender, +1)
 
@@ -238,7 +239,7 @@ async def parse_time_broker(
                     ), "weighted broker does not support partitioning yet."
 
                     fwd = pb.ToSmtDMessage()
-                    fwd.lemma.expr.soapi.CopyFrom(message.lemma.expr.soapi)
+                    fwd.lemma.expr.ssapi.CopyFrom(message.lemma.expr.ssapi)
                     for receiver in interface.workers - {sender}:
                         current_adaptive_share_length = share_length_controllers[receiver].output
                         if message.lemma.metadata.length <= current_adaptive_share_length:

src/smtd/broker/science/brokers/rate_broker.py

@@ -169,7 +169,7 @@ async def rate_broker(
                     )  # we don't support more than 1 formula currently
                     if args.log_unit_clauses:
                         logging.info(
-                            f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.soapi)[:100]}`... was discovered by {sender}"
+                            f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.ssapi)[:100]}`... was discovered by {sender}"
                         )
                     if message.lemma.metadata.length == 1:
                         stats.incr("unit_clauses", sender, +1)

src/smtd/broker/science/brokers/size_broker.py

@@ -26,7 +26,7 @@
 from smtd.broker.science.statistics.SimpleStatsHandler import SimpleStatsHandler
 from smtd.broker.systems.servers.LocalSmtDWorker import LocalSmtDWorker
 from smtd.broker.systems.SmtDBrokerInterface import SmtDBrokerInterface
-from smtd.proto import semi_structured_api_pb2 as soapi
+from smtd.proto import semi_structured_api_pb2 as ssapi
 from smtd.proto import service_api_pb2 as pb
 
 
@@ -136,7 +136,7 @@ async def size_broker(
                     )  # we don't support more than 1 formula currently
                     if args.log_unit_clauses:
                         logging.info(
-                            f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.soapi)[:100]}`... was discovered by {sender}"
+                            f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.ssapi)[:100]}`... was discovered by {sender}"
                         )
                     if message.lemma.metadata.length == 1:
                         stats.incr("unit_clauses", sender, +1)
@@ -151,7 +151,7 @@ async def size_broker(
                     assert message.lemma.metadata.length <= args.max_share_length
 
                     sent_msg = pb.ToSmtDMessage()
-                    sent_msg.lemma.expr.soapi.CopyFrom(message.lemma.expr.soapi)
+                    sent_msg.lemma.expr.ssapi.CopyFrom(message.lemma.expr.ssapi)
                     interface.export_immediate(
                         sent_msg, to_specific_workers=interface.workers - {sender}
                     )