src/smt/assertions.h

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