projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a3a436b) | patch
Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 9 Sep 2016 19:14:09 +0000 (14:14 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 9 Sep 2016 19:14:09 +0000 (14:14 -0500)
commita97944b850f201fd692aa870e830b8fa0369c541
tree7f4ff2086c236b2041ea3546cd82f1af0ba997bctree
parenta3a436b7b52eee9b6b5c93d58fb84e707b5e832bcommit | diff
Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic.  Update logics on sep regressions.
43 files changed:
src/options/quantifiers_options diff | blob | history
src/options/sep_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/sep/theory_sep.cpp diff | blob | history
src/theory/sep/theory_sep.h diff | blob | history
test/regress/regress0/sep/Makefile.am diff | blob | history
test/regress/regress0/sep/chain-int.smt2 diff | blob | history
test/regress/regress0/sep/crash1220.smt2 diff | blob | history
test/regress/regress0/sep/dispose-list-4-init.smt2 diff | blob | history
test/regress/regress0/sep/dup-nemp.smt2 diff | blob | history
test/regress/regress0/sep/emp2-quant-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/loop-1220.smt2 diff | blob | history
test/regress/regress0/sep/nemp.smt2 diff | blob | history
test/regress/regress0/sep/nspatial-simp.smt2 diff | blob | history
test/regress/regress0/sep/pto-01.smt2 diff | blob | history
test/regress/regress0/sep/pto-02.smt2 diff | blob | history
test/regress/regress0/sep/pto-04.smt2 diff | blob | history
test/regress/regress0/sep/sep-01.smt2 diff | blob | history
test/regress/regress0/sep/sep-02.smt2 diff | blob | history
test/regress/regress0/sep/sep-03.smt2 diff | blob | history
test/regress/regress0/sep/sep-find2.smt2 diff | blob | history
test/regress/regress0/sep/sep-neg-1refine.smt2 diff | blob | history
test/regress/regress0/sep/sep-neg-nstrict.smt2 diff | blob | history
test/regress/regress0/sep/sep-neg-nstrict2.smt2 diff | blob | history
test/regress/regress0/sep/sep-neg-simple.smt2 diff | blob | history
test/regress/regress0/sep/sep-neg-swap.smt2 diff | blob | history
test/regress/regress0/sep/sep-nterm-again.smt2 diff | blob | history
test/regress/regress0/sep/sep-nterm-val-model.smt2 diff | blob | history
test/regress/regress0/sep/sep-plus1.smt2 diff | blob | history
test/regress/regress0/sep/sep-simp-unc.smt2 diff | blob | history
test/regress/regress0/sep/sep-simp-unsat-emp.smt2 diff | blob | history
test/regress/regress0/sep/simple-neg-sat.smt2 diff | blob | history
test/regress/regress0/sep/split-find-unsat-w-emp.smt2 diff | blob | history
test/regress/regress0/sep/split-find-unsat.smt2 diff | blob | history
test/regress/regress0/sep/wand-0526-sat.smt2 diff | blob | history
test/regress/regress0/sep/wand-crash.smt2 diff | blob | history
test/regress/regress0/sep/wand-false.smt2 diff | blob | history
test/regress/regress0/sep/wand-nterm-simp.smt2 diff | blob | history
test/regress/regress0/sep/wand-nterm-simp2.smt2 diff | blob | history
test/regress/regress0/sep/wand-simp-sat.smt2 diff | blob | history
test/regress/regress0/sep/wand-simp-sat2.smt2 diff | blob | history
test/regress/regress0/sep/wand-simp-unsat.smt2 diff | blob | history