diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
| commit | d7dc7c2b3038b862af5ea55e7cf6b1fc4e1fe684 (patch) | |
| tree | d6c229a2659bfcb3cdf7c7c786414ecc1e59e61c /src/theory/quantifiers/theory_quantifiers.cpp | |
| parent | 1ec95c559074ed7575a0165deb16fcee45920e9f (diff) | |
Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 649d34922..373a8a0da 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -169,7 +169,7 @@ Node TheoryQuantifiers::getNextDecisionRequest(){ void TheoryQuantifiers::assertUniversal( Node n ){ Assert( n.getKind()==FORALL ); - if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ + if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ getQuantifiersEngine()->assertQuantifier( n, true ); } } |