org.eclipse.efm.symbex/src/solver/CVC4Solver.cpp

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

#include "CVC4Solver.h"

/*
 * Here because "SolverDef.h" could define this macro
 */
#if defined( _AVM_SOLVER_CVC4_ )


#include <util/avm_vfs.h>

#include <fml/expression/AvmCode.h>
#include <fml/builtin/Boolean.h>
#include <fml/expression/BuiltinContainer.h>
#include <fml/builtin/Character.h>
#include <fml/expression/ExpressionComparer.h>
#include <fml/expression/ExpressionConstant.h>
#include <fml/expression/ExpressionConstructor.h>
#include <fml/expression/ExpressionTypeChecker.h>
#include <fml/numeric/Float.h>
#include <fml/builtin/Identifier.h>
#include <fml/numeric/Integer.h>
#include <fml/numeric/Rational.h>
#include <fml/builtin/String.h>

#include <fml/operator/Operator.h>

#include <fml/runtime/ExecutionContext.h>
#include <fml/runtime/ExecutionData.h>
#include <fml/runtime/RuntimeForm.h>
#include <fml/runtime/RuntimeID.h>
#include <fml/runtime/TableOfData.h>

#include <fml/type/TypeManager.h>

#include <fml/workflow/WObject.h>


namespace sep
{


/*
 *******************************************************************************
 * ID
 *******************************************************************************
 */
std::string CVC4Solver::ID = "CVC4";

std::string CVC4Solver::DESCRIPTION = "CVC4 "
		"'Cooperating Validity Checker 4, Efficient Automatic Theorem Prover "
		"for Satisfiability Modulo Theories problems, BSD License'";

avm_uint64_t CVC4Solver::SOLVER_SESSION_ID = 0;


//For automatic destroy of these CVC4 object using assignment
CVC4::Expr CVC4Solver::CVC4_EXPR_NULL;
CVC4::Type CVC4Solver::CVC4_TYPE_NULL;


/**
 * CONSTRUCTOR
 * Default
 */
CVC4Solver::CVC4Solver(bool produce_models_flag)
: base_this_type(CVC4_TYPE_NULL, CVC4_EXPR_NULL),
mParamPrefix( "P_" ),
mExprManager( ),
mSmtEngine( & mExprManager )
{
	SMT_TYPE_BOOL = mExprManager.booleanType();
	SMT_TYPE_INT  = mExprManager.integerType();
	SMT_TYPE_BV32 = mExprManager.mkBitVectorType(32);
	SMT_TYPE_BV64 = mExprManager.mkBitVectorType(64);
	SMT_TYPE_REAL = mExprManager.realType();

	SMT_TYPE_NUMBER = mExprManager.realType();

	SMT_TYPE_STRING = mExprManager.stringType();

	SMT_CST_BOOL_TRUE  = mExprManager.mkConst(true);
	SMT_CST_BOOL_FALSE = mExprManager.mkConst(false);

	SMT_CST_INT_ZERO = mExprManager.mkConst(CVC4::Rational(0));
	SMT_CST_INT_ONE  = mExprManager.mkConst(CVC4::Rational(1));


//	// Set the logic : LINEAR ARITHMETIC
//	mSmtEngine.setLogic("QF_LIRA");
//	// Set the logic : BIT VECTOR
//	mSmtEngine.setLogic("QF_BV");

	// Produce Models
	mSmtEngine.setOption("produce-models", produce_models_flag);

	// Enable Multiple Queries
	mSmtEngine.setOption("incremental", true);
	//Disable dagifying the output
	mSmtEngine.setOption("default-dag-thresh", 0);
	// Set the output-language to CVC's
	mSmtEngine.setOption("output-language", "cvc4");

}


/**
 * DESTRUCTOR
 */
CVC4Solver::~CVC4Solver()
{
	SMT_TYPE_BOOL = CVC4_TYPE_NULL;
	SMT_TYPE_INT  = CVC4_TYPE_NULL;
	SMT_TYPE_BV32 = CVC4_TYPE_NULL;
	SMT_TYPE_BV64 = CVC4_TYPE_NULL;
	SMT_TYPE_REAL = CVC4_TYPE_NULL;

	SMT_TYPE_NUMBER = CVC4_TYPE_NULL;

	SMT_TYPE_STRING = CVC4_TYPE_NULL;

	SMT_CST_BOOL_TRUE  = CVC4_EXPR_NULL;
	SMT_CST_BOOL_FALSE = CVC4_EXPR_NULL;

	SMT_CST_INT_ZERO = CVC4_EXPR_NULL;
	SMT_CST_INT_ONE  = CVC4_EXPR_NULL;
}


/**
 * CONFIGURE
 */
bool CVC4Solver::configure(
		Configuration & aConfiguration, WObject * wfFilterObject,
		ListOfPairMachineData & listOfSelectedVariable)
{
	if( not SatSolver::configure(
		aConfiguration, wfFilterObject, listOfSelectedVariable) )
	{
		return( false );
	}

	return( true );
}



/**
 * CREATE - DESTROY
 * ValidityChecker
 */

bool CVC4Solver::createChecker()
{
//	// Set the logic : LINEAR ARITHMETIC
//	mSmtEngine.setLogic("QF_LIRA");
//	// Set the logic : BIT VECTOR
//	mSmtEngine.setLogic("QF_BV");

//	// Produce Models
//	mSmtEngine.setOption("produce-models", false);
//
//	// Enable Multiple Queries
//	mSmtEngine.setOption("incremental", true);
//	//Disable dagifying the output
//	mSmtEngine.setOption("default-dag-thresh", 0);
//	// Set the output-language to CVC's
//	mSmtEngine.setOption("output-language", "cvc4");


AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )
	++SOLVER_SESSION_ID;
AVM_IF_DEBUG_LEVEL_GTE_HIGH
		mLogFolderLocation = OSS() << VFS::ProjectLogPath << "/cvc4/";

		if ( not VFS::checkWritingFolder(mLogFolderLocation) )
		{
			AVM_OS_LOG << " CVC4Solver::createChecker :> Error: The folder "
					<< "`" << mLogFolderLocation	<< "' "
					<< "---> doesn't exist or is not writable !!!"
					<< std::endl << std::endl;
			return( false );
		}

		std::string logFileLocation = ( OSS() << mLogFolderLocation
				<< "log_" << SOLVER_SESSION_ID << ".cvc4" );

//CVC3	mSmtEngine.setOption("dump-log", logFileLocation);
AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH
AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )

//	SMT_TYPE_BOOL = mExprManager.boolType();
//	SMT_TYPE_INT  = mExprManager.integerType();
//	SMT_TYPE_BV32 = mExprManager.mkBitVectorType(32);
//	SMT_TYPE_BV64 = mExprManager.mkBitVectorType(64);
//	SMT_TYPE_REAL = mExprManager.realType();

//	SMT_TYPE_NUMBER = mExprManager.realType();

//	SMT_TYPE_STRING = mExprManager.stringType();

//	SMT_CST_BOOL_TRUE  = mExprManager.mkConst(true);
//	SMT_CST_BOOL_FALSE = mExprManager.mkConst(false);
//
//	SMT_CST_INT_ZERO  = mExprManager.mkConst(0);
//	SMT_CST_INT_ONE   = mExprManager.mkConst(1);

	resetTable();

	return( true );
}

bool CVC4Solver::destroyChecker()
{
	resetTable();

//	SMT_TYPE_BOOL = CVC4_TYPE_NULL;
//	SMT_TYPE_INT  = CVC4_TYPE_NULL;
//	SMT_TYPE_BV32 = CVC4_TYPE_NULL;
//	SMT_TYPE_BV64 = CVC4_TYPE_NULL;
//	SMT_TYPE_REAL = CVC4_TYPE_NULL;

//	SMT_TYPE_NUMBER = CVC4_TYPE_NULL;

//	SMT_TYPE_STRING = CVC4_TYPE_NULL;

//	SMT_CST_BOOL_TRUE  = CVC4_EXPR_NULL;
//	SMT_CST_BOOL_FALSE = CVC4_EXPR_NULL;
//
//	SMT_CST_INT_ZERO  = CVC4_EXPR_NULL;
//	SMT_CST_INT_ONE   = CVC4_EXPR_NULL;

//	delete( mExprManager );
//	mExprManager = NULL;

	return( true );
}

bool CVC4Solver::resetTable()
{
	base_this_type::resetTable();

	mTableOfParameterExpr.append( CVC4_EXPR_NULL );

	return( true );
}



/**
 * PROVER
 */
//bool CVC4Solver::isSubSet(
//		const ExecutionContext & newEC, const ExecutionContext & oldEC)
//{
//	try
//	{
//		createChecker();
//
//		CVC4::Expr newFormula;
//		CVC4::Expr oldFormula;
//
//		// On construit la formule newFormula =
//		// garde_newEC AND
//		// x1 = e1 AND ---- AND xn = en
//		//
//		// et la formule oldFormula =
//		// garde_oldEC AND
//		// x1 = e'1 AND ---- AND xn = e'n AND
//		// e1 = e'1 AND ---- AND en = e'n
//		//
//		edToExprWithVarEquality(newEC.refExecutionData(), newFormula,
//				oldEC.refExecutionData(), oldFormula);
//
//AVM_IF_DEBUG_FLAG( SMT_SOLVING )
//	oldEC.writeTraceBeforeExec(AVM_OS_TRACE << TAB);
//	AVM_OS_TRACE << TAB << "Expr: " << oldFormula << std::endl;
//
//	newEC.writeTraceBeforeExec(AVM_OS_TRACE << TAB);
//	AVM_OS_TRACE << TAB << "Expr: " << newFormula << std::endl;
//AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )
//
//		// ASSERT de newFormula
//		//
//		mSmtEngine.assertFormula(newFormula);
//
//		// CHECKSAT de oldFormula
//		//
//		// A la place de CHECKSAT on utilise NOT QUERY(NOT oldFormula)
//		//
//		CVC4::Result result = mSmtEngine.query( oldFormula.notExpr() );
//
//		newFormula = CVC4_EXPR_NULL;
//		oldFormula = CVC4_EXPR_NULL;
//		destroyChecker();
//
//		// Si not result alors la formule oldFormula est satisfiable
//		return( result != CVC4::Result::VALID );
//	}
//	catch( const CVC4::Exception & ex )
//	{
//		AVM_OS_TRACE << TAB << "*** Exception caught in CVC4Solver::isSubSet: \n"
//				<< ex << std::endl;
//	}
//
//	return( false );
//}


