projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a84864d) | patch
More work on datatypes theory combination: fix bug in care graph, do not assign value...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 5 Nov 2014 14:32:48 +0000 (15:32 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 5 Nov 2014 14:32:48 +0000 (15:32 +0100)
commit36a5437abbddd484b8bdb18c024cc7573240054f
tree587994c441c49995624029c9094c5caeed9cf7d1tree
parenta84864da338f74958c6754696d98cd6355e798a8commit | diff
More work on datatypes theory combination: fix bug in care graph, do not assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind.  Minor fixes for fun_def_process.  Other minor changes.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/fun_def_process.cpp diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history
src/theory/uf/theory_uf_type_rules.h diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 [new file with mode: 0644] blob