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 theory engine module based on a user plugin.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/plugin_module.h"
      14                 :            : 
      15                 :            : #include "expr/skolem_manager.h"
      16                 :            : #include "smt/env.h"
      17                 :            : #include "theory/trust_substitutions.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : namespace theory {
      21                 :            : 
      22                 :         28 : PluginModule::PluginModule(Env& env, TheoryEngine* theoryEngine, Plugin* p)
      23                 :         56 :     : TheoryEngineModule(env, theoryEngine, "Plugin::" + p->getName()),
      24                 :         56 :       d_plugin(p)
      25                 :            : {
      26                 :         28 : }
      27                 :            : 
      28                 :         91 : void PluginModule::check(CVC5_UNUSED Theory::Effort e)
      29                 :            : {
      30                 :            :   // ignore the effort level?
      31                 :         91 :   std::vector<Node> lems = d_plugin->check();
      32                 :            :   // returned vector is taken as lemmas
      33         [ +  + ]:        104 :   for (const Node& lem : lems)
      34                 :            :   {
      35 [ -  + ][ -  + ]:         13 :     Assert(lem.getType().isBoolean());
                 [ -  - ]
      36                 :            :     // must apply top level substitutions here, since if this lemma was
      37                 :            :     // sent externally, it may not have taken into account the internal
      38                 :            :     // substitutions.
      39                 :         13 :     Node slem = d_env.getTopLevelSubstitutions().apply(lem);
      40                 :            :     // send the lemma
      41                 :         13 :     d_out.lemma(slem, InferenceId::PLUGIN_LEMMA);
      42                 :         13 :   }
      43                 :         91 : }
      44                 :            : 
      45                 :         60 : void PluginModule::notifyLemma(TNode n,
      46                 :            :                                CVC5_UNUSED InferenceId id,
      47                 :            :                                CVC5_UNUSED LemmaProperty p,
      48                 :            :                                const std::vector<Node>& skAsserts,
      49                 :            :                                CVC5_UNUSED const std::vector<Node>& sks)
      50                 :            : {
      51                 :            :   // must take original form as a way to remove internal symbols from the lemma
      52                 :         60 :   notifyLemmaInternal(n);
      53                 :            :   // skolem lemmas are also included
      54         [ +  + ]:         62 :   for (const Node& kn : skAsserts)
      55                 :            :   {
      56                 :          2 :     notifyLemmaInternal(kn);
      57                 :            :   }
      58                 :            :   // currently ignores the other fields, e.g. property and sks
      59                 :         60 : }
      60                 :            : 
      61                 :         62 : void PluginModule::notifyLemmaInternal(const Node& n)
      62                 :            : {
      63                 :         62 :   Node ns = d_env.getSharableFormula(n);
      64         [ +  - ]:         62 :   if (!ns.isNull())
      65                 :            :   {
      66                 :         62 :     d_plugin->notifyTheoryLemma(ns);
      67                 :            :   }
      68                 :         62 : }
      69                 :            : 
      70                 :            : }  // namespace theory
      71                 :            : }  // namespace cvc5::internal