| /dports/math/vampire/vampire-4.5.1/FMB/ |
| H A D | FunctionRelationshipInference.cpp | 215 ClauseList* newClauses = 0; in getCheckingClauses() local
245 addClaimForFunction(x,y,fx,fy,f,arg_srt,ret_srt,0,newClauses); in getCheckingClauses()
280 addClaimForFunction(x,y,fx,fy,f,arg_srt,ret_srt,existential,newClauses); in getCheckingClauses()
285 return newClauses; in getCheckingClauses()
292 ClauseList*& newClauses) in addClaimForFunction() argument
326 addClaim(injective,newClauses); in addClaimForFunction()
327 addClaim(surjective,newClauses); in addClaimForFunction()
328 addClaim(ing_and_nons,newClauses); in addClaimForFunction()
329 addClaim(sur_and_noni,newClauses); in addClaimForFunction()
332 void FunctionRelationshipInference::addClaim(Formula* conjecture, ClauseList*& newClauses) in addClaim() argument
[all …]
|
| H A D | FunctionRelationshipInference.hpp | 59 ClauseList*& newClauses);
61 void addClaim(Formula* conjecture, ClauseList*& newClauses);
|
| /dports/textproc/luceneplusplus/LucenePlusPlus-rel_3.0.8/src/core/search/spans/ |
| H A D | SpanNearQuery.cpp | 106 Collection<SpanQueryPtr> newClauses(Collection<SpanQueryPtr>::newInstance(sz)); in clone() local
109 newClauses[i] = boost::dynamic_pointer_cast<SpanQuery>(clauses[i]->clone()); in clone()
112 SpanNearQueryPtr spanNearQuery(newLucene<SpanNearQuery>(newClauses, slop, inOrder)); in clone()
|
| H A D | SpanOrQuery.cpp | 47 Collection<SpanQueryPtr> newClauses(Collection<SpanQueryPtr>::newInstance(sz)); in clone() local
50 newClauses[i] = boost::dynamic_pointer_cast<SpanQuery>(clauses[i]->clone()); in clone()
53 SpanOrQueryPtr spanOrQuery(newLucene<SpanOrQuery>(newClauses)); in clone()
|
| /dports/devel/splint/splint-3.1.2/src/ |
| H A D | stateClauseList.c | 419 stateClauseList newClauses = uentry_getStateClauseList (unew); in stateClauseList_checkEqual() local
421 if (stateClauseList_isDefined (newClauses)) in stateClauseList_checkEqual()
423 stateClauseList_elements (newClauses, cl) in stateClauseList_checkEqual()
458 sRefSet sc = stateClauseList_getClause (newClauses, cl); in stateClauseList_checkEqual()
|
| /dports/lang/mono/mono-5.10.1.57/external/api-doc-tools/external/Lucene.Net.Light/src/core/Search/Spans/ |
| H A D | SpanNearQuery.cs | 170 SpanQuery[] newClauses = new SpanQuery[sz]; in Clone()
175 newClauses[i] = (SpanQuery) clause.Clone(); in Clone()
177 SpanNearQuery spanNearQuery = new SpanNearQuery(newClauses, internalSlop, inOrder); in Clone()
|
| H A D | SpanOrQuery.cs | 212 SpanQuery[] newClauses = new SpanQuery[sz]; in Clone()
216 newClauses[i] = (SpanQuery) clauses[i].Clone(); in Clone()
218 SpanOrQuery soq = new SpanOrQuery(newClauses); in Clone()
|
| /dports/textproc/luceneplusplus/LucenePlusPlus-rel_3.0.8/src/core/search/payloads/ |
| H A D | PayloadNearQuery.cpp | 38 Collection<SpanQueryPtr> newClauses(Collection<SpanQueryPtr>::newInstance(sz)); in clone() local
41 newClauses[i] = boost::dynamic_pointer_cast<SpanQuery>(clauses[i]->clone()); in clone()
44 PayloadNearQueryPtr payloadNearQuery(newLucene<PayloadNearQuery>(newClauses, slop, inOrder)); in clone()
|
| /dports/lang/mono/mono-5.10.1.57/external/api-doc-tools/external/Lucene.Net.Light/src/core/Search/Payloads/ |
| H A D | PayloadNearQuery.cs | 75 SpanQuery[] newClauses = new SpanQuery[sz]; in Clone()
79 newClauses[i] = clauses[i]; in Clone()
81 PayloadNearQuery boostingNearQuery = new PayloadNearQuery(newClauses, internalSlop, inOrder); in Clone()
|
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | occsimplifier.h | 118 uint64_t newClauses = 0; in _111()
133 << " cl-new: " << newClauses in _111()
164 , newClauses in _111()
|
| H A D | occsimplifier.cpp | 2553 bvestats.newClauses++; in add_varelim_resolvent()
3267 newClauses += other.newClauses; in operator +=()
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | occsimplifier.h | 118 uint64_t newClauses = 0; member
133 << " cl-new: " << newClauses in print()
164 , newClauses in print()
|
| H A D | occsimplifier.cpp | 2553 bvestats.newClauses++; in add_varelim_resolvent()
3267 newClauses += other.newClauses; in operator +=()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | symmetry_breaker.h | 168 void apply(std::vector<Node>& newClauses);
|
| H A D | theory_uf.cpp | 433 vector<Node> newClauses; in presolve() local
434 d_symb.apply(newClauses); in presolve()
435 for(vector<Node>::const_iterator i = newClauses.begin(); in presolve()
436 i != newClauses.end(); in presolve()
|
| H A D | symmetry_breaker.cpp | 459 void SymmetryBreaker::apply(std::vector<Node>& newClauses) { in apply() argument
554 newClauses.push_back(d); in apply()
|
| /dports/math/fricas/fricas-1.3.7/src/doc/ |
| H A D | api.spad | 804 newClauses: List List L := empty()
810 newClauses := cons(clause, newClauses)
813 for c in newClauses repeat
|