diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bv_sat_solver_notify.h | 4 | ||||
-rw-r--r-- | src/prop/cadical.h | 6 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 6 | ||||
-rw-r--r-- | src/prop/cryptominisat.h | 6 | ||||
-rw-r--r-- | src/prop/kissat.h | 6 | ||||
-rw-r--r-- | src/prop/proof_cnf_stream.h | 4 | ||||
-rw-r--r-- | src/prop/proof_post_processor.h | 4 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 6 | ||||
-rw-r--r-- | src/prop/prop_proof_manager.h | 6 | ||||
-rw-r--r-- | src/prop/registrar.h | 6 | ||||
-rw-r--r-- | src/prop/sat_proof_manager.h | 6 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 6 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.h | 6 | ||||
-rw-r--r-- | src/prop/skolem_def_manager.h | 6 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 6 |
15 files changed, 42 insertions, 42 deletions
diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h index fe95e7adb..df698c722 100644 --- a/src/prop/bv_sat_solver_notify.h +++ b/src/prop/bv_sat_solver_notify.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__BVSATSOLVERNOTIFY_H -#define CVC4__PROP__BVSATSOLVERNOTIFY_H +#ifndef CVC5__PROP__BVSATSOLVERNOTIFY_H +#define CVC5__PROP__BVSATSOLVERNOTIFY_H #include "prop/sat_solver_types.h" #include "util/resource_manager.h" diff --git a/src/prop/cadical.h b/src/prop/cadical.h index 910e5def5..ed4c166d4 100644 --- a/src/prop/cadical.h +++ b/src/prop/cadical.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__CADICAL_H -#define CVC4__PROP__CADICAL_H +#ifndef CVC5__PROP__CADICAL_H +#define CVC5__PROP__CADICAL_H #ifdef CVC4_USE_CADICAL @@ -106,4 +106,4 @@ class CadicalSolver : public SatSolver } // namespace cvc5 #endif // CVC4_USE_CADICAL -#endif // CVC4__PROP__CADICAL_H +#endif // CVC5__PROP__CADICAL_H diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index b39423d71..4b41ad691 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -22,8 +22,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__CNF_STREAM_H -#define CVC4__PROP__CNF_STREAM_H +#ifndef CVC5__PROP__CNF_STREAM_H +#define CVC5__PROP__CNF_STREAM_H #include "context/cdhashset.h" #include "context/cdinsert_hashmap.h" @@ -320,4 +320,4 @@ class CnfStream { } // namespace prop } // namespace cvc5 -#endif /* CVC4__PROP__CNF_STREAM_H */ +#endif /* CVC5__PROP__CNF_STREAM_H */ diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index 65e1196f3..ceed47d79 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__CRYPTOMINISAT_H -#define CVC4__PROP__CRYPTOMINISAT_H +#ifndef CVC5__PROP__CRYPTOMINISAT_H +#define CVC5__PROP__CRYPTOMINISAT_H #ifdef CVC4_USE_CRYPTOMINISAT @@ -109,4 +109,4 @@ class CryptoMinisatSolver : public SatSolver } // namespace cvc5 #endif // CVC4_USE_CRYPTOMINISAT -#endif // CVC4__PROP__CRYPTOMINISAT_H +#endif // CVC5__PROP__CRYPTOMINISAT_H diff --git a/src/prop/kissat.h b/src/prop/kissat.h index 6984a7e50..2ab38dbab 100644 --- a/src/prop/kissat.h +++ b/src/prop/kissat.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__KISSAT_H -#define CVC4__PROP__KISSAT_H +#ifndef CVC5__PROP__KISSAT_H +#define CVC5__PROP__KISSAT_H #ifdef CVC4_USE_KISSAT @@ -100,4 +100,4 @@ class KissatSolver : public SatSolver } // namespace cvc5 #endif // CVC4_USE_KISSAT -#endif // CVC4__PROP__KISSAT_H +#endif // CVC5__PROP__KISSAT_H diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index fcca2cb34..5848c64f0 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__PROOF_CNF_STREAM_H -#define CVC4__PROP__PROOF_CNF_STREAM_H +#ifndef CVC5__PROP__PROOF_CNF_STREAM_H +#define CVC5__PROP__PROOF_CNF_STREAM_H #include "context/cdhashmap.h" #include "expr/lazy_proof.h" diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h index 906faaafd..68b6d3a42 100644 --- a/src/prop/proof_post_processor.h +++ b/src/prop/proof_post_processor.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__PROOF_POST_PROCESSOR_H -#define CVC4__PROP__PROOF_POST_PROCESSOR_H +#ifndef CVC5__PROP__PROOF_POST_PROCESSOR_H +#define CVC5__PROP__PROOF_POST_PROCESSOR_H #include <map> #include <unordered_set> diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index a01668913..99c615211 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP_ENGINE_H -#define CVC4__PROP_ENGINE_H +#ifndef CVC5__PROP_ENGINE_H +#define CVC5__PROP_ENGINE_H #include "context/cdlist.h" #include "expr/node.h" @@ -383,4 +383,4 @@ class PropEngine } // namespace prop } // namespace cvc5 -#endif /* CVC4__PROP_ENGINE_H */ +#endif /* CVC5__PROP_ENGINE_H */ diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index 9a080edc1..45136085d 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP_PROOF_MANAGER_H -#define CVC4__PROP_PROOF_MANAGER_H +#ifndef CVC5__PROP_PROOF_MANAGER_H +#define CVC5__PROP_PROOF_MANAGER_H #include "context/cdlist.h" #include "expr/proof.h" @@ -94,4 +94,4 @@ class PropPfManager } // namespace prop } // namespace cvc5 -#endif /* CVC4__PROP__PROOF_MANAGER_H */ +#endif /* CVC5__PROP__PROOF_MANAGER_H */ diff --git a/src/prop/registrar.h b/src/prop/registrar.h index ae085b573..daa364bcb 100644 --- a/src/prop/registrar.h +++ b/src/prop/registrar.h @@ -20,8 +20,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__REGISTRAR_H -#define CVC4__PROP__REGISTRAR_H +#ifndef CVC5__PROP__REGISTRAR_H +#define CVC5__PROP__REGISTRAR_H namespace cvc5 { namespace prop { @@ -42,4 +42,4 @@ public: } // namespace prop } // namespace cvc5 -#endif /* CVC4__PROP__REGISTRAR_H */ +#endif /* CVC5__PROP__REGISTRAR_H */ diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 6407939c7..426771a37 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__SAT_PROOF_MANAGER_H -#define CVC4__SAT_PROOF_MANAGER_H +#ifndef CVC5__SAT_PROOF_MANAGER_H +#define CVC5__SAT_PROOF_MANAGER_H #include "context/cdhashset.h" #include "expr/buffered_proof_generator.h" @@ -590,4 +590,4 @@ class SatProofManager } // namespace prop } // namespace cvc5 -#endif /* CVC4__SAT_PROOF_MANAGER_H */ +#endif /* CVC5__SAT_PROOF_MANAGER_H */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 1f59a7bd6..ae87d1396 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__SAT_SOLVER_H -#define CVC4__PROP__SAT_SOLVER_H +#ifndef CVC5__PROP__SAT_SOLVER_H +#define CVC5__PROP__SAT_SOLVER_H #include <string> @@ -211,4 +211,4 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) { } // namespace prop } // namespace cvc5 -#endif /* CVC4__PROP__SAT_MODULE_H */ +#endif /* CVC5__PROP__SAT_MODULE_H */ diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 71e28ac39..cebbe6e27 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__SAT_SOLVER_FACTORY_H -#define CVC4__PROP__SAT_SOLVER_FACTORY_H +#ifndef CVC5__PROP__SAT_SOLVER_FACTORY_H +#define CVC5__PROP__SAT_SOLVER_FACTORY_H #include <string> #include <vector> @@ -52,4 +52,4 @@ class SatSolverFactory } // namespace prop } // namespace cvc5 -#endif // CVC4__PROP__SAT_SOLVER_FACTORY_H +#endif // CVC5__PROP__SAT_SOLVER_FACTORY_H diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h index 11b726c2a..1b7b9b4dc 100644 --- a/src/prop/skolem_def_manager.h +++ b/src/prop/skolem_def_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__SKOLEM_DEF_MANAGER_H -#define CVC4__PROP__SKOLEM_DEF_MANAGER_H +#ifndef CVC5__PROP__SKOLEM_DEF_MANAGER_H +#define CVC5__PROP__SKOLEM_DEF_MANAGER_H #include <iosfwd> #include <unordered_set> @@ -88,4 +88,4 @@ class SkolemDefManager } // namespace prop } // namespace cvc5 -#endif /* CVC4__PROP__SKOLEM_DEF_MANAGER_H */ +#endif /* CVC5__PROP__SKOLEM_DEF_MANAGER_H */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 3b21bde58..503b37ed7 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PROP__SAT_H -#define CVC4__PROP__SAT_H +#ifndef CVC5__PROP__SAT_H +#define CVC5__PROP__SAT_H // Just defining this for now, since there's no other SAT solver bindings. // Optional blocks below will be unconditionally included @@ -169,4 +169,4 @@ class TheoryProxy : public Registrar } // namespace cvc5 -#endif /* CVC4__PROP__SAT_H */ +#endif /* CVC5__PROP__SAT_H */ |