diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-17 16:41:56 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-17 16:42:10 +0100 |
| commit | 6c49fe8691cf011237be30f4062affc79d8a5314 (patch) | |
| tree | 43de311707603716902815226840083ee26e1749 /src/theory/quantifiers/inst_match.h | |
| parent | 304f3d632766a445b9e2fb9dd617b2c2cfd50fb2 (diff) | |
Improve relevant domain computation for arithmetic, full saturation strategy. Simply E-matching trigger selection, do not use non-trivial triggers unless necessary. Add option to strings.
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
| -rw-r--r-- | src/theory/quantifiers/inst_match.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 6424b67d3..d66d331e5 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -76,7 +76,7 @@ public: void applyRewrite(); /** get */ Node get( int i ); - void getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ); + void getTerms( Node f, std::vector< Node >& inst ); /** set */ void setValue( int i, TNode n ); bool set( QuantifiersEngine* qe, int i, TNode n ); |