diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-04 14:07:16 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-04 22:07:16 +0000 |
commit | faaf466a661ff3c8d7b80dd7614a2fae68016d92 (patch) | |
tree | ecbfed56f09166822436713c5f7dc85f13cdca83 /src | |
parent | 4180569420806f06fdfd7b9ab24f4d3d7724959e (diff) |
Add initial bit-blaster for proof logging. (#6053)
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
Diffstat (limited to 'src')
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/proof_bitblaster.cpp | 87 | ||||
-rw-r--r-- | src/theory/bv/bitblast/proof_bitblaster.h | 51 | ||||
-rw-r--r-- | src/theory/bv/bitblast/simple_bitblaster.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_simple.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_simple.h | 4 |
6 files changed, 144 insertions, 4 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2b04bb40d..c438d9a4f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -516,6 +516,8 @@ libcvc4_add_sources( theory/bv/bitblast/eager_bitblaster.h theory/bv/bitblast/lazy_bitblaster.cpp theory/bv/bitblast/lazy_bitblaster.h + theory/bv/bitblast/proof_bitblaster.cpp + theory/bv/bitblast/proof_bitblaster.h theory/bv/bitblast/simple_bitblaster.cpp theory/bv/bitblast/simple_bitblaster.h theory/bv/bv_eager_solver.cpp diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp new file mode 100644 index 000000000..257107f52 --- /dev/null +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -0,0 +1,87 @@ +/********************* */ +/*! \file proof_bitblaster.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A bit-blaster wrapper around BBSimple for proof logging. + **/ +#include "theory/bv/bitblast/proof_bitblaster.h" + +#include <unordered_set> + +#include "theory/theory_model.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +BBProof::BBProof(TheoryState* state) : d_bb(new BBSimple(state)) {} + +void BBProof::bbAtom(TNode node) +{ + std::vector<TNode> visit; + visit.push_back(node); + std::unordered_set<TNode, TNodeHashFunction> visited; + while (!visit.empty()) + { + TNode n = visit.back(); + if (hasBBAtom(n) || hasBBTerm(n)) + { + visit.pop_back(); + continue; + } + + if (visited.find(n) == visited.end()) + { + visited.insert(n); + if (!Theory::isLeafOf(n, theory::THEORY_BV)) + { + visit.insert(visit.end(), n.begin(), n.end()); + } + } + else + { + if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst()) + { + // unused for now, will be needed for proof logging + Bits bits; + d_bb->makeVariable(n, bits); + } + else if (n.getType().isBitVector()) + { + Bits bits; + d_bb->bbTerm(n, bits); + } + else + { + d_bb->bbAtom(n); + } + visit.pop_back(); + } + } +} + +bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); } + +bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); } + +Node BBProof::getStoredBBAtom(TNode node) +{ + return d_bb->getStoredBBAtom(node); +} + +bool BBProof::collectModelValues(TheoryModel* m, + const std::set<Node>& relevantTerms) +{ + return d_bb->collectModelValues(m, relevantTerms); +} + +} // namespace bv +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h new file mode 100644 index 000000000..af9ca2550 --- /dev/null +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -0,0 +1,51 @@ +/********************* */ +/*! \file proof_bitblaster.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A bit-blaster wrapper around BBSimple for proof logging. + **/ +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H +#define CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H + +#include "theory/bv/bitblast/simple_bitblaster.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +class BBProof +{ + using Bits = std::vector<Node>; + + public: + BBProof(TheoryState* state); + ~BBProof() = default; + + /** Bit-blast atom 'node'. */ + void bbAtom(TNode node); + /** Check if atom was already bit-blasted. */ + bool hasBBAtom(TNode atom) const; + /** Check if term was already bit-blasted. */ + bool hasBBTerm(TNode node) const; + /** Get bit-blasted node stored for atom. */ + Node getStoredBBAtom(TNode node); + /** Collect model values for all relevant terms given in 'relevantTerms'. */ + bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms); + + private: + std::unique_ptr<BBSimple> d_bb; +}; + +} // namespace bv +} // namespace theory +} // namespace CVC4 +#endif diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h index 72a2fb0d8..8c8a5fe09 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.h +++ b/src/theory/bv/bitblast/simple_bitblaster.h @@ -17,7 +17,7 @@ #ifndef CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H #define CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H -#include "theory/bv/bitblast/lazy_bitblaster.h" +#include "theory/bv/bitblast/bitblaster.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index 58be5d826..1c698d686 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -70,7 +70,7 @@ BVSolverSimple::BVSolverSimple(TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) : BVSolver(*s, inferMgr), - d_bitblaster(new BBSimple(s)), + d_bitblaster(new BBProof(s)), d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "") : nullptr) { diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h index 17066e536..efd53436b 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -21,7 +21,7 @@ #include <unordered_map> -#include "theory/bv/bitblast/simple_bitblaster.h" +#include "theory/bv/bitblast/proof_bitblaster.h" #include "theory/bv/bv_solver.h" #include "theory/bv/proof_checker.h" #include "theory/eager_proof_generator.h" @@ -73,7 +73,7 @@ class BVSolverSimple : public BVSolver void addBBLemma(TNode fact); /** Bit-blaster used to bit-blast atoms/terms. */ - std::unique_ptr<BBSimple> d_bitblaster; + std::unique_ptr<BBProof> d_bitblaster; /** Proof generator that manages proofs for lemmas generated by this class. */ std::unique_ptr<EagerProofGenerator> d_epg; |