src/smt/smt_solver.h

   1 /*********************                                                        */
   2 /*! \file smt_solver.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Aina Niemetz
   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 The solver for SMT queries in an SmtEngine.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__SMT__SMT_SOLVER_H
  18 #define CVC4__SMT__SMT_SOLVER_H
  19
  20 #include <vector>
  21
  22 #include "expr/node.h"
  23 #include "theory/logic_info.h"
  24 #include "util/result.h"
  25
  26 namespace CVC4 {
  27
  28 class SmtEngine;
  29 class TheoryEngine;
  30 class ResourceManager;
  31 class ProofNodeManager;
  32
  33 namespace prop {
  34 class PropEngine;
  35 }
  36
  37 namespace theory {
  38 class QuantifiersEngine;
  39 }
  40
  41 namespace smt {
  42
  43 class Assertions;
  44 class SmtEngineState;
  45 class Preprocessor;
  46 struct SmtEngineStatistics;
  47
  48 /**
  49  * A solver for SMT queries.
  50  *
  51  * This class manages the initialization of the theory engine and propositional
  52  * engines and implements the method for checking satisfiability of the current
  53  * set of assertions.
  54  *
  55  * Notice that this class is only conceptually responsible for running
  56  * check-sat commands and an interface for sending formulas to the underlying
  57  * classes. It does not implement any query techniques beyond getting the result
  58  * (unsat/sat/unknown) of check-sat calls. More detailed information (e.g.
  59  * models) can be queries using other classes that examine the state of the
  60  * TheoryEngine directly, which can be accessed via getTheoryEngine.
  61  */
  62 class SmtSolver
  63 {
  64  public:
  65   SmtSolver(SmtEngine& smt,
  66             SmtEngineState& state,
  67             ResourceManager* rm,
  68             Preprocessor& pp,
  69             SmtEngineStatistics& stats);
  70   ~SmtSolver();
  71   /**
  72    * Create theory engine, prop engine based on the logic info.
  73    */
  74   void finishInit(const LogicInfo& logicInfo);
  75   /** Reset all assertions, global declarations, etc.  */
  76   void resetAssertions();
  77   /**
  78    * Interrupt a running query.  This can be called from another thread
  79    * or from a signal handler.  Throws a ModalException if the SmtSolver
  80    * isn't currently in a query.
  81    */
  82   void interrupt();
  83   /**
  84    * This is called by the destructor of SmtEngine, just before destroying the
  85    * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
  86    * is important because there are destruction ordering issues
  87    * between PropEngine and Theory.
  88    */
  89   void shutdown();
  90   /**
  91    * Check satisfiability (used to check satisfiability and entailment)
  92    * in SmtEngine. This is done via adding assumptions (when necessary) to
  93    * assertions as, preprocessing and pushing assertions into the prop engine
  94    * of this class, and checking for satisfiability via the prop engine.
  95    *
  96    * @param as The object managing the assertions in SmtEngine. This class
  97    * maintains a current set of (unprocessed) assertions which are pushed
  98    * into the internal members of this class (TheoryEngine and PropEngine)
  99    * during this call.
 100    * @param assumptions The assumptions for this check-sat call, which are
 101    * temporary assertions.
 102    * @param inUnsatCore Whether assumptions are in the unsat core.
 103    * @param isEntailmentCheck Whether this is an entailment check (assumptions
 104    * are negated in this case).
 105    */
 106   Result checkSatisfiability(Assertions& as,
 107                              const std::vector<Node>& assumptions,
 108                              bool inUnsatCore,
 109                              bool isEntailmentCheck);
 110   /**
 111    * Process the assertions that have been asserted in as. This moves the set of
 112    * assertions that have been buffered into as, preprocesses them, pushes them
 113    * into the SMT solver, and clears the buffer.
 114    */
 115   void processAssertions(Assertions& as);
 116   /**
 117    * Set proof node manager. Enables proofs in this SmtSolver. Should be
 118    * called before finishInit.
 119    */
 120   void setProofNodeManager(ProofNodeManager* pnm);
 121   //------------------------------------------ access methods
 122   /** Get a pointer to the TheoryEngine owned by this solver. */
 123   TheoryEngine* getTheoryEngine();
 124   /** Get a pointer to the PropEngine owned by this solver. */
 125   prop::PropEngine* getPropEngine();
 126   /** Get a pointer to the QuantifiersEngine owned by this solver. */
 127   theory::QuantifiersEngine* getQuantifiersEngine();
 128   /** Get a pointer to the preprocessor */
 129   Preprocessor* getPreprocessor();
 130   //------------------------------------------ end access methods
 131  private:
 132   /** Reference to the parent SMT engine */
 133   SmtEngine& d_smt;
 134   /** Reference to the state of the SmtEngine */
 135   SmtEngineState& d_state;
 136   /** Pointer to a resource manager (owned by SmtEngine) */
 137   ResourceManager* d_rm;
 138   /** Reference to the preprocessor of SmtEngine */
 139   Preprocessor& d_pp;
 140   /** Reference to the statistics of SmtEngine */
 141   SmtEngineStatistics& d_stats;
 142   /**
 143    * Pointer to the proof node manager used by this SmtSolver. A non-null
 144    * proof node manager indicates that proofs are enabled.
 145    */
 146   ProofNodeManager* d_pnm;
 147   /** The theory engine */
 148   std::unique_ptr<TheoryEngine> d_theoryEngine;
 149   /** The propositional engine */
 150   std::unique_ptr<prop::PropEngine> d_propEngine;
 151 };
 152
 153 }  // namespace smt
 154 }  // namespace CVC4
 155
 156 #endif /* CVC4__SMT__SMT_SOLVER_H */