Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * A "valuation" proxy for TheoryEngine
      11                 :            :  *
      12                 :            :  * A "valuation" proxy for TheoryEngine.  This class breaks the dependence
      13                 :            :  * of theories' getValue() implementations on TheoryEngine.  getValue()
      14                 :            :  * takes a Valuation, which delegates to TheoryEngine.
      15                 :            :  */
      16                 :            : 
      17                 :            : #include "cvc5_private.h"
      18                 :            : 
      19                 :            : #ifndef CVC5__THEORY__VALUATION_H
      20                 :            : #define CVC5__THEORY__VALUATION_H
      21                 :            : 
      22                 :            : #include "context/cdlist.h"
      23                 :            : #include "expr/node.h"
      24                 :            : #include "options/theory_options.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : 
      28                 :            : class TheoryEngine;
      29                 :            : 
      30                 :            : namespace theory {
      31                 :            : 
      32                 :            : struct Assertion;
      33                 :            : class TheoryModel;
      34                 :            : class SortInference;
      35                 :            : 
      36                 :            : /**
      37                 :            :  * The status of an equality in the current context.
      38                 :            :  */
      39                 :            : enum EqualityStatus {
      40                 :            :   /** The equality is known to be true and has been propagated */
      41                 :            :   EQUALITY_TRUE_AND_PROPAGATED,
      42                 :            :   /** The equality is known to be false and has been propagated */
      43                 :            :   EQUALITY_FALSE_AND_PROPAGATED,
      44                 :            :   /** The equality is known to be true */
      45                 :            :   EQUALITY_TRUE,
      46                 :            :   /** The equality is known to be false */
      47                 :            :   EQUALITY_FALSE,
      48                 :            :   /** The equality is not known, but is true in the current model */
      49                 :            :   EQUALITY_TRUE_IN_MODEL,
      50                 :            :   /** The equality is not known, but is false in the current model */
      51                 :            :   EQUALITY_FALSE_IN_MODEL,
      52                 :            :   /** The equality is completely unknown */
      53                 :            :   EQUALITY_UNKNOWN
      54                 :            : };/* enum EqualityStatus */
      55                 :            : 
      56                 :            : std::ostream& operator<<(std::ostream& os, EqualityStatus s);
      57                 :            : 
      58                 :            : /**
      59                 :            :  * Returns true if the two statuses are compatible, i.e. both TRUE
      60                 :            :  * or both FALSE (regardless of inmodel/propagation).
      61                 :            :  */
      62                 :            : bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
      63                 :            : 
      64                 :            : class Valuation {
      65                 :            :   TheoryEngine* d_engine;
      66                 :            : public:
      67                 :     749862 :   Valuation(TheoryEngine* engine) :
      68                 :     749862 :     d_engine(engine) {
      69                 :     749862 :   }
      70                 :            : 
      71                 :            :   /**
      72                 :            :    * Return true if n has an associated SAT literal
      73                 :            :    */
      74                 :            :   bool isSatLiteral(TNode n) const;
      75                 :            : 
      76                 :            :   /**
      77                 :            :    * Get the current SAT assignment to the node n.
      78                 :            :    *
      79                 :            :    * This is only permitted if n is a theory atom that has an associated
      80                 :            :    * SAT literal (or its negation).
      81                 :            :    *
      82                 :            :    * @return Node::null() if no current assignment; otherwise true or false.
      83                 :            :    */
      84                 :            :   Node getSatValue(TNode n) const;
      85                 :            : 
      86                 :            :   /**
      87                 :            :    * Returns true if the node has a current SAT assignment. If yes, the
      88                 :            :    * argument "value" is set to its value.
      89                 :            :    *
      90                 :            :    * This is only permitted if n is a theory atom that has an associated
      91                 :            :    * SAT literal.
      92                 :            :    *
      93                 :            :    * @return true if the literal has a current assignment, and returns the
      94                 :            :    * value in the "value" argument; otherwise false and the "value"
      95                 :            :    * argument is unmodified.
      96                 :            :    */
      97                 :            :   bool hasSatValue(TNode n, bool& value) const;
      98                 :            :   /**
      99                 :            :    * Same as above, without setting the value.
     100                 :            :    */
     101                 :            :   bool hasSatValue(TNode n) const;
     102                 :            : 
     103                 :            :   /**
     104                 :            :    * Returns the equality status of the two terms, from the theory that owns the domain type.
     105                 :            :    * The types of a and b must be the same.
     106                 :            :    */
     107                 :            :   EqualityStatus getEqualityStatus(TNode a, TNode b);
     108                 :            : 
     109                 :            :   /**
     110                 :            :    * Returns the candidate model value of the shared term (or null if not
     111                 :            :    * available). A candidate model value is one computed at full effort,
     112                 :            :    * prior to running theory combination and final model construction.
     113                 :            :    */
     114                 :            :   Node getCandidateModelValue(TNode var);
     115                 :            : 
     116                 :            :   /**
     117                 :            :    * Returns pointer to model. This model is only valid during last call effort
     118                 :            :    * check.
     119                 :            :    */
     120                 :            :   TheoryModel* getModel();
     121                 :            :   /**
     122                 :            :    * Returns a pointer to the sort inference module, which lives in TheoryEngine
     123                 :            :    * and is non-null when options::sortInference is true.
     124                 :            :    */
     125                 :            :   SortInference* getSortInference();
     126                 :            : 
     127                 :            :   //-------------------------------------- static configuration of the model
     128                 :            :   /**
     129                 :            :    * Set that k is an unevaluated kind in the TheoryModel, if it exists.
     130                 :            :    * See TheoryModel::setUnevaluatedKind for details.
     131                 :            :    */
     132                 :            :   void setUnevaluatedKind(Kind k);
     133                 :            :   /**
     134                 :            :    * Set that k is an unevaluated kind in the TheoryModel, if it exists.
     135                 :            :    * See TheoryModel::setSemiEvaluatedKind for details.
     136                 :            :    */
     137                 :            :   void setSemiEvaluatedKind(Kind k);
     138                 :            :   /**
     139                 :            :    * Set that k is an irrelevant kind in the TheoryModel, if it exists.
     140                 :            :    * See TheoryModel::setIrrelevantKind for details.
     141                 :            :    */
     142                 :            :   void setIrrelevantKind(Kind k);
     143                 :            :   //-------------------------------------- end static configuration of the model
     144                 :            : 
     145                 :            :   /**
     146                 :            :    * Ensure that the given node will have a designated SAT literal
     147                 :            :    * that is definitionally equal to it.  The result of this function
     148                 :            :    * is a Node that can be queried via getSatValue().
     149                 :            :    *
     150                 :            :    * Note that this call may add lemmas to the SAT solver corresponding to the
     151                 :            :    * definition of subterms eliminated by preprocessing.
     152                 :            :    *
     153                 :            :    * @return the actual node that's been "literalized," which may
     154                 :            :    * differ from the input due to theory-rewriting and preprocessing,
     155                 :            :    * as well as CNF conversion
     156                 :            :    */
     157                 :            :   CVC5_WARN_UNUSED_RESULT Node ensureLiteral(TNode n);
     158                 :            : 
     159                 :            :   /**
     160                 :            :    * This returns the theory-preprocessed form of term n. The theory
     161                 :            :    * preprocessed form of a term t is one returned by
     162                 :            :    * TheoryPreprocess::preprocess (see theory/theory_preprocess.h). In
     163                 :            :    * particular, the returned term has syntax sugar symbols eliminated
     164                 :            :    * (e.g. div, mod, partial datatype selectors), has term formulas (e.g. ITE
     165                 :            :    * terms eliminated) and has been rewritten.
     166                 :            :    *
     167                 :            :    * Note that this call may add lemmas to the SAT solver corresponding to the
     168                 :            :    * definition of subterms eliminated by preprocessing.
     169                 :            :    *
     170                 :            :    * @param n The node to preprocess
     171                 :            :    * @return The preprocessed form of n
     172                 :            :    */
     173                 :            :   Node getPreprocessedTerm(TNode n);
     174                 :            :   /**
     175                 :            :    * Same as above, but also tracks the skolems and their corresponding
     176                 :            :    * definitions in sks and skAsserts respectively.
     177                 :            :    */
     178                 :            :   Node getPreprocessedTerm(TNode n,
     179                 :            :                            std::vector<Node>& skAsserts,
     180                 :            :                            std::vector<Node>& sks);
     181                 :            : 
     182                 :            :   /**
     183                 :            :    * Returns whether the given lit (which must be a SAT literal) is a decision
     184                 :            :    * literal or not.  Throws an exception if lit is not a SAT literal.  "lit" may
     185                 :            :    * be in either phase; that is, if "lit" is a SAT literal, this function returns
     186                 :            :    * true both for lit and the negation of lit.
     187                 :            :    */
     188                 :            :   bool isDecision(Node lit) const;
     189                 :            : 
     190                 :            :   /**
     191                 :            :    * Return whether lit has a fixed SAT assignment (i.e., implied by input
     192                 :            :    * assertions).
     193                 :            :    */
     194                 :            :   bool isFixed(TNode lit) const;
     195                 :            : 
     196                 :            :   /**
     197                 :            :    * Get the assertion level of the SAT solver.
     198                 :            :    */
     199                 :            :   unsigned getAssertionLevel() const;
     200                 :            : 
     201                 :            :   /**
     202                 :            :    * Request an entailment check according to the given theoryOfMode.
     203                 :            :    * See theory.h for documentation on entailmentCheck().
     204                 :            :    */
     205                 :            :   std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
     206                 :            : 
     207                 :            :   /** need check ? */
     208                 :            :   bool needCheck() const;
     209                 :            : 
     210                 :            :   /**
     211                 :            :    * Is the literal lit (possibly) critical for satisfying the input formula in
     212                 :            :    * the current context? This call is applicable only during collectModelInfo
     213                 :            :    * or during LAST_CALL effort.
     214                 :            :    */
     215                 :            :   bool isRelevant(Node lit) const;
     216                 :            : 
     217                 :            :   /** is legal elimination
     218                 :            :    *
     219                 :            :    * Returns true if x -> val is a legal elimination of variable x. This is
     220                 :            :    * useful for ppAssert, when x = val is an entailed equality. This function
     221                 :            :    * determines whether indeed x can be eliminated from the problem via the
     222                 :            :    * substitution x -> val.
     223                 :            :    *
     224                 :            :    * The following criteria imply that x -> val is *not* a legal elimination:
     225                 :            :    * (1) If x is contained in val,
     226                 :            :    * (2) If the type of val is not the same as the type of x,
     227                 :            :    * (3) If val contains an operator that cannot be evaluated, and
     228                 :            :    * produceModels is true. For example, x -> sqrt(2) is not a legal
     229                 :            :    * elimination if we are producing models. This is because we care about the
     230                 :            :    * value of x, and its value must be computed (approximated) by the
     231                 :            :    * non-linear solver.
     232                 :            :    */
     233                 :            :   bool isLegalElimination(TNode x, TNode val);
     234                 :            : 
     235                 :            :   //------------------------------------------- access methods for assertions
     236                 :            :   /**
     237                 :            :    * The following methods are intended only to be used in limited use cases,
     238                 :            :    * for cases where a theory (e.g. quantifiers) requires knowing about the
     239                 :            :    * assertions from other theories.
     240                 :            :    */
     241                 :            :   /** The beginning iterator of facts for theory tid.*/
     242                 :            :   context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
     243                 :            :   /** The beginning iterator of facts for theory tid.*/
     244                 :            :   context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
     245                 :            : };/* class Valuation */
     246                 :            : 
     247                 :            : }  // namespace theory
     248                 :            : }  // namespace cvc5::internal
     249                 :            : 
     250                 :            : #endif /* CVC5__THEORY__VALUATION_H */