/*******************************************************************************
 * 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
 *
 * Created on: 7 déc. 2012
 *
 * Contributors:
 *  Arnault Lapitre (CEA LIST) arnault.lapitre@cea.fr
 *   - Initial API and implementation
 ******************************************************************************/

#ifndef SOLVER_BASESMTSOLVER_H_
#define SOLVER_BASESMTSOLVER_H_

#include <solver/api/SatSolver.h>

#include <common/BF.h>

#include <collection/Typedef.h>

#include <fml/executable/InstanceOfData.h>


#define SMT_ARGS_DATA_INITIAL_COUNT      16

#define SMT_ARGS_DATA_ROOT_CAPACITY     512
#define SMT_ARGS_DATA_DEFAULT_CAPACITY   64

#define SMT_ARGS_DATA_INCR_CAPACITY      16


namespace sep
{

class Configuration;


template< class VarDecl_T , class Sort_T , class Expr_T , bool array_else_vector >
class SmtSolverTraits  :  public SatSolver
{

protected:
	/**
	 * ATTRIBUTES
	 **/
	TableOfInstanceOfData  mTableOfParameterInstance;
	Vector< VarDecl_T >    mTableOfParameterDecl;
	Vector< Expr_T    >    mTableOfParameterExpr;

	Vector< VarDecl_T >    mTableOfVariableDecl;
	Vector< Expr_T    >    mTableOfVariableExpr;

	Vector< Expr_T >       mTableOfParameterExprForNewFormula;
	Vector< Expr_T >       mTableOfParameterExprForOldFormula;


public:
	/**
	 * CONSTRUCTOR
	 * Default
	 */
	SmtSolverTraits()
	: SatSolver(),
	mTableOfParameterInstance( ),
	mTableOfParameterDecl( ),
	mTableOfParameterExpr( ),

	mTableOfVariableDecl( ),
	mTableOfVariableExpr( ),

	mTableOfParameterExprForNewFormula( ),
	mTableOfParameterExprForOldFormula( )
	{
		//!!! NOTHING
	}


	/**
	 * DESTRUCTOR
	 */
	virtual ~SmtSolverTraits()
	{
		destroyChecker();
	}


	/**
	 * CREATE - DESTROY
	 * ValidityChecker
	 */
	inline virtual bool destroyChecker()
	{
		resetTable();

		return( true );
	}


