1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * Method for setting the default options of an SMT engine.
16 #ifndef CVC5__SMT__SET_DEFAULTS_H
17 #define CVC5__SMT__SET_DEFAULTS_H
19 #include "options/options.h"
20 #include "theory/logic_info.h"
26 * Class responsible for setting default options, which includes managing
27 * implied options and dependencies between the options and the logic.
33 * @param isInternalSubsolver Whether we are setting the options for an
34 * internal subsolver (see SmtEngine::isInternalSubsolver).
36 SetDefaults(bool isInternalSubsolver
);
38 * The purpose of this method is to set the default options and update the
39 * logic info for an SMT engine.
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
46 void setDefaults(LogicInfo
& logic
, Options
& opts
);
49 //------------------------- utility methods
51 * Determine whether we will be solving a SyGuS problem.
53 bool isSygus(const Options
& opts
) const;
55 * Determine whether we will be using SyGuS.
57 bool usesSygus(const Options
& opts
) const;
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.
62 bool mustDisableProofs(const Options
& opts
) const;
64 * Return true if we are using "safe" unsat cores, which disables all
65 * techniques that may interfere with producing correct unsat cores.
67 bool safeUnsatCores(const Options
& opts
) const;
68 //------------------------- options setting, prior finalization of logic
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
74 void setDefaultsPre(Options
& opts
);
75 //------------------------- finalization of the logic
77 * Finalize the logic based on the options.
79 void finalizeLogic(LogicInfo
& logic
, Options
& opts
) const;
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
85 void widenLogic(LogicInfo
& logic
, Options
& opts
) const;
86 //------------------------- options setting, post finalization of logic
88 * Set all default options, after we have finalized the logic.
90 void setDefaultsPost(const LogicInfo
& logic
, Options
& opts
) const;
92 * Set defaults related to quantifiers, called when quantifiers are enabled.
93 * This method modifies opt.quantifiers only.
95 void setDefaultsQuantifiers(const LogicInfo
& logic
, Options
& opts
) const;
97 * Set defaults related to SyGuS, called when SyGuS is enabled.
99 void setDefaultsSygus(Options
& opts
) const;
101 * Set default decision mode
103 void setDefaultDecisionMode(const LogicInfo
& logic
, Options
& opts
) const;
104 /** Are we an internal subsolver? */
105 bool d_isInternalSubsolver
;
111 #endif /* CVC5__SMT__SET_DEFAULTS_H */