Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/fp/
H A Dtheory_fp_rewriter.cpp105 k == kind::FLOATINGPOINT_LT); in breakChain()
153 …return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LT,node[1… in gtTolt()
310 Assert(node.getKind() == kind::FLOATINGPOINT_LT); in ltId()
584 Assert(node.getKind() == kind::FLOATINGPOINT_LT); in lt()
1024 preRewriteTable[kind::FLOATINGPOINT_LT] = in init()
1108 postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::ltId; in init()
1193 constantFoldTable[kind::FLOATINGPOINT_LT] = constantFold::lt; in init()
H A Dkinds123 operator FLOATINGPOINT_LT 2: "floating-point less than"
124 typerule FLOATINGPOINT_LT ::CVC4::theory::fp::FloatingPointTestTypeRule
H A Dfp_converter.cpp1380 case kind::FLOATINGPOINT_LT: in convert()
1410 case kind::FLOATINGPOINT_LT: in convert()
H A Dtheory_fp.cpp143 d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_LT); in TheoryFp()
/dports/math/cvc4/CVC4-1.7/src/api/
H A Dcvc4cppkind.h1320 FLOATINGPOINT_LT, enumerator
H A Dcvc4cpp.cpp186 {FLOATINGPOINT_LT, CVC4::Kind::FLOATINGPOINT_LT},
434 {CVC4::Kind::FLOATINGPOINT_LT, FLOATINGPOINT_LT},
/dports/math/cvc4/CVC4-1.7/src/printer/smt2/
H A Dsmt2_printer.cpp718 case kind::FLOATINGPOINT_LT: in toStream()
1109 case kind::FLOATINGPOINT_LT: return "fp.lt"; in smtKindString()
/dports/math/cvc4/CVC4-1.7/src/parser/smt2/
H A Dsmt2.cpp180 addOperator(kind::FLOATINGPOINT_LT, "fp.lt"); in addFloatingPointOperators()