Refactoring of conjecture generator. Determine subgoals are non-canonical based...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 16 Sep 2014 14:56:10 +0000 (16:56 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 16 Sep 2014 14:56:10 +0000 (16:56 +0200)
commitbc3f6fdaf84da10f5fd5ad3a5f5700ec242dd082
tree80f57a46c798f6dbcb2afa712a6853cd1c07c042
parent2cf533e6d7f459484786db9e242bb2e97bab4db0
Refactoring of conjecture generator.  Determine subgoals are non-canonical based on ground equalities.  Add filtering options to options file.
src/smt/smt_engine.cpp
src/theory/quantifiers/conjecture_generator.cpp [changed mode: 0644->0755]
src/theory/quantifiers/conjecture_generator.h [changed mode: 0644->0755]
src/theory/quantifiers/options
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h