Everything working

~ Corrected boundcond
+ Temporary solution to a problem in prefSAT

Debug/test-input/scc1.dl

@@ -0,0 +1,4 @@
+arg(a13).
+arg(a14).
+att(a13,a14).
+att(a14,a13).

src/AF.cpp

@@ -125,17 +125,14 @@ Argument *AF::getArgumentByNumber(int num)
  */
 void AF::restrictTo( SetArguments* theSet, AF* dst )
 {
-	// Gereate G restricted to I
-	SetArguments* A = dst->get_arguments();
-
 	// Create disjointed copies of the Arguments
-	for ( SetArgumentsIterator it = get_arguments()->begin();
-			it != get_arguments()->end(); ++it )
+	for ( SetArgumentsIterator it = this->begin(); it != this->end(); ++it )
 		if ( theSet->exists( *it ) )
 			dst->get_arguments()->add_Argument(
 				new Argument
 				(
 					(*it)->getName(),
+					//(*it)->getNumber(),
 					dst->numArgs(),
 					dst
 				) );

src/Preferred.h

@@ -17,6 +17,7 @@
 #include "SATFormulae.h"
 #include <iostream>
 #include <sstream>
+#include <stdexcept>
 
 using namespace std;
 

src/Preferred_boundcond.cpp

@@ -77,13 +77,63 @@ void Preferred::boundcond( SetArguments* aSCC, SetArguments* e,
 	if ( debug )
 		cerr << "\t\tNodes not satisfying the first condition: " << toBeRemoved << endl;
 
-	// Remove from the set the nodes satisfying both the conditions:
+	// Remove from the set the nodes attacked by nodes satisfying both the conditions:
 	// 	- node in G \ ( S[ i ] U e )
 	// 	- node attacked by e
-	external.setminus( e, &external );
+	//external.setminus( e, &external );
 	for ( SetArgumentsIterator it = toBeRemoved.begin(); it != toBeRemoved.end(); ++it )
 	{
-		if ( external.exists( *it ) )
+		SetArguments attackers = SetArguments();
+		// Find the external attackers (could be done the opposite way, maybe faster)
+		for ( SetArgumentsIterator jt = external.begin(); jt != external.end(); ++jt )
+			if ( (*jt)->get_attacks()->exists( *it ) )
+				attackers.add_Argument( *jt );
+
+		// Check that no attackers are in e
+		int nAttackers = attackers.cardinality();
+		attackers.setminus( e, &attackers );
+		if ( attackers.cardinality() < nAttackers )
+		{
+			if ( debug )
+				cerr << "\t\t" << (*it)->getName() << " attacked by e.\n";
+
+			continue;
+		}
+
+		// Check that every attacker is itself attacked by e
+		bool safe = true;
+		for ( SetArgumentsIterator jt = attackers.begin(); jt != attackers.end(); ++jt )
+		{
+			bool attacked = false;
+			for ( SetArgumentsIterator kt = e->begin(); kt != e->end(); ++kt )
+			{
+				attacked = (*kt)->get_attacks()->exists( *jt );
+				if ( attacked )
+					break;
+			}
+
+//			safe &= attacked;
+//			if ( !safe )
+//				break;
+			if ( !attacked )
+			{
+				safe = false;
+				break;
+			}
+		}
+
+		if ( safe )
+		{
+			if ( debug )
+				cerr << "\t\t" << (*it)->getName() << "'s attackers are attacked by e.\n";
+
+			toBeKept.add_Argument( *it );
+		}
+		else if ( debug )
+			cerr << "\t\tNot every attacker of " << (*it)->getName() << " is attacked by e.\n";
+
+		/*
+		if ( !attackers.empty() )
 		{
 			bool attacked = false;
 			for ( SetArgumentsIterator jt = e->begin(); jt != e->end(); ++jt )
@@ -107,6 +157,7 @@ void Preferred::boundcond( SetArguments* aSCC, SetArguments* e,
 		}
 		else if ( debug )
 			cerr << "\t\t" << (*it)->getName() << " is not external.\n";
+		*/
 	}
 
 	// Readd the nodes to I

src/Preferred_pref.cpp

@@ -82,6 +82,7 @@ void Preferred::pref( AF* theAF, SetArguments* theC )
 	for ( list<SetArguments*>::iterator aSCC = S.begin(); aSCC != S.end(); ++aSCC )
 	{
 		Preferred p = Preferred();
+		vector<Labelling> newLabellings = vector<Labelling>();
 
 		for ( vector<Labelling>::iterator aLabelling = this->labellings.begin();
 				aLabelling != this->labellings.end(); ++aLabelling )
@@ -101,8 +102,28 @@ void Preferred::pref( AF* theAF, SetArguments* theC )
 
 				AF restricted = AF();
 				this->af->restrictTo( *aSCC, &restricted );
-				// Should be G restricted to S[ i ] and I intersect C
-				// And done iff I != Ø (doesn't prefSAT return Ø otherwise..?)
+
+				// TODO: prefSAT problem: the nodes in I are different from
+				// the nodes in the restricted AF.
+				// Temporary solution: rebuild I.
+				for ( SetArgumentsIterator it = restricted.begin(); it != restricted.end(); ++it )
+				{
+					try
+					{
+						Argument* victim = I.getArgumentByName( (*it)->getName() );
+
+						// No exception: the Argument is inside I
+						// Remove it and substitute it with the new one
+						I.remove( victim );
+						I.add_Argument( *it );
+					}
+					catch ( const std::out_of_range& oor )
+					{
+						// The Argument is outside of I. Nothing to do.
+					}
+				}
+
+				// Should be done iff I != Ø (doesn't prefSAT return Ø otherwise..?)
 				p.prefSAT( &restricted, &I );
 			}
 			else
@@ -114,7 +135,8 @@ void Preferred::pref( AF* theAF, SetArguments* theC )
 				(*aSCC)->setminus( &O, &restriction );
 				AF restricted = AF();
 				this->af->restrictTo( &restriction, &restricted );
-				// Should be G restricted to S[ i ] \ O and I intersect C
+				// TODO? the same as above for prefSAT.
+
 				p.pref( &restricted, &I );
 			}
 
@@ -124,22 +146,27 @@ void Preferred::pref( AF* theAF, SetArguments* theC )
 
 			// Create the new Labellings
 			// by merging the current Labelling with every Labelling found
-			for ( Preferred::iterator EStar = p.begin();
-					EStar != p.end(); ++EStar )
+			for ( Preferred::iterator EStar = p.begin(); EStar != p.end(); ++EStar )
 			{
 				if ( debug )
 					cerr << "\t\tFound " << *((*EStar).inargs()) << endl;
 
+				// TODO: Rebuild the Labelling using the original Arguments
+				// Not doing so could cause problems to next boundconds
+				// Currently not possible due to the structure of Labelling
+
 				(*aLabelling).clone( &(*EStar) );
 
 				if ( debug )
 					cerr << "\t\t\tCreated: " << *((*EStar).inargs()) << endl;
-			}
 
+				// Add it to the labellings found
+				newLabellings.push_back( *EStar );
+			}
 		}
 
 		// The generated Labellings are the new Labellings
