| /dports/textproc/hs-pandoc/pandoc-2.14.2/test/command/ |
| H A D | 6925.md | 6 \newtheorem{thm2}[section]{Theorem}
15 \begin{thm2}
20 \end{thm2}
29 ::: thm2
|
| /dports/textproc/hs-pandoc-crossref/pandoc-crossref-0.3.12.0/_cabal_deps/pandoc-2.11.4/test/command/ |
| H A D | 6925.md | 6 \newtheorem{thm2}[section]{Theorem}
15 \begin{thm2}
20 \end{thm2}
29 ::: {.thm2}
|
| /dports/math/cvc3/cvc3-2.4.1/src/sat/ |
| H A D | cnf_theorem_producer.cpp | 59 Theorem thm2; in getSmartClauses() local
83 thm2 = newTheorem(TempVec[0], Assumptions::emptyAssump(), pf); in getSmartClauses()
89 thm2 = newTheorem(Expr(OR, TempVec), Assumptions::emptyAssump(), pf); in getSmartClauses()
94 thm2.setQuantLevel(thm.getQuantLevel()); in getSmartClauses()
95 clauses.push_back(thm2); in getSmartClauses()
141 Theorem thm2; in learnedClauses() local
146 thm2 = newTheorem(assumptions[0], Assumptions::emptyAssump(), pf); in learnedClauses()
153 thm2 = newTheorem(clauseExpr, Assumptions::emptyAssump(), pf); in learnedClauses()
155 thm2.setQuantLevel(thm.getQuantLevel()); in learnedClauses()
156 clauses.push_back(thm2); in learnedClauses()
|
| H A D | cnf_manager.cpp | 93 Theorem thm2 = d_commonRules->symmetryRule(thm); in replaceITErec() local
94 thm2 = d_commonRules->iffMP(thm2, d_rules->ifLiftRule(thm2.getExpr(), 1)); in replaceITErec()
96 d_translateQueueThms.push_back(thm2); in replaceITErec()
|
| /dports/math/cvc3/cvc3-2.4.1/src/search/ |
| H A D | circuit.cpp | 63 Theorem thm2; in propagate() local
89 se->d_rules->propAndrLRT(d_thm, t0, &thm, &thm2); in propagate()
174 &thm, &thm2); in propagate()
212 if (!thm2.isNull() && se->newLiteral(thm2.getExpr()).getValue() == 0) in propagate()
214 se->d_core->addFact(thm2); in propagate()
215 se->recordFact(thm2); in propagate()
216 se->d_literals.push_back(se->newLiteral(thm2.getExpr())); in propagate()
|
| H A D | search_simple.cpp | 87 Theorem thm2; in checkValidRec() local
88 qres = checkValidRec(thm2); in checkValidRec()
91 thm = d_rules->caseSplit(splitter, thm, thm2); in checkValidRec()
94 thm = thm2; in checkValidRec()
|
| H A D | search_sat.cpp | 1084 Theorem thm2 = d_core->getExprTrans()->preprocess(thm); in newUserAssumptionInt() local
1085 Expr e2 = thm2.getExpr(); in newUserAssumptionInt()
1087 d_core->addFact(thm2); in newUserAssumptionInt()
1091 newUserAssumptionIntHelper(thm2, cnf, false); in newUserAssumptionInt()
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_array/ |
| H A D | theory_array.cpp | 582 thm2 = transitivityRule(thm2, simplify(thm2.getRHS())); in update()
583 if (thm2.getRHS().isAtomic()) { in update()
631 if (thm2.getRHS() == sigNew[2]) { in update()
640 if (!thm2.isNull()) { in update()
641 if (thm2.isRefl()) { in update()
646 thm2 = substitutivityRule(sigNew,0,thm2); in update()
647 thm2 = transitivityRule(thm2, in update()
649 thm = transitivityRule(thm, thm2); in update()
657 thm2 = transitivityRule(thm2, simplify(thm2.getRHS())); in update()
659 if (thm2.getRHS().isAtomic()) { in update()
[all …]
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_core/ |
| H A D | theory.cpp | 302 const Theorem& thm2 = findRef(e1); in findRef() local
303 DebugAssert(thm2.getLHS()==e1,""); in findRef()
304 DebugAssert(thm2.getLHS() != thm2.getRHS(),""); in findRef()
305 e.setFind(transitivityRule(thm1,thm2)); in findRef()
318 Theorem thm2 = find(e1); in find() local
319 DebugAssert(thm2.getLHS()==e1,""); in find()
320 DebugAssert(thm2.getLHS() != thm2.getRHS(),""); in find()
321 thm2 = transitivityRule(thm1,thm2); in find()
322 e.setFind(thm2); in find()
323 return thm2; in find()
|
| H A D | expr_transform.cpp | 319 Theorem thm2 = specialSimplify(e[k], cache); in specialSimplify() local
320 if (!thm2.isRefl()) { in specialSimplify()
321 newChildrenThm.push_back(thm2); in specialSimplify()
349 Theorem thm, thm2; in newPPrec() local
389 thm2 = d_core->simplify(newExpr[1]); in newPPrec()
390 thm = d_commonRules->transitivityRule(thm, d_rules->rewriteIteThen(newExpr, thm2)); in newPPrec()
396 thm2 = d_core->simplify(newExpr[2]); in newPPrec()
398 thm = d_commonRules->transitivityRule(thm, d_rules->rewriteIteElse(newExpr, thm2)); in newPPrec()
|
| H A D | theory_core.cpp | 435 Theorem thm2 = in assertFormula() local
1148 Theorem thm2(find(eq[1])); in update() local
1166 Theorem thm2 = find(newEq); in update() local
1167 if (thm2.getRHS().isTrue()) { in update()
1168 thm2 = transitivityRule(thm, thm2); in update()
1177 Theorem thm2 = find(eq); in update() local
1179 thm2 = transitivityRule(symmetryRule(thm),thm2); in update()
3554 Theorem thm2 = simplify(e); in registerAtom() local
3555 if (thm2.getRHS().isTrue()) { in registerAtom()
3564 theoryOf(thm2.getRHS())->registerAtom(thm2.getRHS()); in registerAtom()
[all …]
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Documentation/SBV/Examples/BitPrecise/ |
| H A D | PrefixSum.hs | 98 thm2 :: IO ThmResult
99 thm2 = prove $ flIsCorrect 16 (0, smax) function
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | theory_arith3.cpp | 1521 betaLTt = canonPred(thm2); in normalizeProjectIneqs()
1527 tLTalpha = canonPred(thm2); in normalizeProjectIneqs()
1941 Theorem thm1(alphaLEax), thm2(bxLEbeta); in processFiniteInterval() local
1951 const Expr& beta = thm2.getExpr()[1]; in processFiniteInterval()
1965 tLEac = iffMP(thm2, tLEac); in processFiniteInterval()
2065 enqueueFact(thm2); in assertFact()
2067 DebugAssert(thm2.getExpr().isAnd() && thm2.getExpr().arity()==2, in assertFact()
2069 const Expr& G1orG2 = thm2.getExpr()[0]; in assertFact()
2098 DebugAssert(thm2.getLHS() != thm2.getRHS(), "Expected rewrite"); in assertFact()
2099 thm2 = getCommonRules()->substitutivityRule(thm.getRHS(), thm2); in assertFact()
[all …]
|
| H A D | theory_arith_old.cpp | 1405 Theorem thm2 = termLowerBoundThm[t1]; in addToBuffer() local
1413 Theorem thm2 = termLowerBoundThm[t2]; in addToBuffer() local
1894 betaLTt = canonPred(thm2); in normalizeProjectIneqs()
1899 tLTalpha = canonPred(thm2); in normalizeProjectIneqs()
2407 const Expr& beta = thm2.getExpr()[1]; in processFiniteInterval()
2421 tLEac = iffMP(thm2, tLEac); in processFiniteInterval()
2544 enqueueFact(thm2); in assertFact()
2551 enqueueFact(thm2); in assertFact()
3467 Expr newIneq = thm2.getRHS(); in update()
3477 dontBuffer[thm2.getRHS()] = true; in update()
[all …]
|
| H A D | theory_arith_new.cpp | 621 Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1)); in processSimpleIntEq() local
622 Theorem newRes = getCommonRules()->andIntro(thm1, thm2); in processSimpleIntEq()
1192 Theorem thm1(alphaLEax), thm2(bxLEbeta); in processFiniteInterval() local
1196 thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a))); in processFiniteInterval()
1202 const Expr& beta = thm2.getExpr()[1]; in processFiniteInterval()
1215 Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms); in processFiniteInterval()
1216 tLEac = iffMP(thm2, tLEac); in processFiniteInterval()
1783 Theorem thm2 = substitutivityRule(d, changed, children); in update() local
1785 enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2)); in update()
1789 transitivityRule(symmetryRule(thm2), thm))); in update()
|
| H A D | arith_proof_rules.h | 421 virtual Theorem addInequalities(const Theorem& thm1, const Theorem& thm2) = 0;
|
| H A D | arith_theorem_producer.h | 305 Theorem addInequalities(const Theorem& thm1, const Theorem& thm2);
|
| H A D | arith_theorem_producer_old.h | 305 Theorem addInequalities(const Theorem& thm1, const Theorem& thm2);
|
| H A D | arith_theorem_producer3.h | 304 Theorem addInequalities(const Theorem& thm1, const Theorem& thm2);
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/ |
| H A D | theory_bitvector.cpp | 225 result = iffMP(result, thm2); in bitBlastDisEqn()
2373 Theorem thm2 = thm; in simplifyPendingEq() local
2399 thm2 = transitivityRule(thm2, find(rhs)); in simplifyPendingEq()
2401 thm2 = iffMP(thm2, d_rules->canonBVEQ(thm2.getExpr(), maxEffort)); in simplifyPendingEq()
2402 if (thm2.isRewrite() && thm2.getRHS() == lhs && thm2.getLHS() == rhs) { in simplifyPendingEq()
2403 thm2 = thm; in simplifyPendingEq()
2405 return thm2; in simplifyPendingEq()
2416 const Expr& e2 = thm2.getExpr(); in generalBitBlast()
2420 return thm2; in generalBitBlast()
2422 return iffMP(thm2, bitBlastEqn(thm2.getExpr())); in generalBitBlast()
[all …]
|
| /dports/math/cvc3/cvc3-2.4.1/src/theorem/ |
| H A D | common_theorem_producer.cpp | 334 const Theorem& thm2) { in substitutivityRule() argument
346 e[1] == thm2.getLHS(), in substitutivityRule()
353 CHECK_SOUND(thm2.isRewrite(), in substitutivityRule()
356 + thm2.getExpr().toString() in substitutivityRule()
359 Expr e2(e.getOp(), thm1.getRHS(), thm2.getRHS()); in substitutivityRule()
364 pfs.push_back(thm2.getProof()); in substitutivityRule()
367 Theorem res = newRWTheorem(e, e2, Assumptions(thm1, thm2), pf); in substitutivityRule()
|
| H A D | common_theorem_producer.h | 77 const Theorem& thm2);
|
| /dports/converters/p5-LaTeXML/LaTeXML-0.8.6/t/structure/ |
| H A D | autoref.tex | 72 \refs{thm2}\\
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | common_proof_rules.h | 118 const Theorem& thm2) = 0;
|
| /dports/emulators/hercules/hercules-3.13/ |
| H A D | comm3705.c | 2143 int thm2; in th_remap() local
2152 thm2 = thptr[1]; in th_remap()
2163 thptr[5] = thm2; in th_remap()
2173 thm2 = thptr[5]; in th_remap()
2181 thptr[1] = thm2; in th_remap()
|