diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 15:21:34 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 15:21:40 -0600 |
| commit | 793361d81f0766c6a28ff699ed5447d9b8f8c123 (patch) | |
| tree | fff4d0f9c809400abb22edc13403867558b7426f /src/theory/quantifiers_engine.cpp | |
| parent | b7be76b58846a68dea4c1fcae19d6c3f087994b9 (diff) | |
Correct subtyping for arrays, disable subtyping for predicate subtypes. Bug fixes in quantifiers related to subtypes/parametric sorts. Make macros trace dependencies for get-unsat-core. Add regressions.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ca8a09082..ce6c929b2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -687,13 +687,6 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v Assert( f.getKind()==FORALL ); Assert( vars.size()==terms.size() ); Node body = getInstantiation( f, vars, terms, doVts ); //do virtual term substitution - if( doVts ){ - body = Rewriter::rewrite( body ); - Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl; - Node body_r = d_term_db->rewriteVtsSymbols( body ); - Trace("quant-vts-debug") << " ...result: " << body_r << std::endl; - body = body_r; - } body = quantifiers::QuantifiersRewriter::preprocess( body, true ); Trace("inst-debug") << "...preprocess to " << body << std::endl; Trace("inst-assert") << "(assert " << body << ")" << std::endl; @@ -934,10 +927,13 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i ); }else{ //ensure the type is correct - terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() ); + terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() ); } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; - Assert( !terms[i].isNull() ); + if( terms[i].isNull() ){ + Trace("inst-add-debug") << " -> Failed to make term vector, due to term/type restrictions." << std::endl; + return false; + } #ifdef CVC4_ASSERTIONS Assert( !quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ); #endif |