diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-09 17:22:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 17:22:07 -0700 |
commit | f87f038c5f0821d0fefb01cea00bfdec6004da91 (patch) | |
tree | d948178e1c0d2dc459a976f0d187d2d41a5437c0 /src/prop | |
parent | 550c49a7dd2b13ea29743458336f0c0a0fb6099a (diff) |
Rename CVC4_ macros to CVC5_. (#6327)
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 2 | ||||
-rw-r--r-- | src/prop/cadical.cpp | 4 | ||||
-rw-r--r-- | src/prop/cadical.h | 4 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 2 | ||||
-rw-r--r-- | src/prop/cryptominisat.cpp | 2 | ||||
-rw-r--r-- | src/prop/cryptominisat.h | 4 | ||||
-rw-r--r-- | src/prop/kissat.cpp | 4 | ||||
-rw-r--r-- | src/prop/kissat.h | 4 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 9 | ||||
-rw-r--r-- | src/prop/proof_cnf_stream.cpp | 2 | ||||
-rw-r--r-- | src/prop/sat_proof_manager.cpp | 4 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 6 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 2 |
13 files changed, 25 insertions, 24 deletions
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 96ab5b526..e399fac4c 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -166,7 +166,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i]))); #endif diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index cac015904..5abdada71 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -16,7 +16,7 @@ #include "prop/cadical.h" -#ifdef CVC4_USE_CADICAL +#ifdef CVC5_USE_CADICAL #include "base/check.h" @@ -202,4 +202,4 @@ CadicalSolver::Statistics::~Statistics() { } // namespace prop } // namespace cvc5 -#endif // CVC4_USE_CADICAL +#endif // CVC5_USE_CADICAL diff --git a/src/prop/cadical.h b/src/prop/cadical.h index ed4c166d4..e8a36d0a0 100644 --- a/src/prop/cadical.h +++ b/src/prop/cadical.h @@ -19,7 +19,7 @@ #ifndef CVC5__PROP__CADICAL_H #define CVC5__PROP__CADICAL_H -#ifdef CVC4_USE_CADICAL +#ifdef CVC5_USE_CADICAL #include "prop/sat_solver.h" #include "util/stats_timer.h" @@ -105,5 +105,5 @@ class CadicalSolver : public SatSolver } // namespace prop } // namespace cvc5 -#endif // CVC4_USE_CADICAL +#endif // CVC5_USE_CADICAL #endif // CVC5__PROP__CADICAL_H diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 10c84f582..111c6c2df 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -772,7 +772,7 @@ void CnfStream::convertAndAssert(TNode node, bool negated) convertAndAssertIff(node, negated); break; } - CVC4_FALLTHROUGH; + CVC5_FALLTHROUGH; default: { Node nnode = node; diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index ce5e4e2b0..5e0b056dc 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -14,7 +14,7 @@ ** Implementation of the cryptominisat for cvc4 (bitvectors). **/ -#ifdef CVC4_USE_CRYPTOMINISAT +#ifdef CVC5_USE_CRYPTOMINISAT #include "prop/cryptominisat.h" diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index ceed47d79..b217cee9c 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -19,7 +19,7 @@ #ifndef CVC5__PROP__CRYPTOMINISAT_H #define CVC5__PROP__CRYPTOMINISAT_H -#ifdef CVC4_USE_CRYPTOMINISAT +#ifdef CVC5_USE_CRYPTOMINISAT #include "prop/sat_solver.h" #include "util/stats_timer.h" @@ -108,5 +108,5 @@ class CryptoMinisatSolver : public SatSolver } // namespace prop } // namespace cvc5 -#endif // CVC4_USE_CRYPTOMINISAT +#endif // CVC5_USE_CRYPTOMINISAT #endif // CVC5__PROP__CRYPTOMINISAT_H diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp index 10b7b07de..949af2901 100644 --- a/src/prop/kissat.cpp +++ b/src/prop/kissat.cpp @@ -16,7 +16,7 @@ #include "prop/kissat.h" -#ifdef CVC4_USE_KISSAT +#ifdef CVC5_USE_KISSAT #include "base/check.h" @@ -175,4 +175,4 @@ KissatSolver::Statistics::~Statistics() } // namespace prop } // namespace cvc5 -#endif // CVC4_USE_KISSAT +#endif // CVC5_USE_KISSAT diff --git a/src/prop/kissat.h b/src/prop/kissat.h index 2ab38dbab..b2bc8e074 100644 --- a/src/prop/kissat.h +++ b/src/prop/kissat.h @@ -19,7 +19,7 @@ #ifndef CVC5__PROP__KISSAT_H #define CVC5__PROP__KISSAT_H -#ifdef CVC4_USE_KISSAT +#ifdef CVC5_USE_KISSAT #include "prop/sat_solver.h" #include "util/stats_timer.h" @@ -99,5 +99,5 @@ class KissatSolver : public SatSolver } // namespace prop } // namespace cvc5 -#endif // CVC4_USE_KISSAT +#endif // CVC5_USE_KISSAT #endif // CVC5__PROP__KISSAT_H diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index e29c1032a..e8179c5fe 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -172,10 +172,11 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) { -#ifdef CVC4_ASSERTIONS - if (use_simplification) { - for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i]))); - } +#ifdef CVC5_ASSERTIONS + if (use_simplification) + { + for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i]))); + } #endif int nclauses = clauses_persistent.size(); diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 76421db9b..8527950ce 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -127,7 +127,7 @@ void ProofCnfStream::convertAndAssert(TNode node, bool negated) convertAndAssertIff(node, negated); break; } - CVC4_FALLTHROUGH; + CVC5_FALLTHROUGH; default: { // negate diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 0d075de45..ec29d6bd5 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -352,7 +352,7 @@ void SatProofManager::explainLit( printClause(reason); Trace("sat-proof") << "\n"; } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS // pedantically check that the negation of the literal to explain *does not* // occur in the reason, otherwise we will loop forever for (unsigned i = 0; i < size; ++i) @@ -372,7 +372,7 @@ void SatProofManager::explainLit( Trace("sat-proof") << push; for (unsigned i = 0; i < size; ++i) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS // pedantically make sure that the reason stays the same const Minisat::Clause& reloadedReason = d_solver->ca[reasonRef]; AlwaysAssert(size == static_cast<unsigned>(reloadedReason.size())); diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 117210431..90eec9153 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -42,7 +42,7 @@ MinisatSatSolver* SatSolverFactory::createCDCLTMinisat( SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry, const std::string& name) { -#ifdef CVC4_USE_CRYPTOMINISAT +#ifdef CVC5_USE_CRYPTOMINISAT CryptoMinisatSolver* res = new CryptoMinisatSolver(registry, name); res->init(); return res; @@ -54,7 +54,7 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry, SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry, const std::string& name) { -#ifdef CVC4_USE_CADICAL +#ifdef CVC5_USE_CADICAL CadicalSolver* res = new CadicalSolver(registry, name); res->init(); return res; @@ -66,7 +66,7 @@ SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry, SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry, const std::string& name) { -#ifdef CVC4_USE_KISSAT +#ifdef CVC5_USE_KISSAT KissatSolver* res = new KissatSolver(registry, name); res->init(); return res; diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 503b37ed7..e4924ded4 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -21,7 +21,7 @@ // 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 CVC5_USE_MINISAT #include <unordered_set> |