| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Documentation/SBV/Examples/BitPrecise/ |
| H A D | PrefixSum.hs | 91 thm1 = prove $ flIsCorrect 8 (0, (+)) function
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_core/ |
| H A D | theory.cpp | 298 const Theorem& thm1 = e.getFind(); in findRef() local
313 const Theorem& thm1 = e.getFind(); in find() local
432 const Theorem thm1 = findRef(e[1]); in updateHelper() local
|
| H A D | theory_core.cpp | 995 Theorem thm1 = d_rules->rewriteDistinct(e); in rewrite() local
1147 Theorem thm1(find(eq[0])); in update() local
|
| /dports/math/gmp-ecm/ecm-7.0.4/ |
| H A D | cudakernel_default.cu | 8 unsigned int thm1; in Cuda_Fully_Normalize() local
|
| /dports/science/quantum-espresso/q-e-qe-6.7.0/TDDFPT/tools/ |
| H A D | tddfpt_calculate_spectrum.f90 | 845 & thm1, h2m1,& local
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | theory_arith_old.cpp | 844 Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0)); in processSimpleIntEq() local
1125 Theorem thm1 = isolateVariable(inequalityFindThm, varOnRHS); in processBuffer() local
1296 Theorem thm1 = (compactNonLinear != rhs ? in addToBuffer() local
1404 Theorem thm1 = termUpperBoundThm[t1]; in addToBuffer() local
1412 Theorem thm1 = termUpperBoundThm[t2]; in addToBuffer() local
2397 Theorem thm1(alphaLEax), thm2(bxLEbeta); in processFiniteInterval() local
|
| H A D | theory_arith3.cpp | 864 Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0)); in processSimpleIntEq() local
1069 Theorem thm1 = isolateVariable(ineqThm, varOnRHS); in processBuffer() local
1941 Theorem thm1(alphaLEax), thm2(bxLEbeta); in processFiniteInterval() local
|
| H A D | theory_arith_new.cpp | 620 Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0)); in processSimpleIntEq() local
1192 Theorem thm1(alphaLEax), thm2(bxLEbeta); in processFiniteInterval() local
|
| H A D | arith_theorem_producer.cpp | 2905 Theorem ArithTheoremProducer::addInequalities(const Theorem& thm1, const Theorem& thm2) { in addInequalities()
|
| H A D | arith_theorem_producer3.cpp | 2814 Theorem ArithTheoremProducer3::addInequalities(const Theorem& thm1, const Theorem& thm2) { in addInequalities()
|
| H A D | arith_theorem_producer_old.cpp | 3016 Theorem ArithTheoremProducerOld::addInequalities(const Theorem& thm1, const Theorem& thm2) { in addInequalities()
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/ |
| H A D | theory_bitvector.cpp | 221 Theorem thm1 = substitutivityRule(OR, substThms); in bitBlastDisEqn() local
871 Theorem thm1 = substitutivityRule(ee, changed, newChildrenThm); in simplifyOp() local
1575 Theorem thm1 = d_rules->signExtendRule(paddedE[1]); in rewriteBV() local
|
| /dports/math/cvc3/cvc3-2.4.1/src/theorem/ |
| H A D | common_theorem_producer.cpp | 333 const Theorem& thm1, in substitutivityRule()
|