Update for FASPGRN

-Allow for specifying —use to find only k-answer sets
-Disable min check and SCC for finite valued answer sets

ASPEval.cpp

@@ -33,6 +33,7 @@
 
 bool ASPEval::processAS(std::string asline, bool check)
 {
+	//std::cout<<"Process AS = "<<asline<<std::endl;
 	bool found = false;
 	std::map<AtomPtr, int> acc;
 	std::map<AtomPtr, int>::iterator acc_it;
@@ -72,7 +73,7 @@ bool ASPEval::processAS(std::string asline, bool check)
 		}
 
 		AtomPtr atom(new Atom(args, false));
-
+		//std::cout<<"Atom="<<atomv[sz-1]<<std::endl;
 
 		int a = boost::lexical_cast<int> (atomv[sz-1]);
 
@@ -97,7 +98,9 @@ bool ASPEval::processAS(std::string asline, bool check)
 		if(acc_it == acc.end() || acc[os.str()] < a)
 				acc[os.str()] = a;
 		*/
-	}
+	} // End for
+
+	//std::cout<<"created "<<acc.size()<<" atoms"<<endl;
 
 	/*
 	std::ostringstream os;
@@ -132,12 +135,14 @@ bool ASPEval::processAS(std::string asline, bool check)
 		{
 			fas.push_back(curr_as);
 			strAS.insert(curr_as.getStr());
+			//std::cout<<"strAS.size() = "<<strAS.size() <<endl;
 			found = true;
+			//std::cout<<"No Check!"<<std::endl;
 		}
 		else		// Check minimality
 		{
 			MinCheck* mc;
-
+			//std::cout<<"Min-Checking..."<<endl; //<<curr_as<<endl;
 			mc = new MIPMinCheck(program, curr_as);
 			if(mc->isMinimal())		// Found
 			{
@@ -161,12 +166,12 @@ bool ASPEval::doSolve()
 	//int k = std::max(step, 2);	// start search from k=2
 	bool found = false;
 
-	//std::cout<<"doSolve(): "<<std::endl;
+	std::cout<<"doSolve(): "<<std::endl;
 	//std::cout<<program<<std::endl;
 	do
 	{
 
-		//std::cout<<"k="<<curr_k<<std::endl;
+		std::cout<<"k="<<curr_k<<std::endl;
 		ASPTranslate* tr;
 
 		try
@@ -187,6 +192,7 @@ bool ASPEval::doSolve()
 		{
 			//std::cout<<"Translated program "<<std::endl;
 			//std::cout<<tr->getProgram()<<std::endl;
+			//std::cout<<"Calling solver..."<<std::endl;
 			solver->callSolver(tr->getProgram(), curr_k, maxtime-dur);
 		}
 		catch(GeneralError& e)
@@ -199,14 +205,18 @@ bool ASPEval::doSolve()
 		{
 
 			//fas.clear();
-			std::vector<std::string> aslines = solver->getlines();
+
+			std::string asline = solver->getNextLine();
 			//std::cout<<"Found "<<aslines.size()<<std::endl;
-			for(std::vector<std::string>::iterator it=aslines.begin();
-					it!=aslines.end(); ++it)
-			{
-				bool curfound = processAS(*it, tr->needMinCheck());
-				found = found || curfound;
-			}
+			//int i=0;
+			//for(std::vector<std::string>::iterator it=aslines.begin();
+			//		it!=aslines.end(); ++it)
+			//{
+				//cout<<i<<endl;
+				//cout<<"Processing "<<asline<<endl;
+				found = processAS(asline, tr->needMinCheck());
+				//found = found || curfound;
+			//}
 
 		}
 
@@ -223,6 +233,7 @@ bool ASPEval::doSolve()
 bool ASPEval::answersetsLeft()
 {
 	//std::cout<<"as_idx = "<<as_idx<<", fas = "<<fas.size()<<std::endl;
+	//std::cout<<"curr_k = "<<curr_k<<endl;
 	if(as_idx < fas.size())
 		return true;
 	else if(curr_k <= stop.first)

ASPSolver.h

@@ -80,9 +80,11 @@ class ASPSolver
 
                 virtual bool answerSetsLeft() const = 0;
 
-                std::vector<std::string> getlines() const
+                std::string getNextLine()
 				{
-					return aslines;
+					std::string result = currline;
+					getNextAnswerSet();
+					return result;
 				}
 
         protected:
@@ -104,8 +106,8 @@ class ASPSolver
 
                 //AtomSet currentAnswer;
 
-                std::vector<std::string> aslines;
-
+                // std::vector<std::string> aslines;
+                std::string currline;
                 /* Is there any answers left */
                 bool answersetsleft;
 

ASPTranslate.h

@@ -88,6 +88,7 @@ class ASPTranslate
 
 		// Compute all non-SRCF Atoms
 		getNonSRCFAtoms();
