separate out approxmc when counting

arijitsh · arijitsh · commit ec7cb67e11a9 · 2024-04-03T13:34:08.000-04:00
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -529,6 +529,7 @@ if (NOT NOUNIGEN)
     message(STATUS "ApproxMC static lib:  ${APPROXMC_STATIC_LIBRARIES}")
     message(STATUS "ApproxMC static lib deps: ${APPROXMC_STATIC_LIBRARIES_DEPS}")
     message(STATUS "ApproxMC include dirs: ${APPROXMC_INCLUDE_DIRS}")
+    include_directories(SYSTEM ${APPROXMC_INCLUDE_DIRS})
 
   find_package(sbva CONFIG REQUIRED)
     message(STATUS "Found sbva")
diff --git a/include/stp/Sat/ApxMC.h b/include/stp/Sat/ApxMC.h
@@ -0,0 +1,102 @@
+/********************************************************************
+ * AUTHORS: Arijit Shaw
+ *
+ * BEGIN DATE: November, 2023
+ *
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
+********************************************************************/
+
+/*
+ * Wraps around ApproxMC.
+ */
+#ifndef APXMC_H_
+#define APXMC_H_
+
+#include "approxmc/approxmc.h"
+#include "stp/Sat/SATSolver.h"
+#include <arjun/arjun.h>
+
+#include <unordered_set>
+
+using std::vector;
+
+namespace ApxMC
+{
+class SATSolver;
+}
+
+namespace stp
+{
+#if defined(__GNUC__) || defined(__clang__)
+class __attribute__((visibility("default"))) ApxMC : public SATSolver
+#else
+class ApxMC : public SATSolver
+#endif
+
+{
+  ApproxMC::AppMC* a;
+  ArjunNS::Arjun* arjun;
+  uint64_t seed;
+
+public:
+  ApxMC(uint64_t unisamp_seed);
+
+  ~ApxMC();
+
+  virtual void setMaxConflicts(int64_t max_confl); // set max solver conflicts
+
+  virtual void setMaxTime(int64_t max_time); // set max solver time in seconds
+
+  bool addClause(const vec_literals& ps); // Add a clause to the solver.
+
+  bool okay() const; // FALSE means solver is in a conflicting state
+
+  bool solve(bool& timeout_expired); // Search without assumptions.
+
+  virtual uint8_t modelValue(uint32_t x) const;
+
+  virtual uint32_t newVar();
+
+  void setVerbosity(int v);
+
+  unsigned long nVars() const;
+
+  void printStats() const;
+
+  virtual void enableRefinement(const bool enable);
+
+  // nb CryptoMiniSat has different literal values to the other minisats.
+  virtual lbool true_literal() { return ((uint8_t)1); }
+  virtual lbool false_literal() { return ((uint8_t)-1); }
+  virtual lbool undef_literal() { return ((uint8_t)0); }
+
+  uint32_t
+  getFixedCountWithAssumptions(const stp::SATSolver::vec_literals& assumps,
+                               const std::unordered_set<unsigned>& literals);
+
+  void solveAndDump();
+
+private:
+  void* temp_cl;
+  int64_t max_confl = 0;
+  int64_t max_time = 0; // seconds
+};
+} // namespace stp
+
+#endif
diff --git a/lib/STPManager/STP.cpp b/lib/STPManager/STP.cpp
@@ -34,6 +34,7 @@ THE SOFTWARE.
 #endif
 
 #ifdef USE_UNIGEN
+#include "stp/Sat/ApxMC.h"
 #include "stp/Sat/UniSamp.h"
 #include "stp/Sat/CMSGen.h"
 #endif
@@ -124,10 +125,9 @@ SATSolver* STP::get_new_sat_solver()
       break;
     case UserDefinedFlags::APPROXMC_SOLVER:
 #ifdef USE_UNIGEN
