Skip to content

Commit

Permalink
Add
Browse files Browse the repository at this point in the history
  • Loading branch information
ajreynol committed Feb 24, 2025
1 parent 5e0f1e0 commit 10dd1db
Show file tree
Hide file tree
Showing 5 changed files with 17 additions and 0 deletions.
2 changes: 2 additions & 0 deletions include/cvc5/cvc5_proof_rule.h
Original file line number Diff line number Diff line change
Expand Up @@ -4084,6 +4084,8 @@ enum ENUM(ProofRewriteRule)
EVALUE(SETS_MINUS_SELF),
/** Auto-generated from RARE rule sets-is-empty-elim */
EVALUE(SETS_IS_EMPTY_ELIM),
/** Auto-generated from RARE rule sets-is-singleton-elim */
EVALUE(SETS_IS_SINGLETON_ELIM),
/** Auto-generated from RARE rule str-eq-ctn-false */
EVALUE(STR_EQ_CTN_FALSE),
/** Auto-generated from RARE rule str-eq-ctn-full-false1 */
Expand Down
4 changes: 4 additions & 0 deletions proofs/eo/cpc/rules/Rewrites.eo
Original file line number Diff line number Diff line change
Expand Up @@ -1278,6 +1278,10 @@
:args (x1 (Set @T0))
:conclusion (= (set.is_empty x1) (= x1 (set.empty (Set @T0))))
)
(declare-rule sets-is-singleton-elim ((@T0 Type) (x1 (Set @T0)))
:args (x1)
:conclusion (= (set.is_singleton x1) (= x1 (set.singleton (set.choose x1))))
)
(declare-rule str-eq-ctn-false ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0) :list) (x2 (Seq @T1)) (x3 (Seq @T2) :list) (y1 (Seq @T3)))
:premises ((= (seq.contains y1 x2) false))
:args (x1 x2 x3 y1)
Expand Down
4 changes: 4 additions & 0 deletions src/theory/sets/rewrites
Original file line number Diff line number Diff line change
Expand Up @@ -71,3 +71,7 @@
(define-rule sets-is-empty-elim ((x ?Set))
(set.is_empty x)
(= x (@set.empty_of_type (@type_of x))))

(define-rule sets-is-singleton-elim ((x ?Set))
(set.is_singleton x)
(= x (set.singleton (set.choose x))))
1 change: 1 addition & 0 deletions test/regress/cli/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -1821,6 +1821,7 @@ set(regress_0_tests
regress0/sets/sets-equal.smt2
regress0/sets/sets-extr.smt2
regress0/sets/sets-inter.smt2
regress0/sets/sets-ising-elim-pf.smt2
regress0/sets/sets-new.smt2
regress0/sets/sets-of-sets-subtypes.smt2
regress0/sets/sets-poly-int-real.smt2
Expand Down
6 changes: 6 additions & 0 deletions test/regress/cli/regress0/sets/sets-ising-elim-pf.smt2
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
; EXPECT: unsat
(set-logic ALL)
(declare-const __ (_ BitVec 1))
(set-option :check-proofs true)
(assert (set.is_singleton (set.insert (_ bv0 101) ((_ zero_extend 100) __) (set.singleton (_ bv1 101)))))
(check-sat)

0 comments on commit 10dd1db

Please sign in to comment.