Refactoring.

* CreateSymbol now takes the indexWidth and the valueWidth.
* I've removed most of the calls to setIndexWidth.
* CreateSymbol has been moved into the NodeFactory class.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@956 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp
index 3e2e83b3c678dc751e8014c95faa98094c8e176d..26bad1da015bbe16e77ccc08d33e2d746293a2d8 100644 (file)
--- a/src/AST/ASTNode.cpp
+++ b/src/AST/ASTNode.cpp
@@ -266,9 +266,7 @@ namespace BEEV
                 ostringstream oss;
                 oss << "let_k_" << sz;
 
-                ASTNode CurrentSymbol = bm->CreateSymbol(oss.str().c_str());
-                CurrentSymbol.SetValueWidth(this->GetValueWidth());
-                CurrentSymbol.SetIndexWidth(this->GetIndexWidth());
+                ASTNode CurrentSymbol = bm->CreateSymbol(oss.str().c_str(),this->GetIndexWidth(),this->GetValueWidth());
                 /* If for some reason the variable being created here is
                  * already declared by the user then the printed output will
                  * not be a legal input to the system. too bad. I refuse to

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index e5f26018f2fe0d2ce85d3093bf116977fbf91b22..6b85311b9d33e8ad6cc30bd16c3bda23b3bc3b1c 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -418,7 +418,7 @@ namespace BEEV
                  els = TransformTerm(els);
                  result = simp->CreateSimplifiedTermITE(cond, thn, els);
           }
-          result.SetIndexWidth(term.GetIndexWidth());
+          assert(result.GetIndexWidth() ==term.GetIndexWidth());
           break;
         }
       default:
@@ -437,8 +437,7 @@ namespace BEEV
 
           if (c!=o)
           {
-                 result = nf->CreateTerm(k, width, o);
-                         result.SetIndexWidth(indexwidth);
+                 result = nf->CreateArrayTerm(k,indexwidth, width, o);
           }
           else
                  result = term;

diff --git a/src/AST/NodeFactory/HashingNodeFactory.h b/src/AST/NodeFactory/HashingNodeFactory.h
index 809826c3d78345064e154449bcc91725db870791..ce1d92b2520a8f23ded98621f47376c22b6867bf 100644 (file)
--- a/src/AST/NodeFactory/HashingNodeFactory.h
+++ b/src/AST/NodeFactory/HashingNodeFactory.h
@@ -11,10 +11,9 @@ namespace BEEV
 
 class HashingNodeFactory : public NodeFactory
 {
-       BEEV::STPMgr& bm;
 public:
        HashingNodeFactory(BEEV::STPMgr& bm_)
-       : bm(bm_)
+       :NodeFactory(bm_)
        {
        }
 

diff --git a/src/AST/NodeFactory/NodeFactory.cpp b/src/AST/NodeFactory/NodeFactory.cpp
index 756191a640e696581c8e69fea0ec104ed58f81eb..ff7af9b2acef160da7258fa5c8a99bd103b161e3 100644 (file)
--- a/src/AST/NodeFactory/NodeFactory.cpp
+++ b/src/AST/NodeFactory/NodeFactory.cpp
@@ -1,5 +1,6 @@
 #include "ASTKind.h"
 #include "AST.h"
+#include "../../STPManager/STPManager.h"
 
 NodeFactory::~NodeFactory()
 {
@@ -103,3 +104,11 @@ BEEV::ASTNode NodeFactory::CreateArrayTerm(Kind kind, unsigned int index,
        return result;
 }
 
+
+ASTNode NodeFactory::CreateSymbol(const char * const name, unsigned indexWidth, unsigned valueWidth)
+{
+  ASTNode n = bm.LookupOrCreateSymbol(name);
+  n.SetIndexWidth(indexWidth);
+  n.SetValueWidth(valueWidth);
+  return n;
+}

diff --git a/src/AST/NodeFactory/NodeFactory.h b/src/AST/NodeFactory/NodeFactory.h
index 1317ad9b0051a9f4d9f1abf9d41cf0479d7d4cfc..e09934d4e85163d395413e282a91caa08e602774 100644 (file)
--- a/src/AST/NodeFactory/NodeFactory.h
+++ b/src/AST/NodeFactory/NodeFactory.h
@@ -10,6 +10,7 @@ namespace BEEV
 class ASTNode;
 typedef std::vector<ASTNode> ASTVec;
 extern ASTVec _empty_ASTVec;
+class STPMgr;
 }
 
 using BEEV::ASTNode;
@@ -19,7 +20,12 @@ using BEEV::_empty_ASTVec;
 
 class NodeFactory
 {
+protected:
+        BEEV::STPMgr& bm;
+
 public:
+        NodeFactory(BEEV::STPMgr& bm_) : bm(bm_){}
+
        virtual ~NodeFactory();
 
        virtual BEEV::ASTNode CreateTerm(Kind kind, unsigned int width,
@@ -31,6 +37,7 @@ public:
        virtual BEEV::ASTNode CreateNode(Kind kind,
                        const BEEV::ASTVec& children) =0;
 
+       ASTNode CreateSymbol(const char * const name, unsigned indexWidth, unsigned valueWidth);
 
        ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0,
                        const ASTVec &children = _empty_ASTVec);

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.h b/src/AST/NodeFactory/SimplifyingNodeFactory.h
index c5ce410410708954c3fd0ed74f38ce31f19a752b..75ddeabd20fa1934bd6c966109c0659bb3aa1791 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.h
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.h
@@ -30,7 +30,6 @@ class SimplifyingNodeFactory: public NodeFactory
 
 private:
        NodeFactory& hashing;
-       BEEV::STPMgr& bm; // Only here until the const evaluator is pulled out.
 
        const ASTNode& ASTTrue;
        const ASTNode& ASTFalse;
@@ -57,7 +56,7 @@ public:
 
 
        SimplifyingNodeFactory(NodeFactory& raw_, BEEV::STPMgr& bm_)
-       :hashing(raw_), bm(bm_), ASTTrue(bm.ASTTrue), ASTFalse(bm.ASTFalse), ASTUndefined(bm.ASTUndefined)
+       :hashing(raw_), NodeFactory(bm_), ASTTrue(bm_.ASTTrue), ASTFalse(bm_.ASTFalse), ASTUndefined(bm_.ASTUndefined)
        {
        }
        ;

diff --git a/src/AST/NodeFactory/TypeChecker.h b/src/AST/NodeFactory/TypeChecker.h
index dd2376266490f053c1d2d1577e6dd2d9c0fbe202..840bf179355ea5055adb645b295d8af921688fa8 100644 (file)
--- a/src/AST/NodeFactory/TypeChecker.h
+++ b/src/AST/NodeFactory/TypeChecker.h
@@ -17,10 +17,9 @@ using BEEV::STPMgr;
 class TypeChecker : public NodeFactory
 {
 NodeFactory& f;
-STPMgr& bm;
 
 public:
-       TypeChecker(NodeFactory& f_, STPMgr& bm_) : f(f_), bm(bm_)
+       TypeChecker(NodeFactory& f_, STPMgr& bm_) : f(f_), NodeFactory(bm)
        {}
 
        BEEV::ASTNode CreateTerm(BEEV::Kind kind, unsigned int width, const BEEV::ASTVec &children);

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 207e9e93c57765a12772d1b0a354bbc590a60f1c..dd1106425d84168f7254527e92691eaa08cf5a51 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -89,11 +89,11 @@ namespace BEEV
   ////////////////////////////////////////////////////////////////
   // STPMgr member functions to create ASTSymbol and ASTBVConst
   ////////////////////////////////////////////////////////////////
-  ASTNode STPMgr::CreateSymbol(const char * const name)
+  ASTNode STPMgr::LookupOrCreateSymbol(const char * const name)
   {
-    ASTSymbol temp_sym(name);    
+    ASTSymbol temp_sym(name);
     ASTNode n(LookupOrCreateSymbol(temp_sym));
-    return n;
+   return n;
   }
 
   // FIXME: _name is now a constant field, and this assigns to it
@@ -666,10 +666,8 @@ namespace BEEV
     std::string ccc(d);
     c += "_solver_" + ccc;
 
-    ASTNode CurrentSymbol = CreateSymbol(c.c_str());
+    ASTNode CurrentSymbol = CreateSymbol(c.c_str(),0,n);
     assert(0 !=n);
-    CurrentSymbol.SetValueWidth(n);
-    CurrentSymbol.SetIndexWidth(0);
     return CurrentSymbol;
   } //end of NewVar()
 
@@ -733,9 +731,7 @@ namespace BEEV
     str += "(";
     str += outNum.str();
     str += ")";
-    ASTNode CurrentSymbol = CreateSymbol(str.c_str());
-    CurrentSymbol.SetValueWidth(0);
-    CurrentSymbol.SetIndexWidth(0);
+    ASTNode CurrentSymbol = CreateSymbol(str.c_str(),0,0);
     return CurrentSymbol;
   } // End of NewParameterized_BooleanVar()
 

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index c7dc7ec83ebc0497ca949569acf16993c484d95e..7bb477025459c5114c760072b0954214bce1bafb 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -256,7 +256,7 @@ namespace BEEV
      ****************************************************************/
 
     // Create and return an ASTNode for a symbol
