Field now

Author: msoos

README.md

@@ -179,7 +179,6 @@ The system can be used as a library:
 ```c++
 #include <approxmc/approxmc.h>
 #include <vector>
-#include <complex>
 #include <cassert>
 
 using std::vector;

src/appmcconfig.h

@@ -28,17 +28,18 @@
 
 #pragma once
 
+#include <memory>
 #include <vector>
 #include <cstdint>
 #include <string>
 #include <gmpxx.h>
-#include <complex>
-
-using std::complex;
+#include <cryptominisat5/solvertypesmini.h>
 
 namespace AppMCInt {
 
-struct Config {
+class Config {
+public:
+    Config(const std::unique_ptr<CMSat::FieldGen>& _fg) : multiplier_weight(_fg->one()) {}
     uint32_t start_iter = 0;
     double epsilon = 0.80; //Tolerance.  CAV-2020 paper default
     double delta = 0.2;    //Confidence. CAV-2020 paper default
@@ -56,7 +57,7 @@ struct Config {
 
     std::vector<uint32_t> sampl_vars;
     bool sampl_vars_set = false;
-    complex<mpq_class> multiplier_weight = complex<mpq_class>(1,0);
+    std::unique_ptr<CMSat::Field> multiplier_weight = nullptr;
 };
 
 }

src/approxmc.cpp

@@ -30,11 +30,12 @@
 #include "counter.h"
 #include "appmc_constants.h"
 #include "appmcconfig.h"
+#include "cryptominisat5/solvertypesmini.h"
 #include <iostream>
+#include <memory>
 
 using std::cout;
 using std::endl;
-using std::complex;
 using namespace AppMCInt;
 
 #if defined _WIN32
@@ -46,7 +47,9 @@ using namespace AppMCInt;
 
 namespace ApproxMC {
     struct AppMCPrivateData {
-        AppMCPrivateData(): counter(conf) {}
+        AppMCPrivateData(const std::unique_ptr<CMSat::FieldGen>& fg):
+            conf(fg),
+            counter(conf, fg) {}
         Config conf;
         Counter counter;
         bool sampl_vars_declared = false;
@@ -55,9 +58,9 @@ namespace ApproxMC {
 
 using namespace ApproxMC;
 
-DLL_PUBLIC AppMC::AppMC()
+DLL_PUBLIC AppMC::AppMC(const std::unique_ptr<CMSat::FieldGen>& _fg)
 {
-    data = new AppMCPrivateData;
+    data = new AppMCPrivateData(_fg);
     data->counter.solver = new SATSolver();
     data->counter.solver->set_up_for_scalmc();
     data->counter.solver->set_allow_otf_gauss();
@@ -309,11 +312,11 @@ DLL_PUBLIC bool AppMC::get_sampl_vars_set() const {
     return data->conf.sampl_vars_set;
 }
 
- DLL_PUBLIC void AppMC::set_multiplier_weight(const complex<mpq_class>& weight) {
-     data->conf.multiplier_weight = weight;
+ DLL_PUBLIC void AppMC::set_multiplier_weight(const std::unique_ptr<CMSat::Field>& weight) {
+     data->conf.multiplier_weight = weight->dup();
  }
 
- DLL_PUBLIC const complex<mpq_class>& AppMC::get_multiplier_weight() const {
+ DLL_PUBLIC const std::unique_ptr<CMSat::Field>& AppMC::get_multiplier_weight() const {
      return data->conf.multiplier_weight;
  }
 
@@ -327,7 +330,7 @@ DLL_PUBLIC void AppMC::set_weighted(const bool weighted) {
 DLL_PUBLIC void AppMC::set_projected(const bool) {
 }
 
-DLL_PUBLIC void AppMC::set_lit_weight(const Lit&, const complex<mpq_class>&) {
+DLL_PUBLIC void AppMC::set_lit_weight(const Lit&, const std::unique_ptr<Field>&) {
     cout << "ERROR: Weighted ApproxMC is not supported" << endl;
     exit(-1);
 }

src/approxmc.h

@@ -30,7 +30,9 @@
 #ifndef APPROXMC_H__
 #define APPROXMC_H__
 
+#include <algorithm>
 #include <cstdint>
+#include <memory>
 #include <string>
 #include <vector>
 #ifdef CMS_LOCAL_BUILD
@@ -65,7 +67,7 @@ class AppMC
 #endif
 {
 public:
-    AppMC();
+    AppMC(const std::unique_ptr<CMSat::FieldGen>& _fg);
     ~AppMC();
     ApproxMC::SolCount count();
     bool find_one_solution();
@@ -76,11 +78,11 @@ class AppMC
     bool get_sampl_vars_set() const;
     bool get_opt_sampl_vars_set() const { return false; }
     const std::vector<uint32_t>& get_sampl_vars() const;
-    void set_multiplier_weight(const std::complex<mpq_class>& weight);
-    const std::complex<mpq_class>& get_multiplier_weight() const;
+    void set_multiplier_weight(const std::unique_ptr<CMSat::Field>& weight);
+    const std::unique_ptr<CMSat::Field>& get_multiplier_weight() const;
     void set_weighted(const bool weighted);
     void set_projected(const bool projected);
-    void set_lit_weight(const CMSat::Lit& lit, const std::complex<mpq_class>& weight);
+    void set_lit_weight(const CMSat::Lit& lit, const std::unique_ptr<CMSat::Field>& weight);
 
     // Adding constraints
     void new_var();

src/counter.cpp

@@ -41,7 +41,6 @@
 #include <list>
 #include <array>
 #include <cmath>
-#include <complex>
 
 #include "counter.h"
 #include "appmc_constants.h"

src/counter.h

@@ -28,6 +28,7 @@
 
 #include "appmcconfig.h"
 #include <fstream>
+#include <memory>
 #include <random>
 #include <map>
 #include <utility>
@@ -92,7 +93,7 @@ struct SparseData {
 
 class Counter {
 public:
-    Counter(Config& _conf) : conf(_conf) {}
+    Counter(Config& _conf, const std::unique_ptr<FieldGen>& _fg) : fg(_fg->dup()), conf(_conf) {}
     ApproxMC::SolCount solve();
     string gen_rnd_bits(const uint32_t size,
                         const uint32_t numhashes, SparseData& sparse_data);
@@ -109,6 +110,7 @@ class Counter {
     bool solver_add_xor_clause(const vector<Lit>& lits, const bool rhs);
 
 private:
+    std::unique_ptr<FieldGen> fg;
     Config& conf;
     ApproxMC::SolCount count();
     void add_appmc_options();

src/main.cpp

@@ -26,13 +26,14 @@
  THE SOFTWARE.
  */
 
+#include "cryptominisat5/solvertypesmini.h"
+#include <memory>
 #include <string>
 #include <vector>
 #if defined(__GNUC__) && defined(__linux__)
 #include <cfenv>
 #endif
 #include <cstdint>
-#include <complex>
 #include <set>
 #include <gmp.h>
 
@@ -50,7 +51,6 @@ using std::endl;
 using std::set;
 using std::string;
 using std::vector;
-using std::complex;
 ApproxMC::AppMC* appmc = nullptr;
 argparse::ArgumentParser program = argparse::ArgumentParser("approxmc");
 
@@ -69,6 +69,7 @@ uint32_t sparse = 0;
 int dump_intermediary_cnf = 0;
 int arjun_gates = 0;
 bool debug = false;
+std::unique_ptr<CMSat::FieldGen> fg;
 
 //Arjun
 ArjunNS::SimpConf simp_conf;
@@ -99,7 +100,7 @@ void print_version() {
 
 void add_appmc_options()
 {
-    ApproxMC::AppMC tmp;
+    ApproxMC::AppMC tmp(fg);
     epsilon = tmp.get_epsilon();
     delta = tmp.get_delta();
     simplify = tmp.get_simplify();
@@ -217,18 +218,18 @@ template<class T> void read_stdin(T* myreader) {
     #endif
 }
 
-void print_num_solutions(uint32_t cell_sol_cnt, uint32_t hash_count, const complex<mpq_class>& mult)
-{
-    assert(mult.imag() == 0);
+void print_num_solutions(uint32_t cell_sol_cnt, uint32_t hash_count, const std::unique_ptr<Field>& mult) {
+    const CMSat::Field* ptr = mult.get();
+    const CMSat::FMpz* od = dynamic_cast<const CMSat::FMpz*>(ptr);
     cout << "c [appmc] Number of solutions is: "
-    << cell_sol_cnt << "*2**" << hash_count << "*" << mult << endl;
+    << cell_sol_cnt << "*2**" << hash_count << "*" << od->val << endl;
     if (cell_sol_cnt == 0) cout << "s UNSATISFIABLE" << endl;
     else cout << "s SATISFIABLE" << endl;
 
     mpz_class num_sols(2);
     mpz_pow_ui(num_sols.get_mpz_t(), num_sols.get_mpz_t(), hash_count);
     num_sols *= cell_sol_cnt;
-    mpq_class final = mult.real() * num_sols;
+    mpq_class final = od->val * num_sols;
 
     cout << "s mc " << final << endl;
 }
@@ -267,10 +268,10 @@ void set_approxmc_options()
 template<class T> void parse_file(const std::string& filename, T* reader) {
   #ifndef USE_ZLIB
   FILE * in = fopen(filename.c_str(), "rb");
-  DimacsParser<StreamBuffer<FILE*, CMSat::FN>, T> parser(reader, nullptr, 0);
+  DimacsParser<StreamBuffer<FILE*, CMSat::FN>, T> parser(reader, nullptr, 0, fg);
   #else
   gzFile in = gzopen(filename.c_str(), "rb");
-  DimacsParser<StreamBuffer<gzFile, CMSat::GZ>, T> parser(reader, nullptr, 0);
+  DimacsParser<StreamBuffer<gzFile, CMSat::GZ>, T> parser(reader, nullptr, 0, fg);
   #endif
   if (in == nullptr) {
       std::cout << "ERROR! Could not open file '" << filename
@@ -287,7 +288,7 @@ template<class T> void parse_file(const std::string& filename, T* reader) {
   if (!reader->get_sampl_vars_set()) {
     vector<uint32_t> tmp;
     for(uint32_t i = 0; i < reader->nVars(); i++) tmp.push_back(i);
-    reader->set_sampl_vars(tmp); // will automatically set the opt_sampl_vars
+    reader->set_sampl_vars(tmp);
   } else {
     // Check if CNF has all vars as indep. Then its's all_indep
     set<uint32_t> tmp;
@@ -320,7 +321,8 @@ int main(int argc, char** argv)
         if (i+1 < argc) command_line += " ";
     }
 
-    appmc = new ApproxMC::AppMC;
+    fg = std::make_unique<CMSat::FGenMpz>();
+    appmc = new ApproxMC::AppMC(fg);
     simp_conf.appmc = true;
     simp_conf.oracle_sparsify = false;
     simp_conf.iter1 = 2;
@@ -334,9 +336,9 @@ int main(int argc, char** argv)
     }
     set_approxmc_options();
 
-    ArjunNS::SimplifiedCNF cnf;
-    auto files = program.get<std::vector<std::string>>("inputfile");
-    string fname = files[0];
+    ArjunNS::SimplifiedCNF cnf(fg);
+    const auto& files = program.get<std::vector<std::string>>("inputfile");
+    const string fname(files[0]);
     if (do_arjun) {
         parse_file(fname, &cnf);
         const auto orig_sampl_vars = cnf.sampl_vars;

tests/simpletest.cpp

@@ -23,10 +23,11 @@ THE SOFTWARE.
 #include "gtest/gtest.h"
 
 #include "approxmc.h"
+#include "cryptominisat5/solvertypesmini.h"
 #include "test_helper.h"
+#include <memory>
 #include <string>
 #include <vector>
-#include <complex>
 using std::string;
 using std::vector;
 
@@ -37,7 +38,8 @@ using std::vector;
 
 TEST(normal_interface, start)
 {
-    AppMC s;
+    std::unique_ptr<FieldGen> fg = std::make_unique<CMSat::FGenMpz>();
+    AppMC s(fg);
     s.set_sampl_vars({});
     SolCount c = s.count();
     EXPECT_EQ(1U, c.cellSolCount);
@@ -46,7 +48,8 @@ TEST(normal_interface, start)
 
 TEST(normal_interface, example1)
 {
-    AppMC s;
+    std::unique_ptr<FieldGen> fg = std::make_unique<CMSat::FGenMpz>();
+    AppMC s(fg);
     s.new_vars(2);
     s.add_clause(str_to_cl("-1, 2"));
     s.set_sampl_vars({0, 1});
@@ -57,7 +60,8 @@ TEST(normal_interface, example1)
 
 TEST(normal_interface, example2)
 {
-    AppMC s;
+    std::unique_ptr<FieldGen> fg = std::make_unique<CMSat::FGenMpz>();
+    AppMC s(fg);
     s.new_vars(10);
     vector<uint32_t> sampl;
     for(uint32_t i = 0; i < 10; i++) sampl.push_back(i);
@@ -70,7 +74,8 @@ TEST(normal_interface, example2)
 
 TEST(normal_interface, example3)
 {
-    AppMC s;
+    std::unique_ptr<FieldGen> fg = std::make_unique<CMSat::FGenMpz>();
+    AppMC s(fg);
     s.new_vars(10);
     vector<uint32_t> sampl;
     for(uint32_t i = 0; i < 10; i++) sampl.push_back(i);
@@ -84,7 +89,8 @@ TEST(normal_interface, example3)
 
 TEST(normal_interface, example4)
 {
-    AppMC s;
+    std::unique_ptr<FieldGen> fg = std::make_unique<CMSat::FGenMpz>();
+    AppMC s(fg);
     s.new_vars(10);
     vector<uint32_t> sampl;
     for(uint32_t i = 0; i < 10; i++) sampl.push_back(i);