diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 16:22:19 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 16:22:26 -0500 |
| commit | 2c0482cfb9b8164670cf56187e127d38c5d05bcf (patch) | |
| tree | 804f7806944b9175fdaea8cc919566ca302ddf09 /src/theory/arith/congruence_manager.cpp | |
| parent | 0e513c05b2e0ae3b8e2d08514ccb8007258f963b (diff) | |
Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
Diffstat (limited to 'src/theory/arith/congruence_manager.cpp')
| -rw-r--r-- | src/theory/arith/congruence_manager.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 04d8d50ea..f6e702f5b 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -43,6 +43,8 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true) { d_ee.addFunctionKind(kind::NONLINEAR_MULT); + d_ee.addFunctionKind(kind::EXPONENTIAL); + d_ee.addFunctionKind(kind::SINE); //module to infer additional equalities based on normalization if( options::sNormInferEq() ){ d_eq_infer = new quantifiers::EqualityInference(c, true); |