diff options
Diffstat (limited to 'src/theory/uf/theory_uf.h')
-rw-r--r-- | src/theory/uf/theory_uf.h | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 2bfd7e16c..41f2ba9d5 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -112,17 +112,6 @@ private: */ bool propagateLit(TNode literal); - /** - * Explain why this literal is true by adding assumptions - * with proof (if "pf" is non-NULL). - */ - void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf); - - /** - * Explain a literal, with proof (if "pf" is non-NULL). - */ - Node explain(TNode literal, eq::EqProof* pf); - /** All the function terms that the theory has seen */ context::CDList<TNode> d_functionsTerms; @@ -202,6 +191,9 @@ private: CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); } private: + /** Explain why this literal is true by building an explanation */ + void explain(TNode literal, Node& exp); + bool areCareDisequal(TNode x, TNode y); void addCarePairs(const TNodeTrie* t1, const TNodeTrie* t2, |