| /******************************************************************************* |
| * 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_ */ |