projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a2923ec) | patch
Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 5 May 2016 23:44:47 +0000 (18:44 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 5 May 2016 23:44:56 +0000 (18:44 -0500)
commitc87ee73ad3d51c238700f236c18e425b80e8e7ac
treeaa4214b0fa7d6ef275605253fee88899fa3ce230tree
parenta2923ec61b601b0e3f4f78f22fffc1c2421f0d81commit | diff
Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges.  Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
24 files changed:
proofs/lfsc_checker/check.cpp diff | blob | history
proofs/lfsc_checker/expr.cpp diff | blob | history
proofs/lfsc_checker/expr.h diff | blob | history
proofs/lfsc_checker/main.cpp diff | blob | history
proofs/signatures/th_bv_bitblast.plf diff | blob | history
src/options/options_handler.cpp diff | blob | history
src/options/quantifiers_modes.cpp diff | blob | history
src/options/quantifiers_modes.h diff | blob | history
src/options/quantifiers_options diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/inst_propagator.cpp diff | blob | history
src/theory/quantifiers/inst_propagator.h diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/strings-small.sy [new file with mode: 0644] blob