projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2c1e5b3) | patch
Refactor model building for quantifiers to be a single pass, simplification. Modify...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 24 Mar 2017 14:37:13 +0000 (09:37 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 24 Mar 2017 14:37:32 +0000 (09:37 -0500)
commit67ea40d24cbbcd3f490248754a6abc1989bacc7b
treef74d7a52a5046e346035b1c5b5abec1f17004033tree
parent2c1e5b35ba688c0df297b0510058454c54bab54dcommit | diff
Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
27 files changed:
src/options/quantifiers_options diff | blob | history
src/smt/model.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/ambqi_builder.cpp diff | blob | history
src/theory/quantifiers/ambqi_builder.h diff | blob | history
src/theory/quantifiers/bounded_integers.cpp 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/first_order_model.cpp diff | blob | history
src/theory/quantifiers/first_order_model.h diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/full_model_check.h diff | blob | history
src/theory/quantifiers/inst_propagator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/model_builder.h diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.h 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/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history