| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | constraint.h | 459 void setAssertedToTheTheory(TNode witness, bool inConflict);
482 void setAssumption(bool inConflict);
531 void setInternalAssumption(bool inConflict);
623 inline bool inConflict() const { in inConflict() function
656 void impliedByUnate(ConstraintCP a, bool inConflict);
665 void impliedByIntHole(ConstraintCP a, bool inConflict);
674 void impliedByIntHole(const ConstraintCPVec& b, bool inConflict);
688 void impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool inConflict);
702 void impliedByFarkas(const ConstraintCPVec& b, RationalVectorCP coeffs, bool inConflict);
|
| H A D | dio_solver.cpp | 82 Debug("queueConditions") << !inConflict() << std::endl; in queueConditions()
89 !inConflict() && in queueConditions()
261 if(!inConflict()){ in enqueueInputConstraints()
420 Assert(!inConflict()); in processEquations()
423 while(! queueEmpty() && !inConflict()){ in processEquations()
430 Assert(!inConflict()); in processEquations()
474 return inConflict(); in processEquations()
481 Assert(!inConflict()); in processEquationsForConflict()
494 Assert(!inConflict()); in processEquationsForCut()
786 for(; readIter < N && !inConflict(); ++readIter){ in subAndReduceCurrentFByIndex()
[all …]
|
| H A D | dio_solver.h | 227 bool inConflict() const { return d_conflictIndex.isSet(); } in inConflict() function
231 Assert(!inConflict()); in raiseConflict()
237 Assert(inConflict()); in getConflictIndex()
|
| H A D | constraint.cpp | 1112 Assert(inConflict() == nowInConflict); in setAssumption()
1113 if(Debug.isOn("constraint::conflictCommit") && inConflict()){ in setAssumption()
1175 Assert(inConflict() == nowInConflict); in impliedByUnate()
1176 if(Debug.isOn("constraint::conflictCommit") && inConflict()){ in impliedByUnate()
1201 Assert(inConflict() == nowInConflict); in impliedByTrichotomy()
1202 if(Debug.isOn("constraint::conflictCommit") && inConflict()){ in impliedByTrichotomy()
1229 Assert(inConflict() == nowInConflict); in impliedByIntHole()
1258 Assert(inConflict() == nowInConflict); in impliedByIntHole()
1309 Assert(inConflict() == nowInConflict); in impliedByFarkas()
1329 Assert(inConflict() == nowInConflict); in setInternalAssumption()
[all …]
|
| H A D | congruence_manager.cpp | 130 Assert(!inConflict()); in raiseConflict()
135 bool ArithCongruenceManager::inConflict() const{ in inConflict() function in CVC4::theory::arith::ArithCongruenceManager
235 if(inConflict()){ in propagate()
475 while(! inConflict() && d_eqi_counter.get()<d_eq_infer->getNumPendingMerges() ) { in fixpointInfer()
517 return inConflict(); in fixpointInfer()
|
| H A D | callbacks.cpp | 65 Assert(c->inConflict()); in raiseConflict()
159 Assert( not_c->inConflict() ); in commitConflict()
|
| H A D | congruence_manager.h | 110 bool inConflict() const;
|
| /dports/devel/pear-PHP_CodeSniffer/PHP_CodeSniffer-3.6.1/src/ |
| H A D | Fixer.php | 99 private $inConflict = false; variable in PHP_CodeSniffer\\Fixer
171 $this->inConflict = false;
192 if ($this->numFixes === 0 && $this->inConflict === false) {
356 if ($this->inConflict === true) {
388 if ($this->inConflict === true) {
437 $this->inConflict = false;
476 if ($this->inConflict === true) {
558 $this->inConflict = true;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | model_engine.cpp | 78 Assert( !d_quantEngine->inConflict() ); in check()
227 if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ in checkModel()
237 Assert( !d_quantEngine->inConflict() ); in checkModel()
242 if( d_quantEngine->inConflict() ){ in checkModel()
302 if( d_quantEngine->inConflict() ){ in exhaustiveInstantiate()
|
| /dports/editors/kate/kate-21.12.3/addons/project/git/ |
| H A D | gitdiff.cpp | 348 …bool inConflict = false; // This is set so that a line inside a conflict is recognized as a valid … in mapDiffLine() local
357 inConflict = true; in mapDiffLine()
366 inConflict = true; in mapDiffLine()
371 inConflict = false; in mapDiffLine()
382 … if (ln.startsWith(dest) || ln.startsWith(QLatin1Char(' ')) || ln.isEmpty() || inConflict) { in mapDiffLine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
| H A D | instantiation_engine.cpp | 84 …") << " -> status is " << quantStatus << ", conflict=" << d_quantEngine->inConflict() << std::endl; in doInstantiationRound()
85 if( d_quantEngine->inConflict() ){ in doInstantiationRound()
139 if( d_quantEngine->inConflict() ){ in check()
|
| H A D | inst_match_generator.cpp | 434 Assert(!qe->inConflict()); in getNextMatch()
479 if( qe->inConflict() ){ in addInstantiations()
485 if( qe->inConflict() ){ in addInstantiations()
852 if( qe->inConflict() ){ in addInstantiations()
895 Assert( !qe->inConflict() ); in processNewInstantiations()
924 if (qe->inConflict()) in processNewInstantiations()
969 if (qe->inConflict()) in processNewInstantiations()
1040 if (tat && !qe->inConflict()) in addInstantiations()
1049 if( qe->inConflict() ){ in addInstantiations()
1059 if (tat && !qe->inConflict()) in addInstantiations()
[all …]
|
| H A D | inst_strategy_e_matching.cpp | 116 if( d_quantEngine->inConflict() ){ in process()
259 if( d_quantEngine->inConflict() ){ in process()
265 if( d_quantEngine->inConflict() || ( hasInst && options::multiTriggerPriority() ) ){ in process()
|
| /dports/math/stp/stp-2.3.3/include/stp/Simplifier/constantBitP/multiplication/ |
| H A D | ColumnCounts.h | 155 bool inConflict() in inConflict() function
165 if (inConflict()) in fixedPoint()
191 if (inConflict()) in fixedPoint()
|
| /dports/devel/kdevelop/kdevelop-21.12.3/kdevplatform/vcs/ |
| H A D | vcsdiff.cpp | 327 …bool inConflict = false; // This is set so that a line inside a conflict is recognized as a valid … in mapDiffLine() local
336 inConflict = true; in mapDiffLine()
345 inConflict = true; in mapDiffLine()
350 inConflict = false; in mapDiffLine()
361 … if (ln.startsWith(dest) || ln.startsWith(QLatin1Char(' ')) || ln.isEmpty() || inConflict) { in mapDiffLine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | rewrite_engine.cpp | 77 Assert( !d_quantEngine->inConflict() ); in check()
104 while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) { in check()
133 while( !d_quantEngine->inConflict() && qi->getNextMatch( qcf ) && in checkRewriteRule()
142 …while( !d_quantEngine->inConflict() && tempAddedLemmas==0 && success && ( addedLemmas==0 || !optio… in checkRewriteRule()
|
| H A D | inst_strategy_enumerative.cpp | 95 if (d_quantEngine->inConflict()) in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | bv_subtheory_bitblast.cpp | 154 if (!d_bv->inConflict() in check()
191 Assert(!d_bv->inConflict()); in check()
230 Assert(!d_bv->inConflict()); in check()
|
| H A D | bv_quick_check.cpp | 37 bool BVQuickCheck::inConflict() { return d_inConflict.get(); } in inConflict() function in CVC4::theory::bv::BVQuickCheck
45 Assert(!inConflict()); in setConflict()
167 d_solver->inConflict()); in selectUnsatCore()
|
| H A D | bv_subtheory_core.cpp | 178 Assert (!d_bv->inConflict()); in check()
341 …if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory… in assertFactToEqualityEngine()
363 if (d_bv->inConflict()) { in assertFactToEqualityEngine()
|
| H A D | theory_bv.cpp | 364 if (inConflict()) { in check()
382 Assert (!inConflict()); in check()
388 Assert (inConflict()); in check()
523 Assert(!inConflict()); in collectModelInfo()
539 Assert(!inConflict()); in getModelValue()
554 if (inConflict()) { in propagate()
|
| H A D | bv_quick_check.h | 51 bool inConflict();
|
| H A D | theory_bv.h | 250 bool inConflict() { in inConflict() function
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | regexp_solver.cpp | 154 if (d_parent.inConflict()) in check()
160 if (!d_parent.inConflict() && !spflag) in check()
274 if (d_parent.inConflict()) in check()
282 if (!d_parent.inConflict()) in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | inst_strategy_cegqi.cpp | 290 Assert( !d_quantEngine->inConflict() ); in check()
306 if( d_quantEngine->inConflict() ){ in check()
314 if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ in check()
|