projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e6a5882) | patch
Properly distinguish which EQC to assign values in datatypes, use assertRepresentativ...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 7 Nov 2014 10:37:43 +0000 (11:37 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 7 Nov 2014 10:37:43 +0000 (11:37 +0100)
commit56a523d9c4dd04cedbd812570cd80e3bc94cce4c
treed53f96c61369f826ef38dbf07eea264d27f64c03tree
parente6a588264154bf4b93abd0aaac39dbf10c496e6fcommit | diff
Properly distinguish which EQC to assign values in datatypes, use assertRepresentative.  Disable regression related to records.  Enable fmf-fun related regression (modified).  Apply modified version of Morgan's patch to fix tuples/records in model.  Fix bug with sort inference + patterns.  Minor infrastructure.
src/theory/datatypes/theory_datatypes.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_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/util/sort_inference.cpp diff | blob | history
test/regress/regress0/arrays/Makefile.am diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 diff | blob | history