projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 53c301a) | patch
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 2 May 2016 14:16:30 +0000 (09:16 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 2 May 2016 14:16:36 +0000 (09:16 -0500)
commitf65b945119341ae8afa69bd0b7dc005c9fcc768b
treec264125578d3b8edd752740701789f7b1e4e26bbtree
parent53c301aa808218abe725014e01bddc19fe11a116commit | diff
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
24 files changed:
proofs/lfsc_checker/scccode.cpp diff | blob | history
proofs/lfsc_checker/scccode.h diff | blob | history
proofs/lfsc_checker/sccwriter.cpp diff | blob | history
proofs/signatures/th_quant.plf diff | blob | history
src/theory/quantifiers/ambqi_builder.cpp diff | blob | history
src/theory/quantifiers/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/candidate_generator.h diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.h diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.h diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/model_builder.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/rewrite_engine.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/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/partial-trigger.smt2 [new file with mode: 0644] blob