Added progress bar on verbose mode

NicolaDes · Feb 3, 2018 · ba054b1 · ba054b1
1 parent 60e6f92
commit ba054b1
Show file tree

Hide file tree

Showing 4 changed files with 38 additions and 6 deletions.
diff --git a/include/Solver.hh b/include/Solver.hh
@@ -103,6 +103,8 @@ class Solver{
 		int nPropagations=0; //!< number of propagations
 		int nDecisions=0; //!< number of decisions
 
+		int best_var;
+
 		std::vector<btree<Clause>> prove; //!< Structure to get the counterexample
 
 
@@ -127,6 +129,7 @@ class Solver{
 
 		//!< Decay activities
 		float* activity;
+		float percentage;
 
 
 		/**
@@ -161,6 +164,8 @@ bool canBeSAT();
 
 #endif
 
+		void reset_scores();
+
 		/**
 		 * Select new variable
 		 */

diff --git a/lib/CommandLineInterface.hh b/lib/CommandLineInterface.hh
@@ -106,6 +106,7 @@ namespace tabular{
 			node<Clause>* curr=prove.begin();
 			while(!prove.ended(curr)){
 				std::cout<<curr->left->key_value<<"&"<<curr->right->key_value<<"="<<curr->key_value<<"\n";
+//				if(curr->key_value.size()>0) break;
 				curr=curr->next();
 			}
 		}
@@ -136,6 +137,7 @@ namespace tabular{
 			while(!prove.ended(curr)){
 				fout<<"\""<<curr->left->key_value<<"\" -> "<<"\""<<curr->key_value<<"\";\n";
 				fout<<"\""<<curr->right->key_value<<"\" -> "<<"\""<<curr->key_value<<"\";\n";
+//				if(curr->key_value.size()>0) break;
 				curr=curr->next();
 			}
 		}

diff --git a/release/SATIVA.cc b/release/SATIVA.cc
@@ -20,6 +20,10 @@ void launchOnPig(Solver* solver);
 
 int main(int argc, char** argv){
 
+
+#if VERBOSE
+	system("setterm -cursor off");
+#endif
 	for(int i=1; i<argc;++i){
 		if(argv[i][0]=='-'){
 			if(argv[i][1]=='f') options.filename=argv[i+1];
@@ -35,7 +39,9 @@ int main(int argc, char** argv){
 		launchOnPig(&solver);
 	}else
 		printUsage(argv);
-
+#if VERBOSE
+	system("setterm -cursor on");
+#endif
 	return 0;
 }
 

diff --git a/src/Solver.cc b/src/Solver.cc
@@ -1,6 +1,7 @@
 #include "Solver.hh"
 
 void Solver::init(int nL, int nC){
+	percentage=0.0;
 	watches= new std::vector<Watcher>[(2*nL)+1];
 	watches=watches+nL;
 	reason= new Clause[(2*nL)+1];
@@ -287,10 +288,26 @@ Literal Solver::select(){
 	return branch_variable;
 };
 
+void Solver::reset_scores(){
+	for(int i=-nLiterals;i<nLiterals;++i){
+		activity[i]=0;
+	}
+};
+
 bool Solver::CDCL(){
 	while(true){
+#if VERBOSE
+		printf("[");
+		int i=0;	
+		for(;i<=(int)((percentage*4)*41);++i)printf("=");
+		printf(">");
+		for(;i<=41;++i)printf(" ");
+		printf("%3d%%]\r",(int)((percentage*4)*100));
+#endif
 		Clause* conflict=propagate();
 		if(conflict!=nullptr){ //!< Exist a conflict
+#if VERBOSE
+#endif
 			nConflicts++;
 			std::vector<Literal> to_learn;int btLevel;
 			if(decisionLevel()==root_level){	
@@ -301,12 +318,17 @@ bool Solver::CDCL(){
 			btLevel=analyze(conflict, to_learn);
 			backtrack(btLevel);
 			record(to_learn);
-			decayActivity();
 		}else{
 #if ASSERT
 			assert(canBeSAT());
 #endif
-			if(decisionLevel()==0) simplify();
+			if(decisionLevel()==0){
+				simplify();
+				decayActivity();
+#if VERBOSE
+				percentage=((float)nAssigns())/((float)nLiterals);
+#endif
+			}
 			if(learnts.size()-nAssigns()>=learnts.size()) reduceLearnts();
 			if(nAssigns()==nLiterals) return true;
 			else if(nConflicts>max_conflict) {
@@ -335,9 +357,6 @@ void Solver::simplify(){
 			x->del();
 		}
 	}
-#if VERBOSE
-	if(deletedClauses-tmp>0) std::cout<<"Deleted clauses: "<<deletedClauses-tmp<<", limits: "<<max_conflict<<"\n";
-#endif
 };
 
 void Solver::reduceLearnts(){};