diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_conjecture.cpp')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_conjecture.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index 7fcc3f2af..3af623f13 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -20,6 +20,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" @@ -296,7 +297,7 @@ void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& mode Node dr = Rewriter::rewrite( d[i] ); if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){ if( constructed_cand ){ - ic.push_back( d_qe->getTermUtil()->getSkolemizedBody( dr[0] ).negate() ); + ic.push_back(d_qe->getSkolemize()->getSkolemizedBody(dr[0]).negate()); } if( sk_refine ){ Assert( !isGround() ); @@ -347,9 +348,11 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ Node ce_q = d_ce_sk[0][k]; if( !ce_q.isNull() ){ Assert( !d_inner_vars_disj[k].empty() ); - Assert( d_inner_vars_disj[k].size()==d_qe->getTermUtil()->d_skolem_constants[ce_q].size() ); + std::vector<Node> skolems; + d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems); + Assert(d_inner_vars_disj[k].size() == skolems.size()); std::vector< Node > model_values; - getModelValues( d_qe->getTermUtil()->d_skolem_constants[ce_q], model_values ); + getModelValues(skolems, model_values); sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() ); sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() ); }else{ |