/dports/math/cvc3/cvc3-2.4.1/src/sat/ |
H A D | cnf_manager.cpp | 101 vector<Theorem> thms; in replaceITErec() local 189 vector<Theorem> thms; in translateExprRec() local 227 vector<Theorem> thms; in translateExprRec() local 268 vector<Theorem> thms; in translateExprRec() local 316 vector<Theorem> thms; in translateExprRec() local 384 vector<Theorem> thms ; in translateExprRec() local
|
H A D | cnf_theorem_producer.cpp | 250 const vector<Theorem>& thms) { in CNFtranslate() 273 const vector<Theorem>& thms, in CNFITEtranslate()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_core/ |
H A D | expr_transform.cpp | 166 vector<Theorem> thms; in pushNegationRec() local 186 vector<Theorem> thms; in pushNegationRec() local 203 vector<Theorem> thms; in pushNegationRec() local 256 vector<Theorem> thms; in pushNegation1() local 268 vector<Theorem> thms; in pushNegation1() local
|
H A D | theory_core.cpp | 1008 vector<Theorem> thms; in rewrite() local
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_records/ |
H A D | theory_records.cpp | 53 vector<Theorem> thms; in rewriteAux() local 71 vector<Theorem> thms; in rewriteAux() local 284 vector<Theorem> thms; in computeModel() local 530 vector<Theorem> thms; in setup() local
|
/dports/math/cvc3/cvc3-2.4.1/src/include/ |
H A D | theory.h | 687 const std::vector<Theorem>& thms) in substitutivityRule() 704 const std::vector<Theorem>& thms) in substitutivityRule()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
H A D | theory_arith3.cpp | 244 vector<Theorem> thms; in canon() local 391 vector<Theorem> thms; in canonPred() local 405 vector<Theorem> thms; in canonPredEquiv() local 420 vector<Theorem> thms; in canonConjunctionEquiv() local 438 vector<Theorem> thms; in doSolve() local 969 vector<Theorem> thms; in solvedForm() local 1009 vector<Theorem> thms; in substAndCanonize() local 1051 vector<Theorem> thms; in substAndCanonize() local 1961 vector<Theorem> thms; in processFiniteInterval() local
|
H A D | theory_arith_new.cpp | 280 vector<Theorem> thms; in canonPred() local 297 vector<Theorem> thms; // Vector to hold the simplified versions of e[0] and e[1] in canonPredEquiv() local 319 vector<Theorem> thms; in canonConjunctionEquiv() local 337 vector<Theorem> thms; in doSolve() local 718 vector<Theorem> thms; in solvedForm() local 758 vector<Theorem> thms; in substAndCanonize() local 800 vector<Theorem> thms; in substAndCanonize() local 1212 vector<Theorem> thms; in processFiniteInterval() local 3474 vector<Theorem> thms; // The theorems of the changed terms for the substitution in substAndCanonizeModTableaux() local
|
H A D | arith_theorem_producer.cpp | 1651 vector<Theorem> thms; in finiteInterval() local 1733 vector<Theorem> thms; in darkGrayShadow2ab() local 1824 vector<Theorem> thms; in darkGrayShadow2ba() local 2106 vector<Theorem> thms; in lessThanToLE() local 2601 vector<Theorem> thms(isIntVars); in eqElimIntRule() local 3173 vector<Theorem> thms; in lessThanToLERewrite() local 3227 Theorem ArithTheoremProducer::addInequalities(const vector<Theorem>& thms) { in addInequalities()
|
H A D | arith_theorem_producer3.cpp | 1608 vector<Theorem> thms; in finiteInterval() local 1690 vector<Theorem> thms; in darkGrayShadow2ab() local 1781 vector<Theorem> thms; in darkGrayShadow2ba() local 2064 vector<Theorem> thms; in lessThanToLE() local 2576 vector<Theorem> thms(isIntVars); in eqElimIntRule() local 3061 Theorem ArithTheoremProducer3::addInequalities(const vector<Theorem>& thms) { in addInequalities() 3124 vector<Theorem> thms; in lessThanToLERewrite() local
|
H A D | theory_arith_old.cpp | 250 vector<Theorem> thms; in canon() local 402 vector<Theorem> thms; in canonPred() local 418 vector<Theorem> thms; in canonPredEquiv() local 435 vector<Theorem> thms; in canonConjunctionEquiv() local 454 vector<Theorem> thms; in doSolve() local 949 vector<Theorem> thms; in solvedForm() local 988 vector<Theorem> thms; in substAndCanonize() local 1030 vector<Theorem> thms; in substAndCanonize() local 2417 vector<Theorem> thms; in processFiniteInterval() local
|
H A D | arith_theorem_producer_old.cpp | 1806 vector<Theorem> thms; in finiteInterval() local 1890 vector<Theorem> thms; in darkGrayShadow2ab() local 1984 vector<Theorem> thms; in darkGrayShadow2ba() local 2266 vector<Theorem> thms; in lessThanToLE() local 2778 vector<Theorem> thms(isIntVars); in eqElimIntRule() local 3437 vector<Theorem> thms; in lessThanToLERewrite() local 3775 Theorem ArithTheoremProducerOld::addInequalities(const vector<Theorem>& thms) { in addInequalities()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/ |
H A D | theory_bitvector.cpp | 283 vector<Theorem> thms; in bitBlastIneqn() local 422 vector<Theorem> thms, thms0; in bitBlastTerm() local 447 vector<Theorem> thms, thms0; in bitBlastTerm() local 472 vector<Theorem> thms, thms0; in bitBlastTerm() local 727 vector<Theorem> thms; in pushNegationRec() local 743 vector<Theorem> thms; in pushNegationRec() local 775 vector<Theorem> thms; in pushNegationRec() local 898 vector<Theorem> thms; in rewriteBV() local 987 vector<Theorem> thms; // Rewrites of constant concatenations in rewriteBV() local 1249 vector<Theorem> thms; in rewriteBV() local [all …]
|
H A D | bitvector_theorem_producer.cpp | 895 Theorem BitvectorTheoremProducer::bitExtractAllToConstEq(vector<Theorem>& thms) in bitExtractAllToConstEq()
|
/dports/math/cvc3/cvc3-2.4.1/src/search/ |
H A D | search_impl_base.cpp | 431 vector<Theorem> thms; in enqueueCNFrec() local 474 vector<Theorem> thms; in enqueueCNFrec() local
|
H A D | search_fast.cpp | 848 vector<Theorem> thms; in propagate() local 917 vector<Theorem> thms; in unitPropagation() local 1482 vector<Theorem> thms; // collect proofs of !l_i for unit prop. in addNonLiteralFact() local
|
H A D | variable.cpp | 173 vector<Theorem> thms; in deriveThmRec() local
|
H A D | search_theorem_producer.cpp | 511 SearchEngineTheoremProducer::unitProp(const std::vector<Theorem>& thms, in unitProp() 1109 SearchEngineTheoremProducer::conflictRule(const std::vector<Theorem>& thms, in conflictRule()
|
/dports/math/cvc3/cvc3-2.4.1/src/theorem/ |
H A D | assumptions.cpp | 200 void Assumptions::add(const std::vector<Theorem>& thms) in add()
|
H A D | common_theorem_producer.cpp | 374 const vector<Theorem>& thms) { in substitutivityRule() 426 const vector<Theorem>& thms) { in substitutivityRule() 734 vector<Theorem> thms; in andIntro() local
|
/dports/databases/kyotocabinet/kyotocabinet-1.2.79/ |
H A D | kclangc.cc | 1378 TinyHashMap::Sorter* thms = (TinyHashMap::Sorter*)sort; in kcmapsortdel() local 1388 TinyHashMap::Sorter* thms = (TinyHashMap::Sorter*)sort; in kcmapsortgetkey() local 1398 TinyHashMap::Sorter* thms = (TinyHashMap::Sorter*)sort; in kcmapsortgetvalue() local 1408 TinyHashMap::Sorter* thms = (TinyHashMap::Sorter*)sort; in kcmapsortget() local 1418 TinyHashMap::Sorter* thms = (TinyHashMap::Sorter*)sort; in kcmapsortstep() local
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_array/ |
H A D | theory_array.cpp | 986 vector<Theorem> thms; in computeModel() local
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_uf/ |
H A D | theory_uf.cpp | 523 vector<Theorem> thms; in computeModel() local
|
/dports/astro/py-astlib/astLib-0.11.7/PyWCSTools/wcssubs-3.9.5/ |
H A D | dateutil.c | 2741 char *thms, *fdate; local
|