CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
search.cpp
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file search.cpp
4
*
5
* Author: Clark Barrett, Vijay Ganesh (CNF Converter)
6
*
7
* Created: Fri Jan 17 14:19:54 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
22
#include "
search.h
"
23
#include "
search_rules.h
"
24
#include "
theory_core.h
"
25
#include "
eval_exception.h
"
26
#include "
theorem_manager.h
"
27
#include "
command_line_flags.h
"
28
29
30
using namespace
CVC3;
31
using namespace
std;
32
33
34
//! Constructor
35
SearchEngine::SearchEngine
(
TheoryCore
* core)
36
: d_core(core),
37
d_commonRules(core->getTM()->getRules())
38
{
39
40
const
CLFlags
& flg = (core->
getTM
()->
getFlags
());
41
if
(flg[
"lfsc-mode"
].getInt()!= 0){
42
d_rules
=
createRules
(
this
);
43
44
}
45
else
46
d_rules
=
createRules
();
47
48
}
49
50
51
//! Destructor
52
SearchEngine::~SearchEngine
()
53
{
54
delete
d_rules
;
55
}
56
57
bool
SearchEngine::tryModelGeneration
(
Theorem
& thm) {
58
59
if
(!
lastThm
().isNull())
throw
EvalException
(
"Method tryModelGenereation() (or command COUNTERMODEL)\n must be called only after failed QUERY"
);
60
61
// Save the scope level, to recover on errors
62
push
();
63
d_core
->
collectBasicVars
();
64
bool
success =
d_core
->
refineCounterExample
(thm);
65
if
(!success) {
66
pop
();
67
return
false
;
68
}
69
70
QueryResult
qres =
checkValid
(
d_core
->
falseExpr
(), thm);
71
if
(qres ==
VALID
) {
72
pop
();
73
return
false
;
74
}
75
76
success =
d_core
->
buildModel
(thm);
77
if
(!success) {
78
pop
();
79
return
false
;
80
}
81
82
qres =
checkValid
(
d_core
->
falseExpr
(), thm);
83
if
(qres ==
VALID
) {
84
pop
();
85
return
false
;
86
}
87
88
return
true
;
89
}
90
91
void
SearchEngine::getConcreteModel
(
ExprMap<Expr>
& m)
92
{
93
TRACE
(
"model"
,
"Building a concrete model"
,
""
,
"{"
);
94
if
(!
lastThm
().isNull())
95
throw
EvalException
96
(
"Method getConcreteModel() (or command COUNTERMODEL)\n"
97
" must be called only after failed QUERY"
);
98
// Save the scope level, to recover on errors
99
push
();
100
d_core
->
collectBasicVars
();
101
try
{
102
d_core
->
refineCounterExample
();
103
}
catch
(
Exception
& e) {
104
// Clean up and re-throw the exception
105
pop
();
106
throw
e;
107
}
108
Theorem
thm;
109
QueryResult
qres =
checkValid
(
d_core
->
falseExpr
(), thm);
110
if
(qres ==
VALID
) {
111
vector<Expr> assump;
112
getAssumptions
(assump);
113
d_core
->
inconsistentThm
().
getLeafAssumptions
(assump);
114
Expr
a =
Expr
(
RAW_LIST
, assump,
d_core
->
getEM
());
115
pop
();
116
throw
Exception
117
(
"Model Creation failed after refining counterexample\n"
118
"due to the following assumptions:\n "
119
+a.
toString
()
120
+
"\n\nYou might be using an incomplete fragment of the theory"
);
121
}
122
// else if (qres != INVALID) {
123
// throw EvalException
124
// ("Unable to build concrete model");
125
// }
126
try
{
127
d_core
->
buildModel
(m);
128
}
catch
(
Exception
& e) {
129
// Clean up and re-throw the exception
130
pop
();
131
throw
e;
132
}
133
qres =
checkValid
(
d_core
->
falseExpr
(), thm);
134
if
(qres ==
VALID
) {
135
vector<Expr> assump;
136
getAssumptions
(assump);
137
Expr
a =
Expr
(
RAW_LIST
, assump,
d_core
->
getEM
());
138
pop
();
139
throw
Exception
140
(
"Model Creation failed due to the following assumptions:\n"
141
+a.
toString
()
142
+
"\n\nYou might be using an incomplete fragment of the theory"
);
143
}
144
// else if (qres != INVALID) {
145
// throw EvalException
146
// ("Unable to build concrete model");
147
// }
148
TRACE
(
"model"
,
"Building a concrete model"
,
""
,
"}"
);
149
}
Generated on Sat Aug 3 2013 07:58:30 for CVC3 by
1.8.4