projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ad18245) | patch
Simplification of the preregister and register throught a NodeVisitor class. The...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Wed, 24 Aug 2011 21:03:19 +0000 (21:03 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Wed, 24 Aug 2011 21:03:19 +0000 (21:03 +0000)
commit278cdeb360322c7e9ae4b102abd740d101f37c6d
tree4c6c79e73b1c9cb60b21c8ffb743c4218f61094ftree
parentad18245c092ea6e5b998b556aaec74ef9109bd8ccommit | diff
Simplification of the preregister and register throught a NodeVisitor class. The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.
src/smt/smt_engine.cpp diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/builtin/kinds diff | blob | history
src/theory/theory.cpp diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/theory/uf/kinds diff | blob | history
src/util/Makefile.am diff | blob | history
src/util/node_visitor.h [new file with mode: 0644] blob