Searched refs:TheoryArrays (Results 1 – 6 of 6) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | theory_arrays.cpp | 59 TheoryArrays::TheoryArrays(context::Context* c, in TheoryArrays() function in CVC4::theory::arrays::TheoryArrays
157 TheoryArrays::~TheoryArrays() { in ~TheoryArrays()
316 Node TheoryArrays::ppRewrite(TNode term) { in ppRewrite()
841 void TheoryArrays::propagate(Effort e) in propagate()
965 void TheoryArrays::computeCareGraph() in computeCareGraph()
1252 void TheoryArrays::presolve() in presolve()
1302 void TheoryArrays::check(Effort e) { in check()
1596 void TheoryArrays::setNonLinear(TNode a) in setNonLinear()
1835 void TheoryArrays::checkStore(TNode a) { in checkStore()
2159 bool TheoryArrays::dischargeLemmas() in dischargeLemmas()
[all …]
|
| H A D | theory_arrays.h | 94 class TheoryArrays : public Theory {
142 TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
145 ~TheoryArrays();
275 TheoryArrays& d_arrays;
277 NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {} in NotifyClass()
463 TheoryArraysDecisionStrategy(TheoryArrays* ta);
473 TheoryArrays* d_ta;
|
| H A D | kinds | 7 theory THEORY_ARRAYS ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
|
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | array_proof.h | 69 class TheoryArrays; variable
85 ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine);
94 LFSCArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine) in LFSCArrayProof()
|
| H A D | theory_proof.cpp | 121 d_theoryProofTable[id] = new LFSCArrayProof((theory::arrays::TheoryArrays*)th, this); in registerTheory()
1027 th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, in printTheoryLemmaProof()
|
| H A D | array_proof.cpp | 1070 ArrayProof::ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* pe) in ArrayProof()
|