Home
last modified time | relevance | path

Searched refs:iteTerm (Results 1 – 6 of 6) sorted by relevance

/dports/math/cvc4/CVC4-1.7/test/unit/api/
H A Dterm_black.h505 TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b)); in testIteTerm()
507 TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x)); in testIteTerm()
508 TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b)); in testIteTerm()
509 TS_ASSERT_THROWS(b.iteTerm(x, b), CVC4ApiException&); in testIteTerm()
510 TS_ASSERT_THROWS(x.iteTerm(x, x), CVC4ApiException&); in testIteTerm()
511 TS_ASSERT_THROWS(x.iteTerm(x, b), CVC4ApiException&); in testIteTerm()
513 TS_ASSERT_THROWS(f.iteTerm(b, b), CVC4ApiException&); in testIteTerm()
528 TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(b, b)); in testIteTerm()
529 TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(x, x)); in testIteTerm()
532 TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(b, b)); in testIteTerm()
[all …]
/dports/math/vampire/vampire-4.5.1/Kernel/
H A DFormula.cpp801 TermList iteTerm(Term::createITE(condition, thenTerm, elseTerm, Sorts::SRT_BOOL)); in createITE() local
802 return new BoolTermFormula(iteTerm); in createITE()
/dports/math/cvc4/CVC4-1.7/src/api/
H A Dcvc4cpp.h640 Term iteTerm(const Term& then_t, const Term& else_t) const;
H A Dcvc4cpp.cpp1119 Term Term::iteTerm(const Term& then_t, const Term& else_t) const in iteTerm() function in CVC4::api::Term
/dports/math/cvc4/CVC4-1.7/src/parser/cvc/
H A DCvc.g2087 : iteTerm[f]
2241 iteTerm[CVC4::Expr& f]
/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/
H A Dbitvector_theorem_producer.cpp1177 Expr iteTerm = cond.iteExpr(leftshiftTerm, zeroString); in bitExtractBVMult() local
1178 k.push_back(iteTerm); in bitExtractBVMult()