From: Dejan Jovanović Date: Mon, 26 Mar 2012 19:42:25 +0000 (+0000) Subject: Global registry of SAT solvers, where they are registered at compile time. The availa... X-Git-Tag: cvc5-1.0.0~8261 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6fdc62f34bb1d04b84dfd628ec16335b8f02385e;p=cvc5.git Global registry of SAT solvers, where they are registered at compile time. The available SAT solvers can be seen with the --show-sat-solvers option. --- diff --git a/.cproject b/.cproject index 6467c05f2..bcc6a9ca5 100644 --- a/.cproject +++ b/.cproject @@ -326,6 +326,14 @@ true true + + make + -j10 + check + true + true + true + make -j10 diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index c1dc3b828..e505c168e 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -17,7 +17,9 @@ libprop_la_SOURCES = \ 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 diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 043aa5d24..86fbe4433 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -19,6 +19,7 @@ #pragma once #include "prop/sat_solver.h" +#include "prop/sat_solver_registry.h" #include "prop/bvminisat/simp/SimpSolver.h" namespace CVC4 { @@ -27,8 +28,8 @@ namespace prop { class MinisatSatSolver: public BVSatSolverInterface { BVMinisat::SimpSolver* d_minisat; - MinisatSatSolver(); public: + MinisatSatSolver(); ~MinisatSatSolver(); void addClause(SatClause& clause, bool removable); @@ -76,9 +77,10 @@ public: }; Statistics d_statistics; - friend class SatSolverFactory; }; +template class SatSolverConstructor; + } } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 549c0b679..66aca717d 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -19,6 +19,7 @@ #pragma once #include "prop/sat_solver.h" +#include "prop/sat_solver_registry.h" #include "prop/minisat/simp/SimpSolver.h" namespace CVC4 { @@ -36,11 +37,11 @@ class DPLLMinisatSatSolver : public DPLLSatSolverInterface { /** 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); @@ -93,9 +94,10 @@ public: }; Statistics d_statistics; - friend class SatSolverFactory; }; +template class SatSolverConstructor; + } // prop namespace } // cvc4 namespace diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index eb694852c..61c67ed5f 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -21,7 +21,8 @@ #ifndef __CVC4__PROP__SAT_MODULE_H #define __CVC4__PROP__SAT_MODULE_H -#include +#include +#include #include "util/options.h" #include "util/stats.h" #include "context/cdlist.h" @@ -166,7 +167,6 @@ public: /** 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; diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index fbb244789..c5972d7bb 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -17,6 +17,7 @@ **/ #include "prop/sat_solver_factory.h" +#include "prop/sat_solver_registry.h" #include "prop/minisat/minisat.h" #include "prop/bvminisat/bvminisat.h" @@ -31,6 +32,16 @@ DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { 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& solvers) { + SatSolverRegistry::getSolverIds(solvers); +} diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 09d66b8d4..367397fdf 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -20,6 +20,8 @@ #include "cvc4_public.h" +#include +#include #include "prop/sat_solver.h" namespace CVC4 { @@ -27,8 +29,15 @@ namespace prop { 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& solvers); + }; } diff --git a/src/prop/sat_solver_registry.cpp b/src/prop/sat_solver_registry.cpp new file mode 100644 index 000000000..01434bd80 --- /dev/null +++ b/src/prop/sat_solver_registry.cpp @@ -0,0 +1,61 @@ +/********************* */ +/*! \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& 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; + } +} diff --git a/src/prop/sat_solver_registry.h b/src/prop/sat_solver_registry.h new file mode 100644 index 000000000..df1cf86f8 --- /dev/null +++ b/src/prop/sat_solver_registry.h @@ -0,0 +1,118 @@ +/********************* */ +/*! \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 +#include +#include +#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 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 + 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& solvers); + + /** The Constructors are friends, since they need to register */ + template + friend class SatSolverConstructor; + +}; + +/** + * Declare an instance of this class with the SAT solver in order to put it in the registry. + */ +template +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 +const size_t SatSolverConstructor::s_solverId = SatSolverRegistry::getInstance()->registerSolver(typeid(Solver).name()); + +} +} + diff --git a/src/util/options.cpp b/src/util/options.cpp index d3426e152..b6956a31b 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -35,6 +35,7 @@ #include "util/options.h" #include "util/output.h" #include "util/dump.h" +#include "prop/sat_solver_factory.h" #include "cvc4autoconfig.h" @@ -163,6 +164,7 @@ Additional CVC4 options:\n\ --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\ @@ -324,6 +326,7 @@ enum OptionValue { USE_MMAP, SHOW_DEBUG_TAGS, SHOW_TRACE_TAGS, + SHOW_SAT_SOLVERS, SHOW_CONFIG, STRICT_PARSING, DEFAULT_EXPR_DEPTH, @@ -399,6 +402,7 @@ static struct option cmdlineOptions[] = { { "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' }, @@ -930,6 +934,21 @@ throw(OptionException) { exit(0); break; + case SHOW_SAT_SOLVERS: + { + vector 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");