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 checker
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/oracle_checker.h"
      14                 :            : 
      15                 :            : #include "expr/node_algorithm.h"
      16                 :            : #include "options/base_options.h"
      17                 :            : #include "smt/env.h"
      18                 :            : #include "smt/logic_exception.h"
      19                 :            : #include "theory/rewriter.h"
      20                 :            : 
      21                 :            : namespace cvc5::internal {
      22                 :            : namespace theory {
      23                 :            : namespace quantifiers {
      24                 :            : 
      25                 :       1070 : OracleChecker::OracleChecker(Env& env)
      26                 :       1070 :     : EnvObj(env), NodeConverter(env.getNodeManager())
      27                 :            : {
      28                 :       1070 : }
      29                 :            : 
      30                 :       1182 : Node OracleChecker::checkConsistent(Node app, Node val)
      31                 :            : {
      32                 :       1184 :   Node result = evaluateApp(app);
      33         [ +  - ]:       2360 :   Trace("oracle-calls") << "checkConsistent " << app << " == " << result
      34                 :       1180 :                         << " vs " << val << std::endl;
      35         [ +  + ]:       1180 :   if (result != val)
      36                 :            :   {
      37                 :        966 :     return result;
      38                 :            :   }
      39                 :        214 :   return Node::null();
      40                 :       1180 : }
      41                 :            : 
      42                 :       1182 : Node OracleChecker::evaluateApp(Node app)
      43                 :            : {
      44 [ -  + ][ -  + ]:       1182 :   Assert(app.getKind() == Kind::APPLY_UF);
                 [ -  - ]
      45                 :       1182 :   Node f = app.getOperator();
      46 [ -  + ][ -  + ]:       1182 :   Assert(OracleCaller::isOracleFunction(f));
                 [ -  - ]
      47                 :            :   // get oracle caller
      48         [ +  + ]:       1182 :   if (d_callers.find(f) == d_callers.end())
      49                 :            :   {
      50                 :        326 :     d_callers.insert(std::pair<Node, OracleCaller>(f, OracleCaller(f)));
      51                 :            :   }
      52                 :       1182 :   OracleCaller& caller = d_callers.at(f);
      53                 :            : 
      54                 :            :   // get oracle result
      55                 :       1182 :   std::vector<Node> retv;
      56                 :       1182 :   bool ranOracle = caller.callOracle(app, retv);
      57         [ -  + ]:       1182 :   if (retv.size() != 1)
      58                 :            :   {
      59                 :          0 :     DebugUnhandled() << "Failed to evaluate " << app
      60                 :          0 :                      << " to a single return value, got: " << retv << std::endl;
      61                 :            :     return app;
      62                 :            :   }
      63                 :       1182 :   Node ret = retv[0];
      64                 :       1182 :   ret = rewrite(ret);
      65         [ +  - ]:       1182 :   if (ranOracle)
      66                 :            :   {
      67                 :            :     // prints the result of the oracle, if it was computed in the call above.
      68                 :            :     // this prints the original application, its result, and the exit code
      69                 :            :     // of the binary.
      70                 :       1182 :     d_env.output(options::OutputTag::ORACLES)
      71                 :       1182 :         << "(oracle-call " << app << " " << ret << ")" << std::endl;
      72                 :            :   }
      73         [ +  + ]:       1182 :   if (ret.getNodeManager() != app.getNodeManager())
      74                 :            :   {
      75                 :          2 :     throw LogicException(
      76                 :            :         "Evaluated an oracle call that is not associated with the term manager "
      77                 :          4 :         "of this solver");
      78                 :            :   }
      79         [ -  + ]:       3540 :   if (!CVC5_EQUAL(ret.getType(), app.getType()))
      80                 :            :   {
      81                 :          0 :     std::stringstream ss;
      82                 :          0 :     ss << "Evaluated an oracle call with an unexpected type: " << app << " = "
      83                 :          0 :        << ret << " whose type is " << ret.getType() << ", expected "
      84                 :          0 :        << app.getType();
      85                 :          0 :     throw LogicException(ss.str());
      86                 :          0 :   }
      87 [ -  + ][ -  + ]:       1180 :   Assert(!ret.isNull());
                 [ -  - ]
      88                 :       1180 :   return ret;
      89                 :       1186 : }
      90                 :            : 
      91                 :          0 : Node OracleChecker::evaluate(Node n)
      92                 :            : {
      93                 :            :   // same as convert
      94                 :          0 :   return convert(n);
      95                 :            : }
      96                 :            : 
      97                 :          0 : Node OracleChecker::postConvert(Node n)
      98                 :            : {
      99         [ -  - ]:          0 :   Trace("oracle-checker-debug") << "postConvert: " << n << std::endl;
     100                 :            :   // if it is an oracle function applied to constant arguments
     101                 :          0 :   if (n.getKind() == Kind::APPLY_UF
     102                 :          0 :       && OracleCaller::isOracleFunction(n.getOperator()))
     103                 :            :   {
     104                 :          0 :     bool allConst = true;
     105         [ -  - ]:          0 :     for (const Node& nc : n)
     106                 :            :     {
     107         [ -  - ]:          0 :       if (nc.isConst())
     108                 :            :       {
     109                 :          0 :         continue;
     110                 :            :       }
     111                 :            :       // special case: assume all closed lambdas are constants
     112         [ -  - ]:          0 :       if (nc.getKind() == Kind::LAMBDA)
     113                 :            :       {
     114                 :            :         // if the lambda does not have a free variable (BOUND_VARIABLE)
     115         [ -  - ]:          0 :         if (!expr::hasFreeVar(nc))
     116                 :            :         {
     117                 :            :           // it also cannot have any free symbol
     118                 :          0 :           std::unordered_set<Node> syms;
     119                 :          0 :           expr::getSymbols(nc, syms);
     120         [ -  - ]:          0 :           if (syms.empty())
     121                 :            :           {
     122                 :          0 :             continue;
     123                 :            :           }
     124         [ -  - ]:          0 :         }
     125                 :            :       }
     126                 :            :       // non-constant argument, fail
     127                 :          0 :       allConst = false;
     128                 :          0 :       break;
     129         [ -  - ]:          0 :     }
     130         [ -  - ]:          0 :     if (allConst)
     131                 :            :     {
     132                 :            :       // evaluate the application
     133                 :          0 :       return evaluateApp(n);
     134                 :            :     }
     135                 :            :   }
     136                 :            :   // otherwise, always rewrite
     137                 :          0 :   return rewrite(n);
     138                 :            : }
     139                 :          0 : bool OracleChecker::hasOracles() const { return !d_callers.empty(); }
     140                 :          0 : bool OracleChecker::hasOracleCalls(Node f) const
     141                 :            : {
     142                 :          0 :   std::map<Node, OracleCaller>::const_iterator it = d_callers.find(f);
     143                 :          0 :   return it != d_callers.end();
     144                 :            : }
     145                 :          0 : const std::map<Node, std::vector<Node>>& OracleChecker::getOracleCalls(
     146                 :            :     Node f) const
     147                 :            : {
     148                 :          0 :   Assert(hasOracleCalls(f));
     149                 :          0 :   std::map<Node, OracleCaller>::const_iterator it = d_callers.find(f);
     150                 :          0 :   return it->second.getCachedResults();
     151                 :            : }
     152                 :            : 
     153                 :            : }  // namespace quantifiers
     154                 :            : }  // namespace theory
     155                 :            : }  // namespace cvc5::internal