src/smt/assertions.h

   1 /*********************                                                        */
   2 /*! \file assertions.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Andres Noetzli
   6  ** This file is part of the CVC4 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.\endverbatim
  11  **
  12  ** \brief The module for storing assertions for an SMT engine.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC5__SMT__ASSERTIONS_H
  18 #define CVC5__SMT__ASSERTIONS_H
  19
  20 #include <vector>
  21
  22 #include "context/cdlist.h"
  23 #include "expr/node.h"
  24 #include "preprocessing/assertion_pipeline.h"
  25
  26 namespace cvc5 {
  27 namespace smt {
  28
  29 class AbstractValues;
  30
  31 /**
  32  * Contains all information pertaining to the assertions of an SMT engine.
  33  *
  34  * This class is responsible for setting up the assertions pipeline for
  35  * check-sat calls. It is *not* responsible for the preprocessing itself, and
  36  * instead is intended to be the input to a preprocessor utility.
  37  */
  38 class Assertions
  39 {
  40   /** The type of our internal assertion list */
  41   typedef context::CDList<Node> AssertionList;
  42
  43  public:
  44   Assertions(context::UserContext* u, AbstractValues& absv);
  45   ~Assertions();
  46   /**
  47    * Finish initialization, called once after options are finalized. Sets up
  48    * the required bookkeeping based on the options.
  49    */
  50   void finishInit();
  51   /**
  52    * Clears out the non-context-dependent data in this class.  Necessary to
  53    * clear out our assertion vectors in case someone does a push-assert-pop
  54    * without a check-sat.
  55    */
  56   void clearCurrent();
  57   /*
  58    * Initialize a call to check satisfiability. This adds assumptions to
  59    * the list of assumptions maintained by this class, and finalizes the
  60    * set of formulas (in the assertions pipeline) that will be used for the
  61    * upcoming check-sat call.
  62    *
  63    * @param assumptions The assumptions of the upcoming check-sat call.
  64    * @param inUnsatCore Whether assumptions are in the unsat core.
  65    * @param isEntailmentCheck Whether we are checking entailment of assumptions
  66    * in the upcoming check-sat call.
  67    */
  68   void initializeCheckSat(const std::vector<Node>& assumptions,
  69                           bool inUnsatCore,
  70                           bool isEntailmentCheck);
  71   /**
  72    * Add a formula to the current context: preprocess, do per-theory
  73    * setup, use processAssertionList(), asserting to T-solver for
  74    * literals and conjunction of literals.  Returns false if
  75    * immediately determined to be inconsistent.  This version
  76    * takes a Boolean flag to determine whether to include this asserted
  77    * formula in an unsat core (if one is later requested).
  78    *
  79    * @throw TypeCheckingException, LogicException, UnsafeInterruptException
  80    */
  81   void assertFormula(const Node& n, bool inUnsatCore = true);
  82   /**
  83    * Assert that n corresponds to an assertion from a define-fun-rec command.
  84    * This assertion is added to the set of assertions maintained by this class.
  85    * If this has a global definition, this assertion is persistent for any
  86    * subsequent check-sat calls.
  87    */
  88   void addDefineFunRecDefinition(Node n, bool global);
  89   /**
  90    * Get the assertions pipeline, which contains the set of assertions we are
  91    * currently processing.
  92    */
  93   preprocessing::AssertionPipeline& getAssertionPipeline();
  94   /**
  95    * Get assertions list corresponding to the original list of assertions,
  96    * before preprocessing.
  97    */
  98   context::CDList<Node>* getAssertionList();
  99   /**
 100    * Get the list of assumptions, which are those registered to this class
 101    * on initializeCheckSat.
 102    */
 103   std::vector<Node>& getAssumptions();
 104   /**
 105    * Is the set of assertions globally negated? When this flag is true, the
 106    * overall result of check-sat should be inverted.
 107    */
 108   bool isGlobalNegated() const;
 109   /** Flip the global negation flag. */
 110   void flipGlobalNegated();
 111
 112   //------------------------------------ for proofs
 113   /** Set proof generator */
 114   void setProofGenerator(smt::PreprocessProofGenerator* pppg);
 115   /** Is proof enabled? */
 116   bool isProofEnabled() const;
 117   //------------------------------------ end for proofs
 118  private:
 119   /**
 120    * Fully type-check the argument, and also type-check that it's
 121    * actually Boolean.
 122    * throw@ TypeCheckingException
 123    */
 124   void ensureBoolean(const Node& n);
 125   /**
 126    * Adds a formula to the current context.  Action here depends on
 127    * the SimplificationMode (in the current Options scope); the
 128    * formula might be pushed out to the propositional layer
 129    * immediately, or it might be simplified and kept, or it might not
 130    * even be simplified.
 131    * The arguments isInput and isAssumption are used for bookkeeping for unsat
 132    * cores.
 133    * The argument maybeHasFv should be set to true if the assertion may have
 134    * free variables. By construction, assertions from the smt2 parser are
 135    * guaranteed not to have free variables. However, other cases such as
 136    * assertions from the SyGuS parser may have free variables (say if the
 137    * input contains an assert or define-fun-rec command).
 138    *
 139    * @param isAssumption If true, the formula is considered to be an assumption
 140    * (this is used to distinguish assertions and assumptions)
 141    */
 142   void addFormula(TNode n,
 143                   bool inUnsatCore,
 144                   bool inInput,
 145                   bool isAssumption,
 146                   bool maybeHasFv);
 147   /** pointer to the user context */
 148   context::UserContext* d_userContext;
 149   /** Reference to the abstract values utility */
 150   AbstractValues& d_absValues;
 151   /**
 152    * The assertion list (before any conversion) for supporting
 153    * getAssertions().  Only maintained if in incremental mode.
 154    */
 155   AssertionList* d_assertionList;
 156   /**
 157    * List of lemmas generated for global recursive function definitions. We
 158    * assert this list of definitions in each check-sat call.
 159    */
 160   std::unique_ptr<std::vector<Node>> d_globalDefineFunRecLemmas;
 161   /**
 162    * The list of assumptions from the previous call to checkSatisfiability.
 163    * Note that if the last call to checkSatisfiability was an entailment check,
 164    * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains
 165    * one single assumption ~(a1 AND ... AND an).
 166    */
 167   std::vector<Node> d_assumptions;
 168   /** Whether we did a global negation of the formula. */
 169   bool d_globalNegation;
 170   /** Assertions in the preprocessing pipeline */
 171   preprocessing::AssertionPipeline d_assertions;
 172 };
 173
 174 }  // namespace smt
 175 }  // namespace cvc5
 176
 177 #endif