<commit_before>// -*- c++ -*-
/********************************************************************
 * AUTHORS: <NAME>
 *
 * BEGIN DATE: November, 2005
 *
 * LICENSE: Please view LICENSE file in the home dir of this Program
 ********************************************************************/

#ifndef TRANSFORM_H
#define TRANSFORM_H

#include "AST.h"
#include "../STPManager/STPManager.h"


namespace BEEV
{
  class Simplifier;

  class ArrayTransformer 
  {
  public:

      // These map from array and index to ITE and Symbol.
      struct ArrayRead
      {
        ArrayRead(ASTNode _ite, ASTNode _symbol)
        {
          assert(! _symbol.IsNull());
          assert(_ite.GetValueWidth() == _symbol.GetValueWidth());
          assert ((SYMBOL == _symbol.GetKind() || BVCONST == _symbol.GetKind()));

          ite = _ite;
          symbol = _symbol;
        }

        ASTNode ite;  // if not using refinement this will be the ITE for the read. Otherwise == symbol.
        ASTNode symbol; // each read is allocated a distinct fresh variable.
      };

      // MAP: This maps from arrays to their indexes.
      // This map is used by the TransformArray()
      // function ,as well as the counter example, and refinement.
      // This map is useful in converting array reads into
      // nested ITE constructs. Suppose there are two array reads in the
      // input Read(A,i) and Read(A,j). Then Read(A,i) is replaced with
      // a symbolic constant, say v1, and Read(A,j) is replaced with the
      // following ITE: ITE(i=j,v1,v2)

      typedef map<ASTNode, ArrayRead> arrTypeMap;
      typedef map<ASTNode, arrTypeMap > ArrType ;
      ArrType arrayToIndexToRead;

  private:

    /****************************************************************
     * Private Typedefs and Data                                    *
     ****************************************************************/
    
    // Handy defs
    ASTNode ASTTrue, ASTFalse, ASTUndefined;

        
    // Memo table used by the transformer while it is transforming the
    // formulas and terms
    ASTNodeMap* TransformMap;
    
    // Flag for debuggin the transformer
    const bool debug_transform;

    // Ptr to an external simplifier
    Simplifier * simp;

    // Ptr to STPManager
    STPMgr * bm;
    
    // Ptr to class that records the runtimes for various parts of the
    // code
    RunTimes * runTimes;

    NodeFactory *nf;

    /****************************************************************
     * Private Member Functions                                     *
     ****************************************************************/
    
    ASTNode TranslateSignedDivModRem(const ASTNode& in);
    ASTNode TransformTerm(const ASTNode& inputterm);
    void assertTransformPostConditions(const ASTNode & term, ASTNodeSet& visited);

    ASTNode TransformArrayRead(const ASTNode& term);

    ASTNode TransformFormula(const ASTNode& form);

  public:

    //fill the arrayname_readindices vector if e0 is a READ(Arr,index)
    //and index is a BVCONST
    void FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1);


    /****************************************************************
     * Public Member Functions                                      *
     ****************************************************************/      
    
    // Constructor
    ArrayTransformer(STPMgr * bm, Simplifier* s) : 
      bm(bm), 
      simp(s), 
      debug_transform(0),
      TransformMap(NULL)
    {
      nf = bm->defaultNodeFactory;

      runTimes = bm->GetRunTimes();
      ASTTrue  = bm->CreateNode(TRUE);
      ASTFalse = bm->CreateNode(FALSE);
      ASTUndefined = bm->CreateNode(UNDEFINED);
    }

    // Takes a formula, transforms it by replacing array reads with
    // variables, and returns the transformed formula
    ASTNode TransformFormula_TopLevel(const ASTNode& form);

    void ClearAllTables(void)
    {
      arrayToIndexToRead.clear();
    }
  }; //end of class Transformer

};//end of namespace
#endif<commit_msg>Improvement. Use the simplifying node factory in transformer.<commit_after>// -*- c++ -*-
/********************************************************************
 * AUTHORS: <NAME>
 *
 * BEGIN DATE: November, 2005
 *
 * LICENSE: Please view LICENSE file in the home dir of this Program
 ********************************************************************/

