blob: d95c12b03ad63c1e10632c3c4c55942af6009d47 [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: 27 nov. 2014
*
* Contributors:
* Arnault Lapitre (CEA LIST) arnault.lapitre@cea.fr
* - Initial API and implementation
******************************************************************************/
#ifndef TRACECHECKER_H_
#define TRACECHECKER_H_
#include <fml/operator/OperatorLib.h>
#include <fml/lib/ITracePoint.h>
#include <solver/api/SolverDef.h>
namespace sep
{
class AvmCode;
class BF;
class EvaluationEnvironment;
class ExecutableForm;
class ExecutionContext;
class TracePoint;
class TraceChecker
{
protected:
EvaluationEnvironment & ENV;
ExecutableForm * theLocalExecutableForm;
SolverDef::SOLVER_KIND theSolverKind;
public:
/**
* CONSTRUCTOR
* Default
*/
TraceChecker(EvaluationEnvironment & anENV)
: ENV( anENV ),
theLocalExecutableForm( NULL ),
theSolverKind( SolverDef::DEFAULT_SOLVER_KIND )
{
//!! NOTHING
}
TraceChecker(EvaluationEnvironment & anENV, SolverDef::SOLVER_KIND aSolver)
: ENV( anENV ),
theLocalExecutableForm( NULL ),
theSolverKind( aSolver )
{
//!! NOTHING
}
TraceChecker(EvaluationEnvironment & anENV, ExecutableForm * anExecutable)
: ENV( anENV ),
theLocalExecutableForm( anExecutable ),
theSolverKind( SolverDef::DEFAULT_SOLVER_KIND )
{
//!! NOTHING
}
/**
* DESTRUCTOR
*/
virtual ~TraceChecker()
{
//!! NOTHING
}
/**
* SETTER
* theSolverKind
*/
void setSolverKind(SolverDef::SOLVER_KIND aSolverKind)
{
theSolverKind = aSolverKind;
}
/**
* TEST
* TracePoint Nature
*/
bool isPointNature(const BF & arg,
ENUM_TRACE_POINT::TRACE_NATURE nature) const;
////////////////////////////////////////////////////////////////////////////
// SAT CHECKING API
////////////////////////////////////////////////////////////////////////////
bool isSat(const ExecutionContext & anEC, const BF & arg);
bool isSat(const ExecutionContext & anEC, const AvmCode & aCode);
bool isSat(const ExecutionContext & anEC, AVM_OPCODE anOp, const BF & arg);
bool isSat(const ExecutionContext & anEC, TracePoint * aTP);
bool isSatFormula(const ExecutionContext & anEC, TracePoint * aTP);
bool isSatTime(const ExecutionContext & anEC, TracePoint * aTP);
bool isSatVariable(const ExecutionContext & anEC, TracePoint * aTP);
bool isSatCom(const ExecutionContext & anEC,
TracePoint * aTP, const BF & aTrace);
bool isSatRunnable(const ExecutionContext & anEC,
TracePoint * aTP, const BF & aTrace);
bool isSatRoutine(const ExecutionContext & anEC,
TracePoint * aTP, const BF & aTrace);
bool isSatTransition(const ExecutionContext & anEC,
TracePoint * aTP, const BF & aTrace);
bool isSatState(const ExecutionContext & anEC,
TracePoint * aTP, const BF & aTrace);
bool isSatStatemachine(const ExecutionContext & anEC,
TracePoint * aTP, const BF & aTrace);
bool isSatMachine(const ExecutionContext & anEC,
TracePoint * aTP, const BF & aTrace);
////////////////////////////////////////////////////////////////////////////
// WILL NEVER SAT CHECKING API
////////////////////////////////////////////////////////////////////////////
bool willNeverSat(const ExecutionContext & anEC, const BF & arg);
bool willNeverSat(const ExecutionContext & anEC, AvmCode * aCode);
bool willNeverSat(
const ExecutionContext & anEC, AVM_OPCODE anOp, const BF & arg);
bool willNeverSat(const ExecutionContext & anEC, TracePoint * aTP);
bool willNeverSatTransition(
const ExecutionContext & anEC, TracePoint * aTP);
bool willNeverSatState(
const ExecutionContext & anEC, TracePoint * aTP);
bool willNeverSatStatemachine(
const ExecutionContext & anEC, TracePoint * aTP);
bool willNeverSatMachine(
const ExecutionContext & anEC, TracePoint * aTP);
};
} /* namespace sep */
#endif /* TRACECHECKER_H_ */