projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 411ced2) | patch
Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable...
authorajreynol <andrew.j.reynolds@gmail.com>
Sun, 15 May 2016 17:34:51 +0000 (12:34 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Sun, 15 May 2016 17:34:51 +0000 (12:34 -0500)
commitf58c881034d3b0193dfee8fabf451cc0e9ea20ab
tree09cd8349c8c5d462d628eba4c95814f931692e00tree
parent411ced2c475e5ccb4c114ce2c77a39bf93d139f4commit | diff
Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable e-matching when --strings-exp is enabled.
17 files changed:
contrib/run-script-cascj8-fof diff | blob | history
contrib/run-script-cascj8-tfa diff | blob | history
src/options/options_handler.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/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/kinds diff | blob | history
src/theory/datatypes/theory_datatypes_type_rules.h 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/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.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/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history