Home
last modified time | relevance | path

Searched refs:AXIOM (Results 1 – 25 of 133) sorted by relevance

123456

/dports/math/fricas/fricas-1.3.7/src/aldor/aldor/
H A Dlang.as20 +++ Author: AXIOM-XL library
30 +++ Author: AXIOM-XL library
41 +++ Author: AXIOM-XL library
58 +++ Author: AXIOM-XL library
75 +++ Author: AXIOM-XL library
86 +++ Author: AXIOM-XL library
97 +++ Author: AXIOM-XL library
108 +++ Author: AXIOM-XL library
118 +++ Author: AXIOM-XL library
193 +++ to an AXIOM-XL program.
[all …]
/dports/misc/usd/USD-21.11/pxr/base/tf/testenv/baseline/TfDiagnosticNotice4/non-specific/
H A DdiagnosticNotice4.out1 Fatal Coding Error: AXIOM [testTf], Class Type: AXIOM, in AXIOM, AXIOM:12
3 Fatal Coding Error: AXIOM [testTf], Class Type: AXIOM, in AXIOM, AXIOM:12
/dports/misc/usd/USD-21.11/pxr/base/arch/testenv/
H A DtestMath.cpp31 #define AXIOM(cond) \ macro
51 AXIOM(ArchSign(-123) == -1); in main()
52 AXIOM(ArchSign(123) == 1); in main()
53 AXIOM(ArchSign(0) == 0); in main()
/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_b_justification.h37 AXIOM, //!< no justification, it is only use if proof generation is disabled enumerator
42 m_data(reinterpret_cast<void*>(static_cast<size_t>(AXIOM))) {} in b_justification()
95 case b_justification::AXIOM: return out << "axiom";
H A Dsmt_eq_justification.h35 … AXIOM, //!< no justification, it is only used when proof generation is disabled enumerator
42 m_data(reinterpret_cast<void*>(static_cast<size_t>(AXIOM))) { in eq_justification()
H A Dsmt_conflict_resolution.cpp112 case eq_justification::AXIOM: tout << " axiom\n"; break; in eq_justification2literals()
122 case eq_justification::AXIOM: in eq_justification2literals()
304 case b_justification::AXIOM: in get_max_lvl()
554 case b_justification::AXIOM: in resolve()
716 case b_justification::AXIOM: in implied_by_marked()
849 case eq_justification::AXIOM: in get_proof()
974 SASSERT(js.get_kind() != b_justification::AXIOM); in get_proof()
1092 if (js.get_kind() == b_justification::AXIOM) in visit_b_justification()
1094 SASSERT(js.get_kind() != b_justification::AXIOM); in visit_b_justification()
1147 case eq_justification::AXIOM: in visit_trans_proof()
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dsmt_b_justification.h37 AXIOM, //!< no justification, it is only use if proof generation is disabled enumerator
42 m_data(reinterpret_cast<void*>(static_cast<size_t>(AXIOM))) {} in b_justification()
95 case b_justification::AXIOM: return out << "axiom";
H A Dsmt_eq_justification.h35 … AXIOM, //!< no justification, it is only used when proof generation is disabled enumerator
42 m_data(reinterpret_cast<void*>(static_cast<size_t>(AXIOM))) { in eq_justification()
H A Dsmt_conflict_resolution.cpp112 case eq_justification::AXIOM: tout << " axiom\n"; break; in eq_justification2literals()
122 case eq_justification::AXIOM: in eq_justification2literals()
304 case b_justification::AXIOM: in get_max_lvl()
552 case b_justification::AXIOM: in resolve()
714 case b_justification::AXIOM: in implied_by_marked()
846 case eq_justification::AXIOM: in get_proof()
971 SASSERT(js.get_kind() != b_justification::AXIOM); in get_proof()
1089 if (js.get_kind() == b_justification::AXIOM) in visit_b_justification()
1091 SASSERT(js.get_kind() != b_justification::AXIOM); in visit_b_justification()
1144 case eq_justification::AXIOM: in visit_trans_proof()
[all …]
/dports/math/fricas/fricas-1.3.7/pre-generated/target/share/hypertex/pages/
H A Drootpage.ht11 FriCAS is a fork of AXIOM system.
15 trademarks AXIOM and the AXIOM logo and of the registered
17 AXIOM was originally developed by the Research Division of the International
61 %\tab{16} The AXIOM/NAG Numerical Analyst Expert System
/dports/math/fricas/fricas-1.3.7/src/doc/ht/
H A Drootpage.ht11 FriCAS is a fork of AXIOM system.
15 trademarks AXIOM and the AXIOM logo and of the registered
17 AXIOM was originally developed by the Research Division of the International
61 %\tab{16} The AXIOM/NAG Numerical Analyst Expert System
/dports/math/vampire/vampire-4.5.1/Shell/
H A DGrounding.cpp143 …Clause* axR = new(1) Clause(1, NonspecificInference0(UnitInputType::AXIOM,InferenceRule::EQUALITY_… in getLocalEqualityAxioms()
151 …Clause* axT = new(3) Clause(3, NonspecificInference0(UnitInputType::AXIOM,InferenceRule::EQUALITY_… in getLocalEqualityAxioms()
194 …Clause* axCong = new(3) Clause(3, NonspecificInference0(UnitInputType::AXIOM,InferenceRule::EQUALI… in getEqualityAxioms()
H A DEqualityAxiomatizer.cpp169 Clause* axR = new(1) Clause(1, Clause::AXIOM, new Inference0(Inference::EQUALITY_PROXY_AXIOM2)); in addLocalAxioms()
175 Clause* axT = new(3) Clause(3, Clause::AXIOM, new Inference0(Inference::EQUALITY_PROXY_AXIOM2)); in addLocalAxioms()
300 return Clause::fromStack(lits, Unit::AXIOM, new Inference0(Inference::EQUALITY_PROXY_AXIOM2)); in getFnCongruenceAxiom()
325 return Clause::fromStack(lits, Unit::AXIOM, new Inference0(Inference::EQUALITY_PROXY_AXIOM2)); in getPredCongruenceAxiom()
/dports/math/fricas/fricas-1.3.7/src/algebra/
H A Dffp.spad13 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
14 ++ AXIOM Technical Report Series, ATR/5 NP2522.
243 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
244 ++ AXIOM Technical Report Series, ATR/5 NP2522.
274 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
275 ++ AXIOM Technical Report Series, ATR/5 NP2522.
294 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
295 ++ AXIOM Technical Report Series, ATR/5 NP2522.
H A Dffcat.spad10 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
11 ++ AXIOM Technical Report Series, ATR/5 NP2522.
43 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
44 ++ AXIOM Technical Report Series, ATR/5 NP2522.
103 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
104 ++ AXIOM Technical Report Series, ATR/5 NP2522.
355 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
356 ++ AXIOM Technical Report Series, ATR/5 NP2522.
436 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
437 ++ AXIOM Technical Report Series, ATR/5 NP2522.
/dports/math/vampire/vampire-4.5.1/UnitTests/
H A DtZ3test.cpp243 Clause * cl = new(1) Clause(1,Unit::AXIOM,new Inference0(Inference::INPUT)); in TEST_FUN()
247 cl = new(1) Clause(1,Unit::AXIOM,new Inference0(Inference::INPUT)); in TEST_FUN()
H A DtInterpretedNormalizer.cpp45 …mIterator(getSingletonIterator(lit), NonspecificInference0(UnitInputType::AXIOM, InferenceRule::IN… in TEST_FUN()
/dports/math/fricas/fricas-1.3.7/src/doc/
H A Dbook.tex13 ``\emph{AXIOM---The Scientific Computation System}'' by Jenks and
22 \href{https://github.com/fricas/fricas/blob/master/license/LICENSE.AXIOM}{license/LICENSE.AXIOM}
/dports/math/fricas/fricas-1.3.7/pre-generated/target/share/spadhelp/
H A DPlaneAlgebraicCurvePlot.help9 o $AXIOM/doc/src/algebra/acplot.spad.dvi
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/
H A Dbound_propagator.h70 enum bkind { AXIOM, // doesn't need justification enumerator
199 assert_lower_core(x, m_tmp, strict, a == null_assumption ? AXIOM : ASSUMPTION, 0, a);
203 assert_upper_core(x, m_tmp, strict, a == null_assumption ? AXIOM : ASSUMPTION, 0, a);
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/
H A Dbound_propagator.h70 enum bkind { AXIOM, // doesn't need justification enumerator
199 assert_lower_core(x, m_tmp, strict, a == null_assumption ? AXIOM : ASSUMPTION, 0, a);
203 assert_upper_core(x, m_tmp, strict, a == null_assumption ? AXIOM : ASSUMPTION, 0, a);
/dports/net-mgmt/librenms/librenms-21.5.1/tests/snmpsim/
H A Dvoss_8404c.snmprec6334 1.3.6.1.2.1.47.1.1.1.1.12.26301|4|AXIOM MEMORY
6335 1.3.6.1.2.1.47.1.1.1.1.12.26302|4|AXIOM MEMORY
6336 1.3.6.1.2.1.47.1.1.1.1.12.26303|4|AXIOM MEMORY
6337 1.3.6.1.2.1.47.1.1.1.1.12.26304|4|AXIOM MEMORY
6338 1.3.6.1.2.1.47.1.1.1.1.12.26305|4|AXIOM MEMORY
6364 1.3.6.1.2.1.47.1.1.1.1.12.27801|4|AXIOM MEMORY
6365 1.3.6.1.2.1.47.1.1.1.1.12.27802|4|AXIOM MEMORY
6366 1.3.6.1.2.1.47.1.1.1.1.12.27803|4|AXIOM MEMORY
6367 1.3.6.1.2.1.47.1.1.1.1.12.27804|4|AXIOM MEMORY
6368 1.3.6.1.2.1.47.1.1.1.1.12.27805|4|AXIOM MEMORY
/dports/math/fricas/fricas-1.3.7/src/doc/sphinx/source/
H A Dindex.rst8 <https://github.com/fricas/fricas/blob/master/license/LICENSE.AXIOM>`_.
/dports/math/fricas/fricas-1.3.7/src/input/
H A Daxiom.input3 -- This file is read on start-up by the AXIOM system. It is
/dports/math/vampire/vampire-4.5.1/SAT/
H A DSAT2FO.cpp136 Clause* foConfl = Clause::fromStack(negStack,NonspecificInference0(UnitInputType::AXIOM,rule)); in createConflictClause()

123456