Searched refs:getFreeVarInc (Results 1 – 5 of 5) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | sygus_explain.cpp | 205 Node x = d_tdb->getFreeVarInc(xtn, var_count); in getExplanationFor()
338 Node x = d_tdb->getFreeVarInc(vtn, var_count); in getExplanationFor()
|
| H A D | sygus_repair_const.cpp | 389 Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count); in getSkeleton()
434 child = d_tds->getFreeVarInc(cn.getType(), free_var_count); in getSkeleton()
|
| H A D | term_database_sygus.h | 213 TNode getFreeVarInc(TypeNode tn,
|
| H A D | term_database_sygus.cpp | 118 TNode TermDbSygus::getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_count, bool useSygusT… in getFreeVarInc() function in CVC4::theory::quantifiers::TermDbSygus
206 a = getFreeVarInc( tna, var_count, true ); in mkGeneric()
254 ret = getFreeVarInc(n[0].getType(), var_count, true); in canonizeBuiltin()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | datatypes_sygus.cpp | 1730 return d_tds->getFreeVarInc( n.getType(), var_count ); in getCurrentTemplate()
|