Home
last modified time | relevance | path

Searched refs:msb_t (Results 1 – 9 of 9) sorted by relevance

/dports/math/cvc4/CVC4-1.7/test/regress/regress0/bv/
H A Dbvsmod.smt27 (msb_t ((_ extract 12 12) t)))
9 (abs_t (ite (= msb_t #b0) t (bvneg t))))
13 (ite (and (= msb_s #b0) (= msb_t #b0))
15 (ite (and (= msb_s #b1) (= msb_t #b0))
17 (ite (and (= msb_s #b0) (= msb_t #b1))
/dports/math/boolector/boolector-3.2.2/test/log/
H A Dbvsrem.axiom3 (let (?msb_t (extract[|m-1|:|m-1|] t))
4 (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
6 (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
8 (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
H A Dbvsdiv.axiom3 (let (?msb_t (extract[|m-1|:|m-1|] t))
4 (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
6 (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
8 (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
H A Dbvsmod.axiom3 (let (?msb_t (extract[|m-1|:|m-1|] t))
4 (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
6 (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
8 (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
/dports/security/klee/klee-2.2/docs/SMT-COMP/
H A DQF_BV.smt183 (let (?msb_t (extract[|m-1|:|m-1|] t))
184 (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
186 (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
188 (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
193 (let (?msb_t (extract[|m-1|:|m-1|] t))
194 (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
196 (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
198 (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
203 (let (?msb_t (extract[|m-1|:|m-1|] t))
204 (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
[all …]
/dports/math/cvc4/CVC4-1.7/src/theory/bv/
H A Dtheory_bv_rewrite_rules_operator_elimination.h472 Node msb_t = utils::mkExtract(t, size - 1, size - 1); in apply() local
480 msb_t.eqNode(bit0).iteNode(t, nm->mkNode(kind::BITVECTOR_NEG, t)); in apply()
486 Node cond1 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit0)); in apply()
487 Node cond2 = msb_s.eqNode(bit1).andNode(msb_t.eqNode(bit0)); in apply()
488 Node cond3 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit1)); in apply()
/dports/math/yices/yices-2.6.2/src/mcsat/
H A Dpreprocessor.c592 term_t msb_t = mk_bitextract(tm, t_pre, n-1); in preprocessor_apply() local
616 term_t b1 = mk_ite(tm, msb_t, t1, t2, tau); in preprocessor_apply()
617 term_t b2 = mk_ite(tm, msb_t, t3, t4, tau); in preprocessor_apply()
641 term_t msb_t = mk_bitextract(tm, t_pre, n-1); in preprocessor_apply() local
665 term_t b1 = mk_ite(tm, msb_t, t1, t2, tau); in preprocessor_apply()
666 term_t b2 = mk_ite(tm, msb_t, t3, t4, tau); in preprocessor_apply()
/dports/math/py-pysmt/pysmt-0.9.0/pysmt/
H A Dformula.py911 msb_t = self.BVExtract(t, m-1, m-1)
913 abs_t = self.Ite(self.Equals(msb_t, zero_1), t, self.BVNeg(t))
917 cond2 = self.And(self.Equals(msb_s, zero_1), self.Equals(msb_t, zero_1))
918 cond3 = self.And(self.Equals(msb_s, one_1), self.Equals(msb_t, zero_1))
919 cond4 = self.And(self.Equals(msb_s, zero_1), self.Equals(msb_t, one_1))
/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/
H A Dbitvector_theorem_producer.cpp6492 Expr msb_t = d_theoryBitvector->newBVExtractExpr(t, m-1, m-1); in bvSDivRewrite() local
6497 Expr cond1 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit0)); in bvSDivRewrite()
6498 Expr cond2 = msb_s.eqExpr(bit1).andExpr(msb_t.eqExpr(bit0)); in bvSDivRewrite()
6499 Expr cond3 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit1)); in bvSDivRewrite()
6548 Expr msb_t = d_theoryBitvector->newBVExtractExpr(t, m-1, m-1); in bvSRemRewrite() local
6553 Expr cond1 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit0)); in bvSRemRewrite()
6554 Expr cond2 = msb_s.eqExpr(bit1).andExpr(msb_t.eqExpr(bit0)); in bvSRemRewrite()
6555 Expr cond3 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit1)); in bvSRemRewrite()
6617 Expr cond1 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit0)); in bvSModRewrite()
6618 Expr cond2 = msb_s.eqExpr(bit1).andExpr(msb_t.eqExpr(bit0)); in bvSModRewrite()
[all …]