| /dports/math/cvc3/cvc3-2.4.1/src/search/ |
| H A D | search_theorem_producer.cpp | 310 Proof body(thm.getProof()); in conflictClause()
400 pfs.push_back(i->getProof()); in cutRule()
554 pfs.push_back(i->getProof()); in unitProp()
584 pfs.push_back(b_th.getProof()); in propAndrAF()
614 pfs.push_back(l_th.getProof()); in propAndrAT()
615 pfs.push_back(r_th.getProof()); in propAndrAT()
642 pfs.push_back(a_th.getProof()); in propAndrLRT()
672 pfs.push_back(a_th.getProof()); in propAndrLF()
673 pfs.push_back(r_th.getProof()); in propAndrLF()
702 pfs.push_back(a_th.getProof()); in propAndrRF()
[all …]
|
| /dports/math/cvc3/cvc3-2.4.1/src/sat/ |
| H A D | cnf_theorem_producer.cpp | 64 pfs.push_back(thm.getProof()); in getSmartClauses()
75 pfs.push_back(assumptions[i].getProof()); in getSmartClauses()
144 pf = newPf("learned_clause", thm.getProof()); in learnedClauses()
151 pf = newPf("learned_clause", thm.getProof()); in learnedClauses()
264 pfs.push_back((*i).getProof()); in CNFtranslate()
294 pfs.push_back(thms[0].getProof()); in CNFITEtranslate()
295 pfs.push_back(thms[1].getProof()); in CNFITEtranslate()
296 pfs.push_back(thms[2].getProof()); in CNFITEtranslate()
316 pf = newPf("cnf_add_unit", thm.getExpr(), thm.getProof() ); in CNFAddUnit()
326 pf = newPf("cnf_convert", e, thm.getExpr(), thm.getProof() ); in CNFConvert()
|
| H A D | dpllt_minisat.cpp | 284 node->setNodeProof(clauseThm.getProof()); in generateSatProof()
287 return clauseThm.getProof(); in generateSatProof()
379 SAT::SatProof* proof = getProof(); in getSatProof()
|
| /dports/databases/mongodb36/mongodb-src-r3.6.23/src/mongo/db/ |
| H A D | time_proof_service_test.cpp | 50 TimeProof proof = timeProofService.getProof(time, key); in TEST()
70 TimeProof proof1 = timeProofService.getProof(time1, key); in TEST()
74 TimeProof proof2 = timeProofService.getProof(time2, key); in TEST()
81 TimeProof proof3 = timeProofService.getProof(time3, key); in TEST()
|
| H A D | logical_time_validator_test.cpp | 114 ASSERT_TRUE(newTime.getProof()); in TEST_F()
120 ASSERT_TRUE(newTime2.getProof()); in TEST_F()
198 ASSERT_TRUE(newTime.getProof()); in TEST_F()
206 ASSERT_TRUE(newTime2.getProof()); in TEST_F()
|
| H A D | logical_time_validator.cpp | 98 if (newTime == _lastSeenValidTime.getTime() && _lastSeenValidTime.getProof()) { in _getProof()
102 auto signature = _timeProofService.getProof(newTime, key); in _getProof()
105 if (newTime > _lastSeenValidTime.getTime() || !_lastSeenValidTime.getProof()) { in _getProof()
160 const auto newProof = newTime.getProof(); in validate()
|
| H A D | time_proof_service.cpp | 60 TimeProofService::TimeProof TimeProofService::getProof(LogicalTime time, const Key& key) { in getProof() function in mongo::TimeProofService
78 auto myProof = getProof(time, key); in checkProof()
|
| H A D | logical_time_test.cpp | 149 auto proof = tps.getProof(time, key); in TEST()
155 ASSERT_TRUE(proof == signedTime.getProof()); in TEST()
|
| H A D | signed_logical_time.h | 59 boost::optional<TimeProof> getProof() const { in getProof() function
|
| H A D | time_proof_service.h | 61 TimeProof getProof(LogicalTime time, const Key& key);
|
| /dports/math/cvc3/cvc3-2.4.1/src/theorem/ |
| H A D | common_theorem_producer.cpp | 73 pfs.push_back(phi.getProof()); in queryTCC()
74 pfs.push_back(D_phi.getProof()); in queryTCC()
131 u.push_back(t.getProof()); in implIntro3()
143 pfs.push_back(i->getProof()); in implIntro3()
363 pfs.push_back(thm1.getProof()); in substitutivityRule()
364 pfs.push_back(thm2.getProof()); in substitutivityRule()
497 pfs.push_back(i->getProof()); in substitutivityRule()
572 pfs.push_back(e.getProof()); in contradictionRule()
683 pfs.push_back(e1.getProof()); in iffMP()
709 pfs.push_back(e1.getProof()); in implMP()
[all …]
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | arith_theorem_producer3.cpp | 1622 pfs.push_back(aLEt.getProof()); in finiteInterval()
1839 grayShadow.getProof()); in expandGrayShadow0()
1964 gThm.getProof()); in expandGrayShadowConst()
1969 gThm.getProof()); in expandGrayShadowConst()
1974 gThm.getProof()); in expandGrayShadowConst()
2075 pfs.push_back(less.getProof()); in lessThanToLE()
2583 pfs.push_back(eqn.getProof()); in eqElimIntRule()
2635 pfs.push_back(thm.getProof()); in equalLeaves1()
2664 pfs.push_back(thm.getProof()); in equalLeaves2()
2693 pfs.push_back(thm.getProof()); in equalLeaves3()
[all …]
|
| H A D | arith_theorem_producer_old.cpp | 1820 pfs.push_back(aLEt.getProof()); in finiteInterval()
2042 grayShadow.getProof()); in expandGrayShadow0()
2166 gThm.getProof()); in expandGrayShadowConst()
2171 gThm.getProof()); in expandGrayShadowConst()
2176 gThm.getProof()); in expandGrayShadowConst()
2277 pfs.push_back(less.getProof()); in lessThanToLE()
2785 pfs.push_back(eqn.getProof()); in eqElimIntRule()
2837 pfs.push_back(thm.getProof()); in equalLeaves1()
2866 pfs.push_back(thm.getProof()); in equalLeaves2()
2895 pfs.push_back(thm.getProof()); in equalLeaves3()
[all …]
|
| H A D | arith_theorem_producer.cpp | 1665 pfs.push_back(aLEt.getProof()); in finiteInterval()
1882 grayShadow.getProof()); in expandGrayShadow0()
2006 gThm.getProof()); in expandGrayShadowConst()
2011 gThm.getProof()); in expandGrayShadowConst()
2016 gThm.getProof()); in expandGrayShadowConst()
2118 pfs.push_back(less.getProof()); in lessThanToLE()
2608 pfs.push_back(eqn.getProof()); in eqElimIntRule()
2660 pfs.push_back(thm.getProof()); in equalLeaves1()
2689 pfs.push_back(thm.getProof()); in equalLeaves2()
2718 pfs.push_back(thm.getProof()); in equalLeaves3()
[all …]
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_uf/ |
| H A D | uf_theorem_producer.cpp | 66 pf = newPf("rel_closure", rel.getProof()); in relToClosure()
106 pfs.push_back(t1.getProof()); in relTrans()
107 pfs.push_back(t2.getProof()); in relTrans()
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_quant/ |
| H A D | quant_theorem_producer.cpp | 210 pfs.push_back(t1.getProof()); in universalInst()
302 pfs.push_back(t1.getProof()); in universalInst()
375 pfs.push_back(t1.getProof()); in universalInst()
442 pfs.push_back(t1.getProof()); in partialUniversalInst()
557 pfs.push_back(t1.getProof()); in adjustVarUniv()
599 pfs.push_back(t1.getProof()); in packVar()
648 pfs.push_back(t1.getProof()); in pullVarOut()
681 pfs.push_back(t1.getProof()); in pullVarOut()
721 pfs.push_back(t1.getProof()); in pullVarOut()
780 pfs.push_back(t1.getProof()); in boundVarElim()
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/ |
| H A D | Control.hs | 39 , getProof
91 … , getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3
|
| /dports/databases/mongodb36/mongodb-src-r3.6.23/src/mongo/rpc/metadata/ |
| H A D | logical_time_metadata.cpp | 112 invariant(_clusterTime.getProof()); in writeToMetadata()
113 _clusterTime.getProof()->appendAsBinData(signatureObjBuilder, kSignatureHashFieldName); in writeToMetadata()
|
| /dports/security/certmgr/certmgr-3.0.3/vendor/github.com/google/certificate-transparency-go/certificate-transparency-go-1.0.21/dnsclient/ |
| H A D | dnsclient.go | 151 return c.getProof(ctx, fmt.Sprintf("%d.%d.sth-consistency.%s", first, second, c.base))
171 proof, err := c.getProof(ctx, fmt.Sprintf("%d.%d.tree.%s", leafIndex, treeSize, c.base))
184 func (c *DNSClient) getProof(ctx context.Context, base string) ([][]byte, error) { func
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | theorem.h | 194 Proof getProof() const;
370 Proof getProof() const { return d_thm.getProof(); } in getProof() function
|
| H A D | dpllt_minisat.h | 99 SatProof* getProof() { in getProof() function
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Control/ |
| H A D | BaseIO.hs | 224 getProof :: Query String
225 getProof = Trans.getProof function
|
| /dports/databases/mongodb36/mongodb-src-r3.6.23/src/mongo/rpc/ |
| H A D | metadata.cpp | 105 (!signedTime.getProof() || *signedTime.getProof() == TimeProofService::TimeProof())) { in readRequestMetadata()
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_array/ |
| H A D | array_theorem_producer.cpp | 235 pf = newPf("rewriteRedundantWrite1", write, r_eq_v.getProof()); in rewriteRedundantWrite1()
352 pf = newPf("array_not_eq", e.getProof()); in arrayNotEq()
397 pf = newPf("propagateIndexDiseq", read1eqread2isFalse.getProof()); in propagateIndexDiseq()
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Trans/ |
| H A D | Control.hs | 37 , getProof
|