Fix global-declarations support (#3403)

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 73e9239b8a2473c166f2840ef832f46981d206cf..9829b70d95b5d9907d19026a3d0ad076c74b70b3 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -274,14 +274,20 @@ void Parser::defineVar(const std::string& name, const Expr& val,
   assert(isDeclared(name));
 }
 
-void Parser::defineType(const std::string& name, const Type& type) {
-  d_symtab->bindType(name, type);
+void Parser::defineType(const std::string& name,
+                        const Type& type,
+                        bool levelZero)
+{
+  d_symtab->bindType(name, type, levelZero);
   assert(isDeclared(name, SYM_SORT));
 }
 
 void Parser::defineType(const std::string& name,
-                        const std::vector<Type>& params, const Type& type) {
-  d_symtab->bindType(name, params, type);
+                        const std::vector<Type>& params,
+                        const Type& type,
+                        bool levelZero)
+{
+  d_symtab->bindType(name, params, type, levelZero);
   assert(isDeclared(name, SYM_SORT));
 }
 
@@ -302,12 +308,12 @@ void Parser::defineParameterizedType(const std::string& name,
 }
 
 SortType Parser::mkSort(const std::string& name, uint32_t flags) {
-  if (d_globalDeclarations) {
-    flags |= ExprManager::VAR_FLAG_GLOBAL;
-  }
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Type type = getExprManager()->mkSort(name, flags);
-  defineType(name, type);
+  defineType(
+      name,
+      type,
+      d_globalDeclarations && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
   return type;
 }
 
@@ -319,7 +325,11 @@ SortConstructorType Parser::mkSortConstructor(const std::string& name,
                   << std::endl;
   SortConstructorType type =
       getExprManager()->mkSortConstructor(name, arity, flags);
-  defineType(name, vector<Type>(arity), type);
+  defineType(
+      name,
+      vector<Type>(arity),
+      type,
+      d_globalDeclarations && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
   return type;
 }
 
@@ -374,9 +384,9 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
       }
       if (t.isParametric()) {
         std::vector<Type> paramTypes = t.getParamTypes();
-        defineType(name, paramTypes, t);
+        defineType(name, paramTypes, t, d_globalDeclarations);
       } else {
-        defineType(name, t);
+        defineType(name, t, d_globalDeclarations);
       }
       std::unordered_set< std::string > consNames;
       std::unordered_set< std::string > selNames;
@@ -391,7 +401,8 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
           if(!doOverload) {
             checkDeclaration(constructorName, CHECK_UNDECLARED);
           }
-          defineVar(constructorName, constructor, false, doOverload);
+          defineVar(
+              constructorName, constructor, d_globalDeclarations, doOverload);
           consNames.insert(constructorName);
         }else{
           throw ParserException(constructorName + " already declared in this datatype");
@@ -402,7 +413,7 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
         if(!doOverload) {
           checkDeclaration(testerName, CHECK_UNDECLARED);
         }
-        defineVar(testerName, tester, false, doOverload);
+        defineVar(testerName, tester, d_globalDeclarations, doOverload);
         for (DatatypeConstructor::const_iterator k = ctor.begin(),
                                                  k_end = ctor.end();
              k != k_end; ++k) {
@@ -413,7 +424,7 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
             if(!doOverload) {
               checkDeclaration(selectorName, CHECK_UNDECLARED);
             }
-            defineVar(selectorName, selector, false, doOverload);
+            defineVar(selectorName, selector, d_globalDeclarations, doOverload);
             selNames.insert(selectorName);
           }else{
             throw ParserException(selectorName + " already declared in this datatype");

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 28a033eb9ced3c8d4286ad053f3d878b1fa05d6a..42badf4c5ed1cef6ace4ab3ec10c8954a1a582e4 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -526,12 +526,31 @@ public:
   void defineVar(const std::string& name, const Expr& val,
                  bool levelZero = false, bool doOverload = false);
 
-  /** Create a new type definition. */
-  void defineType(const std::string& name, const Type& type);
+  /**
+   * Create a new type definition.
+   *
+   * @param name The name of the type
+   * @param type The type that should be associated with the name
+   * @param levelZero If true, the type definition is considered global and
+   *                  cannot be removed by poppoing the user context
+   */
+  void defineType(const std::string& name,
+                  const Type& type,
+                  bool levelZero = false);
 
-  /** Create a new (parameterized) type definition. */
+  /**
+   * Create a new (parameterized) type definition.
+   *
+   * @param name The name of the type
+   * @param params The type parameters
+   * @param type The type that should be associated with the name
+   * @param levelZero If true, the type definition is considered global and
+   *                  cannot be removed by poppoing the user context
+   */
   void defineType(const std::string& name,
-                  const std::vector<Type>& params, const Type& type);
+                  const std::vector<Type>& params,
+                  const Type& type,
+                  bool levelZero = false);
 
   /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
   void defineParameterizedType(const std::string& name,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8fc4b6410135aa20bb2aa44a2973e13f9ac63446..7c0ab47a0b4f1e210ca09c325aa806d2b39ecc35 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -846,6 +846,7 @@ set(regress_0_tests
   regress0/smallcnf.cvc
   regress0/smt2output.smt2
   regress0/smtlib/get-unsat-assumptions.smt2
+  regress0/smtlib/global-decls.smt2
   regress0/smtlib/reason-unknown.smt2
   regress0/smtlib/set-info-status.smt2
   regress0/strings/bug001.smt2

diff --git a/test/regress/regress0/datatypes/bug597-rbt.smt2 b/test/regress/regress0/datatypes/bug597-rbt.smt2
index 078fa59f7b3afa56fc75d3d9d30cfff394ace4fc..236865aa3ae94bb9e57126ce43920033e4b5e49a 100644 (file)
--- a/test/regress/regress0/datatypes/bug597-rbt.smt2
+++ b/test/regress/regress0/datatypes/bug597-rbt.smt2
@@ -1,3 +1,4 @@
+(set-option :global-declarations true)
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 

diff --git a/test/regress/regress0/smtlib/global-decls.smt2 b/test/regress/regress0/smtlib/global-decls.smt2
new file mode 100644 (file)
index 0000000..a8b6c17
--- /dev/null
+++ b/test/regress/regress0/smtlib/global-decls.smt2
@@ -0,0 +1,29 @@
+; COMMAND-LINE: --incremental
+(set-option :global-declarations true)
+(set-logic QF_UFDTLIA)
+
+(push 1)
+(declare-datatype Struct1 (par (T0) ((mk-struct1 (struct1-proj0 T0)))))
+(declare-datatypes ((Unit 0)) (((u))))
+(declare-datatypes ((Tree 0)) (((node (data Int) (color Bool) (left Tree) (right Tree)) (nil))))
+(declare-fun x () (Struct1 Bool))
+(declare-sort U1 0)
+(declare-sort U2 1)
+(pop 1)
+
+(assert (= x x))
+
+(define-fun y () (Struct1 Bool) (mk-struct1 true))
+(declare-const z Unit)
+(assert (= u u))
+(assert (is-mk-struct1 y))
+(assert (is-u z))
+
+(declare-fun size (Tree) Int)
+(assert (= (size nil) 0))
+
+(declare-const w1 U1)
+(declare-const w2 (U2 Bool))
+
+(set-info :status sat)
+(check-sat)