Home
last modified time | relevance | path

Searched refs:newVarCnt (Results 1 – 18 of 18) sorted by relevance

/dports/math/vampire/vampire-4.5.1/SAT/
H A DMinimizingSolver.cpp37 void MinimizingSolver::ensureVarCount(unsigned newVarCnt) in ensureVarCount() argument
41 if (newVarCnt<= _varCnt) { in ensureVarCount()
44 _varCnt = newVarCnt; in ensureVarCount()
45 _inner->ensureVarCount(newVarCnt); in ensureVarCount()
46 _asgn.expand(newVarCnt+1); in ensureVarCount()
47 _watcher.expand(newVarCnt+1); in ensureVarCount()
48 _unsClCnt.expand(newVarCnt+1, 0); in ensureVarCount()
49 _heap.elMap().expand(newVarCnt+1); in ensureVarCount()
50 _clIdx.expand(newVarCnt+1); in ensureVarCount()
H A DFallbackSolverWrapper.hpp101 virtual void ensureVarCount(unsigned newVarCnt) override { in ensureVarCount() argument
102 _inner->ensureVarCount(newVarCnt); in ensureVarCount()
103 _fallback->ensureVarCount(newVarCnt); in ensureVarCount()
104 _varCnt=max(_varCnt,newVarCnt); in ensureVarCount()
H A DBufferedSolver.hpp78 …ual void ensureVarCount(unsigned newVarCnt) override { _inner->ensureVarCount(newVarCnt); _varCnt=… in ensureVarCount() argument
H A DTWLSolver.cpp127 void TWLSolver::ensureVarCount(unsigned newVarCnt) in ensureVarCount() argument
131 if(newVarCnt<=_varCnt) { in ensureVarCount()
135 _assignment.expand(newVarCnt+1, AS_UNDEFINED); in ensureVarCount()
136 _assignmentLevels.expand(newVarCnt+1); in ensureVarCount()
137 _assignmentPremises.expand(newVarCnt+1, 0); in ensureVarCount()
138 _lastAssignments.expand(newVarCnt+1, AS_UNDEFINED); in ensureVarCount()
139 _propagationScheduled.expand(newVarCnt+1); in ensureVarCount()
141 _windex.expand((newVarCnt+1)*2); in ensureVarCount()
143 _varCnt=newVarCnt; in ensureVarCount()
145 _variableSelector->ensureVarCount(newVarCnt); in ensureVarCount()
H A DTransparentSolver.cpp38 void TransparentSolver::ensureVarCnt(unsigned newVarCnt) in ensureVarCnt() argument
42 _inner->ensureVarCnt(newVarCnt); in ensureVarCnt()
43 _vars.expand(newVarCnt); in ensureVarCnt()
H A DMinisatInterfacingNewSimp.cpp76 void MinisatInterfacingNewSimp::ensureVarCount(unsigned newVarCnt) in ensureVarCount() argument
81 while(_solver.nVars() < (int)newVarCnt) { in ensureVarCount()
H A DZ3Interfacing.hpp95 void ensureVarCount(unsigned newVarCnt) override { in ensureVarCount() argument
98 while (_varCnt < newVarCnt) { in ensureVarCount()
H A DTransparentSolver.hpp50 virtual void ensureVarCnt(unsigned newVarCnt);
H A DMinisatInterfacing.hpp88 virtual void ensureVarCount(unsigned newVarCnt) override;
H A DMinimizingSolver.hpp70 virtual void ensureVarCount(unsigned newVarCnt) override;
H A DMinisatInterfacingNewSimp.hpp95 virtual void ensureVarCount(unsigned newVarCnt) override;
H A DMinisatInterfacing.cpp51 void MinisatInterfacing::ensureVarCount(unsigned newVarCnt) in ensureVarCount() argument
55 while(_solver.nVars() < (int)newVarCnt) { in ensureVarCount()
H A DSATSolver.hpp132 virtual void ensureVarCount(unsigned newVarCnt) {} in ensureVarCount() argument
H A DTWLSolver.hpp84 virtual void ensureVarCount(unsigned newVarCnt) override;
/dports/math/vampire/vampire-4.5.1/Test/
H A DCheckedSatSolver.cpp39 void CheckedSatSolver::ensureVarCount(unsigned newVarCnt) in ensureVarCount() argument
43 _varCnt = std::max(_varCnt, newVarCnt); in ensureVarCount()
44 _inner->ensureVarCount(newVarCnt); in ensureVarCount()
H A DRecordingSatSolver.cpp87 void RecordingSatSolver::ensureVarCnt(unsigned newVarCnt) in ensureVarCnt() argument
91 REC("act=evc:nwc="<<newVarCnt); in ensureVarCnt()
93 _inner->ensureVarCnt(newVarCnt); in ensureVarCnt()
H A DCheckedSatSolver.hpp66 virtual void ensureVarCount(unsigned newVarCnt) override;
H A DRecordingSatSolver.hpp46 virtual void ensureVarCnt(unsigned newVarCnt);