Solver options

bin/pccheck.cpp

@@ -28,6 +28,7 @@
 #include "prgutil.h"
 #include "random_utils.h"
 #include "resolve.h"
+#include "solver_opt.h"
 #include "uccomp.h"
 #include "ucenc.h"
 #include "unitprop.h"
@@ -94,7 +95,7 @@ parse_arguments(int argc, char *argv[])
    opts.SetHelpDesc(prg_help);
    opts.SinglePositional({&conf.input_file, "input"});
    auto general_opts = opts.MakeOptionsGroup<SUBool::PCCheckGeneralOptions>();
-   auto solver_opts = opts.MakeOptionsGroup<SUBool::PCSolverOptions>();
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>(true);
    auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>(false);
    auto timeout_opts = opts.MakeOptionsGroup<SUBool::PCTimeoutsOptions>(false);
    auto cardinal_opt_group =

bin/pccompile.cpp

@@ -27,6 +27,7 @@
 #include "prgutil.h"
 #include "random_utils.h"
 #include "resolve.h"
+#include "solver_opt.h"
 #include "uccomp.h"
 #include "ucenc.h"
 #include "unitprop.h"
@@ -137,7 +138,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
    auto pclearncomp_opts = opts.MakeOptionsGroup<SUBool::PCLearnCompOptions>();
    auto preprocess_opts =
        opts.MakeOptionsGroup<SUBool::PCCompPreprocessOptions>();
-   auto solver_opts = opts.MakeOptionsGroup<SUBool::PCSolverOptions>();
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>(true);
    auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>(true);
    auto pccheck_random_opts =
        opts.MakeOptionsGroup<SUBool::PCRandomPCChecksOptions>();

lib/enum_opt.h

@@ -9,6 +9,7 @@
 #ifndef __ENUM_OPT_H
 #define __ENUM_OPT_H
 
+#include <boost/optional.hpp>
 #include <boost/program_options.hpp>
 #include <boost/smart_ptr/make_shared.hpp>
 
@@ -29,7 +30,7 @@ namespace SUBool
       const EnumAnnotation<T> &mEnumAnnotation;
       std::string mOptionName;
       std::string mOptionHelp;
-      T mDefaultValue;
+      boost::optional<T> mDefaultValue{};
 
       std::string mOptionValue{};
       boost::shared_ptr<po::option_description> mOptionDesc{};
@@ -37,6 +38,8 @@ namespace SUBool
     public:
       EnumOption(const EnumAnnotation<T> &enum_annotation, std::string opt_name,
           std::string opt_help, const T &default_value);
+      EnumOption(const EnumAnnotation<T> &enum_annotation, std::string opt_name,
+          std::string opt_help);
 
       boost::shared_ptr<po::option_description> Desc();
 
@@ -44,6 +47,7 @@ namespace SUBool
 
       T Value() const;
       bool GetValue(T &val) const;
+      bool Empty() const;
    };
 
    template <class T, typename... Args>
@@ -60,6 +64,14 @@ SUBool::EnumOption<T>::EnumOption(const EnumAnnotation<T> &enum_annotation,
 {
 }
 
+template <class T>
+SUBool::EnumOption<T>::EnumOption(const EnumAnnotation<T> &enum_annotation,
+    std::string opt_name, std::string opt_help)
+    : mEnumAnnotation(enum_annotation), mOptionName(std::move(opt_name)),
+      mOptionHelp(std::move(opt_help)), mDefaultValue()
+{
+}
+
 template <class T>
 boost::shared_ptr<po::option_description>
 SUBool::EnumOption<T>::Desc()
@@ -75,11 +87,21 @@ SUBool::EnumOption<T>::Desc()
       help += '\n';
       help += val.name + " = " + val.desc;
    }
-   return mOptionDesc =
-              boost::make_shared<po::option_description>(mOptionName.c_str(),
-                  po::value<std::string>(&mOptionValue)
-                      ->default_value(mEnumAnnotation.Name(mDefaultValue)),
-                  help.c_str());
+   if (mDefaultValue)
+   {
+      mOptionDesc =
+          boost::make_shared<po::option_description>(mOptionName.c_str(),
+              po::value<std::string>(&mOptionValue)
+                  ->default_value(mEnumAnnotation.Name(*mDefaultValue)),
+              help.c_str());
+   }
+   else
+   {
+      mOptionDesc =
+          boost::make_shared<po::option_description>(mOptionName.c_str(),
+              po::value<std::string>(&mOptionValue), help.c_str());
+   }
+   return mOptionDesc;
 }
 
 template <class T>
@@ -112,6 +134,13 @@ SUBool::EnumOption<T>::GetValue(T &val) const
    return true;
 }
 
