src/smt/set_defaults.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Method for setting the default options of an SMT engine.
  14  */
  15
  16 #ifndef CVC5__SMT__SET_DEFAULTS_H
  17 #define CVC5__SMT__SET_DEFAULTS_H
  18
  19 #include "options/options.h"
  20 #include "theory/logic_info.h"
  21
  22 namespace cvc5 {
  23 namespace smt {
  24
  25 /**
  26  * Class responsible for setting default options, which includes managing
  27  * implied options and dependencies between the options and the logic.
  28  */
  29 class SetDefaults
  30 {
  31  public:
  32   /**
  33    * @param isInternalSubsolver Whether we are setting the options for an
  34    * internal subsolver (see SmtEngine::isInternalSubsolver).
  35    */
  36   SetDefaults(bool isInternalSubsolver);
  37   /**
  38    * The purpose of this method is to set the default options and update the
  39    * logic info for an SMT engine.
  40    *
  41    * @param logic A reference to the logic of SmtEngine, which can be
  42    * updated by this method based on the current options and the logic itself.
  43    * @param opts The options to modify, typically the main options of the
  44    * SmtEngine in scope.
  45    */
  46   void setDefaults(LogicInfo& logic, Options& opts);
  47
  48  private:
  49   //------------------------- utility methods
  50   /**
  51    * Determine whether we will be solving a SyGuS problem.
  52    */
  53   bool isSygus(const Options& opts) const;
  54   /**
  55    * Determine whether we will be using SyGuS.
  56    */
  57   bool usesSygus(const Options& opts) const;
  58   /**
  59    * Return true if proofs must be disabled. This is the case for any technique
  60    * that answers "unsat" without showing a proof of unsatisfiabilty.
  61    */
  62   bool mustDisableProofs(const Options& opts) const;
  63   /**
  64    * Return true if we are using "safe" unsat cores, which disables all
  65    * techniques that may interfere with producing correct unsat cores.
  66    */
  67   bool safeUnsatCores(const Options& opts) const;
  68   //------------------------- options setting, prior finalization of logic
  69   /**
  70    * Set defaults pre, which sets all options prior to finalizing the logic.
  71    * It is required that any options that impact the finalization of logic
  72    * (finalizeLogic).
  73    */
  74   void setDefaultsPre(Options& opts);
  75   //------------------------- finalization of the logic
  76   /**
  77    * Finalize the logic based on the options.
  78    */
  79   void finalizeLogic(LogicInfo& logic, Options& opts) const;
  80   /**
  81    * Widen logic to theories that are required, since some theories imply the
  82    * use of other theories to handle certain operators, e.g. UF to handle
  83    * partial functions.
  84    */
  85   void widenLogic(LogicInfo& logic, Options& opts) const;
  86   //------------------------- options setting, post finalization of logic
  87   /**
  88    * Set all default options, after we have finalized the logic.
  89    */
  90   void setDefaultsPost(const LogicInfo& logic, Options& opts) const;
  91   /**
  92    * Set defaults related to quantifiers, called when quantifiers are enabled.
  93    * This method modifies opt.quantifiers only.
  94    */
  95   void setDefaultsQuantifiers(const LogicInfo& logic, Options& opts) const;
  96   /**
  97    * Set defaults related to SyGuS, called when SyGuS is enabled.
  98    */
  99   void setDefaultsSygus(Options& opts) const;
 100   /**
 101    * Set default decision mode
 102    */
 103   void setDefaultDecisionMode(const LogicInfo& logic, Options& opts) const;
 104   /** Are we an internal subsolver? */
 105   bool d_isInternalSubsolver;
 106 };
 107
 108 }  // namespace smt
 109 }  // namespace cvc5
 110
 111 #endif /* CVC5__SMT__SET_DEFAULTS_H */