Home
last modified time | relevance | path

Searched refs:premise (Results 1 – 25 of 869) sorted by relevance

12345678910>>...35

/dports/math/vampire/vampire-4.5.1/Shell/
H A DInterpolantsNew.cpp104 Unit* premise = parents.next(); in removeTheoryInferences() local
129 Unit* premise = parents.next(); in removeTheoryInferences() local
136 premise->decRefCnt(); in removeTheoryInferences()
250 … ASS(splittingFunction.at(premise) == COLOR_LEFT || splittingFunction.at(premise) == COLOR_RIGHT); in computeBoundary()
268 … ASS(splittingFunction.at(premise) == COLOR_LEFT || splittingFunction.at(premise) == COLOR_RIGHT); in computeBoundary()
463 Unit* premise= parents.next(); in computeSplittingFunction() local
465 if (premise->getColor() == COLOR_LEFT || premise->getColor() == COLOR_RIGHT) in computeSplittingFunction()
488 Unit* premise= parents.next(); in computeSplittingFunction() local
490 … ASS(splittingFunction.at(premise) == COLOR_LEFT || splittingFunction.at(premise) == COLOR_RIGHT); in computeSplittingFunction()
628 todo.push(premise); in next()
[all …]
H A DInterpolantMinimizerNew.cpp98 Unit* premise= parents.next(); in computeSplittingFunction() local
99 if (premise->getColor() == COLOR_LEFT) in computeSplittingFunction()
103 else if (premise->getColor() == COLOR_RIGHT) in computeSplittingFunction()
116 Unit* premise= parents.next(); in computeSplittingFunction() local
118 expr& x_j = *unitsToExpressions.at(premise); in computeSplittingFunction()
119 expr& p_j = *unitsToPenalties.at(premise); in computeSplittingFunction()
252 Unit* premise= parents.next(); in analyzeLocalProof() local
254 if (splittingFunction.at(premise) != splittingFunction.at(current)) in analyzeLocalProof()
324 Unit* premise= parents.next(); in analyzeGreyAreas() local
326 if (premise->getColor() == COLOR_LEFT || premise->getColor() == COLOR_RIGHT) in analyzeGreyAreas()
[all …]
/dports/math/vampire/vampire-4.5.1/Indexing/
H A DArithmeticIndex.hpp48 void handleLiteral(Literal* lit, bool adding, Clause* premise, bool negative=false);
51 bool isNonEqual(TermList t, InterpretedType val, Clause*& premise);
53 bool isGreater(TermList t, InterpretedType val, Clause*& premise);
55 bool isLess(TermList t, InterpretedType val, Clause*& premise);
77 bool isNonEqual(TermList t, InterpretedType val, Clause*& premise)
78 { return _db.isNonEqual(t, val, premise); }
79 bool isGreater(TermList t, InterpretedType val, Clause*& premise)
80 { return _db.isGreater(t, val, premise); }
81 bool isLess(TermList t, InterpretedType val, Clause*& premise)
82 { return _db.isLess(t, val, premise); }
H A DArithmeticIndex.cpp77 premise=ci->lowerLimitPremise;
82 premise=ci->upperLimitPremise;
87 premise=neqPremise;
104 premise=ci->lowerLimitPremise;
121 premise=ci->upperLimitPremise;
176 ctr->neqConstraints.insert(num, premise);
182 if(storedPrem==premise) {
206 ctr->upperLimitPremise=premise;
215 ctr->lowerLimitPremise=premise;
222 if(premise==ctr->upperLimitPremise) {
[all …]
/dports/math/vampire/vampire-4.5.1/Inferences/
H A DInterpretedSimplifier.cpp234 premise=0;
239 if(!premise || sperf->willPerform(premise)) {
244 if(!premise || sperf->willPerform(premise)) {
258 premise=0;
263 if(!premise || sperf->willPerform(premise)) {
268 if(!premise || sperf->willPerform(premise)) {
282 premise=0;
287 if(!premise || sperf->willPerform(premise)) {
292 if(!premise || sperf->willPerform(premise)) {
301 if(premise) {
[all …]
H A DCTFwSubsAndRes.cpp64 Clause* CTFwSubsAndRes::buildSResClause(Clause* cl, unsigned resolvedIndex, Clause* premise) in buildSResClause() argument
73 Inference* inf = new Inference2(Inference::SUBSUMPTION_RESOLUTION, cl, premise); in buildSResClause()
75 max(cl->inputType(), premise->inputType()); in buildSResClause()
108 Clause* premise=res.clause; in perform() local
109 if(premise->hasAux()) { in perform()
113 premise->setAux(0); in perform()
114 if(!ColorHelper::compatible(cl->color(), premise->color())) { in perform()
118 premises = pvi( getSingletonIterator(premise)); in perform()
121 replacement=buildSResClause(cl, res.resolvedQueryLiteralIndex, premise); in perform()
H A DInduction.hpp88 ClauseIterator generateClauses(Clause* premise);
96 InductionClauseIterator(Clause* premise);
114 void process(Clause* premise, Literal* lit);
116 …void produceClauses(Clause* premise, Literal* origLit, Formula* hypothesis, Literal* conclusion, I…
118 …void performMathInductionOne(Clause* premise, Literal* origLit, Literal* lit, Term* t, InferenceRu…
119 …void performMathInductionTwo(Clause* premise, Literal* origLit, Literal* lit, Term* t, InferenceRu…
121 …void performStructInductionOne(Clause* premise, Literal* origLit, Literal* lit, Term* t, Inference…
122 …void performStructInductionTwo(Clause* premise, Literal* origLit, Literal* lit, Term* t, Inference…
123 …void performStructInductionThree(Clause* premise, Literal* origLit, Literal* lit, Term* t, Inferen…
H A DFactoring.cpp183 ClauseIterator Factoring::generateClauses(Clause* premise) in generateClauses() argument
187 if(premise->length()<=1) { in generateClauses()
190 …if(premise->numSelected()==1 && _salg->getLiteralSelector().isNegativeForSelection((*premise)[0]))… in generateClauses()
194 auto it1 = getCombinationIterator(0u,premise->numSelected(),premise->length()); in generateClauses()
196 …auto it2 = getMapAndFlattenIterator(it1,UnificationsOnPositiveFn(premise,_salg->getLiteralSelector… in generateClauses()
198 auto it3 = getMappingIterator(it2,ResultsFn(premise, in generateClauses()
H A DFOOLParamodulation.cpp43 ClauseIterator FOOLParamodulation::generateClauses(Clause* premise) { in generateClauses() argument
81 ArrayishObjectIterator<Clause> literals = premise->getSelectedLiteralIterator(); in generateClauses()
123 unsigned conclusionLength = premise->length() + 1; in generateClauses()
125 GeneratingInference1(InferenceRule::FOOL_PARAMODULATION, premise)); in generateClauses()
130 …usion)[i] = i == literalPosition ? EqHelper::replace((*premise)[i], booleanTerm, troo) : (*premise… in generateClauses()
H A DInduction.cpp113 ClauseIterator Induction::generateClauses(Clause* premise) in generateClauses() argument
117 return pvi(InductionClauseIterator(premise)); in generateClauses()
120 InductionClauseIterator::InductionClauseIterator(Clause* premise) in InductionClauseIterator() argument
132 if((!unitOnly || premise->length()==1) && in InductionClauseIterator()
134 (maxD == 0 || premise->inference().inductionDepth() < maxD) in InductionClauseIterator()
137 for(unsigned i=0;i<premise->length();i++){ in InductionClauseIterator()
138 process(premise,(*premise)[i]); in InductionClauseIterator()
144 void InductionClauseIterator::process(Clause* premise, Literal* lit) in process() argument
264 inf.setInductionDepth(premise->inference().inductionDepth()+1); in produceClauses()
277 SLQueryResult qr(origLit,premise,identity); in produceClauses()
[all …]
H A DEqualityFactoring.cpp177 ClauseIterator EqualityFactoring::generateClauses(Clause* premise) in generateClauses() argument
181 if(premise->length()<=1) { in generateClauses()
184 ASS(premise->numSelected()>0); in generateClauses()
186 auto it1 = premise->getSelectedLiteralIterator(); in generateClauses()
192 auto it4 = getMapAndFlattenIterator(it3,FactorablePairsFn(premise)); in generateClauses()
194 auto it5 = getMappingIterator(it4,ResultFn(premise, in generateClauses()
H A DInferenceEngine.hpp105 virtual ClauseIterator generateClauses(Clause* premise) = 0;
172 virtual void perform(Clause* premise, BwSimplificationRecordIterator& simplifications) = 0;
183 ClauseIterator generateClauses(Clause* premise) in generateClauses() argument
262 ClauseIterator generateClauses(Clause* premise);
H A DEqualityResolution.cpp180 ClauseIterator EqualityResolution::generateClauses(Clause* premise) in generateClauses() argument
184 if(premise->isEmpty()) { in generateClauses()
187 ASS(premise->numSelected()>0); in generateClauses()
189 auto it1 = premise->getSelectedLiteralIterator(); in generateClauses()
193 auto it3 = getMappingIterator(it2,ResultFn(premise, in generateClauses()
/dports/games/brainparty/brainparty/
H A Dsymboliclogic.cpp122 switch (premise->Type) { in FlattenPremise()
124 result << "All " << premise->Job << "s " << premise->Item->PluralDesc; in FlattenPremise()
128 result << "No " << premise->Job << " " << premise->Item->SingularDesc; in FlattenPremise()
132 result << "All " << premise->Item->Noun << " are " << premise->Job << "s"; in FlattenPremise()
136 result << "No " << premise->Item->Noun << " are " << premise->Job << "s"; in FlattenPremise()
140 if (premise->Item == NULL) { in FlattenPremise()
141 if (TheGame->StartsWithVowel(&premise->Job)) { in FlattenPremise()
142 result << premise->Text << " is an " << premise->Job; in FlattenPremise()
144 result << premise->Text << " is a " << premise->Job; in FlattenPremise()
147 result << premise->Text << " " << premise->Item->SingularDesc; in FlattenPremise()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/muz/spacer/
H A Dspacer_unsat_core_plugin.cpp83 if (m_ctx.is_b_open(premise)) in add_lowest_split_to_core()
84 todo.push_back(premise); in add_lowest_split_to_core()
152 if (m_ctx.is_b_open (premise)) { in compute_partial_core()
153 SASSERT(!m_ctx.is_a(premise)); in compute_partial_core()
155 if (m_ctx.is_b_pure (premise)) { in compute_partial_core()
197 expr* premise = args[i]; in compute_partial_core() local
266 if (m_ctx.is_b(premise) && !m_ctx.is_closed(premise)) in compute_partial_core()
268 SASSERT(!m_ctx.is_a(premise)); in compute_partial_core()
270 if (m_ctx.is_b_pure(premise)) in compute_partial_core()
541 if (m_ctx.is_b(premise)) { in advance_to_lowest_partial_cut()
[all …]
H A Dspacer_iuc_proof.cpp131 proof* premise = to_app(cur->get_arg(i)); in compute_marks() local
133 need_to_mark_a |= m_a_mark.is_marked(premise); in compute_marks()
134 need_to_mark_b |= m_b_mark.is_marked(premise); in compute_marks()
135 need_to_mark_h |= m_h_mark.is_marked(premise); in compute_marks()
178 proof* premise = to_app(cur->get_arg(i)); in dump_farkas_stats() local
179 if (!is_a_marked(premise) && is_b_marked(premise)) { in dump_farkas_stats()
271 proof* premise = to_app(curr->get_arg(i-1)); in display_dot() local
272 unsigned pid = ids.at(premise->get_id()); in display_dot()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/
H A Dspacer_unsat_core_plugin.cpp83 if (m_ctx.is_b_open(premise)) in add_lowest_split_to_core()
84 todo.push_back(premise); in add_lowest_split_to_core()
152 if (m_ctx.is_b_open (premise)) { in compute_partial_core()
153 SASSERT(!m_ctx.is_a(premise)); in compute_partial_core()
155 if (m_ctx.is_b_pure (premise)) { in compute_partial_core()
197 expr* premise = args[i]; in compute_partial_core() local
266 if (m_ctx.is_b(premise) && !m_ctx.is_closed(premise)) in compute_partial_core()
268 SASSERT(!m_ctx.is_a(premise)); in compute_partial_core()
270 if (m_ctx.is_b_pure(premise)) in compute_partial_core()
541 if (m_ctx.is_b(premise)) { in advance_to_lowest_partial_cut()
[all …]
H A Dspacer_iuc_proof.cpp131 proof* premise = to_app(cur->get_arg(i)); in compute_marks() local
133 need_to_mark_a |= m_a_mark.is_marked(premise); in compute_marks()
134 need_to_mark_b |= m_b_mark.is_marked(premise); in compute_marks()
135 need_to_mark_h |= m_h_mark.is_marked(premise); in compute_marks()
178 proof* premise = to_app(cur->get_arg(i)); in dump_farkas_stats() local
179 if (!is_a_marked(premise) && is_b_marked(premise)) { in dump_farkas_stats()
271 proof* premise = to_app(curr->get_arg(i-1)); in display_dot() local
272 unsigned pid = ids.at(premise->get_id()); in display_dot()
/dports/math/z3/z3-z3-4.8.13/src/muz/base/
H A Dhnf.cpp226 SASSERT(!premise || fml == m.get_fact(premise)); in mk_horn()
236 if (premise){ in mk_horn()
240 premise = mk_modus_ponens(premise, p1); in mk_horn()
244 premise = mk_modus_ponens(premise, m.mk_rewrite(fml, fml1)); in mk_horn()
248 SASSERT(!premise || (fml1 == fml && fml == m.get_fact(premise))); in mk_horn()
255 if (premise) { in mk_horn()
275 if (premise) { in mk_horn()
302 if (premise) { in mk_horn()
305 premise = mk_modus_ponens(premise, p); in mk_horn()
482 result = m.mk_modus_ponens(premise, eq); in mk_modus_ponens()
[all …]
H A Ddl_boogie_proof.cpp94 proof* premise = premises[i].get(); in mk_input_resolution() local
97 if (!m.is_implies(premise, l1, l2)) { in mk_input_resolution()
103 premises2.push_back(premise); in mk_input_resolution()
167 proof* premise = premises[i].get(); in pp_proof() local
169 if (!index.find(premise, position)) { in pp_proof()
171 rules.push_back(premise); in pp_proof()
173 index.insert(premise, position); in pp_proof()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/
H A Dhnf.cpp227 SASSERT(!premise || fml == m.get_fact(premise)); in mk_horn()
237 if (premise){ in mk_horn()
241 premise = mk_modus_ponens(premise, p1); in mk_horn()
245 premise = mk_modus_ponens(premise, m.mk_rewrite(fml, fml1)); in mk_horn()
249 SASSERT(!premise || (fml1 == fml && fml == m.get_fact(premise))); in mk_horn()
256 if (premise) { in mk_horn()
276 if (premise) { in mk_horn()
303 if (premise) { in mk_horn()
306 premise = mk_modus_ponens(premise, p); in mk_horn()
483 result = m.mk_modus_ponens(premise, eq); in mk_modus_ponens()
[all …]
/dports/math/vampire/vampire-4.5.1/Test/
H A DCheckedFwSimplifier.cpp52 bool willPerform(Clause* premise) in willPerform()
58 _resultSet.insert(premise); in willPerform()
59 _resultsOfFirst.push(premise); in willPerform()
63 _resultsOfSecond.push(premise); in willPerform()
64 if(!_resultSet.remove(premise)) { in willPerform()
68 cout<<"result: "<<premise->toString()<<endl; in willPerform()
/dports/lang/racket/racket-8.3/share/pkgs/redex-lib/redex/private/
H A Dmodeless-jf.rkt51 premise-repeat-names
57 [premise-repeat-names '()]
89 premise-repeat-names
101 (cons #f premise-repeat-names)
113 premise-repeat-names
251 '(#,@premise-repeat-names)
444 premise-jf-procs
506 (let loop ([premise-jf-procs premise-jf-procs]
511 [((cons premise-jf-proc premise-jf-procs)
520 (loop premise-jf-procs
[all …]
/dports/math/vampire/vampire-4.5.1/Kernel/
H A DInference.cpp314 _ptr1 = premise; in init1()
317 premise->incRefCnt(); in init1()
397 init1(ft.rule,ft.premise); in Inference()
400 ASS(!ft.premise->isClause()); in Inference()
420 init1(gi.rule,gi.premise); in Inference()
423 ASS(gi.premise->isClause()); in Inference()
425 _age = gi.premise->age()+1; in Inference()
460 init1(si.rule,si.premise); in Inference()
463 ASS(si.premise->isClause()); in Inference()
465 _age = si.premise->age(); in Inference()
[all …]
H A DInference.hpp498 FormulaTransformation(InferenceRule r, Unit* p) : rule(r), premise(p) {} in FormulaTransformation()
500 Unit* premise; member
510 SimplifyingInference1(InferenceRule r, Clause* main_premise) : rule(r), premise(main_premise) {} in SimplifyingInference1()
512 Clause* premise; member
530 GeneratingInference1(InferenceRule r, Clause* p) : rule(r), premise(p) {} in GeneratingInference1()
532 Clause* premise; member
555 NonspecificInference1(InferenceRule r, Unit* p) : rule(r), premise(p) {} in NonspecificInference1()
557 Unit* premise; member
604 void init1(InferenceRule r, Unit* premise);

12345678910>>...35