Remove using namespace Lib from hpp files.

CASC/PortfolioMode.hpp

@@ -30,7 +30,6 @@
 namespace CASC
 {
 
-using namespace Lib;
 using namespace Shell;
 
 class PortfolioMode {
@@ -54,7 +53,7 @@ class PortfolioMode {
   [[noreturn]] void runSlice(Options& strategyOpt);
 
 #if VDEBUG
-  DHSet<pid_t> childIds;
+  Lib::DHSet<pid_t> childIds;
 #endif
   unsigned _numWorkers;
   // file that will contain a proof
@@ -66,7 +65,7 @@ class PortfolioMode {
    * Note that in the current process this child object is the only one that
    * will be using the problem object.
    */
-  ScopedPtr<Problem> _prb;
+  Lib::ScopedPtr<Problem> _prb;
   float _slowness;
 };
 

DP/DecisionProcedure.hpp

@@ -19,7 +19,6 @@
 
 namespace DP {
 
-using namespace Lib;
 using namespace Kernel;
 
 /**

DP/ShortConflictMetaDP.cpp

@@ -18,6 +18,7 @@ namespace DP
 {
 
 using namespace std;
+using namespace Lib;
 
 /**
  * Computes number of literals in core not implied at the zero level

DP/ShortConflictMetaDP.hpp

@@ -28,7 +28,6 @@
 
 namespace DP {
 
-using namespace Lib;
 using namespace Kernel;
 using namespace SAT;
 
@@ -70,9 +69,9 @@ class ShortConflictMetaDP : public DecisionProcedure {
   unsigned getCoreSize(const LiteralStack& core);
 
 
-  Stack<LiteralStack> _unsatCores;
+  Lib::Stack<LiteralStack> _unsatCores;
 
-  ScopedPtr<DecisionProcedure> _inner;
+  Lib::ScopedPtr<DecisionProcedure> _inner;
   SAT2FO& _sat2fo;
   SATSolver& _solver;
 };

DP/SimpleCongruenceClosure.cpp

@@ -32,6 +32,7 @@ namespace DP
 {
 
 using namespace std;
+using namespace Lib;
 
 const unsigned SimpleCongruenceClosure::NO_SIG_SYMBOL = 0xFFFFFFFF;
 

DP/SimpleCongruenceClosure.hpp

@@ -29,7 +29,6 @@
 
 namespace DP {
 
-using namespace Lib;
 using namespace Kernel;
 
 /**
@@ -163,7 +162,7 @@ class SimpleCongruenceClosure : public DecisionProcedure
   void propagate();
 
   unsigned getProofDepth(unsigned c);
-  void collectUnifyingPath(unsigned c1, unsigned c2, Stack<unsigned>& path);
+  void collectUnifyingPath(unsigned c1, unsigned c2, Lib::Stack<unsigned>& path);
 
   static const unsigned NO_SIG_SYMBOL;
   struct ConstInfo
@@ -202,14 +201,14 @@ class SimpleCongruenceClosure : public DecisionProcedure
 
     /** If reprConst==0, contains other constants whose representative
      * this constant is */
-    Stack<unsigned> classList;
+    Lib::Stack<unsigned> classList;
     /**
      * If reprConst==0, contains list of pair names in whose pairs this
      * constant appears as a representative of one of the arguments.
      * Irregardless of the value of reprConst, also contains representatives
      * of all pairs that have this very constant as one of arguments.
      */
-    Stack<unsigned> useList;
+    Lib::Stack<unsigned> useList;
 
     // needed for getModel:    
     /**
@@ -219,7 +218,7 @@ class SimpleCongruenceClosure : public DecisionProcedure
     /**
      * Meaningful for representatives. A list of edges leaving the class "upwards".
      */
-    Stack<unsigned> upEdges;
+    Lib::Stack<unsigned> upEdges;
     /**
      * Meaningful for namedPairs. 
      * 
@@ -239,7 +238,7 @@ class SimpleCongruenceClosure : public DecisionProcedure
   };
 
   struct ConstOrderingComparator;  
-  typedef DHMap<unsigned,TermList> NFMap;
+  typedef Lib::DHMap<unsigned,TermList> NFMap;
   void computeConstsNormalForm(unsigned c, NFMap& normalForms);
 
 #if VDEBUG
@@ -253,7 +252,7 @@ class SimpleCongruenceClosure : public DecisionProcedure
    * of constants in special cases, such as to indicate that there is
    * no constant.
    */
-  DArray<ConstInfo> _cInfos;
+  Lib::DArray<ConstInfo> _cInfos;
 
   /** Positive literals are made equivalent to this constant */
   unsigned _posLitConst;
@@ -263,31 +262,31 @@ class SimpleCongruenceClosure : public DecisionProcedure
   /**
    * Map from signature symbols to the local constant numbers.
    */
-  DHMap<std::pair<unsigned,SignatureKind>,unsigned> _sigConsts;
+  Lib::DHMap<std::pair<unsigned,SignatureKind>,unsigned> _sigConsts;
 
-  typedef DHMap<CPair,unsigned> PairMap;
+  typedef Lib::DHMap<CPair,unsigned> PairMap;
   /** Names of constant pairs (modulo the congruence!)*/
   PairMap _pairNames;
 
   /** Constants corresponding to terms */
-  DHMap<TermList,unsigned> _termNames;
+  Lib::DHMap<TermList,unsigned> _termNames;
   /** Constants corresponding to literals */
-  DHMap<Literal*,unsigned> _litNames;
+  Lib::DHMap<Literal*,unsigned> _litNames;
 
   /**
    * Equality that caused unsatisfiability; if CEq::isInvalid(), there isn't such.
    */
-  Stack<CEq> _unsatEqs;
-  Deque<CEq> _pendingEqualities;
-  Stack<CEq> _negEqualities;
+  Lib::Stack<CEq> _unsatEqs;
+  Lib::Deque<CEq> _pendingEqualities;
+  Lib::Stack<CEq> _negEqualities;
 
   struct DistinctEntry
   {
     DistinctEntry(Literal* l) : _lit(l) {}
     Literal* _lit;
-    Stack<unsigned> _consts;
+    Lib::Stack<unsigned> _consts;
   };
-  typedef Stack<DistinctEntry> DistinctStack;
+  typedef Lib::Stack<DistinctEntry> DistinctStack;
   DistinctStack _distinctConstraints;
   /** Negated distinct constraints, these can lead to an UNKNOWN satisfiability result 
    * 

Debug/RuntimeStatistics.cpp

@@ -25,6 +25,7 @@ namespace Debug
 {
 
 using namespace std;
+using namespace Lib;
 
 void RSMultiCounter::print(ostream& out)
 {

Debug/RuntimeStatistics.hpp

@@ -87,7 +87,6 @@ square's last digit:
 
 namespace Debug {
 
-using namespace Lib;
 
 class RSObject
 {
@@ -127,21 +126,21 @@ class RSMultiCounter
   void print(std::ostream& out);
   void inc(size_t index) { _counters[index]++; }
 private:
-  ZIArray<size_t> _counters;
+  Lib::ZIArray<size_t> _counters;
 };
 
 class RSMultiStatistic
 : public RSObject
 {
-  typedef List<int> ValList;
+  typedef Lib::List<int> ValList;
 public:
   RSMultiStatistic(const char* name) : RSObject(name) {}
   ~RSMultiStatistic();
 
   void print(std::ostream& out);
   void addRecord(size_t index, int value) { ValList::push(value, _values[index]); }
 private:
-  ZIArray<ValList* > _values;
+  Lib::ZIArray<ValList* > _values;
 };
 
 class RuntimeStatistics
@@ -151,8 +150,9 @@ class RuntimeStatistics
 
   struct RSObjComparator
   {
-    static Comparison compare(const char* name, RSObject* o2)
+    static Lib::Comparison compare(const char* name, RSObject* o2)
     {
+      using namespace Lib;
       int res=strcmp(name, o2->name());
       return (res>0) ? GREATER : ((res==0) ? EQUAL : LESS);
     }
@@ -175,7 +175,7 @@ class RuntimeStatistics
   RuntimeStatistics();
   ~RuntimeStatistics();
 
-  typedef SkipList<RSObject*,RSObjComparator> ObjSkipList;
+  typedef Lib::SkipList<RSObject*,RSObjComparator> ObjSkipList;
   ObjSkipList _objs;
 };
 

Debug/Tracer.cpp

@@ -54,7 +54,7 @@ void Debug::Tracer::printStack(std::ostream& str) {
     str << ' ' << call_stack[sz - (i + 1)];
   str << std::endl;
 
-  if (env.options->traceback()) {
+  if (Lib::env.options->traceback()) {
 // UNIX-like systems, including BSD and Linux but not MacOS
 #if defined(__unix__)
   str << "invoking addr2line(1) ..." << std::endl;

FMB/ClauseFlattening.cpp

@@ -29,6 +29,7 @@
 namespace FMB{
 
 using namespace std;
+using namespace Lib;
 
 bool ClauseFlattening::isShallow(Literal* lit)
 {

FMB/CliqueFinder.hpp

@@ -21,23 +21,23 @@ namespace FMB {
 
   class CliqueFinder {
   public:
-    static unsigned findMaxCliqueSize(DHMap<unsigned,DHSet<unsigned>*>* Ngraph)
+    static unsigned findMaxCliqueSize(Lib::DHMap<unsigned,Lib::DHSet<unsigned>*>* Ngraph)
     {
       //std::cout << "findMaxCliqueSize with " << Ngraph->size() << std::endl;
 
       // at least stores the number of nodes with at least index neighbours
-      DArray<Stack<unsigned>> atleast;
+      Lib::DArray<Lib::Stack<unsigned>> atleast;
       atleast.ensure(Ngraph->size()+1); // the +1 is to protect against a self-loop sneaking in
 
-      DHMap<unsigned,DHSet<unsigned>*>::Iterator miter(*Ngraph);
+      Lib::DHMap<unsigned,Lib::DHSet<unsigned>*>::Iterator miter(*Ngraph);
       while(miter.hasNext()){
         unsigned c;
-        DHSet<unsigned>* nbs;
+        Lib::DHSet<unsigned>* nbs;
         miter.next(c,nbs);
         unsigned size = nbs->size();
         //std::cout << ">> " << c << ": " << size << std::endl;
 
-        //DHSet<unsigned>::Iterator dit(*nbs);
+        //Lib::DHSet<unsigned>::Iterator dit(*nbs);
         //while(dit.hasNext()){ std::cout << dit.next() << std::endl; }
 
         for(;size>0;size--){
@@ -61,13 +61,13 @@ namespace FMB {
         else if (atleast[i].size() > i+1){
           //std::cout << "CASE 2" << std::endl;
           unsigned left = atleast[i].size();
-          Stack<unsigned>::Iterator niter(atleast[i]);
+          Lib::Stack<unsigned>::Iterator niter(atleast[i]);
           while(niter.hasNext() && left >= i+1){
             unsigned c = niter.next();
             //std::cout << ">> " << c << std::endl;
             auto ns = Ngraph->get(c);
             if(ns->size()==i){
-              Stack<unsigned> clique;
+              Lib::Stack<unsigned> clique;
               clique.loadFromIterator(ns->iterator());
               clique.push(c);
               if(checkClique(Ngraph,clique)){
@@ -89,15 +89,15 @@ namespace FMB {
   private:
 
     // check if a clique is a clique
-    static bool checkClique(DHMap<unsigned,DHSet<unsigned>*>* Ngraph, Stack<unsigned>& clique)
+    static bool checkClique(Lib::DHMap<unsigned,Lib::DHSet<unsigned>*>* Ngraph, Lib::Stack<unsigned>& clique)
     {
       //std::cout << "CHECK "; for(unsigned j=0;j<clique.size();j++){ std::cout << clique[j] << " ";}; std::cout << std::endl;
 
       for(unsigned i=0;i<clique.size()-1;i++){
         unsigned c1 = clique[i];
         auto ns = Ngraph->get(c1);
         //std::cout << c1 << " neighbours: "; 
-        //DHSet<unsigned>::Iterator pit(*ns);while(pit.hasNext()){std::cout << pit.next() << " ";};std::cout<<std::endl;
+        //Lib::DHSet<unsigned>::Iterator pit(*ns);while(pit.hasNext()){std::cout << pit.next() << " ";};std::cout<<std::endl;
         for(unsigned j=i+1;j<clique.size();j++){
           unsigned c2 = clique[j];
           //std::cout << "checking " << c2 << " is a neighbour of " << c1 << std::endl;