Branch data     Line data    Source code

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