CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
search_simple.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file search_simple.h
4
*
5
* Author: Clark Barrett
6
*
7
* Created: Sat Mar 29 21:53:46 2003
8
*
9
* <hr>
10
*
11
* License to use, copy, modify, sell and/or distribute this software
12
* and its documentation for any purpose is hereby granted without
13
* royalty, subject to the terms and conditions defined in the \ref
14
* LICENSE file provided with this distribution.
15
*
16
* <hr>
17
*
18
*/
19
/*****************************************************************************/
20
21
#ifndef _cvc3__include__search_simple_h_
22
#define _cvc3__include__search_simple_h_
23
24
#include "
search_impl_base.h
"
25
#include "
statistics.h
"
26
27
namespace
CVC3 {
28
29
class
DecisionEngine;
30
31
/*!
32
* \defgroup SE_Simple Simple Search Engine
33
* \ingroup SE
34
*
35
* This module includes all the components of a very simplistic search
36
* engine. It is used mainly for debugging purposes.
37
*/
38
39
//! Implementation of the simple search engine
40
/*! \ingroup SE_Simple */
41
class
SearchSimple
:
public
SearchImplBase
{
42
/*! \addtogroup SE_Simple
43
* @{
44
*/
45
46
//! Name
47
std::string
d_name
;
48
49
//! Decision Engine
50
DecisionEngine
*
d_decisionEngine
;
51
52
//! Formula being checked
53
CDO<Theorem>
d_goal
;
54
//! Non-literals generated by DP's
55
CDO<Theorem>
d_nonLiterals
;
56
//! Theorem which records simplification of the last query
57
CDO<Theorem>
d_simplifiedThm
;
58
59
//! Recursive DPLL algorithm used by checkValid
60
QueryResult
checkValidRec
(
Theorem
& thm);
61
//! Private helper function for checkValid and restart
62
QueryResult
checkValidMain
(
const
Expr
& e2);
63
64
public
:
65
//! Constructor
66
SearchSimple
(
TheoryCore
* core);
67
//! Destructor
68
~SearchSimple
();
69
70
// Implementation of virtual SearchEngine methods
71
const
std::string&
getName
() {
return
d_name
; }
72
QueryResult
checkValidInternal
(
const
Expr
& e);
73
QueryResult
restartInternal
(
const
Expr
& e);
74
void
addLiteralFact
(
const
Theorem
& thm) {}
75
void
addNonLiteralFact
(
const
Theorem
& thm);
76
77
/*! @} */
// end addtogroup SE_Simple
78
};
79
80
}
81
82
#endif
Generated on Tue May 14 2013 09:02:08 for CVC3 by
1.8.3.1