//bool CVC4Solver::isSubSet(
//		const ExecutionContext & newEC, const ExecutionContext & oldEC)
//{
//	try
//	{
//		createChecker();
//
//AVM_IF_DEBUG_FLAG( SMT_SOLVING )
//	AVM_OS_TRACE << std::endl << "new EC: " << newEC.getIdNumber() << std::endl
//			<< std::endl << "old EC: " << oldEC.getIdNumber() << std::endl;
//AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )
//
//		// On construit la formule newFormula :
//		// garde_newEC AND
//		// x1 = e1 AND ---- AND xn = en
//		//
//		// et la formule oldFormula :
//		// garde_oldEC AND
//		// x1 = e'1 AND ---- AND xn = e'n AND
//		// e1 = e'1 AND ---- AND en = e'n
//		//
//		CVC4::Expr newFormula;
//		CVC4::Expr oldFormula;
//		edToExprWithVarEquality(newEC.refExecutionData(),
//				newFormula, oldEC.refExecutionData(), oldFormula);
//
//		if( oldFormula != SMT_CST_BOOL_FALSE )
//		{
//AVM_IF_DEBUG_FLAG( SMT_SOLVING )
//	oldEC.writeTraceBeforeExec(AVM_OS_TRACE << TAB);
//	AVM_OS_TRACE << TAB << "!!!!!!!!!!!!!!! old Expr: " << oldFormula << std::endl;
//
//	newEC.writeTraceBeforeExec(AVM_OS_TRACE << TAB);
//	AVM_OS_TRACE << TAB << "!!!!!!!!!!!!!!! new Expr: " << newFormula << std::endl;
//AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )
//
//			CVC4::Expr implyFormula;
//			if( not mTableOfParameterExprForOldFormula.empty() )
//			{
//				// On construit la formule itexists
//				// mTableOfParameterExprForOldFormula oldFormula
//				CVC4::Expr itExistsFormula = mExprManager.mkExpr(
//						CVC4::kind::EXISTS,
//						mExprManager.mkExpr(CVC4::kind::BOUND_VAR_LIST,
//								mTableOfParameterExprForOldFormula),
//						oldFormula);
//
//				// On construit la formule newFormula => itExistsFormula
//				//
//				implyFormula = mExprManager.mkExpr(
//						CVC4::kind::IMPLIES, newFormula, itExistsFormula);
//			}
//			else
//			{
//				// On construit la formule newFormula => oldFormula
//				//
//				implyFormula = mExprManager.mkExpr(
//						CVC4::kind::IMPLIES, newFormula, oldFormula);
//			}

//AVM_IF_DEBUG_FLAG( SMT_SOLVING )
//	AVM_OS_TRACE << implyFormula;
//AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )
//
//			// On construit la formule forall
//			// mTableOfParameterExprForNewFormula implyFormula
//			Vector< CVC4::Expr > forAllParameterAndVariableList;
//			forAllParameterAndVariableList.append(mTableOfVariableExpr);
//			forAllParameterAndVariableList.append(
//					mTableOfParameterExprForNewFormula);
//			CVC4::Expr forAllFormula = mExprManager.mkExpr(CVC4::kind::FORALL,
//					mExprManager.mkExpr(CVC4::kind::BOUND_VAR_LIST,
//							forAllParameterAndVariableList),
//					implyFormula);
//			AVM_OS_TRACE << TAB << "--> forAllFormula : ";
//			AVM_OS_TRACE << forAllFormula;
//
//			// QUERY de forAllFormula
//			//
//			CVC4::Result result = mSmtEngine.query( forAllFormula );
//
//			newFormula = CVC4_EXPR_NULL;
//			oldFormula = CVC4_EXPR_NULL;
//			destroyChecker();
//
//			return( result == CVC4::Result::VALID );
//		}
//		else
//		{
//			AVM_OS_TRACE << TAB << "--> cas  oldFormula à false " << std::endl;
//			return( false );
//		}
//	}
//	catch( const CVC4::Exception & ex )
//	{
//		AVM_OS_TRACE << TAB << "*** Exception caught in CVC4Solver::isSubSet: \n"
//				<< ex << std::endl;
//	}
//
//	return( false );
//}



bool CVC4Solver::isSubSet(
		const ExecutionContext & newEC, const ExecutionContext & oldEC)
{
	try
	{
		createChecker();

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << std::endl << "new EC: " << newEC.getIdNumber() << std::endl
			<< std::endl << "old EC: " << oldEC.getIdNumber() << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

		// On construit la formule newFormula :
		// garde_newEC AND
		// x1 = e1 AND ---- AND xn = en
		//
		// la formule oldFormula :
		// garde_oldEC AND
		// x1 = e'1 AND ---- AND xn = e'n
		//
		// et la formule equFormula qui établie l'égalité des mémoires symboliques
		// e1 = e'1 AND ---- AND en = e'n
		//
		CVC4::Expr newFormula;
		CVC4::Expr oldFormula;
		CVC4::Expr equFormula;
		edToExprWithVarEquality(newEC.refExecutionData(), newFormula,
								oldEC.refExecutionData(), oldFormula,
								equFormula);

		bool bResult = false;

		if( oldFormula != SMT_CST_BOOL_FALSE )
		{
AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	oldEC.traceDefault(AVM_OS_TRACE << TAB);
	AVM_OS_TRACE << TAB << "!!!!!!!!!!!!!!! old Expr: " << oldFormula << std::endl;

	newEC.traceDefault(AVM_OS_TRACE << TAB);
	AVM_OS_TRACE << TAB << "!!!!!!!!!!!!!!! new Expr: " << newFormula << std::endl;

//	newEC.writeTraceBeforeExec(AVM_OS_TRACE << TAB);
//	AVM_OS_TRACE << TAB << "!!!!!!!!!!!!!!! equ Expr: " << equFormula << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

			// Déclaration des variables de mTableOfVariableExpr et
			// et des paramètres de mTableOfParameterExpr
			//

			// ASSERT de newFormula
			//
			mSmtEngine.assertFormula(newFormula);

			// ASSERT de equFormula
			//
//			mSmtEngine.assertFormula(equFormula);

			// CHECKSAT de NOT oldFormula
			//
			// A la place on utilise NOT QUERY(oldFormula)
			//



			CVC4::Result toto = mSmtEngine.query( oldFormula );
// !!!!!!!!!!!!!!! 271009 : ESSAI AFA temporaire !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
//			CVC4::Result toto = mSmtEngine.query(
//					mExprManager.mkExpr(CVC4::kind::NOT, oldFormula) );
//			if(toto == CVC4::SATISFIABLE)
//			{
//				int i = 1;
//			}
//			if(toto == CVC4::INVALID)
//			{
//				int i = 2;
//			}

			bool result = ( toto == CVC4::Result::VALID );

			bResult = ( not result );
		}
		else
		{
AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << TAB << "--> cas  oldFormula à false " << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )
		}

		newFormula = CVC4_EXPR_NULL;
		oldFormula = CVC4_EXPR_NULL;
		equFormula = CVC4_EXPR_NULL;
		destroyChecker();

		return( bResult );
	}
	catch( const CVC4::Exception & ex )
	{
		AVM_OS_TRACE << TAB << "*** Exception caught in CVC4Solver::isSubSet: \n"
				<< ex << std::endl;

		destroyChecker();
	}

	return( false );
}