+template <class T>
+bool
+SUBool::EnumOption<T>::Empty() const
+{
+   return mOptionValue.empty();
+}
+
 template <class T, typename... Args>
 auto
 SUBool::make_enum_option(const EnumAnnotation<T> &ann, Args &&...args)

lib/pc_opt.cpp

@@ -117,22 +117,6 @@ SUBool::PCCompPreprocessOptions::GetValues()
    return mPreprocessMethodOption.GetValue(mPreprocessMethod);
 }
 
-SUBool::PCSolverOptions::PCSolverOptions()
-    : OptionsGroup("Solvers"),
-      mSolverTypeOption(kSolverTypeAnnotation, "pccheck-solver",
-          "Solver to be used for the PC check. Only the available solvers are "
-          "listed.",
-          kDefaultSolverType)
-{
-   Add(mSolverTypeOption);
-}
-
-bool
-SUBool::PCSolverOptions::GetValues()
-{
-   return mSolverTypeOption.GetValue(mSolverType);
-}
-
 SUBool::PCOneProveOptions::PCOneProveOptions(bool add_compile_opts)
     : OptionsGroup("1-Provability Encoding"),
       mOneProveOption(AbsEncoder::kUPOneProveAnnotation, "one-prove,1",

lib/pc_opt.h

@@ -99,24 +99,6 @@ namespace SUBool
       AbsComp::PREPROCESS_METHOD PreprocessMethod() const;
    };
 
-   // Solver selection
-   class PCSolverOptions : public OptionsGroup
-   {
-    public:
-      static constexpr SOLVER_TYPE kDefaultSolverType = SOLVER_TYPE::GLUCOSE;
-
-    private:
-      EnumOption<SOLVER_TYPE> mSolverTypeOption;
-      SOLVER_TYPE mSolverType{kDefaultSolverType};
-
-    public:
-      PCSolverOptions();
-
-      virtual bool GetValues() override;
-
-      SOLVER_TYPE SolverType() const;
-   };
-
    class PCOneProveOptions : public OptionsGroup
    {
     public:
@@ -285,12 +267,6 @@ SUBool::PCCompPreprocessOptions::PreprocessMethod() const
    return mPreprocessMethod;
 }
 
-inline SUBool::SOLVER_TYPE
-SUBool::PCSolverOptions::SolverType() const
-{
-   return mSolverType;
-}
-
 inline SUBool::AbsEncoder::UP_ONE_PROVE
 SUBool::PCOneProveOptions::OneProve() const
 {

lib/solver_bind.cpp

@@ -87,18 +87,37 @@ SUBool::solver_wrapper(SOLVER_TYPE solver_type,
       return CadicalWrapper(collect_learnts, adapt);
 #else
       throw BadParameterException(
-          "AbsCheckerSAT::NewSolverWrapper", "Cadical support not available");
+          "solver_wrapper", "Cadical support not available");
 #endif
    case SOLVER_TYPE::KISSAT:
 #if HAS_KISSAT
       return KissatSolverWrapper(adapt);
 #else
       throw BadParameterException(
-          "AbsCheckerSAT::NewSolverWrapper", "Kissat support not available");
+          "solver_wrapper", "Kissat support not available");
 #endif
    default:
+      throw BadParameterException("solver_wrapper", "Unknown solver type");
+   }
+};
+
+SUBool::AbsSolverWrapper
+SUBool::inc_solver_wrapper(INC_SOLVER_TYPE solver_type,
+    bool collect_learnts [[maybe_unused]], SolverInterface::ADAPTATION adapt)
+{
+   switch (solver_type)
+   {
+   case INC_SOLVER_TYPE::GLUCOSE:
+      return SimpSolverWrapper(adapt);
+   case INC_SOLVER_TYPE::CADICAL:
+#if HAS_CADICAL
+      return CadicalWrapper(collect_learnts, adapt);
+#else
       throw BadParameterException(
-          "AbsCheckerSAT::NewSolverWrapper", "Unknown solver type");
+          "inc_solver_wrapper", "Cadical support not available");
+#endif
+   default:
+      throw BadParameterException("inc_solver_wrapper", "Unknown solver type");
    }
 };
 

lib/solver_bind.h

@@ -242,6 +242,11 @@ namespace SUBool
 
    AbsSolverWrapper solver_wrapper(SOLVER_TYPE solver_type,
        bool collect_learnts, SolverInterface::ADAPTATION adapt);
