projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e892d95) | patch
Replace the sequence of hardcoded addTheory() calls with a use of the theory traits...
authorMorgan Deters <mdeters@gmail.com>
Tue, 28 Feb 2012 19:51:10 +0000 (19:51 +0000)
committerMorgan Deters <mdeters@gmail.com>
Tue, 28 Feb 2012 19:51:10 +0000 (19:51 +0000)
commitc492f41a58c1299105d58a3561afccd09e0532bc
tree723364eec109e2c531f10473b2e16cdfd3a88596tree
parente892d95b55fd93fb5b92c230447b5e135da8e07acommit | diff
Replace the sequence of hardcoded addTheory() calls with a use of the theory traits---with the effect that everything with a kinds file is registered as a theory.  Eventually we may want a more dynamic way of selecting theory implementations, but for now we don't have a need for this.  Expected performance impact: none.  (This commit addresses and re-closes the reopened bug #307.)
src/smt/smt_engine.cpp diff | blob | history