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 #include "smt/env_obj.h"
  27
  28 namespace cvc5 {
  29 namespace smt {
  30
  31 class AbstractValues;
  32
  33 /**
  34  * Contains all information pertaining to the assertions of an SMT engine.
  35  *
  36  * This class is responsible for setting up the assertions pipeline for
  37  * check-sat calls. It is *not* responsible for the preprocessing itself, and
  38  * instead is intended to be the input to a preprocessor utility.
  39  */
  40 class Assertions : protected EnvObj
  41 {
  42   /** The type of our internal assertion list */
  43   typedef context::CDList<Node> AssertionList;
  44
  45  public:
  46   Assertions(Env& env, AbstractValues& absv);
  47   ~Assertions();
  48   /**
  49    * Finish initialization, called once after options are finalized. Sets up
  50    * the required bookkeeping based on the options.
  51    */
  52   void finishInit();
  53   /**
  54    * Clears out the non-context-dependent data in this class.  Necessary to
  55    * clear out our assertion vectors in case someone does a push-assert-pop
  56    * without a check-sat.
  57    */
  58   void clearCurrent();
  59   /*
  60    * Initialize a call to check satisfiability. This adds assumptions to
  61    * the list of assumptions maintained by this class, and finalizes the
  62    * set of formulas (in the assertions pipeline) that will be used for the
  63    * upcoming check-sat call.
  64    *
  65    * @param assumptions The assumptions of the upcoming check-sat call.
  66    * @param isEntailmentCheck Whether we are checking entailment of assumptions
  67    * in the upcoming check-sat call.
  68    */
  69   void initializeCheckSat(const std::vector<Node>& assumptions,
  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.
  76    *
  77    * @throw TypeCheckingException, LogicException, UnsafeInterruptException
  78    */
  79   void assertFormula(const Node& n);
  80   /**
  81    * Assert that n corresponds to an assertion from a define-fun or
  82    * define-fun-rec command.
  83    * This assertion is added to the set of assertions maintained by this class.
  84    * If this has a global definition, this assertion is persistent for any
  85    * subsequent check-sat calls.
  86    */
  87   void addDefineFunDefinition(Node n, bool global);
  88   /**
  89    * Get the assertions pipeline, which contains the set of assertions we are
  90    * currently processing.
  91    */
  92   preprocessing::AssertionPipeline& getAssertionPipeline();
  93   /**
  94    * Get assertions list corresponding to the original list of assertions,
  95    * before preprocessing. This includes assertions corresponding to define-fun
  96    * and define-fun-rec.
  97    */
  98   const context::CDList<Node>& getAssertionList() const;
  99   /**
 100    * Get assertions list corresponding to the original list of assertions
 101    * that correspond to definitions (define-fun or define-fun-rec).
 102    */
 103   const context::CDList<Node>& getAssertionListDefinitions() const;
 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 isAssumption,
 149                   bool isFunDef,
 150                   bool maybeHasFv);
 151   /** Reference to the abstract values utility */
 152   AbstractValues& d_absValues;
 153   /** Whether we are producing assertions */
 154   bool d_produceAssertions;
 155   /**
 156    * The assertion list (before any conversion) for supporting getAssertions().
 157    */
 158   AssertionList d_assertionList;
 159   /** The subset of above the correspond to define-fun or define-fun-rec */
 160   AssertionList d_assertionListDefs;
 161   /**
 162    * List of lemmas generated for global (recursive) function definitions. We
 163    * assert this list of definitions in each check-sat call.
 164    */
 165   std::unique_ptr<std::vector<Node>> d_globalDefineFunLemmas;
 166   /**
 167    * The list of assumptions from the previous call to checkSatisfiability.
 168    * Note that if the last call to checkSatisfiability was an entailment check,
 169    * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains
 170    * one single assumption ~(a1 AND ... AND an).
 171    */
 172   std::vector<Node> d_assumptions;
 173   /** Whether we did a global negation of the formula. */
 174   bool d_globalNegation;
 175   /** Assertions in the preprocessing pipeline */
 176   preprocessing::AssertionPipeline d_assertions;
 177 };
 178
 179 }  // namespace smt
 180 }  // namespace cvc5
 181
 182 #endif