diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile.am | 2 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 | ||||
| -rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 309 | ||||
| -rw-r--r-- | src/theory/datatypes/datatypes_sygus.h | 69 | ||||
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 49 | ||||
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 38 | ||||
| -rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
| -rw-r--r-- | src/util/datatype.cpp | 4 | ||||
| -rw-r--r-- | src/util/datatype.h | 3 |
9 files changed, 429 insertions, 49 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index e66d590dc..c72e11809 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -235,6 +235,8 @@ libcvc4_la_SOURCES = \ theory/datatypes/theory_datatypes.h \ theory/datatypes/datatypes_rewriter.h \ theory/datatypes/theory_datatypes.cpp \ + theory/datatypes/datatypes_sygus.h \ + theory/datatypes/datatypes_sygus.cpp \ theory/sets/expr_patterns.h \ theory/sets/normal_form.h \ theory/sets/options_handlers.h \ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c6c3a896c..3db2e252d 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -526,8 +526,6 @@ void Smt2::includeFile(const std::string& filename) { void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) { - //minimize grammar goes here - for( unsigned i=0; i<cnames.size(); i++ ){ std::string name = dt.getName() + "_" + cnames[i]; std::string testerId("is-"); diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp new file mode 100644 index 000000000..af855e166 --- /dev/null +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -0,0 +1,309 @@ +/********************* */ +/*! \file theory_datatypes.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of sygus utilities for theory of datatypes + ** + ** Implementation of sygus utilities for theory of datatypes + **/ + + +#include "theory/datatypes/datatypes_sygus.h" +#include "theory/datatypes/datatypes_rewriter.h" +#include "expr/node_manager.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::datatypes; + +void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ) { + Assert( dt.isSygus() ); + Trace("sygus-split") << "Get sygus splits " << n << std::endl; + TypeNode typ, ptyp; + std::map< int, Kind > arg_kind, parg_kind; + std::map< Kind, int > kinds, pkinds; + std::map< int, Node > arg_const, parg_const; + std::map< Node, int > consts, pconsts; + + //get the kinds for child datatype + Trace("sygus-split") << "Operations for child : " << std::endl; + getSygusKinds( dt, arg_kind, kinds, arg_const, consts ); + typ = TypeNode::fromType(dt.getSygusType()); + + //compute the redundant operators + TypeNode tnn = n.getType(); + if( d_sygus_nred.find( tnn )==d_sygus_nred.end() ){ + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + bool nred = true; + std::map< int, Kind >::iterator it = arg_kind.find( i ); + if( it!=arg_kind.end() ){ + Kind dk; + if( isAntisymmetric( it->second, dk ) ){ + std::map< Kind, int >::iterator ita = kinds.find( dk ); + if( ita!=kinds.end() ){ + Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl; + //check for type mismatches + bool success = true; + unsigned j = ita->second; + for( unsigned k=0; k<2; k++ ){ + unsigned ko = k==0 ? 1 : 0; + TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() ); + TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() ); + if( tni!=tnj ){ + Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl; + success = false; + break; + } + } + if( success ){ + Trace("sygus-split") << "* Sygus norm " << dt.getName() << " : do not consider any " << arg_kind[i] << " terms." << std::endl; + nred = false; + } + } + } + } + d_sygus_nred[tnn].push_back( nred ); + } + } + + + //get parent information, if possible + Node op; + int csIndex; + int sIndex; + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + op = n.getOperator(); + Expr selectorExpr = op.toExpr(); + const Datatype& pdt = Datatype::datatypeOf(selectorExpr); + Assert( pdt.isSygus() ); + csIndex = Datatype::cindexOf(selectorExpr); + sIndex = Datatype::indexOf(selectorExpr); + + std::map< int, std::vector< bool > >::iterator it = d_sygus_pc_nred[op].find( sIndex ); + if( it==d_sygus_pc_nred[op].end() ){ + Trace("sygus-split") << " Constructor, selector index : " << csIndex << " " << sIndex << std::endl; + + Trace("sygus-split") << "Operations for parent : " << std::endl; + getSygusKinds( pdt, parg_kind, pkinds, parg_const, pconsts ); + ptyp = TypeNode::fromType(pdt.getSygusType()); + bool parentKind = parg_kind.find( csIndex )!=parg_kind.end(); + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + bool addSplit = d_sygus_nred[tnn][i]; + if( addSplit && parentKind ){ + if( arg_kind.find( i )!=arg_kind.end() ){ + addSplit = considerSygusSplitKind( dt, pdt, arg_kind[i], parg_kind[csIndex], sIndex, kinds, pkinds, consts, pconsts ); + if( !addSplit ){ + Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << arg_kind[i]; + Trace("sygus-nf") << " as argument " << sIndex << " of " << arg_kind[csIndex] << "." << std::endl; + } + }else if( arg_const.find( i )!=arg_const.end() ){ + addSplit = considerSygusSplitConst( dt, pdt, arg_const[i], parg_kind[csIndex], sIndex, kinds, pkinds, consts, pconsts ); + } + } + d_sygus_pc_nred[op][sIndex].push_back( addSplit ); + } + } + } + + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + bool addSplit = d_sygus_nred[tnn][i]; + if( addSplit ){ + if( !op.isNull() ){ + addSplit = d_sygus_pc_nred[op][sIndex][i]; + } + if( addSplit ){ + Node test = DatatypesRewriter::mkTester( n, i, dt ); + splits.push_back( test ); + } + } + } + Assert( !splits.empty() ); +} + +void SygusSplit::getSygusKinds( const Datatype& dt, std::map< int, Kind >& arg_kind, std::map< Kind, int >& kinds, + std::map< int, Node >& arg_const, std::map< Node, int >& consts ) { + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + Expr sop = dt[i].getSygusOp(); + Assert( !sop.isNull() ); + Trace("sygus-split") << " Operator #" << i << " : " << sop; + if( sop.getKind() == kind::BUILTIN ){ + Kind sk = NodeManager::operatorToKind( Node::fromExpr( sop ) ); + Trace("sygus-split") << ", kind = " << sk; + kinds[sk] = i; + arg_kind[i] = sk; + }else if( sop.isConst() ){ + Node n = Node::fromExpr( sop ); + Trace("sygus-split") << ", constant"; + consts[n] = i; + arg_const[i] = n; + } + Trace("sygus-split") << std::endl; + } +} + +bool SygusSplit::isAssoc( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_CONCAT; +} + +bool SygusSplit::isAntisymmetric( Kind k, Kind& dk ) { + if( k==GT ){ + dk = LT; + return true; + }else if( k==GEQ ){ + dk = LEQ; + return true; + }else if( k==BITVECTOR_UGT ){ + dk = BITVECTOR_ULT; + return true; + }else if( k==BITVECTOR_UGE ){ + dk = BITVECTOR_ULE; + return true; + }else if( k==BITVECTOR_SGT ){ + dk = BITVECTOR_SLT; + return true; + }else if( k==BITVECTOR_SGE ){ + dk = BITVECTOR_SLE; + return true; + }else{ + return false; + } +} + +bool SygusSplit::isIdempotentArg( Node n, Kind ik, int arg ) { + TypeNode tn = n.getType(); + if( n==getTypeValue( tn, 0 ) ){ + if( ik==PLUS || ik==BITVECTOR_PLUS || ik==BITVECTOR_OR || ik==OR ){ + return true; + }else if( ik==BITVECTOR_SHL || ik==BITVECTOR_LSHR ){ + return arg==1; + } + }else if( n==getTypeValue( tn, 1 ) ){ + if( ik==MULT || ik==BITVECTOR_MULT ){ + return true; + }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){ + return arg==1; + } + }else if( n==getTypeMaxValue( tn ) ){ + if( ik==BITVECTOR_AND ){ + return true; + } + } + return false; +} + + +bool SygusSplit::isSingularArg( Node n, Kind ik, int arg ) { + TypeNode tn = n.getType(); + if( n==getTypeValue( tn, 0 ) ){ + if( ik==MULT || ik==BITVECTOR_MULT || ik==BITVECTOR_AND || ik==AND ){ + return true; + }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){ + return arg==0; + } + }else if( n==getTypeMaxValue( tn ) ){ + if( ik==BITVECTOR_OR ){ + return true; + } + } + return false; +} + + +Node SygusSplit::getTypeValue( TypeNode tn, int val ) { + std::map< int, Node >::iterator it = d_type_value[tn].find( val ); + if( it==d_type_value[tn].end() ){ + Node n; + if( tn.isInteger() || tn.isReal() ){ + Rational c(val); + n = NodeManager::currentNM()->mkConst( c ); + }else if( tn.isBitVector() ){ + unsigned int uv = val; + BitVector bval(tn.getConst<BitVectorSize>(), uv); + n = NodeManager::currentNM()->mkConst<BitVector>(bval); + }else if( tn.isBoolean() ){ + if( val==0 || val==1 ){ + n = NodeManager::currentNM()->mkConst( val==1 ); + } + } + d_type_value[tn][val] = n; + return n; + }else{ + return it->second; + } +} + +Node SygusSplit::getTypeMaxValue( TypeNode tn ) { + std::map< TypeNode, Node >::iterator it = d_type_max_value.find( tn ); + if( it==d_type_max_value.end() ){ + Node n; + if( tn.isBitVector() ){ + n = bv::utils::mkOnes(tn.getConst<BitVectorSize>()); + } + d_type_max_value[tn] = n; + return n; + }else{ + return it->second; + } +} +bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, Kind k, Kind parent, int arg, + std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds, + std::map< Node, int >& consts, std::map< Node, int >& pconsts ) { + Assert( kinds.find( k )!=kinds.end() ); + Assert( pkinds.find( parent )!=pkinds.end() ); + Trace("sygus-split") << "Consider sygus split kind " << k << ", parent = " << parent << ", arg = " << arg << "?" << std::endl; + if( k==parent ){ + //check for associativity + if( isAssoc( k ) ){ + //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position + int firstArg = -1; + int c = pkinds[k]; + for( unsigned i=0; i<pdt[c].getNumArgs(); i++ ){ + TypeNode tni = TypeNode::fromType( ((SelectorType)pdt[c][i].getType()).getRangeType() ); + if( datatypes::DatatypesRewriter::isTypeDatatype( tni ) ){ + const Datatype& adt = ((DatatypeType)(tni).toType()).getDatatype(); + if( adt==dt ){ + firstArg = i; + break; + } + } + } + Assert( firstArg!=-1 ); + Trace("sygus-split-debug") << "Associative, with first arg = " << firstArg << std::endl; + return arg==firstArg; + } + } + if( parent==NOT ){ + //negation normal form + /* + if( k==NOT || k==ITE || ( k==AND && kinds.find( OR )!=kinds.end() ) || ( k==OR && kinds.find( AND )!=kinds.end() ) || + ( k==IFF && kinds.find( XOR )!=kinds.end() ) || ( k==XOR && kinds.find( IFF )!=kinds.end() ) ){ + return false; + } + */ + } + /* + if( parent==MINUS ){ + + } + */ + return true; +} + +bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, Node c, Kind parent, int arg, + std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds, + std::map< Node, int >& consts, std::map< Node, int >& pconsts ) { + Trace("sygus-split") << "Consider sygus split const " << c << ", parent = " << parent << ", arg = " << arg << "?" << std::endl; + return true; +} diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h new file mode 100644 index 000000000..c3491b588 --- /dev/null +++ b/src/theory/datatypes/datatypes_sygus.h @@ -0,0 +1,69 @@ +/********************* */ +/*! \file theory_datatypes.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sygus utilities for theory of datatypes + ** + ** Theory of datatypes. + **/ + +#ifndef __CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_H +#define __CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_H + +#include "expr/node.h" +#include "util/datatype.h" +#include <iostream> +#include <map> +#include "context/cdchunk_list.h" + +namespace CVC4 { +namespace theory { +namespace datatypes { + +class SygusSplit +{ +private: + std::map< TypeNode, std::vector< bool > > d_sygus_nred; + std::map< Node, std::map< int, std::vector< bool > > > d_sygus_pc_nred; + std::map< TypeNode, std::map< int, Node > > d_type_value; + std::map< TypeNode, Node > d_type_max_value; +private: + /** consider sygus split */ + bool considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, Kind k, Kind parent, int arg, + std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds, + std::map< Node, int >& consts, std::map< Node, int >& pconsts ); + bool considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, Node c, Kind parent, int arg, + std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds, + std::map< Node, int >& consts, std::map< Node, int >& pconsts ); + /** get sygus kinds */ + void getSygusKinds( const Datatype& dt, std::map< int, Kind >& arg_kind, std::map< Kind, int >& kinds, std::map< int, Node >& arg_const, std::map< Node, int >& consts ); + /** is assoc */ + bool isAssoc( Kind k ); + /** isAntisymmetric */ + bool isAntisymmetric( Kind k, Kind& dk ); + /** is idempotent arg */ + bool isIdempotentArg( Node n, Kind ik, int arg ); + /** is singular arg */ + bool isSingularArg( Node n, Kind ik, int arg ); + /** get value */ + Node getTypeValue( TypeNode tn, int val ); + /** get value */ + Node getTypeMaxValue( TypeNode tn ); +public: + /** get sygus splits */ + void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ); +}; + + +} +} +} + +#endif diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 8db9435ed..bbc8837b9 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -28,6 +28,7 @@ #include "theory/quantifiers/options.h" #include "theory/datatypes/options.h" #include "theory/type_enumerator.h" +#include "theory/datatypes/datatypes_sygus.h" #include <map> @@ -64,6 +65,12 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_true = NodeManager::currentNM()->mkConst( true ); d_dtfCounter = 0; + + if( options::sygusNormalForm() ){ + d_sygus_split = new SygusSplit; + }else{ + d_sygus_split = NULL; + } } TheoryDatatypes::~TheoryDatatypes() { @@ -238,8 +245,8 @@ void TheoryDatatypes::check(Effort e) { }else{ Trace("dt-split") << "*************Split for constructors on " << n << endl; std::vector< Node > children; - if( dt.isSygus() && options::sygusNormalForm() ){ - getSygusSplits( n, dt, children ); + if( dt.isSygus() && d_sygus_split ){ + d_sygus_split->getSygusSplits( n, dt, children ); }else{ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ Node test = DatatypesRewriter::mkTester( n, i, dt ); @@ -248,6 +255,7 @@ void TheoryDatatypes::check(Effort e) { } Assert( !children.empty() ); Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children ); + Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl; d_out->lemma( lemma ); } return; @@ -1915,40 +1923,3 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& } return false; } - -void TheoryDatatypes::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ) { - Assert( dt.isSygus() ); - Trace("sygus-split") << "Get sygus splits " << n << std::endl; - if( n.getKind()==APPLY_SELECTOR_TOTAL ){ - Node op = n.getOperator(); - std::map< Node, std::vector< bool > >::iterator it = d_sygus_splits.find( op ); - if( it==d_sygus_splits.end() ){ - Expr selectorExpr = op.toExpr(); - int csIndex = Datatype::cindexOf(selectorExpr); - int sIndex = Datatype::indexOf(selectorExpr); - Trace("sygus-split") << " Constructor, selector index : " << csIndex << " " << sIndex << std::endl; - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - Expr sop = dt[i].getSygusOp(); - Kind sk = NodeManager::operatorToKind( Node::fromExpr( sop ) ); - Trace("sygus-split") << " Operator #" << i << " : " << sop << ", kind = " << sk << std::endl; - bool addSplit = true; - //TODO - - d_sygus_splits[op].push_back( addSplit ); - } - } - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - if( d_sygus_splits[op][i] ){ - Node test = DatatypesRewriter::mkTester( n, i, dt ); - splits.push_back( test ); - } - } - Assert( !splits.empty() ); - }else{ - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - Node test = DatatypesRewriter::mkTester( n, i, dt ); - splits.push_back( test ); - } - } -} - diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 2f0ec20ec..0421213a6 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -34,10 +34,9 @@ namespace CVC4 { namespace theory { namespace datatypes { -class EqualityQueryTheory; +class SygusSplit; class TheoryDatatypes : public Theory { - friend class EqualityQueryTheory; private: typedef context::CDChunkList<Node> NodeList; typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; @@ -180,8 +179,8 @@ private: unsigned d_dtfCounter; /** expand definition skolem functions */ std::map< Node, Node > d_exp_def_skolem; - /** sygus splits */ - std::map< Node, std::vector< bool > > d_sygus_splits; + /** sygus split utility */ + SygusSplit * d_sygus_split; private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -280,8 +279,6 @@ private: bool mustCommunicateFact( Node n, Node exp ); /** check clash mod eq */ bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ); - /** get sygus splits */ - void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ); private: //equality queries bool hasTerm( TNode a ); @@ -291,6 +288,35 @@ private: public: /** get equality engine */ eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } + + +private: + /** sygus splits */ + std::map< TypeNode, std::vector< bool > > d_sygus_nred; + std::map< Node, std::map< int, std::vector< bool > > > d_sygus_pc_nred; + std::map< TypeNode, std::map< int, Node > > d_type_value; +private: + /** get sygus splits */ + void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ); + /** consider sygus split */ + bool considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, Kind k, Kind parent, int arg, + std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds, + std::map< Node, int >& consts, std::map< Node, int >& pconsts ); + bool considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, Node c, Kind parent, int arg, + std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds, + std::map< Node, int >& consts, std::map< Node, int >& pconsts ); + /** get sygus kinds */ + void getSygusKinds( const Datatype& dt, std::map< int, Kind >& arg_kind, std::map< Kind, int >& kinds, std::map< int, Node >& arg_const, std::map< Node, int >& consts ); + /** is assoc */ + bool isAssoc( Kind k ); + /** isAntisymmetric */ + bool isAntisymmetric( Kind k, Kind& dk ); + /** is idempotent arg */ + bool isIdempotentArg( Node n, Kind ik, int arg ); + /** is singular arg */ + bool isSingularArg( Node n, Kind ik, int arg ); + /** get value */ + Node getTypeValue( TypeNode tn, int val, bool maxVal = false ); };/* class TheoryDatatypes */ }/* CVC4::theory::datatypes namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index ad1508716..cebc5f245 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -196,8 +196,6 @@ option ceGuidedInst --cegqi bool :default false :read-write counterexample-guided quantifier instantiation option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" if and how to apply fairness for cegqi -option sygusMinGrammar --sygus-min-grammar bool :default false - minimize sygus grammars option sygusDecompose --sygus-decompose bool :default false decompose single invocation synthesis conjectures option sygusNormalForm --sygus-normal-form bool :default true diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index c15e103f9..fad2719f4 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -424,6 +424,10 @@ Expr Datatype::getConstructor(std::string name) const { return (*this)[name].getConstructor(); } +Type Datatype::getSygusType() const { + return d_sygus_type; +} + bool Datatype::involvesExternalType() const{ return d_involvesExt; } diff --git a/src/util/datatype.h b/src/util/datatype.h index 084202956..b91348cdb 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -632,6 +632,9 @@ public: * This Datatype must be resolved. */ Expr getConstructor(std::string name) const; + + /** get sygus type */ + Type getSygusType() const; /** * Get whether this datatype involves an external type. If so, |