vc_cmd.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file vc_cmd.h
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Fri Dec 13 22:35:15 2002
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 
00021 #ifndef _cvc3__vc_cvc__vc_cmd_h_
00022 #define _cvc3__vc_cvc__vc_cmd_h_
00023 
00024 #include <string>
00025 #include "compat_hash_map.h"
00026 #include "exception.h"
00027 #include "queryresult.h"
00028 
00029 namespace CVC3 {
00030 
00031   class ValidityChecker;
00032   class Parser;
00033   class Context;  
00034   class Expr;
00035 
00036   template<class Data>
00037   class ExprMap;
00038 
00039 class VCCmd {
00040   ValidityChecker* d_vc;
00041   Parser* d_parser;
00042   // TODO: move state variables into validity checker.
00043   typedef std::hash_map<const char*, Context*> CtxtMap;
00044   std::string d_name_of_cur_ctxt;
00045   CtxtMap d_map;
00046 
00047   //! Take a parsed Expr and evaluate it
00048   bool evaluateCommand(const Expr& e);
00049   // Fetch the next command and evaluate it.  Return true if
00050   // evaluation was successful, false otherwise.  In especially bad
00051   // cases an exception may be thrown.
00052   bool evaluateNext();
00053   void findAxioms(const Expr& e, ExprMap<bool>& skolemAxioms,
00054       ExprMap<bool>& visited);
00055   Expr skolemizeAx(const Expr& e);
00056   void reportResult(QueryResult qres, bool checkingValidity = true);
00057 
00058 public:
00059   VCCmd(ValidityChecker* vc, Parser* parser);
00060   ~VCCmd();
00061 
00062   // Main loop function
00063   void processCommands();
00064 };
00065 
00066 }
00067 
00068 #endif

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1