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                 :            :  * Utility for processing single invocation synthesis conjectures.
      11                 :            :  */
      12                 :            : #include "theory/quantifiers/sygus/template_infer.h"
      13                 :            : 
      14                 :            : #include "expr/skolem_manager.h"
      15                 :            : #include "options/quantifiers_options.h"
      16                 :            : #include "theory/quantifiers/sygus/embedding_converter.h"
      17                 :            : #include "theory/quantifiers/sygus/sygus_utils.h"
      18                 :            : #include "theory/quantifiers/term_util.h"
      19                 :            : 
      20                 :            : using namespace cvc5::internal::kind;
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace theory {
      24                 :            : namespace quantifiers {
      25                 :            : 
      26                 :       6232 : SygusTemplateInfer::SygusTemplateInfer(Env& env) : EnvObj(env), d_ti(env) {}
      27                 :            : 
      28                 :        972 : void SygusTemplateInfer::initialize(Node q)
      29                 :            : {
      30 [ -  + ][ -  + ]:        972 :   Assert(d_quant.isNull());
                 [ -  - ]
      31 [ -  + ][ -  + ]:        972 :   Assert(q.getKind() == Kind::FORALL);
                 [ -  - ]
      32                 :        972 :   d_quant = q;
      33                 :            :   // We are processing without single invocation techniques, now check if
      34                 :            :   // we should fix an invariant template (post-condition strengthening or
      35                 :            :   // pre-condition weakening).
      36                 :        972 :   options::SygusInvTemplMode tmode = options().quantifiers.sygusInvTemplMode;
      37         [ +  + ]:        972 :   if (tmode != options::SygusInvTemplMode::NONE)
      38                 :            :   {
      39                 :            :     // currently only works for single predicate synthesis
      40                 :        709 :     if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate())
      41                 :            :     {
      42                 :        385 :       tmode = options::SygusInvTemplMode::NONE;
      43                 :            :     }
      44         [ +  - ]:        324 :     else if (!options().quantifiers.sygusInvTemplWhenSyntax)
      45                 :            :     {
      46                 :            :       // only use invariant templates if no syntactic restrictions
      47         [ +  + ]:        324 :       if (EmbeddingConverter::hasSyntaxRestrictions(q))
      48                 :            :       {
      49                 :        163 :         tmode = options::SygusInvTemplMode::NONE;
      50                 :            :       }
      51                 :            :     }
      52                 :            :   }
      53                 :            : 
      54         [ +  + ]:        972 :   if (tmode == options::SygusInvTemplMode::NONE)
      55                 :            :   {
      56                 :            :     // not processing invariant templates
      57                 :        927 :     return;
      58                 :            :   }
      59                 :            : 
      60                 :        161 :   Node qq;
      61                 :        161 :   if (q[1].getKind() == Kind::NOT && q[1][0].getKind() == Kind::FORALL)
      62                 :            :   {
      63                 :        154 :     qq = q[1][0][1];
      64                 :            :   }
      65                 :            :   else
      66                 :            :   {
      67                 :          7 :     qq = TermUtil::simpleNegate(q[1]);
      68                 :            :   }
      69         [ +  + ]:        161 :   if (qq.isConst())
      70                 :            :   {
      71                 :            :     // trivial, do not use transition inference
      72                 :          2 :     return;
      73                 :            :   }
      74                 :            : 
      75                 :            :   // if we are doing invariant templates, then construct the template
      76         [ +  - ]:        159 :   Trace("sygus-si") << "- Do transition inference..." << std::endl;
      77                 :        159 :   d_ti.process(qq, q[0][0]);
      78         [ +  - ]:        159 :   Trace("cegqi-inv") << std::endl;
      79                 :        159 :   Node prog = d_ti.getFunction();
      80         [ +  + ]:        159 :   if (!d_ti.isComplete())
      81                 :            :   {
      82                 :            :     // the invariant could not be inferred
      83                 :        114 :     return;
      84                 :            :   }
      85 [ -  + ][ -  + ]:         45 :   Assert(prog == q[0][0]);
                 [ -  - ]
      86                 :         45 :   NodeManager* nm = nodeManager();
      87                 :            :   // map the program back via non-single invocation map
      88                 :         45 :   std::vector<Node> prog_templ_vars;
      89                 :         45 :   d_ti.getVariables(prog_templ_vars);
      90                 :         45 :   d_trans_pre[prog] = d_ti.getPreCondition();
      91                 :         45 :   d_trans_post[prog] = d_ti.getPostCondition();
      92         [ +  - ]:         45 :   Trace("cegqi-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
      93         [ +  - ]:         45 :   Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
      94                 :            : 
      95                 :            :   // construct template argument
      96                 :         45 :   TypeNode atn = prog.getType();
      97         [ +  - ]:         45 :   if (atn.isFunction())
      98                 :            :   {
      99                 :         45 :     atn = atn.getRangeType();
     100                 :            :   }
     101                 :         45 :   d_templ_arg[prog] = NodeManager::mkDummySkolem("I", atn);
     102                 :            : 
     103                 :            :   // construct template
     104                 :         45 :   Node templ;
     105         [ +  - ]:         45 :   if (options().quantifiers.sygusInvAutoUnfold)
     106                 :            :   {
     107         [ +  - ]:         45 :     if (d_ti.isComplete())
     108                 :            :     {
     109         [ +  - ]:         90 :       Trace("cegqi-inv-auto-unfold")
     110                 :         45 :           << "Automatic deterministic unfolding... " << std::endl;
     111                 :            :       // auto-unfold
     112                 :         45 :       DetTrace dt;
     113                 :         45 :       int init_dt = d_ti.initializeTrace(dt);
     114         [ +  + ]:         45 :       if (init_dt == 0)
     115                 :            :       {
     116         [ +  - ]:         10 :         Trace("cegqi-inv-auto-unfold") << "  Init : ";
     117                 :         10 :         dt.print("cegqi-inv-auto-unfold");
     118         [ +  - ]:         10 :         Trace("cegqi-inv-auto-unfold") << std::endl;
     119                 :         10 :         unsigned counter = 0;
     120                 :         10 :         unsigned status = 0;
     121 [ +  + ][ +  + ]:        634 :         while (counter < 100 && status == 0)
     122                 :            :         {
     123                 :        624 :           status = d_ti.incrementTrace(dt);
     124                 :        624 :           counter++;
     125         [ +  - ]:        624 :           Trace("cegqi-inv-auto-unfold") << "  #" << counter << " : ";
     126                 :        624 :           dt.print("cegqi-inv-auto-unfold");
     127         [ +  - ]:       1248 :           Trace("cegqi-inv-auto-unfold")
     128                 :        624 :               << "...status = " << status << std::endl;
     129                 :            :         }
     130         [ +  + ]:         10 :         if (status == 1)
     131                 :            :         {
     132                 :            :           // we have a trivial invariant
     133                 :          4 :           templ = d_ti.constructFormulaTrace(dt);
     134         [ +  - ]:          8 :           Trace("cegqi-inv") << "By finite deterministic terminating trace, a "
     135                 :          0 :                                 "solution invariant is : "
     136                 :          4 :                              << std::endl;
     137         [ +  - ]:          4 :           Trace("cegqi-inv") << "   " << templ << std::endl;
     138                 :            :           // this should be unnecessary
     139                 :          4 :           templ = nm->mkNode(Kind::AND, templ, d_templ_arg[prog]);
     140                 :            :         }
     141                 :            :       }
     142                 :            :       else
     143                 :            :       {
     144         [ +  - ]:         35 :         Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl;
     145                 :            :       }
     146                 :         45 :     }
     147                 :            :   }
     148         [ +  - ]:         90 :   Trace("cegqi-inv") << "Make the template... " << tmode << " " << templ
     149                 :         45 :                      << std::endl;
     150         [ +  + ]:         45 :   if (templ.isNull())
     151                 :            :   {
     152         [ -  + ]:         41 :     if (tmode == options::SygusInvTemplMode::PRE)
     153                 :            :     {
     154                 :          0 :       templ = nm->mkNode(Kind::OR, d_trans_pre[prog], d_templ_arg[prog]);
     155                 :            :     }
     156                 :            :     else
     157                 :            :     {
     158 [ -  + ][ -  + ]:         41 :       Assert(tmode == options::SygusInvTemplMode::POST);
                 [ -  - ]
     159                 :         41 :       templ = nm->mkNode(Kind::AND, d_trans_post[prog], d_templ_arg[prog]);
     160                 :            :     }
     161                 :            :   }
     162         [ +  - ]:         90 :   Trace("cegqi-inv") << "       template (pre-substitution) : " << templ
     163                 :         45 :                      << std::endl;
     164 [ -  + ][ -  + ]:         45 :   Assert(!templ.isNull());
                 [ -  - ]
     165                 :            : 
     166                 :            :   // get the variables
     167                 :         45 :   Node sfvl = SygusUtils::getOrMkSygusArgumentList(prog);
     168         [ +  - ]:         45 :   if (!sfvl.isNull())
     169                 :            :   {
     170                 :         45 :     std::vector<Node> prog_vars(sfvl.begin(), sfvl.end());
     171                 :            :     // subsitute the template arguments
     172         [ +  - ]:         90 :     Trace("cegqi-inv") << "vars : " << prog_templ_vars << " " << prog_vars
     173                 :         45 :                        << std::endl;
     174 [ -  + ][ -  + ]:         45 :     Assert(prog_templ_vars.size() == prog_vars.size());
                 [ -  - ]
     175                 :         90 :     templ = templ.substitute(prog_templ_vars.begin(),
     176                 :            :                              prog_templ_vars.end(),
     177                 :            :                              prog_vars.begin(),
     178                 :         45 :                              prog_vars.end());
     179                 :         45 :   }
     180         [ +  - ]:         45 :   Trace("cegqi-inv") << "       template : " << templ << std::endl;
     181                 :         45 :   d_templ[prog] = templ;
     182 [ +  + ][ +  + ]:        275 : }
     183                 :            : 
     184                 :       3711 : Node SygusTemplateInfer::getTemplate(Node prog) const
     185                 :            : {
     186                 :       3711 :   std::map<Node, Node>::const_iterator tmpl = d_templ.find(prog);
     187         [ +  + ]:       3711 :   if (tmpl != d_templ.end())
     188                 :            :   {
     189                 :         78 :     return tmpl->second;
     190                 :            :   }
     191                 :       3633 :   return Node::null();
     192                 :            : }
     193                 :            : 
     194                 :         78 : Node SygusTemplateInfer::getTemplateArg(Node prog) const
     195                 :            : {
     196                 :         78 :   std::map<Node, Node>::const_iterator tmpla = d_templ_arg.find(prog);
     197         [ +  - ]:         78 :   if (tmpla != d_templ_arg.end())
     198                 :            :   {
     199                 :         78 :     return tmpla->second;
     200                 :            :   }
     201                 :          0 :   return Node::null();
     202                 :            : }
     203                 :            : 
     204                 :            : }  // namespace quantifiers
     205                 :            : }  // namespace theory
     206                 :            : }  // namespace cvc5::internal