Home
last modified time | relevance | path

Searched defs:thms (Results 1 – 24 of 24) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dcnf_manager.cpp101 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 Dcnf_theorem_producer.cpp250 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 Dexpr_transform.cpp166 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 Dtheory_core.cpp1008 vector<Theorem> thms; in rewrite() local
/dports/math/cvc3/cvc3-2.4.1/src/theory_records/
H A Dtheory_records.cpp53 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 Dtheory.h687 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 Dtheory_arith3.cpp244 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 Dtheory_arith_new.cpp280 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 Darith_theorem_producer.cpp1651 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 Darith_theorem_producer3.cpp1608 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 Dtheory_arith_old.cpp250 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 Darith_theorem_producer_old.cpp1806 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 Dtheory_bitvector.cpp283 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 Dbitvector_theorem_producer.cpp895 Theorem BitvectorTheoremProducer::bitExtractAllToConstEq(vector<Theorem>& thms) in bitExtractAllToConstEq()
/dports/math/cvc3/cvc3-2.4.1/src/search/
H A Dsearch_impl_base.cpp431 vector<Theorem> thms; in enqueueCNFrec() local
474 vector<Theorem> thms; in enqueueCNFrec() local
H A Dsearch_fast.cpp848 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 Dvariable.cpp173 vector<Theorem> thms; in deriveThmRec() local
H A Dsearch_theorem_producer.cpp511 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 Dassumptions.cpp200 void Assumptions::add(const std::vector<Theorem>& thms) in add()
H A Dcommon_theorem_producer.cpp374 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 Dkclangc.cc1378 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 Dtheory_array.cpp986 vector<Theorem> thms; in computeModel() local
/dports/math/cvc3/cvc3-2.4.1/src/theory_uf/
H A Dtheory_uf.cpp523 vector<Theorem> thms; in computeModel() local
/dports/astro/py-astlib/astLib-0.11.7/PyWCSTools/wcssubs-3.9.5/
H A Ddateutil.c2741 char *thms, *fdate; local