Index: vis_dev/sharpSAT/src/shared/Interface/AnalyzerData.cpp
===================================================================
--- vis_dev/sharpSAT/src/shared/Interface/AnalyzerData.cpp	(revision 29)
+++ vis_dev/sharpSAT/src/shared/Interface/AnalyzerData.cpp	(revision 29)
@@ -0,0 +1,344 @@
+// Class automatically generated by Dev-C++ New Class wizard
+
+#include "AnalyzerData.h" // class's header file
+
+// class constructor
+AnalyzerData::AnalyzerData()
+{
+    init();
+}
+
+void AnalyzerData::init()
+{
+    nVars = 0;
+    nUsedVars = 0;
+    
+    nOriginalClauses = 0;
+    
+    nRemovedClauses = 0;    
+    
+    nAddedClauses = 0;
+    
+    evalData.clear();
+    evalData.resize(XX_MAX_IDX,0.0);
+    
+    nReceivedSatAssignments = 0;   
+    
+    rnProbOfSat = 0.0;   
+     
+    nConflicts = 0;
+    nImplications = 0;
+    nImplicitImplications = 0;
+    nProcessedComponents = 0;
+        
+    maxDecLevel = 0;
+    nDecisions = 0;    
+}
+
+void AnalyzerData::loadFromFile(const char *lpcstrFileName)
+{
+  ifstream in(lpcstrFileName);
+  
+  init();
+  
+  const int sz = 1024;
+  char buf[sz];
+  char desc[100];
+  
+  bool valIdentified = false;
+  
+  memset(desc,0,100);
+  while(in.getline(desc,100))
+  {
+    valIdentified = false;
+    
+    for(unsigned int i = 0; i < INT_MAX_ID; i++)
+     if(!strcmp(desc,intDataDesc[i]))
+      {
+        valIdentified = true;	
+	in.getline(buf,sz);
+	setI((INT_DATA_ID) i, atoi(buf));
+        break;
+      }    
+    
+    
+    if(!valIdentified)
+     for(int i = 0; i < XX_MAX_IDX; i++)
+      if(!strcmp(desc,doubleDataDesc[i]))
+      {
+        valIdentified = true;
+	in.getline(buf,sz);
+	evalData[i] = strtod(buf,NULL);
+        break;
+      }    
+     
+    if(!valIdentified)
+    {
+      if(!strcmp(desc,"time"))
+      {
+       in.getline(buf,sz);
+       elapsedTime = strtod(buf,NULL);
+      }       
+      else if(!strcmp(desc,"SolverExitState"))
+      {
+         in.getline(buf,sz);
+	 theExitState = (SOLVER_StateT) atoi(buf);
+      } else if(!strcmp(desc,"rnProbOfSAT"))
+      {
+         in >> rnProbOfSat;	 
+      }    
+    }     
+  }
+}
+
+
+void AnalyzerData::writeToFile(const char *lpcstrFileName) const
+{
+  ofstream out(lpcstrFileName);
+  
+  for(int i = 0; i < INT_MAX_ID;i++)
+  {
+     out<<intDataDesc[i]<<endl;   
+     out<<getI((INT_DATA_ID)i)<<endl;
+  }
+  
+  for(int i = 0; i < XX_MAX_IDX;i++)
+  {
+     out<<doubleDataDesc[i]<<endl;   
+     out<<get((DATA_IDX)i)<<endl;
+  }
+  
+  out<<"time"<<endl;
+  out<<elapsedTime<<endl;
+    
+  out<<"SolverExitState"<<endl;
+  out<<theExitState<<endl;
+  
+  #ifdef GMP_BIGNUM
+    char buf[nVars+2];
+    memset(buf,0,nVars+2);
+    mp_exp_t exp;
+    mpf_get_str(buf,&exp,10,nVars+2,rnProbOfSat.get_mpf_t());
+ 
+    out<<"rnProbOfSAT"<<endl;
+    out<<"0."<<buf<<"e"<<exp<<endl;
+  #else
+    out<<"rnProbOfSAT"<<endl;
+    out<<rnProbOfSat<<endl;
+  #endif
+}
+
+
+
+unsigned int AnalyzerData::getI(INT_DATA_ID idataID) const
+{
+  unsigned int res = 0;
+  
+  switch(idataID)
+  {
+    case NVARS: res = nVars;
+                break;
+    case NUSED_VARS: res = nUsedVars;
+                break;
+    case NORIGINAL_CLAUSES: res = nOriginalClauses;
+                break;
+    case NREMOVED_CLAUSES: res = nRemovedClauses;
+                break;
+    case NADDED_CLAUSES: res = nAddedClauses;
+                break;
+    case NRECEIVED_ASS:  res = nReceivedSatAssignments;
+                break;
+    case NCONFLICTS: res = nConflicts; 
+                break;
+    case NIMPLICATIONS: res = nImplications; 
+                break;
+    case NIBCPIMPLS: res = nImplicitImplications; 
+                break;
+    case NPROCESSED_COMPS:res = nProcessedComponents; 
+                break;
+    case MAX_DL: res = maxDecLevel; 
+                break;
+    case MAX_SOL_DL: res = maxSolutionLevel;
+                break;
+    case NDECISIONS: res = nDecisions;     
+                break;
+    default: break;
+  };
+
+  return res;
+}
+
+
+bool AnalyzerData::setI(INT_DATA_ID idataID, int val)
+{ 
+  switch(idataID)
+  {
+    case NVARS: nVars = val;
+                break;
+    case NUSED_VARS: nUsedVars = val;
+                break;
+    case NORIGINAL_CLAUSES: nOriginalClauses = val;
+                break;
+    case NREMOVED_CLAUSES: nRemovedClauses = val;
+                break;
+    case NADDED_CLAUSES: nAddedClauses = val;
+                break;
+    case NRECEIVED_ASS:  nReceivedSatAssignments = val;
+                break;
+    case NCONFLICTS: nConflicts = val; 
+                break;
+    case NIMPLICATIONS: nImplications = val; 
+                break;
+    case NIBCPIMPLS: nImplicitImplications = val; 
+                break;
+    case NPROCESSED_COMPS: nProcessedComponents = val; 
+                break;
+    case MAX_DL:  maxDecLevel = val; 
+                break;
+    case MAX_SOL_DL: maxSolutionLevel = val;
+                break;
+    case NDECISIONS: nDecisions = val;     
+                break;
+    default: return false;
+  };
+  return true;
+}
+
+// class destructor
+AnalyzerData::~AnalyzerData()
+{
+	// insert your code here
+}
+
+
+CRunAnalyzer::CRunAnalyzer()
+{
+	// insert your code here
+}
+
+
+
+
+
+const AnalyzerData &CRunAnalyzer::getData() const
+{		
+    return theData;		
+}
+		
+void CRunAnalyzer::init(int nVars, int nClauses)
+{
+    theData.init();
+	
+	theData.nVars = nVars;
+	theData.nOriginalClauses = nClauses;	
+	
+    first = true;
+}
+	
+
+void CRunAnalyzer::setValue(DATA_IDX dataIDX, double someData)	
+{
+   theData.evalData[dataIDX] = someData;
+}
+
+void CRunAnalyzer::addValue(ID_DATA dataID, int actDecLevel, double someData)
+{
+   switch(dataID)
+   {
+      case CCL_1stUIP:      
+         if(someData > theData.evalData[LONGEST_CCL_1stUIP])
+                      theData.evalData[LONGEST_CCL_1stUIP] = someData;
+	 theData.evalData[AVG_CCL_1stUIP] += (double) someData;
+	 break;
+	 
+      case CCL_lastUIP:      
+         if(someData > theData.evalData[LONGEST_CCL_lastUIP])
+                      theData.evalData[LONGEST_CCL_lastUIP] = someData;
+	 theData.evalData[AVG_CCL_lastUIP] += (double) someData;
+	 break;
+	 
+      case CONFLICT:         
+         theData.nConflicts+= (int) someData;
+	 theData.evalData[AVG_CONFLICT_LEV] += (double) actDecLevel;
+         theData.evalData[AVG_DEC_LEV] += (double) actDecLevel;
+         break;
+	 
+      case DECISION:
+         theData.nDecisions++;
+	 
+	 if (actDecLevel > theData.maxDecLevel)
+               theData.maxDecLevel = actDecLevel;
+	 break;	 
+
+      case SOLUTION:
+         
+         theData.evalData[AVG_SOLUTION_LEV] += (double) actDecLevel;
+         theData.evalData[AVG_DEC_LEV] += (double) actDecLevel;    
+         theData.nReceivedSatAssignments++;  
+         break;
+	 
+      case IMPLICATION:
+      
+         theData.nImplications += (int) someData;
+         break;          
+      case IBCPIMPL:
+         theData.nImplicitImplications += (int) someData;
+         break;          
+   };
+}     
+
+void CRunAnalyzer::addClause()
+{
+    theData.nAddedClauses++;
+}
+ 
+
+void CRunAnalyzer::setUsedVars(unsigned int nUsedVars)
+{
+    theData.nUsedVars = nUsedVars;
+}
+
+void CRunAnalyzer::setSatCount(const CRealNum &rnCodedSols)
+{ 
+ to_div_2exp(theData.rnProbOfSat,rnCodedSols,theData.nUsedVars); 
+}
+
+/*
+bool CRunAnalyzer::includeInPrBackBone(CAssignment &s, double nSols)
+{
+    //theData.thePrBackBone.include(s,nSols);
+	return true;
+}
+*/
+
+CRunAnalyzer::~CRunAnalyzer()
+{
+	// insert your code here
+}
+
+// No description
+void CRunAnalyzer::finishcountSATAnalysis()
+{
+   theData.finishcountSATAnalysis();
+}
+
+
+void AnalyzerData::finishcountSATAnalysis()
+{
+   if (nConflicts != 0)
+   {
+      evalData[AVG_CONFLICT_LEV] /= (double) nConflicts + nImplicitImplications;
+      evalData[AVG_CCL_1stUIP] /= (double) nConflicts + nImplicitImplications;
+      evalData[AVG_CCL_lastUIP] /= (double)nConflicts + nImplicitImplications; 
+   }
+   
+   if (nReceivedSatAssignments != 0)
+   {
+      evalData[AVG_SOLUTION_LEV] /= (double) nReceivedSatAssignments;   
+   }
+   else evalData[AVG_SOLUTION_LEV] = 0.0;
+   
+   if (nConflicts != 0  || nReceivedSatAssignments != 0)
+      evalData[AVG_DEC_LEV] /= (double) nConflicts + nReceivedSatAssignments;    
+}
+
Index: vis_dev/sharpSAT/src/shared/Interface/AnalyzerData.h
===================================================================
--- vis_dev/sharpSAT/src/shared/Interface/AnalyzerData.h	(revision 29)
+++ vis_dev/sharpSAT/src/shared/Interface/AnalyzerData.h	(revision 29)
@@ -0,0 +1,284 @@
+// Class automatically generated by Dev-C++ New Class wizard
+
+#ifndef ANALYZERDATA_H
+#define ANALYZERDATA_H
+
+#include <RealNumberTypes.h>
+
+//#include <Interface/Assignment.h>
+#include "../src_sharpSAT/Basics.h"
+
+#include <vector>
+
+#include <iostream>
+#include <fstream>
+#include <cstring>
+
+using namespace std;
+
+enum DATA_IDX
+{
+
+ AVG_DEC_LEV  = 0,  // average decision Level
+ AVG_CONFLICT_LEV, // average conflict Level
+ AVG_SOLUTION_LEV, // average solution Level
+         
+ LONGEST_CCL_lastUIP, // longest conflict clause by last UIP scheme
+ AVG_CCL_lastUIP, // avg conflict clause length by last UIP scheme
+ LONGEST_CCL_1stUIP, // longest conflict clause by 1st UIP scheme 
+ AVG_CCL_1stUIP,  // avg conflict clause length by 1st UIP scheme
+ 
+ FCACHE_MAXMEM,  // Formula Cache Memoery Bound
+ FCACHE_MEMUSE,  // Formula Cache memory usage
+ FCACHE_USEDBUCKETS, // number of hashbuckets used
+ FCACHE_CACHEDCOMPS,
+ FCACHE_RETRIEVALS, // number of retrieved components
+ FCACHE_INCLUDETRIES, // number of times it was tried to put a component into the cache
+ XX_MAX_IDX 
+};
+
+/// strings describing the data identified by DATA_IDX
+static const char * doubleDataDesc[] = 
+{
+  "avg dec dl","avg conflict dl","avg solution dl","longest ccl lastUIP","avg ccl lastUIP","longest ccl firstUIP","avg ccl firstUIP",
+  "cacher memory bound", "cache mem-usage","cache used buckets","cache cached components","cache retrievals", "cache include tries","NOTHING"
+};
+
+
+enum INT_DATA_ID
+{
+ NVARS =  0,  // num Of Vars
+ NUSED_VARS,
+ NORIGINAL_CLAUSES,
+ NREMOVED_CLAUSES,
+ NADDED_CLAUSES,
+ NRECEIVED_ASS,  // int nReceivedSatAssignments;
+ NCONFLICTS, // int nConflicts; 
+ NIMPLICATIONS, // int nImplications; 
+ NIBCPIMPLS,
+ NPROCESSED_COMPS, // int nProcessedComponents; 
+ MAX_DL, // int maxDecLevel; 
+ MAX_SOL_DL, // int maxSolutionLevel;
+ NDECISIONS, // int nDecisions;         
+ INT_MAX_ID 
+};
+
+/// strings describing the data identified by INT_DATA_ID
+static const char * intDataDesc[] = 
+{
+  "variables","used vars","original clauses","removed clauses","added clauses",
+  "received sat assignments", "conflicts","implications","ibcpimplications","processed components",
+  "max dl","max solution dl","decisions","NOTHING"
+};
+
+
+enum ID_DATA
+{
+ DECISION,  
+ CONFLICT, 
+ SOLUTION, 
+ IMPLICATION,
+ IBCPIMPL,
+ CCL_lastUIP, // conflict clause by last UIP scheme 
+ CCL_1stUIP //  conflict clause by 1st UIP scheme 
+ 
+ 
+ //XX_MAX_IDX = 7
+};
+ 
+ 
+ 
+class AnalyzerData
+{
+  public:    
+        double elapsedTime;
+	
+	SOLVER_StateT theExitState; 
+	/// Zahl der Variablen der Instanz        
+        int nVars;    
+        
+	/// Zahl der Variablen, die tatsï¿œhlich in Klauseln vorkommen
+        int nUsedVars;
+        
+	/// Klauselzahl
+        int nOriginalClauses; 
+	
+	int nRemovedClauses; 
+        
+        int nAddedClauses;                
+        
+        // Zahl der erfllenden Belegungen, die bergeben wurden
+        // sollte Kleiner sein, als die Zahl der eigentlichen Lï¿œungen
+        int nReceivedSatAssignments;
+        
+        /// Anzahl aller getroffenen Entscheidungen
+        int nDecisions;         
+        
+        /// Zahl aller gefundenen Implikationen
+        int nImplications; 
+	
+	int nImplicitImplications; 
+	
+        /// Zahl aller wï¿œrend der Suche aufgetretenen Konflikte
+        int nConflicts; 
+        
+	
+	/// insgesamt bearbeitete Komponenten
+	int nProcessedComponents; 
+        
+        /// maximaler Decision level
+        int maxDecLevel;
+        int maxSolutionLevel;
+	
+	vector<double> evalData;
+        /// Wahrscheinlichkeit der Erfuellbarkeit der Instanz        
+	CRealNum rnProbOfSat;	
+	
+	// class constructor
+	AnalyzerData();
+	// class destructor
+	~AnalyzerData();
+
+	/// setzt alle Werte auf Null zurck (nur intern wichtig).
+	void init();
+	
+	CRealNum getAllAssignments() const
+	{
+	 CRealNum res;
+	 pow2(res,nVars);
+	 return res;
+	}	
+	
+	CRealNum getNumSatAssignments() const
+        {
+	  return rnProbOfSat * getAllAssignments();
+	}
+	
+	void printNumSatAss_whole() const
+	{
+	#ifdef GMP_BIGNUM
+	  CRealNum res;
+	  res.set_prec(nVars);
+	  pow2(res,nVars);
+	  res *= rnProbOfSat;
+	  char buf[nVars+2];
+	  mp_exp_t exp;
+	  memset(buf,0,nVars+2);
+	  mpf_get_str(buf,&exp,10,nVars+2,res.get_mpf_t());
+	  
+	  //cout <<"e"<<(exp>0?"+":"-")<<exp;
+	  for(int i=exp-1; i>=0;i--) if(buf[i] == 0) buf[i] = '0';
+	  //gmp_printf("%F",res.get_mpf_t());
+	  printf(buf);
+	  #endif
+	}
+	
+        char*  printNumSatAss_vis() const
+	{
+	 char* buf=(char*)calloc(nVars+2,sizeof(char));
+	 #ifdef GMP_BIGNUM
+	
+	  CRealNum res;
+	  res.set_prec(nVars);
+	  pow2(res,nVars);
+	  res *= rnProbOfSat;
+	  mp_exp_t exp;
+	  memset(buf,0,nVars+2);
+	  mpf_get_str(buf,&exp,10,nVars+2,res.get_mpf_t());
+	  
+	  //cout <<"e"<<(exp>0?"+":"-")<<exp;
+	  for(int i=exp-1; i>=0;i--) if(buf[i] == 0) buf[i] = '0';
+	  //gmp_printf("%F",res.get_mpf_t());
+	 #endif
+         return buf;
+ 
+	}
+
+	double get(DATA_IDX dataID) const
+	{
+	 return evalData[dataID];
+	}
+	
+	unsigned int getI(INT_DATA_ID idataID) const;
+        
+	bool setI(INT_DATA_ID idataID, int val);
+	
+	void set(DATA_IDX dataID, double val)
+	{
+	 evalData[dataID] = val;
+	}
+	
+	
+	void finishcountSATAnalysis();
+	
+	void writeToFile(const char *lpcstrFileName) const;
+	void loadFromFile(const char *lpcstrFileName);
+};
+/*@}*/
+
+/** \addtogroup RunAnalyze Laufanalyse
+ * \ingroup Interna
+ */
+/*@{*/
+class CRunAnalyzer
+{
+	AnalyzerData theData;    
+
+	bool first;
+    
+  protected:
+	
+	//bool includeInPrBackBone(CAssignment &s,double nSols);
+		
+    
+  public:        
+        
+	// class constructor
+	CRunAnalyzer();
+	// class destructor
+	~CRunAnalyzer();
+		
+	const AnalyzerData &getData() const;
+	
+	AnalyzerData &changeableData(){return theData;}
+	
+	void init(int nVars, int nClauses);        
+        
+	//void setUsedVars(const set<int> &rUsedVars);	
+	
+        void setUsedVars(unsigned int nUsedVars);
+	
+	void setRemovedClauses(int rClauses)
+	{
+	  theData.nRemovedClauses = rClauses;
+	}
+       
+	void addValue(ID_DATA dataID, int actDecLevel = 0, double someData = 0.0);
+	
+	void setValue(DATA_IDX dataIDX, double someData);	
+	
+        void addClause();       
+	
+	void setSatCount(const CRealNum  &rnCodedSols);
+	
+	void setSatProb(const CRealNum  &rnProb)
+	{
+	  theData.rnProbOfSat = rnProb;
+	}
+	
+	
+	
+	void setExitState(SOLVER_StateT st)
+	{
+	  theData.theExitState = st;
+	}
+	void setElapsedTime(double timeV)
+	{
+	 theData.elapsedTime = timeV;
+	}
+
+	// No description
+	void finishcountSATAnalysis();
+};
+#endif // CANALYZERDATA_H
+
Index: vis_dev/sharpSAT/src/shared/Interface/semantic.cache
===================================================================
--- vis_dev/sharpSAT/src/shared/Interface/semantic.cache	(revision 29)
+++ vis_dev/sharpSAT/src/shared/Interface/semantic.cache	(revision 29)
@@ -0,0 +1,22 @@
+;; Object Interface/
+;; SEMANTICDB Tags save file
+(semanticdb-project-database-file "Interface/"
+  :tables (list 
+   (semanticdb-table "AnalyzerData.h"
+    :major-mode 'c-mode
+    :tags '(("ANALYZERDATA_H" variable (:constant-flag t) nil [86 111]) ("RealNumberTypes.h" include (:system-flag t) nil [110 138]) ("../src_sharpSAT/Basics.h" include nil nil [176 211]) ("vector" include (:system-flag t) nil [213 230]) ("iostream" include (:system-flag t) nil [232 251]) ("fstream" include (:system-flag t) nil [252 270]) ("DATA_IDX" type (:members (("AVG_DEC_LEV" variable (:constant-flag t :default-value (328 329) :type "int") (reparse-symbol enumsubparts) [313 329]) ("AVG_CONFLICT_LEV" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [359 376]) ("AVG_SOLUTION_LEV" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [404 421]) ("LONGEST_CCL_lastUIP" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [459 479]) ("AVG_CCL_lastUIP" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [527 543]) ("LONGEST_CCL_1stUIP" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [594 613]) ("AVG_CCL_1stUIP" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [661 676]) ("FCACHE_MAXMEM" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [729 743]) ("FCACHE_MEMUSE" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [777 791]) ("FCACHE_USEDBUCKETS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [824 843]) ("FCACHE_CACHEDCOMPS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [875 894]) ("FCACHE_RETRIEVALS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [896 914]) ("FCACHE_INCLUDETRIES" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [950 970]) ("XX_MAX_IDX" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1038 1051])) :type "enum") nil [295 1052]) ("doubleDataDesc" variable (:pointer 1 :dereference 1 :typemodifiers ("static") :constant-flag t :default-value "{
+  \"avg dec dl\",\"avg conflict dl\",\"avg solution dl\",\"longest ccl lastUIP\",\"avg ccl lastUIP\",\"longest ccl firstUIP\",\"avg ccl firstUIP\",
+  \"cacher memory bound\", \"cache mem-usage\",\"cache used buckets\",\"cache cached components\",\"cache retrievals\", \"cache include tries\",\"NOTHING\"
+}" :type "char") nil [1109 1429]) ("INT_DATA_ID" type (:members (("NVARS" variable (:constant-flag t :default-value (1461 1462) :type "int") (reparse-symbol enumsubparts) [1452 1462]) ("NUSED_VARS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1481 1492]) ("NORIGINAL_CLAUSES" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1494 1512]) ("NREMOVED_CLAUSES" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1514 1531]) ("NADDED_CLAUSES" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1533 1548]) ("NRECEIVED_ASS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1550 1564]) ("NCONFLICTS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1599 1610]) ("NIMPLICATIONS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1632 1646]) ("NIBCPIMPLS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1671 1682]) ("NPROCESSED_COMPS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1684 1701]) ("MAX_DL" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1733 1740]) ("MAX_SOL_DL" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1763 1774]) ("NDECISIONS" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1801 1812]) ("INT_MAX_ID" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [1842 1855])) :type "enum") nil [1432 1856]) ("intDataDesc" variable (:pointer 1 :dereference 1 :typemodifiers ("static") :constant-flag t :default-value "{
+  \"variables\",\"used vars\",\"original clauses\",\"removed clauses\",\"added clauses\",
+  \"received sat assignments\", \"conflicts\",\"implications\",\"ibcpimplications\",\"processed components\",
+  \"max dl\",\"max solution dl\",\"decisions\",\"NOTHING\"
+}" :type "char") nil [1916 2188]) ("ID_DATA" type (:members (("DECISION" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [2207 2216]) ("CONFLICT" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [2220 2229]) ("SOLUTION" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [2232 2241]) ("IMPLICATION" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [2244 2256]) ("IBCPIMPL" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [2258 2267]) ("CCL_lastUIP" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [2269 2281]) ("CCL_1stUIP" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [2322 2395])) :type "enum") nil [2191 2396]) ("AnalyzerData" type (:members (("public" label nil (reparse-symbol classsubparts) [2426 2433]) ("elapsedTime" variable (:type "double") (reparse-symbol classsubparts) [2446 2465]) ("theExitState" variable (:type ("SOLVER_StateT" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2469 2496]) ("nVars" variable (:type "int") (reparse-symbol classsubparts) [2550 2560]) ("nUsedVars" variable (:type "int") (reparse-symbol classsubparts) [2646 2660]) ("nOriginalClauses" variable (:type "int") (reparse-symbol classsubparts) [2695 2716]) ("nRemovedClauses" variable (:type "int") (reparse-symbol classsubparts) [2721 2741]) ("nAddedClauses" variable (:type "int") (reparse-symbol classsubparts) [2760 2778]) ("nReceivedSatAssignments" variable (:type "int") (reparse-symbol classsubparts) [2947 2975]) ("nDecisions" variable (:type "int") (reparse-symbol classsubparts) [3045 3060]) ("nImplications" variable (:type "int") (reparse-symbol classsubparts) [3135 3153]) ("nImplicitImplications" variable (:type "int") (reparse-symbol classsubparts) [3158 3184]) ("nConflicts" variable (:type "int") (reparse-symbol classsubparts) [3262 3277]) ("nProcessedComponents" variable (:type "int") (reparse-symbol classsubparts) [3330 3355]) ("maxDecLevel" variable (:type "int") (reparse-symbol classsubparts) [3411 3427]) ("maxSolutionLevel" variable (:type "int") (reparse-symbol classsubparts) [3436 3457]) ("evalData" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3461 3485]) ("rnProbOfSat" variable (:type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3557 3578]) ("AnalyzerData" function (:prototype-flag t :constructor-flag t :type ("AnalyzerData" type "class")) (reparse-symbol classsubparts) [3605 3620]) ("AnalyzerData" function (:prototype-flag t :destructor-flag t :type "void") (reparse-symbol classsubparts) [3643 3659]) ("init" function (:prototype-flag t :type "void") (reparse-symbol classsubparts) [3721 3733]) ("getAllAssignments" function (:type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3737 3826]) ("getNumSatAssignments" function (:type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3831 3926]) ("printNumSatAss_whole" function (:type "void") (reparse-symbol classsubparts) [3930 4358]) ("printNumSatAss_vis" function (:pointer 1 :type "char") (reparse-symbol classsubparts) [4369 4833]) ("get" function (:arguments (("dataID" variable (:type ("DATA_IDX" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [4847 4863])) :type "double") (reparse-symbol classsubparts) [4836 4902]) ("getI" function (:prototype-flag t :arguments (("idataID" variable (:type ("INT_DATA_ID" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [4924 4944])) :type "unsigned int") (reparse-symbol classsubparts) [4906 4951]) ("setI" function (:prototype-flag t :arguments (("idataID" variable (:type ("INT_DATA_ID" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [4972 4992]) ("val" variable (:type "int") (reparse-symbol arg-sub-list) [4993 5001])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [4962 5002]) ("set" function (:arguments (("dataID" variable (:type ("DATA_IDX" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [5015 5031]) ("val" variable (:type "double") (reparse-symbol arg-sub-list) [5032 5043])) :type "void") (reparse-symbol classsubparts) [5006 5075]) ("finishcountSATAnalysis" function (:prototype-flag t :type "void") (reparse-symbol classsubparts) [5081 5111]) ("writeToFile" function (:prototype-flag t :arguments (("lpcstrFileName" variable (:pointer 1 :constant-flag t :type "char") (reparse-symbol arg-sub-list) [5132 5159])) :type "void") (reparse-symbol classsubparts) [5115 5166]) ("loadFromFile" function (:prototype-flag t :arguments (("lpcstrFileName" variable (:pointer 1 :constant-flag t :type "char") (reparse-symbol arg-sub-list) [5186 5213])) :type "void") (reparse-symbol classsubparts) [5168 5214])) :type "class") nil [2403 5217]) ("CRunAnalyzer" type (:members (("theData" variable (:type ("AnalyzerData" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5318 5339]) ("first" variable (:type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5346 5357]) ("protected" label nil (reparse-symbol classsubparts) [5365 5375]) ("public" label nil (reparse-symbol classsubparts) [5446 5453]) ("CRunAnalyzer" function (:prototype-flag t :constructor-flag t :type ("CRunAnalyzer" type "class")) (reparse-symbol classsubparts) [5494 5509]) ("CRunAnalyzer" function (:prototype-flag t :destructor-flag t :type "void") (reparse-symbol classsubparts) [5532 5548]) ("getData" function (:prototype-flag t :constant-flag t :type ("AnalyzerData" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5553 5589]) ("changeableData" function (:type ("AnalyzerData" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5593 5640]) ("init" function (:prototype-flag t :arguments (("nVars" variable (:type "int") (reparse-symbol arg-sub-list) [5654 5664]) ("nClauses" variable (:type "int") (reparse-symbol arg-sub-list) [5665 5678])) :type "void") (reparse-symbol classsubparts) [5644 5679]) ("setUsedVars" function (:prototype-flag t :arguments (("nUsedVars" variable (:type "unsigned int") (reparse-symbol arg-sub-list) [5773 5796])) :type "void") (reparse-symbol classsubparts) [5756 5797]) ("setRemovedClauses" function (:arguments (("rClauses" variable (:type "int") (reparse-symbol arg-sub-list) [5824 5837])) :type "void") (reparse-symbol classsubparts) [5801 5882]) ("addValue" function (:prototype-flag t :arguments (("dataID" variable (:type ("ID_DATA" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [5906 5921]) ("actDecLevel" variable (:default-value "0" :type "int") (reparse-symbol arg-sub-list) [5922 5941]) ("someData" variable (:default-value "0.0" :type "double") (reparse-symbol arg-sub-list) [5943 5964])) :type "void") (reparse-symbol classsubparts) [5892 5966]) ("setValue" function (:prototype-flag t :arguments (("dataIDX" variable (:type ("DATA_IDX" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [5984 6001]) ("someData" variable (:type "double") (reparse-symbol arg-sub-list) [6002 6018])) :type "void") (reparse-symbol classsubparts) [5970 6019]) ("addClause" function (:prototype-flag t :type "void") (reparse-symbol classsubparts) [6031 6048]) ("setSatCount" function (:prototype-flag t :arguments (("rnCodedSols" variable (:constant-flag t :type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [6076 6105])) :type "void") (reparse-symbol classsubparts) [6059 6106]) ("setSatProb" function (:arguments (("rnProb" variable (:constant-flag t :type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [6126 6150])) :type "void") (reparse-symbol classsubparts) [6110 6189]) ("setExitState" function (:arguments (("st" variable (:type ("SOLVER_StateT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [6215 6232])) :type "void") (reparse-symbol classsubparts) [6197 6268]) ("setElapsedTime" function (:arguments (("timeV" variable (:type "double") (reparse-symbol arg-sub-list) [6290 6303])) :type "void") (reparse-symbol classsubparts) [6270 6340]) ("finishcountSATAnalysis" function (:prototype-flag t :type "void") (reparse-symbol classsubparts) [6362 6392])) :type "class") nil [5296 6395]))
+    :file "AnalyzerData.h"
+    :pointmax 6423
+    )
+   )
+  :file "semantic.cache"
+  :semantic-tag-version "2.0beta3"
+  :semanticdb-version "2.0beta3"
+  )
Index: vis_dev/sharpSAT/src/shared/RealNumberTypes.cpp
===================================================================
--- vis_dev/sharpSAT/src/shared/RealNumberTypes.cpp	(revision 29)
+++ vis_dev/sharpSAT/src/shared/RealNumberTypes.cpp	(revision 29)
@@ -0,0 +1,60 @@
+#include "RealNumberTypes.h"
+
+#include <math.h>
+
+#ifdef GMP_BIGNUM
+
+const mpf_class mpf_TWO = 2.0;
+
+bool pow(mpf_class &res, const mpf_class &base, unsigned long int iExp)
+{
+   mpf_pow_ui(res.get_mpf_t(),base.get_mpf_t(), iExp);        
+   return true;
+}
+
+bool pow2(mpf_class &res, unsigned long int iExp)
+{
+   mpf_class x(2.0,res.get_prec());
+  // x= 2.0;
+   mpf_pow_ui(res.get_mpf_t(),x.get_mpf_t(), iExp);        
+   return true;
+}
+
+bool to_div_2exp(mpf_class &res, const mpf_class &op1, unsigned long int iExp)
+{
+   mpf_div_2exp(res.get_mpf_t(),op1.get_mpf_t(),iExp); 
+   return true;
+}
+
+double to_doubleT(const mpf_class &num)
+{
+  return mpf_get_d(num.get_mpf_t());
+}
+
+#else
+
+bool pow(CRealNum &res, double &base, unsigned long int iExp)
+{
+   res = pow(base, iExp);    
+   return true;    
+}
+
+bool pow2(CRealNum &res, unsigned long int iExp)
+{
+   res = pow(2.00, iExp);        
+   return true;
+}
+
+
+bool to_div_2exp(CRealNum &res, const CRealNum &op1, unsigned long int iExp)
+{
+   res  = op1 / pow(2.00,iExp); 
+   return true;
+}
+
+
+long double to_doubleT(const CRealNum &num)
+{
+  return (long double) num;
+}
+#endif
Index: vis_dev/sharpSAT/src/shared/RealNumberTypes.h
===================================================================
--- vis_dev/sharpSAT/src/shared/RealNumberTypes.h	(revision 29)
+++ vis_dev/sharpSAT/src/shared/RealNumberTypes.h	(revision 29)
@@ -0,0 +1,27 @@
+#ifndef REALNUMBERTYPES_H
+#define REALNUMBERTYPES_H
+
+
+
+using namespace std;
+
+#ifdef GMP_BIGNUM
+ #include <gmpxx.h>
+ typedef mpf_class CRealNum;
+ extern bool pow(mpf_class &res, const mpf_class &base, unsigned long int iExp);
+ extern bool pow2(mpf_class &res, unsigned long int iExp);
+ extern bool to_div_2exp(mpf_class &res, const mpf_class &op1, unsigned long int iExp);
+ extern double to_doubleT(const mpf_class &num);
+ 
+
+
+#else
+ typedef long double CRealNum;
+
+ extern bool pow(CRealNum &res, CRealNum base, unsigned long int iExp);
+ extern bool pow2(CRealNum &res, unsigned long int iExp);
+ extern bool to_div_2exp(CRealNum &res, const CRealNum &op1, unsigned long int iExp);
+ extern long double to_doubleT(const CRealNum &num);
+#endif
+
+#endif
Index: vis_dev/sharpSAT/src/shared/SomeTime.cpp
===================================================================
--- vis_dev/sharpSAT/src/shared/SomeTime.cpp	(revision 29)
+++ vis_dev/sharpSAT/src/shared/SomeTime.cpp	(revision 29)
@@ -0,0 +1,20 @@
+#include "SomeTime.h"
+
+int CStepTime::timeVal = 0;
+
+
+
+bool diffTimes(timeval& ret, const timeval &tLater, const timeval &tEarlier)
+{
+  long int ad = 0;
+  long int bd = 0;  
+  
+  if(tLater.tv_usec < tEarlier.tv_usec)
+  {
+    ad = 1;
+    bd = 1000000;
+  }
+  ret.tv_sec = tLater.tv_sec - ad - tEarlier.tv_sec;
+  ret.tv_usec = tLater.tv_usec + bd - tEarlier.tv_usec;
+  return true;
+}
Index: vis_dev/sharpSAT/src/shared/SomeTime.h
===================================================================
--- vis_dev/sharpSAT/src/shared/SomeTime.h	(revision 29)
+++ vis_dev/sharpSAT/src/shared/SomeTime.h	(revision 29)
@@ -0,0 +1,102 @@
+#ifndef SOMETIME_H
+#define SOMETIME_H
+
+#include<cstdlib>
+#include <sys/time.h> // To seed random generator
+
+using namespace std;
+
+extern bool diffTimes(timeval& ret, const timeval &tLater, const timeval &tEarlier);
+
+class CStepTime
+{
+   static int timeVal;
+   
+ public: 
+ 
+   static void makeStart()
+   {
+     timeVal = 0;
+   }
+   
+   static int getTime() 
+   {
+     return timeVal;
+   }
+   
+   static void stepTime() 
+   {
+     timeVal++;
+   }
+};
+
+
+
+class CStopWatch
+{
+   timeval timeStart;
+   timeval timeStop;
+   
+   long int timeBound;   
+ 
+ public:
+    
+   CStopWatch() {}
+   ~CStopWatch(){} 
+   
+   bool timeBoundBroken()
+   { 
+     timeval actTime;
+     gettimeofday(&actTime,NULL);
+     
+     return actTime.tv_sec - timeStart.tv_sec > timeBound;
+   }
+   
+   bool markStartTime()
+   {
+     return gettimeofday(&timeStart,NULL) == 0;
+   }
+   
+   bool markStopTime()
+   {
+     return gettimeofday(&timeStop,NULL) == 0;
+   }
+   
+   
+   void setTimeBound(long int seconds)
+   {
+     timeBound = seconds;
+   }
+   
+   long int getTimeBound()
+   {
+     return timeBound;
+   }
+   
+   double getElapsedTime()
+   {
+     timeval r;
+     double retT;
+     diffTimes(r,timeStop, timeStart);
+     
+     retT = r.tv_usec;
+     retT /= 1000000.0;
+     retT += (double)r.tv_sec;
+     return retT;
+   }
+   
+   unsigned int getElapsedusecs()
+   {
+     unsigned int retT;
+     timeval r;
+     
+     diffTimes(r,timeStop, timeStart);
+     
+     retT = r.tv_usec;
+     
+     retT += r.tv_sec * 1000000;
+     return retT;   
+   }
+};
+
+#endif
Index: vis_dev/sharpSAT/src/shared/semantic.cache
===================================================================
--- vis_dev/sharpSAT/src/shared/semantic.cache	(revision 29)
+++ vis_dev/sharpSAT/src/shared/semantic.cache	(revision 29)
@@ -0,0 +1,27 @@
+;; Object shared/
+;; SEMANTICDB Tags save file
+(semanticdb-project-database-file "shared/"
+  :tables (list 
+   (semanticdb-table "SomeTime.h"
+    :major-mode 'c-mode
+    :tags '(("SOMETIME_H" variable (:constant-flag t) nil [20 41]) ("sys/time.h" include (:system-flag t) nil [58 79]) ("diffTimes" function (:prototype-flag t :typemodifiers ("extern") :arguments (("ret" variable (:type ("timeval" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [153 166]) ("tLater" variable (:constant-flag t :type ("timeval" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [167 189]) ("tEarlier" variable (:constant-flag t :type ("timeval" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [190 214])) :type ("bool" type (:type "class") nil nil)) nil [131 215]) ("CStepTime" type (:members (("timeVal" variable (:typemodifiers ("static") :type "int") (reparse-symbol classsubparts) [238 257]) ("public" label nil (reparse-symbol classsubparts) [263 270]) ("makeStart" function (:typemodifiers ("static") :type "void") (reparse-symbol classsubparts) [277 328]) ("getTime" function (:typemodifiers ("static") :type "int") (reparse-symbol classsubparts) [336 388]) ("stepTime" function (:typemodifiers ("static") :type "void") (reparse-symbol classsubparts) [396 445])) :type "class") nil [217 448]) ("CStopWatch" type (:members (("timeStart" variable (:type ("timeval" type (:type "class") nil nil)) (reparse-symbol classsubparts) [474 492]) ("timeStop" variable (:type ("timeval" type (:type "class") nil nil)) (reparse-symbol classsubparts) [496 513]) ("timeBound" variable (:type "long int") (reparse-symbol classsubparts) [521 540]) ("public" label nil (reparse-symbol classsubparts) [547 554]) ("CStopWatch" function (:constructor-flag t :type ("CStopWatch" type "class")) (reparse-symbol classsubparts) [563 578]) ("CStopWatch" function (:destructor-flag t :type "void") (reparse-symbol classsubparts) [582 597]) ("timeBoundBroken" function (:type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [606 760]) ("markStartTime" function (:type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [768 846]) ("markStopTime" function (:type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [854 930]) ("setTimeBound" function (:arguments (("seconds" variable (:type "long int") (reparse-symbol arg-sub-list) [960 977])) :type "void") (reparse-symbol classsubparts) [942 1013]) ("getTimeBound" function (:type "long int") (reparse-symbol classsubparts) [1021 1077]) ("getElapsedTime" function (:type "double") (reparse-symbol classsubparts) [1085 1293]) ("getElapsedusecs" function (:type "unsigned int") (reparse-symbol classsubparts) [1301 1515])) :type "class") nil [452 1518]))
+    :file "SomeTime.h"
+    :pointmax 1527
+    )
+   (semanticdb-table "SomeTime.cpp"
+    :major-mode 'c++-mode
+    :tags '(("SomeTime.h" include nil nil [1 22]) ("CStepTime::timeVal" variable (:default-value "0" :type "int") nil [24 51]) ("diffTimes" function (:arguments (("ret" variable (:type ("timeval" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [70 83]) ("tLater" variable (:constant-flag t :type ("timeval" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [84 106]) ("tEarlier" variable (:constant-flag t :type ("timeval" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [107 131])) :type ("bool" type (:type "class") nil nil)) nil [55 380]))
+    :file "SomeTime.cpp"
+    :pointmax 381
+    )
+   (semanticdb-table "RealNumberTypes.h"
+    :major-mode 'c-mode
+    :tags '(("REALNUMBERTYPES_H" variable (:constant-flag t) nil [27 61]) ("gmpxx.h" include (:system-flag t) nil [97 115]) ("CRealNum" type (:typedef ("mpf_class" type (:type "class") nil nil) :superclasses "mpf_class" :type "typedef") nil [117 144]) ("pow" function (:prototype-flag t :typemodifiers ("extern") :arguments (("res" variable (:type ("mpf_class" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [162 177]) ("base" variable (:constant-flag t :type ("mpf_class" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [178 200]) ("iExp" variable (:type "unsigned long int") (reparse-symbol arg-sub-list) [201 224])) :type ("bool" type (:type "class") nil nil)) nil [146 225]) ("pow2" function (:prototype-flag t :typemodifiers ("extern") :arguments (("res" variable (:type ("mpf_class" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [244 259]) ("iExp" variable (:type "unsigned long int") (reparse-symbol arg-sub-list) [260 283])) :type ("bool" type (:type "class") nil nil)) nil [227 284]) ("to_div_2exp" function (:prototype-flag t :typemodifiers ("extern") :arguments (("res" variable (:type ("mpf_class" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [310 325]) ("op1" variable (:constant-flag t :type ("mpf_class" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [326 347]) ("iExp" variable (:type "unsigned long int") (reparse-symbol arg-sub-list) [348 371])) :type ("bool" type (:type "class") nil nil)) nil [286 372]) ("to_doubleT" function (:prototype-flag t :typemodifiers ("extern") :arguments (("num" variable (:constant-flag t :type ("mpf_class" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [399 420])) :type "double") nil [374 421]) ("CRealNum" type (:typedef ("long double") :superclasses "long double" :type "typedef") nil [433 462]) ("pow" function (:prototype-flag t :typemodifiers ("extern") :arguments (("res" variable (:type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [481 495]) ("base" variable (:type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [496 510]) ("iExp" variable (:type "unsigned long int") (reparse-symbol arg-sub-list) [511 534])) :type ("bool" type (:type "class") nil nil)) nil [465 535]) ("pow2" function (:prototype-flag t :typemodifiers ("extern") :arguments (("res" variable (:type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [554 568]) ("iExp" variable (:type "unsigned long int") (reparse-symbol arg-sub-list) [569 592])) :type ("bool" type (:type "class") nil nil)) nil [537 593]) ("to_div_2exp" function (:prototype-flag t :typemodifiers ("extern") :arguments (("res" variable (:type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [619 633]) ("op1" variable (:constant-flag t :type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [634 654]) ("iExp" variable (:type "unsigned long int") (reparse-symbol arg-sub-list) [655 678])) :type ("bool" type (:type "class") nil nil)) nil [595 679]) ("to_doubleT" function (:prototype-flag t :typemodifiers ("extern") :arguments (("num" variable (:constant-flag t :type ("CRealNum" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [711 731])) :type "long double") nil [681 732]))
+    :file "RealNumberTypes.h"
+    :pointmax 748
+    )
+   )
+  :file "semantic.cache"
+  :semantic-tag-version "2.0beta3"
+  :semanticdb-version "2.0beta3"
+  )