-    ASTNode CreateSymbol(const char * const name);
+    ASTNode LookupOrCreateSymbol(const char * const name);
 
     // Create and return an ASTNode for a symbol Width is number of
     // bits.
@@ -273,6 +273,12 @@ namespace BEEV
      * Create Node functions                                        *
      ****************************************************************/
 
+    inline ASTNode CreateSymbol(const char * const name, unsigned indexWidth, unsigned valueWidth)
+    {
+      return defaultNodeFactory->CreateSymbol(name,indexWidth,valueWidth);
+    }
+
+
     // Create and return an interior ASTNode
     inline BEEV::ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children = _empty_ASTVec)
     {
@@ -305,6 +311,11 @@ namespace BEEV
         return defaultNodeFactory->CreateTerm(kind,width,children);
      }
 
+     inline BEEV::ASTNode CreateArrayTerm(BEEV::Kind kind, unsigned int indexWidth, unsigned int width, const BEEV::ASTVec &children =_empty_ASTVec)
+     {
+         return defaultNodeFactory->CreateArrayTerm(kind,indexWidth, width,children);
+     }
+
      inline ASTNode CreateTerm(Kind kind, unsigned int width,
                const ASTNode& child0, const ASTVec &children = _empty_ASTVec) {
        return defaultNodeFactory->CreateTerm(kind, width, child0, children);
@@ -382,10 +393,7 @@ namespace BEEV
         char d[32 + prefix.length()];
         sprintf(d, "%s_%d", prefix.c_str(), _symbol_count++);
 
-        BEEV::ASTNode CurrentSymbol = CreateSymbol(d);
-        CurrentSymbol.SetValueWidth(valueWidth);
-        CurrentSymbol.SetIndexWidth(indexWidth);
-
+        BEEV::ASTNode CurrentSymbol = CreateSymbol(d,indexWidth,valueWidth);
         return CurrentSymbol;
     }
 

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 577f43a0dc8d40e16deb3db4235846628b367f1d..d0569b82873b257110a0aa0131629b06c1a1e650 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -668,9 +668,7 @@ Expr vc_varExpr1(VC vc, const char* name,
                  int indexwidth, int valuewidth) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
 