	virtual bool resetTable()
	{
		if( mTableOfParameterInstance.nonempty() )
		{
			BFVector::raw_iterator< InstanceOfData > it =
					mTableOfParameterInstance.begin();
			BFVector::raw_iterator< InstanceOfData > itEnd =
					mTableOfParameterInstance.end();
			for( ++it /* ignore sentinel */ ; it != itEnd ; ++it )
			{
				(it)->setMark(0);
			}
			mTableOfParameterInstance.clear();
		}
		mTableOfParameterInstance.append( BF::REF_NULL );

		mTableOfParameterDecl.clear();
		mTableOfParameterExpr.clear();

		mTableOfVariableDecl.clear();
		mTableOfVariableExpr.clear();

		mTableOfParameterExprForNewFormula.clear();
		mTableOfParameterExprForOldFormula.clear();

		return( true );
	}

};


template< class VarDecl_T , class Sort_T , class Expr_T ,
		bool array_else_vector , bool need_type_cst_decl >
class SmtSolver;


template< class VarDecl_T , class Sort_T , class Expr_T , bool array_else_vector >
class SmtSolver< VarDecl_T , Sort_T , Expr_T , array_else_vector , true > :
	public SmtSolverTraits< VarDecl_T , Sort_T , Expr_T , array_else_vector >
{


protected:
	/**
	 * TYPEDEF
	 */
	typedef SmtSolver< VarDecl_T , Sort_T , Expr_T ,
			array_else_vector , true >  base_this_type;


public:
	/**
	* CONSTRUCTOR
	* Default
	*/
	SmtSolver(Sort_T nullSort, Expr_T nullExpr)
	: SmtSolverTraits< VarDecl_T , Sort_T , Expr_T , array_else_vector >( ),

	SMT_TYPE_BOOL( nullSort ),
	SMT_TYPE_NAT ( nullSort ),
	SMT_TYPE_INT ( nullSort ),
	SMT_TYPE_BV32( nullSort ),
	SMT_TYPE_BV64( nullSort ),
	SMT_TYPE_REAL( nullSort ),

	SMT_TYPE_NUMBER( nullSort ),

	SMT_TYPE_STRING( nullSort ),

	SMT_CST_BOOL_TRUE ( nullExpr ),
	SMT_CST_BOOL_FALSE( nullExpr ),

	SMT_CST_INT_ZERO( nullExpr ),
	SMT_CST_INT_ONE ( nullExpr )
	{
		//!!! NOTHING
	}


	/**
	* DESTRUCTOR
	*/
	virtual ~SmtSolver()
	{
		//!!! NOTHING
	}


protected:
	/**
	 * ATTRIBUTES
	 **/
	Sort_T SMT_TYPE_BOOL;
	Sort_T SMT_TYPE_NAT;
	Sort_T SMT_TYPE_INT;
	Sort_T SMT_TYPE_BV32;
	Sort_T SMT_TYPE_BV64;
	Sort_T SMT_TYPE_REAL;

	Sort_T SMT_TYPE_NUMBER;

	Sort_T SMT_TYPE_STRING;

	Expr_T SMT_CST_BOOL_TRUE;
	Expr_T SMT_CST_BOOL_FALSE;

	Expr_T SMT_CST_INT_ZERO;
	Expr_T SMT_CST_INT_ONE;


protected:

	template< class data_t , bool is_array_else_vector >
	struct _ARGS_DATA_TRAITS_;

	template< class data_t >
	struct _ARGS_DATA_TRAITS_< data_t , true >
	{
		/**
		 * ATTRIBUTES
		 */
		data_t * table;

		std::size_t capacity;
		std::size_t count;
		std::size_t idx;

		/**
		 * CONSTRUCTOR
		 * Default
		 */
		_ARGS_DATA_TRAITS_( std::size_t aCapacity , std::size_t aCount )
		: table( new data_t[aCapacity] ),
		capacity( aCapacity ),
		count( aCount ),
		idx( 0 )
		{
AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
			AVM_OS_TRACE << "new _ARGS_DATA_ as array  :>"
					<< " capacity = " << std::setw(4) << capacity
					<< " : count = " << std::setw(4) << count
					<< " @" << avm_address_t( this ) << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
		}

		virtual ~_ARGS_DATA_TRAITS_()
		{
			delete[]( table );
		}


		inline void intialize()
		{
			//!!! NOTHING
		}

		inline void finalize()
		{
//			for( idx = 0 ; idx < count ; ++idx )
//			{
//				table[ idx ] = NULL;
//			}
			//!!! NOTHING
		}

	};


	template< class data_t >
	struct _ARGS_DATA_TRAITS_< data_t , false >
	{
		/**
		 * ATTRIBUTES
		 */
		std::vector< data_t > table;

		std::size_t capacity;
		std::size_t count;
		std::size_t idx;

		/**
		 * CONSTRUCTOR
		 * Default
		 */
		_ARGS_DATA_TRAITS_( std::size_t aCapacity , std::size_t aCount )
		: table( aCapacity ),
		capacity( aCapacity ),
		count( aCount ),
		idx( 0 )
		{
AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
			AVM_OS_TRACE << "new _ARGS_DATA_ as array  :>"
					<< " capacity = " << std::setw(4) << capacity
					<< " : count = " << std::setw(4) << count
					<< " @" << avm_address_t( this ) << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
		}

		virtual ~_ARGS_DATA_TRAITS_()
		{
			table.clear();
		}


		inline void intialize()
		{
			table.resize( count );

//AVM_IF_DEBUG_LEVEL_FLAG_AND( HIGH , SMT_SOLVING , (capacity != table.capacity()) )
			if(  capacity != table.capacity() )
			{
				AVM_OS_TRACE << "new _ARGS_TRAITS_ as vector :>"
						<< " capacity = " << capacity
						<< " vector<" << table.capacity()
						<< "> : count = " << count
						<< " @" << avm_address_t( this ) << std::endl;
			}
//AVM_ENDIF_DEBUG_LEVEL_FLAG_AND( HIGH , SMT_SOLVING )
		}

		inline void finalize()
		{
			table.clear();
		}

	};


	typedef _ARGS_DATA_TRAITS_<Expr_T, array_else_vector > ARGS_DATA;


	static List< ARGS_DATA * > ARG_CACHE;


	inline static ARGS_DATA * newARGS( std::size_t count )
	{
AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
		AVM_OS_TRACE << "newARGS :> count = " << std::setw(4) << count;
AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )

		ARGS_DATA * arg = NULL;
//		if( ARG_CACHE.populated() )
//		{
//			if( ARG_CACHE.nonempty() &&
//					(ARG_CACHE.last()->capacity > count) )
//			{
//				ARG_CACHE.pop_last_to( arg );
//				arg->count = count;
//			}
//			else if( ARG_CACHE.nonempty() &&
//					(ARG_CACHE.first()->capacity > count) )
//			{
//				ARG_CACHE.pop_first_to( arg );
//				arg->count = count;
//			}
//			else
//			{
//				arg = new ARGS_TABLE(count, count);
//			}
//		}
//		else
			if( ARG_CACHE.nonempty() && (ARG_CACHE.last()->capacity > count) )
		{
			ARG_CACHE.pop_last_to( arg );
			arg->count = count;
			arg->idx = 0;

AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
			AVM_OS_TRACE << " @" << avm_address_t( arg )
					<< " with capacity = " << arg->capacity << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
		}
		else
		{
AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
			AVM_OS_TRACE << " ==> " << std::flush;
AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )

			arg = new ARGS_DATA(count + SMT_ARGS_DATA_INCR_CAPACITY, count);
		}