void CVC4Solver::edToExprWithVarEquality(const ExecutionData & newED,
		CVC4::Expr & newFormula, const ExecutionData & oldED,
		CVC4::Expr & oldFormula, CVC4::Expr & equFormula)
{
//	AVM_OS_ASSERT_FATAL_NULL_POINTER_EXIT( mSmtEngine ) << "ValidityChecker !!!"
//			<< SEND_EXIT;

	std::vector< CVC4::Expr > newFormulaList;
	std::vector< CVC4::Expr > oldFormulaList;
	std::vector< CVC4::Expr > equFormulaList;

	resetTable();

	// compile PCs
	CVC4::Expr aPC;

//	m_pTableOfParameterExpr = &mTableOfParameterExprForNewFormula;
	newFormulaList.push_back( aPC =
			safe_from_baseform(newED.getPathCondition()) );

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << std::endl << "new PC: " << aPC << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

//	m_pTableOfParameterExpr = NULL;
	oldFormulaList.push_back( aPC =
			safe_from_baseform(oldED.getPathCondition()) );

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << "old PC: " << aPC << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

	InstanceOfData * aVar = NULL;
	BaseTypeSpecifier * varTypeSpecifier = NULL;

	// compile DATAs
	std::ostringstream oss;
	ListOfInstanceOfData::iterator itVar;
	ListOfInstanceOfData::iterator endVar;

	ListOfPairMachineData::iterator itPairMachineData = getSelectedVariable().begin();
	ListOfPairMachineData::iterator endPairMachineData = getSelectedVariable().end();
	avm_offset_t varID = 1;
	for( ; itPairMachineData != endPairMachineData ; ++itPairMachineData )
	{
		if( (*itPairMachineData).second().nonempty() )
		{
			const RuntimeForm & newRF = newED.getRuntime(
					(*itPairMachineData).first() );
			const RuntimeForm & oldRF = oldED.getRuntime(
					(*itPairMachineData).first() );

			itVar = (*itPairMachineData).second().begin();
			endVar = (*itPairMachineData).second().end();
			for( ; itVar != endVar ; ++itVar , ++varID )
			{
				//??? TABLEAUX
				aVar = newRF.rawVariable((*itVar)->getOffset());
				varTypeSpecifier = aVar->getTypeSpecifier();

				oss.str("");
				oss << "V_" << varID;

//				m_pTableOfParameterExpr = &mTableOfParameterExprForNewFormula;
				CVC4::Expr newValue = safe_from_baseform(
						newRF.getData(*itVar), varTypeSpecifier);
//				m_pTableOfParameterExpr = NULL;
				CVC4::Expr oldValue = safe_from_baseform(
						oldRF.getData(*itVar), varTypeSpecifier);

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << varTypeSpecifier->strT() << "  "
			<< (*itVar)->getNameID() << " --> " << oss.str()
			<< std::endl << "\told: " << oldValue << "\tnew: " << newValue;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )


				if( varTypeSpecifier->isTypedBoolean() )
				{
					const BF & newElement = newRF.getData(*itVar);
					const BF & oldElement = oldRF.getData(*itVar);
					if( newElement.isBoolean() && oldElement.isBoolean() )
					{
						// On rajoute l'équivalence entre la nouvelle valeur
						// symbolique et l'ancienne
//						equFormulaList.push_back( mExprManagermkExpr(
//								CVC4::kind::EQUAL, newValue, oldValue) );
						oldFormulaList.push_back(
								(newElement.toBoolean() == oldElement.toBoolean()) ?
										SMT_CST_BOOL_TRUE : SMT_CST_BOOL_FALSE );

						if( newElement.toBoolean() != oldElement.toBoolean() )
						{
							oldFormula = SMT_CST_BOOL_FALSE;
							resetTable();
							return;
						}
					}
					else
					{
						CVC4::Expr varExpr =
								mExprManager.mkVar(oss.str(), SMT_TYPE_BOOL);
						mTableOfVariableExpr.push_back( varExpr );

						newFormulaList.push_back( mExprManager.mkExpr(
								CVC4::kind::EQUAL, varExpr, newValue) );
						oldFormulaList.push_back( mExprManager.mkExpr(
								CVC4::kind::EQUAL, varExpr, oldValue) );
					}
				}
				else if( varTypeSpecifier->weaklyTypedInteger() ||
						varTypeSpecifier->isTypedEnum() ||
						varTypeSpecifier->isTypedMachine() )
				{
					const BF & newElement = newRF.getData(*itVar);
					const BF & oldElement = oldRF.getData(*itVar);
					if ( newElement.isNumeric() && oldElement.isNumeric() )
					{
						// On rajoute l'égalité entre la nouvelle valeur
						// symbolique et l'ancienne
//						equFormulaList.push_back( mExprManager.mkExpr(
//								CVC4::kind::EQUAL, newValue, oldValue) );

						oldFormulaList.push_back(
								(ExpressionComparer::isEQ(newElement, oldElement)) ?
								SMT_CST_BOOL_TRUE : SMT_CST_BOOL_FALSE  );

						if( ExpressionComparer::isNEQ(newElement, oldElement) )
						{
							oldFormula = SMT_CST_BOOL_FALSE;
							resetTable();
							return;
						}
					}
					else
					{
						CVC4::Expr varExpr =
								mExprManager.mkVar(oss.str(), SMT_TYPE_INT);
						mTableOfVariableExpr.push_back( varExpr );

						newFormulaList.push_back( mExprManager.mkExpr(
								CVC4::kind::EQUAL, varExpr, newValue) );

						oldFormulaList.push_back( mExprManager.mkExpr(
								CVC4::kind::EQUAL, varExpr, oldValue) );
					}
				}
				else if( varTypeSpecifier->weaklyTypedReal() )
				{
					const BF & newElement = newRF.getData(*itVar);
					const BF & oldElement = oldRF.getData(*itVar);
					if ( newElement.isNumeric() && oldElement.isNumeric() )
					{
						// On rajoute l'égalité entre la nouvelle valeur
						// symbolique et l'ancienne
//						equFormulaList.push_back( mExprManager.mkExpr(
//								CVC4::kind::EQUAL, newValue, oldValue) );

						oldFormulaList.push_back(
								(ExpressionComparer::isEQ(newElement, oldElement)) ?
								SMT_CST_BOOL_TRUE : SMT_CST_BOOL_FALSE  );

						if( ExpressionComparer::isNEQ(newElement, oldElement) )
						{
							oldFormula = SMT_CST_BOOL_FALSE;
							resetTable();
							return;
						}
					}
					else
					{
						CVC4::Expr varExpr =
								mExprManager.mkVar(oss.str(), SMT_TYPE_REAL);
						mTableOfVariableExpr.push_back( varExpr );

						newFormulaList.push_back( mExprManager.mkExpr(
								CVC4::kind::EQUAL, varExpr, newValue) );

						oldFormulaList.push_back( mExprManager.mkExpr(
								CVC4::kind::EQUAL, varExpr, oldValue) );
					}
				}
				else
				{
					AVM_OS_ERROR_ALERT << "Unexpected an instance type << "
							<< aVar->getFullyQualifiedNameID() << " as : " << oss.str() << " : "
							<< varTypeSpecifier->getFullyQualifiedNameID() << ">> !!!"
							<< SEND_ALERT;

					CVC4::Expr varExpr =
							mExprManager.mkVar(oss.str(), SMT_TYPE_REAL);
					mTableOfVariableExpr.push_back( varExpr );

					newFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL, varExpr, newValue) );

					oldFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL, varExpr, oldValue) );
				}
			}
		}
	}

	Vector< CVC4::Expr >::iterator it = mTableOfParameterExpr.begin();
	for( ; it != mTableOfParameterExpr.end() ; ++it )
	{
		if( not mTableOfParameterExprForNewFormula.contains( *it ) )
		{
			mTableOfParameterExprForOldFormula.append( *it );
		}
	}

//	oldFormula = mSmtEngine.simplify(
//			mExprManager.mkExpr(CVC4::kind::AND, oldFormulaList) );
//
//	newFormula = mSmtEngine.simplify(
//			mExprManager.mkExpr(CVC4::kind::AND, newFormulaList) );

// Temporaire pour trace : remplacer ensuite par les 2 égalités précédentes
	CVC4::Expr oldFormulAvantSimplfy =
			mExprManager.mkExpr(CVC4::kind::AND, oldFormulaList);

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << std::endl << "oldFormula avant simplify : "
			<< oldFormulAvantSimplfy << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

	oldFormula = mSmtEngine.simplify( oldFormulAvantSimplfy );

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << "oldFormula après simplify : "
			<< oldFormula << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )


	CVC4::Expr newFormulAvantSimplfy =
			mExprManager.mkExpr(CVC4::kind::AND, newFormulaList);

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << std::endl << "newFormula avant simplify : "
			<< newFormulAvantSimplfy << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

	newFormula = mSmtEngine.simplify( newFormulAvantSimplfy );

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << "newFormula après simplify : "
			<< newFormula << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

//	CVC4::Expr equFormulAvantSimplfy = mExprManager.mkExpr(CVC4::kind::AND, equFormulaList);
//AVM_IF_DEBUG_FLAG( SMT_SOLVING )
//	AVM_OS_TRACE << std::endl << "equFormula avant simplify : ";
//			<< equFormulAvantSimplfy << std::endl;
//AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )
//	equFormula = mSmtEngine.simplify( equFormulAvantSimplfy );

	resetTable();
}



bool CVC4Solver::isEqualSet(
		const ExecutionContext & newEC, const ExecutionContext & oldEC)
{
	try
	{
		createChecker();

		CVC4::Expr newFormula;
		CVC4::Expr oldFormula;

		edToExpr(newEC.refExecutionData(), newFormula,
				oldEC.refExecutionData(), oldFormula);

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	oldEC.traceDefault(AVM_OS_TRACE << TAB);
	AVM_OS_TRACE << TAB << "Expr: " << oldFormula << std::endl;

	newEC.traceDefault(AVM_OS_TRACE << TAB);
	AVM_OS_TRACE << TAB << "Expr: " << newFormula << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

//		CVC4::Expr equalTest = mExprManager.mkExpr(CVC4::kind::FORALL,
//			mExprManager.mkExpr(CVC4::kind::BOUND_VAR_LIST, mTableOfVariableExpr),
//			mExprManager.mkExpr(CVC4::kind::EXISTS,
//				mExprManager.mkExpr(CVC4::kind::BOUND_VAR_LIST, mTableOfParameterExpr),
//				mExprManager.mkExpr(CVC4::kind::EQUAL, oldFormula, newFormula)));
//
//		CVC4::Expr equalTest = mExprManager.mkExpr(CVC4::kind::EXISTS,
//				mTableOfParameterExpr,
//				mExprManager.mkExpr(CVC4::kind::EQUAL,
//						oldFormula, newFormula));

		CVC4::Expr equalTest = mExprManager.mkExpr(CVC4::kind::EQUAL,
				oldFormula, newFormula);

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << TAB << "isSubSet Expr: " << equalTest << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

		CVC4::Result result = mSmtEngine.query(equalTest);

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << TAB << "\nisEqual result : "
			<< TAB << ( (result.isValid() == CVC4::Result::VALID) ?
					"true" : "false" ) << std::endl	<< std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

		newFormula = CVC4_EXPR_NULL;
		oldFormula = CVC4_EXPR_NULL;
		destroyChecker();

		return( result == CVC4::Result::VALID );
	}
	catch( const CVC4::Exception & ex )
	{
		AVM_OS_TRACE << TAB << "*** Exception caught in CVC4Solver::isEqualSet: \n"
				<< ex << std::endl;

		destroyChecker();
	}

	return( false );
}


