resolved merge conflicts

diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index a0c9cbe6b54aac022d363304daaa0af257565071..dfd893fe8288b789923a7a4bd272e6e9435251b4 100644 (file)
--- 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 9c4e554e19145b978ec2ff8fb5b555528e263535..31c911736648c95d975959fecb68448dbdaa369c 100644 (file)
--- 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 c6c0d6def7a5f285964be78ebc868e64adf207d7..929bccada3e0831e1a16c3d8cfa1454e290ebe61 100644 (file)
--- 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 37071eb2ef458998c9ed9afd766d1ff7628d9917..21743267003afaa651b08ae369fee50ad2a7f9be 100644 (file)
--- 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;