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/node.h"
  26 #include "smt/smt_engine.h"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30
  31 /**
  32  * This function initializes the smt engine smte to check the satisfiability
  33  * of the argument "query". It takes the logic and options of the current
  34  * SMT engine in scope.
  35  *
  36  * Notice this method intentionally does not fully initialize smte. This means
  37  * that the options of smte can still be modified after it is returned by
  38  * this method.
  39  *
  40  * Notice that some aspects of subsolvers are not incoporated by this call.
  41  * For example, the type of separation logic heaps is not set on smte, even
  42  * if the current SMT engine has declared a separation logic heap.
  43  *
  44  * @param smte The smt engine pointer to initialize
  45  * @param needsTimeout Whether we would like to set a timeout
  46  * @param timeout The timeout (in milliseconds)
  47  */
  48 void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
  49                          bool needsTimeout = false,
  50                          unsigned long timeout = 0);
  51
  52 /**
  53  * This returns the result of checking the satisfiability of formula query.
  54  *
  55  * If necessary, smte is initialized to the SMT engine that checked its
  56  * satisfiability.
  57  */
  58 Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
  59                           Node query,
  60                           bool needsTimeout = false,
  61                           unsigned long timeout = 0);
  62
  63 /**
  64  * This returns the result of checking the satisfiability of formula query.
  65  *
  66  * In contrast to above, this is used if the user of this method is not
  67  * concerned with the state of the SMT engine after the check.
  68  *
  69  * @param query The query to check
  70  * @param needsTimeout Whether we would like to set a timeout
  71  * @param timeout The timeout (in milliseconds)
  72  */
  73 Result checkWithSubsolver(Node query,
  74                           bool needsTimeout = false,
  75                           unsigned long timeout = 0);
  76
  77 /**
  78  * This returns the result of checking the satisfiability of formula query.
  79  * Additionally, if the query is satisfiable, it adds the model values for vars
  80  * into modelVars.
  81  *
  82  * @param query The query to check
  83  * @param vars The variables we are interesting in getting a model for.
  84  * @param modelVals A vector storing the model values of variables in vars.
  85  * @param needsTimeout Whether we would like to set a timeout
  86  * @param timeout The timeout (in milliseconds)
  87  */
  88 Result checkWithSubsolver(Node query,
  89                           const std::vector<Node>& vars,
  90                           std::vector<Node>& modelVals,
  91                           bool needsTimeout = false,
  92                           unsigned long timeout = 0);
  93
  94 }  // namespace theory
  95 }  // namespace CVC4
  96
  97 #endif /* CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H */