SolverDef::SATISFIABILITY_RING CVC4Solver::isSatisfiable(const BF & aCondition)
{
AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )
	AVM_OS_TRACE << "CVC4Solver::isSatisfiable(...) "
			":" << SOLVER_SESSION_ID << ">" << std::endl
			<< "\t" << aCondition.str() << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )

	if( aCondition.isBoolean() )
	{
AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << TAB << "is satisfiable : " << aCondition.str() << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

		return( aCondition.toBoolean() ?
				SolverDef::SATISFIABLE : SolverDef::UNSATISFIABLE );
	}

	if( aCondition.isFloat() )
	{
AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << TAB << "is satisfiable : " << aCondition.str() << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

		return( ( aCondition.toFloat() != 0 ) ?
				SolverDef::SATISFIABLE : SolverDef::UNSATISFIABLE );
	}


	try
	{
		createChecker();

		// compile Formula
		CVC4::Expr aFormula= safe_from_baseform( aCondition );


AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )
	AVM_OS_TRACE << "CVC4Condition :" << SOLVER_SESSION_ID << ">" << std::endl;
	AVM_IF_DEBUG_LEVEL_GTE_HIGH
		AVM_OS_TRACE << "\t";
		aFormula.printAst(AVM_OS_TRACE);
		AVM_OS_TRACE << std::endl;
	AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH
	AVM_OS_TRACE << "\t" << aFormula << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )

		CVC4::Result result = mSmtEngine.checkSat( aFormula );

		// ATTENTION : lorsque CVC4 répond UNKNOWN,
		// on considère que la garde est SATISFIABLE
		SolverDef::SATISFIABILITY_RING satisfiability = SolverDef::SATISFIABLE;

		switch( result.isSat() )
		{
			case CVC4::Result::SAT:
			//case CVC4::VALID:
			{
				satisfiability = SolverDef::SATISFIABLE;
				break;
			}

			case CVC4::Result::UNSAT:
			//case CVC4::INVALID:
			{
				satisfiability = SolverDef::UNSATISFIABLE;
				break;
			}

			case CVC4::Result::SAT_UNKNOWN:
			{
				satisfiability = SolverDef::UNKNOWN_SAT;
				break;
			}

//			case CVC4::Result::ABORT:
			default:
			{
				satisfiability = SolverDef::ABORT_SAT;
				break;
			}
		}

AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )
	AVM_OS_TRACE << "result :" << SOLVER_SESSION_ID << "> "
			<< SolverDef::strSatisfiability(satisfiability) << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )

		aFormula = CVC4_EXPR_NULL;
		destroyChecker();

		return( satisfiability );
	}
	catch ( const CVC4::Exception & ex )
	{
		AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl
				<< "\tCVC4Solver::isSatisfiable< CVC4::Exception :"
				<< SOLVER_SESSION_ID << ">\n\t" << ex << std::endl
				<< REPEAT("--------", 10) << std::endl
				<< "\t  " << aCondition.str() << std::endl
				<< REPEAT("********", 10) << std::endl;

		destroyChecker();

		return( SolverDef::UNKNOWN_SAT );
	}
	catch ( const std::exception & ex )
	{
		AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl
				<< "\tCVC4Solver::isSatisfiable< std::exception :"
				<< SOLVER_SESSION_ID << ">\n\t" << ex.what() << std::endl
				<< REPEAT("--------", 10) << std::endl
				<< "\t  " << aCondition.str() << std::endl
				<< REPEAT("********", 10) << std::endl;

		destroyChecker();

		return( SolverDef::UNKNOWN_SAT );
	}
	catch ( ... )
	{
		AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl
				<< "\tCVC4Solver::isSatisfiable< unknown::exception :"
				<< SOLVER_SESSION_ID << ">" << std::endl
				<< REPEAT("--------", 10) << std::endl
				<< "\t  " << aCondition.str() << std::endl
				<< REPEAT("********", 10) << std::endl;

		destroyChecker();

		return( SolverDef::UNKNOWN_SAT );
	}

	return( SolverDef::UNKNOWN_SAT );
}



/**
 * SOLVER
 */
bool CVC4Solver::solveImpl(const BF & aCondition,
		BFVector & dataVector, BFVector & valuesVector)
{
AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )
	AVM_OS_TRACE << "CVC4Solver::solve(...) "
			":" << SOLVER_SESSION_ID << ">" << std::endl
			<< "\t" << aCondition.str() << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )

	try
	{
		// Produce Models option --> true
		createChecker( );

		resetTable();

		// compile Formula
		CVC4::Expr aFormula = safe_from_baseform( aCondition );


AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )
	AVM_OS_TRACE << "CVC4Condition :" << SOLVER_SESSION_ID << ">" << std::endl;
	AVM_IF_DEBUG_LEVEL_GTE_HIGH
		AVM_OS_TRACE << "\t";
		aFormula.printAst(AVM_OS_TRACE);
		AVM_OS_TRACE << std::endl;
	AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH
		AVM_OS_TRACE << "\t" << aFormula << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING )


		CVC4::Result result = mSmtEngine.checkSat( aFormula );

		if( result.isSat() == CVC4::Result::SAT )
		{
//			CVC4::Model * concreteModel = mSmtEngine.getModel();

			for( std::size_t i = 1 ; i < mTableOfParameterInstance.size() ; ++i )
			{
				dataVector.append( mTableOfParameterInstance[i] );

				const CVC4::Expr & var = mTableOfParameterExpr[i];
				CVC4::Expr val = mSmtEngine.getValue(var);

				if( val == SMT_CST_BOOL_TRUE )
				{
					valuesVector.append( ExpressionConstant::BOOLEAN_TRUE );
				}
				else if( val == SMT_CST_BOOL_FALSE )
				{
					valuesVector.append( ExpressionConstant::BOOLEAN_FALSE );
				}
				else if( val.getKind() == CVC4::kind::CONST_RATIONAL )
				{
					CVC4::Rational rat = val.getConst< CVC4::Rational >();

#if defined( _AVM_BUILTIN_NUMERIC_GMP_ )

					if( rat.isIntegral() )
					{
						valuesVector.append( ExpressionConstructor::newInteger(
								rat.getNumerator().get_mpz() ) );
					}
					else // C'est un rationel (num/den)
					{
						valuesVector.append(
								ExpressionConstructor::newRational(
										rat.get_mpq() ) );
					}

#else

					if( rat.isIntegral() )
					{
						if( rat.sgn() > 0 )
						{
							valuesVector.append( ExpressionConstructor::newUInteger(
									rat.getNumerator().getUnsignedLong()) );
						}
						else
						{
							valuesVector.append( ExpressionConstructor::newInteger(
									rat.getNumerator().getLong()) );
						}
					}
					else // C'est un rationel (num/den)
					{
						valuesVector.append(
								ExpressionConstructor::newRational(
									static_cast< avm_integer_t >(
										rat.getNumerator().getLong() ),
									static_cast< avm_integer_t >(
										rat.getDenominator().getLong() ) ) );
					}

#endif /* _AVM_BUILTIN_NUMERIC_GMP_ */

				}
				else
				{
					valuesVector.append( dataVector.back() );

				}

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << mTableOfParameterInstance.rawAt( i )->getFullyQualifiedNameID()
			<< " --> " << var << " = " << val << std::endl;
//	AVM_OS_COUT<< mTableOfParameterInstance.rawAt( i )->getFullyQualifiedNameID()
//			<< " --> " << var << " = " << val << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )
			}
		}

		aFormula = CVC4_EXPR_NULL;
		destroyChecker();

		return( result.isSat() == CVC4::Result::SAT );
	}
	catch ( const CVC4::Exception & ex )
	{
		AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl
				<< "\tCVC4Solver::solve< CVC4::Exception :"
				<< SOLVER_SESSION_ID << ">\n\t" << ex << std::endl
				<< REPEAT("--------", 10) << std::endl
				<< "\t  " << aCondition.str() << std::endl
				<< REPEAT("********", 10) << std::endl;

		destroyChecker();

		return( false );
	}
	catch ( const std::exception & ex )
	{
		AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl
				<< "\tCVC4Solver::solve< std::exception :"
				<< SOLVER_SESSION_ID << ">\n\t" << ex.what() << std::endl
				<< REPEAT("--------", 10) << std::endl
				<< "\t  " << aCondition.str() << std::endl
				<< REPEAT("********", 10) << std::endl;

		destroyChecker();

		return( false );
	}
	catch ( ... )
	{
		AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl
				<< "\tCVC4Solver::solve< unknown::exception :"
				<< SOLVER_SESSION_ID << ">" << std::endl
				<< REPEAT("--------", 10) << std::endl
				<< "\t  " << aCondition.str() << std::endl
				<< REPEAT("********", 10) << std::endl;

		destroyChecker();

		return( false );
	}

	return( false );
}


/**
 * TOOLS
 */

