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 22, 2024 — Jul 22, 2025 Showing page 53 of 62 Search / Filter on:
Fix for empty sort problem	Juergen Christ	More...				over 9 years ago
Non-termination fix due to assumption watching	Juergen Christ	More...				over 9 years ago
Strong usage checks for assumptions	Juergen Christ	More...				over 9 years ago
Implemented get-unsat-assumptions	Juergen Christ	More...				over 9 years ago
Proofs under assumptions	Juergen Christ	More...				over 9 years ago
SMTLIB 2.5 model output	Juergen Christ	More...				over 9 years ago
Fixed a typo in args parser	Juergen Christ	More...				over 9 years ago
Working version of checking under assumptions	Juergen Christ	More...				over 9 years ago
Fixed setup of assertion store	Juergen Christ	More...				over 9 years ago
Bugfix UnsatCoreCollector: Also collect primary	Jochen Hoenicke	More...				over 9 years ago
Start of assumptions	Juergen Christ	More...				over 9 years ago
EPR: almost-all atoms now seem to work on one example	Alexander Nutz	More...				over 9 years ago
backup	Alexander Nutz	More...				over 9 years ago
towards "almost-all atoms"	Alexander Nutz	More...				over 9 years ago
backup before slight change of plan	Alexander Nutz	More...				over 9 years ago
epr: increment	Alexander Nutz	More...				over 9 years ago
Separate mSmtInterpol and mCheckingSolver in Interpolator.	Jochen Hoenicke	More...				over 9 years ago
Use timeout handler from SMTInterpol directly.	Jochen Hoenicke	More...				over 9 years ago
Complain about quantifier only on assert.	Jochen Hoenicke	More...				over 9 years ago
Minor documentation fix	Jochen Hoenicke	More...				over 9 years ago
Removed recursion from UnsatCoreCollector	Juergen Christ	More...				over 9 years ago
fixes - unquantified EprPredicateAtoms are now also registered via addAtom in the DPLLEngine - towards EprPredicate model handling - updated Clausifier.toPositive(..) sucht that it can handle quantified formulas	Alexander Nutz	More...				over 9 years ago
basic changes towards EPR handling added some new classes for managing EPR atoms and the model that will be computed	Alexander Nutz	More...				over 9 years ago
towards EPR support. Main changes so far: \n 1. if a quantified logic is set, the predicate-to-function-conversion of CClosure is not done \n 2. quantifiers are removed from the formula, TermVariables remaining in the formula are assumed to be implicitly forall-quantified (existentially quantified formulas are skolemized, EPR forbids quantifier alternation and existential inside forall) \n 3. clausification registers clauses containing TermVariables in the (new) EprTheory, instead of the DPLLEngine	Alexander Nutz	More...				over 9 years ago
Fix bitvector constant cache.	Jochen Hoenicke	More...				over 9 years ago
Changed timeout logic.	Jochen Hoenicke	More...				over 9 years ago
Bugfix for array model comparison	Juergen Christ	More...				almost 10 years ago
Purge timer queue after canceling task	Juergen Christ	More...				almost 10 years ago
Reworked output of rationals of sort Real	Juergen Christ	More...				almost 10 years ago
Weakened assertion in insertPropagetdLiteralBefore	Jochen Hoenicke	More...				almost 10 years ago

←
1
2
…
49
50
51
52
53
54
55
56
57
…
61
62
→