+   AbsSolverWrapper inc_solver_wrapper(INC_SOLVER_TYPE solver_type,
+       bool collect_learnts, SolverInterface::ADAPTATION adapt);
+
+   constexpr SOLVER_TYPE default_solver_type();
+   constexpr INC_SOLVER_TYPE default_inc_solver_type();
 
    template <class S> class SolverWrapperTemplate : public AbsSolverWrapper
    {
@@ -295,4 +300,34 @@ SUBool::SolverPool::NewSolver(Args &&...arg)
        std::make_unique<S>(std::forward<Args>(arg)...));
    return std::prev(mSolverList.end());
 }
+
+#if HAS_GLUCOSE
+constexpr SUBool::SOLVER_TYPE
+SUBool::default_solver_type()
+{
+   return SOLVER_TYPE::GLUCOSE;
+}
+constexpr SUBool::INC_SOLVER_TYPE
+SUBool::default_inc_solver_type()
+{
+   return INC_SOLVER_TYPE::GLUCOSE;
+}
+
+#elif HAS_CADICAL
+
+constexpr SUBool::SOLVER_TYPE
+SUBool::default_solver_type()
+{
+   return SOLVER_TYPE::CADICAL;
+}
+
+constexpr SUBool::INC_SOLVER_TYPE
+SUBool::default_inc_solver_type()
+{
+   return INC_SOLVER_TYPE::CADICAL;
+}
+#else
+#error No incremental solver available
+#endif // HAS_CADICAL or HAS_GLUCOSE
+
 #endif

lib/solver_opt.cpp

+/*
+ * Project SUBool
+ * Petr Kucera, 2022
+ */
+/**@file solver_opt.cpp
+ * Solver selection options group.
+ */
+
+#include "solver_opt.h"
+
+SUBool::SolverOptions::SolverOptions(bool pccheck_solver_type)
+    : OptionsGroup("Solvers"),
+      mSolverTypeOption(kSolverTypeAnnotation, "pccheck-solver",
+          "Solver to be used for the PC check. Default is to have the same "
+          "solver for PC checks as the solver for other queries which is given "
+          "by option --solver. Only the available solvers are listed."),
+      mIncSolverTypeOption(kIncSolverTypeAnnotation, "solver",
+          "General purpose solver, must be an incremental solver.",
+          default_inc_solver_type())
+{
+   if (pccheck_solver_type)
+   {
+      Add(mIncSolverTypeOption);
+      Add(mSolverTypeOption);
+   }
+}
+
+bool
+SUBool::SolverOptions::GetValues()
+{
+   if (!mIncSolverTypeOption.GetValue(mIncSolverType))
+   {
+      return false;
+   }
+   if (!mSolverTypeOption.Empty())
+   {
+      SOLVER_TYPE solver_type;
+      if (!mSolverTypeOption.GetValue(solver_type))
+      {
+         return false;
+      }
+      mSolverType = solver_type;
+   }
+   return true;
+}
+

lib/solver_opt.h

+/*
+ * Project SUBool
+ * Petr Kucera, 2022
+ */
+/**@file solver_opt.h
+ * Solver selection options group.
+ */
+
+#ifndef __SOLVER_OPT_H
+#define __SOLVER_OPT_H
+
+#include <boost/optional.hpp>
+
+#include "enum_opt.h"
+#include "prg_opt_group.h"
+#include "solver_bind.h"
+
+namespace SUBool
+{
+   // Solver selection
+   class SolverOptions : public OptionsGroup
+   {
+    private:
+      EnumOption<SOLVER_TYPE> mSolverTypeOption;
+      EnumOption<INC_SOLVER_TYPE> mIncSolverTypeOption;
+
+      boost::optional<SOLVER_TYPE> mSolverType{};
+      INC_SOLVER_TYPE mIncSolverType{default_inc_solver_type()};
+
+    public:
+      SolverOptions(bool pccheck_solver_type);
+
+      virtual bool GetValues() override;
+
+      SOLVER_TYPE SolverType() const;
+      INC_SOLVER_TYPE IncSolverType() const;
+   };
+} // namespace SUBool
+
+inline SUBool::SOLVER_TYPE
+SUBool::SolverOptions::SolverType() const
+{
+   if (mSolverType)
+   {
+      return *mSolverType;
+   }
+   switch (mIncSolverType)
+   {
+   case INC_SOLVER_TYPE::GLUCOSE:
+      return SOLVER_TYPE::GLUCOSE;
+   case INC_SOLVER_TYPE::CADICAL:
+      return SOLVER_TYPE::CADICAL;
+   default:
+      throw BadParameterException(
+          "SolverOptions::SolverType", "Unknown inc solver type");
+   }
+}
+
+inline SUBool::INC_SOLVER_TYPE
+SUBool::SolverOptions::IncSolverType() const
+{
+   return mIncSolverType;
+}
+#endif