+
 		if(nonSRCFAtoms.size()>0 && anydisj)
 			needmincheck = true;
 		// Do shift for disj rules with SRCF atoms

CLSolver.cpp

@@ -46,13 +46,13 @@ CLSolver::CLSolver(std::set<std::string> filter, bool co)
         lpargs.push_back("-W");
         lpargs.push_back("no-atom-undefined");
         lpargs.push_back("-W");
-        lpargs.push_back("no-define-cyclic");
+        lpargs.push_back("no-file-included");
         lpargs.push_back("-W");
-        lpargs.push_back("no-define-redfinition");
+        lpargs.push_back("no-operation-undefined");
         lpargs.push_back("-W");
-        lpargs.push_back("no-nonmonotone-aggregate");
+        lpargs.push_back("no-variable-unbounded");
         lpargs.push_back("-W");
-        lpargs.push_back("no-term-undefined");
+        lpargs.push_back("no-global-variable");
         lpargs.push_back("dummy");
 
         /*
@@ -95,7 +95,7 @@ void CLSolver::callSolver(std::string program, int k, int time_limit)
 {
 
         int retcode = 0;
-        aslines.clear();
+        //aslines.clear();
         if(pb->isOpen())
                 retcode = pb->close();
 
@@ -149,11 +149,12 @@ void CLSolver::callSolver(std::string program, int k, int time_limit)
 				std::string sat("SATISFIABLE");
 				std::string unsat("UNSATISFIABLE");
 				std::string timelimit("*** Info : (clingo): INTERRUPTED by signal!");
-				std::getline(iopipe, outputline);
+				std::getline(iopipe, outputline, '\n');
 				if(outputline!=sat && outputline != unsat && outputline!=timelimit )
 				{
-					aslines.push_back(outputline);
+					currline = outputline;
 					//std::cout<<outputline<<std::endl;
+					/*
 					try
 					{
 						while(std::getline(iopipe, outputline))
@@ -171,19 +172,22 @@ void CLSolver::callSolver(std::string program, int k, int time_limit)
 						ostr<<e.what()<<std::endl;
 						throw FatalError(ostr.str());
 					}
+					*/
 					answersetsleft = true;
 				}
 				else
 				{
+					/*
 					 if(outputline == sat)
 						 answersetsleft = true;
 					 else
+					 */
 						 answersetsleft = false;
 				}
 
 			}
 
-			retcode = pb->close();
+			//retcode = pb->close();
 
         }
         catch(FatalError& e)
@@ -307,8 +311,9 @@ void CLSolver::getNextAnswerSet()
                 resultParser->parseLine(outputline);
                 currentAnswer = resultParser->getAnswerSet();
 				*/
-				std::cout<<outputline<<std::endl;
-                answersetsleft = true;
+				//std::cout<<outputline<<std::endl;
+			currline = outputline;
+            answersetsleft = true;
         }
         else
                 answersetsleft = false;

Globals.cpp

@@ -35,8 +35,8 @@
 #include <boost/algorithm/string/trim.hpp>
 #include "Globals.h"
 
-#define MAXDENOM 10
-#define MAXK 10
+#define MAXDENOM 100
+#define MAXK 100
 #define MAXT 600
 #define REP 0
 
@@ -54,8 +54,11 @@ Globals::Globals()
         intOpt["maxk"] = MAXK;
         intOpt["maxt"] = MAXT;
         intOpt["rp"] = REP;
+        intOpt["usek"] = 0;
+        boolOpt["fin"] = false;
         boolOpt["check"] = false;
         boolOpt["help"] = false;
+        boolOpt["noscc"] = false;
 
         //strOpt["DLVArgs"] = "-silent --";
 }
@@ -87,8 +90,12 @@ void Globals::processArgs(GetPot cl)
 
         int trans_k = cl("--trans", 0);
 
+        int use_k = cl("--usek", 0);
+
         const bool checkOnly = cl.options_contain("-c") || cl.search("--check");
         const bool help = cl.options_contain("-h") || cl.search("--help");
+        const bool noscc = cl.options_contain("-s") || cl.search("--noscc");
+        const bool finas = cl.options_contain("-f") || cl.search("--usek");
 
         int rep = cl("--rnd", REP);
         if(rep>0)
@@ -108,6 +115,9 @@ void Globals::processArgs(GetPot cl)
         boolOpt["check"] = checkOnly;
         intOpt["rp"] = rep;
         boolOpt["help"] = help;
+        boolOpt["noscc"] = noscc;
+
+        boolOpt["fin"] = finas;
 
         /* Determine the input file */
 

GraphProcessor.cpp

@@ -31,6 +31,7 @@
 
 GraphProcessor::GraphProcessor(DependencyGraph* dg)//, ASPSolverEngine* se)//, Eval* eval, int k)
 //	:solver_engine(se)//, ev(eval), step(k)
