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 |
9853 |
TheoryBuiltin::TheoryBuiltin(context::Context* c, |
29 |
|
context::UserContext* u, |
30 |
|
OutputChannel& out, |
31 |
|
Valuation valuation, |
32 |
|
const LogicInfo& logicInfo, |
33 |
9853 |
ProofNodeManager* pnm) |
34 |
|
: Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm), |
35 |
|
d_state(c, u, valuation), |
36 |
9853 |
d_im(*this, d_state, pnm, "theory::builtin::") |
37 |
|
{ |
38 |
|
// indicate we are using the default theory state and inference managers |
39 |
9853 |
d_theoryState = &d_state; |
40 |
9853 |
d_inferManager = &d_im; |
41 |
9853 |
} |
42 |
|
|
43 |
9853 |
TheoryRewriter* TheoryBuiltin::getTheoryRewriter() { return &d_rewriter; } |
44 |
|
|
45 |
3768 |
ProofRuleChecker* TheoryBuiltin::getProofChecker() { return &d_checker; } |
46 |
|
|
47 |
|
std::string TheoryBuiltin::identify() const |
48 |
|
{ |
49 |
|
return std::string("TheoryBuiltin"); |
50 |
|
} |
51 |
|
|
52 |
9853 |
void TheoryBuiltin::finishInit() |
53 |
|
{ |
54 |
|
// Notice that choice is an unevaluated kind belonging to this theory. |
55 |
|
// However, it should be set as an unevaluated kind where it is used, e.g. |
56 |
|
// in the quantifiers theory. This ensures that a logic like QF_LIA, which |
57 |
|
// includes the builtin theory, does not mark any kinds as unevaluated and |
58 |
|
// hence it is easy to check for illegal eliminations via TheoryModel |
59 |
|
// (see TheoryModel::isLegalElimination) since there are no unevaluated kinds |
60 |
|
// present. |
61 |
9853 |
} |
62 |
|
|
63 |
|
} // namespace builtin |
64 |
|
} // namespace theory |
65 |
29322 |
} // namespace cvc5 |