| /******************************************************************************* |
| * 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: 29 févr. 2012 |
| * |
| * Contributors: |
| * Arnault Lapitre (CEA LIST) arnault.lapitre@cea.fr |
| * - Initial API and implementation |
| ******************************************************************************/ |
| |
| #ifndef SOLVER_SOLVERDEF_H_ |
| #define SOLVER_SOLVERDEF_H_ |
| |
| |
| /** |
| * DEFINE MACRO W.R.T. LICENSE CONSTRAINT |
| */ |
| #if defined( _ECLIPSE_PUBLIC_LICENSE_ ) |
| |
| |
| //// Default |
| //#define _AVM_SOLVER_CVC4_ |
| // |
| //// Incubation |
| //#define _AVM_SOLVER_Z3_ |
| |
| // Experimental |
| #if defined( _AVM_SOLVER_YICES_V2_ ) |
| #undef _AVM_SOLVER_YICES_V2_ |
| #endif /* _AVM_SOLVER_YICES_V2_ */ |
| |
| // Deprecated |
| #if defined( _AVM_SOLVER_OMEGA_ ) |
| #undef _AVM_SOLVER_OMEGA_ |
| #endif /* _AVM_SOLVER_OMEGA_ */ |
| |
| |
| #else |
| |
| |
| //// Default |
| //#if not defined( _AVM_SOLVER_CVC4_ ) |
| //#define _AVM_SOLVER_CVC4_ |
| //#endif /* _AVM_SOLVER_CVC4_ */ |
| // |
| //// Incubation |
| //#if not defined( _AVM_SOLVER_Z3_ ) |
| //#define _AVM_SOLVER_Z3_ |
| //#endif /* _AVM_SOLVER_Z3_ */ |
| // |
| //// Experimental |
| //#if not defined( _AVM_SOLVER_YICES_V2_ ) |
| //#define _AVM_SOLVER_YICES_V2_ |
| //#endif /* _AVM_SOLVER_YICES_V2_ */ |
| // |
| // |
| //// Deprecated |
| //#if not defined( _AVM_SOLVER_OMEGA_ ) |
| //#define _AVM_SOLVER_OMEGA_ |
| //#endif /* _AVM_SOLVER_OMEGA_ */ |
| |
| |
| #endif /* _ECLIPSE_PUBLIC_LICENSE_ */ |
| |
| |
| #include <string> |
| |
| //#if defined( _AVM_SOLVER_OMEGA_ ) |
| // |
| //#endif /* _AVM_SOLVER_OMEGA_ */ |
| |
| |
| //#if defined( _AVM_SOLVER_CVC4_ ) |
| // |
| //#elif defined( _AVM_SOLVER_CVC3_ ) |
| // |
| //#endif /* _AVM_SOLVER_CVC_ */ |
| // |
| // |
| //#if defined( _AVM_SOLVER_YICES_V2_ ) |
| // |
| //#elif defined( _AVM_SOLVER_YICES_V1_ ) |
| // |
| //#endif /* _AVM_SOLVER_YICES_ */ |
| // |
| // |
| //#if defined( _AVM_SOLVER_Z3_ ) |
| // |
| //#endif /* _AVM_SOLVER_Z3_ */ |
| |
| |
| namespace sep |
| { |
| |
| |
| class OutStream; |
| |
| |
| class SolverDef |
| { |
| |
| public: |
| /** |
| * TYPE DECLARATIONS |
| */ |
| |
| enum SATISFIABILITY_RING { |
| UNSATISFIABLE = 0, |
| SATISFIABLE = 1, |
| |
| ABORT_SAT, |
| UNKNOWN_SAT |
| }; |
| |
| |
| enum VALIDITY_RING { |
| INVALID = 0, |
| VALID = 1, |
| |
| ABORT_VALID, |
| UNKNOWN_VALID |
| }; |
| |
| |
| /** |
| * TYPE DECLARATIONS |
| */ |
| enum SOLVER_KIND |
| { |
| SOLVER_UNDEFINED_KIND = 0x0000, |
| |
| SOLVER_OMEGA_KIND = 0x00001, |
| |
| SOLVER_YICES1_KIND = 0x00010, |
| SOLVER_YICES2_KIND = 0x00020, |
| |
| SOLVER_YICES_KIND = SOLVER_YICES1_KIND |
| | SOLVER_YICES2_KIND, |
| |
| SOLVER_Z3_KIND = 0x00100, |
| |
| SOLVER_CVC3_KIND = 0x01000, |
| SOLVER_CVC3_BV32_KIND = 0x02000, |
| |
| SOLVER_CVC4_KIND = 0x04000, |
| SOLVER_CVC4_BV32_KIND = 0x08000, |
| |
| SOLVER_CVC_KIND = SOLVER_CVC3_KIND |
| | SOLVER_CVC4_KIND, |
| |
| SOLVER_CVC_BV_KIND = SOLVER_CVC3_BV32_KIND |
| | SOLVER_CVC4_BV32_KIND |
| }; |
| |
| |
| public: |
| /** |
| * CONSTRUCTOR |
| * Default |
| */ |
| SolverDef() |
| { |
| //!! NOTHING |
| } |
| |
| |
| /** |
| * DESTRUCTOR |
| */ |
| virtual ~SolverDef() |
| { |
| //!! NOTHING |
| } |
| |
| /** |
| * ATTRIBUTES |
| */ |
| static bool DEFAULT_SOLVER_USAGE_FLAG; |
| |
| static SolverDef::SOLVER_KIND DEFAULT_SOLVER_KIND; |
| |
| |
| /** |
| * toString |
| */ |
| static std::string strSatisfiability(SATISFIABILITY_RING ring); |
| |
| static std::string strValidity(VALIDITY_RING ring); |
| |
| static std::string strSolver(SOLVER_KIND king); |
| |
| /** |
| * toSolver |
| */ |
| static SOLVER_KIND toSolver(std::string strKing, |
| SOLVER_KIND defaultKind /*= SOLVER_UNDEFINED_KIND*/); |
| |
| /** |
| * SOLVER |
| * Available |
| * List |
| */ |
| static bool isAvailableSolver(SOLVER_KIND king); |
| |
| static void toStreamSolverList(OutStream & os, |
| const std::string & aHeader = "solvers"); |
| |
| |
| }; |
| |
| } /* namespace sep */ |
| #endif /* SOLVER_SOLVERDEF_H_ */ |
