diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 10:13:45 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 10:13:45 -0500 |
| commit | 4ff2946e1338d3f500b7e6bababee50fadad68d6 (patch) | |
| tree | 6f1306e4476e3f7496d7a4e045e63d942802a392 /src/theory/quantifiers/conjecture_generator.h | |
| parent | 1b2e6c81be2a8ab0656ff2ee3938ef4587e24e25 (diff) | |
Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.h')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index b6e17e7a1..c89d0f2ee 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -39,7 +39,7 @@ public: std::map< TNode, OpArgIndex > d_child; std::vector< TNode > d_ops; std::vector< TNode > d_op_terms; - void addTerm( ConjectureGenerator * s, TNode n, unsigned index = 0 ); + void addTerm( std::vector< TNode >& terms, TNode n, unsigned index = 0 ); Node getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args ); void getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms ); }; |