diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 14:25:07 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 14:25:07 -0600 |
| commit | c3c8d013d2a879eaa1d205e57af32a7f8bb8c0b7 (patch) | |
| tree | f4a8372d8cd693df5f33e8d49cea53dbb418349e /src/theory/quantifiers/ce_guided_instantiation.cpp | |
| parent | 623e701247ed08e3f59d57b18ebe42f4d4db221e (diff) | |
Bug fixes and refactoring of parametric datatypes, add some regressions.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
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 |