blob: e32e14f2125076a2affabce0b2dbb0126d01c726 [file] [log] [blame]
/*******************************************************************************
* 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: 9 juil. 2009
*
* Contributors:
* Arnault Lapitre (CEA LIST) arnault.lapitre@cea.fr
* - Initial API and implementation
******************************************************************************/
#ifndef SOLVER_SOLVERFACTORY_H_
#define SOLVER_SOLVERFACTORY_H_
#include <collection/Typedef.h>
#include <fml/runtime/ExecutionContext.h>
#include <fml/runtime/ExecutionData.h>
#include <solver/api/SolverDef.h>
namespace sep
{
class Element;
class BF;
class EvaluationEnvironment;
class InstanceOfData;
class SatSolver;
class SolverFactory
{
public:
/**
* ATTRIBUTE
*/
static SatSolver * theDefaultSolver4CheckSatisfiability;
static SatSolver * theDefaultSolver4ModelsProduction;
static BFVector thePCParameters;
static BFVector thePCParameterValues;
////////////////////////////////////////////////////////////////////////////
// Pour pouvoir reutiliser tout l'outillage de Diverity
static APExecutionData theSymbolicED;
public:
/**
* LOADER - DISPOSER
* DESTROY
*/
static void load();
static void dispose();
static void destroy(SatSolver * aSolver);
/**
* SOLVER API
*/
static SolverDef::SATISFIABILITY_RING isSatisfiable(
SolverDef::SOLVER_KIND aSolverKind, const BF & aCondition);
inline static bool isStrongSatisfiable(
SolverDef::SOLVER_KIND aSolverKind, const BF & aCondition)
{
return( SolverFactory::isSatisfiable(aSolverKind, aCondition)
== SolverDef::SATISFIABLE );
}
inline static bool isWeakSatisfiable(
SolverDef::SOLVER_KIND aSolverKind, const BF & aCondition)
{
return( SolverFactory::isSatisfiable(aSolverKind, aCondition)
!= SolverDef::UNSATISFIABLE );
}
static SolverDef::SATISFIABILITY_RING isSatisfiable(
const BF & aCondition, bool useDefaultSolver = false);
inline static bool isStrongSatisfiable(
const BF & aCondition, bool useDefaultSolver)
{
return( SolverFactory::isSatisfiable(aCondition, useDefaultSolver)
== SolverDef::SATISFIABLE );
}
inline static bool isWeakSatisfiable(
const BF & aCondition, bool useDefaultSolver)
{
return( SolverFactory::isSatisfiable(aCondition, useDefaultSolver)
!= SolverDef::UNSATISFIABLE );
}
inline static bool isStrongSatisfiable(const BF & aCondition)
{
return( SolverFactory::isSatisfiable(aCondition,
SolverDef::DEFAULT_SOLVER_USAGE_FLAG) == SolverDef::SATISFIABLE );
}
inline static bool isWeakSatisfiable(const BF & aCondition)
{
return( SolverFactory::isSatisfiable(aCondition,
SolverDef::DEFAULT_SOLVER_USAGE_FLAG) != SolverDef::UNSATISFIABLE );
}
/**
* USED BY FAM LtlProverFilter
*/
static bool isEmptyIntersection(
ListOfInstanceOfData aListOfVarParam,
const ExecutionContext & aMainEC,
const ExecutionContext & aComparEC);
static bool isSubSet(
const ExecutionContext & aMainEC,
const ExecutionContext & aComparEC);
/**
* SOLVER
*/
static SatSolver * newSolver4CheckSatisfiability(
SolverDef::SOLVER_KIND aSolverKind);
static SatSolver * newSolver4ModelsProduction(
SolverDef::SOLVER_KIND aSolverKind);
////////////////////////////////////////////////////////////////////////////
// CONDITION PARAMETER SOLVING
////////////////////////////////////////////////////////////////////////////
static bool solve(SolverDef::SOLVER_KIND aSolverKind, const BF & aCondition,
BFVector & dataVector, BFVector & valuesVector);
////////////////////////////////////////////////////////////////////////////
// EXECUTION CONTEXT SOLVING
////////////////////////////////////////////////////////////////////////////
inline static APExecutionData solve(
EvaluationEnvironment & ENV, const ExecutionContext & anEC)
{
// return( SolverFactory::solve(
// SolverDef::DEFAULT_SOLVER_KIND, ENV, anEC) );
return( SolverFactory::solve(
(*theDefaultSolver4ModelsProduction), ENV, anEC) );
}
inline static APExecutionData solve(SolverDef::SOLVER_KIND aSolverKind,
EvaluationEnvironment & ENV, const ExecutionContext & anEC)
{
return( SolverFactory::solve(aSolverKind, ENV, anEC,
anEC.refExecutionData().getAllPathCondition()) );
}
static APExecutionData solve(SolverDef::SOLVER_KIND aSolverKind,
EvaluationEnvironment & ENV, const ExecutionContext & anEC,
const BF & aCondition);
inline static APExecutionData solve(SatSolver & aSolver,
EvaluationEnvironment & ENV, const ExecutionContext & anEC)
{
APExecutionData anED = anEC.getAPExecutionData();
return( SolverFactory::solve(aSolver, ENV, anED) ?
anED : APExecutionData::REF_NULL);
}
inline static APExecutionData solve(SatSolver & aSolver,
EvaluationEnvironment & ENV, const ExecutionContext & anEC,
const BF & aCondition)
{
APExecutionData anED = anEC.getAPExecutionData();
return( SolverFactory::solve(aSolver, ENV, anED, aCondition) ?
anED : APExecutionData::REF_NULL);
}
////////////////////////////////////////////////////////////////////////////
// EXECUTION DATA SOLVING
////////////////////////////////////////////////////////////////////////////
inline static bool solve(
EvaluationEnvironment & ENV, APExecutionData & anED)
{
return( SolverFactory::solve(
(*theDefaultSolver4ModelsProduction), ENV, anED) );
}
inline static bool solve(SatSolver & aSolver,
EvaluationEnvironment & ENV, APExecutionData & anED)
{
return( SolverFactory::solve(aSolver, ENV, anED,
anED->getAllPathCondition()) );
}
static bool solve(SatSolver & aSolver, EvaluationEnvironment & ENV,
APExecutionData & anED, const BF & aCondition);
////////////////////////////////////////////////////////////////////////////
// EXECUTION CONTEXT NUMERIZATION
////////////////////////////////////////////////////////////////////////////
inline static ExecutionContext * numerize(
EvaluationEnvironment & ENV, const ExecutionContext & anEC)
{
return( SolverFactory::numerize(
(*theDefaultSolver4ModelsProduction), ENV, anEC) );
}
inline static ExecutionContext * numerize(SatSolver & aSolver,
EvaluationEnvironment & ENV, const ExecutionContext & anEC)
{
APExecutionData newED = SolverFactory::solve(aSolver, ENV, anEC);
// ATTENTION : Hauteur à modifier !!!
return( new ExecutionContext(anEC, newED, anEC.getHeight() + 1, 0) );
}
////////////////////////////////////////////////////////////////////////////
// EXECUTION CONTEXT PARAMETERS NUMERIZATION
////////////////////////////////////////////////////////////////////////////
inline static bool solveParameters(APExecutionData & anED)
{
return( solveParameters(anED, anED->getAllPathCondition()) );
}
static bool solveParameters(APExecutionData & anED, const BF & aCondition);
////////////////////////////////////////////////////////////////////////////
// Pour pouvoir reutiliser tout l'outillage de DIVERSITY
////////////////////////////////////////////////////////////////////////////
static void setModel(EvaluationEnvironment & ENV, APExecutionData & anED);
static void resetModel(APExecutionData & anED);
static void setRuntimeParametersSolvingValues(APExecutionData & anED);
static void updateRuntimeParametersValues(const BF & aValue);
static void finalizeRuntimeParameters();
////////////////////////////////////////////////////////////////////////////
// EXECUTION DATA NEWFRESH
////////////////////////////////////////////////////////////////////////////
static APExecutionData solveNewfresh(SolverDef::SOLVER_KIND aSolverKind,
EvaluationEnvironment & ENV, const ExecutionContext & anEC,
const BF & aCondition);
};
}
#endif /* SOLVER_SOLVERFACTORY_H_ */