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                 :            :  * The solver for interpolation queries.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "smt/interpolation_solver.h"
      14                 :            : 
      15                 :            : #include <sstream>
      16                 :            : 
      17                 :            : #include "base/modal_exception.h"
      18                 :            : #include "expr/node_algorithm.h"
      19                 :            : #include "options/quantifiers_options.h"
      20                 :            : #include "options/smt_options.h"
      21                 :            : #include "smt/env.h"
      22                 :            : #include "smt/set_defaults.h"
      23                 :            : #include "smt/sygus_solver.h"
      24                 :            : #include "theory/quantifiers/quantifiers_attributes.h"
      25                 :            : #include "theory/quantifiers/sygus/sygus_interpol.h"
      26                 :            : #include "theory/smt_engine_subsolver.h"
      27                 :            : #include "theory/trust_substitutions.h"
      28                 :            : 
      29                 :            : using namespace cvc5::internal::theory;
      30                 :            : 
      31                 :            : namespace cvc5::internal {
      32                 :            : namespace smt {
      33                 :            : 
      34                 :       1870 : InterpolationSolver::InterpolationSolver(Env& env) : EnvObj(env) {}
      35                 :            : 
      36                 :       3668 : InterpolationSolver::~InterpolationSolver() {}
      37                 :            : 
      38                 :        419 : bool InterpolationSolver::getInterpolant(const std::vector<Node>& axioms,
      39                 :            :                                          const Node& conj,
      40                 :            :                                          const TypeNode& grammarType,
      41                 :            :                                          Node& interpol)
      42                 :            : {
      43         [ -  + ]:        419 :   if (!options().smt.produceInterpolants)
      44                 :            :   {
      45                 :          0 :     const char* msg =
      46                 :            :         "Cannot get interpolation when produce-interpolants options is off.";
      47                 :          0 :     throw ModalException(msg);
      48                 :            :   }
      49                 :            :   // apply top-level substitutions
      50         [ +  - ]:        838 :   Trace("sygus-interpol") << "SolverEngine::getInterpol: conjecture " << conj
      51                 :        419 :                           << std::endl;
      52                 :            :   // We can apply top-level substitutions x -> t that are implied by the
      53                 :            :   // assertions but only if all symbols in (= x t) are also contained in the
      54                 :            :   // goal (to satisfy the shared symbol requirement of get-interpolant).
      55                 :            :   // We construct a subset of the top-level substitutions (tlShared) here that
      56                 :            :   // can legally be applied, and conjoin these with our final solution when
      57                 :            :   // applicable below.
      58                 :        419 :   SubstitutionMap& tls = d_env.getTopLevelSubstitutions().get();
      59                 :        419 :   SubstitutionMap tlsShared;
      60                 :        419 :   std::unordered_map<Node, Node> subs = tls.getSubstitutions();
      61                 :        419 :   std::unordered_set<Node> conjSyms;
      62                 :        419 :   expr::getSymbols(conj, conjSyms);
      63                 :        419 :   std::vector<Node> axiomsn;
      64         [ +  + ]:        489 :   for (const std::pair<const Node, Node>& s : subs)
      65                 :            :   {
      66                 :            :     // Furthermore note that if we have a target grammar, we cannot conjoin
      67                 :            :     // substitutions since this would violate the grammar from the user.
      68         [ +  + ]:         70 :     if (grammarType.isNull())
      69                 :            :     {
      70                 :         67 :       bool isShared = true;
      71                 :            :       // legal substitution if all variables in (= x t) also appear in the goal
      72         [ +  + ]:         67 :       if (conjSyms.find(s.first) == conjSyms.end())
      73                 :            :       {
      74                 :            :         // solved variable is not shared
      75                 :         51 :         isShared = false;
      76                 :            :       }
      77                 :            :       else
      78                 :            :       {
      79                 :         16 :         std::unordered_set<Node> ssyms;
      80                 :         16 :         expr::getSymbols(s.second, ssyms);
      81         [ +  + ]:         17 :         for (const Node& sym : ssyms)
      82                 :            :         {
      83         [ +  + ]:          5 :           if (conjSyms.find(sym) == conjSyms.end())
      84                 :            :           {
      85                 :            :             // variable in right hand side is not shared
      86                 :          4 :             isShared = false;
      87                 :          4 :             break;
      88                 :            :           }
      89                 :            :         }
      90                 :         16 :       }
      91         [ +  + ]:         67 :       if (isShared)
      92                 :            :       {
      93                 :            :         // can apply as a substitution
      94                 :         12 :         tlsShared.addSubstitution(s.first, s.second);
      95                 :         12 :         continue;
      96                 :            :       }
      97                 :            :     }
      98                 :            :     // must treat the substitution as an assertion
      99                 :         58 :     axiomsn.emplace_back(s.first.eqNode(s.second));
     100                 :            :   }
     101         [ +  + ]:       1054 :   for (const Node& ax : axioms)
     102                 :            :   {
     103                 :        635 :     axiomsn.emplace_back(rewrite(tlsShared.apply(ax)));
     104                 :            :   }
     105                 :        419 :   Node conjn = tlsShared.apply(conj);
     106                 :        419 :   conjn = rewrite(conjn);
     107                 :        419 :   std::string name("__internal_interpol");
     108                 :            : 
     109                 :        419 :   d_tlsConj = Node::null();
     110                 :        419 :   d_subsolver = std::make_unique<quantifiers::SygusInterpol>(d_env);
     111         [ +  + ]:        419 :   if (d_subsolver->solveInterpolation(
     112                 :            :           name, axiomsn, conjn, grammarType, interpol))
     113                 :            :   {
     114         [ +  + ]:        411 :     if (!tlsShared.empty())
     115                 :            :     {
     116                 :            :       // must conjoin equalities from shared top-level substitutions
     117                 :          4 :       NodeManager* nm = nodeManager();
     118                 :          4 :       d_tlsConj = tlsShared.toFormula(nm);
     119                 :          4 :       interpol = nm->mkNode(Kind::AND, d_tlsConj, interpol);
     120                 :            :     }
     121         [ +  + ]:        411 :     if (options().smt.checkInterpolants)
     122                 :            :     {
     123                 :         12 :       checkInterpol(interpol, axioms, conj);
     124                 :            :     }
     125                 :        411 :     return true;
     126                 :            :   }
     127                 :          8 :   return false;
     128                 :        419 : }
     129                 :            : 
     130                 :         94 : bool InterpolationSolver::getInterpolantNext(Node& interpol)
     131                 :            : {
     132                 :            :   // should already have initialized a subsolver, since we are immediately
     133                 :            :   // preceeded by a successful call to get-interpolant(-next).
     134 [ -  + ][ -  + ]:         94 :   Assert(d_subsolver != nullptr);
                 [ -  - ]
     135         [ -  + ]:         94 :   if (!d_subsolver->solveInterpolationNext(interpol))
     136                 :            :   {
     137                 :          0 :     return false;
     138                 :            :   }
     139                 :            :   // conjoin the top-level substitutions, as computed in getInterpolant
     140         [ -  + ]:         94 :   if (!d_tlsConj.isNull())
     141                 :            :   {
     142                 :          0 :     NodeManager* nm = nodeManager();
     143                 :          0 :     interpol = nm->mkNode(Kind::AND, d_tlsConj, interpol);
     144                 :            :   }
     145                 :         94 :   return true;
     146                 :            : }
     147                 :            : 
     148                 :         12 : void InterpolationSolver::checkInterpol(Node interpol,
     149                 :            :                                         const std::vector<Node>& easserts,
     150                 :            :                                         const Node& conj)
     151                 :            : {
     152 [ -  + ][ -  + ]:         12 :   Assert(interpol.getType().isBoolean());
                 [ -  - ]
     153         [ +  - ]:         24 :   Trace("check-interpol")
     154                 :         12 :       << "SolverEngine::checkInterpol: get expanded assertions" << std::endl;
     155                 :         12 :   bool canTrustResult = SygusSolver::canTrustSynthesisResult(options());
     156         [ -  + ]:         12 :   if (!canTrustResult)
     157                 :            :   {
     158                 :          0 :     warning() << "Running check-interpolants is not guaranteed to pass with "
     159                 :          0 :                  "the current options."
     160                 :          0 :               << std::endl;
     161                 :            :   }
     162                 :            : 
     163                 :         12 :   Options subOptions;
     164                 :         12 :   subOptions.copyValues(d_env.getOptions());
     165                 :         12 :   subOptions.write_smt().produceInterpolants = false;
     166                 :         12 :   SetDefaults::disableChecking(subOptions);
     167                 :         12 :   SubsolverSetupInfo ssi(d_env, subOptions);
     168                 :            :   // two checks: first, axioms imply interpol, second, interpol implies conj.
     169         [ +  + ]:         36 :   for (unsigned j = 0; j < 2; j++)
     170                 :            :   {
     171         [ +  + ]:         24 :     if (j == 1)
     172                 :            :     {
     173         [ +  - ]:         24 :       Trace("check-interpol")
     174                 :         12 :           << "SolverEngine::checkInterpol: conjecture is " << conj << std::endl;
     175                 :            :     }
     176         [ +  - ]:         48 :     Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j
     177                 :         24 :                             << ": make new SMT engine" << std::endl;
     178                 :            :     // Start new SMT engine to check solution
     179                 :         24 :     std::unique_ptr<SolverEngine> itpChecker;
     180                 :         24 :     initializeSubsolver(nodeManager(), itpChecker, ssi);
     181         [ +  - ]:         48 :     Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j
     182                 :         24 :                             << ": asserting formulas" << std::endl;
     183         [ +  + ]:         24 :     if (j == 0)
     184                 :            :     {
     185         [ +  + ]:         37 :       for (const Node& e : easserts)
     186                 :            :       {
     187                 :         25 :         itpChecker->assertFormula(e);
     188                 :            :       }
     189                 :         12 :       Node negitp = interpol.notNode();
     190                 :         12 :       itpChecker->assertFormula(negitp);
     191                 :         12 :     }
     192                 :            :     else
     193                 :            :     {
     194                 :         12 :       itpChecker->assertFormula(interpol);
     195 [ -  + ][ -  + ]:         12 :       Assert(!conj.isNull());
                 [ -  - ]
     196                 :         12 :       itpChecker->assertFormula(conj.notNode());
     197                 :            :     }
     198         [ +  - ]:         48 :     Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j
     199                 :         24 :                             << ": check the assertions" << std::endl;
     200                 :         24 :     Result r = itpChecker->checkSat();
     201         [ +  - ]:         48 :     Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j
     202                 :         24 :                             << ": result is " << r << std::endl;
     203                 :         24 :     std::stringstream serr;
     204         [ -  + ]:         24 :     if (r.getStatus() != Result::UNSAT)
     205                 :            :     {
     206         [ -  - ]:          0 :       if (j == 0)
     207                 :            :       {
     208                 :            :         serr << "SolverEngine::checkInterpol(): negated produced solution "
     209                 :            :                 "cannot be shown "
     210                 :          0 :                 "satisfiable with assertions, result was "
     211                 :          0 :              << r;
     212                 :            :       }
     213                 :            :       else
     214                 :            :       {
     215                 :            :         serr << "SolverEngine::checkInterpol(): negated conjecture cannot be "
     216                 :          0 :                 "shown satisfiable with produced solution, result was "
     217                 :          0 :              << r;
     218                 :            :       }
     219 [ -  - ][ -  - ]:          0 :       bool hardFailure = canTrustResult && !r.isUnknown();
     220         [ -  - ]:          0 :       if (hardFailure)
     221                 :            :       {
     222                 :          0 :         InternalError() << serr.str();
     223                 :            :       }
     224                 :            :       else
     225                 :            :       {
     226                 :          0 :         warning() << serr.str() << std::endl;
     227                 :            :       }
     228                 :            :     }
     229                 :         24 :   }
     230                 :         12 : }
     231                 :            : 
     232                 :            : }  // namespace smt
     233                 :            : }  // namespace cvc5::internal