projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8dc28ec) | patch
Shorter explanations for strings based on tracking which parts of normal forms are...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 1 Mar 2016 22:29:14 +0000 (16:29 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 1 Mar 2016 22:29:14 +0000 (16:29 -0600)
commit811834a6aeab1e055b0417eaf988fc682e74e65a
tree0c9067c163a4c09faf7e10493124abedf63436fctree
parent8dc28ec4709b847a995d57bc39b8bfbaf7c5a344commit | diff
Shorter explanations for strings based on tracking which parts of normal forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.
16 files changed:
src/Makefile.am diff | blob | history
src/options/quantifiers_options diff | blob | history
src/options/strings_options diff | blob | history
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/quantifiers/anti_skolem.cpp [new file with mode: 0644] blob
src/theory/quantifiers/anti_skolem.h [new file with mode: 0644] blob
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/quant_split.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/anti-sk-simp.smt2 [new file with mode: 0755] blob