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   bool d_calledFromParser;
00047 
00048   //! Print the symbols in e, cache results
00049   void printSymbols(Expr e, ExprMap<bool>& cache);
00050   //! Take a parsed Expr and evaluate it
00051   bool evaluateCommand(const Expr& e);
00052   // Fetch the next command and evaluate it.  Return true if
00053   // evaluation was successful, false otherwise.  In especially bad
00054   // cases an exception may be thrown.
00055   bool evaluateNext();
00056   void findAxioms(const Expr& e, ExprMap<bool>& skolemAxioms,
00057       ExprMap<bool>& visited);
00058   Expr skolemizeAx(const Expr& e);
00059   void reportResult(QueryResult qres, bool checkingValidity = true);
00060   void printModel();
00061   void printCounterExample();
00062 
00063 public:
00064   VCCmd(ValidityChecker* vc, Parser* parser, bool calledFromParser=false);
00065   ~VCCmd();
00066 
00067   // Main loop function
00068   void processCommands();
00069 };
00070 
00071 }
00072 
00073 #endif

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