/usr/include/cvc3/vc_cmd.h is in libcvc3-dev 2.4.1-5ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 | /*****************************************************************************/
/*!
* \file vc_cmd.h
*
* Author: Clark Barrett
*
* Created: Fri Dec 13 22:35:15 2002
*
* <hr>
*
* 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.
*
* <hr>
*
*/
/*****************************************************************************/
#ifndef _cvc3__vc_cvc__vc_cmd_h_
#define _cvc3__vc_cvc__vc_cmd_h_
#include <string>
#include "compat_hash_map.h"
#include "exception.h"
#include "queryresult.h"
namespace CVC3 {
class ValidityChecker;
class Parser;
class Context;
class Expr;
template<class Data>
class ExprMap;
class VCCmd {
ValidityChecker* d_vc;
Parser* d_parser;
// TODO: move state variables into validity checker.
typedef std::hash_map<const char*, Context*> CtxtMap;
std::string d_name_of_cur_ctxt;
CtxtMap d_map;
bool d_calledFromParser;
//! Print the symbols in e, cache results
void printSymbols(Expr e, ExprMap<bool>& cache);
//! Take a parsed Expr and evaluate it
bool evaluateCommand(const Expr& e);
// Fetch the next command and evaluate it. Return true if
// evaluation was successful, false otherwise. In especially bad
// cases an exception may be thrown.
bool evaluateNext();
void findAxioms(const Expr& e, ExprMap<bool>& skolemAxioms,
ExprMap<bool>& visited);
Expr skolemizeAx(const Expr& e);
void reportResult(QueryResult qres, bool checkingValidity = true);
void printModel();
void printCounterExample();
public:
VCCmd(ValidityChecker* vc, Parser* parser, bool calledFromParser=false);
~VCCmd();
// Main loop function
void processCommands();
};
}
#endif
|