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