| Age | Commit message (Collapse) | Author |
|---|
|
for dynamically allocating these tags upon request.
|
|
variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations. Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort.
|
|
for E-matching. Minor work to equality infer.
|
|
updates to datatypes lemmas, other minor changes.
|
|
|
|
fmfBoundIntLazy for stringsExp.
|
|
entailment checks. Other minor infrastructure.
|
|
|
|
equality path reconstruction
|
|
|
|
|
|
CegConjecture.
|
|
|
|
|
|
|
|
Squash-merge from the proof branch
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
QuantConflictFind.
|
|
involve uninterpreted sorts, including bounded integer quantification.
|
|
changes default behavior.
|
|
sort inference, related to constants. Add several quantifiers options, minor refactoring.
|
|
universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.
|
|
cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.
|
|
as well.
|
|
|
|
forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.
|
|
|
|
|
|
FMF.
|
|
solver. Minor additions to datatypes and qcf.
|
|
|
|
|
|
Disable ITE terms in quant conflict find.
|
|
|
|
reductions in quantifiers engine.
|
|
fixes in quantifiers related to subtypes/parametric sorts. Make macros trace dependencies for get-unsat-core. Add regressions.
|
|
|
|
preprocessing, implement get-qe-disjunct.
|
|
rewriter.
|
|
|
|
|