void CVC4Solver::edToExpr(
		const ExecutionData & newED, CVC4::Expr & newFormula,
		const ExecutionData & oldED, CVC4::Expr & oldFormula)
{
//	AVM_OS_ASSERT_FATAL_NULL_POINTER_EXIT( mSmtEngine ) << "ValidityChecker !!!"
//			<< SEND_EXIT;

	resetTable();

	// compile PCs
	CVC4::Expr aPC;
	std::vector< CVC4::Expr > newFormulaList;
	newFormulaList.push_back( aPC = safe_from_baseform(newED.getPathCondition()) );

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << std::endl << "new PC: " << aPC << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

	std::vector< CVC4::Expr > oldFormulaList;
	oldFormulaList.push_back( aPC = safe_from_baseform(oldED.getPathCondition()) );

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << "old PC: " << aPC << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

	InstanceOfData * aVar = NULL;
	BaseTypeSpecifier * varTypeSpecifier = NULL;

	// compile DATAs
	std::ostringstream oss;
	ListOfInstanceOfData::iterator itVar;
	ListOfInstanceOfData::iterator endVar;

	ListOfPairMachineData::iterator itPairMachineData = getSelectedVariable().begin();
	ListOfPairMachineData::iterator endPairMachineData = getSelectedVariable().end();
	avm_offset_t varID = 1;
	for( ; itPairMachineData != endPairMachineData ; ++itPairMachineData )
	{
		if( (*itPairMachineData).second().nonempty() )
		{
			const RuntimeForm & newRF = newED.getRuntime(
					(*itPairMachineData).first() );
			const RuntimeForm & oldRF = oldED.getRuntime(
					(*itPairMachineData).first() );

			itVar = (*itPairMachineData).second().begin();
			endVar = (*itPairMachineData).second().end();
			for( ; itVar != endVar ; ++itVar , ++varID )
			{
				//??? TABLEAUX
				aVar = newRF.rawVariable((*itVar)->getOffset());
				varTypeSpecifier = aVar->getTypeSpecifier();

				oss.str("");
				oss << "V_" << varID;

				CVC4::Expr newValue = safe_from_baseform(
						newRF.getData(*itVar), varTypeSpecifier);
				CVC4::Expr oldValue = safe_from_baseform(
						oldRF.getData(*itVar), varTypeSpecifier);

				if( varTypeSpecifier->isTypedBoolean() )
				{
					CVC4::Expr varExpr =
							mExprManager.mkVar(oss.str(), SMT_TYPE_BOOL);
					mTableOfVariableExpr.push_back( varExpr );
					newFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL, varExpr, newValue) );
					oldFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL,varExpr, oldValue) );
				}
				else if( varTypeSpecifier->weaklyTypedInteger() ||
						varTypeSpecifier->isTypedEnum() )
				{
					CVC4::Expr varExpr =
							mExprManager.mkVar(oss.str(), SMT_TYPE_INT);
					mTableOfVariableExpr.push_back( varExpr );
					newFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL, varExpr, newValue) );
					oldFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL, varExpr, oldValue) );
				}
				else if( varTypeSpecifier->weaklyTypedReal() )
				{
					CVC4::Expr varExpr =
							mExprManager.mkVar(oss.str(), SMT_TYPE_REAL);
					mTableOfVariableExpr.push_back( varExpr );
					newFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL, varExpr, newValue) );
					oldFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL, varExpr, oldValue) );
				}
				else
				{
					AVM_OS_ERROR_ALERT << "Unexpected an instance type << "
							<< aVar->getFullyQualifiedNameID() << " as : " << oss.str() << " : "
							<< varTypeSpecifier->getFullyQualifiedNameID() << ">> !!!"
							<< SEND_ALERT;

					CVC4::Expr varExpr = mExprManager.mkVar(oss.str(), SMT_TYPE_REAL);
					mTableOfVariableExpr.push_back( varExpr );
					newFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL, varExpr, newValue) );
					oldFormulaList.push_back( mExprManager.mkExpr(
							CVC4::kind::EQUAL, varExpr, oldValue) );
				}
			}
		}
	}

	oldFormula = mSmtEngine.simplify(
			mExprManager.mkExpr(CVC4::kind::AND, oldFormulaList) );

	newFormula = mSmtEngine.simplify(
			mExprManager.mkExpr(CVC4::kind::AND, newFormulaList) );


	resetTable();
}


/*
CVC4::Expr CVC4Solver::edToExpr(const ExecutionData & anED)
{
	AVM_OS_ASSERT_FATAL_NULL_POINTER_EXIT( mSmtEngine ) << "ValidityChecker !!!"
			<< SEND_EXIT;

//AVM_IF_DEBUG_FLAG( SMT_SOLVING )
//	AVM_OS_TRACE << TAB << "edToExpr ED: \n";
//	anED.toStreamData(AVM_OS_TRACE, "\t");
//	AVM_OS_TRACE << std::flush;
//AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

	resetTable();

	// compile PC
	CVC4::Expr pcExpr = mSmtEngine.simplify(safe_from_baseform(anED.getPathCondition()));
AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << TAB << "\nPC: " << pcExpr << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )
	mSmtEngine.assertFormula( pcExpr );

	std::vector< CVC4::Expr > aFormulaList;
	InstanceOfData * aVar = NULL;
	BaseTypeSpecifier * varTypeSpecifier = NULL;
	ListOfInstanceOfData::iterator itVar;

	// compile DATA
	ListOfListOfInstanceOfData::iterator itPairMachineData =
			getSelectedVariable()->begin();
	for( ; itPairMachineData != getSelectedVariable()->end() ; ++itPairMachineData )
	{
		if( (*itPairMachineData).second().nonempty() )
		{
			itVar = (*itPairMachineData).begin();
			RuntimeForm * aRF = anED.get(*itVar);

			for( ; itVar != (*itPairMachineData).end() ; ++itVar )
			{
				aVar = aRF.getExecutable()->getBasicData((*itVar)->getOffset());
				varTypeSpecifier = aVar->getTypeSpecifier();

				if( varTypeSpecifier->isTypedBoolean() )
				{
					aFormulaList.push_back( safe_from_baseform(
							aRF.getData(*itVar), varTypeSpecifier) );
				}
				else if( varTypeSpecifier->weaklyTypedInteger() ||
						varTypeSpecifier->isTypedEnum() )
				{
					aFormulaList.push_back( safe_from_baseform(
							aRF.getData(*itVar), varTypeSpecifier) );
				}
				else if( varTypeSpecifier->weaklyTypedReal() )
				{
					aFormulaList.push_back( safe_from_baseform(
							aRF.getData(*itVar), varTypeSpecifier) );
				}
				else
				{
					AVM_OS_ERROR_ALERT << "Unexpected an instance type << "
							<< aVar->getFullyQualifiedNameID() " : "
							<< varTypeSpecifier->getFullyQualifiedNameID() << ">> !!!"
							<< SEND_ALERT;

					aFormulaList.push_back( safe_from_baseform(
							aRF.getData(*itVar), varTypeSpecifier) );
				}
			}
		}
	}

	CVC4::Expr edExpr =  mExprManager.mkExpr(CVC4::kind::TUPLE, aFormulaList);

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << TAB << "Expr: ";
	AVM_OS_TRACE << edExpr << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

	resetTable();

	return( edExpr );
}

*/


CVC4::Expr CVC4Solver::edToExpr(const ExecutionData & anED)
{
//	AVM_OS_ASSERT_FATAL_NULL_POINTER_EXIT( mSmtEngine ) << "ValidityChecker !!!"
//			<< SEND_EXIT;

//AVM_IF_DEBUG_FLAG( SMT_SOLVING )
//	AVM_OS_TRACE << TAB << "edToExpr ED: \n";
//	anED.toStreamData(AVM_OS_TRACE, "\t");
//	AVM_OS_TRACE << std::flush;
//AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

	resetTable();

	std::vector< CVC4::Expr > aFormulaList;

	// compile PC
	aFormulaList.push_back( safe_from_baseform(anED.getPathCondition()) );

	BaseTypeSpecifier * varTypeSpecifier = NULL;
	ListOfInstanceOfData::iterator itVar;
	ListOfInstanceOfData::iterator endVar;

	// compile DATA
	ListOfPairMachineData::iterator itPairMachineData = getSelectedVariable().begin();
	ListOfPairMachineData::iterator endPairMachineData = getSelectedVariable().end();
	avm_offset_t varID = 0;
	for( ; itPairMachineData != endPairMachineData ; ++itPairMachineData )
	{
		if( (*itPairMachineData).second().nonempty() )
		{
			const RuntimeForm & aRF = anED.getRuntime(
					(*itPairMachineData).first() );

			itVar = (*itPairMachineData).second().begin();
			endVar = (*itPairMachineData).second().end();
			for( ; itVar != endVar ; ++itVar , ++varID )
			{
				//??? TABLEAUX
				InstanceOfData * aVar = aRF.rawVariable((*itVar)->getOffset());

				varTypeSpecifier = aVar->getTypeSpecifier();

				if( varTypeSpecifier->isTypedBoolean() )
				{
					aFormulaList.push_back( mExprManager.mkExpr(CVC4::kind::EQUAL,
							getVariableExpr(aVar, SMT_TYPE_BOOL, varID),
							safe_from_baseform(aRF.getData(*itVar),
									varTypeSpecifier)) );
				}
				else if( varTypeSpecifier->weaklyTypedInteger() ||
						varTypeSpecifier->isTypedEnum() )
				{
					aFormulaList.push_back( mExprManager.mkExpr(CVC4::kind::EQUAL,
							getVariableExpr(aVar, SMT_TYPE_INT, varID),
							safe_from_baseform(aRF.getData(*itVar),
									varTypeSpecifier)) );
				}
				else if( varTypeSpecifier->weaklyTypedReal() )
				{
					aFormulaList.push_back( mExprManager.mkExpr(CVC4::kind::EQUAL,
							getVariableExpr(aVar, SMT_TYPE_REAL, varID),
							safe_from_baseform(aRF.getData(*itVar),
									varTypeSpecifier)) );
				}
				else
				{
					AVM_OS_ERROR_ALERT << "Unexpected an instance type << "
							<< aVar->getFullyQualifiedNameID() << " : "
							<< varTypeSpecifier->getFullyQualifiedNameID() << ">> !!!"
							<< SEND_ALERT;

					aFormulaList.push_back( mExprManager.mkExpr(CVC4::kind::EQUAL,
							getVariableExpr(aVar, SMT_TYPE_REAL, varID),
							safe_from_baseform(aRF.getData(*itVar),
									varTypeSpecifier)) );
				}
			}
		}
	}

	CVC4::Expr edExpr = mExprManager.mkExpr(CVC4::kind::EXISTS,
			mExprManager.mkExpr(
					CVC4::kind::BOUND_VAR_LIST, mTableOfParameterExpr),
			mSmtEngine.simplify(
					mExprManager.mkExpr(CVC4::kind::AND, aFormulaList)) );

AVM_IF_DEBUG_FLAG( SMT_SOLVING )
	AVM_OS_TRACE << TAB << "Expr: ";
	AVM_OS_TRACE << edExpr << std::endl;
AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

	resetTable();

	return( edExpr );
}


