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                 :            :  * Learner for literals asserted at level zero.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__PROP__LEMMA_INPROCESS_H
      16                 :            : #define CVC5__PROP__LEMMA_INPROCESS_H
      17                 :            : 
      18                 :            : #include <unordered_set>
      19                 :            : 
      20                 :            : #include "context/cdhashset.h"
      21                 :            : #include "context/cdo.h"
      22                 :            : #include "expr/node.h"
      23                 :            : #include "prop/cnf_stream.h"
      24                 :            : #include "smt/env_obj.h"
      25                 :            : #include "theory/trust_substitutions.h"
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : 
      29                 :            : class TheoryEngine;
      30                 :            : 
      31                 :            : namespace prop {
      32                 :            : 
      33                 :            : class ZeroLevelLearner;
      34                 :            : 
      35                 :            : /**
      36                 :            :  * Lemma inprocess, which heuristically simplifies lemmas to an equivalent
      37                 :            :  * form based on the current simplifications stored by the zero level learner.
      38                 :            :  *
      39                 :            :  * The intution of this class is to increase the likelihood that literals in the
      40                 :            :  * SAT solver are reused. For example if a = 0 is learned at decision level
      41                 :            :  * zero, and there is a SAT literal P(0), if P(a) is introduced as a new literal
      42                 :            :  * in a lemma, we may replace it by P(0).
      43                 :            :  *
      44                 :            :  * As another example, if we learn a=b, c=b and we have a literal P(a), then
      45                 :            :  * we may replace P(c) with P(a).
      46                 :            :  *
      47                 :            :  * This simplification is done selectively and will never replace a known SAT
      48                 :            :  * literal by a new SAT literal. Further policies are determined by
      49                 :            :  * lemma-inprocess-mode.
      50                 :            :  *
      51                 :            :  * Generally this method can only be applied to lemmas where the structure of
      52                 :            :  * the lemma is not important. This includes quantifier instantiation lemmas
      53                 :            :  * for example.
      54                 :            :  */
      55                 :            : class LemmaInprocess : protected EnvObj
      56                 :            : {
      57                 :            :   using NodeSet = context::CDHashSet<Node>;
      58                 :            : 
      59                 :            :  public:
      60                 :            :   LemmaInprocess(Env& env, CnfStream* cs, ZeroLevelLearner& zll);
      61                 :         10 :   ~LemmaInprocess() {}
      62                 :            :   /** Inprocess lemma */
      63                 :            :   TrustNode inprocessLemma(TrustNode& trn);
      64                 :            : 
      65                 :            :  private:
      66                 :            :   /**
      67                 :            :    * Process internal, returns an equivalent formula to lem, assuming d_tsmap.
      68                 :            :    */
      69                 :            :   Node processInternal(const Node& lem);
      70                 :            :   /** Pointer to CNF stream */
      71                 :            :   CnfStream* d_cs;
      72                 :            :   /** Reference to the current available simplification */
      73                 :            :   theory::TrustSubstitutionMap& d_tsmap;
      74                 :            :   /** Mapping from simplified literals to a known SAT literal */
      75                 :            :   context::CDHashMap<Node, Node> d_subsLitMap;
      76                 :            :   /** Equivalent literal lemmas we have sent */
      77                 :            :   context::CDHashSet<Node> d_eqLitLemmas;
      78                 :            : };
      79                 :            : 
      80                 :            : }  // namespace prop
      81                 :            : }  // namespace cvc5::internal
      82                 :            : 
      83                 :            : #endif