source: vis_dev/sharpSAT/src/src_sharpSAT/main.cpp @ 76

Last change on this file since 76 was 9, checked in by cecile, 13 years ago

add sharpSat

File size: 5.6 KB
Line 
1#include <iostream>
2
3#include <ctime> // To seed random generator
4#include <sys/time.h> // To seed random generator
5
6//include shared files
7#include <SomeTime.h>
8#include <Interface/AnalyzerData.h>
9
10#include "MainSolver/MainSolver.h"
11#include "Basics.h"
12
13
14using namespace std;
15
16
17CMainSolver theSolver;
18
19// No description
20void finalcSATEvaluation()
21{
22   const AnalyzerData &rAda = theRunAn.getData(); 
23       
24   if(rAda.theExitState == TIMEOUT)
25   {
26     toSTDOUT(endl << " TIMEOUT !"<<endl);
27     return;
28   } 
29       
30   toSTDOUT(endl<<endl);
31   toSTDOUT("#Variables:\t\t"<< rAda.nVars<<endl);
32   
33   if(rAda.nVars != rAda.nUsedVars)
34      toSTDOUT("#used Variables:\t"<< rAda.nUsedVars<<endl);
35   toSTDOUT("#Clauses:\t\t"<< rAda.nOriginalClauses<<endl);
36   toSTDOUT("#Clauses removed:\t"<< rAda.nRemovedClauses<<endl);
37   toSTDOUT("\n#added Clauses: \t"<< rAda.nAddedClauses<<endl);
38   
39   toSTDOUT("\n# of all assignments:\t" << rAda.getAllAssignments() 
40       << " = 2^(" << rAda.nVars<<")" <<endl);   
41
42   toSTDOUT("Pr[satisfaction]:\t" << rAda.rnProbOfSat <<endl);   
43
44   toSTDOUT("# of solutions:\t\t" << rAda.getNumSatAssignments() <<endl);
45   toSTDOUT("#SAT (full):   \t\t"); 
46    if(!CSolverConf::quietMode) rAda.printNumSatAss_whole();
47    toSTDOUT(endl);
48       
49    toDEBUGOUT(".. found in:\t\t" << rAda.nReceivedSatAssignments << " units"<<endl);
50   
51    toSTDOUT(endl);
52   
53    toSTDOUT("Num. conflicts:\t\t" << rAda.nConflicts<<endl);
54    toSTDOUT("Num. implications:\t" << rAda.nImplications<<endl);
55    toSTDOUT("Num. decisions:\t\t" << rAda.nDecisions<<endl);   
56    toSTDOUT("max decision level:\t" << rAda.maxDecLevel<<"\t\t");
57    toSTDOUT("avg decision level:\t"<< rAda.get(AVG_DEC_LEV)<<endl); 
58    toSTDOUT("avg conflict level:\t"<< rAda.get(AVG_CONFLICT_LEV)<<endl);
59    toSTDOUT("avg solution level:\t"<< rAda.get(AVG_SOLUTION_LEV)<<endl);
60   
61    toSTDOUT("CCLLen 1stUIP - max:\t"<< rAda.get(LONGEST_CCL_1stUIP));
62    toSTDOUT("\t avg:\t"<< rAda.get(AVG_CCL_1stUIP)<<endl);
63    toSTDOUT("CCLLen lastUIP - max:\t"<< rAda.get(LONGEST_CCL_lastUIP));
64    toSTDOUT("\t avg:\t"<< rAda.get(AVG_CCL_lastUIP)<<endl);
65   
66   
67    toSTDOUT(endl);
68    toSTDOUT("FormulaCache stats:"<<endl);
69    toSTDOUT("memUse:\t\t\t"<<rAda.get(FCACHE_MEMUSE) <<endl);   
70    toSTDOUT("cached:\t\t\t"<<rAda.get(FCACHE_CACHEDCOMPS)<<endl);
71    toSTDOUT("used Buckets:\t\t"<<rAda.get(FCACHE_USEDBUCKETS)<<endl);
72    toSTDOUT("cache retrievals:\t"<<rAda.get(FCACHE_RETRIEVALS)<<endl);
73    toSTDOUT("cache tries:\t\t"<<rAda.get(FCACHE_INCLUDETRIES)<<endl);
74   
75    toSTDOUT("\n\nZeit: "<<rAda.elapsedTime<<"s\n\n"); 
76   
77}
78
79void finalcSATEvaluationfor_vis()
80{
81  const AnalyzerData &rAda = theRunAn.getData(); 
82  char* buf=rAda.printNumSatAss_vis();
83  char time[50];
84  sprintf(time,"%f",rAda.elapsedTime);
85  strcat(buf," [Time=");strcat(buf,time);
86  strcat(buf,"s]");
87  fprintf(stdout,"%s",buf);
88  free(buf); 
89 
90}
91int main(int argc, char *argv[])
92{ 
93 char *s;
94 char dataFile[1024];
95 memset(dataFile,0,1024);
96 strcpy(dataFile,"data.txt"); 
97 bool fileout = false;
98 
99 CSolverConf::analyzeConflicts = true;
100 CSolverConf::doNonChronBackTracking = true;
101 
102 CSolverConf::count = true;
103 
104 //toSTDOUT ("sharpSAT v1.1, July 1st, 2006"<<endl);
105 //toSTDOUT ("copyright 2006, Humboldt UniversitÀt zu Berlin"<<endl);
106 
107 if (argc <= 1){
108   
109  cout << "Usage: sharpSAT [options] [CNF_File]"<<endl;
110  cout << "Options: "<<endl;
111  cout << "\t -noPP  \t turn off preprocessing"<<endl;
112  cout << "\t -noCA  \t no conflict analysis nor -clauses"<<endl;
113  cout << "\t -noNCB \t turn off nonchronological backtracking"<<endl;
114  cout << "\t -q     \t quiet mode"<<endl;
115  cout << "\t -t [s] \t set time bound to s seconds"<<endl;
116  cout << "\t -noCC  \t turn off component caching"<<endl;
117  cout << "\t -cs [n]\t set max cache size to n MB"<<endl;
118  cout << "\t -noIBCP\t turn off implicit BCP"<<endl;
119  cout << "\t"<<endl;
120 
121  return -1;
122 }   
123
124 for(int i = 1; i < argc; i++)
125 {
126   if(strcmp(argv[i],"-noNCB") == 0) CSolverConf::doNonChronBackTracking = false;
127   if(strcmp(argv[i],"-noCC") == 0) CSolverConf::allowComponentCaching = false;   
128   if(strcmp(argv[i],"-noIBCP") == 0) CSolverConf::allowImplicitBCP = false;
129   if(strcmp(argv[i],"-noPP") == 0) CSolverConf::allowPreProcessing = false;
130   if(strcmp(argv[i],"-nocount") == 0) CSolverConf::count = false;
131
132   else if(strcmp(argv[i],"-noCA") == 0)
133   { 
134     CSolverConf::analyzeConflicts = false;     
135   }   
136   else if(strcmp(argv[i],"-q") == 0) CSolverConf::quietMode = true;   
137   else if(strcmp(argv[i],"-FrA") == 0)
138   {
139      memset(dataFile,0,1024);
140      fileout = true;
141      if(argc <= i+1){ toSTDOUT("wrong parameters"<<endl); return -1;}
142      strcpy(dataFile,argv[i+1]); 
143   }
144   else if(strcmp(argv[i],"-t") == 0)
145   {
146      if(argc <= i+1){ toSTDOUT("wrong parameters"<<endl); return -1;}
147      CSolverConf::secsTimeBound = atoi(argv[i+1]);
148      toSTDOUT("time bound:" <<CSolverConf::secsTimeBound<<"s\n");
149      theSolver.setTimeBound(CSolverConf::secsTimeBound);
150   }         
151   else if(strcmp(argv[i],"-cs") == 0)
152   {
153      if(argc <= i+1){toSTDOUT("wrong parameters"<<endl); return -1;}
154      CSolverConf::maxCacheSize = atoi(argv[i+1])*1024*1024;   
155      //cout <<"maxCacheSize:" <<CSolverConf::maxCacheSize<<"bytes\n";   
156   }     
157   else s = argv[i];   
158 }
159
160 toSTDOUT("cachesize Max:\t"<<CSolverConf::maxCacheSize/1024 << " kbytes"<<endl);   
161 
162 // first: delete all data in the output
163 if(fileout) theRunAn.getData().writeToFile(dataFile); 
164 
165 theRunAn = CRunAnalyzer(); 
166 
167 theSolver.solve(s);
168 
169 theRunAn.finishcountSATAnalysis();
170 finalcSATEvaluationfor_vis();
171 if(fileout) theRunAn.getData().writeToFile(dataFile);
172 return 0;
173}
Note: See TracBrowser for help on using the repository browser.