/usr/include/cvc3/search_simple.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 74 75 76 77 78 79 80 81 82 | /*****************************************************************************/
/*!
* \file search_simple.h
*
* Author: Clark Barrett
*
* Created: Sat Mar 29 21:53:46 2003
*
* <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__include__search_simple_h_
#define _cvc3__include__search_simple_h_
#include "search_impl_base.h"
#include "statistics.h"
namespace CVC3 {
class DecisionEngine;
/*!
* \defgroup SE_Simple Simple Search Engine
* \ingroup SE
*
* This module includes all the components of a very simplistic search
* engine. It is used mainly for debugging purposes.
*/
//! Implementation of the simple search engine
/*! \ingroup SE_Simple */
class SearchSimple: public SearchImplBase {
/*! \addtogroup SE_Simple
* @{
*/
//! Name
std::string d_name;
//! Decision Engine
DecisionEngine* d_decisionEngine;
//! Formula being checked
CDO<Theorem> d_goal;
//! Non-literals generated by DP's
CDO<Theorem> d_nonLiterals;
//! Theorem which records simplification of the last query
CDO<Theorem> d_simplifiedThm;
//! Recursive DPLL algorithm used by checkValid
QueryResult checkValidRec(Theorem& thm);
//! Private helper function for checkValid and restart
QueryResult checkValidMain(const Expr& e2);
public:
//! Constructor
SearchSimple(TheoryCore* core);
//! Destructor
~SearchSimple();
// Implementation of virtual SearchEngine methods
const std::string& getName() { return d_name; }
QueryResult checkValidInternal(const Expr& e);
QueryResult restartInternal(const Expr& e);
void addLiteralFact(const Theorem& thm) {}
void addNonLiteralFact(const Theorem& thm);
/*! @} */ // end addtogroup SE_Simple
};
}
#endif
|