+:found(false)
 {
 	components = dg->getComponents();
 
@@ -91,11 +92,12 @@ void GraphProcessor::eval(unsigned idx)
 	currentComp = currentComp + input.getFacts();
 
 	// Decide what evaluation method we should call
-	/*
-	std::cout<<"Evaluating component "<<idx<<": " << std::endl;
-	std::cout<<currentComp<<std::endl;
-	std::cout <<"with input "<< std::endl << input << std::endl;
-	*/
+
+
+	//std::cout<<"Evaluating component "<<idx<<": " << std::endl;
+	//std::cout<<currentComp<<std::endl;
+	//std::cout <<"with input "<< std::endl << input << std::endl;
+
 
 	FAnswerSet currentAS;
 
@@ -113,16 +115,17 @@ void GraphProcessor::eval(unsigned idx)
 	//bool needcheck = !components[idx]->isSRCF() && components[idx]->isDisjunctive();
 	evaluator  = new ASPEval(eng, currentComp, stop, step, step);
 
-	bool found = false;
-	while(evaluator->answersetsLeft() && !found)
+	//found = false;
+	while(!found && evaluator->answersetsLeft())
 	{
 		if(idx == numComp-1)
 		{
 			// Last component to be evaluated
 			// Just stream it out
 			// std::cout<<"Reached last component, streaming answer set: "<<std::endl;
 			currentAS = evaluator->getNextAnswerSet();
-			std::cout<<currentAS.getStrClean()<<std::endl;
+			//std::cout<<currentAS.getStrClean()<<std::endl;
+			std::cout<<"<<Consistent>>"<<std::endl;
 			found = true;
 		}
 		else
@@ -135,7 +138,7 @@ void GraphProcessor::eval(unsigned idx)
 		}
 	}
 
-	delete evaluator;
+	//delete evaluator;
 
 }
 

GraphProcessor.h

@@ -66,6 +66,7 @@ class GraphProcessor
 		std::vector<Component*> components;
 		std::vector<Program> compPrograms;
 		int numComp;
+		bool found;
 
 		/* Initial input EDB */
 

MIPMinCheck.cpp

@@ -15,10 +15,13 @@ void MIPMinCheck::writeMPS()
 	glp_set_prob_name(lp, "chekmin");
 	glp_set_obj_dir(lp, GLP_MIN);
 
+
 	// Size of the matrix
 	int nCols = mipreg.colVars.size();
 	int nRows = mipreg.rowVars.size();
 
+	//std::cout<<"MIP size = "<<nCols<<"x"<<nRows<<std::endl;
+
 	// Adding columns
 	glp_add_cols(lp, nCols);
 	int i,j,counter;
@@ -118,13 +121,17 @@ bool MIPMinCheck::callMIP()
 	// Pass the solver with the problem to be solved to CbcModel
 	CbcModel model(solver1);
 
+
 	model.setLogLevel(0);
 	// Do complete search
+	//cout<<"solveMIP"<<endl;
 	model.branchAndBound();
+	//cout<<"Done!"<<endl;
 
 	double z = model.getObjValue();
 
 	return (target-z) < EPS;
+	//return true;
 	//std::cout<<"Target = "<<target<<" Obj = "<<z<<std::endl;
 }
 

MIPRegistry.h

@@ -541,7 +541,7 @@ class MIPRegistry
 				// If current lower bound of v_a < c, then change it to c;
 				AtomPtr atomc = bl[0]->getAtom();
 				Rational c = atomc->getRat();
-				if(colVars[idxva].lb < c)
+				if(colVars[idxva].lb < c && colVars[idxva].ub >= c)
 					colVars[idxva].lb = c;
 			}
 			// Check for #c <- a
@@ -554,7 +554,7 @@ class MIPRegistry
 				// If current upper bound for v_a is > c, then change it to c;
 				AtomPtr atomc = hl[0];
 				Rational c = atomc->getRat();
-				if(colVars[idxva].ub > c)
+				if(colVars[idxva].ub > c && colVars[idxva].lb <= c)
 					colVars[idxva].ub = c;
 			}
 			// Check for a <- b and a <- not b
@@ -571,7 +571,7 @@ class MIPRegistry
 				if(bl[0]->isNAF())
 				{
 					Rational asb = as[b];
-					if(colVars[idxva].lb < asb)
+					if(colVars[idxva].lb < asb && colVars[idxva].ub >= asb)
 						colVars[idxva].lb = asb;
 				}
 				else
@@ -702,7 +702,9 @@ class MIPRegistry
 			AtomPtr a = it->first;
 			Rational v = it->second;
 			int idxva = colsAtom[atommap[a]];
-			if(colVars[idxva].ub > v)
+			//if(colVars[idxva].name == "v0")
+				//std::cout<<"update column bounds "<<colVars[idxva].ub<<" with "<<v<<endl;
+			if(colVars[idxva].ub > v && colVars[idxva].lb <= v)
 				colVars[idxva].ub = v;
 		}