| Age | Commit message (Collapse) | Author |
|---|
|
|
|
support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
|
|
|
|
|
|
|
|
|
|
issue.
|
|
|
|
Conflicts:
src/theory/strings/theory_strings.cpp
|
|
is needed.
|
|
|
|
|
|
|
|
is needed.
|
|
|
|
instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
to bogus model). Minor cleanup of QCF.
|
|
bottleneck).
|
|
for QCF_MC mode.
|
|
domain instantiation breadth-first.
|
|
SMT-Lib
|
|
added). Bug fix for QCF (was missing instantiations due to not using getRepresentative).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.
|
|
|
|
|
|
|
|
|
|
|
|
|
