com.cyc.cycjava.cycl.inference.harness
Class inference_tactician_strategic_uninterestingness
java.lang.Object
com.cyc.tool.subl.util.SubLTrampolineFile
com.cyc.tool.subl.util.SubLTranslatedFile
com.cyc.cycjava.cycl.inference.harness.inference_tactician_strategic_uninterestingness
- All Implemented Interfaces:
- CommonSymbols, SubLFile
public final class inference_tactician_strategic_uninterestingness
- extends SubLTranslatedFile
| Fields inherited from interface com.cyc.tool.subl.jrtl.nativeCode.subLisp.CommonSymbols |
ANSWER_TAG, APPEND_KEYWORD, APPEND_STACK_TRACES_TO_ERROR_MESSAGES, AREF, ASSEMBLE_FIXNUMS_TO_INTEGER, ATOM, BIGNUMP, BINARY_KEYWORD, BINDING_TYPE, BOOLEANP, CAAR, CADR, CAND, CAR, CCATCH, CDEC, CDESTRUCTURING_BIND, CDO, CDO_ALL_SYMBOLS, CDO_EXTERNAL_SYMBOLS, CDO_SYMBOLS, CDOHASH, CDOLIST, CDOTIMES, CDR, CHAR, CHAR_E_SYMBOL, CHAR_EQUAL_SYMBOL, CHAR_GREATER_THAN_OR_EQUAL_SYMBOL, CHAR_GREATER_THAN_SYMBOL, CHAR_GT_SYMBOL, CHAR_GTE_SYMBOL, CHAR_LESS_THAN_OR_EQUAL_SYMBOL, CHAR_LESS_THAN_SYMBOL, CHAR_LT_SYMBOL, CHAR_LTE_SYMBOL, CHAR_NE_SYMBOL, CHAR_NOT_EQUAL_SYMBOL, CHARACTERP, CHECK_TYPE, CINC, CLET, CMULTIPLE_VALUE_BIND, CNOT, CONS, CONSP, CONSTANT, COR, CPOP, CPROGV, CPUSH, CPUSHNEW, CREATE_KEYWORD, CSETF, CSETQ, CSOME, CTIME, CUNWIND_PROTECT, CVS_ID, DEBUG_IO, DECLAIM, DECLARE, DEFCONSTANT, DEFINE, DEFLEXICAL, DEFMACRO, DEFPARAMETER, DEFVAR, DIRECTION_KEYWORD, DYNAMIC, EIGHT_INTEGER, EIGHTEEN_INTEGER, ELEMENT_TYPE_KEYWORD, ELEVEN_INTEGER, END_KEYWORD, ENFORCE_MUST, ENFORCE_TYPE, EQ, EQL, EQUAL, EQUALP, ERROR, ERROR_KEYWORD, ERROR_OUTPUT, EVAL, EXTERNAL_FORMAT_KEYWORD, EXTERNAL_KEYWORD, FIF, FIFTEEN_INTEGER, FIRST, FIVE_INTEGER, FIXNUMP, FLOATP, FOUR_INTEGER, FOURTEEN_INTEGER, FUNCTION, FUNCTION_SPEC_P, FUNCTIONP, FUNLESS, FWHEN, GET, GETHASH, GETHASH_WITHOUT_VALUES, GUID_P, HASH_TABLE_ITERATOR_P, HASH_TABLE_P, IDENTITY, IF_DOES_NOT_EXIST_KEYWORD, IF_EXISTS_KEYWORD, IGNORE, INITIALIZATION_TYPE, INITIALIZER, INPUT_KEYWORD, INPUT_STREAM_P, INTEGERP, INTERNAL_KEYWORD, IO_KEYWORD, KEYWORDP, KILL_KEYWORD, LAMBDA_SYMBOL, LEXICAL, LIST, LISTP, LISTS, LOCK_P, LONG_BIGNUM_P, MACRO_ENV, MACRO_FORM, MEDIUM_BIGNUM_P, MEMBER, MINUS_ONE_INTEGER, MULTIPLE_VALUE_LIST, MUST, NCONC, NEW_VERSION_KEYWORD, NIL, NINE_INTEGER, NINETEEN_INTEGER, NREVERSE, NTH, NTH_VALUE, NULL, NULL_INPUT, NULL_OUTPUT, NUM_E_SYMBOL, NUM_GT_SYMBOL, NUM_GTE_SYMBOL, NUM_LT_SYMBOL, NUM_LTE_SYMBOL, NUM_NE_SYMBOL, NUMBERP, ONE_HUNDRED_THIRTY_SEVEN_INTEGER, ONE_HUNDRED_TWENTY_SEVEN_INTEGER, ONE_INTEGER, ONE_THOUSAND_INTEGER, OPTIONAL_SYMBOL, OTHERWISE, OUTPUT_KEYWORD, OUTPUT_STREAM_P, OVERWRITE_KEYWORD, PACKAGEP, PCASE, PCOND, PIF, PROBE_KEYWORD, PROCESS_TO_END, PROCESSP, PROCLAIM, PROGN, PUNLESS, PWHEN, QUERY_IO, QUIT, QUOTE, RENAME_AND_DELETE_KEYWORD, REST_SYMBOL, RET, RET_NIL, RET_T, RETURN_TAG, REVERSE, RW_LOCK_P, SECOND, SEQUENCEP, SEVEN_INTEGER, SEVENTEEN_INTEGER, SHORT_BIGNUM_P, SHOW_STACK_TRACES, SIX_INTEGER, SIXTEEN_INTEGER, SIXTY_FOUR_INTEGER, SORT, SSS, STANDARD_INPUT, STANDARD_OUTPUT, START_KEYWORD, STREAMP, STRING_E_SYMBOL, STRING_EQUAL_SYMBOL, STRING_GREATER_THAN_OR_EQUAL_SYMBOL, STRING_GREATER_THAN_SYMBOL, STRING_GT_SYMBOL, STRING_GTE_SYMBOL, STRING_LESS_THAN_OR_EQUAL_SYMBOL, STRING_LESS_THAN_SYMBOL, STRING_LT_SYMBOL, STRING_LTE_SYMBOL, STRING_NE_SYMBOL, STRING_NOT_EQUAL_SYMBOL, STRINGP, STRUCTURE_P, SUPERSEDE_KEYWORD, SUSPEND_TYPE_CHECKING, SYMBOL_FUNCTION, SYMBOL_VALUE, SYMBOLP, T, TEN_INTEGER, TERMINAL_IO, TEXT_KEYWORD, THIRTEEN_INTEGER, THIRTY_FOUR_INTEGER, THIRTY_THREE_INTEGER, THIRTY_TWO_INTEGER, THREE_INTEGER, TRACE_OUTPUT, TRUE, TWELVE_INTEGER, TWENTY_INTEGER, TWO_HUNDRED_FIFTY_FOUR_INTEGER, TWO_HUNDRED_FORTY_FOUR_INTEGER, TWO_INTEGER, UNDECLARED, UNPROVIDED, VALUES, VECTOR, VECTORP, WITH_ERROR_HANDLER, WITH_STATIC_AREA, WITH_THREAD_PRIVATE_AREA, WITH_WORKING_AREA, WORLD, ZERO_DOUBLE, ZERO_INTEGER |
|
Method Summary |
static SubLObject |
declare_inference_tactician_strategic_uninterestingness_file()
|
void |
declareFunctions()
Declares the mapping between functions and symbols for all named
functions defined in the file. |
static SubLObject |
hl_module_only_applies_to_hl_predicatesP(SubLObject hl_module)
|
static SubLObject |
hl_module_requires_hl_predicate_transformationP(SubLObject hl_module,
SubLObject problem)
|
static SubLObject |
hl_module_requires_unbound_predicate_transformationP(SubLObject hl_module)
|
static SubLObject |
inference_chooses_to_set_aside_problem_int(SubLObject inference,
SubLObject problem,
SubLObject justifyP)
|
static SubLObject |
inference_chooses_to_set_aside_transformation_tactic_int(SubLObject inference,
SubLObject transformation_tactic,
SubLObject justifyP)
|
static SubLObject |
inference_chooses_to_throw_away_all_transformations_on_problem_int(SubLObject inference,
SubLObject problem,
SubLObject justifyP)
|
static SubLObject |
inference_chooses_to_throw_away_all_transformations_on_problemP_internal(SubLObject inference,
SubLObject problem)
|
static SubLObject |
inference_chooses_to_throw_away_all_transformations_on_problemP(SubLObject inference,
SubLObject problem)
|
static SubLObject |
inference_chooses_to_throw_away_problem_int(SubLObject inference,
SubLObject problem,
SubLObject justifyP)
|
static SubLObject |
inference_chooses_to_throw_away_transformation_tactic_int(SubLObject inference,
SubLObject transformation_tactic,
SubLObject justifyP)
|
static SubLObject |
inference_chooses_to_throw_away_transformation_tacticP(SubLObject inference,
SubLObject transformation_tactic)
|
static SubLObject |
init_inference_tactician_strategic_uninterestingness_file()
|
void |
initializeVariables()
Initializes all global variables and private internal variables
for constants defined in the file. |
static SubLObject |
legacy_strategy_chooses_to_throw_away_tacticP(SubLObject strategy,
SubLObject tactic,
SubLObject motivation)
|
static SubLObject |
problem_has_executed_a_complete_removal_tacticP(SubLObject problem,
SubLObject strategic_context)
|
static SubLObject |
problem_has_executed_a_complete_tacticP(SubLObject problem,
SubLObject strategic_context,
SubLObject type)
|
static SubLObject |
problem_has_relevant_supporting_problemP(SubLObject problem,
SubLObject strategic_context,
SubLObject consider_transformation_tacticsP)
|
static SubLObject |
problem_uses_evaluatable_predicateP(SubLObject problem)
|
static SubLObject |
problem_uses_hl_predicateP(SubLObject problem)
|
void |
runTopLevelForms()
Runs all top-level forms in order. |
static SubLObject |
setup_inference_tactician_strategic_uninterestingness_file()
|
static SubLObject |
simple_strategy_chooses_to_ignore_tacticP(SubLObject strategy,
SubLObject tactic)
|
static SubLObject |
simple_strategy_chooses_to_set_aside_problem_int(SubLObject strategy,
SubLObject problem,
SubLObject justifyP)
|
static SubLObject |
simple_strategy_chooses_to_set_aside_problemP(SubLObject strategy,
SubLObject problem)
|
static SubLObject |
simple_strategy_chooses_to_set_aside_tactic_int(SubLObject strategy,
SubLObject tactic,
SubLObject justifyP)
|
static SubLObject |
simple_strategy_chooses_to_set_aside_tacticP(SubLObject strategy,
SubLObject tactic)
|
static SubLObject |
simple_strategy_chooses_to_set_aside_transformation_tactic_int(SubLObject strategy,
SubLObject transformation_tactic,
SubLObject justifyP)
|
static SubLObject |
simple_strategy_chooses_to_throw_away_problem_int(SubLObject strategy,
SubLObject problem,
SubLObject justifyP)
|
static SubLObject |
simple_strategy_chooses_to_throw_away_problemP(SubLObject strategy,
SubLObject problem)
|
static SubLObject |
simple_strategy_chooses_to_throw_away_tactic_int(SubLObject strategy,
SubLObject tactic,
SubLObject justifyP)
|
static SubLObject |
simple_strategy_chooses_to_throw_away_tacticP(SubLObject strategy,
SubLObject tactic)
|
static SubLObject |
simple_strategy_chooses_to_throw_away_transformation_tactic_int(SubLObject strategy,
SubLObject transformation_tactic,
SubLObject justifyP)
|
static SubLObject |
simple_strategy_chooses_to_throw_away_transformation_tacticP_internal(SubLObject strategy,
SubLObject transformation_tactic)
|
static SubLObject |
simple_strategy_chooses_to_throw_away_transformation_tacticP(SubLObject strategy,
SubLObject transformation_tactic)
|
static SubLObject |
simple_strategy_deems_rewrite_tactic_redundantP(SubLObject strategy,
SubLObject tactic)
|
static SubLObject |
strategy_admits_all_tactics_wrt_proof_specP(SubLObject strategy)
|
static SubLObject |
strategy_admits_tactic_wrt_proof_specP(SubLObject strategy,
SubLObject tactic)
|
static SubLObject |
strategy_allows_use_of_hl_moduleP(SubLObject strategy,
SubLObject hl_module)
|
static SubLObject |
strategy_allows_use_of_tactic_hl_moduleP(SubLObject strategy,
SubLObject tactic)
|
static SubLObject |
strategy_deems_problem_tactically_uninterestingP(SubLObject strategy,
SubLObject problem)
|
static SubLObject |
strategy_has_enough_proofs_for_problemP(SubLObject strategy,
SubLObject problem)
|
static SubLObject |
strategy_last_uninterestingness_explanation()
|
static SubLObject |
tactic_completeP(SubLObject tactic,
SubLObject strategic_context)
|
static SubLObject |
tactic_disallowedP(SubLObject tactic,
SubLObject strategic_context)
|
static SubLObject |
tactic_exceeds_productivity_limitP(SubLObject tactic,
SubLObject strategic_context)
|
static SubLObject |
tactic_impossibleP(SubLObject tactic,
SubLObject strategic_context)
|
static SubLObject |
tactic_preferredP(SubLObject tactic,
SubLObject strategic_context)
|
static SubLObject |
tactic_requires_evaluatable_predicate_transformationP(SubLObject tactic)
|
static SubLObject |
tactic_requires_hl_predicate_transformationP(SubLObject tactic)
|
static SubLObject |
tactic_requires_unbound_predicate_transformationP(SubLObject tactic)
|
static SubLObject |
tactically_uninteresting_problem_p(SubLObject problem)
|
static SubLObject |
why_inference_chooses_to_set_aside_problem(SubLObject inference,
SubLObject problem)
|
static SubLObject |
why_inference_chooses_to_set_aside_transformation_tactic(SubLObject inference,
SubLObject transformation_tactic)
|
static SubLObject |
why_inference_chooses_to_throw_away_problem(SubLObject inference,
SubLObject problem)
|
static SubLObject |
why_simple_strategy_chooses_to_set_aside_problem(SubLObject strategy,
SubLObject problem)
|
static SubLObject |
why_simple_strategy_chooses_to_set_aside_tactic(SubLObject strategy,
SubLObject tactic)
|
static SubLObject |
why_simple_strategy_chooses_to_set_aside_transformation_tactic(SubLObject strategy,
SubLObject transformation_tactic)
|
| Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
me
public static final SubLFile me
myName
public static final java.lang.String myName
- See Also:
- Constant Field Values
$strategy_gathering_uninterestingness_explanationsP$
public static SubLSymbol $strategy_gathering_uninterestingness_explanationsP$
- Whether we are gathering explanations of strategic uninterestingness
$list0
public static final SubLList $list0
$kw1$REMOVAL
public static final SubLSymbol $kw1$REMOVAL
$kw2$TRANSFORMATION
public static final SubLSymbol $kw2$TRANSFORMATION
$str3$thrown_away_wrt_both_removal_and_
public static final SubLString $str3$thrown_away_wrt_both_removal_and_
$str4$thrown_away_wrt_removal
public static final SubLString $str4$thrown_away_wrt_removal
$str5$thrown_away_wrt_transformation
public static final SubLString $str5$thrown_away_wrt_transformation
$kw6$THROW_AWAY_TACTIC
public static final SubLSymbol $kw6$THROW_AWAY_TACTIC
$str7$
public static final SubLString $str7$
$str8$set_aside_wrt_both_removal_and_tr
public static final SubLString $str8$set_aside_wrt_both_removal_and_tr
$str9$set_aside_wrt_removal
public static final SubLString $str9$set_aside_wrt_removal
$str10$set_aside_wrt_transformation
public static final SubLString $str10$set_aside_wrt_transformation
$kw11$SET_ASIDE_TACTIC
public static final SubLSymbol $kw11$SET_ASIDE_TACTIC
$str12$problem_is_tactically_uninteresti
public static final SubLString $str12$problem_is_tactically_uninteresti
$str13$inference_is_not_continuable__and
public static final SubLString $str13$inference_is_not_continuable__and
$str14$non_good_problem_has_already_exec
public static final SubLString $str14$non_good_problem_has_already_exec
$str15$rewrite_tactic_is_redundant
public static final SubLString $str15$rewrite_tactic_is_redundant
$str16$HL_module_is_forbidden
public static final SubLString $str16$HL_module_is_forbidden
$kw17$GENERALIZED_REMOVAL
public static final SubLSymbol $kw17$GENERALIZED_REMOVAL
$str18$problem_is_strategically_no_good
public static final SubLString $str18$problem_is_strategically_no_good
$str19$tactic_exceeds_productivity_limit
public static final SubLString $str19$tactic_exceeds_productivity_limit
$sym20$STRATEGIC_CONTEXT_P
public static final SubLSymbol $sym20$STRATEGIC_CONTEXT_P
$str21$problem_exceeds_max_proof_depth
public static final SubLString $str21$problem_exceeds_max_proof_depth
$str22$proof_checker_mode_is_enabled_and
public static final SubLString $str22$proof_checker_mode_is_enabled_and
$sym23$INFERENCE_CHOOSES_TO_THROW_AWAY_ALL_TRANSFORMATIONS_ON_PROBLEM_
public static final SubLSymbol $sym23$INFERENCE_CHOOSES_TO_THROW_AWAY_ALL_TRANSFORMATIONS_ON_PROBLEM_
$kw24$_MEMOIZED_ITEM_NOT_FOUND_
public static final SubLSymbol $kw24$_MEMOIZED_ITEM_NOT_FOUND_
$str25$problem_uses_an_HL_predicate__HL_
public static final SubLString $str25$problem_uses_an_HL_predicate__HL_
$str26$problem_uses_an_evaluatable_predi
public static final SubLString $str26$problem_uses_an_evaluatable_predi
$kw27$REWRITE
public static final SubLSymbol $kw27$REWRITE
$str28$problem_exceeds_max_transformatio
public static final SubLString $str28$problem_exceeds_max_transformatio
$sym29$SIMPLE_STRATEGY_CHOOSES_TO_THROW_AWAY_TRANSFORMATION_TACTIC_
public static final SubLSymbol $sym29$SIMPLE_STRATEGY_CHOOSES_TO_THROW_AWAY_TRANSFORMATION_TACTIC_
$str30$proof_checker_mode_is_enabled__an
public static final SubLString $str30$proof_checker_mode_is_enabled__an
$str31$the_rule_for_this_tactic_has_an_i
public static final SubLString $str31$the_rule_for_this_tactic_has_an_i
$str32$tactic_requires_HL_predicate_tran
public static final SubLString $str32$tactic_requires_HL_predicate_tran
$str33$tactic_requires_unbound_predicate
public static final SubLString $str33$tactic_requires_unbound_predicate
$str34$tactic_requires_evaluatable_predi
public static final SubLString $str34$tactic_requires_evaluatable_predi
$list35
public static final SubLList $list35
$const36$isa
public static final SubLObject $const36$isa
$const37$genls
public static final SubLObject $const37$genls
$kw38$COMPLETE
public static final SubLSymbol $kw38$COMPLETE
$kw39$INCOMPLETE
public static final SubLSymbol $kw39$INCOMPLETE
$kw40$IMPOSSIBLE
public static final SubLSymbol $kw40$IMPOSSIBLE
$kw41$PREFERRED
public static final SubLSymbol $kw41$PREFERRED
$kw42$DISPREFERRED
public static final SubLSymbol $kw42$DISPREFERRED
$kw43$DISALLOWED
public static final SubLSymbol $kw43$DISALLOWED
$kw44$CONTENT
public static final SubLSymbol $kw44$CONTENT
$kw45$EXECUTED
public static final SubLSymbol $kw45$EXECUTED
$kw46$JOIN_ORDERED
public static final SubLSymbol $kw46$JOIN_ORDERED
$kw47$JOIN
public static final SubLSymbol $kw47$JOIN
$kw48$LOGICAL
public static final SubLSymbol $kw48$LOGICAL
$kw49$ANYTHING
public static final SubLSymbol $kw49$ANYTHING
$kw50$NOTHING
public static final SubLSymbol $kw50$NOTHING
$str51$Time_to_support_proof_spec_admitt
public static final SubLString $str51$Time_to_support_proof_spec_admitt
$list52
public static final SubLList $list52
$list53
public static final SubLList $list53
$list54
public static final SubLList $list54
$list55
public static final SubLList $list55
$list56
public static final SubLList $list56
$list57
public static final SubLList $list57
$const58$ist
public static final SubLObject $const58$ist
$const59$not
public static final SubLObject $const59$not
$kw60$POS
public static final SubLSymbol $kw60$POS
$kw61$NEG
public static final SubLSymbol $kw61$NEG
$list62
public static final SubLList $list62
$sym63$CLET
public static final SubLSymbol $sym63$CLET
$list64
public static final SubLList $list64
$sym65$STRATEGY_NOTE_UNINTERESTINGNESS_EXPLANATION
public static final SubLSymbol $sym65$STRATEGY_NOTE_UNINTERESTINGNESS_EXPLANATION
$sym66$STRATEGY_POSSIBLY_NOTE_UNINTERESTINGNESS_EXPLANATION
public static final SubLSymbol $sym66$STRATEGY_POSSIBLY_NOTE_UNINTERESTINGNESS_EXPLANATION
$sym67$STRATEGY_UNINTERESTINGNESS_EXPLANATION_P
public static final SubLSymbol $sym67$STRATEGY_UNINTERESTINGNESS_EXPLANATION_P
$list68
public static final SubLList $list68
$list69
public static final SubLList $list69
$kw70$ALLOW_OTHER_KEYS
public static final SubLSymbol $kw70$ALLOW_OTHER_KEYS
$kw71$PROBLEM
public static final SubLSymbol $kw71$PROBLEM
$kw72$TACTIC
public static final SubLSymbol $kw72$TACTIC
$kw73$LINK
public static final SubLSymbol $kw73$LINK
$kw74$SUBEXPLANATION
public static final SubLSymbol $kw74$SUBEXPLANATION
$sym75$PWHEN
public static final SubLSymbol $sym75$PWHEN
$sym76$_STRATEGY_GATHERING_UNINTERESTINGNESS_EXPLANATIONS__
public static final SubLSymbol $sym76$_STRATEGY_GATHERING_UNINTERESTINGNESS_EXPLANATIONS__
$list77
public static final SubLList $list77
$list78
public static final SubLList $list78
$sym79$STRATEGY_UNINTERESTINGNESS_EXPLANATION_TYPE_P
public static final SubLSymbol $sym79$STRATEGY_UNINTERESTINGNESS_EXPLANATION_TYPE_P
$sym80$PROBLEM_P
public static final SubLSymbol $sym80$PROBLEM_P
$sym81$TACTIC_P
public static final SubLSymbol $sym81$TACTIC_P
$sym82$PROBLEM_LINK_P
public static final SubLSymbol $sym82$PROBLEM_LINK_P
legacy_strategy_chooses_to_throw_away_tacticP
public static final SubLObject legacy_strategy_chooses_to_throw_away_tacticP(SubLObject strategy,
SubLObject tactic,
SubLObject motivation)
simple_strategy_chooses_to_throw_away_problemP
public static final SubLObject simple_strategy_chooses_to_throw_away_problemP(SubLObject strategy,
SubLObject problem)
simple_strategy_chooses_to_throw_away_problem_int
public static final SubLObject simple_strategy_chooses_to_throw_away_problem_int(SubLObject strategy,
SubLObject problem,
SubLObject justifyP)
simple_strategy_chooses_to_throw_away_tacticP
public static final SubLObject simple_strategy_chooses_to_throw_away_tacticP(SubLObject strategy,
SubLObject tactic)
simple_strategy_chooses_to_throw_away_tactic_int
public static final SubLObject simple_strategy_chooses_to_throw_away_tactic_int(SubLObject strategy,
SubLObject tactic,
SubLObject justifyP)
problem_has_executed_a_complete_removal_tacticP
public static final SubLObject problem_has_executed_a_complete_removal_tacticP(SubLObject problem,
SubLObject strategic_context)
strategy_allows_use_of_tactic_hl_moduleP
public static final SubLObject strategy_allows_use_of_tactic_hl_moduleP(SubLObject strategy,
SubLObject tactic)
strategy_allows_use_of_hl_moduleP
public static final SubLObject strategy_allows_use_of_hl_moduleP(SubLObject strategy,
SubLObject hl_module)
simple_strategy_chooses_to_set_aside_problemP
public static final SubLObject simple_strategy_chooses_to_set_aside_problemP(SubLObject strategy,
SubLObject problem)
why_simple_strategy_chooses_to_set_aside_problem
public static final SubLObject why_simple_strategy_chooses_to_set_aside_problem(SubLObject strategy,
SubLObject problem)
simple_strategy_chooses_to_set_aside_problem_int
public static final SubLObject simple_strategy_chooses_to_set_aside_problem_int(SubLObject strategy,
SubLObject problem,
SubLObject justifyP)
simple_strategy_chooses_to_set_aside_tacticP
public static final SubLObject simple_strategy_chooses_to_set_aside_tacticP(SubLObject strategy,
SubLObject tactic)
why_simple_strategy_chooses_to_set_aside_tactic
public static final SubLObject why_simple_strategy_chooses_to_set_aside_tactic(SubLObject strategy,
SubLObject tactic)
simple_strategy_chooses_to_set_aside_tactic_int
public static final SubLObject simple_strategy_chooses_to_set_aside_tactic_int(SubLObject strategy,
SubLObject tactic,
SubLObject justifyP)
simple_strategy_chooses_to_ignore_tacticP
public static final SubLObject simple_strategy_chooses_to_ignore_tacticP(SubLObject strategy,
SubLObject tactic)
strategy_deems_problem_tactically_uninterestingP
public static final SubLObject strategy_deems_problem_tactically_uninterestingP(SubLObject strategy,
SubLObject problem)
strategy_has_enough_proofs_for_problemP
public static final SubLObject strategy_has_enough_proofs_for_problemP(SubLObject strategy,
SubLObject problem)
tactically_uninteresting_problem_p
public static final SubLObject tactically_uninteresting_problem_p(SubLObject problem)
problem_has_relevant_supporting_problemP
public static final SubLObject problem_has_relevant_supporting_problemP(SubLObject problem,
SubLObject strategic_context,
SubLObject consider_transformation_tacticsP)
why_inference_chooses_to_set_aside_problem
public static final SubLObject why_inference_chooses_to_set_aside_problem(SubLObject inference,
SubLObject problem)
inference_chooses_to_set_aside_problem_int
public static final SubLObject inference_chooses_to_set_aside_problem_int(SubLObject inference,
SubLObject problem,
SubLObject justifyP)
why_inference_chooses_to_throw_away_problem
public static final SubLObject why_inference_chooses_to_throw_away_problem(SubLObject inference,
SubLObject problem)
inference_chooses_to_throw_away_problem_int
public static final SubLObject inference_chooses_to_throw_away_problem_int(SubLObject inference,
SubLObject problem,
SubLObject justifyP)
inference_chooses_to_throw_away_all_transformations_on_problemP_internal
public static final SubLObject inference_chooses_to_throw_away_all_transformations_on_problemP_internal(SubLObject inference,
SubLObject problem)
inference_chooses_to_throw_away_all_transformations_on_problemP
public static final SubLObject inference_chooses_to_throw_away_all_transformations_on_problemP(SubLObject inference,
SubLObject problem)
inference_chooses_to_throw_away_all_transformations_on_problem_int
public static final SubLObject inference_chooses_to_throw_away_all_transformations_on_problem_int(SubLObject inference,
SubLObject problem,
SubLObject justifyP)
problem_uses_hl_predicateP
public static final SubLObject problem_uses_hl_predicateP(SubLObject problem)
problem_uses_evaluatable_predicateP
public static final SubLObject problem_uses_evaluatable_predicateP(SubLObject problem)
simple_strategy_deems_rewrite_tactic_redundantP
public static final SubLObject simple_strategy_deems_rewrite_tactic_redundantP(SubLObject strategy,
SubLObject tactic)
- Returns:
- booleanp; Whether TACTIC is redundant for STRATEGY to execute, because
the problem store topology indicates that such a rewrite has already been done.
tactic_exceeds_productivity_limitP
public static final SubLObject tactic_exceeds_productivity_limitP(SubLObject tactic,
SubLObject strategic_context)
why_simple_strategy_chooses_to_set_aside_transformation_tactic
public static final SubLObject why_simple_strategy_chooses_to_set_aside_transformation_tactic(SubLObject strategy,
SubLObject transformation_tactic)
simple_strategy_chooses_to_set_aside_transformation_tactic_int
public static final SubLObject simple_strategy_chooses_to_set_aside_transformation_tactic_int(SubLObject strategy,
SubLObject transformation_tactic,
SubLObject justifyP)
why_inference_chooses_to_set_aside_transformation_tactic
public static final SubLObject why_inference_chooses_to_set_aside_transformation_tactic(SubLObject inference,
SubLObject transformation_tactic)
inference_chooses_to_set_aside_transformation_tactic_int
public static final SubLObject inference_chooses_to_set_aside_transformation_tactic_int(SubLObject inference,
SubLObject transformation_tactic,
SubLObject justifyP)
simple_strategy_chooses_to_throw_away_transformation_tacticP_internal
public static final SubLObject simple_strategy_chooses_to_throw_away_transformation_tacticP_internal(SubLObject strategy,
SubLObject transformation_tactic)
simple_strategy_chooses_to_throw_away_transformation_tacticP
public static final SubLObject simple_strategy_chooses_to_throw_away_transformation_tacticP(SubLObject strategy,
SubLObject transformation_tactic)
simple_strategy_chooses_to_throw_away_transformation_tactic_int
public static final SubLObject simple_strategy_chooses_to_throw_away_transformation_tactic_int(SubLObject strategy,
SubLObject transformation_tactic,
SubLObject justifyP)
inference_chooses_to_throw_away_transformation_tacticP
public static final SubLObject inference_chooses_to_throw_away_transformation_tacticP(SubLObject inference,
SubLObject transformation_tactic)
inference_chooses_to_throw_away_transformation_tactic_int
public static final SubLObject inference_chooses_to_throw_away_transformation_tactic_int(SubLObject inference,
SubLObject transformation_tactic,
SubLObject justifyP)
tactic_requires_hl_predicate_transformationP
public static final SubLObject tactic_requires_hl_predicate_transformationP(SubLObject tactic)
hl_module_requires_hl_predicate_transformationP
public static final SubLObject hl_module_requires_hl_predicate_transformationP(SubLObject hl_module,
SubLObject problem)
hl_module_only_applies_to_hl_predicatesP
public static final SubLObject hl_module_only_applies_to_hl_predicatesP(SubLObject hl_module)
tactic_requires_unbound_predicate_transformationP
public static final SubLObject tactic_requires_unbound_predicate_transformationP(SubLObject tactic)
hl_module_requires_unbound_predicate_transformationP
public static final SubLObject hl_module_requires_unbound_predicate_transformationP(SubLObject hl_module)
tactic_requires_evaluatable_predicate_transformationP
public static final SubLObject tactic_requires_evaluatable_predicate_transformationP(SubLObject tactic)
tactic_completeP
public static final SubLObject tactic_completeP(SubLObject tactic,
SubLObject strategic_context)
tactic_impossibleP
public static final SubLObject tactic_impossibleP(SubLObject tactic,
SubLObject strategic_context)
tactic_preferredP
public static final SubLObject tactic_preferredP(SubLObject tactic,
SubLObject strategic_context)
tactic_disallowedP
public static final SubLObject tactic_disallowedP(SubLObject tactic,
SubLObject strategic_context)
problem_has_executed_a_complete_tacticP
public static final SubLObject problem_has_executed_a_complete_tacticP(SubLObject problem,
SubLObject strategic_context,
SubLObject type)
strategy_admits_tactic_wrt_proof_specP
public static final SubLObject strategy_admits_tactic_wrt_proof_specP(SubLObject strategy,
SubLObject tactic)
strategy_admits_all_tactics_wrt_proof_specP
public static final SubLObject strategy_admits_all_tactics_wrt_proof_specP(SubLObject strategy)
strategy_last_uninterestingness_explanation
public static final SubLObject strategy_last_uninterestingness_explanation()
declare_inference_tactician_strategic_uninterestingness_file
public static final SubLObject declare_inference_tactician_strategic_uninterestingness_file()
init_inference_tactician_strategic_uninterestingness_file
public static final SubLObject init_inference_tactician_strategic_uninterestingness_file()
setup_inference_tactician_strategic_uninterestingness_file
public static final SubLObject setup_inference_tactician_strategic_uninterestingness_file()
declareFunctions
public void declareFunctions()
- Description copied from interface:
SubLFile
- Declares the mapping between functions and symbols for all named
functions defined in the file.
Like CRTL define.
initializeVariables
public void initializeVariables()
- Description copied from interface:
SubLFile
- Initializes all global variables and private internal variables
for constants defined in the file.
Like CRTL init.
runTopLevelForms
public void runTopLevelForms()
- Description copied from interface:
SubLFile
- Runs all top-level forms in order.
Like CRTL setup.