S

SMTInterpol

Settings | Report Duplicate

0

I Use This!

Very Low Activity

Commits : Listings

Analyzed about 15 hours ago. based on code collected about 15 hours ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Jul 27, 2024 — Jul 27, 2025 Showing page 19 of 62 Search / Filter on:
add function to collect from a set of variables the ones that are unsupported in a given clause.	henkele	More...				almost 5 years ago
add: replace non-shared symbols after interpolating congruence lemma.	henkele	More...				almost 5 years ago
add function to replace non-shared symbols in a provisional interpolant by an auxiliary variable.	henkele	More...				almost 5 years ago
add a function to collect all possible subterms in a given term while ignoring any annotations. use getAllSubTerms instead of getSubTerms.	henkele	More...				almost 5 years ago
add TermSubstitutor to substitute a term by another term, e.g. to replace non-shared symbols occurring in a provisional interpolant.	henkele	More...				almost 5 years ago
Fix proof production for quantified formulas.	Tanja Schindler	More...				almost 5 years ago
add function to order a set of terms descending with their nested function depth	henkele	More...				almost 5 years ago
add function to compute the nesting depth of functions. used to order terms	henkele	More...				almost 5 years ago
add function to collect non-logical symbols in a term	henkele	More...				almost 5 years ago
adapt colorLiterals to color all symbols occurring in an input clause	henkele	More...				almost 5 years ago
add function to update the color of all non-logical symbols in a term according to a specific partition.	henkele	More...				almost 5 years ago
add function to collect the set of non-logical symbols in a given term that are not AB-shared in the given partition.	henkele	More...				almost 5 years ago
adopt getOccurrence() to use getOccurrenceOfUnknownTerm() instead of creating a new Occurrence for an unknown term. addOccurrence() must now create a new Occurrence and add the info to mSymbolPartition.	henkele	More...				almost 5 years ago
add example for tree interpolation with quantifier	henkele	More...				almost 5 years ago
Quant: Final check prefers instantiation with older terms.	Tanja Schindler	More...				almost 5 years ago
More logging and refactoring	Leonard Fichtner	More...				almost 5 years ago
remove set-option commands to allow overwriting on command line	Jochen Hoenicke	More...				almost 5 years ago
Add E-matching options.	Tanja Schindler	More...				almost 5 years ago
Fix comment	Jochen Hoenicke	More...				almost 5 years ago
Expand comment in checkRewriteRemoveForall.	Jochen Hoenicke	More...				almost 5 years ago
Bugfixes in handling of LBool.UNKNOWN etc. (also added additional Option to enable UNKNOWN handling) + Tests	Leonard Fichtner	More...				almost 5 years ago
Quant: Handle instances from final check and checkpoint similarly.	Tanja Schindler	More...				almost 5 years ago
Merge branch 'master' into MUSes	Leonard Fichtner	More...				almost 5 years ago
Intermediate commit because of needed merge	Leonard Fichtner	More...				almost 5 years ago
Change the check for :skolem rewrite rule.	Jochen Hoenicke	More...				almost 5 years ago
BugFix in EnumOption	Jochen Hoenicke	More...				almost 5 years ago
Little change in documentation	Leonard Fichtner	More...				almost 5 years ago
Added handling of LBool.UNKNOWN (untested)	Leonard Fichtner	More...				almost 5 years ago
Refactoring	Leonard Fichtner	More...				almost 5 years ago
Bugfix, where an error would occur, because a timeout in resumeSatisfiableCaseLoopUntilNextMus was not handled correctly. Also reactivated the guard for the expensive assert in UnexploredMap (which I previously forgot)	Leonard Fichtner	More...				almost 5 years ago

←
1
2
…
15
16
17
18
19
20
21
22
23
…
61
62
→