Age | Commit message (Collapse) | Author |
|
for E-matching. Minor work to equality infer.
|
|
updates to datatypes lemmas, other minor changes.
|
|
|
|
|
|
cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
|
|
|
|
quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
|
|
Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.
|
|
|
|
how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.
|
|
assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.
|
|
|
|
quantifiers check. Minor fix for conjecture generation.
|
|
|
|
|
|
|
|
|
|
support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
|
|
|
|
for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp). Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model. Add option for relational triggers such as x = f(y), --relational-trigger.
|
|
|
|
|
|
boolean terms, improvement for pre skolemization
|
|
bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
|
|
infrastructure for recognizing quantifier macros
|
|
code from quantifiers-specific code
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat.
The namespaces weren't changed, only the file locations.
|