| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | theory_arrays.cpp | 393 …Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal <… in propagate()
402 if (d_inCheckModel && getSatContext()->getLevel() != d_topLevel) { in propagate()
711 Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); in preRegisterTermInternal()
712 while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) { in preRegisterTermInternal()
854 Debug("arrays") << spaces(getSatContext()->getLevel()) in explain()
987 Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); in computeCareGraph()
988 while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) { in computeCareGraph()
1500 Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; in check()
1519 Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; in check()
1601 Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; in setNonLinear()
[all …]
|
| H A D | theory_arrays.h | 281 …Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNoti… in eqNotifyTriggerEquality()
292 …Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNoti… in eqNotifyTriggerPredicate()
306 …Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNoti… in eqNotifyTriggerTermEquality()
328 …Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNoti… in eqNotifyConstantTermMerge()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | theory_arith_private.h | 652 inline context::Context* getSatContext() const { return d_containing.getSatContext(); } in getSatContext() function
|
| H A D | theory_arith_private.cpp | 1761 Debug("arith::arithvar") << "@" << getSatContext()->getLevel() in requestArithVar()
1843 context::Context::ScopedPush speculativePush(getSatContext()); in dioCutting()
2224 int level = getSatContext()->getLevel(); in attemptSolveInteger()
2249 d_lastContextIntegerAttempted = getSatContext()->getLevel(); in attemptSolveInteger()
2287 context::Context::ScopedPush speculativePush(getSatContext()); in replayLog()
2518 context::Context::ScopedPush speculativePush(getSatContext()); in tryBranchCut()
2663 context::Context::ScopedPush speculativePush(getSatContext()); in replayLogRec()
3095 int level = getSatContext()->getLevel(); in solveInteger()
4063 Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl; in explain()
4130 Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c << endl; in propagate()
[all …]
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | ext_theory.cpp | 33 d_ext_func_terms(p->getSatContext()), in ExtTheory()
35 d_has_extf(p->getSatContext()), in ExtTheory()
|
| H A D | quantifiers_engine.h | 99 context::Context* getSatContext();
|
| H A D | theory.h | 365 context::Context* getSatContext() const { in getSatContext() function
|
| H A D | quantifiers_engine.cpp | 264 context::Context* QuantifiersEngine::getSatContext() in getSatContext() function in QuantifiersEngine
266 return d_te->theoryOf(THEORY_QUANTIFIERS)->getSatContext(); in getSatContext()
|
| H A D | theory_engine.h | 524 inline context::Context* getSatContext() const { in getSatContext() function
|
| H A D | theory_engine.cpp | 225 …d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master"… in finishInit()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | theory_bv.h | 244 std::string indentStr(getSatContext()->getLevel(), ' '); in indent()
|
| H A D | theory_bv.cpp | 831 …Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::stor… in storePropagation()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf_strong_solver.cpp | 186 d_nodes[n] = new RegionNodeInfo( d_cf->d_thss->getSatContext() ); in setRep()
547 d_regions.push_back( new Region( this, d_thss->getSatContext() ) ); in newEqClass()
1356 context::Context* StrongSolverTheoryUF::getSatContext() { in getSatContext() function in CVC4::theory::uf::StrongSolverTheoryUF
1357 return d_th->getSatContext(); in getSatContext()
1659 rm = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this ); in preRegisterTerm()
|
| H A D | theory_uf_strong_solver.h | 371 context::Context* getSatContext();
|
| H A D | theory_uf.cpp | 88 d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this); in finishInit()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | inst_strategy_cegqi.cpp | 58 d_elim_quants(qe->getSatContext()), in InstStrategyCegqi()
191 d_quantEngine->getSatContext(), in registerCbqiLemma()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_conjecture.cpp | 208 d_qe->getSatContext(), in assign()
245 d_qe->getSatContext(), d_qe->getValuation())); in assign()
|
| H A D | cegis_unif.cpp | 395 : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()), in CegisUnifEnumDecisionStrategy()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | datatypes_sygus.cpp | 1304 d_td->getSatContext(), in registerSizeTerm()
1387 m, d_td->getSatContext(), d_td->getValuation())); in registerMeasureTerm()
|
| H A D | theory_datatypes.cpp | 104 ei = new EqcInfo( getSatContext() ); in getOrMakeEqcInfo()
548 new SygusSymBreakNew(this, getQuantifiersEngine(), getSatContext()); in finishInit()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | bounded_integers.cpp | 493 d_quantEngine->getSatContext(), in checkOwnership()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.cpp | 460 "sep_neg_guard", g, getSatContext(), getValuation())); in check()
846 HeapAssertInfo* ei = new HeapAssertInfo( getSatContext() ); in getOrMakeEqcInfo()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | conjecture_generator.cpp | 171 EqcInfo* ei = new EqcInfo( d_quantEngine->getSatContext() ); in getOrMakeEqcInfo()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sets/ |
| H A D | theory_sets_rels.cpp | 1654 ei = new EqcInfo(d_sets_theory.getSatContext()); in getOrMakeEqcInfo()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | theory_strings.cpp | 562 getSatContext(), getUserContext(), d_valuation)); in presolve()
1092 EqcInfo* ei = new EqcInfo( getSatContext() ); in getOrMakeEqcInfo()
|