Home
last modified time | relevance | path

Searched defs:registerTerm (Results 1 – 15 of 15) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/example/
H A Dtheory_uf_tim.cpp50 void TheoryUFTim::registerTerm(TNode n) { in registerTerm() function in TheoryUFTim
/dports/math/cvc4/CVC4-1.7/test/unit/theory/
H A Dtheory_white.h103 void registerTerm(TNode n) { in registerTerm() function
H A Dtheory_engine_white.h215 void registerTerm(TNode) { Unimplemented(); } in registerTerm() function
/dports/math/cvc4/CVC4-1.7/src/proof/
H A Duf_proof.cpp581 void UFProof::registerTerm(Expr term) { in registerTerm() function in CVC4::UFProof
H A Dbitvector_proof.cpp83 void BitVectorProof::registerTerm(Expr term) { in registerTerm() function in CVC4::proof::BitVectorProof
H A Darith_proof.cpp653 void ArithProof::registerTerm(Expr term) { in registerTerm() function in CVC4::ArithProof
H A Darray_proof.cpp1075 void ArrayProof::registerTerm(Expr term) { in registerTerm() function in CVC4::ArrayProof
H A Dtheory_proof.cpp177 void TheoryProofEngine::registerTerm(Expr term) { in registerTerm() function in CVC4::TheoryProofEngine
1124 void BooleanProof::registerTerm(Expr term) { in registerTerm() function in CVC4::BooleanProof
/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dext_theory.cpp400 void ExtTheory::registerTerm(Node n) in registerTerm() function in CVC4::theory::ExtTheory
/dports/math/cvc4/CVC4-1.7/src/theory/bv/
H A Dbv_inequality_graph.cpp228 TermId InequalityGraph::registerTerm(TNode term) { in registerTerm() function in InequalityGraph
H A Dslicer.cpp462 ExtractTerm Slicer::registerTerm(TNode node) { in registerTerm() function in CVC4::theory::bv::Slicer
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dsygus_sampler.cpp263 Node SygusSampler::registerTerm(Node n, bool forceKeep) in registerTerm() function in CVC4::theory::quantifiers::SygusSampler
/dports/math/cvc4/CVC4-1.7/src/theory/fp/
H A Dtheory_fp.cpp812 void TheoryFp::registerTerm(TNode node) { in registerTerm() function in CVC4::theory::fp::TheoryFp
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Ddatatypes_sygus.cpp165 void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) { in registerTerm() function in SygusSymBreakNew
/dports/math/cvc4/CVC4-1.7/src/theory/strings/
H A Dtheory_strings.cpp3887 void TheoryStrings::registerTerm( Node n, int effort ) { in registerTerm() function in CVC4::theory::strings::TheoryStrings