From d43e5fb294d89ba69f7d2607a12c8700b7ec9345 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 14 Sep 2016 16:41:27 -0500 Subject: [PATCH] Support for unique variable generation in node manager. --- src/expr/expr_manager_template.cpp | 5 ++--- src/expr/expr_manager_template.h | 4 ++-- src/expr/node_manager.cpp | 13 +++++++------ src/expr/node_manager.h | 10 +++++----- src/parser/smt2/Smt2.g | 2 +- src/parser/smt2/smt2.cpp | 2 ++ src/theory/sep/theory_sep.cpp | 2 +- 7 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index aa5634e7a..6d8497a60 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -941,11 +941,10 @@ Expr ExprManager::mkBoundVar(Type type) { return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode)); } -Expr ExprManager::mkSepNil(Type type) { +Expr ExprManager::mkUniqueVar(Type type, Kind k){ NodeManagerScope nms(d_nodeManager); - Node n = d_nodeManager->mkSepNil(*type.d_typeNode); + Node n = d_nodeManager->mkUniqueVar(*type.d_typeNode, k); return n.toExpr(); - //return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode)); } Expr ExprManager::mkAssociative(Kind kind, diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index f30b720de..95b9c60bf 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -547,9 +547,9 @@ public: Expr mkBoundVar(Type type); /** - * Create a (nameless) new nil reference for separation logic of type + * Create unique variable of type */ - Expr mkSepNil(Type type); + Expr mkUniqueVar( Type type, Kind k); /** Get a reference to the statistics registry for this ExprManager */ Statistics getStatistics() const throw(); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 94b136c46..f7e76c06b 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -170,7 +170,7 @@ NodeManager::~NodeManager() { d_operators[i] = Node::null(); } - d_sep_nils.clear(); + d_unique_vars.clear(); //d_tupleAndRecordTypes.clear(); d_tt_cache.d_children.clear(); @@ -683,13 +683,14 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { return n; } -Node NodeManager::mkSepNil(const TypeNode& type) { - std::map< TypeNode, Node >::iterator it = d_sep_nils.find( type ); - if( it==d_sep_nils.end() ){ - Node n = NodeBuilder<0>(this, kind::SEP_NIL); +Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) { + std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); + if( it==d_unique_vars[k].end() ){ + Node n = NodeBuilder<0>(this, k); n.setAttribute(TypeAttr(), type); n.setAttribute(TypeCheckedAttr(), true); - d_sep_nils[type] = n; + d_unique_vars[k][type] = n; + Assert( n.getMetaKind() == kind::metakind::VARIABLE ); return n; }else{ return it->second; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 79c7320f7..3c3636d5f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -158,8 +158,8 @@ class NodeManager { */ Node d_operators[kind::LAST_KIND]; - /** sep nil per type */ - std::map< TypeNode, Node > d_sep_nils; + /** unique vars per (Kind,Type) */ + std::map< Kind, std::map< TypeNode, Node > > d_unique_vars; /** * A list of subscribers for NodeManager events. @@ -489,12 +489,12 @@ public: /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); - - /** Create nil reference for separation logic with the given type (unique per type). */ - Node mkSepNil(const TypeNode& type); /** Make a new abstract value with the given type. */ Node mkAbstractValue(const TypeNode& type); + + /** make unique (per Type,Kind) variable. */ + Node mkUniqueVar(const TypeNode& type, Kind k); /** * Create a constant of type T. It will have the appropriate diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 29d3e45b6..f88b30212 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1610,7 +1610,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } else if(f.getKind() == CVC4::kind::SEP_NIL_REF) { //We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational. //However, the expression has 0 children. So we convert to a SEP_NIL variable. - expr = EXPR_MANAGER->mkSepNil(type); + expr = EXPR_MANAGER->mkUniqueVar(type, kind::SEP_NIL); } else { if(f.getType() != type) { PARSER_STATE->parseError("Type ascription not satisfied."); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a46eae475..8db344f92 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -368,6 +368,8 @@ void Smt2::setLogic(std::string name) { name = "UFBV"; } else if(name == "SLIA") { name = "UFSLIA"; + } else if(name == "SAT") { + name = "UF"; } else if(name == "ALL_SUPPORTED") { //no change } else { diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 7ee5a1b73..7b4200db0 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1129,7 +1129,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { Node TheorySep::getNilRef( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); if( it==d_nil_ref.end() ){ - Node nil = NodeManager::currentNM()->mkSepNil( tn ); + Node nil = NodeManager::currentNM()->mkUniqueVar( tn, kind::SEP_NIL ); setNilRef( tn, nil ); return nil; }else{ -- 2.30.2