diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-16 16:56:10 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-16 16:56:10 +0200 |
| commit | bc3f6fdaf84da10f5fd5ad3a5f5700ec242dd082 (patch) | |
| tree | 80f57a46c798f6dbcb2afa712a6853cd1c07c042 /src/theory/quantifiers/term_database.h | |
| parent | 2cf533e6d7f459484786db9e242bb2e97bab4db0 (diff) | |
Refactoring of conjecture generator. Determine subgoals are non-canonical based on ground equalities. Add filtering options to options file.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 504ecd667..91ad0135b 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -145,6 +145,8 @@ public: * subsRep is whether subs contains only representatives */ TNode evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep ); + /** same as above, but without substitution */ + TNode evaluateTerm( TNode n ); /** is entailed (incomplete check) */ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); public: |