Merge branch 'main' into cadical-fix-init

src/api/cpp/cvc5.cpp

@@ -6873,21 +6873,14 @@ void Solver::ensureWellFormedTerm(const Term& t) const
   // only check if option is set
   if (d_slv->getOptions().expr.wellFormedChecking)
   {
-    bool wasShadow = false;
-    if (internal::expr::hasFreeOrShadowedVar(*t.d_node, wasShadow))
+    // Call isWellFormedTerm of the underlying solver, which checks if the
+    // given node has free variables. We do not check for variable shadowing,
+    // since this can be handled by our rewriter.
+    if (!d_slv->isWellFormedTerm(*t.d_node))
     {
       std::stringstream se;
-      se << "cannot process term " << *t.d_node << " with ";
-      if (wasShadow)
-      {
-        se << "shadowed variables " << std::endl;
-      }
-      else
-      {
-        std::unordered_set<internal::Node> fvs;
-        internal::expr::getFreeVariables(*t.d_node, fvs);
-        se << "free variables: " << fvs << std::endl;
-      }
+      se << "cannot process term " << *t.d_node << " with free variables"
+         << std::endl;
       throw CVC5ApiException(se.str().c_str());
     }
   }

src/expr/node_algorithm.cpp

@@ -348,23 +348,23 @@ bool checkVariablesInternal(TNode n,
       else if (cur.isClosure())
       {
         // add to scope
+        std::vector<TNode> boundvars;
         for (const TNode& cn : cur[0])
         {
-          if (checkShadow)
+          if (scope.find(cn) != scope.end())
           {
-            if (scope.find(cn) != scope.end())
+            if (checkShadow)
             {
               wasShadow = true;
               return true;
             }
           }
           else
           {
-            // should not shadow
-            Assert(scope.find(cn) == scope.end())
-                << "Shadowed variable " << cn << " in " << cur << "\n";
+            // add to scope if it is not shadowing
+            boundvars.push_back(cn);
+            scope.insert(cn);
           }
-          scope.insert(cn);
         }
         // must make recursive call to use separate cache
         if (checkVariablesInternal(
@@ -374,7 +374,7 @@ bool checkVariablesInternal(TNode n,
           return true;
         }
         // cleanup
-        for (const TNode& cn : cur[0])
+        for (const TNode& cn : boundvars)
         {
           scope.erase(cn);
         }

src/options/options_handler.cpp

@@ -36,6 +36,7 @@
 #include "options/language.h"
 #include "options/main_options.h"
 #include "options/option_exception.h"
+#include "options/parser_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "util/didyoumean.h"
@@ -400,5 +401,17 @@ void OptionsHandler::showTraceTags(const std::string& flag, bool value)
   printTags(Configuration::getTraceTags());
 }
 
+void OptionsHandler::strictParsing(const std::string& flag, bool value)
+{
+  if (value)
+  {
+    d_options->write_parser().parsingMode = options::ParsingMode::STRICT;
+  }
+  else if (d_options->parser.parsingMode == options::ParsingMode::STRICT)
+  {
+    d_options->write_parser().parsingMode = options::ParsingMode::DEFAULT;
+  }
+}
+
 }  // namespace options
 }  // namespace cvc5::internal

src/options/options_handler.h

@@ -111,6 +111,9 @@ class OptionsHandler
   /** Show all trace tags and exit */
   void showTraceTags(const std::string& flag, bool value);
 
+  /***************************** parser options *******************************/
+  void strictParsing(const std::string& flag, bool value);
+
  private:
   /** Pointer to the containing Options object.*/
   Options* d_options;

src/options/parser_options.toml

@@ -7,7 +7,26 @@ name   = "Parser"
   long       = "strict-parsing"
   type       = "bool"
   default    = "false"
-  help       = "be less tolerant of non-conforming inputs"
+  predicates = ["strictParsing"]
+  help       = "be less tolerant of non-conforming inputs, this is an alias for --parsing-mode=strict"
+
+[[option]]
+  name       = "parsingMode"
+  category   = "expert"
+  long       = "parsing-mode=MODE"
+  type       = "ParsingMode"
+  default    = "DEFAULT"
+  help       = "choose parsing mode, see --parsing-mode=help"
+  help_mode  = "Parsing modes."
+[[option.mode.DEFAULT]]
+  name = "default"
+  help = "Be reasonably tolerant of non-conforming inputs."
+[[option.mode.STRICT]]
+  name = "strict"
+  help = "Be less tolerant of non-conforming inputs."
+[[option.mode.LENIENT]]
+  name = "lenient"
+  help = "Be more tolerant of non-conforming inputs."
 
 [[option]]
   name       = "semanticChecks"

src/parser/parser.cpp

@@ -126,8 +126,17 @@ std::unique_ptr<Parser> Parser::mkParser(modes::InputLanguage lang,
       || lang == modes::InputLanguage::SYGUS_2_1)
   {
     bool isSygus = (lang == modes::InputLanguage::SYGUS_2_1);
-    bool strictMode = solver->getOptionInfo("strict-parsing").boolValue();
-    parser.reset(new Smt2Parser(solver, sm, strictMode, isSygus));
+    ParsingMode parsingMode = ParsingMode::DEFAULT;
+    std::string mode = solver->getOption("parsing-mode");
+    if (mode == "strict")
+    {
+      parsingMode = ParsingMode::STRICT;
+    }
+    else if (mode == "lenient")
+    {
+      parsingMode = ParsingMode::LENIENT;
+    }
+    parser.reset(new Smt2Parser(solver, sm, parsingMode, isSygus));
   }
   else
   {

src/parser/parser_state.cpp

@@ -37,14 +37,14 @@ namespace parser {
 ParserState::ParserState(ParserStateCallback* psc,
                          Solver* solver,
                          SymManager* sm,
-                         bool strictMode)
+                         ParsingMode parsingMode)
     : d_solver(solver),
       d_tm(d_solver->getTermManager()),
       d_psc(psc),
       d_symman(sm),
       d_symtab(sm->getSymbolTable()),
       d_checksEnabled(true),
-      d_strictMode(strictMode),
+      d_parsingMode(parsingMode),
       d_parseOnly(d_solver->getOptionInfo("parse-only").boolValue())
 {
 }

src/parser/parser_state.h

@@ -36,6 +36,17 @@ namespace parser {
 
 class Command;
 
+/**
+ * The parsing mode, defines how strict we are on accepting non-conforming
+ * inputs.
+ */
+enum class ParsingMode
+{
+  DEFAULT,  // reasonably strict
+  STRICT,   // more strict
+  LENIENT,  // less strict
+};
+
 /**
  * Callback from the parser state to the parser, for command preemption
  * and error handling.
@@ -67,16 +78,16 @@ class CVC5_EXPORT ParserState
    * @attention The parser takes "ownership" of the given
    * input and will delete it on destruction.
    *
-   * @param psc The callback for implementing parser-specific methods
-   * @param solver solver API object
-   * @param symm reference to the symbol manager
-   * @param input the parser input
-   * @param strictMode whether to incorporate strict(er) compliance checks
+   * @param psc The callback for implementing parser-specific methods.
+   * @param solver The solver API object.
+   * @param symm The symbol manager.
+   * @param input The parser input.
+   * @param parsingMode The parsing mode.
    */
   ParserState(ParserStateCallback* psc,
               Solver* solver,
               SymManager* sm,
-              bool strictMode = false);
+              ParsingMode parsingMode = ParsingMode::DEFAULT);
 
   virtual ~ParserState();
 
@@ -91,13 +102,15 @@ class CVC5_EXPORT ParserState
   void disableChecks() { d_checksEnabled = false; }
 
   /** Enable strict parsing, according to the language standards. */
-  void enableStrictMode() { d_strictMode = true; }
+  void enableStrictMode() { d_parsingMode = ParsingMode::STRICT; }
 
   /** Disable strict parsing. Allows certain syntactic infelicities to
       pass without comment. */
-  void disableStrictMode() { d_strictMode = false; }
+  void disableStrictMode() { d_parsingMode = ParsingMode::DEFAULT; }
+
+  bool strictModeEnabled() { return d_parsingMode == ParsingMode::STRICT; }
 
-  bool strictModeEnabled() { return d_strictMode; }
+  bool lenientModeEnabled() { return d_parsingMode == ParsingMode::LENIENT; }
 
   const std::string& getForcedLogic() const;
   bool logicIsForced() const;
@@ -577,7 +590,7 @@ class CVC5_EXPORT ParserState
   bool d_checksEnabled;
 
   /** Are we parsing in strict mode? */
-  bool d_strictMode;
+  ParsingMode d_parsingMode;
 
   /** Are we in parse-only mode? */
   bool d_parseOnly;

src/parser/smt2/smt2_parser.cpp

@@ -23,11 +23,11 @@ namespace parser {
 
 Smt2Parser::Smt2Parser(Solver* solver,
                        SymManager* sm,
-                       bool isStrict,
+                       ParsingMode parsingMode,
                        bool isSygus)
     : Parser(solver, sm),
-      d_slex(isStrict, isSygus),
-      d_state(this, solver, sm, isStrict, isSygus),
+      d_slex(parsingMode == ParsingMode::STRICT, isSygus),
+      d_state(this, solver, sm, parsingMode, isSygus),
       d_termParser(d_slex, d_state),
       d_cmdParser(d_slex, d_state, d_termParser)
 {

src/parser/smt2/smt2_parser.h

@@ -39,7 +39,7 @@ class Smt2Parser : public Parser
  public:
   Smt2Parser(Solver* solver,
              SymManager* sm,
-             bool isStrict = false,
+             ParsingMode parsingMode = ParsingMode::DEFAULT,
              bool isSygus = false);
   virtual ~Smt2Parser() {}
   /** Set the logic */

src/parser/smt2/smt2_state.cpp

@@ -27,9 +27,9 @@ namespace parser {
 Smt2State::Smt2State(ParserStateCallback* psc,
                      Solver* solver,
                      SymManager* sm,
-                     bool strictMode,
+                     ParsingMode parsingMode,
                      bool isSygus)
-    : ParserState(psc, solver, sm, strictMode),
+    : ParserState(psc, solver, sm, parsingMode),
       d_isSygus(isSygus),
       d_logicSet(false),
       d_seenSetLogic(false)

src/parser/smt2/smt2_state.h

@@ -43,7 +43,7 @@ class Smt2State : public ParserState
   Smt2State(ParserStateCallback* psc,
             Solver* solver,
             SymManager* sm,
-            bool strictMode = false,
+            ParsingMode parsingMode = ParsingMode::DEFAULT,
             bool isSygus = false);
 
   ~Smt2State();
@@ -280,7 +280,8 @@ class Smt2State : public ParserState
 
   void checkUserSymbol(const std::string& name)
   {
-    if (name.length() > 0 && (name[0] == '.' || name[0] == '@'))
+    if (!lenientModeEnabled() && name.length() > 0
+        && (name[0] == '.' || name[0] == '@'))
     {
       std::stringstream ss;
       ss << "cannot declare or define symbol `" << name

src/preprocessing/passes/ackermann.cpp

@@ -145,13 +145,13 @@ void storeFunctionAndAddLemmas(TNode func,
  * storeFunctionAndAddLemmas will then add the constraint g(x)=g(y) ->
  * f(g(x))=f(g(y)).
  * Now that we see g(x) and g(y), we explicitly add them as well. */
-void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
+void collectFunctionsAndLemmas(NodeManager* nm,
+                               FunctionToArgsMap& fun_to_args,
                                SubstitutionMap& fun_to_skolem,
                                std::vector<TNode>* vec,
                                AssertionPipeline* assertions)
 {
   TNodeSet seen;
-  NodeManager* nm = NodeManager::currentNM();
   TNode term;
   while (!vec->empty())
   {
@@ -203,11 +203,11 @@ size_t getBVSkolemSize(size_t capacity)
  * a sufficient bit-vector size.
  * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to
  * the fresh skolem BV variables. variables */
-void collectUSortsToBV(const std::unordered_set<TNode>& vars,
+void collectUSortsToBV(NodeManager* nm,
+                       const std::unordered_set<TNode>& vars,
                        const USortToBVSizeMap& usortCardinality,
                        SubstitutionMap& usVarsToBVVars)
 {
-  NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
 
   for (TNode var : vars)
@@ -253,7 +253,8 @@ std::unordered_set<TNode> getVarsWithUSorts(AssertionPipeline* assertions)
  * size. The size is calculated to have enough capacity, that can accommodate
  * the variables occured in the original formula. At the end, all variables of
  * uninterpreted sorts will be converted into Skolem variables of BV */
-void usortsToBitVectors(const LogicInfo& d_logic,
+void usortsToBitVectors(NodeManager* nm,
+                        const LogicInfo& d_logic,
                         AssertionPipeline* assertions,
                         USortToBVSizeMap& usortCardinality,
                         SubstitutionMap& usVarsToBVVars)
@@ -277,7 +278,7 @@ void usortsToBitVectors(const LogicInfo& d_logic,
       usortCardinality[type] = usortCardinality[type] + 1;
     }
 
-    collectUSortsToBV(toProcess, usortCardinality, usVarsToBVVars);
+    collectUSortsToBV(nm, toProcess, usortCardinality, usVarsToBVVars);
 
     for (size_t i = 0, size = assertions->size(); i < size; ++i)
     {
@@ -315,8 +316,11 @@ PreprocessingPassResult Ackermann::applyInternal(
   {
     to_process.push_back(a);
   }
-  collectFunctionsAndLemmas(
-      d_funcToArgs, d_funcToSkolem, &to_process, assertionsToPreprocess);
+  collectFunctionsAndLemmas(nodeManager(),
+                            d_funcToArgs,
+                            d_funcToSkolem,
+                            &to_process,
+                            assertionsToPreprocess);
 
   /* replace applications of UF by skolems */
   // FIXME for model building, github issue #1901
@@ -327,8 +331,11 @@ PreprocessingPassResult Ackermann::applyInternal(
   }
 
   /* replace uninterpreted sorts with bit-vectors */
-  usortsToBitVectors(
-      d_logic, assertionsToPreprocess, d_usortCardinality, d_usVarsToBVVars);
+  usortsToBitVectors(nodeManager(),
+                     d_logic,
+                     assertionsToPreprocess,
+                     d_usortCardinality,
+                     d_usVarsToBVVars);
 
   return PreprocessingPassResult::NO_CONFLICT;
 }