Making progress

Author: msoos

src/autarky.cpp

@@ -29,6 +29,7 @@
 #include "constants.h"
 
 using namespace ArjunNS;
+using namespace ArjunInt;
 using namespace CMSat;
 using std::vector;
 using std::fixed;

src/autarky.h

@@ -34,11 +34,12 @@
 #include "src/formula.h"
 
 using namespace CMSat;
-using namespace ArjunInt;
 using namespace ArjunNS;
 using std::vector;
 using std::set;
 
+namespace ArjunInt {
+
 class Autarky {
 public:
     Autarky(const Config& _conf);
@@ -59,3 +60,4 @@ class Autarky {
     const Config conf;
 
 };
+}

src/formula.h

@@ -41,7 +41,7 @@ using CMSat::lit_Error;
 using CMSat::SATSolver;
 using std::map;
 
-namespace ArjunNS {
+namespace ArjunInt {
 
 struct CL {
     constexpr CL(const vector<Lit>& _lits) : lits(_lits) {}
@@ -63,12 +63,12 @@ class FHolder {
         // solver_train
         vector<CL> clauses;
         Lit out = lit_Error;
-        aig_ptr aig = nullptr;
+        ArjunNS::aig_ptr aig = nullptr;
     };
 
     set<uint32_t> get_dependent_vars(const Formula& f, uint32_t v) const {
         set<uint32_t> ret;
-        AIG::get_dependent_vars(f.aig, ret, v);
+        ArjunNS::AIG::get_dependent_vars(f.aig, ret, v);
         return ret;
     }
 
@@ -83,14 +83,14 @@ class FHolder {
         Formula ret;
         ret = compose_ite(fleft, fright, branch.out, helpers);
         ret.clauses.insert(ret.clauses.end(), branch.clauses.begin(), branch.clauses.end());
-        ret.aig = AIG::new_ite(fleft.aig, fright.aig, branch.aig);
+        ret.aig = ArjunNS::AIG::new_ite(fleft.aig, fright.aig, branch.aig);
         return ret;
     }
 
     Formula neg(const Formula& f) {
         Formula ret = f;
         ret.out = ~f.out;
-        ret.aig = AIG::new_not(f.aig);
+        ret.aig = ArjunNS::AIG::new_not(f.aig);
         return ret;
     }
 
@@ -114,7 +114,7 @@ class FHolder {
 
         assert(fleft.aig != nullptr);
         assert(fright.aig != nullptr);
-        ret.aig = AIG::new_or(fleft.aig, fright.aig);
+        ret.aig = ArjunNS::AIG::new_or(fleft.aig, fright.aig);
         return ret;
     }
 
@@ -145,7 +145,7 @@ class FHolder {
         ret.clauses.push_back(CL({b, fresh, ~r}));
         ret.clauses.push_back(CL({b, ~fresh, r}));
         ret.out = Lit(fresh_v, false);
-        ret.aig = AIG::new_ite(fleft.aig, fright.aig, branch);
+        ret.aig = ArjunNS::AIG::new_ite(fleft.aig, fright.aig, branch);
         return ret;
     }
 
@@ -155,15 +155,12 @@ class FHolder {
     }
 
 private:
-    AIGManager aig_mng;
+    ArjunNS::AIGManager aig_mng;
     T* solver = nullptr;
     Lit my_true_lit = lit_Error;
 };
 
-}
-
-
-inline std::ostream& operator<<(std::ostream& os, const ArjunNS::FHolder<ArjunInt::MetaSolver2>::Formula& f) {
+inline std::ostream& operator<<(std::ostream& os, const FHolder<ArjunInt::MetaSolver2>::Formula& f) {
     os << " === Formula out: " << f.out << " === " << endl;
     for (const auto& cl : f.clauses) {
         for (const auto& l : cl.lits) os << std::setw(6) << l;
@@ -173,3 +170,5 @@ inline std::ostream& operator<<(std::ostream& os, const ArjunNS::FHolder<ArjunIn
     os << " === End Formula === ";
     return os;
 }
+
+}

src/interpolant.cpp

@@ -32,6 +32,7 @@ extern "C" {
 
 using namespace CMSat;
 using namespace CaDiCaL;
+using namespace ArjunInt;
 
 void MyTracer::add_derived_clause(uint64_t id, bool /*red*/, const std::vector<int> & clause,
                                const std::vector<uint64_t> & oantec) {

src/interpolant.h

@@ -42,6 +42,8 @@ using std::vector;
 using std::map;
 using namespace ArjunNS;
 
+namespace ArjunInt {
+
 struct MyTracer : public CaDiCaL::Tracer {
     MyTracer(const uint32_t _orig_num_vars, const set<uint32_t>& input_vars,
             const ArjunInt::Config& _conf, map<Lit, aig_ptr>& _lit_to_aig, const AIGManager& _aig_mng) :
@@ -139,4 +141,4 @@ class Interpolant {
     vector<uint32_t> var_to_indic; //maps an ORIG VAR to an INDICATOR VAR
     vector<aig_ptr> defs; //definition of variables in terms of AIG. ORIGINAL number space
 };
-
+}

src/manthan.cpp

@@ -3,8 +3,7 @@
 
  Copyright (c) 2020, Mate Soos and Kuldeep S. Meel. All rights reserved.
 
- Permission is hereby granted, free of charge, to any person obtaining a copy
- of this software and associated documentation files (the "Software"), to deal
+ 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
@@ -73,13 +72,6 @@ using namespace CMSat;
 // no repair, learning/mbve does it: benchmarks-qdimacs/rankfunc57_unsigned_64.qdimacs.cnf
 // interesting, does not finish, but fast: benchmarks-qdimacs/query48_exquery_1344n.qdimacs.cnf
 
-vector<int> lits_to_ints(const vector<Lit>& lits) {
-    vector<int> ret;
-    ret.reserve(lits.size());
-    for(const auto& l: lits) ret.push_back(lit_to_pl(l));
-    return ret;
-}
-
 template<typename S>
 void Manthan::inject_cnf(S& s) const {
     s.new_vars(cnf.nVars());

src/manthan.h

@@ -51,6 +51,7 @@ using sample = vector<lbool>;
 using namespace ArjunInt;
 using namespace ArjunNS;
 
+namespace ArjunInt {
 class ManthanLearn;
 
 class Manthan {
@@ -169,6 +170,12 @@ class Manthan {
             assert(val != l_Undef);
             return val == l_True;
         }
+        vector<int> lits_to_ints(const vector<Lit>& lits) {
+            vector<int> ret;
+            ret.reserve(lits.size());
+            for(const auto& l: lits) ret.push_back(lit_to_pl(l));
+            return ret;
+        }
 
         // debug
         bool verify_final_cnf(const SimplifiedCNF& fcnf) const;
@@ -200,3 +207,4 @@ class Manthan {
         SimplifiedCNF cnf;
         AIGManager aig_mng;
 };
+}

src/manthan_learn.cpp

@@ -31,6 +31,7 @@
 using std::setprecision;
 using std::fixed;
 using std::setw;
+using namespace ArjunInt;
 
 void ManthanLearn::full_train() {
     // Sampling

src/manthan_learn.h

@@ -39,6 +39,8 @@ using sample = vector<lbool>;
 //#define MLPACK_PRINT_WARN
 #include <mlpack.hpp>
 
+namespace ArjunInt {
+
 class ManthanLearn {
 public:
     ManthanLearn(Manthan& _manthan, const Config& _conf, const ArjunNS::Arjun::ManthanConf& _mconf) :
@@ -58,3 +60,4 @@ class ManthanLearn {
     const Config& conf;
     const ArjunNS::Arjun::ManthanConf& mconf;
 };
+}

src/metasolver.h

@@ -48,10 +48,12 @@ class MetaSolver {
         if (solver_type == SolverType::cms) {
             cms = std::make_unique<CMSat::SATSolver>();
             cms->set_prefix("c o ");
-        } else {
+        } else if (solver_type == SolverType::cadical) {
             cadical = std::make_unique<CaDiCaL::Solver>();
             cadical_nvars = 0;
             cadical->prefix("c o ");
+        } else {
+            throw std::invalid_argument("Unsupported solver type");
         }
     }