From 54853f9584f2de2bf4e1ff16517b44a45e6d7cf2 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 14 Sep 2021 10:39:43 -0700 Subject: [PATCH] proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147) 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. --- src/CMakeLists.txt | 2 + src/smt/proof_post_processor.cpp | 1 + .../bv/bitblast/bitblast_proof_generator.cpp | 123 +++++++++++ .../bv/bitblast/bitblast_proof_generator.h | 75 +++++++ src/theory/bv/bitblast/node_bitblaster.cpp | 10 + src/theory/bv/bitblast/node_bitblaster.h | 7 + src/theory/bv/bitblast/proof_bitblaster.cpp | 198 ++++++++++-------- src/theory/bv/bitblast/proof_bitblaster.h | 14 +- src/theory/bv/bv_solver_bitblast_internal.cpp | 8 +- src/theory/bv/bv_solver_bitblast_internal.h | 2 + test/regress/CMakeLists.txt | 3 + test/regress/regress0/bv/bvproof1.smt2 | 4 + test/regress/regress0/bv/bvproof2.smt2 | 7 + test/regress/regress0/bv/bvproof3.smt2 | 6 + 14 files changed, 364 insertions(+), 96 deletions(-) create mode 100644 src/theory/bv/bitblast/bitblast_proof_generator.cpp create mode 100644 src/theory/bv/bitblast/bitblast_proof_generator.h create mode 100644 test/regress/regress0/bv/bvproof1.smt2 create mode 100644 test/regress/regress0/bv/bvproof2.smt2 create mode 100644 test/regress/regress0/bv/bvproof3.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 223d3ff1f..abc2d7219 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -601,6 +601,8 @@ libcvc5_add_sources( 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 diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 4bb875f72..3866c1e0e 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -22,6 +22,7 @@ #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" diff --git a/src/theory/bv/bitblast/bitblast_proof_generator.cpp b/src/theory/bv/bitblast/bitblast_proof_generator.cpp new file mode 100644 index 000000000..57435f651 --- /dev/null +++ b/src/theory/bv/bitblast/bitblast_proof_generator.cpp @@ -0,0 +1,123 @@ +/****************************************************************************** + * 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 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 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 diff --git a/src/theory/bv/bitblast/bitblast_proof_generator.h b/src/theory/bv/bitblast/bitblast_proof_generator.h new file mode 100644 index 000000000..114bf4749 --- /dev/null +++ b/src/theory/bv/bitblast/bitblast_proof_generator.h @@ -0,0 +1,75 @@ +/****************************************************************************** + * 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 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> d_cache; +}; + +} // namespace bv +} // namespace theory +} // namespace cvc5 +#endif diff --git a/src/theory/bv/bitblast/node_bitblaster.cpp b/src/theory/bv/bitblast/node_bitblaster.cpp index 9f738634c..898501195 100644 --- a/src/theory/bv/bitblast/node_bitblaster.cpp +++ b/src/theory/bv/bitblast/node_bitblaster.cpp @@ -36,6 +36,9 @@ void NodeBitblaster::bbAtom(TNode node) 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 @@ -166,6 +169,13 @@ bool NodeBitblaster::isVariable(TNode node) 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 diff --git a/src/theory/bv/bitblast/node_bitblaster.h b/src/theory/bv/bitblast/node_bitblaster.h index 94b9d638b..ecb2970e8 100644 --- a/src/theory/bv/bitblast/node_bitblaster.h +++ b/src/theory/bv/bitblast/node_bitblaster.h @@ -63,6 +63,13 @@ class NodeBitblaster : public TBitblaster, protected EnvObj /** 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; diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index bef23c0b5..6119e9d7c 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -17,6 +17,7 @@ #include #include "proof/conv_proof_generator.h" +#include "theory/bv/bitblast/bitblast_proof_generator.h" #include "theory/theory_model.h" namespace cvc5 { @@ -44,6 +45,7 @@ BBProof::BBProof(Env& env, d_tcontext.get(), false) : nullptr), + d_bbpg(pnm ? new BitblastProofGenerator(pnm, d_tcpg.get()) : nullptr), d_recordFineGrainedProofs(fineGrained) { } @@ -52,119 +54,137 @@ BBProof::~BBProof() {} void BBProof::bbAtom(TNode node) { - std::vector visit; - visit.push_back(node); - std::unordered_set 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 visit; + std::unordered_set 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 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 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 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); } @@ -187,7 +207,7 @@ bool BBProof::collectModelValues(TheoryModel* m, 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; } diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index be150a0e8..0cf8b40f7 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -27,6 +27,8 @@ class TConvProofGenerator; namespace theory { namespace bv { +class BitblastProofGenerator; + class BBProof : protected EnvObj { using Bits = std::vector; @@ -51,26 +53,32 @@ class BBProof : protected EnvObj /** Collect model values for all relevant terms given in 'relevantTerms'. */ bool collectModelValues(TheoryModel* m, const std::set& 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 d_bb; /** The associated proof node manager. */ ProofNodeManager* d_pnm; /** Term context for d_tcpg to not rewrite below BV leafs. */ std::unique_ptr d_tcontext; - /** The associated term conversion proof generator. */ + /** Term conversion proof generator for bit-blast steps. */ std::unique_ptr d_tcpg; + /** Bitblast proof generator. */ + std::unique_ptr d_bbpg; /** Map bit-vector nodes to bit-blasted nodes. */ std::unordered_map d_bbMap; - + /** Flag to indicate whether fine-grained proofs should be recorded. */ bool d_recordFineGrainedProofs; }; + } // namespace bv } // namespace theory } // namespace cvc5 diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp index 490ba325c..0c43cddbf 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.cpp +++ b/src/theory/bv/bv_solver_bitblast_internal.cpp @@ -17,6 +17,7 @@ #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" @@ -74,7 +75,8 @@ BVSolverBitblastInternal::BVSolverBitblastInternal( 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) { } @@ -126,10 +128,8 @@ bool BVSolverBitblastInternal::preNotifyFact( } 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); } diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h index 72b8b4f4d..2c53b9056 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.h +++ b/src/theory/bv/bv_solver_bitblast_internal.h @@ -79,6 +79,8 @@ class BVSolverBitblastInternal : public BVSolver std::unique_ptr d_bitblaster; /** Proof rule checker */ BVProofRuleChecker d_checker; + /** Proof generator for unpacking BITVECTOR_EAGER_ATOM. */ + std::unique_ptr d_epg; }; } // namespace bv diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index be95286cc..fd734b321 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -260,6 +260,9 @@ set(regress_0_tests 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 diff --git a/test/regress/regress0/bv/bvproof1.smt2 b/test/regress/regress0/bv/bvproof1.smt2 new file mode 100644 index 000000000..a947aa84a --- /dev/null +++ b/test/regress/regress0/bv/bvproof1.smt2 @@ -0,0 +1,4 @@ +(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)))))) diff --git a/test/regress/regress0/bv/bvproof2.smt2 b/test/regress/regress0/bv/bvproof2.smt2 new file mode 100644 index 000000000..f06194952 --- /dev/null +++ b/test/regress/regress0/bv/bvproof2.smt2 @@ -0,0 +1,7 @@ +(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) diff --git a/test/regress/regress0/bv/bvproof3.smt2 b/test/regress/regress0/bv/bvproof3.smt2 new file mode 100644 index 000000000..5650bc5d6 --- /dev/null +++ b/test/regress/regress0/bv/bvproof3.smt2 @@ -0,0 +1,6 @@ +; 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) -- 2.30.2