| /dports/math/stp/stp-2.3.3/tests/generated-tests/generators/ |
| H A D | mulDivRem.cpp | 93 else if (SBVREM == k) in getSignedResult()
175 go(4, aS, bS, getSignedResult(aS, SBVREM, bS), "bvsrem"); in testSolver()
|
| /dports/math/stp/stp-2.3.3/include/stp/Simplifier/ |
| H A D | StrengthReduction.h | 132 kind == SBVREM) in topLevel()
160 else if (kind == SBVREM) in topLevel()
271 k == SBVREM || k == BVSX)) in topLevel()
327 case SBVREM: in topLevel()
|
| H A D | UnsignedIntervalAnalysis.h | 706 case SBVREM: in visit()
|
| /dports/math/stp/stp-2.3.3/lib/Simplifier/ |
| H A D | DifficultyScore.cpp | 38 k == SBVREM || k == SBVMOD; in isLikeDivision()
|
| H A D | consteval.cpp | 329 case SBVREM: in NonMemberBVConstEvaluator()
338 if (k == SBVREM) in NonMemberBVConstEvaluator()
|
| H A D | Simplifier.cpp | 3148 case SBVREM: in simplify_term_switch()
|
| /dports/math/stp/stp-2.3.3/lib/Printer/ |
| H A D | PLPrinter.cpp | 58 case SBVREM: in functionToCVCName()
241 case SBVREM: in PL_Print1()
|
| H A D | SMTLIBPrinter.cpp | 261 case SBVREM: in functionToSMTLIBName()
|
| H A D | CPrinter.cpp | 189 case SBVREM: in C_Print1()
|
| /dports/math/stp/stp-2.3.3/lib/AST/ |
| H A D | ASTKind.kinds | 48 SBVREM 2 2 Term
|
| H A D | ASTmisc.cpp | 409 case SBVREM: in BVTypeCheck_term_kind()
|
| /dports/math/stp/stp-2.3.3/tools/time_constantbitprop/ |
| H A D | time_cbitp.cpp | 227 run_with_various_prob(signedRemainder, output, stp::SBVREM); in main()
|
| /dports/math/stp/stp-2.3.3/lib/Simplifier/constantBitP/ |
| H A D | ConstantBitPropagation.cpp | 719 case SBVREM: in dispatchToTransferFunctions()
758 else if (k == SBVREM) in dispatchToTransferFunctions()
|
| /dports/math/stp/stp-2.3.3/tools/test_constantbitprop/ |
| H A D | test_cbitp.cpp | 443 kind == SBVREM) in some_random_tests()
815 random_tests(&signedRemainder, SBVREM); in random_tests()
1044 signature.kind = SBVREM; in check_bvdiv_mod_mult()
|
| /dports/math/stp/stp-2.3.3/lib/AST/NodeFactory/ |
| H A D | SimplifyingNodeFactory.cpp | 43 using stp::SBVREM;
1643 case SBVREM: in CreateTerm()
1665 NodeFactory::CreateTerm(SBVREM, width, children[0], children[1][0]); in CreateTerm()
1675 …result = bm.CreateTerm(BVUMINUS,width,bm.CreateTerm(SBVREM,width,children[0][0],children[1]));//1… in CreateTerm()
1720 result = NodeFactory::CreateTerm(SBVREM,width,one,children[1]); //8883 -> 206 | 1566 ms in CreateTerm()
|
| /dports/math/stp/stp-2.3.3/lib/Parser/ |
| H A D | smt2.y | 82 using stp::SBVREM; //!< Signed bitvector remainder
136 using stp::SBVREM; //!< Signed bitvector remainder
1229 ASTNode * n = stp::GlobalParserInterface->newNode(SBVREM, width, *$2, *$3);
|
| H A D | cvc.y | 1006 ASTNode * n = new ASTNode(GlobalParserInterface->nf->CreateTerm(SBVREM, $3, *$5, *$7));
|
| H A D | smt.y | 893 ASTNode * n = GlobalParserInterface->newNode(SBVREM, width, *$2, *$3);
|
| /dports/math/stp/stp-2.3.3/include/stp/ |
| H A D | c_interface.h | 1054 SBVREM, //!< Signed bitvector remainder enumerator
|
| /dports/math/stp/stp-2.3.3/lib/AbsRefineCounterExample/ |
| H A D | ArrayTransformer.cpp | 141 if (SBVREM == in.GetKind()) in TranslateSignedDivModRem()
|
| /dports/math/stp/stp-2.3.3/lib/Interface/ |
| H A D | c_interface.cpp | 1190 return createBinaryTerm(vc, n_bits, stp::SBVREM, left, right); in vc_sbvRemExpr()
|
| /dports/math/stp/stp-2.3.3/lib/ToSat/ |
| H A D | BitBlaster.cpp | 885 case SBVREM: in BBTerm()
|