diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-11 14:00:27 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-11 14:00:27 +0000 |
commit | 57790a14676596e8c6ed42ff7ecd8038ddbaf09b (patch) | |
tree | 7e4d5c81f197beab924092fb72cc945d48a47e69 /src/smt/smt_engine.h | |
parent | 5181426cd8def23d67b69227fff033ef12850e68 (diff) |
Added some ITE rewrites,
Added ITE simplifier - on by default only for QF_LIA benchmarks
Fixed one bug in arrays
Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 43d3e1125..10a37b712 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -229,6 +229,19 @@ class CVC4_PUBLIC SmtEngine { TimerStat d_nonclausalSimplificationTime; /** time spent in static learning */ TimerStat d_staticLearningTime; + /** time spent in simplifying ITEs */ + TimerStat d_simpITETime; + /** time spent removing ITEs */ + TimerStat d_iteRemovalTime; + /** time spent in theory preprocessing */ + TimerStat d_theoryPreprocessTime; + /** time spent converting to CNF */ + TimerStat d_cnfConversionTime; + /** Num of assertions before ite removal */ + IntStat d_numAssertionsPre; + /** Num of assertions after ite removal */ + IntStat d_numAssertionsPost; + /** how the SMT engine got the answer -- SAT solver or DE */ BackedStat<std::string> d_statResultSource; |