From: Andres Noetzli Date: Sun, 27 Oct 2019 18:06:40 +0000 (-0700) Subject: Fix global-declarations support (#3403) X-Git-Tag: cvc5-1.0.0~3873 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=24936010e7d0dc644bd2bf1f533ac0abee678f6b;p=cvc5.git Fix global-declarations support (#3403) --- diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 73e9239b8..9829b70d9 100644 --- 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& params, const Type& type) { - d_symtab->bindType(name, params, type); + const std::vector& 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(arity), type); + defineType( + name, + vector(arity), + type, + d_globalDeclarations && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER)); return type; } @@ -374,9 +384,9 @@ std::vector Parser::mkMutualDatatypeTypes( } if (t.isParametric()) { std::vector 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 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 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 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 28a033eb9..42badf4c5 100644 --- 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& params, const Type& type); + const std::vector& 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 8fc4b6410..7c0ab47a0 100644 --- 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 078fa59f7..236865aa3 100644 --- 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 index 000000000..a8b6c17b2 --- /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)