Age | Commit message (Collapse) | Author |
|
|
|
quantifiers check. Minor fix for conjecture generation.
|
|
|
|
|
|
|
|
* SET_SINGLETON kind renamed to just SINGLETON
* "setenum" smt2 opertor renamed to "singleton"[1]
* "in" smt2 operator renamed to "member"[2]
[1] It was anyhow accepting exactly one argument, so was bit misleading
to call set enumerator.
[2] The corresponding kind was called MEMBER, so this will also make them
consistent. Only inconsistency now is for subset: kind is called
SUBSET but operator is called "subseteq".
|
|
|
|
incorrectly applied selector terms.
|
|
|
|
formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
|
|
for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
|
|
module.
|
|
bounds. Refactoring of InstConstantAttribute to be internal to TermDb.
|
|
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
|
|
miniscoping option --ag-miniscope-quant, minor cleanup
|
|
|
|
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.
|
|
instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine
|
|
|
|
infrastructure for recognizing quantifier macros
|
|
refactoring code out of instantiators in preparation for quantifiers equality engine
|
|
be used yet), added new totality lemma option for uf strong solver
|
|
equality query
|
|
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.)
|
|
|
|
the default option for uf strong solver
|
|
duplicate of TheoryEngine::theoryOf(TheoryId)
|
|
src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat.
The namespaces weren't changed, only the file locations.
|