src/theory/smt_engine_subsolver.h

   1 /*********************                                                        */
   2 /*! \file smt_engine_subsolver.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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
  11  **
  12  ** \brief Utilities for initializing subsolvers (copies of SmtEngine) during
  13  ** solving.
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
  19 #define CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
  20
  21 #include <map>
  22 #include <memory>
  23 #include <vector>
  24
  25 #include "expr/expr_manager.h"
  26 #include "expr/node.h"
  27 #include "smt/smt_engine.h"
  28
  29 namespace CVC4 {
  30 namespace theory {
  31
  32 /**
  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.
  36  *
  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
  39  * this method.
  40  *
  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.
  44  *
  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)
  48  */
  49 void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
  50                          bool needsTimeout = false,
  51                          unsigned long timeout = 0);
  52
  53 /**
  54  * This returns the result of checking the satisfiability of formula query.
  55  *
  56  * If necessary, smte is initialized to the SMT engine that checked its
  57  * satisfiability.
  58  */
  59 Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
  60                           Node query,
  61                           bool needsTimeout = false,
  62                           unsigned long timeout = 0);
  63
  64 /**
  65  * This returns the result of checking the satisfiability of formula query.
  66  *
  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.
  69  *
  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)
  73  */
  74 Result checkWithSubsolver(Node query,
  75                           bool needsTimeout = false,
  76                           unsigned long timeout = 0);
  77
  78 /**
  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
  81  * into modelVars.
  82  *
  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)
  88  */
  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);
  94
  95 }  // namespace theory
  96 }  // namespace CVC4
  97
  98 #endif /* CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H */