Branch data     Line data    Source code

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