theorem_manager.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theorem_manager.cpp
 * 
 * Author: Sergey Berezin
 * 
 * Created: Feb 11 02:39:35 GMT 2003
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/
// File: theorem_manager.cpp
//
// AUTHOR: Sergey Berezin, 07/05/02
//
// Defines some functions for class TheoremManager.  They are not
// inlined becaule they use ExprManager (expr_manager.h), which
// includes theorem_manager.h.
// 
///////////////////////////////////////////////////////////////////////////////


#include "theorem_value.h"
#include "memory_manager_chunks.h"
#include "memory_manager_malloc.h"
#include "command_line_flags.h"
#include "common_proof_rules.h"


using namespace std;
using namespace CVCL;


// ExprManager is not initialized in vcl yet when we are created; we
// use d_em as our local cache to fetch the EM when our getEM() is
// first called.

TheoremManager::TheoremManager(ContextManager* cm,
                               ExprManager* em,
                               const CLFlags& flags)
  : d_cm(cm), d_em(em), d_flags(flags),
    d_withProof(flags["proofs"].getBool()),
    d_withAssump(flags["assump"].getBool()), d_flag(1),
    d_active(true)
{
  d_em->newKind(PF_APPLY, "|-");
  d_em->newKind(PF_HOLE, "**");
  DebugAssert(!d_withProof || d_withAssump, 
              "TheoremManager(): proofs without assumptions are not allowed");
  if (flags["mm"].getString() == "chunks") {
    d_mm = new MemoryManagerChunks(sizeof(TheoremValue));
    d_rwmm = new MemoryManagerChunks(sizeof(RWTheoremValue));
    d_reflmm = new MemoryManagerChunks(sizeof(ReflexivityTheoremValue));
  } else {
    d_mm = new MemoryManagerMalloc();
    d_rwmm = new MemoryManagerMalloc();
    d_reflmm = new MemoryManagerMalloc();
  }
  d_rules = createProofRules();
}


TheoremManager::~TheoremManager()
{
  delete d_mm;
  delete d_rwmm;
  delete d_reflmm;
}


void TheoremManager::clear() {
  delete d_rules;
  d_active=false;
}

---