From c3c8d013d2a879eaa1d205e57af32a7f8bb8c0b7 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 2 Dec 2016 14:25:07 -0600 Subject: Bug fixes and refactoring of parametric datatypes, add some regressions. --- src/theory/quantifiers/ce_guided_instantiation.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp') diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index ecf4bb74d..f4b63f929 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -17,7 +17,6 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" @@ -277,7 +276,7 @@ void CegInstantiation::preRegisterQuantifier( Node q ) { Node pat = q[2][0][0]; if( pat.getKind()==APPLY_UF ){ TypeNode tn = pat[0].getType(); - if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( dt.isSygus() ){ //do unfolding if it induces Boolean structure, @@ -696,7 +695,7 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) if( n.getKind()==APPLY_UF ){ TypeNode tn = n[0].getType(); Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl; - if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( dt.isSygus() ){ Trace("cegqi-eager") << "Unfold eager : " << n << std::endl; @@ -769,7 +768,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { std::string f(ss.str()); f.erase(f.begin()); TypeNode tn = prog.getType(); - Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( dt.isSygus() ); //get the solution -- cgit v1.2.3