-		this->labellings = p.labellings;
+		this->labellings.assign( newLabellings.begin(), newLabellings.end() );
 	}
 }
 

src/main.cpp

@@ -73,22 +73,22 @@ int main(int argc, char *argv[])
 
 //	// First: a1, a6
 //	SetArguments C_set1 = SetArguments();
-//	C_set1.add_Argument(framework.getArgumentByName("a1"));
-//	C_set1.add_Argument(framework.getArgumentByName("a6"));
+//	C_set1.add_Argument(framework.getArgumentByName("a13"));
+//	C_set1.add_Argument(framework.getArgumentByName("a14"));
 //
 //	p.prefSAT(&framework, &C_set1);
 	p.pref( &framework, framework.get_arguments() );
-	int n = 1;
 
+	int n = 1;
 	for (Preferred::iterator it = p.begin(); it != p.end(); it++)
 	{
 		cout << "Extension " << n++ << endl;
-		for (SetArgumentsIterator itarg = (*it).inargs()->begin();
-				itarg != (*it).inargs()->end(); itarg++)
-		{
-			cout << (*itarg)->getName() << endl;
-		}
-		cout << "Or even " << endl;
+//		for (SetArgumentsIterator itarg = (*it).inargs()->begin();
+//				itarg != (*it).inargs()->end(); itarg++)
+//		{
+//			cout << (*itarg)->getName() << endl;
+//		}
+//		cout << "Or even " << endl;
 		cout << *((*it).inargs()) << endl;
 	}