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                 :            :  * Oracle caller
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__EXPR__ORACLE_H
      16                 :            : #define CVC5__EXPR__ORACLE_H
      17                 :            : 
      18                 :            : #include <vector>
      19                 :            : 
      20                 :            : #include "expr/node.h"
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : 
      24                 :            : /**
      25                 :            :  * An oracle, which stores a function whose interface is from a vector of nodes
      26                 :            :  * to a vector of nodes. It is expected to serve as an oracle interface as
      27                 :            :  * described in Polgreen et al VMCAI 2022 and the SyGuS version 2.1 standard.
      28                 :            :  */
      29                 :            : class Oracle
      30                 :            : {
      31                 :            :  public:
      32                 :            :   /** Construct an oracle whose implementation is the given function. */
      33                 :       1070 :   Oracle(std::function<std::vector<Node>(const std::vector<Node>&)> fn)
      34                 :       1070 :       : d_fn(fn)
      35                 :            :   {
      36                 :       1070 :   }
      37                 :       1065 :   ~Oracle() {}
      38                 :            :   /** Run the function on the given input */
      39                 :       1182 :   std::vector<Node> run(const std::vector<Node>& input) const
      40                 :            :   {
      41                 :       1182 :     return d_fn(input);
      42                 :            :   }
      43                 :            :   /** Get the function for this oracle */
      44                 :        535 :   std::function<std::vector<Node>(const std::vector<Node>&)> getFunction() const
      45                 :            :   {
      46                 :        535 :     return d_fn;
      47                 :            :   }
      48                 :            : 
      49                 :            :  private:
      50                 :            :   /** The function for this oracle */
      51                 :            :   std::function<std::vector<Node>(const std::vector<Node>&)> d_fn;
      52                 :            : };
      53                 :            : 
      54                 :            : }  // namespace cvc5::internal
      55                 :            : 
      56                 :            : #endif /*CVC5__EXPR__ORACLE_H*/