		return( arg );
	}


	inline static void freeARGS( ARGS_DATA * & arg )
	{
AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
		AVM_OS_TRACE << "freeARGS:> count = " << std::setw(4) << arg->count
				<< " @" << avm_address_t( arg )
				<< " with capacity = " << arg->capacity << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )

		ARG_CACHE.append( arg );
	}


public:

	/**
	* Cache lifecycle
	*/
	inline static void initCache()
	{
		for( std::size_t i = 0 ; i < SMT_ARGS_DATA_INITIAL_COUNT ; ++i )
		{
			ARG_CACHE.append(new ARGS_DATA( SMT_ARGS_DATA_DEFAULT_CAPACITY, 0) );
		}
		ARG_CACHE.append(new ARGS_DATA( SMT_ARGS_DATA_ROOT_CAPACITY, 0) );
	}

	inline static void finalizeCache( )
	{
		std::size_t args_count = 0;

		while( ARG_CACHE.nonempty() )
		{
			++args_count;
			delete( ARG_CACHE.pop_last() );
		}

AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
		AVM_OS_TRACE << "Solver::finalize#cache:> count = " << args_count
				<< std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING )
	}


	struct ARGS
	{
		/**
		 * ATTRIBUTES
		 */
		ARGS_DATA * mData;

		/**
		 * CONSTRUCTOR
		 * Default
		 */
		ARGS( std::size_t count )
		: mData( newARGS(count) )
		{
			mData->intialize( );
		}

		virtual ~ARGS()
		{
			mData->finalize( );

			freeARGS( mData );
		}


		/**
		* OPERATORS
		*/
		inline ARGS_DATA * operator-> () const
		{
AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_ASSERT_FATAL_NULL_POINTER_EXIT( mData ) << "ARGS_DATA Pointer !!!"
			<< SEND_EXIT;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

			return( mData );
		}

		inline Expr_T & operator[](std::size_t offset) const
		{
			return( mData->table[ offset ] );
		}

		// Table Iterator
		inline bool hasNext() const
		{
			return( mData->idx < mData->count );
		}

		inline std::size_t offset() const
		{
			return( mData->idx );
		}

		inline void iter()
		{
			mData->idx = 0;
		}

		inline Expr_T & current()
		{
			return( mData->table[ mData->idx ] );
		}

		inline Expr_T & next()
		{
			return( mData->table[ mData->idx++ ] );
		}

		inline void next(Expr_T val)
		{
			mData->table[ mData->idx++ ] = val;
		}

//		inline void next(const data_t & val)
//		{
//			mData->table[ mData->idx++ ] = val;
//		}

	};

};


template< class VarDecl_T , class Sort_T , class Expr_T , bool array_else_vector >
List< typename SmtSolver< VarDecl_T , Sort_T , Expr_T ,
		array_else_vector , true >::ARGS_DATA * >
SmtSolver< VarDecl_T , Sort_T , Expr_T , array_else_vector , true >::ARG_CACHE;


template< class VarDecl_T , class Sort_T , class Expr_T , bool array_else_vector >
class SmtSolver< VarDecl_T , Sort_T , Expr_T ,  array_else_vector , false > :
	public SmtSolverTraits< VarDecl_T , Sort_T , Expr_T , array_else_vector >
{


protected:
	/**
	 * TYPEDEF
	 */
	typedef SmtSolver< VarDecl_T , Sort_T , Expr_T ,
			array_else_vector , false >  base_this_type;


public:
	/**
	 * CONSTRUCTOR
	 * Default
	 */
	SmtSolver()
	: SmtSolverTraits< VarDecl_T , Sort_T , Expr_T , array_else_vector >( )
	{
		//!!! NOTHING
	}


	/**
	 * DESTRUCTOR
	 */
	virtual ~SmtSolver()
	{
		//!!! NOTHING
	}


	/**
	* Cache lifecycle
	*/
	inline static void initCache()
	{
		//!!! NOTHING
	}

	inline static void finalizeCache( )
	{
		//!!! NOTHING
	}

};


} /* namespace sep */
#endif /* SOLVER_BASESMTSOLVER_H_ */