diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 03:01:41 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 03:01:41 +0000 |
| commit | a81ea9670349abe03da96cf45fbaa115c4098325 (patch) | |
| tree | 7bb03f748aaaddee5da8d3a9a17c416659d0fb73 /src/smt/smt_engine.h | |
| parent | e116ffc5c17be0b4a4a3b92ec43edd07c7c59c82 (diff) | |
Adding constant propagation code - needs more testing - off by default
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 4c0fed74c..e0f544f9e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -239,6 +239,8 @@ class CVC4_PUBLIC SmtEngine { TimerStat d_definitionExpansionTime; /** time spent in non-clausal simplification */ TimerStat d_nonclausalSimplificationTime; + /** Num of constant propagations found during nonclausal simp */ + IntStat d_numConstantProps; /** time spent in static learning */ TimerStat d_staticLearningTime; /** time spent in simplifying ITEs */ |