| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf.cpp | 42 TheoryUF::TheoryUF(context::Context* c, in TheoryUF() function in CVC4::theory::uf::TheoryUF
69 TheoryUF::~TheoryUF() { in ~TheoryUF()
77 void TheoryUF::finishInit() { in finishInit()
114 void TheoryUF::check(Effort level) { in check()
327 bool TheoryUF::propagate(TNode literal) { in propagate()
342 void TheoryUF::propagate(Effort effort) { in propagate()
369 Node TheoryUF::explain(TNode literal) { in explain()
428 void TheoryUF::presolve() { in presolve()
586 void TheoryUF::addSharedTerm(TNode t) { in addSharedTerm()
682 void TheoryUF::computeCareGraph() { in computeCareGraph()
[all …]
|
| H A D | theory_uf.h | 38 class TheoryUF : public Theory {
46 TheoryUF& d_uf;
48 NotifyClass(TheoryUF& uf): d_uf(uf) {} in NotifyClass()
273 TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out,
277 ~TheoryUF();
|
| H A D | theory_uf_strong_solver.h | 32 class TheoryUF; variable
364 OutputChannel& out, TheoryUF* th);
367 TheoryUF* getTheory() { return d_th; } in getTheory()
434 TheoryUF* d_th;
|
| H A D | kinds | 7 theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
|
| H A D | theory_uf_strong_solver.cpp | 1322 TheoryUF* th) in StrongSolverTheoryUF()
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_uf/ |
| H A D | uf_theorem_producer.h | 31 class TheoryUF; variable
34 TheoryUF* d_theoryUF;
38 UFTheoremProducer(TheoremManager* tm, TheoryUF* theoryUF) : in UFTheoremProducer()
|
| H A D | theory_uf.cpp | 42 TheoryUF::TheoryUF(TheoryCore* core)//, bool useAckermann) in TheoryUF() function in TheoryUF
71 TheoryUF::~TheoryUF() { in ~TheoryUF()
79 void TheoryUF::assertFact(const Theorem& e) in assertFact()
156 void TheoryUF::checkSat(bool fullEffort) in checkSat()
211 Theorem TheoryUF::rewrite(const Expr& e) in rewrite()
236 void TheoryUF::setup(const Expr& e) in setup()
337 void TheoryUF::checkType(const Expr& e) in checkType()
417 void TheoryUF::computeType(const Expr& e) in computeType()
471 Type TheoryUF::computeBaseType(const Type& t) { in computeBaseType()
591 Expr TheoryUF::computeTCC(const Expr& e) in computeTCC()
[all …]
|
| H A D | uf_theorem_producer.cpp | 41 UFProofRules* TheoryUF::createProofRules() { in createProofRules()
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | theory_uf.h | 48 class TheoryUF :public Theory {
73 TheoryUF(TheoryCore* core);
74 ~TheoryUF();
|
| H A D | translator.h | 40 class TheoryUF; variable
100 TheoryUF* d_theoryUF;
167 void setTheoryUF(TheoryUF* theoryUF) { d_theoryUF = theoryUF; } in setTheoryUF()
|
| H A D | vcl.h | 38 class TheoryUF; variable
58 TheoryUF* d_theoryUF;
|
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | uf_proof.h | 54 class TheoryUF; variable
68 UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine);
75 LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine) in LFSCUFProof()
|
| H A D | theory_proof.cpp | 79 d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this); in registerTheory()
1023 th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v, in printTheoryLemmaProof()
|
| H A D | uf_proof.cpp | 576 UFProof::UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* pe) in UFProof()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | model_engine.cpp | 93 …uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEO… in check()
|
| /dports/math/cvc3/cvc3-2.4.1/src/vcl/ |
| H A D | vcl.cpp | 491 d_theories.push_back(d_theoryUF = new TheoryUF(d_theoryCore)); in init()
|