From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 14 Sep 2016 21:41:27 +0000 (-0500)
Subject: Support for unique variable generation in node manager.
X-Git-Tag: cvc5-1.0.0~6028^2~51
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d43e5fb294d89ba69f7d2607a12c8700b7ec9345;p=cvc5.git

Support for unique variable generation in node manager.
---

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{