Age | Commit message (Collapse) | Author |
|
|
|
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.
|
|
|
|
|
|
records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.
|
|
incomplete for fmc.
|
|
|
|
|
|
to quantifier instantiations.
|
|
enumerator and codatatype rewriter, further simplify fmc.
|
|
The explanation for a != b is now:
1. a == find(a)
2. ( find(a) == find(b) ) == false
3. find(b) == b
This simplifies the creation of transitivity proofs for disequalities.
|
|
for selectors applied to codatatype values.
|
|
|
|
variables known to be don't-cares.
|
|
Breaking an edge between the sat solver and command.h.
|
|
type.h.
|
|
process.
|
|
|
|
be compiled.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|