blob: 4e03574899f13680e84b194b81ca002fb5fde822 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
/********************* */
/*! \file sat_solver_registry.h
** \verbatim
** Original author: dejan
** Major contributors: none
** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
** Copyright (c) 2009-2012 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief This class transforms a sequence of formulas into clauses.
**
** This class takes a sequence of formulas.
** It outputs a stream of clauses that is propositionally
** equi-satisfiable with the conjunction of the formulas.
** This stream is maintained in an online fashion.
**
** Compile time registration of SAT solvers with the SAT solver factory
**/
#pragma once
#include "cvc4_private.h"
#include <map>
#include <string>
#include <cxxabi.h>
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
namespace CVC4 {
namespace prop {
/**
* Interface for SAT solver constructors. Solvers should declare an instantiation of the
* SatSolverConstructor interface below.
*/
class SatSolverConstructorInterface {
public:
virtual ~SatSolverConstructorInterface() {}
virtual SatSolver* construct() = 0;
};
/**
* Registry containing all the registered SAT solvers.
*/
class SatSolverRegistry {
typedef std::map<std::string, SatSolverConstructorInterface*> registry_type;
/** Map from ids to solver constructors */
registry_type d_solvers;
/** Nobody can create the registry, there can be only one! */
SatSolverRegistry() {}
/**
* Register a SAT solver with the registry. The Constructor type should be a subclass
* of the SatSolverConstructor.
*/
template <typename Constructor>
size_t registerSolver(const char* id) {
int status;
char* demangled = abi::__cxa_demangle(id, 0, 0, &status);
d_solvers[demangled] = new Constructor();
free(demangled);
return d_solvers.size();
}
/** Get the instance of the registry */
static SatSolverRegistry* getInstance();
public:
/** Destructor */
~SatSolverRegistry();
/**
* Returns the constructor for the given SAT solver.
*/
static SatSolverConstructorInterface* getConstructor(std::string id);
/** Get the ids of the available solvers */
static void getSolverIds(std::vector<std::string>& solvers);
/** The Constructors are friends, since they need to register */
template<typename Solver>
friend class SatSolverConstructor;
};
/**
* Declare an instance of this class with the SAT solver in order to put it in the registry.
*/
template<typename Solver>
class SatSolverConstructor : public SatSolverConstructorInterface {
/** Static solver id we use for initialization */
static const size_t s_solverId;
public:
/** Constructs the solver */
SatSolver* construct() {
return new Solver();
}
};
template<typename Solver>
const size_t SatSolverConstructor<Solver>::s_solverId = SatSolverRegistry::getInstance()->registerSolver<SatSolverConstructor>(typeid(Solver).name());
}
}
|
