projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1267706) | patch
* removing rewriteEquality from the rewriter
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 14 Jun 2012 01:08:11 +0000 (01:08 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 14 Jun 2012 01:08:11 +0000 (01:08 +0000)
commitdd713fdbc16b07adc8011dea09b53fb3bc168662
treecc58788ed58fd86c5aaa58c0fafa2bbb0f8b6567tree
parent1267706e0c508ada17d75c07c4606eb108ae5309commit | diff
* removing rewriteEquality from the rewriter
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
18 files changed:
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/arrays/theory_arrays_rewriter.h diff | blob | history
src/theory/booleans/theory_bool_rewriter.h diff | blob | history
src/theory/builtin/theory_builtin_rewriter.h diff | blob | history
src/theory/bv/bitblaster.cpp diff | blob | history
src/theory/bv/theory_bv_rewriter.h diff | blob | history
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/mkrewriter diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/rewriter.cpp diff | blob | history
src/theory/rewriter.h diff | blob | history
src/theory/rewriter_tables_template.h diff | blob | history
src/theory/rewriterules/theory_rewriterules_rewriter.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/uf/theory_uf_rewriter.h diff | blob | history
test/regress/regress0/aufbv/Makefile.am diff | blob | history
test/regress/regress0/aufbv/bug348.smt [new file with mode: 0644] blob