| /dports/math/stp/stp-2.3.3/lib/Simplifier/ |
| H A D | RemoveUnconstrained.cpp | 342 case BVSGE: in topLevel_other()
352 if (kind == BVSGT || kind == BVSGE) in topLevel_other()
380 assert(kind == BVSGE || kind == BVGE); in topLevel_other()
444 if (kind == BVSGE || kind == BVGE) in topLevel_other()
460 if (kind == BVSGE || kind == BVGE) in topLevel_other()
|
| H A D | DifficultyScore.cpp | 57 else if (k == EQ || k == BVGE || k == BVGT || k == BVSGE || k == BVSGT) in eval()
|
| H A D | AIGSimplifyPropositionalCore.cpp | 77 if (k == BVGT || k == BVGE || k == EQ || k == BVSGE || k == BVSGT || in theoryToFresh()
|
| H A D | Simplifier.cpp | 465 case BVSGE: in SimplifyAtomicFormula()
613 k = BVSGE; in CreateSimplifiedINEQ()
615 assert(k == BVGT || k == BVGE || k == BVSGT || k == BVSGE); in CreateSimplifiedINEQ()
631 if (k == BVLE || k == BVGE || k == BVSLE || k == BVSGE) in CreateSimplifiedINEQ()
671 if (comparator != 0 && (k == BVSGT || k == BVSGE)) in CreateSimplifiedINEQ()
697 if (k == BVSGT || k == BVSGE) in CreateSimplifiedINEQ()
766 case BVSGE: in CreateSimplifiedINEQ()
|
| /dports/math/stp/stp-2.3.3/include/stp/Util/ |
| H A D | Functions.h | 97 l.push_back(Function(stp::BVSGE, "signed greater than equals", in Functions()
|
| /dports/math/stp/stp-2.3.3/lib/Printer/ |
| H A D | PLPrinter.cpp | 70 case BVSGE: in functionToCVCName()
283 case BVSGE: in PL_Print1()
|
| H A D | SMTLIBPrinter.cpp | 209 case BVSGE: in functionToSMTLIBName()
|
| H A D | CPrinter.cpp | 282 case BVSGE: in C_Print1()
|
| /dports/math/stp/stp-2.3.3/lib/AST/ |
| H A D | ASTmisc.cpp | 211 BVSLE == kind || BVSGT == kind || BVSGE == kind || SYMBOL == kind || in isAtomic()
570 case BVSGE: in BVTypeCheck_nonterm_kind()
|
| H A D | ASTKind.kinds | 66 BVSGE 2 2 Form
|
| /dports/math/stp/stp-2.3.3/include/stp/Simplifier/ |
| H A D | StrengthReduction.h | 270 (k == BVSGT || k == BVSGE || k == SBVDIV || k == BVSRSHIFT || in topLevel()
309 case BVSGE: in topLevel()
|
| /dports/math/stp/stp-2.3.3/include/stp/AST/ |
| H A D | ASTNode.h | 116 k == BVSLE || k == BVSGT || k == BVSGE || k == EQ; in isPred()
|
| /dports/math/stp/stp-2.3.3/tools/time_constantbitprop/ |
| H A D | time_cbitp.cpp | 185 run_with_various_prob(&bvSignedGreaterThanEqualsBothWays, output, stp::BVSGE); in main()
|
| /dports/math/py-pysmt/pysmt-0.9.0/pysmt/test/ |
| H A D | examples.py | 31 BVULT, BVUGT, BVULE, BVUGE, BVSGE,
35 BVSLT, BVSGT, BVSGE, BVSDiv, BVSRem,
355 expr=BVSGE(bv16, BVZero(16)),
462 expr=Or(BVSGT(BVZero(16), bv16), BVSGE(bv16, BVZero(16))),
|
| H A D | test_bv.py | 264 mgr.Ite(mgr.BVSGE(bvx, mgr.BV(0, 8)),
285 mgr.Ite(mgr.BVSGE(bvx, mgr.BV(0, 8)),
|
| /dports/math/py-pysmt/pysmt-0.9.0/pysmt/ |
| H A D | shortcuts.py | 722 def BVSGE(left, right): function
730 return get_env().formula_manager.BVSGE(left, right)
|
| H A D | fnode.py | 802 def BVSGE(self, right): member in FNode
803 return self._apply_infix(right, _mgr().BVSGE)
|
| /dports/math/petanque/arybo-release-1.1.0/arybo/tools/ |
| H A D | triton_.py | 141 TAstN.BVSGE: lambda x,y: EX.ExprCmpGte(x,y,True),
|
| /dports/math/py-arybo/arybo-1.1.0/arybo/tools/ |
| H A D | triton_.py | 141 TAstN.BVSGE: lambda x,y: EX.ExprCmpGte(x,y,True),
|
| /dports/math/stp/stp-2.3.3/lib/Parser/ |
| H A D | smt2.y | 95 using stp::BVSGE; //!< Signed bitvector greater-equals
149 using stp::BVSGE; //!< Signed bitvector greater-equals
841 ASTNode * n = stp::GlobalParserInterface->newNode(BVSGE, *$3, *$4);
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | theory_bitvector.h | 80 BVSGE, enumerator
|
| /dports/math/stp/stp-2.3.3/tools/test_constantbitprop/ |
| H A D | test_cbitp.cpp | 773 random_tests(&bvSignedGreaterThanEqualsBothWays, BVSGE); in random_tests()
1002 signature.kind = BVSGE; in check_bv_signed_comps()
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/ |
| H A D | theory_bitvector.cpp | 1611 case BVSGE: in rewriteBV()
1772 getEM()->newKind(BVSGE, "_BVSGE"); in TheoryBitvector()
1818 kinds.push_back(BVSGE); in TheoryBitvector()
3275 case BVSGE: in computeType()
3317 case BVSGE: in computeModelTerm()
3367 case BVSGE: in computeModel()
3629 case BVSGE: in printSmtLibShared()
3866 case BVSGE: in print()
4604 case BVSGE: in parseExprOp()
|
| /dports/math/stp/stp-2.3.3/include/stp/ |
| H A D | c_interface.h | 1067 BVSGE, //!< Signed bitvector greater-equals enumerator
|
| /dports/math/stp/stp-2.3.3/lib/Simplifier/constantBitP/ |
| H A D | ConstantBitPropagation.cpp | 690 MAPTFN(BVSGE, bvSignedGreaterThanEqualsBothWays) in dispatchToTransferFunctions()
|