1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Gereon Kremer, Aina Niemetz
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * The theory inference utility.
16 #include "theory/theory_inference.h"
18 #include "theory/theory_inference_manager.h"
20 using namespace cvc5::kind
;
25 SimpleTheoryLemma::SimpleTheoryLemma(InferenceId id
,
29 : TheoryInference(id
), d_node(n
), d_property(p
), d_pg(pg
)
33 TrustNode
SimpleTheoryLemma::processLemma(LemmaProperty
& p
)
35 Assert(!d_node
.isNull());
37 return TrustNode::mkTrustLemma(d_node
, d_pg
);
40 SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id
,
44 : TheoryInference(id
), d_conc(conc
), d_exp(exp
), d_pg(pg
)
48 Node
SimpleTheoryInternalFact::processFact(std::vector
<Node
>& exp
,