Home
last modified time | relevance | path

Searched refs:FLOATINGPOINT_REM (Results 1 – 8 of 8) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/fp/
H A Dtheory_fp_rewriter.cpp263 Assert(node.getKind() == kind::FLOATINGPOINT_REM); in compactRemainder()
269 if (working[0].getKind() == kind::FLOATINGPOINT_REM && // short-cut matters! in compactRemainder()
285 nm->mkNode(kind::FLOATINGPOINT_REM, working[0][0], working[1])); in compactRemainder()
433 Assert(node.getKind() == kind::FLOATINGPOINT_REM); in rem()
1013 preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity; in init()
1098 postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::compactRemainder; in init()
1183 constantFoldTable[kind::FLOATINGPOINT_REM] = constantFold::rem; in init()
H A Dkinds101 operator FLOATINGPOINT_REM 2 "floating-point remainder"
102 typerule FLOATINGPOINT_REM ::CVC4::theory::fp::FloatingPointOperationTypeRule
H A Dfp_converter.cpp1011 case kind::FLOATINGPOINT_REM: in convert()
1147 case kind::FLOATINGPOINT_REM: in convert()
H A Dtheory_fp.cpp134 d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_REM); in TheoryFp()
/dports/math/cvc4/CVC4-1.7/src/api/
H A Dcvc4cppkind.h1269 FLOATINGPOINT_REM, enumerator
H A Dcvc4cpp.cpp181 {FLOATINGPOINT_REM, CVC4::Kind::FLOATINGPOINT_REM},
429 {CVC4::Kind::FLOATINGPOINT_REM, FLOATINGPOINT_REM},
/dports/math/cvc4/CVC4-1.7/src/printer/smt2/
H A Dsmt2_printer.cpp713 case kind::FLOATINGPOINT_REM: in toStream()
1101 case kind::FLOATINGPOINT_REM: return "fp.rem"; in smtKindString()
/dports/math/cvc4/CVC4-1.7/src/parser/smt2/
H A Dsmt2.cpp175 addOperator(kind::FLOATINGPOINT_REM, "fp.rem"); in addFloatingPointOperators()