Home
last modified time | relevance | path

Searched refs:isTester (Results 1 – 16 of 16) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Ddatatypes_rewriter.h84 static int isTester(Node n, Node& a);
86 static int isTester(Node n);
H A Ddatatypes_rewriter.cpp207 else if (tn.isTester()) in getOperatorKindForSygusBuiltin()
573 int DatatypesRewriter::isTester(Node n, Node& a) in isTester() function in CVC4::theory::datatypes::DatatypesRewriter
583 int DatatypesRewriter::isTester(Node n) in isTester() function in CVC4::theory::datatypes::DatatypesRewriter
601 Assert(n.getType().isConstructor() || n.getType().isTester() in indexOf()
H A Dtheory_datatypes.cpp489 int tindex = DatatypesRewriter::isTester( atom, t_arg ); in assertFact()
974 int tindex = DatatypesRewriter::isTester( lbl ); in getLabelIndex()
/dports/math/cvc4/CVC4-1.7/src/expr/
H A Dtype_node.h629 bool isTester() const;
934 if(isTester()) { in getRangeType()
986 inline bool TypeNode::isTester() const { in isTester() function
H A Dtype.cpp282 bool Type::isTester() const { in isTester() function in CVC4::Type
284 return d_typeNode->isTester(); in isTester()
472 PrettyCheckArgument(isNull() || isTester(), this); in TesterType()
H A Dtype.h371 bool isTester() const;
H A Dtype_node.cpp292 if(isTester()) { in getArgTypes()
H A Dsymbol_table.cpp264 } else if (t.isTester()) { in markOverloaded()
H A Ddatatype.cpp76 item.getType().isTester() || in indexOf()
H A Dexpr_manager_template.cpp801 testerType.isTester() && in checkResolvedDatatype()
/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dtheory_datatype.h143 inline bool isTester(const Expr& e) in isTester() function
/dports/math/cvc3/cvc3-2.4.1/src/theory_datatype/
H A Ddatatype_theorem_producer.cpp101 CHECK_SOUND(isTester(e), "Tester expected"); in rewriteTestCons()
H A Dtheory_datatype_lazy.cpp296 else if (isTester(sigNew) && isConstructor(sigNew[0])) { in update()
H A Dtheory_datatype.cpp330 else if (isTester(e)) { in rewrite()
398 else if (isTester(sigNew) && isConstructor(sigNew[0])) { in update()
/dports/math/cvc4/CVC4-1.7/src/parser/
H A Dparser.cpp154 } else if(t.isTester()) { in getKindForFunction()
195 return type.isFunction() || type.isConstructor() || type.isTester() || in isFunctionLike()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Dsygus_enumerator.cpp84 int tst = datatypes::DatatypesRewriter::isTester(sbl[0], a); in initialize()