diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-15 12:34:51 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-15 12:34:51 -0500 |
| commit | f58c881034d3b0193dfee8fabf451cc0e9ea20ab (patch) | |
| tree | 09cd8349c8c5d462d628eba4c95814f931692e00 /src/theory/quantifiers/theory_quantifiers.cpp | |
| parent | 411ced2c475e5ccb4c114ce2c77a39bf93d139f4 (diff) | |
Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable e-matching when --strings-exp is enabled.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index efe40aaa8..7ad13b3a8 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -72,8 +72,11 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) { void TheoryQuantifiers::preRegisterTerm(TNode n) { Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; - if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){ - getQuantifiersEngine()->registerQuantifier( n ); + if( n.getKind()==FORALL ){ + if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ + getQuantifiersEngine()->registerQuantifier( n ); + Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl; + } } } |