summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bv_sat_solver_notify.h4
-rw-r--r--src/prop/cadical.h6
-rw-r--r--src/prop/cnf_stream.h6
-rw-r--r--src/prop/cryptominisat.h6
-rw-r--r--src/prop/kissat.h6
-rw-r--r--src/prop/proof_cnf_stream.h4
-rw-r--r--src/prop/proof_post_processor.h4
-rw-r--r--src/prop/prop_engine.h6
-rw-r--r--src/prop/prop_proof_manager.h6
-rw-r--r--src/prop/registrar.h6
-rw-r--r--src/prop/sat_proof_manager.h6
-rw-r--r--src/prop/sat_solver.h6
-rw-r--r--src/prop/sat_solver_factory.h6
-rw-r--r--src/prop/skolem_def_manager.h6
-rw-r--r--src/prop/theory_proxy.h6
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback