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