projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8a8455d) | patch
Add priorities to getNextDecision. Properly handle case for finite types + unbounded...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 3 Nov 2016 20:09:12 +0000 (15:09 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 3 Nov 2016 20:09:26 +0000 (15:09 -0500)
commitb6d5d0b11cf7624cd7a3e0a2f6f77d83d2f7001a
treeb0e5acbce9023c28bf1bb85eee5da97b79c94561tree
parent8a8455d955c084c9a9f7add1f4e4da6b1dbc35ebcommit | diff
Add priorities to getNextDecision. Properly handle case for finite types + unbounded heaps in sep logic. Fix another simple memory leak in sygus.
25 files changed:
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.h diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.h diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/sep/theory_sep.cpp diff | blob | history
src/theory/sep/theory_sep.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.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.h diff | blob | history
test/regress/regress0/sep/Makefile.am diff | blob | history
test/regress/regress0/sep/sep-fmf-priority.smt2 [new file with mode: 0644] blob