762cdfd8be4286712dfca7d6da232bd5654a21ec
1 /********************* */
2 /*! \file inference_manager.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Datatypes inference manager
15 #include "theory/datatypes/inference_manager.h"
17 #include "expr/dtype.h"
18 #include "options/datatypes_options.h"
19 #include "theory/theory.h"
21 using namespace CVC4::kind
;
27 DatatypesInference::DatatypesInference(Node conc
, Node exp
, ProofGenerator
* pg
)
28 : SimpleTheoryInternalFact(conc
, exp
, pg
)
30 // false is not a valid explanation
31 Assert(d_exp
.isNull() || !d_exp
.isConst() || d_exp
.getConst
<bool>());
34 bool DatatypesInference::mustCommunicateFact(Node n
, Node exp
)
36 Trace("dt-lemma-debug") << "Compute for " << exp
<< " => " << n
<< std::endl
;
37 bool addLemma
= false;
38 if (options::dtInferAsLemmas() && !exp
.isConst())
40 // all units are lemmas
43 else if (n
.getKind() == EQUAL
)
45 TypeNode tn
= n
[0].getType();
52 const DType
& dt
= tn
.getDType();
53 addLemma
= dt
.involvesExternalType();
56 else if (n
.getKind() == LEQ
|| n
.getKind() == OR
)
62 Trace("dt-lemma-debug") << "Communicate " << n
<< std::endl
;
65 Trace("dt-lemma-debug") << "Do not need to communicate " << n
<< std::endl
;
69 bool DatatypesInference::process(TheoryInferenceManager
* im
)
71 // check to see if we have to communicate it to the rest of the system
72 if (mustCommunicateFact(d_conc
, d_exp
))
74 // send it as an (explained) lemma
75 std::vector
<Node
> exp
;
76 if (!d_exp
.isNull() && !d_exp
.isConst())
80 return im
->lemmaExp(d_conc
, exp
, {});
82 // assert the internal fact
83 bool polarity
= d_conc
.getKind() != NOT
;
84 TNode atom
= polarity
? d_conc
: d_conc
[0];
85 im
->assertInternalFact(atom
, polarity
, d_exp
);
89 InferenceManager::InferenceManager(Theory
& t
,
91 ProofNodeManager
* pnm
)
92 : InferenceManagerBuffered(t
, state
, pnm
)
96 void InferenceManager::addPendingInference(Node conc
,
100 d_pendingFact
.push_back(std::make_shared
<DatatypesInference
>(conc
, exp
, pg
));
103 void InferenceManager::process()
105 // process pending lemmas, used infrequently, only for definitional lemmas
107 // now process the pending facts
111 bool InferenceManager::sendLemmas(const std::vector
<Node
>& lemmas
)
114 for (const Node
& lem
: lemmas
)
124 } // namespace datatypes
125 } // namespace theory