Home
last modified time | relevance | path

Searched refs:TheorySep (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.cpp61 TheorySep::~TheorySep() { in ~TheorySep()
87 Node TheorySep::ppRewrite(TNode term) { in ppRewrite()
103 bool TheorySep::propagate(TNode literal) in propagate()
137 void TheorySep::propagate(Effort e){ in propagate()
142 Node TheorySep::explain(TNode literal) in explain()
176 void TheorySep::computeCareGraph() { in computeCareGraph()
294 void TheorySep::presolve() { in presolve()
305 void TheorySep::check(Effort e) { in check()
842 TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) { in getOrMakeEqcInfo()
1552 bool TheorySep::hasTerm( Node a ){ in hasTerm()
[all …]
H A Dtheory_sep.h37 class TheorySep : public Theory {
66TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, c…
67 ~TheorySep();
132 TheorySep& d_sep;
135 NotifyClass(TheorySep& sep) : d_sep(sep) {} in NotifyClass()
H A Dkinds7 theory THEORY_SEP ::CVC4::theory::sep::TheorySep "theory/sep/theory_sep.h"
/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dquantifiers_engine.cpp463 sep::TheorySep* theory_sep = in ppNotifyAssertions()
464 static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP)); in ppNotifyAssertions()