This commit refactors the proof bit-blaster to properly track the pre- and post-rewrites in bbAtom(). The individual bit-blast steps are recorded in a term conversion proof generator. The overall bit-blast proof is stored in a BitblastProofGenerator, which tracks the pre- and post-rewrite and includes the bit-blast proof of the TCPG.
theory/bv/abstraction.h
theory/bv/bitblast/aig_bitblaster.cpp
theory/bv/bitblast/aig_bitblaster.h
+ theory/bv/bitblast/bitblast_proof_generator.cpp
+ theory/bv/bitblast/bitblast_proof_generator.h
theory/bv/bitblast/bitblast_strategies_template.h
theory/bv/bitblast/bitblast_utils.h
theory/bv/bitblast/bitblaster.h
#include "smt/smt_engine.h"
#include "theory/arith/arith_utilities.h"
#include "theory/builtin/proof_checker.h"
+#include "theory/bv/bitblast/bitblast_proof_generator.h"
#include "theory/bv/bitblast/proof_bitblaster.h"
#include "theory/rewriter.h"
#include "theory/strings/infer_proof_cons.h"
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mathias Preiner
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * Bitblast proof generator for generating bit-blast proof steps.
+ */
+#include "theory/bv/bitblast/bitblast_proof_generator.h"
+
+#include "proof/conv_proof_generator.h"
+#include "theory/rewriter.h"
+
+namespace cvc5 {
+namespace theory {
+namespace bv {
+
+BitblastProofGenerator::BitblastProofGenerator(ProofNodeManager* pnm,
+ TConvProofGenerator* tcpg)
+ : d_pnm(pnm), d_tcpg(tcpg)
+{
+}
+
+std::shared_ptr<ProofNode> BitblastProofGenerator::getProofFor(Node eq)
+{
+ const auto& [t, bbt] = d_cache.at(eq);
+
+ CDProof cdp(d_pnm);
+ /* Coarse-grained bit-blast step. */
+ if (t.isNull())
+ {
+ cdp.addStep(eq, PfRule::BV_BITBLAST, {}, {eq});
+ }
+ else
+ {
+ /* Fine-grained bit-blast step for bit-blasting bit-vector atoms (bbAtom()).
+ * Bit-blasting atoms involves three steps:
+ *
+ * 1) pre-rewrite: rewrite atom
+ * 2) bit-blast rewritten atom
+ * 3) post-rewrite: rewrite bit-blasted atom
+ *
+ * The CDProof is used for constructing the following proof of
+ * transitivity:
+ *
+ * --------- RW ----------- BB ------------- RW
+ * t = rwt rwt = bbt bbt = rwbbt
+ * ---------------------------------------------- TRANS
+ * t = rwbbt
+ *
+ *
+ * where BB corresponds to the conversion proof PI_1 and a bit-blasting
+ * step. Note that if t and bbt remain the same after rewriting the
+ * transitivity proof is not needed.
+ *
+ * The full proof tree is as follows:
+ *
+ * ------------------- RW ------------------ BB ------------ RW
+ * P(x,y) = P(x',y') PI_1 P(x'',y'') = bbt bbt = rwbbt
+ * ------------------------------------------------------------------ TRANS
+ * P(x,y) = rwbbt
+ *
+ *
+ * PI_1 := -------- BB* ---------- BB*
+ * x' = x'' y' = y''
+ * ----------------------- CONG
+ * P(x',y') = P(x'',y'')
+ *
+ *
+ * where P is an arbitrary bit-vector atom and t := P(x,y), rwt := P(x',y').
+ * BB* corresponds to recursively applying bit-blasting to all the
+ * sub-terms and recording these bit-blast steps in the conversion proof.
+ */
+
+ Node rwt = Rewriter::rewrite(t);
+
+ std::vector<Node> transSteps;
+
+ // Record pre-rewrite of bit-vector atom.
+ if (t != rwt)
+ {
+ cdp.addStep(t.eqNode(rwt), PfRule::REWRITE, {}, {t});
+ transSteps.push_back(t.eqNode(rwt));
+ }
+
+ // Add bit-blast proof from conversion generator.
+ cdp.addProof(d_tcpg->getProofFor(rwt.eqNode(bbt)));
+ transSteps.push_back(rwt.eqNode(bbt));
+
+ // Record post-rewrite of bit-blasted term.
+ Node rwbbt = Rewriter::rewrite(bbt);
+ if (bbt != rwbbt)
+ {
+ cdp.addStep(bbt.eqNode(rwbbt), PfRule::REWRITE, {}, {bbt});
+ transSteps.push_back(bbt.eqNode(rwbbt));
+ }
+
+ // If pre- and post-rewrite did not apply, no rewrite steps need to be
+ // recorded and the given equality `eq` is already justified by the proof
+ // given by the conversion proof generator.
+ if (transSteps.size() > 1)
+ {
+ cdp.addStep(eq, PfRule::TRANS, transSteps, {});
+ }
+ }
+
+ return cdp.getProofFor(eq);
+}
+
+void BitblastProofGenerator::addBitblastStep(TNode t, TNode bbt, TNode eq)
+{
+ d_cache.emplace(eq, std::make_tuple(t, bbt));
+}
+
+} // namespace bv
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mathias Preiner
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * Bitblast proof generator for generating bit-blast proof steps.
+ */
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_PROOF_GENERATOR_H
+#define CVC5__THEORY__BV__BITBLAST__BITBLAST_PROOF_GENERATOR_H
+
+#include "proof/proof_generator.h"
+#include "proof/proof_node_manager.h"
+
+namespace cvc5 {
+
+class TConvProofGenerator;
+
+namespace theory {
+namespace bv {
+
+/** Proof generator fot bit-blast proofs. */
+class BitblastProofGenerator : public ProofGenerator
+{
+ public:
+ BitblastProofGenerator(ProofNodeManager* pnm, TConvProofGenerator* tcpg);
+ ~BitblastProofGenerator(){};
+
+ /**
+ * Get proof for, which expects an equality of the form t = bb(t).
+ * This returns a proof based on the term conversion proof generator utility.
+ */
+ std::shared_ptr<ProofNode> getProofFor(Node eq) override;
+
+ std::string identify() const override { return "BitblastStepProofGenerator"; }
+
+ /**
+ * Record bit-blast step for bit-vector atom t.
+ *
+ * @param t Bit-vector atom
+ * @param bbt The bit-blasted term obtained from bit-blasting t without
+ * applying any rewriting.
+ * @param eq The equality that needs to be justified,
+ * i.e.,t = rewrite(bb(rewrite(t)))
+ */
+ void addBitblastStep(TNode t, TNode bbt, TNode eq);
+
+ private:
+ /** The associated proof node manager. */
+ ProofNodeManager* d_pnm;
+ /**
+ * The associated term conversion proof generator, which tracks the
+ * individual bit-blast steps.
+ */
+ TConvProofGenerator* d_tcpg;
+
+ /**
+ * Cache that maps equalities to information required to reconstruct the
+ * proof for given equality.
+ */
+ std::unordered_map<Node, std::tuple<Node, Node>> d_cache;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace cvc5
+#endif
return;
}
+ /* Note: We rewrite here since it's not guaranteed (yet) that facts sent
+ * to theories are rewritten.
+ */
Node normalized = rewrite(node);
Node atom_bb =
normalized.getKind() != kind::CONST_BOOLEAN
return d_variables.find(node) != d_variables.end();
}
+Node NodeBitblaster::applyAtomBBStrategy(TNode node)
+{
+ Assert(node.getKind() != kind::CONST_BOOLEAN);
+ Assert(node.getKind() != kind::BITVECTOR_BITOF);
+ return d_atomBBStrategies[node.getKind()](node, this);
+}
+
} // namespace bv
} // namespace theory
} // namespace cvc5
/** Checks whether node is a variable introduced via `makeVariable`.*/
bool isVariable(TNode node);
+ /**
+ * Bit-blast `node` and return the result without applying any rewrites.
+ *
+ * This method is used by BBProof and does not cache the result for `node`.
+ */
+ Node applyAtomBBStrategy(TNode node);
+
private:
/** Query SAT solver for assignment of node 'a'. */
Node getModelFromSatSolver(TNode a, bool fullModel) override;
#include <unordered_set>
#include "proof/conv_proof_generator.h"
+#include "theory/bv/bitblast/bitblast_proof_generator.h"
#include "theory/theory_model.h"
namespace cvc5 {
d_tcontext.get(),
false)
: nullptr),
+ d_bbpg(pnm ? new BitblastProofGenerator(pnm, d_tcpg.get()) : nullptr),
d_recordFineGrainedProofs(fineGrained)
{
}
void BBProof::bbAtom(TNode node)
{
- std::vector<TNode> visit;
- visit.push_back(node);
- std::unordered_set<TNode> visited;
-
- bool fpenabled = isProofsEnabled() && d_recordFineGrainedProofs;
-
- NodeManager* nm = NodeManager::currentNM();
-
- while (!visit.empty())
+ bool fineProofs = isProofsEnabled() && d_recordFineGrainedProofs;
+
+ /* Bit-blasting bit-vector atoms consists of 3 steps:
+ * 1. rewrite the atom
+ * 2. bit-blast the rewritten atom
+ * 3. rewrite the resulting bit-blasted term
+ *
+ * This happens in a single call to d_bb->bbAtom(...). When we record
+ * fine-grained proofs, we explicitly record the above 3 steps.
+ *
+ * Note: The below post-order traversal corresponds to the recursive
+ * bit-blasting of bit-vector terms that happens implicitly when calling the
+ * corresponding bit-blasting strategy in d_bb->bbAtom(...).
+ */
+ if (fineProofs)
{
- TNode n = visit.back();
- if (hasBBAtom(n) || hasBBTerm(n))
- {
- visit.pop_back();
- continue;
- }
+ std::vector<TNode> visit;
+ std::unordered_set<TNode> visited;
+ NodeManager* nm = NodeManager::currentNM();
+
+ // post-rewrite atom
+ Node rwNode = Rewriter::rewrite(node);
- if (visited.find(n) == visited.end())
+ // Post-order traversal of `rwNode` to make sure that all subterms are
+ // bit-blasted and recorded.
+ visit.push_back(rwNode);
+ while (!visit.empty())
{
- visited.insert(n);
- if (!Theory::isLeafOf(n, theory::THEORY_BV))
+ TNode n = visit.back();
+ if (hasBBAtom(n) || hasBBTerm(n))
{
- visit.insert(visit.end(), n.begin(), n.end());
+ visit.pop_back();
+ continue;
}
- }
- else
- {
- if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
+
+ if (visited.find(n) == visited.end())
{
- Bits bits;
- d_bb->makeVariable(n, bits);
- if (fpenabled)
+ visited.insert(n);
+ if (!Theory::isLeafOf(n, theory::THEORY_BV))
{
- Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
- d_bbMap.emplace(n, n_tobv);
- d_tcpg->addRewriteStep(n,
- n_tobv,
- PfRule::BV_BITBLAST_STEP,
- {},
- {n.eqNode(n_tobv)},
- false);
+ visit.insert(visit.end(), n.begin(), n.end());
}
}
- else if (n.getType().isBitVector())
+ else
{
- Bits bits;
- d_bb->bbTerm(n, bits);
- Kind kind = n.getKind();
- if (fpenabled)
+ /* Handle BV theory leafs as variables, i.e., apply the BITVECTOR_BITOF
+ * operator to each bit of `n`. */
+ if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
{
- Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
- d_bbMap.emplace(n, n_tobv);
- Node c_tobv;
+ Bits bits;
+ d_bb->makeVariable(n, bits);
+
+ Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
+ d_bbMap.emplace(n, bbt);
+ d_tcpg->addRewriteStep(
+ n, bbt, PfRule::BV_BITBLAST_STEP, {}, {n.eqNode(bbt)});
+ }
+ else if (n.getType().isBitVector())
+ {
+ Bits bits;
+ d_bb->bbTerm(n, bits);
+
+ Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
+ Node rbbt;
if (n.isConst())
{
- c_tobv = n;
+ d_bbMap.emplace(n, bbt);
+ rbbt = n;
}
else
{
- std::vector<Node> children_tobv;
- if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
- {
- children_tobv.push_back(n.getOperator());
- }
-
- for (const auto& child : n)
- {
- children_tobv.push_back(d_bbMap.at(child));
- }
- c_tobv = nm->mkNode(kind, children_tobv);
+ d_bbMap.emplace(n, bbt);
+ rbbt = reconstruct(n);
}
- d_tcpg->addRewriteStep(c_tobv,
- n_tobv,
- PfRule::BV_BITBLAST_STEP,
- {},
- {c_tobv.eqNode(n_tobv)},
- false);
+ d_tcpg->addRewriteStep(
+ rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
}
- }
- else
- {
- d_bb->bbAtom(n);
- if (fpenabled)
+ else
{
- Node n_tobv = getStoredBBAtom(n);
- std::vector<Node> children_tobv;
- for (const auto& child : n)
- {
- children_tobv.push_back(d_bbMap.at(child));
- }
- Node c_tobv = nm->mkNode(n.getKind(), children_tobv);
- d_tcpg->addRewriteStep(c_tobv,
- n_tobv,
- PfRule::BV_BITBLAST_STEP,
- {},
- {c_tobv.eqNode(n_tobv)},
- false);
+ Assert(n == rwNode);
}
+ visit.pop_back();
}
- visit.pop_back();
}
+
+ /* Bit-blast given rewritten bit-vector atom `node`.
+ * Note: This will pre and post-rewrite and store it in the bit-blasting
+ * cache. */
+ d_bb->bbAtom(node);
+ Node result = d_bb->getStoredBBAtom(node);
+
+ // Retrieve bit-blasted `rwNode` without post-rewrite.
+ Node bbt = rwNode.getKind() == kind::CONST_BOOLEAN
+ || rwNode.getKind() == kind::BITVECTOR_BITOF
+ ? rwNode
+ : d_bb->applyAtomBBStrategy(rwNode);
+
+ Node rbbt = reconstruct(rwNode);
+
+ d_tcpg->addRewriteStep(
+ rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
+
+ d_bbpg->addBitblastStep(node, bbt, node.eqNode(result));
+ }
+ else
+ {
+ d_bb->bbAtom(node);
+
+ /* Record coarse-grain bit-blast proof step. */
+ if (isProofsEnabled() && !d_recordFineGrainedProofs)
+ {
+ Node bbt = getStoredBBAtom(node);
+ d_bbpg->addBitblastStep(Node(), Node(), node.eqNode(bbt));
+ }
+ }
+}
+
+Node BBProof::reconstruct(TNode t)
+{
+ NodeManager* nm = NodeManager::currentNM();
+
+ std::vector<Node> children;
+ if (t.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ children.push_back(t.getOperator());
}
- /* Record coarse-grain bit-blast proof step. */
- if (isProofsEnabled() && !d_recordFineGrainedProofs)
+ for (const auto& child : t)
{
- Node node_tobv = getStoredBBAtom(node);
- d_tcpg->addRewriteStep(node,
- node_tobv,
- PfRule::BV_BITBLAST,
- {},
- {node.eqNode(node_tobv)},
- false);
+ children.push_back(d_bbMap.at(child));
}
+ return nm->mkNode(t.getKind(), children);
}
bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
return d_bb->collectModelValues(m, relevantTerms);
}
-TConvProofGenerator* BBProof::getProofGenerator() { return d_tcpg.get(); }
+BitblastProofGenerator* BBProof::getProofGenerator() { return d_bbpg.get(); }
bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
namespace theory {
namespace bv {
+class BitblastProofGenerator;
+
class BBProof : protected EnvObj
{
using Bits = std::vector<Node>;
/** Collect model values for all relevant terms given in 'relevantTerms'. */
bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
- TConvProofGenerator* getProofGenerator();
+ BitblastProofGenerator* getProofGenerator();
private:
/** Return true if proofs are enabled. */
bool isProofsEnabled() const;
+ /** Helper to reconstruct term `t` based on `d_bbMap`. */
+ Node reconstruct(TNode t);
+
/** The associated simple bit-blaster. */
std::unique_ptr<NodeBitblaster> d_bb;
/** The associated proof node manager. */
ProofNodeManager* d_pnm;
/** Term context for d_tcpg to not rewrite below BV leafs. */
std::unique_ptr<TermContext> d_tcontext;
- /** The associated term conversion proof generator. */
+ /** Term conversion proof generator for bit-blast steps. */
std::unique_ptr<TConvProofGenerator> d_tcpg;
+ /** Bitblast proof generator. */
+ std::unique_ptr<BitblastProofGenerator> d_bbpg;
/** Map bit-vector nodes to bit-blasted nodes. */
std::unordered_map<Node, Node> d_bbMap;
-
+ /** Flag to indicate whether fine-grained proofs should be recorded. */
bool d_recordFineGrainedProofs;
};
+
} // namespace bv
} // namespace theory
} // namespace cvc5
#include "theory/bv/bv_solver_bitblast_internal.h"
#include "proof/conv_proof_generator.h"
+#include "theory/bv/bitblast/bitblast_proof_generator.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"
ProofNodeManager* pnm)
: BVSolver(env, *s, inferMgr),
d_pnm(pnm),
- d_bitblaster(new BBProof(env, s, pnm, false))
+ d_bitblaster(new BBProof(env, s, pnm, false)),
+ d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
{
}
}
else
{
- d_bitblaster->getProofGenerator()->addRewriteStep(
- fact, n, PfRule::BV_EAGER_ATOM, {}, {fact});
TrustNode tlem =
- TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
+ d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
}
std::unique_ptr<BBProof> d_bitblaster;
/** Proof rule checker */
BVProofRuleChecker d_checker;
+ /** Proof generator for unpacking BITVECTOR_EAGER_ATOM. */
+ std::unique_ptr<EagerProofGenerator> d_epg;
};
} // namespace bv
regress0/bv/bv_to_int_zext.smt2
regress0/bv/bvcomp.cvc
regress0/bv/bvmul-pow2-only.smt2
+ regress0/bv/bvproof1.smt2
+ regress0/bv/bvproof2.smt2
+ regress0/bv/bvproof3.smt2
regress0/bv/bvsimple.cvc
regress0/bv/bvsmod.smt2
regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smtv1.smt2
--- /dev/null
+(set-logic QF_BV)
+(set-info :status unsat)
+(declare-const x Bool)
+(check-sat-assuming ((not (bvuge (bvcomp (_ bv0 4) (_ bv0 4)) (ite x (_ bv1 1) (_ bv0 1))))))
--- /dev/null
+(set-logic QF_ABV)
+(set-info :status unsat)
+(declare-const v (_ BitVec 1))
+(declare-const _v (_ BitVec 2))
+(declare-fun a () (Array (_ BitVec 3) (_ BitVec 2)))
+(assert (not (= (store (store (store a ((_ zero_extend 1) _v) (_ bv0 2)) (_ bv1 3) (_ bv0 2)) (_ bv0 3) (_ bv0 2)) (store (store (store (store a (_ bv0 3) (_ bv0 2)) ((_ zero_extend 2) v) (_ bv0 2)) (_ bv1 3) (_ bv0 2)) ((_ zero_extend 1) _v) (_ bv0 2)))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --bitblast=eager
+(set-logic QF_BV)
+(set-info :status unsat)
+(declare-const x (_ BitVec 1))
+(assert (= (_ bv2 4) ((_ zero_extend 3) x)))
+(check-sat)
projects / cvc5.git / commitdiff