Configuration for the smt tactic preprocessor. The preprocessor is applied whenever a new hypothesis is introduced.
simp_attr: is the attribute name for the simplification lemmas that are used during the preprocessing step.
max_steps: it is the maximum number of steps performed by the simplifier.
zeta: if tt, then zeta reduction (i.e., unfolding let-expressions) is used during preprocessing.
- cc_cfg : cc_config
- em_cfg : ematch_config
- pre_cfg : smt_pre_config
- em_attr : name
Configuration for the smt_state object.
- em_attr: is the attribute name for the hinst_lemmas that are used for ematching
Return tt iff classical excluded middle was enabled at smt_state.mk
Try to close main goal by using equalities implied by the congruence closure module.
Produce new facts using heuristic lemma instantiation based on E-matching.
This tactic tries to match patterns from lemmas in the main goal with terms
in the main goal. The set of lemmas is populated with theorems
tagged with the attribute specified at smt_config.em_attr, and lemmas
added using tactics such as smt_tactic.add_lemmas.
The current set of lemmas can be retrieved using the tactic smt_tactic.get_lemmas.
Remark: the given predicate is applied to every new instance. The instance is only added to the state if the predicate returns tt.
Produce new facts using heuristic lemma instantiation based on E-matching. This tactic tries to match patterns from the given lemmas with terms in the main goal.
Preprocess the given term using the same simplifications rules used when we introduce a new hypothesis. The result is pair containing the resulting term and a proof that it is equal to the given one.
iterate_at_most n t: repeat the given tactic at most n times or until t fails
iterate_exactly n t : execute t n times
This lift operation will restart the SMT state. It is useful for using tactics that change the set of hypotheses.
Apply the given tactic to all goals.
LCF-style AND_THEN tactic. It applies tac1, and if succeed applies tac2 to each subgoal produced by tac1
Add a new goal for t, and the hypothesis (h : t) in the current goal.
Add the hypothesis (h : t) in the current goal if v has type t.
Add a new goal for t, and the hypothesis (h : t := ?M) in the current goal.
Add the hypothesis (h : t := v) in the current goal if v has type t.
Add (h : t := pr) to the current goal
Add (h : t) to the current goal, given a proof (pr : t)
Return a proof for e, if 'e' is a known fact in the main goal.
Return a refutation for e (i.e., a proof for (not e)), if 'e' has been refuted in the main goal.