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 checking for illegal inputs
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "smt/illegal_checker.h"
      14                 :            : 
      15                 :            : #include <unordered_set>
      16                 :            : 
      17                 :            : #include "base/modal_exception.h"
      18                 :            : #include "expr/dtype.h"
      19                 :            : #include "expr/node_algorithm.h"
      20                 :            : #include "options/arith_options.h"
      21                 :            : #include "options/arrays_options.h"
      22                 :            : #include "options/bags_options.h"
      23                 :            : #include "options/base_options.h"
      24                 :            : #include "options/datatypes_options.h"
      25                 :            : #include "options/ff_options.h"
      26                 :            : #include "options/fp_options.h"
      27                 :            : #include "options/main_options.h"
      28                 :            : #include "options/sep_options.h"
      29                 :            : #include "options/sets_options.h"
      30                 :            : #include "options/smt_options.h"
      31                 :            : #include "options/uf_options.h"
      32                 :            : #include "smt/env.h"
      33                 :            : #include "smt/logic_exception.h"
      34                 :            : 
      35                 :            : namespace cvc5::internal {
      36                 :            : namespace smt {
      37                 :            : 
      38                 :      52216 : IllegalChecker::IllegalChecker(Env& e)
      39                 :      52216 :     : EnvObj(e), d_visited(userContext()), d_assertionIndex(userContext(), 0)
      40                 :            : {
      41                 :            :   // Determine any illegal kinds that are dependent on options that need to be
      42                 :            :   // guarded here. Note that nearly all illegal kinds should be properly guarded
      43                 :            :   // by either the theory engine, theory solvers, or by theory rewriters. We
      44                 :            :   // only require special handling for rare cases, including array constants,
      45                 :            :   // where array constants *must* be rewritten by the rewriter for the purposes
      46                 :            :   // of model verification, but we do not want array constants to appear in
      47                 :            :   // assertions unless --arrays-exp is enabled.
      48                 :            : 
      49                 :            :   // Note that we don't guard against HO_APPLY, since it can naturally be
      50                 :            :   // handled in proofs.
      51                 :            : 
      52                 :            :   // Array constants are not supported unless arraysExp is enabled
      53                 :      52216 :   if (logicInfo().isTheoryEnabled(theory::THEORY_ARRAYS)
      54 [ +  + ][ +  + ]:      52216 :       && !options().arrays.arraysExp)
                 [ +  + ]
      55                 :            :   {
      56                 :      33465 :     d_illegalKinds.insert(Kind::STORE_ALL);
      57                 :            :   }
      58                 :      52216 :   if (logicInfo().isTheoryEnabled(theory::THEORY_ARITH)
      59 [ +  + ][ +  + ]:      52216 :       && !options().arith.arithExp)
                 [ +  + ]
      60                 :            :   {
      61                 :          5 :     d_illegalKinds.insert(Kind::POW);
      62                 :          5 :     d_illegalKinds.insert(Kind::PI);
      63                 :          5 :     d_illegalKinds.insert(Kind::EXPONENTIAL);
      64                 :          5 :     d_illegalKinds.insert(Kind::SINE);
      65                 :          5 :     d_illegalKinds.insert(Kind::COSINE);
      66                 :          5 :     d_illegalKinds.insert(Kind::TANGENT);
      67                 :          5 :     d_illegalKinds.insert(Kind::COSECANT);
      68                 :          5 :     d_illegalKinds.insert(Kind::SECANT);
      69                 :          5 :     d_illegalKinds.insert(Kind::COTANGENT);
      70                 :          5 :     d_illegalKinds.insert(Kind::ARCSINE);
      71                 :          5 :     d_illegalKinds.insert(Kind::ARCCOSINE);
      72                 :          5 :     d_illegalKinds.insert(Kind::ARCTANGENT);
      73                 :          5 :     d_illegalKinds.insert(Kind::ARCCOSECANT);
      74                 :          5 :     d_illegalKinds.insert(Kind::ARCSECANT);
      75                 :          5 :     d_illegalKinds.insert(Kind::ARCCOTANGENT);
      76                 :          5 :     d_illegalKinds.insert(Kind::SQRT);
      77                 :          5 :     d_illegalKinds.insert(Kind::IAND);
      78                 :          5 :     d_illegalKinds.insert(Kind::PIAND);
      79                 :          5 :     d_illegalKinds.insert(Kind::POW2);
      80                 :          5 :     d_illegalKinds.insert(Kind::INTS_LOG2);
      81                 :            :   }
      82                 :      52216 :   if (logicInfo().isTheoryEnabled(theory::THEORY_DATATYPES)
      83 [ +  + ][ +  + ]:      52216 :       && !options().datatypes.datatypesExp)
                 [ +  + ]
      84                 :            :   {
      85                 :          5 :     d_illegalKinds.insert(Kind::MATCH);
      86                 :            :     // catches all occurrences of nullables
      87                 :          5 :     d_illegalKinds.insert(Kind::NULLABLE_TYPE);
      88                 :            :   }
      89 [ +  + ][ -  + ]:      52216 :   if (logicInfo().hasCardinalityConstraints() && !options().uf.ufCardExp)
                 [ -  + ]
      90                 :            :   {
      91                 :          0 :     d_illegalKinds.insert(Kind::CARDINALITY_CONSTRAINT);
      92                 :            :   }
      93         [ +  + ]:      52216 :   if (logicInfo().isTheoryEnabled(theory::THEORY_SETS))
      94                 :            :   {
      95         [ +  + ]:      32126 :     if (!options().sets.setsCardExp)
      96                 :            :     {
      97                 :          5 :       d_illegalKinds.insert(Kind::SET_CARD);
      98                 :            :     }
      99         [ +  + ]:      32126 :     if (!options().sets.relsExp)
     100                 :            :     {
     101                 :          5 :       d_illegalKinds.insert(Kind::RELATION_TABLE_JOIN);
     102                 :          5 :       d_illegalKinds.insert(Kind::RELATION_TRANSPOSE);
     103                 :          5 :       d_illegalKinds.insert(Kind::RELATION_PRODUCT);
     104                 :          5 :       d_illegalKinds.insert(Kind::RELATION_JOIN);
     105                 :          5 :       d_illegalKinds.insert(Kind::RELATION_TCLOSURE);
     106                 :          5 :       d_illegalKinds.insert(Kind::RELATION_IDEN);
     107                 :          5 :       d_illegalKinds.insert(Kind::RELATION_JOIN_IMAGE);
     108                 :          5 :       d_illegalKinds.insert(Kind::RELATION_GROUP);
     109                 :          5 :       d_illegalKinds.insert(Kind::RELATION_AGGREGATE);
     110                 :          5 :       d_illegalKinds.insert(Kind::RELATION_PROJECT);
     111                 :            :     }
     112                 :            :   }
     113                 :            :   // unsupported theories disables all kinds belonging to the theory
     114                 :      52216 :   std::unordered_set<theory::TheoryId> unsupportedTheories;
     115 [ +  + ][ +  + ]:      52216 :   if (logicInfo().isTheoryEnabled(theory::THEORY_FP) && !options().fp.fp)
                 [ +  + ]
     116                 :            :   {
     117                 :          5 :     unsupportedTheories.insert(theory::TheoryId::THEORY_FP);
     118                 :            :     // Require a special check for rounding mode
     119                 :          5 :     d_illegalTypes.insert(nodeManager()->roundingModeType());
     120                 :            :   }
     121 [ +  + ][ +  + ]:      52216 :   if (logicInfo().isTheoryEnabled(theory::THEORY_FF) && !options().ff.ff)
                 [ +  + ]
     122                 :            :   {
     123                 :          5 :     unsupportedTheories.insert(theory::TheoryId::THEORY_FF);
     124                 :            :   }
     125 [ +  + ][ +  + ]:      52216 :   if (logicInfo().isTheoryEnabled(theory::THEORY_BAGS) && !options().bags.bags)
                 [ +  + ]
     126                 :            :   {
     127                 :          5 :     unsupportedTheories.insert(theory::TheoryId::THEORY_BAGS);
     128                 :            :   }
     129 [ +  + ][ +  + ]:      52216 :   if (logicInfo().isTheoryEnabled(theory::THEORY_SEP) && !options().sep.sep)
                 [ +  + ]
     130                 :            :   {
     131                 :          5 :     unsupportedTheories.insert(theory::TheoryId::THEORY_SEP);
     132                 :            :   }
     133         [ +  + ]:      52216 :   if (!unsupportedTheories.empty())
     134                 :            :   {
     135         [ +  + ]:       1915 :     for (int32_t i = 0; i < static_cast<int32_t>(Kind::LAST_KIND); ++i)
     136                 :            :     {
     137                 :       1910 :       Kind k = static_cast<Kind>(i);
     138                 :            :       // these two kinds are special cased in kindToTheoryId, skip
     139 [ +  - ][ +  + ]:       1910 :       if (k == Kind::UNDEFINED_KIND || k == Kind::NULL_EXPR)
     140                 :            :       {
     141                 :          5 :         continue;
     142                 :            :       }
     143                 :       1905 :       theory::TheoryId tid = theory::kindToTheoryId(k);
     144         [ +  + ]:       1905 :       if (unsupportedTheories.find(tid) != unsupportedTheories.end())
     145                 :            :       {
     146                 :        490 :         d_illegalKinds.insert(k);
     147                 :            :       }
     148                 :            :     }
     149                 :            :   }
     150                 :      52216 : }
     151                 :            : 
     152                 :      50529 : void IllegalChecker::checkAssertions(Assertions& as)
     153                 :            : {
     154 [ +  + ][ +  - ]:      50529 :   if (d_illegalKinds.empty() && d_illegalTypes.empty())
                 [ +  + ]
     155                 :            :   {
     156                 :            :     // nothing to check
     157                 :      21224 :     return;
     158                 :            :   }
     159                 :            :   // check illegal kinds here
     160                 :      29305 :   const context::CDList<Node>& assertions = as.getAssertionList();
     161                 :      29305 :   size_t asize = assertions.size();
     162         [ +  + ]:     134063 :   for (size_t i = d_assertionIndex.get(); i < asize; ++i)
     163                 :            :   {
     164                 :     104762 :     Node n = assertions[i];
     165         [ +  - ]:     104762 :     Trace("illegal-check") << "Check assertion " << n << std::endl;
     166                 :     104763 :     Kind k = checkInternal(n);
     167         [ +  + ]:     104761 :     if (k != Kind::UNDEFINED_KIND)
     168                 :            :     {
     169                 :          3 :       std::stringstream ss;
     170                 :          3 :       ss << "Cannot handle assertion with term of kind " << k
     171                 :          3 :          << " in this configuration.";
     172                 :            :       // suggested options only in non-safe builds
     173                 :            : #if !defined(CVC5_SAFE_MODE) && !defined(CVC5_STABLE_MODE)
     174         [ -  + ]:          3 :       if (k == Kind::STORE_ALL)
     175                 :            :       {
     176                 :          0 :         ss << " Try --arrays-exp.";
     177                 :            :       }
     178                 :            :       else
     179                 :            :       {
     180                 :          3 :         theory::TheoryId tid = theory::kindToTheoryId(k);
     181                 :            :         // if the kind was disabled based a theory, report it.
     182 [ +  + ][ -  - ]:          3 :         switch (tid)
                    [ - ]
     183                 :            :         {
     184                 :          1 :           case theory::THEORY_FF: ss << " Try --ff."; break;
     185                 :          2 :           case theory::THEORY_FP: ss << " Try --fp."; break;
     186                 :          0 :           case theory::THEORY_BAGS: ss << " Try --bags."; break;
     187                 :          0 :           case theory::THEORY_SEP: ss << " Try --sep."; break;
     188                 :          0 :           default: break;
     189                 :            :         }
     190                 :            :       }
     191                 :            : #endif
     192                 :          3 :       throw SafeLogicException(ss.str());
     193                 :          3 :     }
     194                 :     104762 :   }
     195                 :      29301 :   d_assertionIndex = asize;
     196                 :            : }
     197                 :            : 
     198                 :     104762 : Kind IllegalChecker::checkInternal(TNode n)
     199                 :            : {
     200 [ -  + ][ -  + ]:     104762 :   Assert(!d_illegalKinds.empty());
                 [ -  - ]
     201                 :     104762 :   std::vector<TNode> visit;
     202                 :     104762 :   std::unordered_set<TypeNode> allTypes;
     203                 :     104762 :   TNode cur;
     204                 :     104762 :   visit.push_back(n);
     205                 :            :   Kind k;
     206                 :            :   do
     207                 :            :   {
     208                 :    2458862 :     cur = visit.back();
     209                 :    2458862 :     visit.pop_back();
     210         [ +  + ]:    2458862 :     if (d_visited.find(cur) == d_visited.end())
     211                 :            :     {
     212                 :    1135846 :       k = cur.getKind();
     213         [ +  + ]:    1135846 :       if (d_illegalKinds.find(k) != d_illegalKinds.end())
     214                 :            :       {
     215                 :          3 :         return k;
     216                 :            :       }
     217         [ +  + ]:    1135843 :       else if (cur.isVar())
     218                 :            :       {
     219                 :            :         // check its type
     220                 :     215964 :         TypeNode tn = cur.getType();
     221                 :     215964 :         expr::getComponentTypes(tn, allTypes);
     222                 :     215964 :       }
     223                 :    1135843 :       d_visited.insert(cur);
     224         [ +  + ]:    1135843 :       if (cur.hasOperator())
     225                 :            :       {
     226                 :     782673 :         visit.push_back(cur.getOperator());
     227                 :            :       }
     228                 :    1135843 :       visit.insert(visit.end(), cur.begin(), cur.end());
     229                 :            :     }
     230         [ +  + ]:    2458859 :   } while (!visit.empty());
     231                 :            :   // now, go back and check if the types are legal
     232                 :     104759 :   std::vector<TypeNode> tlist(allTypes.begin(), allTypes.end());
     233         [ +  + ]:     246248 :   for (size_t i = 0; i < tlist.size(); i++)
     234                 :            :   {
     235                 :     141490 :     TypeNode tn = tlist[i];
     236                 :            :     // Must additionally get the subfield types from datatypes.
     237         [ +  + ]:     141490 :     if (tn.isDatatype())
     238                 :            :     {
     239                 :      11944 :       const DType& dt = tn.getDType();
     240                 :      11944 :       std::unordered_set<TypeNode> sftypes = dt.getSubfieldTypes();
     241                 :      11944 :       std::unordered_set<TypeNode> sfctypes;
     242                 :            :       // get the component types of each of the subfield types
     243         [ +  + ]:      29553 :       for (const TypeNode& sft : sftypes)
     244                 :            :       {
     245                 :            :         // as an optimization, if we've already considered this type, don't
     246                 :            :         // have to find its component types
     247         [ +  + ]:      17609 :         if (allTypes.find(sft) == allTypes.end())
     248                 :            :         {
     249                 :       4137 :           expr::getComponentTypes(sft, sfctypes);
     250                 :            :         }
     251                 :            :       }
     252         [ +  + ]:      16517 :       for (const TypeNode& sft : sfctypes)
     253                 :            :       {
     254         [ +  + ]:       4573 :         if (allTypes.find(sft) == allTypes.end())
     255                 :            :         {
     256                 :       4407 :           tlist.emplace_back(sft);
     257                 :       4407 :           allTypes.insert(sft);
     258                 :            :         }
     259                 :            :       }
     260                 :      11944 :     }
     261                 :     141490 :     k = tn.getKind();
     262                 :     141490 :     if (d_illegalKinds.find(k) != d_illegalKinds.end()
     263 [ +  - ][ +  + ]:     141490 :         || d_illegalTypes.find(tn) != d_illegalTypes.end())
                 [ +  + ]
     264                 :            :     {
     265                 :          1 :       std::stringstream ss;
     266                 :          1 :       ss << "Cannot handle term with type " << tn << " in this configuration";
     267                 :          1 :       throw SafeLogicException(ss.str());
     268                 :          1 :     }
     269                 :     141490 :   }
     270                 :     104758 :   return Kind::UNDEFINED_KIND;
     271                 :     104765 : }
     272                 :            : 
     273                 :            : }  // namespace smt
     274                 :            : }  // namespace cvc5::internal