diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-07-27 12:39:53 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-27 19:39:53 +0000 |
commit | 4c87b04c95b60c34d2e8313e82579fbb0415eaf7 (patch) | |
tree | 097ecca3b4494722a4cc36dd136b37f274e3fceb /src/proof | |
parent | 3a180a2f8ffe8ad5756119ce0cbe61ab4ab28127 (diff) |
proof: Add eqrange expansion rule. (#6936)
Adds proof support for the eqrange operator.
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/proof_rule.cpp | 1 | ||||
-rw-r--r-- | src/proof/proof_rule.h | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 3991305ca..7e1cdf8d3 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -120,6 +120,7 @@ const char* toString(PfRule id) case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; + case PfRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND"; //================================================= Bit-Vector rules case PfRule::BV_BITBLAST: return "BV_BITBLAST"; case PfRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 173e4df9a..78e773bdc 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -713,6 +713,15 @@ enum class PfRule : uint32_t // Conclusion: (not (= (select a k) (select b k))) // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))). ARRAYS_EXT, + // ======== EQ_RANGE expansion + // Children: none + // Arguments: ((eqrange a b i j)) + // ---------------------------------------- + // Conclusion: (= + // (eqrange a b i j) + // (forall ((x T)) + // (=> (and (<= i x) (<= x j)) (= (select a x) (select b x))))) + ARRAYS_EQ_RANGE_EXPAND, // ======== Array Trust // Children: (P1 ... Pn) // Arguments: (F) |