projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0348b52) | patch
Support for separation logic. Enable cbqi by default for pure BV.
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 17 Jun 2016 20:55:56 +0000 (15:55 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 17 Jun 2016 20:57:28 +0000 (15:57 -0500)
commit1a2547995acc5a98c8969e628ac5e1c45b0efe94
tree0d9abd19ba7b3b742da3e745da00c0457237f84btree
parent0348b525a951a8709f9dc4b5757ce0bcb48a9472commit | diff
Support for separation logic. Enable cbqi by default for pure BV.
72 files changed:
src/Makefile.am diff | blob | history
src/Makefile.theories diff | blob | history
src/expr/Makefile.am diff | blob | history
src/expr/sepconst.cpp [new file with mode: 0644] blob
src/expr/sepconst.h [new file with mode: 0644] blob
src/options/Makefile.am diff | blob | history
src/options/sep_options [new file with mode: 0644] blob
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/boolean_terms.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/bv/bv_subtheory_algebraic.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/sep/kinds [new file with mode: 0644] blob
src/theory/sep/theory_sep.cpp [new file with mode: 0644] blob
src/theory/sep/theory_sep.h [new file with mode: 0644] blob
src/theory/sep/theory_sep_rewriter.cpp [new file with mode: 0644] blob
src/theory/sep/theory_sep_rewriter.h [new file with mode: 0644] blob
src/theory/sep/theory_sep_type_rules.h [new file with mode: 0644] blob
src/theory/term_registration_visitor.cpp diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/valuation.cpp diff | blob | history
src/theory/valuation.h diff | blob | history
test/Makefile.am diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/sep/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/sep/chain-int.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/crash1220.smt2 [new file with mode: 0755] blob
test/regress/regress0/sep/dispose-list-4-init.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/fmf-nemp-2.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/loop-1220.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/nemp.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/nspatial-simp.smt2 [new file with mode: 0755] blob
test/regress/regress0/sep/pto-01.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/pto-02.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/pto-04.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/quant_wand.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-01.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-02.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-03.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-find2.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-neg-1refine.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-neg-nstrict.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-neg-nstrict2.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-neg-simple.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-neg-swap.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-nterm-again.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-nterm-val-model.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-plus1.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/sep-simp-unc.smt2 [new file with mode: 0755] blob
test/regress/regress0/sep/sep-simp-unsat-emp.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/simple-neg-sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/split-find-unsat-w-emp.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/split-find-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/wand-0526-sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/wand-crash.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/wand-nterm-simp.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/wand-nterm-simp2.smt2 [new file with mode: 0644] blob
test/regress/regress0/sep/wand-simp-sat.smt2 [new file with mode: 0755] blob
test/regress/regress0/sep/wand-simp-sat2.smt2 [new file with mode: 0755] blob
test/regress/regress0/sep/wand-simp-unsat.smt2 [new file with mode: 0755] blob