[dlvhex-notify] SF.net SVN: dlvhex:[3554] dlvhex/branches/dlvhex-refactoring/src/dlvhex/ ClaspSolver.cpp

[<chr...@us...>]

Revision: 3554
          http://dlvhex.svn.sourceforge.net/dlvhex/?rev=3554&view=rev
Author:   chrisr86
Date:     2012-02-17 22:38:19 +0000 (Fri, 17 Feb 2012)
Log Message:
-----------


Modified Paths:
--------------
    dlvhex/branches/dlvhex-refactoring/src/dlvhex/ClaspSolver.cpp

Modified: dlvhex/branches/dlvhex-refactoring/src/dlvhex/ClaspSolver.cpp
===================================================================
--- dlvhex/branches/dlvhex-refactoring/src/dlvhex/ClaspSolver.cpp	2012-02-17 21:10:04 UTC (rev 3553)
+++ dlvhex/branches/dlvhex-refactoring/src/dlvhex/ClaspSolver.cpp	2012-02-17 22:38:19 UTC (rev 3554)
@@ -185,6 +185,13 @@
 
 bool ClaspSolver::ExternalPropagator::propagate(Clasp::Solver& s){
 
+/*
+	Nogood ng;
+	ng.insert(ID(ID::MAINKIND_LITERAL | ID::SUBKIND_ATOM_ORDINARYG, 0));
+	ng.insert(ID(ID::MAINKIND_LITERAL | ID::SUBKIND_ATOM_ORDINARYG, 2));
+	cs.addNogoodToClasp(ng);
+*/
+
 	if (cs.learner.size() != 0){
 
 		DBGLOG(DBG, "Translating clasp assignment to HEX-interpretation");
@@ -226,20 +233,10 @@
 	DBGLOG(DBG, "Result: " << (inconsistent ? "" : "not ") << "inconsistent");
 
 	return !inconsistent;
-
-
-/*
-	Nogood ng;
-	ng.insert(ID(ID::MAINKIND_LITERAL | ID::SUBKIND_ATOM_ORDINARYG, 0));
-	ng.insert(ID(ID::MAINKIND_LITERAL | ID::SUBKIND_ATOM_ORDINARYG, 2));
-	return addNogoodToSolver(cg, ng);
-*/
 }
 
 bool ClaspSolver::addNogoodToClasp(Nogood& ng){
 
-	//claspInstance.enableUpdateShortImplications(false);
-
 #ifndef NDEBUG
 	std::stringstream ss;
 	ss << "{ ";
@@ -269,6 +266,7 @@
 	ss << " }";
 	clauseCreator->end();
 
+	//std::cout << claspInstance.numTernary() << ", " << claspInstance.numBinary() << ", " << claspInstance.numLearntShort() << std::endl;
 	/*
 	if (claspInstance.master()->numLearntConstraints() > 0){
 		Clasp::LitVec lv;
@@ -544,10 +542,31 @@
 	return initiallyInconsistent;
 }
 
+/*
+class MyDistributor : public Clasp::Distributor{
+public:
+	uint32 receive(const Clasp::Solver& in, Clasp::SharedLiterals** out, uint32 maxOut){
+		std::cout << "Distributing learned knowledge" << std::endl;
+	}
+
+	MyDistributor() : Clasp::Distributor(2, 3, 32){
+	}
+
+protected:
+	void doPublish(const Clasp::Solver& source, Clasp::SharedLiterals* lits){
+		std::cout << "Distributing learned knowledge" << std::endl;
+	}
+};
+*/
+
 ClaspSolver::ClaspSolver(ProgramCtx& c, OrdinaryASPProgram& p) : ctx(c), program(p), sem_request(0), sem_answer(0), modelRequest(false), terminationRequest(false), endOfModels(false), translatedNogoods(0){
 
 	reg = ctx.registry();
 
+//claspInstance.enableUpdateShortImplications(false);
+//claspInstance.enableConstraintSharing();
+//claspInstance.enableLearntSharing(new MyDistributor());
+
 	clauseCreator = new Clasp::ClauseCreator(claspInstance.master());
 	bool initiallyInconsistent = sendProgramToClasp(p);
 	DBGLOG(DBG, "Initially inconsistent: " << initiallyInconsistent);

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.