-  node o = b->CreateSymbol(name);
-  o.SetIndexWidth(indexwidth);
-  o.SetValueWidth(valuewidth);
+  node o = b->CreateSymbol(name,indexwidth,valuewidth);
 
   nodestar output = new node(o);
   ////if(cinterface_exprdelete_on) created_exprs.push_back(output);
@@ -685,24 +683,29 @@ Expr vc_varExpr(VC vc, const char * name, Type type) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar a = (nodestar)type;
 
-  node o = b->CreateSymbol(name);
+  unsigned indexWidth;
+  unsigned valueWidth;
+
   switch(a->GetKind()) {
   case BEEV::BITVECTOR:
-    o.SetIndexWidth(0);
-    o.SetValueWidth((*a)[0].GetUnsignedConst());
+    indexWidth = 0;
+    valueWidth = (*a)[0].GetUnsignedConst();
     break;
   case BEEV::ARRAY:
-    o.SetIndexWidth((*a)[0].GetUnsignedConst());
-    o.SetValueWidth((*a)[1].GetUnsignedConst());
+    indexWidth = (*a)[0].GetUnsignedConst();
+    valueWidth = (*a)[1].GetUnsignedConst();
     break;
   case BEEV::BOOLEAN:
-    o.SetIndexWidth(0);
-    o.SetValueWidth(0);
+    indexWidth = 0;
+    valueWidth = 0;
     break;
   default:
     BEEV::FatalError("CInterface: vc_varExpr: Unsupported type",*a);
     break;
+
   }
