diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-27 20:08:01 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-27 18:08:01 -0700 |
| commit | f8bda2828e5f3e984623e38ea0778d36144bd05c (patch) | |
| tree | 425258145cd80aab9a537bf4042d476ec494711f /src/theory/quantifiers/extended_rewrite.h | |
| parent | fa55d0680afab5d319f393bafd3f7ecdf8870b1f (diff) | |
Refactor extended rewriter, move rewrites to aggressive (#2387)
This is work towards #2305.
With this PR, CVC4's performance is fairly reasonable on the Kind2 BMC benchmarks with --decision=internal --ext-rew-prep --ext-rew-prep-agg.
Diffstat (limited to 'src/theory/quantifiers/extended_rewrite.h')
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 4d3f08b1d..29f3b7bb3 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -64,6 +64,9 @@ class ExtendedRewriter * may be applied as a preprocessing step. */ bool d_aggr; + /** true/false nodes */ + Node d_true; + Node d_false; /** cache that the extended rewritten form of n is ret */ void setCache(Node n, Node ret); /** add to children @@ -213,10 +216,13 @@ class ExtendedRewriter * (2) a variable y such that x < y based on an ordering, * then this method adds x to vars and y to subs and return true, otherwise * it returns false. + * If usePred is true, we may additionally add n -> true, or n[0] -> false + * is n is a negation. */ bool inferSubstitution(Node n, std::vector<Node>& vars, - std::vector<Node>& subs); + std::vector<Node>& subs, + bool usePred = false); /** extended rewrite * * Prints debug information, indicating the rewrite n ---> ret was found. |