Repository cleanup: stray files, dead code and duplicated logic

.gitignore

@@ -11,17 +11,11 @@ tags
 .ycm_extra_conf.pyc
 # documentation
 doc/*
-# Python cache
-python_interface/__pycache__
-
+# editor and OS files
 .vscode/*
-backup/*
-equivalence_or_not/tables/*
-equivalence_or_not/*/*.json
-dyadic/tables/*
-dyadic/*/*.json
-revlib/tables/*
-revlib/*/*.json
+.DS_Store
+
+# results produced by the benchmark scripts
 benchmark*/**/tables/**
 benchmark*/**/*.json
 POPL24/TABLES/Algorithms/*.pdf

cli/CMakeLists.txt

@@ -23,11 +23,6 @@ file(GLOB main_files "${CMAKE_CURRENT_SOURCE_DIR}/*.cc")
 foreach(file ${main_files})
     get_filename_component(binary ${file} NAME_WLE)
     add_executable(${binary} ${file} ${CMAKE_CURRENT_BINARY_DIR}/version.cc)
-    get_target_property(sources ${binary} SOURCES)
-    foreach(src ${sources})
-        # CLI-only: -DCACHE_AC -DCACHE_OPT_CONGR (optional: -DOPT_AC, -DCACHE_CONGR, -march=native)
-        set_source_files_properties(${src} PROPERTIES COMPILE_FLAGS "-DCACHE_AC -DCACHE_OPT_CONGR")
-    endforeach()
     target_link_libraries(${binary} lsta)
 endforeach()
 

cli/autoq.cc

@@ -4,7 +4,6 @@
 #include "autoq/error.hh"
 #include "autoq/error_messages.hh"
 #include "autoq/parsing/parser/timbuk_parser.hh"
-#include "autoq/parsing/complex_parser.hh"
 #include "autoq/serialization/timbuk_serializer.hh"
 #include "autoq/aut_description.hh"
 #include "autoq/inclusion.hh"
@@ -20,7 +19,6 @@
 #include <iomanip>
 #include <regex>
 #include <fenv.h>
-#include <csignal>
 #ifdef __APPLE__
 #include <fenv_darwin.h>
 #endif
@@ -52,8 +50,6 @@ int extract_qubit(const std::string& filename) {
 }
 
 namespace {
-constexpr unsigned int kTimeoutSeconds = 1800;
-constexpr int kExitCodeTimeout = 124;
 constexpr size_t kBytesPerMB = 1024 * 1024;
 
 // CLI option names (placeholder names in help)
@@ -113,35 +109,6 @@ void print_equivalence_result(bool result,
 
 using AUTOQ::adjust_N_in_nTuple;
 
-namespace {
-AUTOQ::ConcreteAutomata* g_timeout_aut1 = nullptr;
-AUTOQ::ConcreteAutomata* g_timeout_aut2 = nullptr;
-}
-
-void timeout_handler(int) {
-    auto& st = AUTOQ::default_execution_stats();
-    std::map<std::string, std::string> stats;
-    stats["gate"] = AUTOQ::Util::Convert::ToString(st.total_gate_time - st.total_removeuseless_time - st.total_reduce_time);
-    stats["removeuseless"] = AUTOQ::Util::Convert::ToString(st.total_removeuseless_time);
-    stats["reduce"] = AUTOQ::Util::Convert::ToString(st.total_reduce_time);
-    stats["include"] = AUTOQ::Util::Convert::ToString(st.total_include_time);
-    stats["total"] = std::to_string(kTimeoutSeconds);
-    stats["result"] = std::to_string(st.gateCount);
-    stats["aut1.trans"] = g_timeout_aut1 ? std::to_string(g_timeout_aut1->count_transitions()) : "0";
-    stats["aut1.leaves"] = g_timeout_aut1 ? std::to_string(g_timeout_aut1->count_leaves()) : "0";
-    stats["aut2.trans"] = g_timeout_aut2 ? std::to_string(g_timeout_aut2->count_transitions()) : "0";
-    stats["aut2.leaves"] = g_timeout_aut2 ? std::to_string(g_timeout_aut2->count_leaves()) : "0";
-        AUTOQ::Util::Log::info(AUTOQ::Util::Convert::ToString2(stats));
-    exit(kExitCodeTimeout);
-}
-
-void set_timeout(unsigned int seconds, AUTOQ::ConcreteAutomata* aut1, AUTOQ::ConcreteAutomata* aut2) {
-    g_timeout_aut1 = aut1;
-    g_timeout_aut2 = aut2;
-    signal(SIGALRM, timeout_handler);
-    alarm(seconds);
-}
-
 template<typename Symbol>
 static void run_execution_impl(const std::string& pre, const std::string& circuit,
                                const ParameterMap& params) {
@@ -176,7 +143,6 @@ static void run_equivalence(const std::string& circuit1, const std::string& circ
         THROW_AUTOQ_ERROR("Cannot extract qubit count from circuit: " + circuit2);
     AUTOQ::ConcreteAutomata aut = AUTOQ::ConcreteAutomata::prefix_basis(n1);
     AUTOQ::ConcreteAutomata aut2 = AUTOQ::ConcreteAutomata::prefix_basis(n2);
-    // set_timeout(kTimeoutSeconds, &aut, &aut2);  // optional: enable to dump stats on timeout
     aut.execute(circuit1, {}, {}, params);
     aut2.execute(circuit2, {}, {}, params);
     bool result = aut <<= aut2;
@@ -191,10 +157,9 @@ template<typename Symbol>
 static void run_verification_impl(const std::string& pre, const std::string& post, const std::string& circuit,
                                   const ParameterMap& params, bool latex,
                                   const chrono::steady_clock::time_point& start) {
-    using Aut = AUTOQ::Automata<Symbol>;
     auto& st = AUTOQ::default_execution_stats();
     st.startFromFileToAutomata = std::chrono::steady_clock::now();
-    auto [autVec, qp] = AUTOQ::Parsing::TimbukParser<Symbol, Symbol>::ReadTwoAutomata(pre, post, circuit);
+    auto [autVec, qp] = AUTOQ::Parsing::TimbukParser<Symbol>::ReadTwoAutomata(pre, post, circuit);
     st.endFromFileToAutomata = std::chrono::steady_clock::now();
     auto aut = autVec.at(0);
     auto spec = autVec.at(1);
@@ -213,18 +178,16 @@ static void run_verification(const std::string& pre, const std::string& post, co
     auto spec1 = ReadAutomaton(post);
     auto pre1 = ReadAutomaton(pre);
     if (std::holds_alternative<AUTOQ::SymbolicAutomata>(spec1) || std::holds_alternative<AUTOQ::SymbolicAutomata>(pre1) || AUTOQ::SymbolicAutomata::check_the_invariants_types(circuit) == "Symbolic") {
-        auto aut1 = ReadAutomaton(pre);
-        if (std::holds_alternative<AUTOQ::PredicateAutomata>(aut1))
+        if (std::holds_alternative<AUTOQ::PredicateAutomata>(pre1))
             THROW_AUTOQ_ERROR(EM::kPredicatePrecondition);
         run_verification_impl<AUTOQ::Symbol::Symbolic>(pre, post, circuit, params, latex, start);
     } else if (std::holds_alternative<AUTOQ::PredicateAutomata>(spec1)) {
         THROW_AUTOQ_ERROR(EM::kPredicateAutomataPost);
     } else if (std::holds_alternative<AUTOQ::ConcreteAutomata>(spec1)) {
-        auto aut1 = ReadAutomaton(pre);
         std::visit([](auto&& arg) {
             if constexpr (!std::is_same_v<std::decay_t<decltype(arg)>, AUTOQ::ConcreteAutomata>)
                 THROW_AUTOQ_ERROR(EM::kConcretePostPre);
-        }, aut1);
+        }, pre1);
         run_verification_impl<AUTOQ::Symbol::Concrete>(pre, post, circuit, params, latex, start);
     } else {
         THROW_AUTOQ_ERROR(EM::kUnsupportedPostType);

include/autoq/complex/constrained_complex.hh

@@ -33,79 +33,43 @@ struct AUTOQ::Complex::ConstrainedComplex : std::map<int, std::tuple<std::string
     ConstrainedComplex& operator+=(const ConstrainedComplex &o) { *this = *this + o; return *this; }
     ConstrainedComplex operator*(const ConstrainedComplex &o) const {
         AUTOQ::Complex::ConstrainedComplex result;
-
-        if (this->size() < o.size()) {
-            for (const auto &[k, v] : *this) {
-                auto it = o.find(k);
-                if (it != o.end()) { // we only merge common terms (keys)
-                    std::tuple<std::string, std::vector<bool>, std::vector<bool>> obj;
-                    const auto &w = it->second;
-                    if (std::get<0>(v) != std::get<0>(w)) {
-                        THROW_AUTOQ_ERROR("One term can only have one coefficient!");
-                    } else {
-                        std::get<0>(obj) = std::get<0>(v);
-                    }
-                    if (std::get<1>(v).size() != std::get<1>(w).size()) {
-                        THROW_AUTOQ_ERROR("All terms should have the same number of global constraints!");
-                    } else {
-                        const auto &a = std::get<1>(v);
-                        const auto &b = std::get<1>(w);
-                        auto &c = std::get<1>(obj);
-                        c.resize(a.size());
-                        for (size_t i = 0; i < a.size(); ++i) {
-                            c[i] = a[i] || b[i]; // merge global constraints
-                        }
-                    }
-                    if (std::get<2>(v).size() != std::get<2>(w).size()) {
-                        THROW_AUTOQ_ERROR("The same terms should have the same number of local constraints!");
-                    } else {
-                        const auto &a = std::get<2>(v);
-                        const auto &b = std::get<2>(w);
-                        auto &c = std::get<2>(obj);
-                        c.resize(a.size());
-                        for (size_t i = 0; i < a.size(); ++i) {
-                            c[i] = a[i] || b[i]; // merge global constraints
-                        }
-                    }
-                    result[k] = obj;
+        // Iterate over the smaller operand and look terms up in the larger one;
+        // the merge below is symmetric, so the choice does not affect the result.
+        const ConstrainedComplex &small = (this->size() < o.size()) ? *this : o;
+        const ConstrainedComplex &large = (this->size() < o.size()) ? o : *this;
+        for (const auto &[k, v] : small) {
+            auto it = large.find(k);
+            if (it == large.end()) continue; // we only merge common terms (keys)
+            std::tuple<std::string, std::vector<bool>, std::vector<bool>> obj;
+            const auto &w = it->second;
+            if (std::get<0>(v) != std::get<0>(w)) {
+                THROW_AUTOQ_ERROR("One term can only have one coefficient!");
+            } else {
+                std::get<0>(obj) = std::get<0>(v);
+            }
+            if (std::get<1>(v).size() != std::get<1>(w).size()) {
+                THROW_AUTOQ_ERROR("All terms should have the same number of global constraints!");
+            } else {
+                const auto &a = std::get<1>(v);
+                const auto &b = std::get<1>(w);
+                auto &c = std::get<1>(obj);
+                c.resize(a.size());
+                for (size_t i = 0; i < a.size(); ++i) {
+                    c[i] = a[i] || b[i]; // merge global constraints
                 }
             }
-        } else {
-            for (const auto &[k, v] : o) {
-                auto it = this->find(k);
-                if (it != this->end()) { // we only merge common terms (keys)
-                    std::tuple<std::string, std::vector<bool>, std::vector<bool>> obj;
-                    const auto &w = it->second;
-                    if (std::get<0>(v) != std::get<0>(w)) {
-                        THROW_AUTOQ_ERROR("One term can only have one coefficient!");
-                    } else {
-                        std::get<0>(obj) = std::get<0>(v);
-                    }
-                    if (std::get<1>(v).size() != std::get<1>(w).size()) {
-                        THROW_AUTOQ_ERROR("All terms should have the same number of global constraints!");
-                    } else {
-                        const auto &a = std::get<1>(v);
-                        const auto &b = std::get<1>(w);
-                        auto &c = std::get<1>(obj);
-                        c.resize(a.size());
-                        for (size_t i = 0; i < a.size(); ++i) {
-                            c[i] = a[i] || b[i]; // merge global constraints
-                        }
-                    }
-                    if (std::get<2>(v).size() != std::get<2>(w).size()) {
-                        THROW_AUTOQ_ERROR("The same terms should have the same number of local constraints!");
-                    } else {
-                        const auto &a = std::get<2>(v);
-                        const auto &b = std::get<2>(w);
-                        auto &c = std::get<2>(obj);
-                        c.resize(a.size());
-                        for (size_t i = 0; i < a.size(); ++i) {
-                            c[i] = a[i] || b[i]; // merge global constraints
-                        }
-                    }
-                    result[k] = obj;
+            if (std::get<2>(v).size() != std::get<2>(w).size()) {
+                THROW_AUTOQ_ERROR("The same terms should have the same number of local constraints!");
+            } else {
+                const auto &a = std::get<2>(v);
+                const auto &b = std::get<2>(w);
+                auto &c = std::get<2>(obj);
+                c.resize(a.size());
+                for (size_t i = 0; i < a.size(); ++i) {
+                    c[i] = a[i] || b[i]; // merge local constraints
                 }
             }
+            result[k] = obj;
         }
         return result;
     }

include/autoq/gate_helpers.hh

@@ -16,7 +16,7 @@ void concrete_gate_finish(AUTOQ::Automata<Symbol>& self, const char* name, int t
     self.stats_->total_gate_time += duration;
     if (self.stats_->gateLog)
         std::cout << name << t << "：" << self.stateNum << " states " << self.count_transitions()
-                  << " transitions " << AUTOQ::Util::print_duration(duration) << "\n";
+                  << " transitions " << AUTOQ::Util::Convert::ToString(duration) << "\n";
 }
 
 /// Copy result base fields from src and check state-number overflow for product-shaped expansion.