+  node o = b->CreateSymbol(name,indexWidth,valueWidth);
+
   nodestar output = new node(o);
   ////if(cinterface_exprdelete_on) created_exprs.push_back(output);
   BVTypeCheck(*output);

diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex
index deb231cdb31f8017f084136091e68d4ab19a54c2..fc26be2520111e61f366bd84541c903ba712ecf6 100644 (file)
--- a/src/parser/CVC.lex
+++ b/src/parser/CVC.lex
@@ -122,7 +122,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 "POP"            { return POP_TOK;}
 
 (({LETTER})|(_)({ANYTHING}))({ANYTHING})*      {
-  BEEV::ASTNode nptr = (BEEV::ParserBM)->CreateSymbol(yytext); 
+  BEEV::ASTNode nptr = parserInterface->LookupOrCreateSymbol(yytext); 
 
   // Check valuesize to see if it's a prop var.  I don't like doing
   // type determination in the lexer, but it's easier than rewriting

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index c5dedc0d3d4254a7889ea6e01e4728f341353ba4..1d20fcdaa39d703b0b34b091a59d97e4b0d95fe9 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -659,14 +659,14 @@ Formula         :     '(' Formula ')'
 |      TRUELIT_TOK 
 {
   $$ = new ASTNode(parserInterface->CreateNode(TRUE)); 
-  $$->SetIndexWidth(0); 
-  $$->SetValueWidth(0);
+  assert($$->GetIndexWidth() == 0);
+  assert($$->GetValueWidth() == 0);
 }
 |      FALSELIT_TOK 
 { 
   $$ = new ASTNode(parserInterface->CreateNode(FALSE)); 
-  $$->SetIndexWidth(0); 
-  $$->SetValueWidth(0);
+  assert($$->GetIndexWidth() == 0);
+  assert($$->GetValueWidth() == 0);
 }
 
 |      LET_TOK LetDecls IN_TOK Formula

diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h
index b14be075eabc22d33d28f0fe62c61c68034a792c..89569d865cb9858573c25434c48c502bad4b2383 100644 (file)
--- a/src/parser/ParserInterface.h
+++ b/src/parser/ParserInterface.h
@@ -87,9 +87,9 @@ public:
        return bm.CreateBVConst(width, bvconst);
     }
 
-    ASTNode CreateSymbol(const char * const name)
+    ASTNode LookupOrCreateSymbol(const char * const name)
     {
-       return bm.CreateSymbol(name);
+       return bm.LookupOrCreateSymbol(name);
     }
 };
 }

