20 files changed, 79 insertions, 63 deletions
diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h
index 686848829..77163cfe6 100644
--- a/src/prop/bv_sat_solver_notify.h
+++ b/src/prop/bv_sat_solver_notify.h
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file sat_solver_notify.h
+/*! \file bv_sat_solver_notify.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Dejan Jovanovic, Morgan Deters
+ **   Liana Hadarean, Alex Ozdemir, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP__BVSATSOLVERNOTIFY_H
-#define __CVC4__PROP__BVSATSOLVERNOTIFY_H
+#ifndef CVC4__PROP__BVSATSOLVERNOTIFY_H
+#define CVC4__PROP__BVSATSOLVERNOTIFY_H
 
 #include "prop/sat_solver_types.h"
 
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 57ef8ef30..76d473395 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -2,9 +2,9 @@
 /*! \file bvminisat.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Liana Hadarean, Tim King
+ **   Liana Hadarean, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index efb90a3f0..ca9c553d9 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -2,9 +2,9 @@
 /*! \file bvminisat.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Mathias Preiner, Liana Hadarean
+ **   Mathias Preiner, Liana Hadarean, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 3fd210699..5a0968ec8 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -2,9 +2,9 @@
 /*! \file cadical.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner
+ **   Mathias Preiner, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index 2e2c1cc51..e43a2d278 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -2,9 +2,9 @@
 /*! \file cadical.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner
+ **   Mathias Preiner, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP__CADICAL_H
-#define __CVC4__PROP__CADICAL_H
+#ifndef CVC4__PROP__CADICAL_H
+#define CVC4__PROP__CADICAL_H
 
 #ifdef CVC4_USE_CADICAL
 
@@ -87,4 +87,4 @@ class CadicalSolver : public SatSolver
 }  // namespace CVC4
 
 #endif  // CVC4_USE_CADICAL
-#endif  // __CVC4__PROP__CADICAL_H
+#endif  // CVC4__PROP__CADICAL_H
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 84c315547..dc4722fa1 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Dejan Jovanovic, Liana Hadarean, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index e0996014a..8e60863fa 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Dejan Jovanovic, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -22,8 +22,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP__CNF_STREAM_H
-#define __CVC4__PROP__CNF_STREAM_H
+#ifndef CVC4__PROP__CNF_STREAM_H
+#define CVC4__PROP__CNF_STREAM_H
 
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
@@ -338,4 +338,4 @@ class TseitinCnfStream : public CnfStream {
 } /* CVC4::prop namespace */
 } /* CVC4 namespace */
 
