| /dports/math/vampire/vampire-4.5.1/Inferences/ |
| H A D | InterpretedEvaluation.cpp | 106 static DArray<Literal*> newLits(32); in simplify() local
109 newLits.ensure(clen); in simplify()
118 newLits[next++]=lit; in simplify()
132 newLits[next++]=res; in simplify()
153 newLits.expand(clen+sideConditions.length()); in simplify()
154 while(side.hasNext()){ newLits[next++]=side.next();} in simplify()
159 (*res)[i] = newLits[i]; in simplify()
|
| H A D | Condensation.cpp | 65 static DArray<Literal*> newLits(32); in simplify() local
85 newLits.ensure(newLen); in simplify()
100 newLits[next] = lit; in simplify()
119 newLits[next] = lit; in simplify()
134 success=MLMatcher::canBeMatched(newLits.array(), newLen, cl,alts.array(),0,false); in simplify()
148 (*res)[i] = newLits[i]; in simplify()
|
| H A D | InferenceEngine.cpp | 277 static DHSet<Literal*> newLits; in simplify() local
278 newLits.reset(); in simplify()
280 newLits.loadFromIterator(Clause::Iterator(*d)); in simplify()
281 ASS_EQ(origLits.size(),newLits.size()); in simplify()
|
| /dports/math/vampire/vampire-4.5.1/Shell/ |
| H A D | TheoryFlattening.cpp | 158 Stack<Literal*> newLits; in apply() local
159 Literal* nlit = replaceTopTerms(lit,newLits,maxVar,abstracted); in apply()
161 ASS(newLits.isEmpty()); in apply()
170 lits.loadFromIterator(Stack<Literal*>::Iterator(newLits)); in apply()
174 result.loadFromIterator(Stack<Literal*>::Iterator(newLits)); in apply()
191 Literal* TheoryFlattening::replaceTopTerms(Literal* lit, Stack<Literal*>& newLits,unsigned& maxVar, in replaceTopTerms() argument
245 newLits.push(lit); in replaceTopTerms()
251 Term* tt = replaceTopTermsInTerm(t,newLits,maxVar,interpreted,abstracted); in replaceTopTerms()
266 Term* TheoryFlattening::replaceTopTermsInTerm(Term* term, Stack<Literal*>& newLits, in replaceTopTermsInTerm() argument
314 newLits.push(lit); in replaceTopTermsInTerm()
[all …]
|
| H A D | TheoryFlattening.hpp | 53 Literal* replaceTopTerms(Literal* lit, Stack<Literal*>& newLits,unsigned& maxVar,
55 Term* replaceTopTermsInTerm(Term* term, Stack<Literal*>& newLits,
|
| /dports/math/cvc3/cvc3-2.4.1/src/sat/ |
| H A D | cnf_manager.cpp | 550 void CNF_Manager::cons(unsigned lb, unsigned ub, const Expr& e2, vector<unsigned>& newLits) in cons() argument
553 newLits.push_back(lb); in cons()
566 cons(new_lb, ub, e2, newLits); in cons()
578 cons(lb, new_ub, e2, newLits); in cons()
582 cons(new_lb, ub, e2, newLits); in cons()
585 for (index = 0; index < newLits.size(); ++index) { in cons()
586 d_vc->assertFormula(e2[newLits[index]].negate()); in cons()
588 cons(lb, new_ub, e2, newLits); in cons()
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | cnf_manager.h | 245 void cons(unsigned lb, unsigned ub, const CVC3::Expr& e2, std::vector<unsigned>& newLits);
|
| /dports/math/clingo/clingo-5.5.1/clasp/src/ |
| H A D | cb_enumerator.cpp | 48 void release(SharedLiterals* newLits) { in release() argument
51 current = newLits; in release()
|
| /dports/math/clasp/clasp-3.3.5/src/ |
| H A D | cb_enumerator.cpp | 48 void release(SharedLiterals* newLits) { in release() argument
51 current = newLits; in release()
|
| /dports/math/clingo/clingo-5.5.1/clasp/clasp-da10954/src/ |
| H A D | cb_enumerator.cpp | 48 void release(SharedLiterals* newLits) { in release() argument
51 current = newLits; in release()
|