1 /********************* */
2 /*! \file smt_engine_subsolver.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Utilities for initializing subsolvers (copies of SmtEngine) during
16 #include "cvc4_private.h"
18 #ifndef CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
19 #define CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
25 #include "expr/expr_manager.h"
26 #include "expr/node.h"
27 #include "smt/smt_engine.h"
33 * This function initializes the smt engine smte to check the satisfiability
34 * of the argument "query". It takes the logic and options of the current
35 * SMT engine in scope.
37 * Notice this method intentionally does not fully initialize smte. This means
38 * that the options of smte can still be modified after it is returned by
41 * Notice that some aspects of subsolvers are not incoporated by this call.
42 * For example, the type of separation logic heaps is not set on smte, even
43 * if the current SMT engine has declared a separation logic heap.
45 * @param smte The smt engine pointer to initialize
46 * @param needsTimeout Whether we would like to set a timeout
47 * @param timeout The timeout (in milliseconds)
49 void initializeSubsolver(std::unique_ptr
<SmtEngine
>& smte
,
50 bool needsTimeout
= false,
51 unsigned long timeout
= 0);
54 * This returns the result of checking the satisfiability of formula query.
56 * If necessary, smte is initialized to the SMT engine that checked its
59 Result
checkWithSubsolver(std::unique_ptr
<SmtEngine
>& smte
,
61 bool needsTimeout
= false,
62 unsigned long timeout
= 0);
65 * This returns the result of checking the satisfiability of formula query.
67 * In contrast to above, this is used if the user of this method is not
68 * concerned with the state of the SMT engine after the check.
70 * @param query The query to check
71 * @param needsTimeout Whether we would like to set a timeout
72 * @param timeout The timeout (in milliseconds)
74 Result
checkWithSubsolver(Node query
,
75 bool needsTimeout
= false,
76 unsigned long timeout
= 0);
79 * This returns the result of checking the satisfiability of formula query.
80 * Additionally, if the query is satisfiable, it adds the model values for vars
83 * @param query The query to check
84 * @param vars The variables we are interesting in getting a model for.
85 * @param modelVals A vector storing the model values of variables in vars.
86 * @param needsTimeout Whether we would like to set a timeout
87 * @param timeout The timeout (in milliseconds)
89 Result
checkWithSubsolver(Node query
,
90 const std::vector
<Node
>& vars
,
91 std::vector
<Node
>& modelVals
,
92 bool needsTimeout
= false,
93 unsigned long timeout
= 0);
98 #endif /* CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H */