1 /********************* */
2 /*! \file theory_rewriterules_params.h
4 ** Original author: bobot
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Parameters for the rewrite rules theory
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
20 #include "cvc4_private.h"
22 #ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H
23 #define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H
27 namespace rewriterules
{
30 Specify if the propagation is done by lemma or by real theory propagation
32 static const bool propagate_as_lemma
= true;
35 Cache the instantiation of rules in order to remove duplicate
37 static const bool cache_match
= true;
40 Compute when the rules are created which terms in the body can lead
41 to new instantiation (try only single trigger). During propagation
42 we check if the instantiation of these terms are known terms.
44 static const bool compute_opt
= true;
47 rewrite the matching found
49 static const bool rewrite_instantiation
= true;
52 use the representative for the matching found
54 static const bool representative_instantiation
= false;
57 Wait the specified number of check after a new propagation (a
58 previous unknown guards becomes true) is found before verifying again the guards.
60 Allow to break loop with other theories.
62 static const size_t checkSlowdown
= 0;
65 Use the current model to eliminate guard before asking for notification
67 static const bool useCurrentModel
= false;
70 Simulate rewriting by tagging rewritten terms.
72 static const bool simulateRewritting
= true;
75 Do narrowing at full effort
77 static const bool narrowing_full_effort
= false;
80 Direct rewrite: Add rewrite rules directly in the rewriter.
82 static const bool direct_rewrite
= false;
84 }/* CVC4::theory::rewriterules namespace */
85 }/* CVC4::theory namespace */
88 #endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H */