theorem_manager.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theorem_manager.cpp
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Feb 11 02:39:35 GMT 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 // File: theorem_manager.cpp
00021 //
00022 // AUTHOR: Sergey Berezin, 07/05/02
00023 //
00024 // Defines some functions for class TheoremManager.  They are not
00025 // inlined becaule they use ExprManager (expr_manager.h), which
00026 // includes theorem_manager.h.
00027 // 
00028 ///////////////////////////////////////////////////////////////////////////////
00029 
00030 
00031 #include "theorem_value.h"
00032 #include "memory_manager_chunks.h"
00033 #include "memory_manager_malloc.h"
00034 #include "command_line_flags.h"
00035 #include "common_proof_rules.h"
00036 
00037 
00038 using namespace std;
00039 using namespace CVC3;
00040 
00041 
00042 // ExprManager is not initialized in vcl yet when we are created; we
00043 // use d_em as our local cache to fetch the EM when our getEM() is
00044 // first called.
00045 
00046 TheoremManager::TheoremManager(ContextManager* cm,
00047                                ExprManager* em,
00048                                const CLFlags& flags)
00049   : d_cm(cm), d_em(em), d_flags(flags),
00050     d_withProof(flags["proofs"].getBool()),
00051     d_withAssump(true), d_flag(1),
00052     d_active(true)
00053 {
00054   d_em->newKind(PF_APPLY, "|-");
00055   d_em->newKind(PF_HOLE, "**");
00056   DebugAssert(!d_withProof || d_withAssump, 
00057         "TheoremManager(): proofs without assumptions are not allowed");
00058   if (flags["mm"].getString() == "chunks") {
00059     d_mm = new MemoryManagerChunks(sizeof(RegTheoremValue));
00060     d_rwmm = new MemoryManagerChunks(sizeof(RWTheoremValue));
00061   } else {
00062     d_mm = new MemoryManagerMalloc();
00063     d_rwmm = new MemoryManagerMalloc();
00064   }
00065   d_rules = createProofRules();
00066 }
00067 
00068 
00069 TheoremManager::~TheoremManager()
00070 {
00071   delete d_mm;
00072   delete d_rwmm;
00073 }
00074 
00075 
00076 void TheoremManager::clear() {
00077   delete d_rules;
00078   d_active=false;
00079 }

Generated on Wed Nov 18 16:13:31 2009 for CVC3 by  doxygen 1.5.2