From f3590092818d9eab9d961ea602093029ff472a85 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 10 Jul 2017 14:06:52 -0500 Subject: Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions. --- src/theory/quantifiers/term_database.h | 212 ++++++++++++++++++++++++++++++--- 1 file changed, 197 insertions(+), 15 deletions(-) (limited to 'src/theory/quantifiers/term_database.h') diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 912961e19..b1d4f7f2b 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -93,6 +93,14 @@ typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribu struct SygusProxyAttributeId {}; typedef expr::Attribute SygusProxyAttribute; +// attribute for associating a synthesis function with a first order variable +struct SygusSynthFunAttributeId {}; +typedef expr::Attribute SygusSynthFunAttribute; + +// attribute for associating a variable list with a synth fun +struct SygusSynthFunVarListAttributeId {}; +typedef expr::Attribute SygusSynthFunVarListAttribute; + //attribute for fun-def abstraction type struct AbsTypeFunDefAttributeId {}; typedef expr::Attribute AbsTypeFunDefAttribute; @@ -109,6 +117,11 @@ typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAtt struct QuantIdNumAttributeId {}; typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; +/** sygus var num */ +struct SygusVarNumAttributeId {}; +typedef expr::Attribute SygusVarNumAttribute; + + class QuantifiersEngine; @@ -495,6 +508,8 @@ public: static bool isAssoc( Kind k ); /** is comm */ static bool isComm( Kind k ); + /** ( x k ... ) k x = ( x k ... ) */ + static bool isNonAdditive( Kind k ); /** is bool connective */ static bool isBoolConnective( Kind k ); /** is bool connective term */ @@ -559,20 +574,50 @@ public: static void computeQuantAttributes( Node q, QAttributes& qa ); };/* class TermDb */ +class SygusInvarianceTest { +protected: + // check whether nvn[ x ] should be excluded + virtual bool invariant( TermDbSygus * tds, Node nvn, Node x ) = 0; +public: + bool is_invariant( TermDbSygus * tds, Node nvn, Node x ){ + if( invariant( tds, nvn, x ) ){ + d_update_nvn = nvn; + return true; + }else{ + return false; + } + } + // result of the node after invariant replacements + Node d_update_nvn; +}; + +class EvalSygusInvarianceTest : public SygusInvarianceTest { +public: + Node d_conj; + TNode d_var; + std::map< Node, Node > d_visited; + Node d_result; +protected: + bool invariant( quantifiers::TermDbSygus * tds, Node nvn, Node x ); +}; + class TermDbSygus { private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; - std::map< TypeNode, std::vector< Node > > d_fv; + std::map< TypeNode, std::vector< Node > > d_fv[2]; std::map< Node, TypeNode > d_fv_stype; std::map< Node, int > d_fv_num; + bool hasFreeVar( Node n, std::map< Node, bool >& visited ); +public: Node d_true; Node d_false; public: - TNode getVar( TypeNode tn, int i ); - TNode getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ); - bool isVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); } + TNode getFreeVar( TypeNode tn, int i, bool useSygusType = false ); + TNode getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_count, bool useSygusType = false ); + bool isFreeVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); } int getVarNum( Node n ) { return d_fv_num[n]; } + bool hasFreeVar( Node n ); private: std::map< TypeNode, std::map< int, Node > > d_generic_base; std::map< TypeNode, std::vector< Node > > d_generic_templ; @@ -581,8 +626,15 @@ private: public: bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 ); private: + void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ); + bool involvesDivByZero( Node n, std::map< Node, bool >& visited ); +private: + // stores root + std::map< Node, Node > d_measured_term; + std::map< Node, Node > d_measured_term_active_guard; //information for sygus types std::map< TypeNode, TypeNode > d_register; //stores sygus -> builtin type + std::map< TypeNode, std::vector< Node > > d_var_list; std::map< TypeNode, std::map< int, Kind > > d_arg_kind; std::map< TypeNode, std::map< Kind, int > > d_kinds; std::map< TypeNode, std::map< int, Node > > d_arg_const; @@ -592,6 +644,7 @@ private: std::map< TypeNode, std::vector< int > > d_id_funcs; std::map< TypeNode, std::vector< Node > > d_const_list; //sorted list of constants for type std::map< TypeNode, unsigned > d_const_list_pos; + std::map< TypeNode, std::map< Node, Node > > d_semantic_skolem; //information for builtin types std::map< TypeNode, std::map< int, Node > > d_type_value; std::map< TypeNode, Node > d_type_max_value; @@ -601,36 +654,63 @@ private: std::map< TypeNode, std::map< Node, Node > > d_normalized; std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin; std::map< TypeNode, std::map< Node, Node > > d_builtin_const_to_sygus; + // grammar information + // root -> type -> _ + std::map< TypeNode, std::map< TypeNode, unsigned > > d_min_type_depth; + //std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > > d_consider_const; + // type -> cons -> _ + std::map< TypeNode, unsigned > d_min_term_size; + std::map< TypeNode, std::map< unsigned, unsigned > > d_min_cons_term_size; public: TermDbSygus( context::Context* c, QuantifiersEngine* qe ); ~TermDbSygus(){} bool reset( Theory::Effort e ); std::string identify() const { return "TermDbSygus"; } - +public: + /** register the sygus type */ + void registerSygusType( TypeNode tn ); + /** register a term that we will do enumerative search on */ + void registerMeasuredTerm( Node e, Node root, bool mkActiveGuard = false ); + /** is measured term */ + Node isMeasuredTerm( Node e ); + /** get active guard */ + Node getActiveGuardForMeasureTerm( Node e ); + /** get measured terms */ + void getMeasuredTerms( std::vector< Node >& mts ); +public: //general sygus utilities bool isRegistered( TypeNode tn ); + // get the minimum depth of type in its parent grammar + unsigned getMinTypeDepth( TypeNode root_tn, TypeNode tn ); + // get the minimum size for a constructor term + unsigned getMinTermSize( TypeNode tn ); + unsigned getMinConsTermSize( TypeNode tn, unsigned cindex ); +public: TypeNode sygusToBuiltinType( TypeNode tn ); - int getKindArg( TypeNode tn, Kind k ); - int getConstArg( TypeNode tn, Node n ); - int getOpArg( TypeNode tn, Node n ); + int getKindConsNum( TypeNode tn, Kind k ); + int getConstConsNum( TypeNode tn, Node n ); + int getOpConsNum( TypeNode tn, Node n ); bool hasKind( TypeNode tn, Kind k ); bool hasConst( TypeNode tn, Node n ); bool hasOp( TypeNode tn, Node n ); - Node getArgConst( TypeNode tn, int i ); - Node getArgOp( TypeNode tn, int i ); - Kind getArgKind( TypeNode tn, int i ); + Node getConsNumConst( TypeNode tn, int i ); + Node getConsNumOp( TypeNode tn, int i ); + Kind getConsNumKind( TypeNode tn, int i ); bool isKindArg( TypeNode tn, int i ); bool isConstArg( TypeNode tn, int i ); unsigned getNumIdFuncs( TypeNode tn ); unsigned getIdFuncIndex( TypeNode tn, unsigned i ); - void registerSygusType( TypeNode tn ); /** get arg type */ TypeNode getArgType( const DatatypeConstructor& c, int i ); + /** get first occurrence */ + int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn ); + /** is type match */ + bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ); /** 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 ); + Node isSingularArg( Node n, Kind ik, int arg ); /** get offset arg */ bool hasOffsetArg( Kind ik, int arg, int& offset, Kind& ok ); /** get value */ @@ -643,10 +723,14 @@ public: Node getGenericBase( TypeNode tn, const Datatype& dt, int c ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); Node sygusToBuiltin( Node n, TypeNode tn ); + Node sygusToBuiltin( Node n ) { return sygusToBuiltin( n, n.getType() ); } + Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args ); Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 ); Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true ); - int getSygusTermSize( Node n ); + unsigned getSygusTermSize( Node n ); + // returns size + unsigned getSygusConstructors( Node n, std::vector< Node >& cons ); /** given a term, construct an equivalent smaller one that respects syntax */ Node minimizeBuiltinTerm( Node n ); /** given a term, expand it into more basic components */ @@ -655,19 +739,36 @@ public: Kind getComparisonKind( TypeNode tn ); Kind getPlusKind( TypeNode tn, bool is_neg = false ); bool doCompare( Node a, Node b, Kind k ); + // get semantic skolem for n (a sygus term whose builtin version is n) + Node getSemanticSkolem( TypeNode tn, Node n, bool doMk = true ); + /** involves div-by-zero */ + bool involvesDivByZero( Node n ); + /** get operator kind */ static Kind getOperatorKind( Node op ); /** print sygus term */ static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ); - + /** get anchor */ static Node getAnchor( Node n ); + static unsigned getAnchorDepth( Node n ); + +public: // for symmetry breaking + bool considerArgKind( TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg ); + bool considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg ); + bool considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg ); + int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg ); + //for eager instantiation private: std::map< Node, std::map< Node, bool > > d_subterms; std::map< Node, std::vector< Node > > d_evals; std::map< Node, std::vector< std::vector< Node > > > d_eval_args; + std::map< Node, std::vector< bool > > d_eval_args_const; std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc; + + void getExplanationFor( TermRecBuild& trb, Node n, Node vn, std::vector< Node >& exp, std::map< TypeNode, int >& var_count, + SygusInvarianceTest& et, Node vnr, Node& vnr_exp, int& sz ); public: void registerEvalTerm( Node n ); void registerModelValue( Node n, Node v, std::vector< Node >& exps, std::vector< Node >& terms, std::vector< Node >& vals ); @@ -677,6 +778,87 @@ public: std::vector< Node > exp; return unfold( en, vtm, exp, false ); } + Node getEagerUnfold( Node n, std::map< Node, Node >& visited ); + // returns straightforward exp => n = vn + void getExplanationForConstantEquality( Node n, Node vn, std::vector< Node >& exp ); + void getExplanationForConstantEquality( Node n, Node vn, std::vector< Node >& exp, std::map< unsigned, bool >& cexc ); + Node getExplanationForConstantEquality( Node n, Node vn ); + Node getExplanationForConstantEquality( Node n, Node vn, std::map< unsigned, bool >& cexc ); + // we have n = vn => eval( n ) = bvr, returns exp => eval( n ) = bvr + // ensures the explanation still allows for vnr + void getExplanationFor( Node n, Node vn, std::vector< Node >& exp, SygusInvarianceTest& et, Node vnr, unsigned& sz ); + void getExplanationFor( Node n, Node vn, std::vector< Node >& exp, SygusInvarianceTest& et ); + // builtin evaluation, returns rewrite( bn [ args / vars(tn) ] ) + Node evaluateBuiltin( TypeNode tn, Node bn, std::vector< Node >& args ); + Node evaluateBuiltin( TypeNode tn, Node bn, Node ar, unsigned i ); + // evaluate with unfolding + Node evaluateWithUnfolding( Node n, std::map< Node, Node >& visited ); + Node evaluateWithUnfolding( Node n ); +//for calculating redundant operators +private: + //whether each constructor is redundant + // 0 : not redundant, 1 : redundant, 2 : partially redundant + std::map< TypeNode, std::vector< int > > d_sygus_red_status; + // type to (rewritten) to original + std::map< TypeNode, std::map< Node, Node > > d_gen_terms; + std::map< TypeNode, std::map< Node, bool > > d_gen_redundant; + //compute generic redundant + bool computeGenericRedundant( TypeNode tn, Node g ); +public: + bool isGenericRedundant( TypeNode tn, unsigned i ); + +//sygus pbe +private: + std::map< Node, std::vector< std::vector< Node > > > d_pbe_exs; + std::map< Node, std::vector< Node > > d_pbe_exos; + std::map< Node, unsigned > d_pbe_term_id; +private: + class PbeTrie { + private: + Node addPbeExampleEval( TypeNode etn, Node e, Node b, std::vector< Node >& ex, quantifiers::TermDbSygus * tds, unsigned index, unsigned ntotal ); + public: + PbeTrie(){} + ~PbeTrie(){} + Node d_lazy_child; + std::map< Node, PbeTrie > d_children; + void clear() { d_children.clear(); } + Node addPbeExample( TypeNode etn, Node e, Node b, TermDbSygus * tds, unsigned index, unsigned ntotal ); + }; + std::map< Node, std::map< TypeNode, PbeTrie > > d_pbe_trie; +public: + /** register examples for an enumerative search term. + This should be a comprehensive set of examples. */ + void registerPbeExamples( Node e, std::vector< std::vector< Node > >& exs, + std::vector< Node >& exos, std::vector< Node >& exts ); + /** get examples */ + bool hasPbeExamples( Node e ); + unsigned getNumPbeExamples( Node e ); + /** return value is the required value for the example */ + void getPbeExample( Node e, unsigned i, std::vector< Node >& ex ); + Node getPbeExampleOut( Node e, unsigned i ); + int getPbeExampleId( Node n ); + /** add the search val, returns an equivalent value (possibly the same) */ + Node addPbeSearchVal( TypeNode tn, Node e, Node bvr ); + +// extended rewriting +private: + std::map< Node, Node > d_ext_rewrite_cache; + Node extendedRewritePullIte( Node n ); +public: + Node extendedRewrite( Node n ); + +// for default grammar construction +private: + TypeNode mkUnresolvedType(const std::string& name, std::set& unres); + void mkSygusConstantsForType( TypeNode type, std::vector& ops ); + void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); + void mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, std::vector< CVC4::Datatype >& datatypes, std::set& unres ); +public: + TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons ); + TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun ){ + std::map< TypeNode, std::vector< Node > > extra_cons; + return mkSygusDefaultType( range, bvl, fun, extra_cons ); + } }; }/* CVC4::theory::quantifiers namespace */ -- cgit v1.2.3