diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-01 10:39:13 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-01 10:39:13 -0700 |
commit | 0cc88cf09c59effc41a076d4d78ef2082f780509 (patch) | |
tree | 29499ec78572f954eb053083a32ac4bfca4aa530 /src/prop | |
parent | 689f1f89ccea1825a7b222e5af97f5133069ff74 (diff) | |
parent | 172e0bd41cbd410fb1e66bc32a9a9b8523bc40e2 (diff) |
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bv_sat_solver_notify.h | 10 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 4 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 4 | ||||
-rw-r--r-- | src/prop/cadical.cpp | 4 | ||||
-rw-r--r-- | src/prop/cadical.h | 10 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 2 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 8 | ||||
-rw-r--r-- | src/prop/cryptominisat.cpp | 4 | ||||
-rw-r--r-- | src/prop/cryptominisat.h | 10 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 4 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 4 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 2 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 8 | ||||
-rw-r--r-- | src/prop/registrar.h | 10 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 10 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 4 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.h | 10 | ||||
-rw-r--r-- | src/prop/sat_solver_types.h | 20 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 4 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 10 |
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 */ |