diff --git a/src/parser/smtlib.lex b/src/parser/smtlib.lex
index 40362b7ce220672921db8d8df85f4b84f688a969..4326f4459bb93bd6bf396698f42a9383bd82a9e6 100644 (file)
--- a/src/parser/smtlib.lex
+++ b/src/parser/smtlib.lex
@@ -220,7 +220,7 @@ bit{DIGIT}+     {
 "boolbv"        { return BOOL_TO_BV_TOK;}
 
 (({LETTER})|(_)({ANYTHING}))({ANYTHING})*      {
-  BEEV::ASTNode nptr = parserInterface->CreateSymbol(smttext); 
+  BEEV::ASTNode nptr = parserInterface->LookupOrCreateSymbol(smttext); 
 
   // Check valuesize to see if it's a prop var.  I don't like doing
   // type determination in the lexer, but it's easier than rewriting

diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex
index 1c821b035c62deef70b9271afc1fbc2cbeb4537f..edeae9cb956f9ff7c07d5b3d19a7b97d63da1247 100644 (file)
--- a/src/parser/smtlib2.lex
+++ b/src/parser/smtlib2.lex
@@ -68,7 +68,7 @@
     if (s[0] == '|' && s[str.size()-1] == '|')
        str = str.substr(1,str.length()-2);
     
-    BEEV::ASTNode nptr = BEEV::parserInterface->CreateSymbol(str.c_str()); 
+    BEEV::ASTNode nptr = BEEV::parserInterface->LookupOrCreateSymbol(str.c_str()); 
 
   // Check valuesize to see if it's a prop var.  I don't like doing
   // type determination in the lexer, but it's easier than rewriting

diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index 18ccb2734dd72245a390e5bf99c8d7f2fcc295bf..5932df347971118a5a42b2e56da71355d9f06810 100644 (file)
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -151,9 +151,7 @@ static string tolower(const char * name)
                                        oss << "?let_k_" << sz;
 
                                        ASTNode CurrentSymbol = n.GetSTPMgr()->CreateSymbol(
-                                                       oss.str().c_str());
-                                       CurrentSymbol.SetValueWidth(n.GetValueWidth());
-                                       CurrentSymbol.SetIndexWidth(n.GetIndexWidth());
+                                                       oss.str().c_str(),n.GetIndexWidth(), n.GetValueWidth());
                                        /* If for some reason the variable being created here is
                                         * already declared by the user then the printed output will
                                         * not be a legal input to the system. too bad. I refuse to

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 7cda322328b9b07e93577a6a556bd0f92420e60b..1f24bf753b19bbd9fcbf7432db80cd63193109e4 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -215,7 +215,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
                if (n.GetIndexWidth() != 0)
                {
                        const ASTNode& r = it->second;
-                       r.SetIndexWidth(n.GetIndexWidth());
+                       assert(r.GetIndexWidth() == n.GetIndexWidth());
                        assert(BVTypeCheck(r));
                        ASTNode replaced = replace(r, fromTo, cache,nf);
                        if (replaced != r)
@@ -264,10 +264,10 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
                        // If the index and value width aren't saved, they are reset sometimes (??)
                        const unsigned int indexWidth = n.GetIndexWidth();
                        const unsigned int valueWidth = n.GetValueWidth();
-                       result = nf->CreateTerm(n.GetKind(), n.GetValueWidth(),
+                       result = nf->CreateArrayTerm(n.GetKind(),indexWidth, n.GetValueWidth(),
                                        children);
-                       result.SetValueWidth(valueWidth);
-                       result.SetIndexWidth(indexWidth);
+                       assert(result.GetValueWidth() == valueWidth);
+
                }
                else
                        result = n;

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index dab3a50a24040117062ef50968486c36f48058c3..26bb1ee693d64cd4820e41476c743662295cf629 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -966,6 +966,7 @@ namespace BEEV
     return nf->CreateNode(EQ, in1, in2);
   }
 
+  // nb. this is sometimes used to build array terms.
   //accepts cond == t1, then part is t2, and else part is t3
   ASTNode Simplifier::CreateSimplifiedTermITE(const ASTNode& in0, 
                                               const ASTNode& in1, 
@@ -989,7 +990,7 @@ namespace BEEV
             FatalError("CreateSimplifiedTermITE: "\
                        "the lengths of the two branches don't match", t1);
           }
-        return nf->CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2);
+        return nf->CreateArrayTerm(ITE, t1.GetIndexWidth(),t1.GetValueWidth(), t0, t1, t2);
       }
 
     if (t0 == ASTTrue)
@@ -1009,7 +1010,7 @@ namespace BEEV
         return t2;
       }
 
-    return nf->CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2);
+    return nf->CreateArrayTerm(ITE, t1.GetIndexWidth(),t1.GetValueWidth(), t0, t1, t2);
   }
 
   ASTNode 
@@ -1690,8 +1691,7 @@ namespace BEEV
                        assert(v.size() > 0);
                        if (v != actualInputterm.GetChildren()) // short-cut.
                        {
-                               output = nf->CreateTerm(k, inputValueWidth, v);
-                               output.SetIndexWidth(actualInputterm.GetIndexWidth());
+                               output = nf->CreateArrayTerm(k,actualInputterm.GetIndexWidth(), inputValueWidth, v);
                        }
                        else
                                output = actualInputterm;
@@ -3321,7 +3321,7 @@ namespace BEEV
                                SimplifyFormula(term[0],VarConstMap),
                                SimplifyArrayTerm(term[1], VarConstMap),
                                SimplifyArrayTerm(term[2], VarConstMap));
-               output.SetIndexWidth(iw);
+               assert(output.GetIndexWidth() == iw);
        }
                break;
        case WRITE: {
@@ -3330,8 +3330,7 @@ namespace BEEV
                ASTNode idx = SimplifyTerm(term[1]);
                ASTNode val = SimplifyTerm(term[2]);
 
-               output = nf->CreateTerm(WRITE, term.GetValueWidth(), array, idx, val);
-               output.SetIndexWidth(iw); // save the value and set, otherwise it sometimes fails.
+               output = nf->CreateArrayTerm(WRITE,iw, term.GetValueWidth(), array, idx, val);
        }
 
                break;

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 9f87cbf9f7cb9abdca20789de10723bfcec246d4..d3e31412e9235e175785db03a7390c0a8c39b785 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -561,15 +561,9 @@ namespace BEEV
     
     ostringstream oss;
     oss << "cnf" << "{" << varphi.GetNodeNum() << "}";
-    psi = bm->CreateSymbol(oss.str().c_str());
-    
-    //########################################
-    // step 2, set widths appropriately
-    //########################################
-    
-    psi.SetValueWidth(varphi.GetValueWidth());
-    psi.SetIndexWidth(varphi.GetIndexWidth());
+    psi = bm->CreateSymbol(oss.str().c_str(),varphi.GetIndexWidth(),varphi.GetValueWidth());
     
+
     //########################################
     // step 3, recurse over children
     //########################################
@@ -609,7 +603,7 @@ namespace BEEV
     
     ostringstream oss;
     oss << "cnf" << "{" << varphi.GetNodeNum() << "}";
-    ASTNode psi = bm->CreateSymbol(oss.str().c_str());
+    ASTNode psi = bm->CreateSymbol(oss.str().c_str(),0,0);
     
     //########################################
     // step 2, add defs
@@ -640,7 +634,7 @@ namespace BEEV
     
     ostringstream oss;
     oss << "cnf" << "{" << varphi.GetNodeNum() << "}";
-    ASTNode psi = bm->CreateSymbol(oss.str().c_str());
+    ASTNode psi = bm->CreateSymbol(oss.str().c_str(),0,0);
     
     //########################################
     // step 2, add defs
@@ -707,7 +701,7 @@ namespace BEEV
     
     ostringstream oss;
     oss << "cnf" << "{" << varphi.GetNodeNum() << "}";
-    ASTNode psi = bm->CreateSymbol(oss.str().c_str());
+    ASTNode psi = bm->CreateSymbol(oss.str().c_str(),0,0);
     
     //########################################
     // step 3, add defs
@@ -918,14 +912,14 @@ namespace BEEV
                                            ClauseList* defs)
   {
     ASTNode dummy_false_var = 
-      bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
+      bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*",0,0));
     info[varphi]->clausespos = SINGLETON(dummy_false_var);
   } //End of convertFormulaToCNFPosFALSE()
 
   void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, 
                                           ClauseList* defs)
   {
-    ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
+    ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*",0,0);
     info[varphi]->clausespos = SINGLETON(dummy_true_var);
   } //End of convertFormulaToCNFPosTRUE
 
@@ -1292,7 +1286,7 @@ namespace BEEV
   void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, 
                                            ClauseList* defs)
   {
-    ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
+    ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*",0,0);
     info[varphi]->clausesneg = SINGLETON(dummy_true_var);
   } //End of convertFormulaToCNFNegFALSE()
 
@@ -1300,7 +1294,7 @@ namespace BEEV
                                           ClauseList* defs)
   {
     ASTNode dummy_false_var = 
-      bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
+      bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*",0,0));
     info[varphi]->clausesneg = SINGLETON(dummy_false_var);
   } //End of convertFormulaToCNFNegTRUE()
 
@@ -1773,7 +1767,7 @@ namespace BEEV
   {
     bm->GetRunTimes()->start(RunTimes::CNFConversion);
     scanFormula(varphi, true, false);
-    ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
+    ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*",0,0);
     ClauseList* defs = SINGLETON(dummy_true_var);
     convertFormulaToCNF(varphi, defs);
     ClauseList* top = info[varphi]->clausespos;