From ffdf7434ba53191546e13663764894852e8bc6dd Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 14 Jul 2021 18:27:33 -0700 Subject: [PATCH] bv: Rename simple solver to bitblast-internal. (#6888) --- src/CMakeLists.txt | 4 +-- src/options/bv_options.toml | 6 ++-- ...le.cpp => bv_solver_bitblast_internal.cpp} | 31 ++++++++++--------- ...simple.h => bv_solver_bitblast_internal.h} | 24 +++++++------- src/theory/bv/theory_bv.cpp | 11 ++++--- src/theory/inference_id.cpp | 6 ++-- src/theory/inference_id.h | 4 +-- test/regress/regress0/bv/ackermann1.smt2 | 2 +- test/regress/regress0/bv/bool-model.smt2 | 2 +- test/regress/regress0/bv/bool-to-bv-ite.smt2 | 2 +- test/regress/regress0/bv/bug734.smt2 | 2 +- test/regress/regress0/bv/issue-4076.smt2 | 2 +- .../regress0/bv/pr4993-bvugt-bvurem-b.smt2 | 2 +- .../proofs/open-pf-if-unordered-iff.smt2 | 2 +- .../regress0/proofs/open-pf-rederivation.smt2 | 2 +- test/regress/regress1/bug520.smt2 | 2 +- 16 files changed, 54 insertions(+), 50 deletions(-) rename src/theory/bv/{bv_solver_simple.cpp => bv_solver_bitblast_internal.cpp} (77%) rename src/theory/bv/{bv_solver_simple.h => bv_solver_bitblast_internal.h} (75%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e001dd462..8dc1f986f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -589,10 +589,10 @@ libcvc5_add_sources( theory/bv/bv_solver.h theory/bv/bv_solver_bitblast.cpp theory/bv/bv_solver_bitblast.h + theory/bv/bv_solver_bitblast_internal.cpp + theory/bv/bv_solver_bitblast_internal.h theory/bv/bv_solver_lazy.cpp theory/bv/bv_solver_lazy.h - theory/bv/bv_solver_simple.cpp - theory/bv/bv_solver_simple.h theory/bv/bv_subtheory.h theory/bv/bv_subtheory_algebraic.cpp theory/bv/bv_subtheory_algebraic.h diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 8d4c2b1de..3faf9a111 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -220,9 +220,9 @@ name = "Bitvector Theory" [[option.mode.LAZY]] name = "lazy" help = "Enables the lazy BV solver infrastructure." -[[option.mode.SIMPLE]] - name = "simple" - help = "Enables simple bitblasting solver with proof support." +[[option.mode.BITBLAST_INTERNAL]] + name = "bitblast-internal" + help = "Enables bitblasting to internal SAT solver with proof support." [[option]] name = "bvAssertInput" diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp similarity index 77% rename from src/theory/bv/bv_solver_simple.cpp rename to src/theory/bv/bv_solver_bitblast_internal.cpp index 414de41ce..bd47cc45e 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_bitblast_internal.cpp @@ -10,10 +10,11 @@ * directory for licensing information. * **************************************************************************** * - * Simple bit-blast solver that sends bitblast lemmas directly to MiniSat. + * Bit-blast solver that sends bit-blast lemmas directly to the internal + * MiniSat. */ -#include "theory/bv/bv_solver_simple.h" +#include "theory/bv/bv_solver_bitblast_internal.h" #include "proof/conv_proof_generator.h" #include "theory/bv/theory_bv.h" @@ -66,16 +67,15 @@ void collectBVAtoms(TNode n, std::unordered_set& atoms) } // namespace -BVSolverSimple::BVSolverSimple(TheoryState* s, - TheoryInferenceManager& inferMgr, - ProofNodeManager* pnm) +BVSolverBitblastInternal::BVSolverBitblastInternal( + TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) : BVSolver(*s, inferMgr), d_pnm(pnm), d_bitblaster(new BBProof(s, pnm, false)) { } -void BVSolverSimple::addBBLemma(TNode fact) +void BVSolverBitblastInternal::addBBLemma(TNode fact) { if (!d_bitblaster->hasBBAtom(fact)) { @@ -88,17 +88,17 @@ void BVSolverSimple::addBBLemma(TNode fact) if (d_pnm == nullptr) { - d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA); + d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA); } else { TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator()); - d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_LEMMA); + d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA); } } -bool BVSolverSimple::preNotifyFact( +bool BVSolverBitblastInternal::preNotifyFact( TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) { if (fact.getKind() == kind::NOT) @@ -119,7 +119,7 @@ bool BVSolverSimple::preNotifyFact( if (d_pnm == nullptr) { - d_im.lemma(lemma, InferenceId::BV_SIMPLE_LEMMA); + d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA); } else { @@ -127,7 +127,7 @@ bool BVSolverSimple::preNotifyFact( fact, n, PfRule::BV_EAGER_ATOM, {}, {fact}); TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator()); - d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA); + d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA); } std::unordered_set bv_atoms; @@ -141,13 +141,16 @@ bool BVSolverSimple::preNotifyFact( return true; } -bool BVSolverSimple::collectModelValues(TheoryModel* m, - const std::set& termSet) +bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m, + const std::set& termSet) { return d_bitblaster->collectModelValues(m, termSet); } -BVProofRuleChecker* BVSolverSimple::getProofChecker() { return &d_checker; } +BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker() +{ + return &d_checker; +} } // namespace bv } // namespace theory diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_bitblast_internal.h similarity index 75% rename from src/theory/bv/bv_solver_simple.h rename to src/theory/bv/bv_solver_bitblast_internal.h index 0af4f5b89..8a1886084 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_bitblast_internal.h @@ -10,39 +10,37 @@ * directory for licensing information. * **************************************************************************** * - * Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat. + * Bit-blast solver that sends bit-blast lemmas directly to the internal + * MiniSat. */ #include "cvc5_private.h" -#ifndef CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H -#define CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H +#ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H +#define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H #include "theory/bv/bitblast/proof_bitblaster.h" #include "theory/bv/bv_solver.h" #include "theory/bv/proof_checker.h" namespace cvc5 { - -class TConvProofGenerator; - namespace theory { namespace bv { /** - * Simple bit-blasting solver that sends bit-blasting lemmas directly to the + * Bit-blasting solver that sends bit-blasting lemmas directly to the * internal MiniSat. It is also ablo to handle atoms of kind * BITVECTOR_EAGER_ATOM. * * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact(). */ -class BVSolverSimple : public BVSolver +class BVSolverBitblastInternal : public BVSolver { public: - BVSolverSimple(TheoryState* state, - TheoryInferenceManager& inferMgr, - ProofNodeManager* pnm); - ~BVSolverSimple() = default; + BVSolverBitblastInternal(TheoryState* state, + TheoryInferenceManager& inferMgr, + ProofNodeManager* pnm); + ~BVSolverBitblastInternal() = default; void preRegisterTerm(TNode n) override {} @@ -52,7 +50,7 @@ class BVSolverSimple : public BVSolver bool isPrereg, bool isInternal) override; - std::string identify() const override { return "BVSolverSimple"; }; + std::string identify() const override { return "BVSolverBitblastInternal"; }; bool collectModelValues(TheoryModel* m, const std::set& termSet) override; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 3d7f11f6d..b3cf6da59 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -20,8 +20,8 @@ #include "proof/proof_checker.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/bv_solver_bitblast.h" +#include "theory/bv/bv_solver_bitblast_internal.h" #include "theory/bv/bv_solver_lazy.h" -#include "theory/bv/bv_solver_simple.h" #include "theory/bv/theory_bv_utils.h" #include "theory/ee_setup_info.h" #include "theory/trust_substitutions.h" @@ -56,8 +56,8 @@ TheoryBV::TheoryBV(context::Context* c, break; default: - AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE); - d_internal.reset(new BVSolverSimple(&d_state, d_im, pnm)); + AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL); + d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, pnm)); } d_theoryState = &d_state; d_inferManager = &d_im; @@ -69,9 +69,10 @@ TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; } ProofRuleChecker* TheoryBV::getProofChecker() { - if (options::bvSolver() == options::BVSolver::SIMPLE) + if (options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL) { - return static_cast(d_internal.get())->getProofChecker(); + return static_cast(d_internal.get()) + ->getProofChecker(); } return nullptr; } diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 0ef0ad6bd..612c99d82 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -112,8 +112,10 @@ const char* toString(InferenceId i) case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT"; case InferenceId::BV_LAZY_CONFLICT: return "BV_LAZY_CONFLICT"; case InferenceId::BV_LAZY_LEMMA: return "BV_LAZY_LEMMA"; - case InferenceId::BV_SIMPLE_LEMMA: return "BV_SIMPLE_LEMMA"; - case InferenceId::BV_SIMPLE_BITBLAST_LEMMA: return "BV_SIMPLE_BITBLAST_LEMMA"; + case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA: + return "BV_BITBLAST_EAGER_LEMMA"; + case InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA: + return "BV_BITBLAST_INTERNAL_BITBLAST_LEMMA"; case InferenceId::BV_EXTF_LEMMA: return "BV_EXTF_LEMMA"; case InferenceId::BV_EXTF_COLLAPSE: return "BV_EXTF_COLLAPSE"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index ba268b396..ebbccfd54 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -175,8 +175,8 @@ enum class InferenceId BV_BITBLAST_CONFLICT, BV_LAZY_CONFLICT, BV_LAZY_LEMMA, - BV_SIMPLE_LEMMA, - BV_SIMPLE_BITBLAST_LEMMA, + BV_BITBLAST_INTERNAL_EAGER_LEMMA, + BV_BITBLAST_INTERNAL_BITBLAST_LEMMA, BV_EXTF_LEMMA, BV_EXTF_COLLAPSE, // ---------------------------------- end bitvector theory diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2 index 579e438a5..f70dc4a3d 100644 --- a/test/regress/regress0/bv/ackermann1.smt2 +++ b/test/regress/regress0/bv/ackermann1.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --bitblast=eager --no-check-models -; COMMAND-LINE: --bitblast=eager --bv-solver=simple --no-check-models +; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal --no-check-models ; EXPECT: sat (set-logic QF_UFBV) (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress0/bv/bool-model.smt2 b/test/regress/regress0/bv/bool-model.smt2 index f30dbef6f..2a2998b35 100644 --- a/test/regress/regress0/bv/bool-model.smt2 +++ b/test/regress/regress0/bv/bool-model.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --bitblast=eager -; COMMAND-LINE: --bitblast=eager --bv-solver=simple +; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal (set-info :status sat) (set-logic QF_BV) (declare-fun x () Bool) diff --git a/test/regress/regress0/bv/bool-to-bv-ite.smt2 b/test/regress/regress0/bv/bool-to-bv-ite.smt2 index de0ec8897..09fcb4e11 100644 --- a/test/regress/regress0/bv/bool-to-bv-ite.smt2 +++ b/test/regress/regress0/bv/bool-to-bv-ite.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --bool-to-bv=ite -; COMMAND-LINE: --bool-to-bv=ite --bv-solver=simple +; COMMAND-LINE: --bool-to-bv=ite --bv-solver=bitblast-internal ; EXPECT: sat (set-logic QF_BV) (declare-fun x2 () (_ BitVec 3)) diff --git a/test/regress/regress0/bv/bug734.smt2 b/test/regress/regress0/bv/bug734.smt2 index 5e92036ec..0e392d3c6 100644 --- a/test/regress/regress0/bv/bug734.smt2 +++ b/test/regress/regress0/bv/bug734.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --incremental -; COMMAND-LINE: --incremental --bv-solver=simple +; COMMAND-LINE: --incremental --bv-solver=bitblast-internal ; EXPECT: sat ; EXPECT: sat (set-logic QF_BV) diff --git a/test/regress/regress0/bv/issue-4076.smt2 b/test/regress/regress0/bv/issue-4076.smt2 index e94779439..12bc3e4ca 100644 --- a/test/regress/regress0/bv/issue-4076.smt2 +++ b/test/regress/regress0/bv/issue-4076.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --incremental -; COMMAND-LINE: --incremental --bv-solver=simple +; COMMAND-LINE: --incremental --bv-solver=bitblast-internal ; EXPECT: sat ; EXPECT: sat (set-logic ALL) diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 index 0c6e7e0eb..2a924dac8 100644 --- a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 +++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: -; COMMAND-LINE: --bv-solver=simple +; COMMAND-LINE: --bv-solver=bitblast-internal (set-logic QF_BV) (set-info :status unsat) (declare-const x (_ BitVec 4)) diff --git a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 index 98d75d74f..8cb717258 100644 --- a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 +++ b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-solver=simple +; COMMAND-LINE: --bv-solver=bitblast-internal ; EXPECT: unsat (set-logic ALL) (declare-const __ (_ BitVec 3)) diff --git a/test/regress/regress0/proofs/open-pf-rederivation.smt2 b/test/regress/regress0/proofs/open-pf-rederivation.smt2 index 7095ec942..877389184 100644 --- a/test/regress/regress0/proofs/open-pf-rederivation.smt2 +++ b/test/regress/regress0/proofs/open-pf-rederivation.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-solver=simple +; COMMAND-LINE: --bv-solver=bitblast-internal ; EXPECT: unsat (set-logic ALL) (declare-const __ (_ BitVec 7)) diff --git a/test/regress/regress1/bug520.smt2 b/test/regress/regress1/bug520.smt2 index cfafc0a0a..238fec914 100644 --- a/test/regress/regress1/bug520.smt2 +++ b/test/regress/regress1/bug520.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --bitblast=lazy ; COMMAND-LINE: --bitblast=eager --no-check-models -; COMMAND-LINE: --bv-solver=simple +; COMMAND-LINE: --bv-solver=bitblast-internal ; EXPECT: sat ; Automatically generated by SBV. Do not edit. (set-logic QF_UFBV) -- 2.30.2