projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2159129) | patch
Standardize more instances of skolems (#8351)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 24 Mar 2022 18:14:59 +0000 (13:14 -0500)
committerGitHub <noreply@github.com>
Thu, 24 Mar 2022 18:14:59 +0000 (18:14 +0000)
commit730f4cf0c5cf5af8475e338fbe28e099b14bfed5
treea357098060534f04ce5fdb3374210d99048f0670tree
parent2159129fb16b55de49dbc42c0e71293959e7be3acommit | diff
Standardize more instances of skolems (#8351)

This is work towards limiting our usage of witness terms for skolems.

It standardizes witnessing of disequalities for sets, bags, and arrays in the appropriate way that uses mkSkolemFunction(...) instead of mkSkolem(...).
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/theory/arrays/skolem_cache.cpp diff | blob | history
src/theory/arrays/skolem_cache.h diff | blob | history
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/bags/solver_state.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history