src/theory/rewriterules/theory_rewriterules_params.h

   1 /*********************                                                        */
   2 /*! \file theory_rewriterules_params.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief Parameters for the rewrite rules theory
  15  **
  16  ** [[ Add lengthier description here ]]
  17  ** \todo document this file
  18  **/
  19
  20 #include "cvc4_private.h"
  21
  22 #ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H
  23 #define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace rewriterules {
  28
  29 /**
  30    Specify if the propagation is done by lemma or by real theory propagation
  31  */
  32 static const bool propagate_as_lemma = true;
  33
  34 /**
  35    Cache the instantiation of rules in order to remove duplicate
  36  */
  37 static const bool cache_match = true;
  38
  39 /**
  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.
  43  */
  44 static const bool compute_opt = true;
  45
  46 /**
  47    rewrite the matching found
  48  */
  49 static const bool rewrite_instantiation = true;
  50
  51 /**
  52    use the representative for the matching found
  53  */
  54 static const bool representative_instantiation = false;
  55
  56 /**
  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.
  59
  60    Allow to break loop with other theories.
  61  */
  62 static const size_t checkSlowdown = 0;
  63
  64 /**
  65    Use the current model to eliminate guard before asking for notification
  66  */
  67 static const bool useCurrentModel = false;
  68
  69 /**
  70    Simulate rewriting by tagging rewritten terms.
  71  */
  72 static const bool simulateRewritting = true;
  73
  74 /**
  75    Do narrowing at full effort
  76 */
  77 static const bool narrowing_full_effort = false;
  78
  79 /**
  80    Direct rewrite: Add rewrite rules directly in the rewriter.
  81  */
  82 static const bool direct_rewrite = false;
  83
  84 }/* CVC4::theory::rewriterules namespace */
  85 }/* CVC4::theory namespace */
  86 }/* CVC4 namespace */
  87
  88 #endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H */