Searched refs:RemoveTermFormulas (Results 1 – 7 of 7) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/smt/ |
| H A D | term_formula_removal.cpp | 28 RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u) in RemoveTermFormulas() function in CVC4::RemoveTermFormulas
33 RemoveTermFormulas::~RemoveTermFormulas() {} in ~RemoveTermFormulas()
35 void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps) in run()
57 Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, in run()
240 Node RemoveTermFormulas::getSkolemForNode(Node node) const in getSkolemForNode()
251 Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { in replace()
298 bool RemoveTermFormulas::hasNestedTermChildren( TNode node ) { in hasNestedTermChildren()
|
| H A D | term_formula_removal.h | 35 class RemoveTermFormulas {
82 RemoveTermFormulas(context::UserContext* u);
83 ~RemoveTermFormulas();
|
| H A D | smt_engine.cpp | 510 RemoveTermFormulas d_iteRemover;
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/ |
| H A D | preprocessing_pass_context.h | 43 RemoveTermFormulas* iteRemover,
52 RemoveTermFormulas* getIteRemover() { return d_iteRemover; } in getIteRemover()
102 RemoveTermFormulas* d_iteRemover;
|
| H A D | preprocessing_pass_context.cpp | 27 RemoveTermFormulas* iteRemover, in PreprocessingPassContext()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_engine.h | 102 class RemoveTermFormulas; variable
455 RemoveTermFormulas& d_tform_remover;
477 RemoveTermFormulas& iteRemover, const LogicInfo& logic,
886 RemoveTermFormulas* getTermFormulaRemover() { return &d_tform_remover; } in getTermFormulaRemover()
|
| H A D | theory_engine.cpp | 283 RemoveTermFormulas& iteRemover, in TheoryEngine()
|