-      newS = new UniSamp(bm->UserFlags.unisamp_seed, bm->UserFlags.num_samples,
-      bm->UserFlags.samples_generated);
+      newS = new ApxMC(bm->UserFlags.unisamp_seed);
 #else
-      std::cerr << "UniSamp support was not enabled at configure time."
+      std::cerr << "ApproxMC support was not enabled at configure time."
                 << std::endl;
       exit(-1);
 #endif
diff --git a/lib/Sat/ApxMC.cpp b/lib/Sat/ApxMC.cpp
@@ -0,0 +1,227 @@
+/********************************************************************
+ * AUTHORS: Arijit Shaw
+ *
+ * BEGIN DATE: November, 2023
+ *
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
+********************************************************************/
+
+#include "approxmc/approxmc.h"
+#include "stp/Sat/ApxMC.h"
+#include <algorithm>
+#include <unordered_set>
+using std::vector;
+
+using namespace CMSat;
+using namespace ApxMC; // namespace in appmc library
+
+namespace stp
+{
+
+
+void ApxMC::enableRefinement(const bool enable)
+{
+  // might break if we simplify with refinement enabled..
+  //   if (enable)
+  //   {
+  //     s->set_no_simplify_at_startup();
+  //   }
+}
+
+ApxMC::ApxMC(uint64_t unisamp_seed)
+{
+
+  a = new ApproxMC::AppMC;
+  arjun = new ArjunNS::Arjun;
+  seed = unisamp_seed;
+
+  a->set_verbosity(0);
+  arjun->set_verbosity(0);
+  // s->log_to_file("stp.cnf");
+  //s->set_num_threads(num_threads);
+  //s->set_default_polarity(false);
+  //s->set_allow_otf_gauss();
+  temp_cl = (void*)new vector<CMSat::Lit>;
+}
+
+ApxMC::~ApxMC()
+{
+  delete a;
+  vector<CMSat::Lit>* real_temp_cl = (vector<CMSat::Lit>*)temp_cl;
+  delete real_temp_cl;
+}
+
+void ApxMC::setMaxConflicts(int64_t _max_confl)
+{
+  max_confl = _max_confl;
+}
+
+void ApxMC::setMaxTime(int64_t _max_time)
+{
+  max_time = _max_time;
+}
+
+bool ApxMC::addClause(const vec_literals& ps) // Add a clause to the solver.
+{
+  // Cryptominisat uses a slightly different vec class.
+  // Cryptominisat uses a slightly different Lit class too.
+
+  vector<CMSat::Lit>& real_temp_cl = *(vector<CMSat::Lit>*)temp_cl;
+  real_temp_cl.clear();
+  for (int i = 0; i < ps.size(); i++)
+  {
+    real_temp_cl.push_back(CMSat::Lit(var(ps[i]), sign(ps[i])));
+  }
+  arjun->add_clause(real_temp_cl);
+  return a->add_clause(real_temp_cl);
+}
+
+bool ApxMC::okay() const // FALSE means solver is in a conflicting state
+{
+  //return a->okay();
+  return true; //TODO AS: implement well
+}
+
+bool ApxMC::solve(bool& timeout_expired) // Search without assumptions.
+{
+
+  /*
+   * STP uses -1 for a value of "no timeout" -- this means that we only set the
+   * timeout _in the SAT solver_ if the value is >= 0. This avoids us
+   * accidentally setting a large limit (or one in the past).
+   */
+
+  // CMSat::lbool ret = s->solve(); // TODO AS
+  std::cout << "c [stp->appmc] ApxMC solving instance with " << a->nVars()
+            << " variables." << std::endl;
+
+  vector<uint32_t> sampling_vars, sampling_vars_orig;
+  for (uint32_t i = 0; i < a->nVars(); i++)
+    sampling_vars.push_back(i);
+
+  arjun->set_seed(5);
+
+  sampling_vars_orig = sampling_vars;
+  arjun->set_sampl_vars(sampling_vars_orig);
+  sampling_vars = arjun->run_backwards();
+  std::cout << "c [appmc->arjun] sampling var size [from arjun] "
+            << sampling_vars.size() << "\n";
+
+  delete arjun;
+
+  //TODO AS: this is debugging as Arjun is not performing correctly
+  //sampling_vars = sampling_vars_orig;
+
+  a->set_sampl_vars(sampling_vars);
+
+  auto sol_count = a->count();
+
+  std::cout << "c [stp->appmc] Number of Solutions " << sol_count.cellSolCount
+            << "*2**" << sol_count.hashCount - 1  << std::endl;
+  exit(0);
+  return true;
+}
+
+uint8_t ApxMC::modelValue(uint32_t x) const
+{
+  //   if (appmc_models[0].size() < sampling_vars.size())
+  //     std::cout << "c [stp->appmc] ERROR! found model size is not large enough\n";
+  return true;
+}
+
+uint32_t ApxMC::newVar()
+{
+  a->new_var();
+  arjun->new_var();
+  return a->nVars() - 1;
+}
+
+void ApxMC::setVerbosity(int v)
+{
+  a->set_verbosity(0);
+  arjun->set_verbosity(0);
+}
+
+unsigned long ApxMC::nVars() const
+{
+  return a->nVars();
+}
+
+void ApxMC::printStats() const
+{
+  // s->printStats();
+}
+
+void ApxMC::solveAndDump()
+{
+  bool t;
+  solve(t);
+  //s->open_file_and_dump_irred_clauses("clauses.txt");
+}
+
+// Count how many literals/bits get fixed subject to the assumptions..
+uint32_t ApxMC::getFixedCountWithAssumptions(
+    const stp::SATSolver::vec_literals& assumps,
+    const std::unordered_set<unsigned>& literals)
+{
+  /* TODO AS skip all?
+  const uint64_t conf = 0; // TODO AS: s->get_sum_conflicts();
+  assert(conf == 0);
+
+
+  // const CMSat::lbool r = s->simplify();  TODO AS
+
+
+  // Add the assumptions are clauses.
+  vector<CMSat::Lit>& real_temp_cl = *(vector<CMSat::Lit>*)temp_cl;
+  for (int i = 0; i < assumps.size(); i++)
+  {
+    real_temp_cl.clear();
+    real_temp_cl.push_back(CMSat::Lit(var(assumps[i]), sign(assumps[i])));
+    a->add_clause(real_temp_cl);
+  }
+
+
+  //std::cerr << assumps.size() << " assumptions" << std::endl;
+
+  std::vector<CMSat::Lit> zero = s->get_zero_assigned_lits();
+  for (CMSat::Lit l : zero)
+  {
+      if (literals.find(l.var()) != literals.end())
+        assigned++;
+  }
+
+
+
+  //std::cerr << assigned << " assignments at end" <<std::endl;
+
+  // The assumptions are each single literals (corresponding to bits) that are true/false.
+  // so in the result they should be all be set
+  assert(assumps.size() >= 0);
+  assert(assigned >= static_cast<uint32_t>(assumps.size()));
+  assert(s->get_sum_conflicts() == conf ); // no searching, so no conflicts.
+  assert(CMSat::l_False != r); // always satisfiable.
+  */
+
+  uint32_t assigned = 0;
+
+  return assigned;
+}
+
+} //end namespace stp
diff --git a/lib/Sat/CMakeLists.txt b/lib/Sat/CMakeLists.txt
@@ -35,6 +35,7 @@ if (USE_UNIGEN)
     include_directories(${CMSGEN_INCLUDE_DIRS})
     include_directories(${ARJUN_INCLUDE_DIRS})
     message(STATUS "Including ApproxMC, CMSGen and UniGen")
+    set(sat_lib_to_add ${sat_lib_to_add} ApxMC.cpp)
     set(sat_lib_to_add ${sat_lib_to_add} UniSamp.cpp)
     set(sat_lib_to_add ${sat_lib_to_add} CMSGen.cpp)
 endif()
