From: PaulMeng <pmtruth@hotmail.com>
Date: Tue, 5 Jul 2016 18:21:11 +0000 (-0400)
Subject: resolved merge conflicts
X-Git-Tag: cvc5-1.0.0~6048
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0294ec0d13c631bf471c07ba26809cda0f0b9b51;p=cvc5.git

resolved merge conflicts
---

diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index a0c9cbe6b..dfd893fe8 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -613,9 +613,6 @@ public:
   /** get the record representation for this datatype */
   inline Record * getRecord() const;
 
-  /** get the record representation for this datatype */
-  inline Record * getRecord() const;
-
   /**
    * Return the cardinality of this datatype (the sum of the
    * cardinalities of its constructors).  The Datatype must be
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 9c4e554e1..31c911736 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -124,9 +124,6 @@ public:
   /** Get the type for regular expressions. */
   RegExpType regExpType() const;
 
-  /** Get the type for regular expressions. */
-  RegExpType regExpType() const;
-
   /** Get the type for reals. */
   RealType realType() const;
 
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index c6c0d6def..929bccada 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -268,8 +268,6 @@ class EagerBitblaster : public TBitblaster<Node> {
 
   MinisatEmptyNotify d_notify;
 
-  MinisatEmptyNotify d_notify;
-
   Node getModelFromSatSolver(TNode a, bool fullModel);
   bool isSharedTerm(TNode node);
 
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 37071eb2e..217432670 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -139,20 +139,6 @@ private:
    */
   bool lemma(Node n, SetsLemmaTag t);
 
-  /** send out a lemma */
-  enum SetsLemmaTag {
-    SETS_LEMMA_DISEQUAL,
-    SETS_LEMMA_MEMBER,
-    SETS_LEMMA_GRAPH,
-    SETS_LEMMA_OTHER
-  };
-
-  /**
-   * returns true if a lemmas was generated
-   * returns false otherwise (found in cache)
-   */
-  bool lemma(Node n, SetsLemmaTag t);
-
   class TermInfoManager {
     TheorySetsPrivate& d_theory;
     context::Context* d_context;