#ifndef TRANSFORM_H
#define TRANSFORM_H

#include "AST.h"
#include "../STPManager/STPManager.h"
#include "../AST/NodeFactory/SimplifyingNodeFactory.h"

namespace BEEV
{
  class Simplifier;

  class ArrayTransformer 
  {
  public:

      // These map from array and index to ITE and Symbol.
      struct ArrayRead
      {
        ArrayRead(ASTNode _ite, ASTNode _symbol)
        {
          assert(! _symbol.IsNull());
          assert(_ite.GetValueWidth() == _symbol.GetValueWidth());
          assert ((SYMBOL == _symbol.GetKind() || BVCONST == _symbol.GetKind()));

          ite = _ite;
          symbol = _symbol;
        }

        ASTNode ite;  // if not using refinement this will be the ITE for the read. Otherwise == symbol.
        ASTNode symbol; // each read is allocated a distinct fresh variable.
      };

      // MAP: This maps from arrays to their indexes.
      // This map is used by the TransformArray()
      // function ,as well as the counter example, and refinement.
      // This map is useful in converting array reads into
      // nested ITE constructs. Suppose there are two array reads in the
      // input Read(A,i) and Read(A,j). Then Read(A,i) is replaced with
      // a symbolic constant, say v1, and Read(A,j) is replaced with the
      // following ITE: ITE(i=j,v1,v2)

      typedef map<ASTNode, ArrayRead> arrTypeMap;
      typedef map<ASTNode, arrTypeMap > ArrType ;
      ArrType arrayToIndexToRead;

  private:

    /****************************************************************
     * Private Typedefs and Data                                    *
     ****************************************************************/
    
    // Handy defs
    ASTNode ASTTrue, ASTFalse, ASTUndefined;

        
    // Memo table used by the transformer while it is transforming the
    // formulas and terms
    ASTNodeMap* TransformMap;
    
    // Flag for debuggin the transformer
    const bool debug_transform;

    // Ptr to an external simplifier
    Simplifier * simp;

    // Ptr to STPManager
    STPMgr * bm;
    
    // Ptr to class that records the runtimes for various parts of the
    // code
    RunTimes * runTimes;

    NodeFactory *nf;

    /****************************************************************
     * Private Member Functions                                     *
     ****************************************************************/
    
    ASTNode TranslateSignedDivModRem(const ASTNode& in);
    ASTNode TransformTerm(const ASTNode& inputterm);
    void assertTransformPostConditions(const ASTNode & term, ASTNodeSet& visited);

    ASTNode TransformArrayRead(const ASTNode& term);

    ASTNode TransformFormula(const ASTNode& form);

  public:

    //fill the arrayname_readindices vector if e0 is a READ(Arr,index)
    //and index is a BVCONST
    void FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1);


    /****************************************************************
     * Public Member Functions                                      *
     ****************************************************************/      
    
    // Constructor
    ArrayTransformer(STPMgr * bm, Simplifier* s) : 
      bm(bm), 
      simp(s), 
      debug_transform(0),
      TransformMap(NULL)
    {
      nf = new SimplifyingNodeFactory(*(bm->hashingNodeFactory), *bm);

      runTimes = bm->GetRunTimes();
      ASTTrue  = bm->CreateNode(TRUE);
      ASTFalse = bm->CreateNode(FALSE);
      ASTUndefined = bm->CreateNode(UNDEFINED);
    }

    ~ArrayTransformer()
    {
      delete nf;
    }

    // Takes a formula, transforms it by replacing array reads with
    // variables, and returns the transformed formula
    ASTNode TransformFormula_TopLevel(const ASTNode& form);

    void ClearAllTables(void)
    {
      arrayToIndexToRead.clear();
    }
  }; //end of class Transformer

};//end of namespace
#endif
{'fraction_non_alphanumeric': 0.20400289365806606, 'fraction_numerical': 0.002652519893899204, 'mean_word_length': 2.6654882898806895, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '893914', 'n_tokens_mistral': 2330, 'n_tokens_neox': 2104, 'n_words': 675}