diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/arith_proof.h | 6 | ||||
-rw-r--r-- | src/proof/arith_proof_recorder.h | 4 | ||||
-rw-r--r-- | src/proof/array_proof.h | 6 | ||||
-rw-r--r-- | src/proof/bitvector_proof.h | 6 | ||||
-rw-r--r-- | src/proof/clausal_bitvector_proof.h | 6 | ||||
-rw-r--r-- | src/proof/clause_id.h | 6 | ||||
-rw-r--r-- | src/proof/cnf_proof.h | 6 | ||||
-rw-r--r-- | src/proof/dimacs_printer.h | 6 | ||||
-rw-r--r-- | src/proof/drat/drat_proof.h | 6 | ||||
-rw-r--r-- | src/proof/er/er_proof.h | 6 | ||||
-rw-r--r-- | src/proof/lemma_proof.h | 6 | ||||
-rw-r--r-- | src/proof/lfsc_proof_printer.h | 6 | ||||
-rw-r--r-- | src/proof/lrat/lrat_proof.h | 4 | ||||
-rw-r--r-- | src/proof/proof.h | 6 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 6 | ||||
-rw-r--r-- | src/proof/proof_output_channel.h | 6 | ||||
-rw-r--r-- | src/proof/resolution_bitvector_proof.h | 6 | ||||
-rw-r--r-- | src/proof/sat_proof.h | 6 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 6 | ||||
-rw-r--r-- | src/proof/simplify_boolean_node.h | 6 | ||||
-rw-r--r-- | src/proof/skolemization_manager.h | 6 | ||||
-rw-r--r-- | src/proof/theory_proof.h | 6 | ||||
-rw-r--r-- | src/proof/uf_proof.h | 6 | ||||
-rw-r--r-- | src/proof/unsat_core.h | 6 |
24 files changed, 70 insertions, 70 deletions
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index a93bf4c57..a1df24fac 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__ARITH__PROOF_H -#define __CVC4__ARITH__PROOF_H +#ifndef CVC4__ARITH__PROOF_H +#define CVC4__ARITH__PROOF_H #include <memory> #include <unordered_set> @@ -172,4 +172,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__ARITH__PROOF_H */ +#endif /* CVC4__ARITH__PROOF_H */ diff --git a/src/proof/arith_proof_recorder.h b/src/proof/arith_proof_recorder.h index fe7bffbd0..3fff6968d 100644 --- a/src/proof/arith_proof_recorder.h +++ b/src/proof/arith_proof_recorder.h @@ -42,8 +42,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF__ARITH_PROOF_RECORDER_H -#define __CVC4__PROOF__ARITH_PROOF_RECORDER_H +#ifndef CVC4__PROOF__ARITH_PROOF_RECORDER_H +#define CVC4__PROOF__ARITH_PROOF_RECORDER_H #include <map> #include <set> diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 7e3340af0..372ad1f67 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__ARRAY__PROOF_H -#define __CVC4__ARRAY__PROOF_H +#ifndef CVC4__ARRAY__PROOF_H +#define CVC4__ARRAY__PROOF_H #include <memory> #include <unordered_set> @@ -117,4 +117,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__ARRAY__PROOF_H */ +#endif /* CVC4__ARRAY__PROOF_H */ diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 91c07fcb5..f0a0717fa 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__BITVECTOR_PROOF_H -#define __CVC4__BITVECTOR_PROOF_H +#ifndef CVC4__BITVECTOR_PROOF_H +#define CVC4__BITVECTOR_PROOF_H #include <set> #include <unordered_map> @@ -276,4 +276,4 @@ class BitVectorProof : public TheoryProof }/* CVC4 namespace */ -#endif /* __CVC4__BITVECTOR__PROOF_H */ +#endif /* CVC4__BITVECTOR__PROOF_H */ diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h index b53bcd5e2..b10b1ad1c 100644 --- a/src/proof/clausal_bitvector_proof.h +++ b/src/proof/clausal_bitvector_proof.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H -#define __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H +#ifndef CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H +#define CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H #include <iostream> #include <sstream> @@ -135,4 +135,4 @@ class LfscErBitVectorProof : public LfscClausalBitVectorProof } // namespace CVC4 -#endif /* __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */ +#endif /* CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */ diff --git a/src/proof/clause_id.h b/src/proof/clause_id.h index e8b9841c8..4a9ebc74a 100644 --- a/src/proof/clause_id.h +++ b/src/proof/clause_id.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF__CLAUSE_ID_H -#define __CVC4__PROOF__CLAUSE_ID_H +#ifndef CVC4__PROOF__CLAUSE_ID_H +#define CVC4__PROOF__CLAUSE_ID_H namespace CVC4 { @@ -30,4 +30,4 @@ typedef unsigned ClauseId; }/* CVC4 namespace */ -#endif /* __CVC4__PROOF__CLAUSE_ID_H */ +#endif /* CVC4__PROOF__CLAUSE_ID_H */ diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index a17777c66..e589950bc 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__CNF_PROOF_H -#define __CVC4__CNF_PROOF_H +#ifndef CVC4__CNF_PROOF_H +#define CVC4__CNF_PROOF_H #include <iosfwd> #include <unordered_map> @@ -212,4 +212,4 @@ public: } /* CVC4 namespace */ -#endif /* __CVC4__CNF_PROOF_H */ +#endif /* CVC4__CNF_PROOF_H */ diff --git a/src/proof/dimacs_printer.h b/src/proof/dimacs_printer.h index f46cb51ec..2ae4abefa 100644 --- a/src/proof/dimacs_printer.h +++ b/src/proof/dimacs_printer.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF__DIMACS_PRINTER_H -#define __CVC4__PROOF__DIMACS_PRINTER_H +#ifndef CVC4__PROOF__DIMACS_PRINTER_H +#define CVC4__PROOF__DIMACS_PRINTER_H #include <iosfwd> #include <memory> @@ -63,4 +63,4 @@ void printDimacs( } // namespace proof } // namespace CVC4 -#endif // __CVC4__PROOF__DIMACS_PRINTER_H +#endif // CVC4__PROOF__DIMACS_PRINTER_H diff --git a/src/proof/drat/drat_proof.h b/src/proof/drat/drat_proof.h index c4b7c2e02..082107d0a 100644 --- a/src/proof/drat/drat_proof.h +++ b/src/proof/drat/drat_proof.h @@ -19,8 +19,8 @@ ** **/ -#ifndef __CVC4__PROOF__DRAT__DRAT_PROOF_H -#define __CVC4__PROOF__DRAT__DRAT_PROOF_H +#ifndef CVC4__PROOF__DRAT__DRAT_PROOF_H +#define CVC4__PROOF__DRAT__DRAT_PROOF_H #include "cvc4_private.h" #include "prop/sat_solver.h" @@ -137,4 +137,4 @@ class DratProof } // namespace proof } // namespace CVC4 -#endif // __CVC4__PROOF__DRAT__DRAT_PROOF_H +#endif // CVC4__PROOF__DRAT__DRAT_PROOF_H diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h index 0a0038738..f5af0783b 100644 --- a/src/proof/er/er_proof.h +++ b/src/proof/er/er_proof.h @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF__ER__ER_PROOF_H -#define __CVC4__PROOF__ER__ER_PROOF_H +#ifndef CVC4__PROOF__ER__ER_PROOF_H +#define CVC4__PROOF__ER__ER_PROOF_H #include <memory> #include <vector> @@ -205,4 +205,4 @@ class ErProof } // namespace proof } // namespace CVC4 -#endif // __CVC4__PROOF__ER__ER_PROOF_H +#endif // CVC4__PROOF__ER__ER_PROOF_H diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h index b4b40ef1b..7dfce57cf 100644 --- a/src/proof/lemma_proof.h +++ b/src/proof/lemma_proof.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__LEMMA_PROOF_H -#define __CVC4__LEMMA_PROOF_H +#ifndef CVC4__LEMMA_PROOF_H +#define CVC4__LEMMA_PROOF_H #include "expr/expr.h" #include "proof/clause_id.h" @@ -112,4 +112,4 @@ std::ostream& operator<<(std::ostream & out, const LemmaProofRecipe & recipe); } /* CVC4 namespace */ -#endif /* __CVC4__LEMMA_PROOF_H */ +#endif /* CVC4__LEMMA_PROOF_H */ diff --git a/src/proof/lfsc_proof_printer.h b/src/proof/lfsc_proof_printer.h index beef4823e..f2f55aa94 100644 --- a/src/proof/lfsc_proof_printer.h +++ b/src/proof/lfsc_proof_printer.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF__LFSC_PROOF_PRINTER_H -#define __CVC4__PROOF__LFSC_PROOF_PRINTER_H +#ifndef CVC4__PROOF__LFSC_PROOF_PRINTER_H +#define CVC4__PROOF__LFSC_PROOF_PRINTER_H #include <iosfwd> #include <string> @@ -151,4 +151,4 @@ class LFSCProofPrinter } // namespace proof } // namespace CVC4 -#endif /* __CVC4__PROOF__LFSC_PROOF_PRINTER_H */ +#endif /* CVC4__PROOF__LFSC_PROOF_PRINTER_H */ diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h index f231e5a6b..33b2fad3f 100644 --- a/src/proof/lrat/lrat_proof.h +++ b/src/proof/lrat/lrat_proof.h @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF__LRAT__LRAT_PROOF_H -#define __CVC4__PROOF__LRAT__LRAT_PROOF_H +#ifndef CVC4__PROOF__LRAT__LRAT_PROOF_H +#define CVC4__PROOF__LRAT__LRAT_PROOF_H #include <iosfwd> #include <string> diff --git a/src/proof/proof.h b/src/proof/proof.h index b39d73134..9e7e20a22 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF__PROOF_H -#define __CVC4__PROOF__PROOF_H +#ifndef CVC4__PROOF__PROOF_H +#define CVC4__PROOF__PROOF_H #include "options/smt_options.h" @@ -67,4 +67,4 @@ # define PSTATS(x) #endif /* CVC4_PROOF_STATS */ -#endif /* __CVC4__PROOF__PROOF_H */ +#endif /* CVC4__PROOF__PROOF_H */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 0d3250b12..eb5942bea 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF_MANAGER_H -#define __CVC4__PROOF_MANAGER_H +#ifndef CVC4__PROOF_MANAGER_H +#define CVC4__PROOF_MANAGER_H #include <iosfwd> #include <memory> @@ -351,4 +351,4 @@ std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k); -#endif /* __CVC4__PROOF_MANAGER_H */ +#endif /* CVC4__PROOF_MANAGER_H */ diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h index 9bf1e0e5c..ff84a3743 100644 --- a/src/proof/proof_output_channel.h +++ b/src/proof/proof_output_channel.h @@ -13,8 +13,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H -#define __CVC4__PROOF_OUTPUT_CHANNEL_H +#ifndef CVC4__PROOF_OUTPUT_CHANNEL_H +#define CVC4__PROOF_OUTPUT_CHANNEL_H #include <memory> #include <set> @@ -74,4 +74,4 @@ public: } /* CVC4 namespace */ -#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */ +#endif /* CVC4__PROOF_OUTPUT_CHANNEL_H */ diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h index 24d1bc76f..5fd11092f 100644 --- a/src/proof/resolution_bitvector_proof.h +++ b/src/proof/resolution_bitvector_proof.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H -#define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H +#ifndef CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H +#define CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H #include <iosfwd> @@ -110,4 +110,4 @@ class LfscResolutionBitVectorProof : public ResolutionBitVectorProof } // namespace CVC4 -#endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */ +#endif /* CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */ diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 82bd93947..ec0928c07 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__SAT__PROOF_H -#define __CVC4__SAT__PROOF_H +#ifndef CVC4__SAT__PROOF_H +#define CVC4__SAT__PROOF_H #include <stdint.h> @@ -373,4 +373,4 @@ void toSatClause(const typename Solver::TClause& minisat_cl, } /* CVC4 namespace */ -#endif /* __CVC4__SAT__PROOF_H */ +#endif /* CVC4__SAT__PROOF_H */ diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index bc32b7959..d9c959ae4 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__SAT__PROOF_IMPLEMENTATION_H -#define __CVC4__SAT__PROOF_IMPLEMENTATION_H +#ifndef CVC4__SAT__PROOF_IMPLEMENTATION_H +#define CVC4__SAT__PROOF_IMPLEMENTATION_H #include "proof/clause_id.h" #include "proof/cnf_proof.h" @@ -1081,4 +1081,4 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) { } /* CVC4 namespace */ -#endif /* __CVC4__SAT__PROOF_IMPLEMENTATION_H */ +#endif /* CVC4__SAT__PROOF_IMPLEMENTATION_H */ diff --git a/src/proof/simplify_boolean_node.h b/src/proof/simplify_boolean_node.h index 0b1cf4990..fe8b7174b 100644 --- a/src/proof/simplify_boolean_node.h +++ b/src/proof/simplify_boolean_node.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__SIMPLIFY_BOOLEAN_NODE_H -#define __CVC4__SIMPLIFY_BOOLEAN_NODE_H +#ifndef CVC4__SIMPLIFY_BOOLEAN_NODE_H +#define CVC4__SIMPLIFY_BOOLEAN_NODE_H namespace CVC4 { @@ -24,4 +24,4 @@ Node simplifyBooleanNode(const Node &n); }/* CVC4 namespace */ -#endif /* __CVC4__SIMPLIFY_BOOLEAN_NODE_H */ +#endif /* CVC4__SIMPLIFY_BOOLEAN_NODE_H */ diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h index 54b30e6f0..cb23268f3 100644 --- a/src/proof/skolemization_manager.h +++ b/src/proof/skolemization_manager.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__SKOLEMIZATION_MANAGER_H -#define __CVC4__SKOLEMIZATION_MANAGER_H +#ifndef CVC4__SKOLEMIZATION_MANAGER_H +#define CVC4__SKOLEMIZATION_MANAGER_H #include <iostream> #include <unordered_map> @@ -52,4 +52,4 @@ private: -#endif /* __CVC4__SKOLEMIZATION_MANAGER_H */ +#endif /* CVC4__SKOLEMIZATION_MANAGER_H */ diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 94765d95a..b487b62a8 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY_PROOF_H -#define __CVC4__THEORY_PROOF_H +#ifndef CVC4__THEORY_PROOF_H +#define CVC4__THEORY_PROOF_H #include <iosfwd> #include <unordered_map> @@ -401,4 +401,4 @@ public: } /* CVC4 namespace */ -#endif /* __CVC4__THEORY_PROOF_H */ +#endif /* CVC4__THEORY_PROOF_H */ diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index e5fd396c5..ca8b3f90e 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__UF__PROOF_H -#define __CVC4__UF__PROOF_H +#ifndef CVC4__UF__PROOF_H +#define CVC4__UF__PROOF_H #include <memory> #include <unordered_set> @@ -102,4 +102,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__UF__PROOF_H */ +#endif /* CVC4__UF__PROOF_H */ diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h index 6e0c84840..0217b6326 100644 --- a/src/proof/unsat_core.h +++ b/src/proof/unsat_core.h @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__UNSAT_CORE_H -#define __CVC4__UNSAT_CORE_H +#ifndef CVC4__UNSAT_CORE_H +#define CVC4__UNSAT_CORE_H #include <iosfwd> #include <vector> @@ -71,4 +71,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__UNSAT_CORE_H */ +#endif /* CVC4__UNSAT_CORE_H */ |