CVC4::Expr & CVC4Solver::getParameterExpr(const BF & bfParameter)
{
	InstanceOfData * aParameter = bfParameter.to_ptr< InstanceOfData >();

	if( aParameter->getMark() == 0 )
	{
		BaseTypeSpecifier * paramTypeSpecifier =
				aParameter->referedTypeSpecifier();

		CVC4::Type paramType;

		if( paramTypeSpecifier->isTypedBoolean() )
		{
			paramType = SMT_TYPE_BOOL;
		}
		else if( paramTypeSpecifier->weaklyTypedInteger() )
		{
			if( SolverDef::DEFAULT_SOLVER_KIND ==
					SolverDef::SOLVER_CVC4_BV32_KIND )
			{
				paramType = SMT_TYPE_BV32;
			}
			else
//				if( SolverDef::DEFAULT_SOLVER_KIND ==
//						SolverDef::SOLVER_CVC4_KIND )
			{
				paramType = SMT_TYPE_INT;
			}
//			else
//			{
//			AVM_OS_FATAL_ERROR_EXIT
//					<< "SolverDef::DEFAULT_SOLVER_KIND <> "
//						"CVC4_INT and <> CVC4_BV32 !!!\n"
//					<< SEND_EXIT;
//
//				paramType = SMT_TYPE_INT;
//			}
		}
		else if( paramTypeSpecifier->weaklyTypedReal() )
		{
			paramType = SMT_TYPE_REAL;
		}
		else if( paramTypeSpecifier->isTypedString() )
		{
			paramType = SMT_TYPE_STRING;
		}
		else if( paramTypeSpecifier->isTypedEnum() )
		{
			paramType = SMT_TYPE_INT;
			// TODO Attention : il faudrait rajouter les contraintes
			// d'intervalle pour le type énuméré
		}
		else if( paramTypeSpecifier->isTypedMachine() )
		{
			// TODO:> Consolidation après TEST
			paramType = SMT_TYPE_INT;
		}
		else
		{
			AVM_OS_ERROR_ALERT << "Unexpected an instance type << "
					<< aParameter->getFullyQualifiedNameID() << " : "
					<< paramTypeSpecifier->getFullyQualifiedNameID() << ">> !!!"
					<< SEND_ALERT;

			paramType = SMT_TYPE_REAL;
		}


		CVC4::Expr paramExpr = mExprManager.mkVar( OSS() << "P_"
				<< mTableOfParameterInstance.size(), paramType );

//AVM_IF_DEBUG_FLAG( SMT_SOLVING )
//	AVM_OS_TRACE << TAB  << "P_" << mTableOfParameterInstance.size()
//			<< " <- " << aParameter->getFullyQualifiedNameID() << std::endl;
//	AVM_OS_TRACE << std::flush;
//AVM_ENDIF_DEBUG_FLAG( SMT_SOLVING )

		aParameter->setMark( mTableOfParameterInstance.size() );
		mTableOfParameterInstance.append( bfParameter );

		mTableOfParameterExpr.append(paramExpr);
//		if( m_pTableOfParameterExpr != NULL )
//		{
//			m_pTableOfParameterExpr->append(paramExpr);
//		}
	}

	return( mTableOfParameterExpr[ aParameter->getMark() ] );

}


CVC4::Expr & CVC4Solver::getVariableExpr(InstanceOfData * aVar,
		CVC4::Type varType, avm_offset_t varID)
{
	if( mTableOfVariableExpr.size() <= varID )
	{
		mTableOfVariableExpr.push_back(
				mExprManager.mkVar( OSS() << "V_" << varID, varType ) );
	}

	return( mTableOfVariableExpr.at(varID) );
}



CVC4::Expr CVC4Solver::safe_from_baseform(const BF & exprForm,
		BaseTypeSpecifier * typeSpecifier)
{
	try
	{
		return( from_baseform(exprForm, typeSpecifier) );
	}
	catch ( const CVC4::Exception & ex )
	{
		AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl
				<< "\tCVC4Solver::safe_from_baseform< CVC4::Exception :"
				<< SOLVER_SESSION_ID << ">\n\t" << ex << std::endl
				<< REPEAT("--------", 10) << std::endl
				<< "\tFailed to CONVERT sep::fml::expression to CVC4::Expr:>" << std::endl
				<< "\t  " << exprForm.str() << std::endl
				<< REPEAT("********", 10) << std::endl;

		destroyChecker();

		return( SMT_CST_INT_ZERO );
	}
	catch ( const std::exception & ex )
	{
		AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl
				<< "\tCVC4Solver::safe_from_baseform< std::exception :"
				<< SOLVER_SESSION_ID << ">\n\t" << ex.what() << std::endl
				<< REPEAT("--------", 10) << std::endl
				<< "\tFailed to CONVERT sep::fml::expression to CVC4::Expr:>" << std::endl
				<< "\t  " << exprForm.str() << std::endl
				<< REPEAT("********", 10) << std::endl;

		destroyChecker();

		return( SMT_CST_INT_ZERO );
	}
	catch ( ... )
	{
		AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl
				<< "\tCVC4Solver::safe_from_baseform< unknown::exception :"
				<< SOLVER_SESSION_ID << ">" << std::endl
				<< REPEAT("--------", 10) << std::endl
				<< "\tFailed to CONVERT sep::fml::expression to CVC4::Expr:>" << std::endl
				<< "\t  " << exprForm.str() << std::endl
				<< REPEAT("********", 10) << std::endl;

		destroyChecker();

		return( SMT_CST_INT_ZERO );
	}

	return( SMT_CST_INT_ZERO );
}

CVC4::Expr CVC4Solver::from_baseform(
		const BF & exprForm, BaseTypeSpecifier * typeSpecifier)
{
	AVM_OS_ASSERT_FATAL_NULL_SMART_POINTER_EXIT( exprForm ) << "expression !!!"
			<< SEND_EXIT;

	switch( exprForm.classKind() )
	{
		case FORM_AVMCODE_KIND:
		{
			AvmCode * aCode = exprForm.to_ptr< AvmCode >();

			typeSpecifier = TypeManager::UNIVERSAL;

			switch( aCode->getAvmOpCode() )
			{
				// COMPARISON OPERATION
				case AVM_OPCODE_EQ:
				{
					const BF & arg0 = aCode->first();
					const BF & arg1 = aCode->second();

					if( ExpressionTypeChecker::isBoolean(arg0) &&
							ExpressionTypeChecker::isBoolean(arg1) )
					{
						return( mExprManager.mkExpr(CVC4::kind::EQUAL,
								from_baseform(arg0, TypeManager::BOOLEAN),
								from_baseform(arg1, TypeManager::BOOLEAN)) );
					}
					else
					{
						return( mExprManager.mkExpr(CVC4::kind::EQUAL,
								from_baseform(arg0, typeSpecifier),
								from_baseform(arg1, typeSpecifier)) );
					}
				}

				case AVM_OPCODE_NEQ:
				{
					const BF & arg0 = aCode->first();
					const BF & arg1 = aCode->second();

					if( ExpressionTypeChecker::isBoolean(arg0) &&
							ExpressionTypeChecker::isBoolean(arg1) )
					{
						return( mExprManager.mkExpr(CVC4::kind::NOT,
								mExprManager.mkExpr(CVC4::kind::EQUAL,
									from_baseform(arg0, TypeManager::BOOLEAN),
									from_baseform(arg1, TypeManager::BOOLEAN))) );
					}
					else
					{
						return( mExprManager.mkExpr(CVC4::kind::DISTINCT,
								from_baseform(arg0, typeSpecifier),
								from_baseform(arg1, typeSpecifier)) );
					}
				}

				case AVM_OPCODE_LT:
				{
					if( SolverDef::DEFAULT_SOLVER_KIND ==
							SolverDef::SOLVER_CVC4_BV32_KIND )
					{
						return( mExprManager.mkExpr(CVC4::kind::BITVECTOR_SLT,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)) );
					}
					else
//						if( SolverDef::DEFAULT_SOLVER_KIND ==
//								SolverDef::SOLVER_CVC4_KIND )
					{
						return( mExprManager.mkExpr(CVC4::kind::LT,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)) );
					}
				}

				case AVM_OPCODE_LTE:
				{
					if( SolverDef::DEFAULT_SOLVER_KIND ==
							SolverDef::SOLVER_CVC4_BV32_KIND )
					{
						CVC4::Expr leftMember;
						CVC4::Expr rightMember;
						BFVector rightList;
						BFVector leftList;

						if( aCode->first().is< AvmCode >() &&
							( aCode->first().to_ptr< AvmCode >()->
									isOpCode( AVM_OPCODE_PLUS ) ) )
						{
							AvmCode::iterator it =
									aCode->first().to_ptr< AvmCode >()->begin();
							AvmCode::iterator endIt =
									aCode->first().to_ptr< AvmCode >()->end();
							for( ; it != endIt ; ++it )
							{
								if( (*it).is< AvmCode >() &&
									( (*it).to_ptr< AvmCode >()->
											isOpCode( AVM_OPCODE_UMINUS ) ) )
								{
									rightList.append(
											(*it).to_ptr< AvmCode >()->getArg1() );
								}
								else if( (*it).isInteger() &&
										( (*it).toInteger() < 0 ) )
								{
									rightList.append( ExpressionConstructor::
											newInteger(- (*it).toInteger()) );
								}
								else
								{
									leftList.append( (*it) );
								}
							}
						}
						else if( not ( aCode->first().isInteger() &&
									 ( aCode->first().toInteger() == 0 ) ) )
						{
							leftList.append( aCode->first() );
						}

						if( aCode->second().is< AvmCode >() &&
							( aCode->second().to_ptr< AvmCode >()->
									isOpCode( AVM_OPCODE_PLUS ) ) )
						{
							AvmCode::iterator it =
									aCode->second().to_ptr< AvmCode >()->begin();
							AvmCode::iterator endIt =
									aCode->second().to_ptr< AvmCode >()->end();
							for( ; it != endIt ; ++it )
							{
								if( (*it).is< AvmCode >() &&
									( (*it).to_ptr< AvmCode >()->
											isOpCode( AVM_OPCODE_UMINUS ) ) )
								{
									leftList.append(
											(*it).to_ptr< AvmCode >()->getArg1() );
								}
								else if( (*it).isInteger() &&
										( (*it).toInteger() < 0 ) )
								{
									leftList.append( ExpressionConstructor::
											newInteger(- (*it).toInteger()) );
								}
								else
								{
									rightList.append( (*it) );
								}
							}
						}
						else if( not ( aCode->second().isInteger() &&
									 ( aCode->second().toInteger() == 0 ) ) )
						{
							rightList.append( aCode->second() );
						}

						if( leftList.empty() )
						{
							leftMember = from_baseform(
									ExpressionConstant::INTEGER_ZERO,
									typeSpecifier);
						}
						else if( leftList.singleton() )
						{
							leftMember = from_baseform(leftList[0], typeSpecifier);
						}
						else
						{
							// leftMember = BVPLUS des elements de leftList
							leftMember = from_baseform( leftList[0], typeSpecifier );
							for (std::size_t i = 1 ; i < leftList.size() ; i ++)
							{
								leftMember =  mExprManager.mkExpr(
										CVC4::kind::BITVECTOR_PLUS, leftMember,
										from_baseform(leftList[i], typeSpecifier));
							}
						}

						if( rightList.empty() )
						{
							rightMember = from_baseform(
									ExpressionConstant::INTEGER_ZERO,
									typeSpecifier);
						}
						else if( rightList.singleton() )
						{
							rightMember = from_baseform(rightList[0], typeSpecifier);
						}
						else
						{
							// rightMember = BVPLUS des elements de rightList
							rightMember = from_baseform( rightList[0], typeSpecifier );
							for (std::size_t i = 1 ; i < rightList.size() ; i ++)
							{
								rightMember =  mExprManager.mkExpr(
										CVC4::kind::BITVECTOR_PLUS, rightMember,
										from_baseform(rightList[i], typeSpecifier));
							}
						}

						return( mExprManager.mkExpr(CVC4::kind::BITVECTOR_SLE,
								leftMember, rightMember) );
					}
					else
//						if( SolverDef::DEFAULT_SOLVER_KIND ==
//								SolverDef::SOLVER_CVC4_KIND )
					{
						return( mExprManager.mkExpr(CVC4::kind::LEQ,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)) );
					}
				}

				case AVM_OPCODE_GT:
				{
					if( SolverDef::DEFAULT_SOLVER_KIND ==
							SolverDef::SOLVER_CVC4_BV32_KIND )
					{
						return( mExprManager.mkExpr(CVC4::kind::BITVECTOR_SGT,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)) );
					}
					else
//						if( SolverDef::DEFAULT_SOLVER_KIND ==
//								SolverDef::SOLVER_CVC4_KIND )
					{
						return( mExprManager.mkExpr(CVC4::kind::GT,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)) );
					}
				}

				case AVM_OPCODE_GTE:
				{
					if( SolverDef::DEFAULT_SOLVER_KIND ==
							SolverDef::SOLVER_CVC4_BV32_KIND )
					{
						return( mExprManager.mkExpr(CVC4::kind::BITVECTOR_SGE,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)) );
					}
					else
