S

SMTInterpol

Settings | Report Duplicate

0

I Use This!

Very Low Activity

Commits : Listings

Analyzed 1 day ago. based on code collected 1 day ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Jul 26, 2024 — Jul 26, 2025 Showing page 18 of 62 Search / Filter on:
Fix bug in final check.	Tanja Schindler	More...				almost 5 years ago
Fix bug in InstClause.	Tanja Schindler	More...				almost 5 years ago
fix: typo '@EQ' instead of 'EQ'	henkele	More...				almost 5 years ago
Don't unnecessarily backtrack in clearAssumption	Jochen Hoenicke	More...				almost 5 years ago
fix: handle annotated term in getSymbols()	henkele	More...				almost 5 years ago
More Tests for Unknown ReMus, eliminated a bug in the ConstraintAdministrationSolver (which only occurs if it is reset multiple times)	Leonard Fichtner	More...				almost 5 years ago
modify addQuantifier: only add quantifier if unsupported variable appears in interpolant	henkele	More...				almost 5 years ago
fix: deep check after resolution step was not using quantified interpolant	henkele	More...				almost 5 years ago
modify checkInductivity: assert auxiliary equations in partitions in which the corresponding auxiliary variable appears in the interpolant and/or in which the outermost symbol of the replaced term is contained.	henkele	More...				almost 5 years ago
modify checkInductivity: replace variables in interpolant by constant terms before asserting them	henkele	More...				almost 5 years ago
modify checkInductivity: purify literals and replace variables by constant terms before they get asserted	henkele	More...				almost 5 years ago
modify checkInductivity: initialize some maps resp. sets to store info about used variables, the terms that they replaced and the constant terms which are used to obtain a closed formula	henkele	More...				almost 5 years ago
modify fixVars: use getTermVariables instead of using getAllSubterms and collecting all term variables from this set.	henkele	More...				almost 5 years ago
add function to collect all TermVariables in a term.	henkele	More...				almost 5 years ago
modify interpolation of congruence: do not use source of literal but its occurrence when dealing with special case, i.e. mixed Term in congruence and outermost function symbol is AB-shared	henkele	More...				almost 5 years ago
add null check within fixupAndLet to convert(): term may contain a purification variable even if auxMap is null.	henkele	More...				almost 5 years ago
A little additional logging in remus, more javadocs, a little exception case added	Leonard Fichtner	More...				almost 5 years ago
Add statistics.	Tanja Schindler	More...				almost 5 years ago
add function to purify a term and directly replace purification variables through a constant term.	henkele	More...				almost 5 years ago
add function to replace auxiliary variables by a constant term in order to obtain a closed formula.	henkele	More...				almost 5 years ago
use interpolate instantiation lemma in walkLeafNode(), replace non-shared symbols and add quantifiers if necessary.	henkele	More...				almost 5 years ago
add function to interpolate instantiation lemmata	henkele	More...				almost 5 years ago
modify getAllSubTerms: annotated terms are no longer included in subterm set.	henkele	More...				almost 5 years ago
add: if necessary introduce quantifiers after each resolution step. Maybe there is a better place to do this.	henkele	More...				almost 5 years ago
fix in replaceNonSharedSymbols: remove TermVariables from the set of non-shared symbols as they do not need to be replaced.	henkele	More...				almost 5 years ago
Adapt interpolation of congruence lemma to deal with mixed terms in literals. We now need the clause as additional input to retrieve the source partition.	henkele	More...				almost 5 years ago
add function to add quantifiers to provisional interpolants if they contain unsupported variables.	henkele	More...				almost 5 years ago
Bugfix for logging of time needed for heuristic. Time is now elapsed with nanoTime(). Further, I have noticed, that the UnsatCores that I return are non-standard. I will fix this in near future.	Leonard Fichtner	More...				almost 5 years ago
Changed the FIRST heuristic to now shrink the vanilla UC, also refactoring	Leonard Fichtner	More...				almost 5 years ago
add function to sort variables in dependency order.	henkele	More...				almost 5 years ago

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