1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mudathir Mohamed, Andrew Reynolds, Haniel Barbosa |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of the builtin theory. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/builtin/theory_builtin.h" |
17 |
|
|
18 |
|
#include "expr/kind.h" |
19 |
|
#include "proof/proof_node_manager.h" |
20 |
|
#include "theory/builtin/theory_builtin_rewriter.h" |
21 |
|
#include "theory/theory_model.h" |
22 |
|
#include "theory/valuation.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
namespace builtin { |
27 |
|
|
28 |
9942 |
TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation) |
29 |
|
: Theory(THEORY_BUILTIN, env, out, valuation), |
30 |
|
d_checker(env), |
31 |
|
d_state(env, valuation), |
32 |
9942 |
d_im(env, *this, d_state, d_pnm, "theory::builtin::") |
33 |
|
{ |
34 |
|
// indicate we are using the default theory state and inference managers |
35 |
9942 |
d_theoryState = &d_state; |
36 |
9942 |
d_inferManager = &d_im; |
37 |
9942 |
} |
38 |
|
|
39 |
9942 |
TheoryRewriter* TheoryBuiltin::getTheoryRewriter() { return &d_rewriter; } |
40 |
|
|
41 |
3796 |
ProofRuleChecker* TheoryBuiltin::getProofChecker() { return &d_checker; } |
42 |
|
|
43 |
|
std::string TheoryBuiltin::identify() const |
44 |
|
{ |
45 |
|
return std::string("TheoryBuiltin"); |
46 |
|
} |
47 |
|
|
48 |
9942 |
void TheoryBuiltin::finishInit() |
49 |
|
{ |
50 |
|
// Notice that choice is an unevaluated kind belonging to this theory. |
51 |
|
// However, it should be set as an unevaluated kind where it is used, e.g. |
52 |
|
// in the quantifiers theory. This ensures that a logic like QF_LIA, which |
53 |
|
// includes the builtin theory, does not mark any kinds as unevaluated and |
54 |
|
// hence it is easy to check for illegal eliminations via TheoryModel |
55 |
|
// (see TheoryModel::isLegalElimination) since there are no unevaluated kinds |
56 |
|
// present. |
57 |
9942 |
} |
58 |
|
|
59 |
|
} // namespace builtin |
60 |
|
} // namespace theory |
61 |
29577 |
} // namespace cvc5 |