<useDefaultCommand>true</useDefaultCommand>
<runAllBuilders>true</runAllBuilders>
</target>
+ <target name="check" path="test/regress" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+ <buildCommand>make</buildCommand>
+ <buildArguments>-j10</buildArguments>
+ <buildTarget>check</buildTarget>
+ <stopOnError>true</stopOnError>
+ <useDefaultCommand>true</useDefaultCommand>
+ <runAllBuilders>true</runAllBuilders>
+ </target>
<target name="check" path="test/unit" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
<buildCommand>make</buildCommand>
<buildArguments>-j10</buildArguments>
cnf_stream.cpp \
sat_solver.h \
sat_solver_factory.h \
- sat_solver_factory.cpp
+ sat_solver_factory.cpp \
+ sat_solver_registry.h \
+ sat_solver_registry.cpp
SUBDIRS = minisat bvminisat
#pragma once
#include "prop/sat_solver.h"
+#include "prop/sat_solver_registry.h"
#include "prop/bvminisat/simp/SimpSolver.h"
namespace CVC4 {
class MinisatSatSolver: public BVSatSolverInterface {
BVMinisat::SimpSolver* d_minisat;
- MinisatSatSolver();
public:
+ MinisatSatSolver();
~MinisatSatSolver();
void addClause(SatClause& clause, bool removable);
};
Statistics d_statistics;
- friend class SatSolverFactory;
};
+template class SatSolverConstructor<MinisatSatSolver>;
+
}
}
#pragma once
#include "prop/sat_solver.h"
+#include "prop/sat_solver_registry.h"
#include "prop/minisat/simp/SimpSolver.h"
namespace CVC4 {
/** Context we will be using to synchronzie the sat solver */
context::Context* d_context;
- DPLLMinisatSatSolver ();
-
public:
+ DPLLMinisatSatSolver ();
~DPLLMinisatSatSolver();
+
static SatVariable toSatVariable(Minisat::Var var);
static Minisat::Lit toMinisatLit(SatLiteral lit);
static SatLiteral toSatLiteral(Minisat::Lit lit);
};
Statistics d_statistics;
- friend class SatSolverFactory;
};
+template class SatSolverConstructor<DPLLMinisatSatSolver>;
+
} // prop namespace
} // cvc4 namespace
#ifndef __CVC4__PROP__SAT_MODULE_H
#define __CVC4__PROP__SAT_MODULE_H
-#include <stdint.h>
+#include <string>
+#include <stdint.h>
#include "util/options.h"
#include "util/stats.h"
#include "context/cdlist.h"
/** Create a new boolean variable in the solver. */
virtual SatVariable newVar(bool theoryAtom = false) = 0;
-
/** Check the satisfiability of the added clauses */
virtual SatValue solve() = 0;
**/
#include "prop/sat_solver_factory.h"
+#include "prop/sat_solver_registry.h"
#include "prop/minisat/minisat.h"
#include "prop/bvminisat/bvminisat.h"
return new DPLLMinisatSatSolver();
}
+SatSolver* SatSolverFactory::create(const char* name) {
+ SatSolverConstructorInterface* constructor = SatSolverRegistry::getConstructor(name);
+ if (constructor) {
+ return constructor->construct();
+ } else {
+ return NULL;
+ }
+}
-
+void SatSolverFactory::getSolverIds(std::vector<std::string>& solvers) {
+ SatSolverRegistry::getSolverIds(solvers);
+}
#include "cvc4_public.h"
+#include <string>
+#include <vector>
#include "prop/sat_solver.h"
namespace CVC4 {
class SatSolverFactory {
public:
+
static BVSatSolverInterface* createMinisat();
static DPLLSatSolverInterface* createDPLLMinisat();
+
+ static SatSolver* create(const char* id);
+
+ /** Get the solver ids that are available */
+ static void getSolverIds(std::vector<std::string>& solvers);
+
};
}
--- /dev/null
+/********************* */
+/*! \file sat_solver_registry.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): barrett, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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
+ **/
+
+#include "prop/sat_solver_registry.h"
+#include "sstream"
+
+using namespace std;
+using namespace CVC4;
+using namespace prop;
+
+SatSolverConstructorInterface* SatSolverRegistry::getConstructor(string id) {
+ SatSolverRegistry* registry = getInstance();
+ registry_type::const_iterator find = registry->d_solvers.find(id);
+ if (find == registry->d_solvers.end()) {
+ return NULL;
+ } else {
+ return find->second;
+ }
+}
+
+void SatSolverRegistry::getSolverIds(std::vector<std::string>& solvers) {
+ SatSolverRegistry* registry = getInstance();
+ registry_type::const_iterator it = registry->d_solvers.begin();
+ registry_type::const_iterator it_end = registry->d_solvers.end();
+ for (; it != it_end; ++ it) {
+ solvers.push_back(it->first);
+ }
+}
+
+SatSolverRegistry* SatSolverRegistry::getInstance() {
+ static SatSolverRegistry registry;
+ return ®istry;
+}
+
+SatSolverRegistry::~SatSolverRegistry() {
+ registry_type::const_iterator it = d_solvers.begin();
+ registry_type::const_iterator it_end = d_solvers.begin();
+ for (; it != it_end; ++ it) {
+ delete it->second;
+ }
+}
--- /dev/null
+/********************* */
+/*! \file sat_solver_registry.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): barrett, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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 instantiatiation 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 SatSolverConstrutor.
+ */
+ 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());
+
+}
+}
+
#include "util/options.h"
#include "util/output.h"
#include "util/dump.h"
+#include "prop/sat_solver_factory.h"
#include "cvc4autoconfig.h"
--debug | -d debug something (e.g. -d arith), can repeat\n\
--show-debug-tags show all avalable tags for debugging\n\
--show-trace-tags show all avalable tags for tracing\n\
+ --show-sat-solvers show all available SAT solvers\n\
--default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
--print-expr-types print types with variables when printing exprs\n\
--lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\
USE_MMAP,
SHOW_DEBUG_TAGS,
SHOW_TRACE_TAGS,
+ SHOW_SAT_SOLVERS,
SHOW_CONFIG,
STRICT_PARSING,
DEFAULT_EXPR_DEPTH,
{ "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION },
{ "show-debug-tags", no_argument , NULL, SHOW_DEBUG_TAGS },
{ "show-trace-tags", no_argument , NULL, SHOW_TRACE_TAGS },
+ { "show-sat-solvers", no_argument , NULL, SHOW_SAT_SOLVERS },
{ "show-config", no_argument , NULL, SHOW_CONFIG },
{ "segv-nospin", no_argument , NULL, SEGV_NOSPIN },
{ "help" , no_argument , NULL, 'h' },
exit(0);
break;
+ case SHOW_SAT_SOLVERS:
+ {
+ vector<string> solvers;
+ prop::SatSolverFactory::getSolverIds(solvers);
+ printf("Available SAT solvers: ");
+ for (unsigned i = 0; i < solvers.size(); ++ i) {
+ if (i > 0) {
+ printf(", ");
+ }
+ printf("%s", solvers[i].c_str());
+ }
+ printf("\n");
+ exit(0);
+ break;
+ }
case SHOW_CONFIG:
fputs(Configuration::about().c_str(), stdout);
printf("\n");
projects / cvc5.git / commitdiff