FMCAD25

CMakeLists.txt

@@ -1,4 +1,4 @@
-cmake_minimum_required(VERSION 3.30)
+cmake_minimum_required(VERSION 3.16)
 project(dreal4_cmake)
 include(CMakePrintHelpers)
 
@@ -52,6 +52,8 @@ set(LIBCDS_HOME "${PROJECT_SOURCE_DIR}/src/third_party/com_github_khizmax_libcds
 set(JSON_HOME "${PROJECT_SOURCE_DIR}/src/third_party/com_github_nlohmann_json/")
 set(PICOSAT_HOME "${PROJECT_SOURCE_DIR}/src/third_party/com_github_dreal-deps_picosat/")
 
+unset(DREAL_SOURCES)
+unset(DREAL_SOURCES CACHE)
 file(GLOB_RECURSE DREAL_SOURCES
         "${PROJECT_SOURCE_DIR}/src/dreal/*/**.cc"
         "${PROJECT_SOURCE_DIR}/src/dreal/*/**.yy"
@@ -61,7 +63,7 @@ file(GLOB_RECURSE DREAL_SOURCES
         "${LIBCDS_HOME}/src/**.cpp"
         "${PICOSAT_HOME}/src/**.c"
 )
-add_library(dreal4_cmake
+add_library(dreal4_cmake STATIC
         ${DREAL_SOURCES}
         ${BISON_smt2_parser_OUTPUTS} ${FLEX_smt2_scanner_OUTPUTS}
         ${BISON_dr_parser_OUTPUTS} ${FLEX_dr_scanner_OUTPUTS}
@@ -79,8 +81,9 @@ target_include_directories(dreal4_cmake PUBLIC
 )
 
 # system dependencies
+find_library(   FLEX_LIB NAMES libfl.a    HINTS "${FLEX_ROOT}" PATH_SUFFIXES lib libs lib32 lib64 REQUIRED NO_CACHE)
 target_include_directories(dreal4_cmake PUBLIC "${FLEX_INCLUDE_DIRS}")
-target_link_libraries(dreal4_cmake PUBLIC "${FLEX_LIBRARIES}")
+target_link_libraries(dreal4_cmake PUBLIC "${FLEX_LIB}")
 
 find_path(       GMP_INC NAMES gmpxx.h    HINTS "${GMP_ROOT}" PATH_SUFFIXES include includes     REQUIRED NO_CACHE)
 find_library(  GMP_C_LIB NAMES libgmp.a   HINTS "${GMP_ROOT}" PATH_SUFFIXES lib libs lib32 lib64 REQUIRED NO_CACHE)
@@ -106,7 +109,7 @@ include(FetchContent)
 FetchContent_Declare(
         ibex
         GIT_REPOSITORY https://github.com/ncsys-lab/ibex-lib
-        GIT_TAG 4d61b84139eaeab628506d9edaf5fd8879a3302e)  # Kunal's M1 + namespace fixes
+        GIT_TAG 33408ed0733da56979ddf797473609d4c39ea1ea)  # Kunal's M1 + namespace fixes
 FetchContent_MakeAvailable(ibex)
 
 FetchContent_Declare(
@@ -154,6 +157,9 @@ target_link_libraries(
         dreal4_cmake PUBLIC ibex nlopt spdlog::spdlog fmt::fmt
 )
 
+# On some platforms, linking is purely sequential, and the order you specify libraries in matters.
+# I am repeating these libraries from above so that everything gets resolved on Ubuntu
+target_link_libraries(dreal4_cmake PUBLIC "${GMP_C_LIB}" "${GMP_CXX_LIB}")
 
 # executable
 add_executable(dreal4 "${PROJECT_SOURCE_DIR}/src/dreal/dreal_main.cc")

src/dreal/dreal_main.cc

@@ -476,6 +476,24 @@ void HandleSigInt(const int) {
 }  // namespace
 
 int main(int argc, const char* argv[]) {
+  // default stack size is 8MB
+  // CPS-pattern matching algo goes DEEP...
+  // doing 63MB because that's approximately the max on macOS
+  constexpr rlim_t desired_stack_size = 63 * 1024 * 1024;
+  rlimit rl{0};
+  getrlimit(RLIMIT_STACK, &rl);
+  rl.rlim_cur = std::max(rl.rlim_cur, desired_stack_size);
+  setrlimit(RLIMIT_STACK, &rl);
+  rl.rlim_cur = 0;
+  getrlimit(RLIMIT_STACK, &rl);
+  if (rl.rlim_cur < desired_stack_size) {
+    std::cerr << "Failed to configure desired stack size limit. Exiting." << std::endl;
+    std::cerr << "\tCurrent Size = " << rl.rlim_cur << std::endl;
+    std::cerr << "\tMaximum Size = " << rl.rlim_max << std::endl;
+    std::cerr << "\tDesired Size = " << desired_stack_size << std::endl;
+    exit(-1);
+  }
+
   std::signal(SIGINT, HandleSigInt);
   dreal::MainProgram main_program{argc, argv};
   return main_program.Run();

src/dreal/solver/auditor.cc

@@ -18,16 +18,73 @@
 #include "dreal/solver/filter_assertion.h"
 #include "dreal/util/assert.h"
 #include "dreal/util/logging.h"
+#include "dreal/version.h"
 
 namespace dreal
 {
-    void audit(const Formula& formula, const std::optional<Box>& box) {
+    std::ofstream literal_log("/tmp/dreal_audit_sat_literal_log.txt");
+    std::set<int> literal_log_clause;
+
+    void sat_log_label_clause(const std::string& s) {
+        if (!DREAL_EXPERIMENTAL_SAT_AUDIT_ENABLED) return;
+        literal_log << s << std::endl;
+    }
+
+    void sat_log_literal(const int lit, const std::optional<Variable>& def) {
+        if (!DREAL_EXPERIMENTAL_SAT_AUDIT_ENABLED) return;
+        DREAL_ASSERT(lit != 0);
+
+        static std::set<Variable> seen_literals;
+        if (def && !seen_literals.count(*def)) {
+            literal_log << "def:\t" << ::abs(lit) << " := " << *def << std::endl;
+            seen_literals.emplace(*def);
+        }
+
+        literal_log_clause.insert(lit);
+    }
+
+    void sat_log_literal0() {
+        if (!DREAL_EXPERIMENTAL_SAT_AUDIT_ENABLED) return;
+        for (int v : literal_log_clause) literal_log << v << ' ';
+        literal_log << '0' << std::endl;
+        literal_log_clause.clear();
+    }
+
+    void theory_audit_literals(
+        const std::string& label,
+        const PredicateAbstractor& pa, /*copy*/ std::vector<Formula> lits, const std::optional<Box>& box
+    ) {
+        // the operands passed here are expensive to produce, so really shouldn't be called unnecessarily.
+        DREAL_ASSERT(DREAL_EXPERIMENTAL_THEORY_AUDIT_ENABLED);
+
+        for (auto& l : lits) {
+            if (is_variable(l)) {
+                // f = b
+                const auto iter = pa.var_to_formula_map().find(get_variable(l));
+                if (iter != pa.var_to_formula_map().end()) l = iter->second;
+                // else ...  the variable is probably, actually, a BOOL such as `DigitalPDController_0__omega_sensor_bit0__t0ad`
+            }
+            else {
+                // f = ¬b
+                DREAL_ASSERT(is_negation(l) && is_variable(get_operand(l)));
+                const auto iter = pa.var_to_formula_map().find(get_variable(get_operand(l)));
+                if (iter != pa.var_to_formula_map().end()) l = !iter->second;
+                // else ...  the variable is probably, actually, a BOOL such as `DigitalPDController_0__omega_sensor_bit0__t0ad`
+            }
+        }
+        theory_audit_formula(label, make_disjunction(lits), box);
+    }
+
+    void theory_audit_formula(const std::string& label, const Formula& formula, const std::optional<Box>& box) {
+        // the operands passed here are expensive to produce, so really shouldn't be called unnecessarily.
+        DREAL_ASSERT(DREAL_EXPERIMENTAL_THEORY_AUDIT_ENABLED);
+
         const auto& vs = formula.GetFreeVariables();
 
         std::string lemma_comment;
         {
             std::ostringstream s;
-            s << ";\t∀ ";
+            s << ";\t" << label << "\t∀ ";
             for (const auto& v : vs) {
                 s << v;
                 if (box) s << "∈" << (*box)[v];

src/dreal/solver/auditor.h

@@ -6,10 +6,22 @@
 #define AUDITOR_H
 
 #include <dreal/util/box.h>
+#include <dreal/util/predicate_abstractor.h>
+#include <optional>
 
 namespace dreal
 {
-    void audit(const Formula& formula, const std::optional<Box>& box);
+
+    void sat_log_label_clause(const std::string& label);
+    void sat_log_literal(int lit, const std::optional<Variable>& def = {});
+    void sat_log_literal0();
+
+    void theory_audit_literals(
+        const std::string& label,
+        const PredicateAbstractor& pa, /*copy*/ std::vector<Formula> lits,
+        const std::optional<Box>& box
+    );
+    void theory_audit_formula(const std::string& label, const Formula& formula, const std::optional<Box>& box);
 }
 
 #endif //AUDITOR_H

src/dreal/solver/context.cc

@@ -113,7 +113,26 @@ optional<string> Context::GetOption(const string& key) const {
 const Config& Context::config() const { return impl_->config(); }
 Config& Context::mutable_config() { return impl_->mutable_config(); }
 
-string Context::version() { return DREAL_VERSION_STRING; }
+string Context::version() {
+  std::ostringstream oss;
+  oss << DREAL_VERSION_FULL << '.';
+  oss << DREAL_VERSION_MAJOR << '.';
+  oss << DREAL_VERSION_MINOR << '.';
+  oss << DREAL_VERSION_REVISION << '.';
+
+  oss << "patmat" << pattern_matching_mode << '.';
+  oss << "parmod" << partial_model_mode << '.';
+
+  oss << "audit" <<
+    static_cast<int>(DREAL_EXPERIMENTAL_THEORY_AUDIT_ENABLED) <<
+    static_cast<int>(DREAL_EXPERIMENTAL_SAT_AUDIT_ENABLED);
+
+#ifdef DREAL_EXPERIMENTAL_GENERATE_HEURISTICS_CSV
+  oss << ".GENERATE_CSV";
+#endif
+
+  return oss.str();
+}
 
 const Box& Context::box() const { return impl_->box(); }