//						if( SolverDef::DEFAULT_SOLVER_KIND ==
//								SolverDef::SOLVER_CVC4_KIND )
					{
						return( mExprManager.mkExpr(CVC4::kind::GEQ,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)) );
					}
				}


				case AVM_OPCODE_CONTAINS:
				{
					BuiltinCollection * aCollection =
							aCode->first().to_ptr< BuiltinCollection >();

					if( aCollection->singleton() )
					{
						const BF & col = aCollection->at(0);
						const BF & elt = aCode->second();

						if( ExpressionTypeChecker::isBoolean(col) &&
								ExpressionTypeChecker::isBoolean(elt) )
						{
							return( mExprManager.mkExpr(CVC4::kind::EQUAL,
									from_baseform(col, TypeManager::BOOLEAN),
									from_baseform(elt, TypeManager::BOOLEAN)) );
						}
						else
						{
							return( mExprManager.mkExpr(CVC4::kind::EQUAL,
									from_baseform(col, typeSpecifier),
									from_baseform(elt, typeSpecifier)) );
						}
					}
					else if( aCollection->populated() )
					{
						ARGS arg( aCollection->size() );
						const BF & elt = aCode->second();
						bool isBoolElt = ExpressionTypeChecker::isBoolean(elt);

						for( std::size_t offset = 0 ; arg.hasNext() ; ++offset )
						{
							const BF & col = aCollection->at( offset );

							if( isBoolElt && ExpressionTypeChecker::isBoolean(col) )
							{
								arg.next( mExprManager.mkExpr(CVC4::kind::EQUAL,
										from_baseform(col, TypeManager::BOOLEAN),
										from_baseform(elt, TypeManager::BOOLEAN) ));
							}
							else
							{
								arg.next( mExprManager.mkExpr(CVC4::kind::EQUAL,
										from_baseform(col, typeSpecifier),
										from_baseform(elt, typeSpecifier) ));
							}
						}

						return( mExprManager.mkExpr(CVC4::kind::OR, arg->table) );
					}
					else
					{
						return( ((typeSpecifier != NULL) &&
								typeSpecifier->isTypedBoolean()) ?
										SMT_CST_BOOL_FALSE : SMT_CST_INT_ZERO );
					}
				}


				// LOGICAL OPERATION
				case AVM_OPCODE_NOT:
				{
					return( mExprManager.mkExpr(CVC4::kind::NOT,
							from_baseform(aCode->first(), TypeManager::BOOLEAN)) );
				}

				case AVM_OPCODE_AND:
				{
					ARGS arg( aCode->size() );

					AvmCode::iterator it = aCode->begin();
					for( ; arg.hasNext() ; ++it )
					{
						arg.next( from_baseform(*it, TypeManager::BOOLEAN) );
					}

					return( mExprManager.mkExpr(CVC4::kind::AND, arg->table) );
				}

				case AVM_OPCODE_NAND:
				{
					return( mExprManager.mkExpr(CVC4::kind::NOT,
							mExprManager.mkExpr(CVC4::kind::AND,
									from_baseform(aCode->first(),
											TypeManager::BOOLEAN),
									from_baseform(aCode->second(),
											TypeManager::BOOLEAN))) );
				}

				case AVM_OPCODE_XAND:
				{
					return( mExprManager.mkExpr(CVC4::kind::OR,
							mExprManager.mkExpr(CVC4::kind::AND,
									from_baseform(aCode->first(),
											TypeManager::BOOLEAN),
									from_baseform(aCode->second(),
											TypeManager::BOOLEAN)),
							mExprManager.mkExpr(CVC4::kind::AND,
									mExprManager.mkExpr(CVC4::kind::NOT,
											from_baseform(aCode->first(),
													TypeManager::BOOLEAN)),
									mExprManager.mkExpr(CVC4::kind::NOT,
											from_baseform(aCode->second(),
													TypeManager::BOOLEAN))) ) );
				}


				case AVM_OPCODE_OR:
				{
					ARGS arg( aCode->size() );

					AvmCode::iterator it = aCode->begin();
					for( ; arg.hasNext() ; ++it )
					{
						arg.next( from_baseform(*it, TypeManager::BOOLEAN) );
					}

					return( mExprManager.mkExpr(CVC4::kind::OR, arg->table) );
				}

				case AVM_OPCODE_NOR:
				{
					return( mExprManager.mkExpr(CVC4::kind::NOT,
							mExprManager.mkExpr(CVC4::kind::OR,
									from_baseform(aCode->first(),
											TypeManager::BOOLEAN),
									from_baseform(aCode->second(),
											TypeManager::BOOLEAN))) );
				}


				// BITWISE OPERATION
				case AVM_OPCODE_BAND:
				{
					return( mExprManager.mkExpr(CVC4::kind::BITVECTOR_AND,
							from_baseform(aCode->first(), typeSpecifier),
							from_baseform(aCode->second(), typeSpecifier)) );
				}

				case AVM_OPCODE_BOR:
				{
					return( mExprManager.mkExpr(CVC4::kind::BITVECTOR_OR,
							from_baseform(aCode->first(), typeSpecifier),
							from_baseform(aCode->second(), typeSpecifier)) );
				}

				case AVM_OPCODE_LSHIFT:
				{
					if( aCode->second().isInteger() )
					{
						return( mExprManager.mkExpr(CVC4::kind::BITVECTOR_SHL,
								from_baseform(aCode->first(), typeSpecifier),
								mExprManager.mkConst( CVC4::Rational(
										static_cast<unsigned long int>(
											aCode->second().toInteger())) ) ) );
					}
					else
					{
						AVM_OS_FATAL_ERROR_EXIT
								<< "Unexpected second argument for "
									"newFixedLeftShiftExpr !!!\n"
								<< aCode->toString( AVM_TAB1_INDENT )
								<< SEND_EXIT;

						break;
					}
				}

				case AVM_OPCODE_RSHIFT:
				{
					if( aCode->second().isInteger() )
					{
						return( mExprManager.mkExpr(CVC4::kind::BITVECTOR_ASHR,
								from_baseform(aCode->first(), typeSpecifier),
								mExprManager.mkConst( CVC4::Rational(
										static_cast<unsigned long int>(
											aCode->second().toInteger())) ) ) );
					}
					else
					{
						AVM_OS_FATAL_ERROR_EXIT
								<< "Unexpected second argument for "
									"newFixedRightShiftExpr !!!\n"
								<< aCode->toString( AVM_TAB1_INDENT )
								<< SEND_EXIT;

						break;
					}
				}

				case AVM_OPCODE_XOR:
				{
					return( mExprManager.mkExpr(CVC4::kind::OR,
							mExprManager.mkExpr(CVC4::kind::AND,
								from_baseform(aCode->first(), typeSpecifier),
								mExprManager.mkExpr(CVC4::kind::NOT,
									from_baseform(aCode->second(), typeSpecifier))),
							mExprManager.mkExpr(CVC4::kind::AND,
								mExprManager.mkExpr(CVC4::kind::NOT,
									from_baseform(aCode->first(), typeSpecifier)),
								from_baseform(aCode->second(), typeSpecifier)) ) );
				}

				case AVM_OPCODE_XNOR:
				{
					return( mExprManager.mkExpr(CVC4::kind::OR,
							mExprManager.mkExpr(CVC4::kind::AND,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)),
							mExprManager.mkExpr(CVC4::kind::AND,
								mExprManager.mkExpr(CVC4::kind::NOT,
									from_baseform(aCode->first(), typeSpecifier)),
								mExprManager.mkExpr(CVC4::kind::NOT,
									from_baseform(aCode->second(), typeSpecifier))) ) );
				}


				// ARITHMETIC OPERATION
				case AVM_OPCODE_PLUS:
				{
					ARGS arg( aCode->size() );

					AvmCode::iterator it = aCode->begin();
					for( ; arg.hasNext() ; ++it )
					{
						arg.next( from_baseform(*it, typeSpecifier) );
					}

					if( SolverDef::DEFAULT_SOLVER_KIND ==
							SolverDef::SOLVER_CVC4_BV32_KIND )
					{
						return( mExprManager.mkExpr(
								CVC4::kind::BITVECTOR_PLUS, arg->table) );
					}
					else
//						if( SolverDef::DEFAULT_SOLVER_KIND ==
//								SolverDef::SOLVER_CVC4_KIND )
					{
						return( mExprManager.mkExpr(
								CVC4::kind::PLUS, arg->table) );
					}
				}

				case AVM_OPCODE_UMINUS:
				{
					return( mExprManager.mkExpr(CVC4::kind::UMINUS,
							from_baseform(aCode->first(), typeSpecifier)) );
				}

				case AVM_OPCODE_MINUS:
				{
					if( SolverDef::DEFAULT_SOLVER_KIND ==
							SolverDef::SOLVER_CVC4_BV32_KIND )
					{
						return( mExprManager.mkExpr(CVC4::kind::BITVECTOR_SUB,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)) );
					}
					else
