|
From: <chr...@us...> - 2012-02-17 22:38:25
|
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.
|