-#endif /* __CVC4__PROP__CNF_STREAM_H */
+#endif /* CVC4__PROP__CNF_STREAM_H */
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 970ba13cf..62e2c5a43 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -2,9 +2,9 @@
 /*! \file cryptominisat.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Mathias Preiner
+ **   Liana Hadarean, Mathias Preiner, Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 17cc1568c..d3c5aeb30 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -2,9 +2,9 @@
 /*! \file cryptominisat.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Mathias Preiner
+ **   Mathias Preiner, Liana Hadarean, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP__CRYPTOMINISAT_H
-#define __CVC4__PROP__CRYPTOMINISAT_H
+#ifndef CVC4__PROP__CRYPTOMINISAT_H
+#define CVC4__PROP__CRYPTOMINISAT_H
 
 #ifdef CVC4_USE_CRYPTOMINISAT
 
@@ -95,4 +95,4 @@ public:
 }  // namespace CVC4
 
 #endif  // CVC4_USE_CRYPTOMINISAT
-#endif  // __CVC4__PROP__CRYPTOMINISAT_H
+#endif  // CVC4__PROP__CRYPTOMINISAT_H
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 3c11d5ad8..4995a60dd 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -2,9 +2,9 @@
 /*! \file minisat.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters, Tim King
+ **   Liana Hadarean, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index dc42066d7..d4720def5 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -2,9 +2,9 @@
 /*! \file minisat.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Mathias Preiner, Morgan Deters
+ **   Mathias Preiner, Liana Hadarean, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index e1200c7e5..b12573085 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 2ff862d18..aaa65b85a 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP_ENGINE_H
-#define __CVC4__PROP_ENGINE_H
+#ifndef CVC4__PROP_ENGINE_H
+#define CVC4__PROP_ENGINE_H
 
 #include <sys/time.h>
 
@@ -248,4 +248,4 @@ public:
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PROP_ENGINE_H */
+#endif /* CVC4__PROP_ENGINE_H */
diff --git a/src/prop/registrar.h b/src/prop/registrar.h
index 46c2cdd0d..0846b8829 100644
--- a/src/prop/registrar.h
+++ b/src/prop/registrar.h
@@ -2,9 +2,9 @@
 /*! \file registrar.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Liana Hadarean, Morgan Deters
+ **   Liana Hadarean, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -20,8 +20,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP__REGISTRAR_H
-#define __CVC4__PROP__REGISTRAR_H
+#ifndef CVC4__PROP__REGISTRAR_H
+#define CVC4__PROP__REGISTRAR_H
 
 namespace CVC4 {
 namespace prop {
@@ -42,4 +42,4 @@ public:
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PROP__REGISTRAR_H */
+#endif /* CVC4__PROP__REGISTRAR_H */
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 70e46eceb..45bfca4d6 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -2,9 +2,9 @@
 /*! \file sat_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Dejan Jovanovic, Morgan Deters
+ **   Dejan Jovanovic, Liana Hadarean, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP__SAT_SOLVER_H
-#define __CVC4__PROP__SAT_SOLVER_H
+#ifndef CVC4__PROP__SAT_SOLVER_H
+#define CVC4__PROP__SAT_SOLVER_H
 
 #include <stdint.h>
 
@@ -192,4 +192,4 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PROP__SAT_MODULE_H */
+#endif /* CVC4__PROP__SAT_MODULE_H */
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 81e15777d..cfab5703c 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -2,9 +2,9 @@
 /*! \file sat_solver_factory.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner, Dejan Jovanovic, Tim King
+ **   Mathias Preiner, Liana Hadarean, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index eb588af13..5f8649768 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -2,9 +2,9 @@
 /*! \file sat_solver_factory.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner, Dejan Jovanovic, Liana Hadarean
+ **   Mathias Preiner, Liana Hadarean, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP__SAT_SOLVER_FACTORY_H
-#define __CVC4__PROP__SAT_SOLVER_FACTORY_H
+#ifndef CVC4__PROP__SAT_SOLVER_FACTORY_H
+#define CVC4__PROP__SAT_SOLVER_FACTORY_H
 
 #include <string>
 #include <vector>
@@ -50,4 +50,4 @@ class SatSolverFactory
 }  // namespace prop
 }  // namespace CVC4
 
-#endif  // __CVC4__PROP__SAT_SOLVER_FACTORY_H
+#endif  // CVC4__PROP__SAT_SOLVER_FACTORY_H
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index ed1c5397d..f1fd6233e 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -2,9 +2,9 @@
 /*! \file sat_solver_types.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Kshitij Bansal, Liana Hadarean
+ **   Dejan Jovanovic, Liana Hadarean, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -26,6 +26,7 @@
 
 #include <sstream>
 #include <string>
+#include <unordered_set>
 #include <vector>
 
 namespace CVC4 {
@@ -167,6 +168,21 @@ struct SatLiteralHashFunction {
  */
 typedef std::vector<SatLiteral> SatClause;
 
+struct SatClauseSetHashFunction
+{
+  inline size_t operator()(
+      const std::unordered_set<SatLiteral, SatLiteralHashFunction>& clause)
+      const
+  {
+    size_t acc = 0;
+    for (const auto& l : clause)
+    {
+      acc ^= l.hash();
+    }
+    return acc;
+  }
+};
+
 /**
  * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
  * so that the SAT solver can (or should) remove them when the lifespan is over.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 2526830f9..f6cd42eff 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -2,9 +2,9 @@
 /*! \file theory_proxy.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Guy Katz
+ **   Morgan Deters, Tim King, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index e2923ddff..3bb15aa4e 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,12 +16,12 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP__SAT_H
-#define __CVC4__PROP__SAT_H
+#ifndef CVC4__PROP__SAT_H
+#define CVC4__PROP__SAT_H
 
 // Just defining this for now, since there's no other SAT solver bindings.
 // Optional blocks below will be unconditionally included
-#define __CVC4_USE_MINISAT
+#define CVC4_USE_MINISAT
 
 #include <iosfwd>
 #include <unordered_set>
@@ -152,4 +152,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PROP__SAT_H */
+#endif /* CVC4__PROP__SAT_H */