/*******************************************************************************
 * Copyright (c) 2016 CEA LIST.
 *
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 *  Arnault Lapitre (CEA LIST) arnault.lapitre@cea.fr
 *   - Initial API and implementation
 ******************************************************************************/
#include "SatSolver.h"


#include <util/avm_vfs.h>

#include <fml/expression/ExpressionConstant.h>
#include <fml/expression/ExpressionConstructor.h>
#include <fml/expression/ExpressionFactory.h>

#include <fml/workflow/WObject.h>


namespace sep
{

class Configuration;


bool SatSolver::configure(
		Configuration & aConfiguration, WObject * wfFilterObject,
		ListOfPairMachineData & listOfSelectedVariable)
{
	mListOfSelectedVariable = listOfSelectedVariable;

	if( mListOfSelectedVariable.empty() )
	{
		AVM_OS_WARNING_ALERT
				<< "Unexpected in SatSolver "
					"an empty selected variable list !!!"
				<< SEND_ALERT;

		return( true );
	}


AVM_IF_DEBUG_FLAG2( CONFIGURING , SOLVING )
	AVM_OS_TRACE << std::endl
			<< "Listes des variables utilisées pour la redondance" << std::endl;

	std::size_t varCount = 0;
	ListOfInstanceOfData::const_iterator itVar;
	ListOfInstanceOfData::const_iterator endVar;

	ListOfPairMachineData::const_iterator itPairMachineData =
			mListOfSelectedVariable.begin();
	ListOfPairMachineData::const_iterator endPairMachineData =
			mListOfSelectedVariable.end();
	for( ; itPairMachineData != endPairMachineData ; ++itPairMachineData )
	{
		AVM_OS_TRACE << "\t" << "Machine:> "
				<< (*itPairMachineData).first().getFullyQualifiedNameID() << std::endl;

		if( (*itPairMachineData).second().nonempty() )
		{
			itVar = (*itPairMachineData).second().begin();
			endVar = (*itPairMachineData).second().end();
			for( ; itVar != endVar ; ++itVar , ++varCount )
			{
				AVM_OS_TRACE << "\t\t" << str_header( *itVar ) << std::endl;
			}
		}
	}

	AVM_OS_TRACE << "Total:> " << varCount << std::endl << std::endl;
AVM_ENDIF_DEBUG_FLAG2( CONFIGURING , SOLVING )


	mLogFolderLocation = VFS::ProjectDebugPath;

	return( true );
}


/**
 * SOLVER
 * an empty << dataVector >> compute by the solver
 * an empty << valuesVector >> compute by the solver
 */
bool SatSolver::solve(const BF & aCondition,
		BFVector & dataVector, BFVector & valuesVector)
{
	BF fullCondition = completeUsingDataTypeConstraint(aCondition, dataVector);

AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SOLVING )
	AVM_OS_TRACE << "SatSolver::solve(...) :>" << std::endl
			<< "\tcondition:> " << aCondition.str() << std::endl
			<< "\tfull cond:> " << fullCondition.str() << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SOLVING )

	if( fullCondition.isEqualTrue() )
	{
		return( true );
	}
	else if( fullCondition.isEqualFalse() )
	{
		return( false );
	}

	return( solveImpl(fullCondition, dataVector, valuesVector) );
}


BF SatSolver::completeUsingDataTypeConstraint(
		const BF & aCondition, BFVector & dataVector) const
{
	BF allCondition = aCondition;
	BF typeConstraint;

	BFVector paramsVector( dataVector );
	ExpressionFactory::collectVariable(aCondition, paramsVector);

	BFVector::raw_iterator< InstanceOfData > itParam = paramsVector.begin();
	BFVector::raw_iterator< InstanceOfData > endParam = paramsVector.end();
	for( ; itParam != endParam ; ++itParam )
	{
		typeConstraint = (itParam)->getTypeSpecifier()->genConstraint( *itParam );

AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SOLVING )
		AVM_OS_TRACE << "completeUsingDataTypeConstraint:> "
				<< str_header( *itParam ) << std::endl
				<< "\tconstraint:> " << typeConstraint.str() << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SOLVING )

		if( typeConstraint.isEqualFalse() )
		{
			return( ExpressionConstant::BOOLEAN_FALSE );
		}
		else if( typeConstraint.isNotEqualTrue() )
		{
			allCondition = ExpressionConstructor::andExpr(
					allCondition, typeConstraint);
		}
	}

	return( allCondition );
}


}