Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz, Daniel Larraz
       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 abduction queries.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "smt/abduction_solver.h"
      17                 :            : 
      18                 :            : #include <sstream>
      19                 :            : 
      20                 :            : #include "base/modal_exception.h"
      21                 :            : #include "options/quantifiers_options.h"
      22                 :            : #include "options/smt_options.h"
      23                 :            : #include "smt/env.h"
      24                 :            : #include "smt/set_defaults.h"
      25                 :            : #include "smt/sygus_solver.h"
      26                 :            : #include "theory/quantifiers/quantifiers_attributes.h"
      27                 :            : #include "theory/quantifiers/sygus/sygus_abduct.h"
      28                 :            : #include "theory/quantifiers/sygus/sygus_utils.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                 :       6245 : AbductionSolver::AbductionSolver(Env& env) : EnvObj(env) {}
      38                 :            : 
      39                 :      12430 : AbductionSolver::~AbductionSolver() {}
      40                 :        416 : bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
      41                 :            :                                 const Node& goal,
      42                 :            :                                 const TypeNode& grammarType,
      43                 :            :                                 Node& abd)
      44                 :            : {
      45         [ -  + ]:        416 :   if (!options().smt.produceAbducts)
      46                 :            :   {
      47                 :          0 :     const char* msg = "Cannot get abduct when produce-abducts options is off.";
      48                 :          0 :     throw ModalException(msg);
      49                 :            :   }
      50         [ +  - ]:        416 :   Trace("sygus-abduct") << "Axioms: " << axioms << std::endl;
      51         [ +  - ]:        832 :   Trace("sygus-abduct") << "SolverEngine::getAbduct: goal " << goal
      52                 :        416 :                         << std::endl;
      53                 :        416 :   SubstitutionMap& tls = d_env.getTopLevelSubstitutions().get();
      54                 :        832 :   std::vector<Node> axiomsn;
      55         [ +  + ]:        947 :   for (const Node& ax : axioms)
      56                 :            :   {
      57                 :        531 :     axiomsn.emplace_back(tls.apply(ax));
      58                 :            :   }
      59                 :        832 :   std::vector<Node> asserts(axiomsn.begin(), axiomsn.end());
      60                 :            :   // must expand definitions
      61                 :        832 :   Node conjn = tls.apply(goal);
      62                 :        416 :   conjn = rewrite(conjn);
      63                 :            :   // now negate
      64                 :        416 :   conjn = conjn.negate();
      65                 :        416 :   d_abdConj = conjn;
      66                 :        416 :   asserts.push_back(conjn);
      67                 :        832 :   std::string name("__internal_abduct");
      68                 :            :   Node aconj = quantifiers::SygusAbduct::mkAbductionConjecture(
      69                 :        832 :       nodeManager(), name, asserts, axiomsn, grammarType);
      70                 :            :   // should be a quantified conjecture with one function-to-synthesize
      71                 :        832 :   Assert(aconj.getKind() == Kind::FORALL && aconj[0].getNumChildren() == 1);
      72                 :            :   // remember the abduct-to-synthesize
      73                 :        416 :   d_sssf = aconj[0][0];
      74         [ +  - ]:        832 :   Trace("sygus-abduct") << "SolverEngine::getAbduct: made conjecture : "
      75                 :        416 :                         << aconj << ", solving for " << d_sssf << std::endl;
      76                 :            : 
      77                 :        832 :   Options subOptions;
      78                 :        416 :   subOptions.copyValues(d_env.getOptions());
      79                 :        416 :   subOptions.write_quantifiers().sygus = true;
      80                 :            :   // by default, we don't want disjunctive terms (ITE, OR) in abducts
      81         [ +  - ]:        416 :   if (!d_env.getOptions().quantifiers.sygusGrammarUseDisjWasSetByUser)
      82                 :            :   {
      83                 :        416 :     subOptions.write_quantifiers().sygusGrammarUseDisj = false;
      84                 :            :   }
      85                 :        416 :   SetDefaults::disableChecking(subOptions);
      86                 :        832 :   SubsolverSetupInfo ssi(d_env, subOptions);
      87                 :            :   // we generate a new smt engine to do the abduction query
      88                 :        416 :   initializeSubsolver(nodeManager(), d_subsolver, ssi);
      89                 :            :   // get the logic
      90                 :        832 :   LogicInfo l = d_subsolver->getLogicInfo().getUnlockedCopy();
      91                 :            :   // enable everything needed for sygus
      92                 :        416 :   l.enableSygus();
      93                 :        416 :   d_subsolver->setLogic(l);
      94                 :            :   // assert the abduction query
      95                 :        416 :   d_subsolver->assertFormula(aconj);
      96                 :        416 :   d_axioms = axioms;
      97                 :        828 :   return getAbductInternal(abd);
      98                 :            : }
      99                 :            : 
     100                 :         92 : bool AbductionSolver::getAbductNext(Node& abd)
     101                 :            : {
     102                 :            :   // Since we are using the subsolver's check-sat interface directly, we
     103                 :            :   // simply call getAbductInternal again here. We assert that the subsolver
     104                 :            :   // is already initialized, which must be the case or else we are not in the
     105                 :            :   // proper SMT mode to make this call. Due to the default behavior of
     106                 :            :   // subsolvers having synthesis conjectures, this is guaranteed to produce
     107                 :            :   // a new solution.
     108 [ -  + ][ -  + ]:         92 :   Assert(d_subsolver != nullptr);
                 [ -  - ]
     109                 :         92 :   return getAbductInternal(abd);
     110                 :            : }
     111                 :            : 
     112                 :        508 : bool AbductionSolver::getAbductInternal(Node& abd)
     113                 :            : {
     114                 :            :   // should have initialized the subsolver by now
     115 [ -  + ][ -  + ]:        508 :   Assert(d_subsolver != nullptr);
                 [ -  - ]
     116         [ +  - ]:       1016 :   Trace("sygus-abduct") << "  SolverEngine::getAbduct check sat..."
     117                 :        508 :                         << std::endl;
     118                 :       1012 :   Result r = d_subsolver->checkSat();
     119         [ +  - ]:       1008 :   Trace("sygus-abduct") << "  SolverEngine::getAbduct result: " << r
     120                 :        504 :                         << std::endl;
     121                 :            :   // get the synthesis solution
     122                 :       1008 :   std::map<Node, Node> sols;
     123                 :            :   // use the "getSubsolverSynthSolutions" interface, since we asserted the
     124                 :            :   // internal form of the SyGuS conjecture and used check-sat.
     125         [ +  + ]:        504 :   if (d_subsolver->getSubsolverSynthSolutions(sols))
     126                 :            :   {
     127 [ -  + ][ -  + ]:        491 :     Assert(sols.size() == 1);
                 [ -  - ]
     128                 :        491 :     std::map<Node, Node>::iterator its = sols.find(d_sssf);
     129         [ +  - ]:        491 :     if (its != sols.end())
     130                 :            :     {
     131         [ +  - ]:        982 :       Trace("sygus-abduct") << "SolverEngine::getAbduct: solution is "
     132                 :        491 :                             << its->second << std::endl;
     133                 :        491 :       abd = its->second;
     134         [ +  + ]:        491 :       if (abd.getKind() == Kind::LAMBDA)
     135                 :            :       {
     136                 :        487 :         abd = abd[1];
     137                 :            :       }
     138                 :            :       // get the grammar type for the abduct
     139                 :            :       Node agdtbv =
     140                 :        491 :           theory::quantifiers::SygusUtils::getOrMkSygusArgumentList(d_sssf);
     141         [ +  + ]:        491 :       if(!agdtbv.isNull())
     142                 :            :       {
     143 [ -  + ][ -  + ]:        487 :         Assert(agdtbv.getKind() == Kind::BOUND_VAR_LIST);
                 [ -  - ]
     144                 :            :         // convert back to original
     145                 :            :         // must replace formal arguments of abd with the free variables in the
     146                 :            :         // input problem that they correspond to.
     147                 :        974 :         std::vector<Node> vars;
     148                 :        487 :         std::vector<Node> syms;
     149                 :            :         SygusVarToTermAttribute sta;
     150         [ +  + ]:       1397 :         for (const Node& bv : agdtbv)
     151                 :            :         {
     152                 :        910 :           vars.push_back(bv);
     153         [ +  - ]:        910 :           syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
     154                 :            :         }
     155                 :        487 :         abd = abd.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
     156                 :            :       }
     157                 :            : 
     158                 :            :       // if check abducts option is set, we check the correctness
     159         [ +  + ]:        491 :       if (options().smt.checkAbducts)
     160                 :            :       {
     161                 :         35 :         checkAbduct(abd);
     162                 :            :       }
     163                 :        491 :       return true;
     164                 :            :     }
     165         [ -  - ]:          0 :     Trace("sygus-abduct") << "SolverEngine::getAbduct: could not find solution!"
     166                 :          0 :                           << std::endl;
     167                 :          0 :     throw RecoverableModalException("Could not find solution for get-abduct.");
     168                 :            :   }
     169                 :         13 :   return false;
     170                 :            : }
     171                 :            : 
     172                 :         35 : void AbductionSolver::checkAbduct(Node a)
     173                 :            : {
     174 [ -  + ][ -  + ]:         35 :   Assert(a.getType().isBoolean());
                 [ -  - ]
     175         [ +  - ]:         70 :   Trace("check-abduct") << "SolverEngine::checkAbduct: get expanded assertions"
     176                 :         35 :                         << std::endl;
     177                 :         35 :   bool canTrustResult = SygusSolver::canTrustSynthesisResult(options());
     178         [ +  + ]:         35 :   if (!canTrustResult)
     179                 :            :   {
     180                 :          3 :     warning() << "Running check-abducts is not guaranteed to pass with the "
     181                 :          3 :                  "current options."
     182                 :          3 :               << std::endl;
     183                 :            :   }
     184                 :         70 :   std::vector<Node> asserts(d_axioms.begin(), d_axioms.end());
     185                 :         35 :   asserts.push_back(a);
     186                 :            : 
     187                 :         70 :   Options subOptions;
     188                 :         35 :   subOptions.copyValues(d_env.getOptions());
     189                 :         35 :   subOptions.write_smt().produceAbducts = false;
     190                 :         35 :   SetDefaults::disableChecking(subOptions);
     191                 :         70 :   SubsolverSetupInfo ssi(d_env, subOptions);
     192                 :            :   // two checks: first, consistent with assertions, second, implies negated goal
     193                 :            :   // is unsatisfiable.
     194         [ +  + ]:        105 :   for (unsigned j = 0; j < 2; j++)
     195                 :            :   {
     196         [ +  - ]:        140 :     Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j
     197                 :         70 :                           << ": make new SMT engine" << std::endl;
     198                 :            :     // Start new SMT engine to check solution
     199                 :         70 :     std::unique_ptr<SolverEngine> abdChecker;
     200                 :         70 :     initializeSubsolver(nodeManager(), abdChecker, ssi);
     201         [ +  - ]:        140 :     Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j
     202                 :         70 :                           << ": asserting formulas" << std::endl;
     203         [ +  + ]:        383 :     for (const Node& e : asserts)
     204                 :            :     {
     205                 :        313 :       abdChecker->assertFormula(e);
     206                 :            :     }
     207         [ +  - ]:        140 :     Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j
     208                 :         70 :                           << ": check the assertions" << std::endl;
     209                 :        140 :     Result r = abdChecker->checkSat();
     210         [ +  - ]:        140 :     Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j
     211                 :         70 :                           << ": result is " << r << std::endl;
     212                 :        140 :     std::stringstream serr;
     213                 :         70 :     bool isError = false;
     214                 :         70 :     bool hardFailure = canTrustResult;
     215         [ +  + ]:         70 :     if (j == 0)
     216                 :            :     {
     217         [ +  + ]:         35 :       if (r.getStatus() != Result::SAT)
     218                 :            :       {
     219                 :          1 :         isError = true;
     220                 :            :         serr
     221                 :            :             << "SolverEngine::checkAbduct(): produced solution cannot be shown "
     222                 :          1 :                "to be consistent with assertions, result was "
     223                 :          1 :             << r;
     224         [ +  - ]:          1 :         hardFailure = r.isUnknown() ? false : hardFailure;
     225                 :            :       }
     226         [ +  - ]:         70 :       Trace("check-abduct")
     227                 :         35 :           << "SolverEngine::checkAbduct: goal is " << d_abdConj << std::endl;
     228                 :            :       // add the goal to the set of assertions
     229 [ -  + ][ -  + ]:         35 :       Assert(!d_abdConj.isNull());
                 [ -  - ]
     230                 :         35 :       asserts.push_back(d_abdConj);
     231                 :            :     }
     232                 :            :     else
     233                 :            :     {
     234         [ -  + ]:         35 :       if (r.getStatus() != Result::UNSAT)
     235                 :            :       {
     236                 :          0 :         isError = true;
     237                 :            :         serr << "SolverEngine::checkAbduct(): negated goal cannot be shown "
     238                 :          0 :                 "unsatisfiable with produced solution, result was "
     239                 :          0 :              << r;
     240         [ -  - ]:          0 :         hardFailure = r.isUnknown() ? false : hardFailure;
     241                 :            :       }
     242                 :            :     }
     243                 :            :     // did we get an unexpected result?
     244         [ +  + ]:         70 :     if (isError)
     245                 :            :     {
     246         [ -  + ]:          1 :       if (hardFailure)
     247                 :            :       {
     248                 :          0 :         InternalError() << serr.str();
     249                 :            :       }
     250                 :            :       else
     251                 :            :       {
     252                 :          1 :         warning() << serr.str() << std::endl;
     253                 :            :       }
     254                 :            :     }
     255                 :            :   }
     256                 :         35 : }
     257                 :            : 
     258                 :            : }  // namespace smt
     259                 :            : }  // namespace cvc5::internal