prop/sat_solver_types.h \
prop/sat_solver_factory.h \
prop/sat_solver_factory.cpp \
- prop/sat_solver_registry.h \
- prop/sat_solver_registry.cpp \
- prop/options_handlers.h \
smt/smt_engine.cpp \
smt/smt_engine_check_proof.cpp \
smt/smt_engine.h \
#pragma once
#include "prop/sat_solver.h"
-#include "prop/sat_solver_registry.h"
#include "prop/bvminisat/simp/SimpSolver.h"
#include "context/cdo.h"
#pragma once
#include "prop/sat_solver.h"
-#include "prop/sat_solver_registry.h"
#include "prop/minisat/simp/SimpSolver.h"
namespace CVC4 {
module PROP "prop/options.h" SAT layer
-option - --show-sat-solvers void :handler CVC4::prop::showSatSolvers :handler-include "prop/options_handlers.h"
- show all available SAT solvers
-
option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate greater_equal(0.0) less_equal(1.0)
sets the frequency of random decisions in the sat solver (P=0.0 by default)
option satRandomSeed random-seed --random-seed=S uint32_t :default 0 :read-write
+++ /dev/null
-/********************* */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PROP__OPTIONS_HANDLERS_H
-#define __CVC4__PROP__OPTIONS_HANDLERS_H
-
-#include "prop/sat_solver_factory.h"
-#include <string>
-#include <vector>
-
-namespace CVC4 {
-namespace prop {
-
-inline void showSatSolvers(std::string option, SmtEngine* smt) {
- std::vector<std::string> solvers;
- 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);
-}
-
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PROP__OPTIONS_HANDLERS_H */
**/
#include "prop/sat_solver_factory.h"
-#include "prop/sat_solver_registry.h"
#include "prop/minisat/minisat.h"
#include "prop/bvminisat/bvminisat.h"
namespace CVC4 {
namespace prop {
-template class SatSolverConstructor<MinisatSatSolver>;
-template class SatSolverConstructor<BVMinisatSatSolver>;
-
BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, const std::string& name) {
return new BVMinisatSatSolver(mainSatContext, name);
}
return new MinisatSatSolver();
}
-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);
-}
-
} /* CVC4::prop namespace */
} /* CVC4 namespace */
static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, const std::string& name = "");
static DPLLSatSolverInterface* createDPLLMinisat();
- static SatSolver* create(const char* id);
-
- /** Get the solver ids that are available */
- static void getSolverIds(std::vector<std::string>& solvers);
-
};/* class SatSolverFactory */
}/* CVC4::prop namespace */
+++ /dev/null
-/********************* */
-/*! \file sat_solver_registry.cpp
- ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 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
- **/
-
-#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.end();
- for (; it != it_end; ++ it) {
- delete it->second;
- }
- d_solvers.clear();
-}
+++ /dev/null
-/********************* */
-/*! \file sat_solver_registry.h
- ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 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());
-
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
projects / cvc5.git / commitdiff