Even apply formulas that have been blocked, as last steps in a proof.
Even apply formulas that have been blocked, as last
steps in a proof. this can be necessary in order to
generate genuine models (ModelSearchProver
)
Turn ground constraints into disjunctive normal form
Even split propositional formulae that do not contain quantifiers or eliminated constants
Ignore universal quantifiers in a problem that would require free variables, by converting the quantifiers to existential ones.
Use heuristics to distinguish between constructor and query function symbols, and make the latter ones partial
Options for solving problems in positive or negated version
Resolve negative predicate literals in clauses with positive facts
Portfolios optimised for particular domains
Globally, we can also choose to construct proofs depending on whether interpolation specs were given (the default)
Represent numeric side conditions (inequalities) in quantified formulas
using the StrengthenTree
constructor
Represent numeric side conditions (inequalities) in quantified formulas
using the StrengthenTree
constructor
Accept an extended set of escape sequences in strings: \\, \x, \a, \b, \f, \n, \r, \t, \v.
Accept an extended set of escape sequences in strings: \\, \x, \a, \b, \f, \n, \r, \t, \v. Without this option, only the official SMT-LIB escapes are accepted.
Use the FunctionalConsistency
dummy theory
to represent applications of functionality in proofs.
Use the FunctionalConsistency
dummy theory
to represent applications of functionality in proofs.