//						if( SolverDef::DEFAULT_SOLVER_KIND ==
//								SolverDef::SOLVER_CVC4_KIND )
					{
						return( mExprManager.mkExpr(CVC4::kind::MINUS,
								from_baseform(aCode->first(), typeSpecifier),
								from_baseform(aCode->second(), typeSpecifier)) );
					}
				}

				case AVM_OPCODE_MULT:
				{
					ARGS arg( aCode->size() );

					AvmCode::iterator it = aCode->begin();
					for( ; arg.hasNext() ; ++it )
					{
						arg.next( from_baseform(*it, typeSpecifier) );
					}

					if( SolverDef::DEFAULT_SOLVER_KIND ==
							SolverDef::SOLVER_CVC4_BV32_KIND )
					{
						return( mExprManager.mkExpr(
									CVC4::kind::BITVECTOR_MULT, arg->table) );
					}
					else
//						if( SolverDef::DEFAULT_SOLVER_KIND ==
//								SolverDef::SOLVER_CVC4_KIND )
					{
						return( mExprManager.mkExpr(
								CVC4::kind::MULT, arg->table) );
					}
				}

				case AVM_OPCODE_DIV:
				{
					return( mExprManager.mkExpr(CVC4::kind::DIVISION,
							from_baseform(aCode->first(), typeSpecifier),
							from_baseform(aCode->second(), typeSpecifier)) );
				}

				case AVM_OPCODE_POW:
				{
					return( mExprManager.mkExpr(CVC4::kind::POW,
							from_baseform(aCode->first(), typeSpecifier),
							from_baseform(aCode->second(), typeSpecifier)) );
				}

//				case AVM_OPCODE_MOD:

				default:
				{
					AVM_OS_FATAL_ERROR_EXIT
							<< "CVC4Solver::from_baseform:> "
								"Unsupported expression !!!\n"
							<< aCode->toString( AVM_TAB1_INDENT )
							<< SEND_EXIT;

					break;
				}
			}

			break;
		}

		case FORM_INSTANCE_DATA_KIND:
		{
			return( getParameterExpr( exprForm ) );
		}

		case FORM_BUILTIN_BOOLEAN_KIND:
		{
			if( exprForm.to_ptr< Boolean >()->getValue() )
			{
				return( ((typeSpecifier != NULL) &&
						typeSpecifier->isTypedBoolean()) ?
								SMT_CST_BOOL_TRUE : SMT_CST_INT_ONE );
			}
			else
			{
				return( ((typeSpecifier != NULL) &&
						typeSpecifier->isTypedBoolean()) ?
								SMT_CST_BOOL_FALSE : SMT_CST_INT_ZERO );
			}
		}


		case FORM_BUILTIN_INTEGER_KIND:
		{
			if( SolverDef::DEFAULT_SOLVER_KIND ==
					SolverDef::SOLVER_CVC4_BV32_KIND )
			{
				return( mExprManager.mkConst( CVC4::BitVector( 32,
						static_cast<unsigned long int>(
								exprForm.to_ptr< Integer >()->toInteger())) ) );
			}
			else
//				if( SolverDef::DEFAULT_SOLVER_KIND == SolverDef::SOLVER_CVC4_KIND )
			{
				if( (typeSpecifier != NULL) &&
						typeSpecifier->isTypedBoolean() )
				{
					return( exprForm.to_ptr< Integer >()->isZero() ?
							SMT_CST_BOOL_FALSE : SMT_CST_BOOL_TRUE );
				}
				else
				{
#if defined( _AVM_BUILTIN_NUMERIC_GMP_ )

					return( mExprManager.mkConst( CVC4::Rational( CVC4::Integer(
							exprForm.to_ptr< Integer >()->getValue() ) ) ) );

#else

					return( mExprManager.mkConst( CVC4::Rational(
							exprForm.to_ptr< Integer >()->str()) ) );

#endif /* _AVM_BUILTIN_NUMERIC_GMP_ */
				}
			}
//			else
//			{
//			AVM_OS_FATAL_ERROR_EXIT
//					<< "SolverDef::DEFAULT_SOLVER_KIND <> "
//						"CVC4_INT and <> CVC4_BV32 !!!\n"
//					<< SEND_EXIT;
//
//				return( mExprManager.mkConst( CVC4::Rational(
//						exprForm.to_ptr< Integer >()->getValue() ) ) );
//			}
		}

		case FORM_BUILTIN_RATIONAL_KIND:
		{
			if( (typeSpecifier != NULL) && typeSpecifier->isTypedBoolean() )
			{
				return( exprForm.to_ptr< Rational >()->isZero() ?
						SMT_CST_BOOL_FALSE : SMT_CST_BOOL_TRUE );
			}
			else
			{
#if defined( _AVM_BUILTIN_NUMERIC_GMP_ )

				return( mExprManager.mkConst( CVC4::Rational(
						exprForm.to_ptr< Rational >()->getValue() ) ) );

#else

				return( mExprManager.mkConst( CVC4::Rational(
						exprForm.to_ptr< Rational >()->str() ) ) );

//				return( mExprManager.mkConst( CVC4::Rational(
//						exprForm.to_ptr< Rational >()->getNumerator(),
//						exprForm.to_ptr< Rational >()->getDenominator()) ) );
//
//				return( mExprManager.mkConst( CVC4::Rational(
//						exprForm.to_ptr< Rational >()->strNumerator(),
//						exprForm.to_ptr< Rational >()->strDenominator()) ) );

#endif /* _AVM_BUILTIN_NUMERIC_GMP_  */
			}
		}

		case FORM_BUILTIN_FLOAT_KIND:
		{
			if( (typeSpecifier != NULL) && typeSpecifier->isTypedBoolean() )
			{
				return( exprForm.to_ptr< Float >()->isZero() ?
						SMT_CST_BOOL_FALSE : SMT_CST_BOOL_TRUE  );
			}
			else
			{
#if defined( _AVM_BUILTIN_NUMERIC_GMP_ )

				return( mExprManager.mkConst( CVC4::Rational( mpq_class(
						exprForm.to_ptr< Float >()->getValue() ) ) ) );

#else

				return( mExprManager.mkConst(
						CVC4::Rational(exprForm.str()) ) );

#endif /* _AVM_BUILTIN_NUMERIC_GMP_ */
			}
		}


		case FORM_RUNTIME_ID_KIND:
		{
			return( mExprManager.mkConst(
					CVC4::Rational( exprForm.bfRID().getRid() ) ) );
		}


		case FORM_BUILTIN_CHARACTER_KIND:
		{
			AVM_OS_ERROR_ALERT << "Unexpected a CHAR as expression << "
					<< exprForm.to_ptr< Character >()->getValue()
					<< " >> !!!"
					<< SEND_ALERT;

			return( mExprManager.mkConst( CVC4::Rational(
					exprForm.to_ptr< Character >()->getValue() ) ) );
		}

		case FORM_BUILTIN_STRING_KIND:
		{
			return( mExprManager.mkConst( CVC4::String(
					exprForm.to_ptr< String >()->getValue() ) ) );
		}

		case FORM_BUILTIN_QUALIFIED_IDENTIFIER_KIND:
		{
			AVM_OS_FATAL_ERROR_EXIT
					<< "Unexpected a STRING | UFI as expression << "
					<< exprForm.to_ptr< String >()->getValue() << " >> !!!"
					<< SEND_EXIT;

			break;
//			return( mExprManager.mkConst(
//					exprForm.to_ptr< String >()->getValue() ) );
		}

		case FORM_BUILTIN_IDENTIFIER_KIND:
		{
			AVM_OS_FATAL_ERROR_EXIT
					<< "Unexpected a IDENTIFIER as expression << "
					<< exprForm.to_ptr< Identifier >()->getValue()
					<< " >> !!!"
					<< SEND_EXIT;

			break;
//			return( mExprManager.mkConst(
//					exprForm.to_ptr< Identifier >()->getValue() ) );
		}

		case FORM_OPERATOR_KIND:
		{
			AVM_OS_FATAL_ERROR_EXIT
					<< "Unexpected an OPERATOR as expression << "
					<< exprForm.to_ptr< Operator >()->standardSymbol()
					<< " >> !!!"
					<< SEND_EXIT;

			break;
//			return( mExprManager.mkConst(
//					exprForm.to_ptr< Operator >()->standardSymbol() ) );
		}


		case FORM_INSTANCE_BUFFER_KIND:
		case FORM_INSTANCE_CONNECTOR_KIND:
		case FORM_INSTANCE_MACHINE_KIND:
		case FORM_INSTANCE_PORT_KIND:

		default:
		{
			AVM_OS_FATAL_ERROR_EXIT
					<< "Unexpected BASEFORM KIND as expression << "
					<< exprForm.str() << " >> !!!"
					<< SEND_EXIT;

			break;
//			return( mExprManager.mkConst(
//					exprForm.to_ptr< BaseInstanceForm >()->getFullyQualifiedNameID() ) );
		}
	}

	AVM_OS_FATAL_ERROR_EXIT
			<< "CVC4Solver::from_baseform ERROR !!!"
			<< SEND_EXIT;

	return( SMT_CST_INT_ZERO );
}


} /* namespace sep */


#endif /* _AVM_SOLVER_CVC4_ */