Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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                 :            :  * Learner for literals asserted at level zero.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "prop/lemma_inprocess.h"
      17                 :            : 
      18                 :            : #include "expr/node_algorithm.h"
      19                 :            : #include "options/theory_options.h"
      20                 :            : #include "prop/zero_level_learner.h"
      21                 :            : #include "smt/env.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : namespace prop {
      25                 :            : 
      26                 :          5 : LemmaInprocess::LemmaInprocess(Env& env, CnfStream* cs, ZeroLevelLearner& zll)
      27                 :            :     : EnvObj(env),
      28                 :            :       d_cs(cs),
      29                 :         10 :       d_tsmap(zll.getSimplifications()),
      30                 :         10 :       d_subsLitMap(userContext()),
      31                 :          5 :       d_eqLitLemmas(userContext())
      32                 :            : {
      33                 :          5 : }
      34                 :          3 : TrustNode LemmaInprocess::inprocessLemma(TrustNode& trn)
      35                 :            : {
      36         [ -  + ]:          3 :   if (trn.getKind() == TrustNodeKind::CONFLICT)
      37                 :            :   {
      38                 :          0 :     return trn;
      39                 :            :   }
      40                 :          6 :   const Node& proven = trn.getProven();
      41                 :          6 :   Node provenp = processInternal(proven);
      42         [ +  - ]:          3 :   if (provenp != proven)
      43                 :            :   {
      44         [ +  - ]:          6 :     Trace("lemma-inprocess-lemma")
      45                 :          3 :         << "Inprocess " << proven << " returns " << provenp << std::endl;
      46                 :            :     // proofs not supported
      47                 :          3 :     return TrustNode::mkTrustNode(trn.getKind(), provenp);
      48                 :            :   }
      49                 :          0 :   return trn;
      50                 :            : }
      51                 :            : 
      52                 :          3 : Node LemmaInprocess::processInternal(const Node& lem)
      53                 :            : {
      54                 :          6 :   std::vector<Node> eqLitLemmas;
      55                 :          3 :   NodeManager* nm = nodeManager();
      56                 :          6 :   std::unordered_map<TNode, Node> visited;
      57                 :          3 :   std::unordered_map<TNode, Node>::iterator it;
      58                 :          6 :   std::vector<TNode> visit;
      59                 :          3 :   context::CDHashMap<Node, Node>::iterator its;
      60                 :          6 :   TNode cur;
      61                 :          3 :   visit.emplace_back(lem);
      62                 :         15 :   do
      63                 :            :   {
      64                 :         18 :     cur = visit.back();
      65         [ +  - ]:         18 :     Trace("lemma-inprocess-visit") << "visit " << cur << std::endl;
      66 [ -  + ][ -  + ]:         18 :     Assert(cur.getType().isBoolean());
                 [ -  - ]
      67                 :         18 :     it = visited.find(cur);
      68         [ +  + ]:         18 :     if (it == visited.end())
      69                 :            :     {
      70         [ +  + ]:         12 :       if (expr::isBooleanConnective(cur))
      71                 :            :       {
      72                 :          6 :         visited[cur] = Node::null();
      73                 :          6 :         visit.insert(visit.end(), cur.begin(), cur.end());
      74                 :            :       }
      75                 :            :       else
      76                 :            :       {
      77                 :          6 :         visit.pop_back();
      78                 :            :         // literal case
      79                 :          6 :         bool prevLit = d_cs->hasLiteral(cur);
      80                 :          6 :         Node scur = d_tsmap.get().apply(cur, d_env.getRewriter());
      81                 :          6 :         its = d_subsLitMap.find(scur);
      82         [ -  + ]:          6 :         if (its != d_subsLitMap.end())
      83                 :            :         {
      84         [ -  - ]:          0 :           if (cur != its->second)
      85                 :            :           {
      86         [ -  - ]:          0 :             Trace("lemma-inprocess")
      87                 :          0 :                 << "Replace (indirect): " << cur << " -> " << its->second
      88                 :          0 :                 << ", prevLit = " << prevLit << std::endl;
      89                 :          0 :             visited[cur] = its->second;
      90                 :          0 :             continue;
      91                 :            :           }
      92                 :            :         }
      93                 :            :         else
      94                 :            :         {
      95                 :          6 :           bool currLit = prevLit;
      96         [ +  + ]:          6 :           if (scur != cur)
      97                 :            :           {
      98                 :          3 :             currLit = d_cs->hasLiteral(scur);
      99                 :          3 :             scur = rewrite(scur);
     100         [ +  - ]:          6 :             Trace("lemma-inprocess-debug")
     101                 :          3 :                 << "Inprocess " << cur << " -> " << scur << std::endl;
     102                 :          3 :             bool doReplace = false;
     103    [ +  + ][ - ]:          3 :             switch (options().theory.lemmaInprocess)
     104                 :            :             {
     105                 :          2 :               case options::LemmaInprocessMode::FULL:
     106                 :          2 :                 doReplace = (scur.isConst() || currLit || !prevLit);
     107                 :          2 :                 break;
     108                 :          1 :               case options::LemmaInprocessMode::LIGHT:
     109                 :          1 :                 doReplace = (scur.isConst() || (currLit && !prevLit));
     110                 :          1 :                 break;
     111                 :          0 :               default: break;
     112                 :            :             }
     113         [ +  - ]:          3 :             if (doReplace)
     114                 :            :             {
     115                 :          3 :               if (options().theory.lemmaInprocessInferEqLit
     116 [ +  + ][ -  + ]:          3 :                   && ((scur.isConst() || currLit) && prevLit))
         [ -  - ][ +  - ]
                 [ +  + ]
     117                 :            :               {
     118                 :            :                 // inferred they are equivalent? maybe should send clause here?
     119                 :          3 :                 Node eql = rewrite(scur.eqNode(cur));
     120         [ +  - ]:          1 :                 if (d_eqLitLemmas.find(eql) == d_eqLitLemmas.end())
     121                 :            :                 {
     122                 :          1 :                   d_eqLitLemmas.insert(eql);
     123                 :          1 :                   eqLitLemmas.emplace_back(eql);
     124                 :            :                 }
     125                 :            :               }
     126         [ +  - ]:          6 :               Trace("lemma-inprocess")
     127                 :          0 :                   << "Replace: " << cur << " -> " << scur
     128                 :          0 :                   << ", currLit = " << currLit << ", prevLit = " << prevLit
     129                 :          3 :                   << std::endl;
     130                 :          3 :               visited[cur] = scur;
     131                 :          3 :               d_subsLitMap[scur] = scur;
     132                 :          3 :               continue;
     133                 :            :             }
     134                 :            :           }
     135                 :          3 :           d_subsLitMap[scur] = cur;
     136                 :            :         }
     137                 :          3 :         visited[cur] = cur;
     138                 :            :       }
     139                 :          9 :       continue;
     140                 :            :     }
     141                 :          6 :     visit.pop_back();
     142         [ +  - ]:          6 :     if (it->second.isNull())
     143                 :            :     {
     144                 :         12 :       Node ret = cur;
     145                 :          6 :       bool childChanged = false;
     146                 :         12 :       std::vector<Node> children;
     147         [ +  + ]:         15 :       for (const Node& cn : cur)
     148                 :            :       {
     149                 :          9 :         it = visited.find(cn);
     150 [ -  + ][ -  + ]:          9 :         Assert(it != visited.end());
                 [ -  - ]
     151 [ -  + ][ -  + ]:          9 :         Assert(!it->second.isNull());
                 [ -  - ]
     152 [ +  - ][ +  + ]:          9 :         childChanged = childChanged || cn != it->second;
     153                 :          9 :         children.push_back(it->second);
     154                 :            :       }
     155         [ +  - ]:          6 :       if (childChanged)
     156                 :            :       {
     157                 :          6 :         ret = nm->mkNode(cur.getKind(), children);
     158                 :          6 :         ret = rewrite(ret);
     159                 :            :       }
     160                 :          6 :       visited[cur] = ret;
     161                 :            :     }
     162         [ +  + ]:         18 :   } while (!visit.empty());
     163 [ -  + ][ -  + ]:          3 :   Assert(visited.find(lem) != visited.end());
                 [ -  - ]
     164 [ -  + ][ -  + ]:          3 :   Assert(!visited.find(lem)->second.isNull());
                 [ -  - ]
     165                 :          6 :   Node ret = visited[lem];
     166         [ +  + ]:          3 :   if (!eqLitLemmas.empty())
     167                 :            :   {
     168                 :          1 :     eqLitLemmas.emplace_back(ret);
     169                 :          1 :     return nm->mkAnd(eqLitLemmas);
     170                 :            :   }
     171                 :          2 :   return ret;
     172                 :            : }
     173                 :            : 
     174                 :            : }  // namespace prop
     175                 :            : }  // namespace cvc5::internal