diff options
Diffstat (limited to 'src/expr')
60 files changed, 422 insertions, 233 deletions
diff --git a/src/expr/array.h b/src/expr/array.h index 580ba5d06..a53ac3cd2 100644 --- a/src/expr/array.h +++ b/src/expr/array.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,11 +16,11 @@ #include "cvc4_public.h" -#ifndef __CVC4__ARRAY_H -#define __CVC4__ARRAY_H +#ifndef CVC4__ARRAY_H +#define CVC4__ARRAY_H // we get ArrayType right now by #including type.h. // array.h is still useful for the auto-generated kinds #includes. #include "expr/type.h" -#endif /* __CVC4__ARRAY_H */ +#endif /* CVC4__ARRAY_H */ diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index 0f66273e1..eff2c2151 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index 9375d8648..0adcfde36 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -18,8 +18,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__ARRAY_STORE_ALL_H -#define __CVC4__ARRAY_STORE_ALL_H +#ifndef CVC4__ARRAY_STORE_ALL_H +#define CVC4__ARRAY_STORE_ALL_H #include <iosfwd> #include <memory> @@ -72,4 +72,4 @@ struct CVC4_PUBLIC ArrayStoreAllHashFunction { } // namespace CVC4 -#endif /* __CVC4__ARRAY_STORE_ALL_H */ +#endif /* CVC4__ARRAY_STORE_ALL_H */ diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h index 331ac8849..94258896a 100644 --- a/src/expr/ascription_type.h +++ b/src/expr/ascription_type.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__ASCRIPTION_TYPE_H -#define __CVC4__ASCRIPTION_TYPE_H +#ifndef CVC4__ASCRIPTION_TYPE_H +#define CVC4__ASCRIPTION_TYPE_H #include "expr/type.h" @@ -63,4 +63,4 @@ inline std::ostream& operator<<(std::ostream& out, AscriptionType at) { }/* CVC4 namespace */ -#endif /* __CVC4__ASCRIPTION_TYPE_H */ +#endif /* CVC4__ASCRIPTION_TYPE_H */ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 9481cde99..b9234883b 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -2,9 +2,9 @@ /*! \file attribute.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Dejan Jovanovic + ** Tim King, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/attribute.h b/src/expr/attribute.h index db6fb52a0..46302fc9f 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -21,8 +21,8 @@ #include "expr/node.h" #include "expr/type_node.h" -#ifndef __CVC4__EXPR__ATTRIBUTE_H -#define __CVC4__EXPR__ATTRIBUTE_H +#ifndef CVC4__EXPR__ATTRIBUTE_H +#define CVC4__EXPR__ATTRIBUTE_H #include <string> #include <stdint.h> @@ -578,4 +578,4 @@ NodeManager::setAttribute(TypeNode n, const AttrKind&, }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__ATTRIBUTE_H */ +#endif /* CVC4__EXPR__ATTRIBUTE_H */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index c6dc66eb2..e47dce434 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -20,8 +20,8 @@ # error expr/attribute_internals.h should only be included by expr/attribute.h #endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */ -#ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H -#define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H +#ifndef CVC4__EXPR__ATTRIBUTE_INTERNALS_H +#define CVC4__EXPR__ATTRIBUTE_INTERNALS_H #include <cstdint> #include <unordered_map> @@ -486,4 +486,4 @@ const uint64_t Attribute<T, bool, context_dep>::s_id = }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__ATTRIBUTE_INTERNALS_H */ +#endif /* CVC4__EXPR__ATTRIBUTE_INTERNALS_H */ diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h index 1a6220db2..88ecc90a8 100644 --- a/src/expr/attribute_unique_id.h +++ b/src/expr/attribute_unique_id.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/chain.h b/src/expr/chain.h index 6a785f282..9df819b4d 100644 --- a/src/expr/chain.h +++ b/src/expr/chain.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__CHAIN_H -#define __CVC4__CHAIN_H +#ifndef CVC4__CHAIN_H +#define CVC4__CHAIN_H #include "expr/kind.h" #include <iostream> @@ -48,4 +48,4 @@ struct CVC4_PUBLIC ChainHashFunction { }/* CVC4 namespace */ -#endif /* __CVC4__CHAIN_H */ +#endif /* CVC4__CHAIN_H */ diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 8bedd4979..3b925d0b1 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 615ad0e10..0e8ace709 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__DATATYPE_H -#define __CVC4__DATATYPE_H +#ifndef CVC4__DATATYPE_H +#define CVC4__DATATYPE_H #include <functional> #include <iostream> @@ -1288,4 +1288,4 @@ inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const }/* CVC4 namespace */ -#endif /* __CVC4__DATATYPE_H */ +#endif /* CVC4__DATATYPE_H */ diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp index f9093cb22..789eaf20e 100644 --- a/src/expr/emptyset.cpp +++ b/src/expr/emptyset.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index 8cca1e4b8..a9487e9a7 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -2,9 +2,9 @@ /*! \file emptyset.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Tim King, Morgan Deters + ** Tim King, Kshitij Bansal, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp index 6be2e37f1..22600d79d 100644 --- a/src/expr/expr_iomanip.cpp +++ b/src/expr/expr_iomanip.cpp @@ -2,9 +2,9 @@ /*! \file expr_iomanip.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Tim King, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index 936a62589..9a582f8c8 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -2,9 +2,9 @@ /*! \file expr_iomanip.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__EXPR__EXPR_IOMANIP_H -#define __CVC4__EXPR__EXPR_IOMANIP_H +#ifndef CVC4__EXPR__EXPR_IOMANIP_H +#define CVC4__EXPR__EXPR_IOMANIP_H #include <iosfwd> @@ -236,4 +236,4 @@ std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) CVC4_PUBLIC; }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__EXPR_IOMANIP_H */ +#endif /* CVC4__EXPR__EXPR_IOMANIP_H */ diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h index a546638ad..b494796a1 100644 --- a/src/expr/expr_manager_scope.h +++ b/src/expr/expr_manager_scope.h @@ -2,9 +2,9 @@ /*! \file expr_manager_scope.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters + ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR_MANAGER_SCOPE_H -#define __CVC4__EXPR_MANAGER_SCOPE_H +#ifndef CVC4__EXPR_MANAGER_SCOPE_H +#define CVC4__EXPR_MANAGER_SCOPE_H #include "expr/expr.h" #include "expr/node_manager.h" @@ -66,4 +66,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_MANAGER_SCOPE_H */ +#endif /* CVC4__EXPR_MANAGER_SCOPE_H */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index d0d36508f..988705aa8 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 4e0ab700c..17affaef0 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -2,9 +2,9 @@ /*! \file expr_manager_template.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway + ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__EXPR_MANAGER_H -#define __CVC4__EXPR_MANAGER_H +#ifndef CVC4__EXPR_MANAGER_H +#define CVC4__EXPR_MANAGER_H #include <vector> @@ -520,7 +520,7 @@ public: /** * Create a new, fresh variable for use in a binder expression - * (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). It is + * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE). It is * an error for this bound variable to exist outside of a binder, * and it should also only be used in a single binder expression. * That is, two distinct FORALL expressions should use entirely @@ -539,7 +539,7 @@ public: /** * Create a (nameless) new, fresh variable for use in a binder - * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). + * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE). * It is an error for this bound variable to exist outside of a * binder, and it should also only be used in a single binder * expression. That is, two distinct FORALL expressions should use @@ -586,4 +586,4 @@ ${mkConst_instantiations} }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_MANAGER_H */ +#endif /* CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h index 77ada6f11..d31e8e4fc 100644 --- a/src/expr/expr_stream.h +++ b/src/expr/expr_stream.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__EXPR_STREAM_H -#define __CVC4__EXPR_STREAM_H +#ifndef CVC4__EXPR_STREAM_H +#define CVC4__EXPR_STREAM_H #include "expr/expr.h" @@ -41,5 +41,5 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_STREAM_H */ +#endif /* CVC4__EXPR_STREAM_H */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 96bdb2d04..d6a6f47bb 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -33,7 +33,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 36 "${template}" +#line 37 "${template}" using namespace CVC4::kind; using namespace std; @@ -200,6 +200,10 @@ public: TypeNode typeNode = TypeNode::fromType(type); NodeManager* to_nm = NodeManager::fromExprManager(to); Node n = to_nm->mkBoundVar(name, typeNode); // FIXME thread safety + + // Make sure that the correct `NodeManager` is in scope while + // converting the node to an expression. + NodeManagerScope to_nms(to_nm); to_e = n.toExpr(); } else if(n.getKind() == kind::VARIABLE) { bool isGlobal; @@ -214,6 +218,10 @@ public: TypeNode typeNode = TypeNode::fromType(type); NodeManager* to_nm = NodeManager::fromExprManager(to); Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety + + // Make sure that the correct `NodeManager` is in scope while + // converting the node to an expression. + NodeManagerScope to_nms(to_nm); to_e = n.toExpr(); } else { Unhandled(); @@ -228,6 +236,10 @@ public: TypeNode typeNode = TypeNode::fromType(type); NodeManager* to_nm = NodeManager::fromExprManager(to); Node n = to_nm->mkBoundVar(typeNode); // FIXME thread safety + + // Make sure that the correct `NodeManager` is in scope while + // converting the node to an expression. + NodeManagerScope to_nms(to_nm); to_e = n.toExpr(); } else @@ -244,6 +256,11 @@ public: vmap.d_from[to_int] = from_int; vmap.d_to[from_int] = to_int; vmap.d_typeMap[to_e] = from_e;// insert other direction too + + // Make sure that the expressions are associated with the correct + // `ExprManager`s. + Assert(from_e.getExprManager() == from); + Assert(to_e.getExprManager() == to); return Node::fromExpr(to_e); } } else { diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index da9d22389..a32590050 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -23,8 +23,8 @@ // "expr.h" safely, then go on to completely declare their own stuff. ${includes} -#ifndef __CVC4__EXPR_H -#define __CVC4__EXPR_H +#ifndef CVC4__EXPR_H +#define CVC4__EXPR_H #include <stdint.h> #include <iosfwd> @@ -612,7 +612,7 @@ private: ${getConst_instantiations} -#line 613 "${template}" +#line 616 "${template}" inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { return (size_t) e.getId(); @@ -620,4 +620,4 @@ inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_H */ +#endif /* CVC4__EXPR_H */ diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index af66b1630..a5ae73802 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -2,9 +2,9 @@ /*! \file kind_map.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King + ** Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__KIND_MAP_H -#define __CVC4__KIND_MAP_H +#ifndef CVC4__KIND_MAP_H +#define CVC4__KIND_MAP_H #include <stdint.h> #include <iterator> @@ -271,4 +271,4 @@ inline KindMap operator^(Kind k1, KindMap m2) { }/* CVC4 namespace */ -#endif /* __CVC4__KIND_MAP_H */ +#endif /* CVC4__KIND_MAP_H */ diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index dcc98a1b7..e1a933e7b 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -2,9 +2,9 @@ /*! \file kind_template.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Mathias Preiner + ** Andres Noetzli, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -64,7 +64,7 @@ std::string kindToString(::CVC4::Kind k) { std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { switch(typeConstant) { ${type_constant_descriptions} -#line 51 "${template}" +#line 68 "${template}" default: out << "UNKNOWN_TYPE_CONSTANT"; break; @@ -77,7 +77,7 @@ namespace theory { std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { switch(theoryId) { ${theory_descriptions} -#line 64 "${template}" +#line 81 "${template}" default: out << "UNKNOWN_THEORY"; break; @@ -91,7 +91,7 @@ TheoryId kindToTheoryId(::CVC4::Kind k) { case kind::NULL_EXPR: break; ${kind_to_theory_id} -#line 78 "${template}" +#line 95 "${template}" case kind::LAST_KIND: break; } @@ -101,7 +101,7 @@ ${kind_to_theory_id} TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) { switch(typeConstant) { ${type_constant_to_theory_id} -#line 88 "${template}" +#line 105 "${template}" case LAST_TYPE: break; } @@ -111,7 +111,7 @@ ${type_constant_to_theory_id} std::string getStatsPrefix(TheoryId theoryId) { switch(theoryId) { ${theory_stats_prefixes} -#line 98 "${template}" +#line 115 "${template}" default: break; } diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index cdeb5ec88..93c37f6cc 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__KIND_H -#define __CVC4__KIND_H +#ifndef CVC4__KIND_H +#define CVC4__KIND_H #include <iosfwd> @@ -104,4 +104,4 @@ std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__KIND_H */ +#endif /* CVC4__KIND_H */ diff --git a/src/expr/matcher.h b/src/expr/matcher.h index ff0631728..95ece7d23 100644 --- a/src/expr/matcher.h +++ b/src/expr/matcher.h @@ -2,9 +2,9 @@ /*! \file matcher.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__MATCHER_H -#define __CVC4__MATCHER_H +#ifndef CVC4__MATCHER_H +#define CVC4__MATCHER_H #include <iosfwd> #include <string> @@ -116,4 +116,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__MATCHER_H */ +#endif /* CVC4__MATCHER_H */ diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp index 4ffa4dd44..5116392cb 100644 --- a/src/expr/metakind_template.cpp +++ b/src/expr/metakind_template.cpp @@ -2,9 +2,9 @@ /*! \file metakind_template.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Morgan Deters, Andres Noetzli, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 1aad647a6..3550acf05 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -2,9 +2,9 @@ /*! \file metakind_template.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Tim King + ** Morgan Deters, Andres Noetzli, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__KIND__METAKIND_H -#define __CVC4__KIND__METAKIND_H +#ifndef CVC4__KIND__METAKIND_H +#define CVC4__KIND__METAKIND_H #include <iosfwd> @@ -118,13 +118,13 @@ namespace kind { namespace metakind { /* these are #defines so their sum can be #if-checked in node_value.h */ -#define __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 20 -#define __CVC4__EXPR__NODE_VALUE__NBITS__KIND 10 -#define __CVC4__EXPR__NODE_VALUE__NBITS__ID 40 -#define __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 26 +#define CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 20 +#define CVC4__EXPR__NODE_VALUE__NBITS__KIND 10 +#define CVC4__EXPR__NODE_VALUE__NBITS__ID 40 +#define CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 26 static const unsigned MAX_CHILDREN = - (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1; + (1u << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1; }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ @@ -143,11 +143,11 @@ struct NodeValuePoolEq { #include "expr/node_value.h" -#endif /* __CVC4__KIND__METAKIND_H */ +#endif /* CVC4__KIND__METAKIND_H */ ${metakind_includes} -#ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP namespace CVC4 { @@ -234,4 +234,4 @@ ${theory_alternate_doc}"; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */ +#endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */ diff --git a/src/expr/node.cpp b/src/expr/node.cpp index b983c81f5..de1d5475b 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -2,9 +2,9 @@ /*! \file node.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Morgan Deters, Tim King, Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/node.h b/src/expr/node.h index 750a5547b..768d7b948 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -19,8 +19,8 @@ // circular dependency #include "expr/node_value.h" -#ifndef __CVC4__NODE_H -#define __CVC4__NODE_H +#ifndef CVC4__NODE_H +#define CVC4__NODE_H #include <stdint.h> @@ -459,7 +459,7 @@ public: assertTNodeNotExpired(); return getMetaKind() == kind::metakind::VARIABLE; } - + /** * Returns true if this node represents a nullary operator */ @@ -467,13 +467,15 @@ public: assertTNodeNotExpired(); return getMetaKind() == kind::metakind::NULLARY_OPERATOR; } - + + /** + * Returns true if this node represents a closure, that is an expression + * that binds variables. + */ inline bool isClosure() const { assertTNodeNotExpired(); - return getKind() == kind::LAMBDA || - getKind() == kind::FORALL || - getKind() == kind::EXISTS || - getKind() == kind::REWRITE_RULE; + return getKind() == kind::LAMBDA || getKind() == kind::FORALL + || getKind() == kind::EXISTS || getKind() == kind::CHOICE; } /** @@ -487,7 +489,7 @@ public: /** * Returns a node representing the operator of this expression. - * If this is an APPLY, then the operator will be a functional term. + * If this is an APPLY_UF, then the operator will be a functional term. * Otherwise, it will be a node with kind BUILTIN. */ NodeTemplate<true> getOperator() const; @@ -1271,7 +1273,7 @@ NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const { /** * Returns a node representing the operator of this expression. - * If this is an APPLY, then the operator will be a functional term. + * If this is an APPLY_UF, then the operator will be a functional term. * Otherwise, it will be a node with kind BUILTIN. */ template <bool ref_count> @@ -1568,4 +1570,4 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& }/* CVC4 namespace */ -#endif /* __CVC4__NODE_H */ +#endif /* CVC4__NODE_H */ diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 3905ad5c9..25ffb0778 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -2,9 +2,9 @@ /*! \file node_algorithm.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -159,6 +159,14 @@ bool hasBoundVar(TNode n) bool hasFreeVar(TNode n) { + std::unordered_set<Node, NodeHashFunction> fvs; + return getFreeVariables(n, fvs, false); +} + +bool getFreeVariables(TNode n, + std::unordered_set<Node, NodeHashFunction>& fvs, + bool computeFv) +{ std::unordered_set<TNode, TNodeHashFunction> bound_var; std::unordered_map<TNode, bool, TNodeHashFunction> visited; std::vector<TNode> visit; @@ -174,8 +182,7 @@ bool hasFreeVar(TNode n) continue; } Kind k = cur.getKind(); - bool isQuant = k == kind::FORALL || k == kind::EXISTS || k == kind::LAMBDA - || k == kind::CHOICE; + bool isQuant = cur.isClosure(); std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv = visited.find(cur); if (itv == visited.end()) @@ -184,7 +191,14 @@ bool hasFreeVar(TNode n) { if (bound_var.find(cur) == bound_var.end()) { - return true; + if (computeFv) + { + fvs.insert(cur); + } + else + { + return true; + } } } else if (isQuant) @@ -218,7 +232,8 @@ bool hasFreeVar(TNode n) visited[cur] = true; } } while (!visit.empty()); - return false; + + return !fvs.empty(); } void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms) @@ -257,5 +272,117 @@ void getSymbols(TNode n, } while (!visit.empty()); } +Node substituteCaptureAvoiding(TNode n, Node src, Node dest) +{ + if (n == src) + { + return dest; + } + if (src == dest) + { + return n; + } + std::vector<Node> srcs; + std::vector<Node> dests; + srcs.push_back(src); + dests.push_back(dest); + return substituteCaptureAvoiding(n, srcs, dests); +} + +Node substituteCaptureAvoiding(TNode n, + std::vector<Node>& src, + std::vector<Node>& dest) +{ + std::unordered_map<TNode, Node, TNodeHashFunction> visited; + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::vector<TNode> visit; + TNode curr; + visit.push_back(n); + Assert(src.size() == dest.size(), + "Substitution domain and range must be equal size"); + do + { + curr = visit.back(); + visit.pop_back(); + it = visited.find(curr); + + if (it == visited.end()) + { + auto itt = std::find(src.rbegin(), src.rend(), curr); + if (itt != src.rend()) + { + Assert( + (std::distance(src.begin(), itt.base()) - 1) >= 0 + && static_cast<unsigned>(std::distance(src.begin(), itt.base()) - 1) + < dest.size()); + Node n = dest[std::distance(src.begin(), itt.base()) - 1]; + visited[curr] = n; + continue; + } + if (curr.getNumChildren() == 0) + { + visited[curr] = curr; + continue; + } + + visited[curr] = Node::null(); + // if binder, rename variables to avoid capture + if (curr.isClosure()) + { + NodeManager* nm = NodeManager::currentNM(); + // have new vars -> renames subs in the end of current sub + for (const Node& v : curr[0]) + { + src.push_back(v); + dest.push_back(nm->mkBoundVar(v.getType())); + } + } + // save for post-visit + visit.push_back(curr); + // visit children + if (curr.getMetaKind() == kind::metakind::PARAMETERIZED) + { + // push the operator + visit.push_back(curr.getOperator()); + } + for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i) + { + visit.push_back(curr[i]); + } + } + else if (it->second.isNull()) + { + // build node + NodeBuilder<> nb(curr.getKind()); + if (curr.getMetaKind() == kind::metakind::PARAMETERIZED) + { + // push the operator + Assert(visited.find(curr.getOperator()) != visited.end()); + nb << visited[curr.getOperator()]; + } + // collect substituted children + for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i) + { + Assert(visited.find(curr[i]) != visited.end()); + nb << visited[curr[i]]; + } + Node n = nb; + visited[curr] = n; + + // remove renaming + if (curr.isClosure()) + { + // remove beginning of sub which correspond to renaming of variables in + // this binder + unsigned nchildren = curr[0].getNumChildren(); + src.resize(src.size() - nchildren); + dest.resize(dest.size() - nchildren); + } + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + return visited[n]; +} + } // namespace expr } // namespace CVC4 diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index d825d7f57..656f162ae 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -2,9 +2,9 @@ /*! \file node_algorithm.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Andres Noetzli, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR__NODE_ALGORITHM_H -#define __CVC4__EXPR__NODE_ALGORITHM_H +#ifndef CVC4__EXPR__NODE_ALGORITHM_H +#define CVC4__EXPR__NODE_ALGORITHM_H #include <unordered_map> #include <vector> @@ -60,6 +60,19 @@ bool hasBoundVar(TNode n); bool hasFreeVar(TNode n); /** + * Get the free variables in n, that is, the subterms of n of kind + * BOUND_VARIABLE that are not bound in n, adds these to fvs. + * @param n The node under investigation + * @param fvs The set which free variables are added to + * @param computeFv If this flag is false, then we only return true/false and + * do not add to fvs. + * @return true iff this node contains a free variable. + */ +bool getFreeVariables(TNode n, + std::unordered_set<Node, NodeHashFunction>& fvs, + bool computeFv = true); + +/** * For term n, this function collects the symbols that occur as a subterms * of n. A symbol is a variable that does not have kind BOUND_VARIABLE. * @param n The node under investigation @@ -70,6 +83,19 @@ void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms); void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms, std::unordered_set<TNode, TNodeHashFunction>& visited); +/** + * Substitution of Nodes in a capture avoiding way. + */ +Node substituteCaptureAvoiding(TNode n, Node src, Node dest); + +/** + * Simultaneous substitution of Nodes in a capture avoiding way. Elements in + * source will be replaced by their corresponding element in dest. Both + * vectors should have the same size. + */ +Node substituteCaptureAvoiding(TNode n, + std::vector<Node>& src, + std::vector<Node>& dest); } // namespace expr } // namespace CVC4 diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 9f258c560..9128bc190 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -152,8 +152,8 @@ #include "expr/node.h" #include "expr/type_node.h" -#ifndef __CVC4__NODE_BUILDER_H -#define __CVC4__NODE_BUILDER_H +#ifndef CVC4__NODE_BUILDER_H +#define CVC4__NODE_BUILDER_H #include <cstdlib> #include <iostream> @@ -274,7 +274,7 @@ class NodeBuilder { */ inline void realloc() { size_t newSize = 2 * size_t(d_nvMaxChildren); - size_t hardLimit = (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1; + size_t hardLimit = (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1; realloc(__builtin_expect( ( newSize > hardLimit ), false ) ? hardLimit : newSize); } @@ -774,9 +774,9 @@ template <unsigned nchild_thresh> void NodeBuilder<nchild_thresh>::realloc(size_t toSize) { Assert( toSize > d_nvMaxChildren, "attempt to realloc() a NodeBuilder to a smaller/equal size!" ); - Assert( toSize < (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN), + Assert( toSize < (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN), "attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)", - toSize, (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 ); + toSize, (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 ); if(__builtin_expect( ( nvIsAllocated() ), false )) { // Ensure d_nv is not modified on allocation failure @@ -1342,4 +1342,4 @@ std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb }/* CVC4 namespace */ -#endif /* __CVC4__NODE_BUILDER_H */ +#endif /* CVC4__NODE_BUILDER_H */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a40d1511b..66d597a36 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -2,9 +2,9 @@ /*! \file node_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -363,7 +363,10 @@ void NodeManager::reclaimZombies() { std::vector<NodeValue*> NodeManager::TopologicalSort( const std::vector<NodeValue*>& roots) { std::vector<NodeValue*> order; + // The stack of nodes to visit. The Boolean value is false when visiting the + // node in preorder and true when visiting it in postorder. std::vector<std::pair<bool, NodeValue*> > stack; + // Nodes that have been visited in both pre- and postorder NodeValueIDSet visited; const NodeValueIDSet root_set(roots.begin(), roots.end()); @@ -382,17 +385,20 @@ std::vector<NodeValue*> NodeManager::TopologicalSort( order.push_back(current); } stack.pop_back(); - } else { + } + else if (visited.find(current) == visited.end()) + { stack.back().first = true; - Assert(visited.count(current) == 0); visited.insert(current); for (unsigned i = 0; i < current->getNumChildren(); ++i) { expr::NodeValue* child = current->getChild(i); - if (visited.find(child) == visited.end()) { - stack.push_back(std::make_pair(false, child)); - } + stack.push_back(std::make_pair(false, child)); } } + else + { + stack.pop_back(); + } } } Assert(order.size() == roots.size()); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 7cafb6e11..510e6d585 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -25,8 +25,8 @@ #include "expr/expr.h" #include "expr/expr_manager.h" -#ifndef __CVC4__NODE_MANAGER_H -#define __CVC4__NODE_MANAGER_H +#ifndef CVC4__NODE_MANAGER_H +#define CVC4__NODE_MANAGER_H #include <vector> #include <string> @@ -276,6 +276,17 @@ class NodeManager { Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") << std::endl; } + + // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies` + // already contains a node value with the same id as `nv`, but the pointers + // are different, then the wrong `NodeManager` was in scope for one of the + // two nodes when it reached refcount zero. This can happen for example if + // you create a node with a `NodeManager` n1 and then call `Node::toExpr()` + // on that node while a different `NodeManager` n2 is in scope. When that + // `Expr` is deleted and the node reaches refcount zero in the `Expr`'s + // destructor, then `markForDeletion()` will be called on n2. + Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv); + d_zombies.insert(nv); // FIXME multithreading if(safeToReclaimZombies()) { @@ -1204,9 +1215,9 @@ inline TypeNode NodeManager::fromType(Type t) { }/* CVC4 namespace */ -#define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/metakind.h" -#undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/node_builder.h" @@ -1548,4 +1559,4 @@ NodeClass NodeManager::mkConstInternal(const T& val) { }/* CVC4 namespace */ -#endif /* __CVC4__NODE_MANAGER_H */ +#endif /* CVC4__NODE_MANAGER_H */ diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h index fe2e38924..99bfcb8a9 100644 --- a/src/expr/node_manager_attributes.h +++ b/src/expr/node_manager_attributes.h @@ -2,9 +2,9 @@ /*! \file node_manager_attributes.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/node_manager_listeners.cpp b/src/expr/node_manager_listeners.cpp index a38181107..ecb089dc9 100644 --- a/src/expr/node_manager_listeners.cpp +++ b/src/expr/node_manager_listeners.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/node_manager_listeners.h b/src/expr/node_manager_listeners.h index 6834aabbb..501c6129f 100644 --- a/src/expr/node_manager_listeners.h +++ b/src/expr/node_manager_listeners.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR__NODE_MANAGER_LISTENERS_H -#define __CVC4__EXPR__NODE_MANAGER_LISTENERS_H +#ifndef CVC4__EXPR__NODE_MANAGER_LISTENERS_H +#define CVC4__EXPR__NODE_MANAGER_LISTENERS_H #include "base/listener.h" #include "util/resource_manager.h" @@ -64,4 +64,4 @@ class RlimitPerListener : public Listener { }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__NODE_MANAGER_LISTENERS_H */ +#endif /* CVC4__EXPR__NODE_MANAGER_LISTENERS_H */ diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index 6783fd3ea..7e0478acc 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -2,9 +2,9 @@ /*! \file node_self_iterator.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andres Noetzli + ** Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR__NODE_SELF_ITERATOR_H -#define __CVC4__EXPR__NODE_SELF_ITERATOR_H +#ifndef CVC4__EXPR__NODE_SELF_ITERATOR_H +#define CVC4__EXPR__NODE_SELF_ITERATOR_H #include <iterator> @@ -125,4 +125,4 @@ inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const { }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__NODE_SELF_ITERATOR_H */ +#endif /* CVC4__EXPR__NODE_SELF_ITERATOR_H */ diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp index 4404e78ca..0900ec9af 100644 --- a/src/expr/node_trie.cpp +++ b/src/expr/node_trie.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h index d0c0f0627..7aa740a42 100644 --- a/src/expr/node_trie.h +++ b/src/expr/node_trie.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR__NODE_TRIE_H -#define __CVC4__EXPR__NODE_TRIE_H +#ifndef CVC4__EXPR__NODE_TRIE_H +#define CVC4__EXPR__NODE_TRIE_H #include <map> #include "expr/node.h" @@ -109,4 +109,4 @@ typedef NodeTemplateTrie<false> TNodeTrie; } // namespace theory } // namespace CVC4 -#endif /* __CVC4__EXPR__NODE_TRIE_H */ +#endif /* CVC4__EXPR__NODE_TRIE_H */ diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index e3c8ef331..d7faf0814 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -2,9 +2,9 @@ /*! \file node_value.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 6bba80dd1..024a13941 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -2,9 +2,9 @@ /*! \file node_value.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Dejan Jovanovic + ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -23,8 +23,8 @@ // circular dependency #include "expr/metakind.h" -#ifndef __CVC4__EXPR__NODE_VALUE_H -#define __CVC4__EXPR__NODE_VALUE_H +#ifndef CVC4__EXPR__NODE_VALUE_H +#define CVC4__EXPR__NODE_VALUE_H #include <stdint.h> @@ -59,10 +59,10 @@ namespace kind { namespace expr { -#if __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \ - __CVC4__EXPR__NODE_VALUE__NBITS__KIND + \ - __CVC4__EXPR__NODE_VALUE__NBITS__ID + \ - __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 96 +#if CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \ + CVC4__EXPR__NODE_VALUE__NBITS__KIND + \ + CVC4__EXPR__NODE_VALUE__NBITS__ID + \ + CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 96 # error NodeValue header bit assignment does not sum to 96 ! #endif /* sum != 96 */ @@ -71,10 +71,10 @@ namespace expr { */ class NodeValue { - static const unsigned NBITS_REFCOUNT = __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT; - static const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND; - static const unsigned NBITS_ID = __CVC4__EXPR__NODE_VALUE__NBITS__ID; - static const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; + static const unsigned NBITS_REFCOUNT = CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT; + static const unsigned NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND; + static const unsigned NBITS_ID = CVC4__EXPR__NODE_VALUE__NBITS__ID; + static const unsigned NBITS_NCHILDREN = CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; /** Maximum reference count possible. Used for sticky * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */ @@ -549,4 +549,4 @@ static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__NODE_VALUE_H */ +#endif /* CVC4__EXPR__NODE_VALUE_H */ diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp index 709cb4e1a..fd3b69d26 100644 --- a/src/expr/pickle_data.cpp +++ b/src/expr/pickle_data.cpp @@ -2,9 +2,9 @@ /*! \file pickle_data.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h index 7fa23f3d4..316b6285c 100644 --- a/src/expr/pickle_data.h +++ b/src/expr/pickle_data.h @@ -2,9 +2,9 @@ /*! \file pickle_data.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -20,8 +20,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PICKLE_DATA_H -#define __CVC4__PICKLE_DATA_H +#ifndef CVC4__PICKLE_DATA_H +#define CVC4__PICKLE_DATA_H #include <sstream> #include <deque> @@ -44,8 +44,8 @@ namespace expr { namespace pickle { const unsigned NBITS_BLOCK = 64; -const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND; -const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; +const unsigned NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND; +const unsigned NBITS_NCHILDREN = CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; const unsigned NBITS_CONSTBLOCKS = 32; struct BlockHeader { @@ -117,4 +117,4 @@ public: }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PICKLE_DATA_H */ +#endif /* CVC4__PICKLE_DATA_H */ diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index 8e1f07b08..42198d676 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Kshitij Bansal, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/pickler.h b/src/expr/pickler.h index ae9f6d94f..02abdf18d 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -18,8 +18,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__PICKLER_H -#define __CVC4__PICKLER_H +#ifndef CVC4__PICKLER_H +#define CVC4__PICKLER_H #include "expr/variable_type_map.h" #include "expr/expr.h" @@ -126,4 +126,4 @@ protected: }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PICKLER_H */ +#endif /* CVC4__PICKLER_H */ diff --git a/src/expr/record.cpp b/src/expr/record.cpp index 123000ab4..03682c8d4 100644 --- a/src/expr/record.cpp +++ b/src/expr/record.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/record.h b/src/expr/record.h index 3d2abf844..bfa5d9395 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -2,9 +2,9 @@ /*! \file record.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andres Noetzli + ** Tim King, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__RECORD_H -#define __CVC4__RECORD_H +#ifndef CVC4__RECORD_H +#define CVC4__RECORD_H #include <functional> #include <iostream> @@ -90,4 +90,4 @@ std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC; }/* CVC4 namespace */ -#endif /* __CVC4__RECORD_H */ +#endif /* CVC4__RECORD_H */ diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 9401e772c..600f666bc 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 19a42a303..07f557059 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -2,9 +2,9 @@ /*! \file symbol_table.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Christopher L. Conway + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__SYMBOL_TABLE_H -#define __CVC4__SYMBOL_TABLE_H +#ifndef CVC4__SYMBOL_TABLE_H +#define CVC4__SYMBOL_TABLE_H #include <memory> #include <string> @@ -246,4 +246,4 @@ class CVC4_PUBLIC SymbolTable { } // namespace CVC4 -#endif /* __CVC4__SYMBOL_TABLE_H */ +#endif /* CVC4__SYMBOL_TABLE_H */ diff --git a/src/expr/type.cpp b/src/expr/type.cpp index fe8cc097b..f2b5945dd 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/type.h b/src/expr/type.h index 4d22f1538..2c68c9e73 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -2,9 +2,9 @@ /*! \file type.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway + ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__TYPE_H -#define __CVC4__TYPE_H +#ifndef CVC4__TYPE_H +#define CVC4__TYPE_H #include <climits> #include <cstdint> @@ -665,4 +665,4 @@ class CVC4_PUBLIC TesterType : public Type { }/* CVC4 namespace */ -#endif /* __CVC4__TYPE_H */ +#endif /* CVC4__TYPE_H */ diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index 35a4e46a8..8c03cea98 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -19,8 +19,8 @@ // ordering dependence #include "expr/node.h" -#ifndef __CVC4__EXPR__TYPE_CHECKER_H -#define __CVC4__EXPR__TYPE_CHECKER_H +#ifndef CVC4__EXPR__TYPE_CHECKER_H +#define CVC4__EXPR__TYPE_CHECKER_H namespace CVC4 { namespace expr { @@ -40,4 +40,4 @@ public: }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__TYPE_CHECKER_H */ +#endif /* CVC4__EXPR__TYPE_CHECKER_H */ diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 4fbed28a5..078c275f8 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -2,9 +2,9 @@ /*! \file type_checker_template.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b54290612..b093e596e 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 5b0caf659..8ed26596b 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -19,8 +19,8 @@ // circular dependency #include "expr/node_value.h" -#ifndef __CVC4__TYPE_NODE_H -#define __CVC4__TYPE_NODE_H +#ifndef CVC4__TYPE_NODE_H +#define CVC4__TYPE_NODE_H #include <stdint.h> @@ -1072,4 +1072,4 @@ static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) { }/* CVC4 namespace */ -#endif /* __CVC4__NODE_H */ +#endif /* CVC4__NODE_H */ diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 74152a5ac..88447a125 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -2,9 +2,9 @@ /*! \file type_properties_template.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__TYPE_PROPERTIES_H -#define __CVC4__TYPE_PROPERTIES_H +#ifndef CVC4__TYPE_PROPERTIES_H +#define CVC4__TYPE_PROPERTIES_H #line 23 "${template}" @@ -138,4 +138,4 @@ ${type_groundterms} }/* CVC4::kind namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__TYPE_PROPERTIES_H */ +#endif /* CVC4__TYPE_PROPERTIES_H */ diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index 9898bcb3f..5c9daf784 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -2,9 +2,9 @@ /*! \file uninterpreted_constant.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Tim King, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index 6d4081ba0..fb6557497 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h index 04adb246c..ba1c60549 100644 --- a/src/expr/variable_type_map.h +++ b/src/expr/variable_type_map.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__VARIABLE_TYPE_MAP_H -#define __CVC4__VARIABLE_TYPE_MAP_H +#ifndef CVC4__VARIABLE_TYPE_MAP_H +#define CVC4__VARIABLE_TYPE_MAP_H #include <unordered_map> @@ -60,4 +60,4 @@ struct CVC4_PUBLIC ExprManagerMapCollection { }/* CVC4 namespace */ -#endif /* __CVC4__VARIABLE_MAP_H */ +#endif /* CVC4__VARIABLE_MAP_H */ |