projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8d29fef) | patch
Handle fmf.card as input from user, add support in SMT2 parser, as requested by Marti...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 9 Apr 2014 20:43:37 +0000 (15:43 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 9 Apr 2014 20:59:38 +0000 (15:59 -0500)
commit40fbc4aa1961cbeea2451251e54909285d2f4292
treeed4032bec587ef0e1ea0318a38c2d990e9f1f19ftree
parent8d29fef7286ab07c630c65284bfb399e2f7f5326commit | diff
Handle fmf.card as input from user, add support in SMT2 parser, as requested by Martin Brain.  Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.
src/parser/smt2/Smt2.g diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.h diff | blob | history
src/theory/uf/theory_uf_type_rules.h diff | blob | history