projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2c09bb1) | patch
Do not drop patterns during boolean term rewriting. Narrow sygus search space based...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 22 Jan 2015 08:40:51 +0000 (09:40 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 22 Jan 2015 08:40:51 +0000 (09:40 +0100)
commit9867d5a61ccde30f7e4616a652ef86a9b15ae6d8
tree2b8987cbac1745268bfee3d66b2a06973ff53683tree
parent2c09bb19994bc1baa97e30642a0281692c181a4bcommit | diff
Do not drop patterns during boolean term rewriting. Narrow sygus search space based on commutative operators.
src/smt/boolean_terms.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history