diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_pbe.h')
-rw-r--r-- | src/theory/quantifiers/ce_guided_pbe.h | 273 |
1 files changed, 273 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h new file mode 100644 index 000000000..f40f29b2a --- /dev/null +++ b/src/theory/quantifiers/ce_guided_pbe.h @@ -0,0 +1,273 @@ +/********************* */ +/*! \file ce_guided_pbe.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief utility for processing programming by examples synthesis conjectures + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H +#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H + +#include "context/cdhashmap.h" +#include "context/cdchunk_list.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class CegConjecture; +class CegConjecturePbe; +class CegEntailmentInfer; + +class CegConjecturePbe { +private: + QuantifiersEngine* d_qe; + quantifiers::TermDbSygus * d_tds; + CegConjecture* d_parent; + + std::map< Node, bool > d_examples_invalid; + std::map< Node, bool > d_examples_out_invalid; + std::map< Node, std::vector< std::vector< Node > > > d_examples; + std::map< Node, std::vector< Node > > d_examples_out; + std::map< Node, std::vector< Node > > d_examples_term; + + void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol ); + bool d_is_pbe; +public: + Node d_true; + Node d_false; + enum { + enum_io, + enum_ite_condition, + enum_concat_term, + enum_any, + }; + enum { + strat_ITE, + strat_CONCAT, + strat_ID, + }; +public: + CegConjecturePbe( QuantifiersEngine * qe, CegConjecture * p ); + ~CegConjecturePbe(); + + void initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas ); + bool getPbeExamples( Node v, std::vector< std::vector< Node > >& exs, + std::vector< Node >& exos, std::vector< Node >& exts); + bool isPbe() { return d_is_pbe; } +private: // for registration + void collectEnumeratorTypes( Node c, TypeNode tn, unsigned enum_role ); + void registerEnumerator( Node et, Node c, TypeNode tn, unsigned enum_role, bool inSearch ); + void staticLearnRedundantOps( Node c, std::vector< Node >& lemmas ); + void staticLearnRedundantOps( Node c, Node e, std::map< Node, bool >& visited, std::vector< Node >& redundant, + std::vector< Node >& lemmas, int ind ); + + /** register candidate conditional */ + bool inferTemplate( unsigned k, Node n, std::map< Node, unsigned >& templ_var_index, std::map< unsigned, unsigned >& templ_injection ); + /** get guard status */ + int getGuardStatus( Node g ); +public: + class IndexFilter { + public: + IndexFilter(){} + void mk( std::vector< Node >& vals, bool pol = true ); + std::map< unsigned, unsigned > d_next; + unsigned start(); + unsigned next( unsigned i ); + void clear() { d_next.clear(); } + bool isEq( std::vector< Node >& vs, Node v ); + }; +private: + // subsumption trie + class SubsumeTrie { + private: + Node addTermInternal( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, bool spol, IndexFilter * f, + unsigned index, int status, bool checkExistsOnly, bool checkSubsume ); + public: + SubsumeTrie(){} + Node d_term; + std::map< Node, SubsumeTrie > d_children; + // adds term to the trie, removes based on subsumption + Node addTerm( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL ); + // adds condition to the trie (does not do subsumption) + Node addCond( CegConjecturePbe * pbe, Node c, std::vector< Node >& vals, bool pol, IndexFilter * f = NULL ); + // returns the set of terms that are subsets of vals + void getSubsumed( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL ); + // returns the set of terms that are supersets of vals + void getSubsumedBy( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed_by, IndexFilter * f = NULL ); + private: + void getLeavesInternal( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f, + unsigned index, int status ); + public: + // v[-1,1,0] -> children always false, always true, both + void getLeaves( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f = NULL ); + public: + bool isEmpty() { return d_term.isNull() && d_children.empty(); } + void clear() { + d_term = Node::null(); + d_children.clear(); + } + }; + + class EnumInfo { + private: + /** an OR of all in d_enum_res */ + //std::vector< Node > d_enum_total; + //bool d_enum_total_true; + Node d_enum_solved; + public: + EnumInfo() : d_role( enum_io ){} + Node d_parent_candidate; + + // for template + Node d_template; + Node d_template_arg; + + // TODO : make private + unsigned d_role; + + Node d_active_guard; + std::vector< Node > d_enum_slave; + /** values we have enumerated */ + std::vector< Node > d_enum_vals; + /** this either stores the values of f( I ) for inputs + or the value of f( I ) = O if d_role==enum_io + */ + std::vector< std::vector< Node > > d_enum_vals_res; + std::vector< Node > d_enum_subsume; + std::map< Node, unsigned > d_enum_val_to_index; + SubsumeTrie d_term_trie; + public: + bool isTemplated() { return !d_template.isNull(); } + void addEnumValue( CegConjecturePbe * pbe, Node v, std::vector< Node >& results ); + void setSolved( Node slv ); + bool isSolved() { return !d_enum_solved.isNull(); } + Node getSolved() { return d_enum_solved; } + }; + std::map< Node, EnumInfo > d_einfo; +private: + class CandidateInfo; + class EnumTypeInfoStrat { + public: + unsigned d_this; + /** conditional solutions */ + std::vector< TypeNode > d_csol_cts; + std::vector< Node > d_cenum; + }; + class EnumTypeInfo { + public: + EnumTypeInfo() : d_parent( NULL ){} + CandidateInfo * d_parent; + // role -> _ + std::map< unsigned, Node > d_enum; + TypeNode d_this_type; + // strategies for enum_io role + std::map< Node, EnumTypeInfoStrat > d_strat; + bool isSolved( CegConjecturePbe * pbe ); + }; + class CandidateInfo { + public: + CandidateInfo() : d_check_sol( false ), d_cond_count( 0 ){} + Node d_this_candidate; + TypeNode d_root; + std::map< TypeNode, EnumTypeInfo > d_tinfo; + std::vector< Node > d_esym_list; + // role -> sygus type -> enumerator + std::map< TypeNode, Node > d_search_enum; + bool d_check_sol; + unsigned d_cond_count; + Node d_solution; + void initialize( Node c ); + void initializeType( TypeNode tn ); + Node getRootEnumerator(); + bool isNonTrivial(); + }; + // candidate -> sygus type -> info + std::map< Node, CandidateInfo > d_cinfo; + + /** add enumerated value */ + void addEnumeratedValue( Node x, Node v, std::vector< Node >& lems ); + bool getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp ); + +private: + // filtering verion + /* + class FilterSubsumeTrie { + public: + SubsumeTrie d_trie; + IndexFilter d_filter; + Node addTerm( Node t, std::vector< bool >& vals, std::vector< Node >& subsumed, bool checkExistsOnly = false ){ + return d_trie.addTerm( t, vals, subsumed, &d_filter, d_filter.start(), checkExistsOnly ); + } + }; + */ + class UnifContext { + public: + UnifContext() : d_has_string_pos(0) {} + //IndexFilter d_filter; + // the value of the context conditional + std::vector< Node > d_vals; + // update the examples + bool updateContext( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol ); + // the position in the strings + std::vector< unsigned > d_str_pos; + // 0 : pos not modified, 1 : pos indicates suffix incremented, -1 : pos indicates prefix incremented + int d_has_string_pos; + // update the string examples + bool updateStringPosition( CegConjecturePbe * pbe, std::vector< unsigned >& pos ); + // is return value modified + bool isReturnValueModified(); + class UEnumInfo { + public: + UEnumInfo() : d_status(-1){} + int d_status; + // enum val -> polarity -> solved + std::map< Node, std::map< unsigned, Node > > d_look_ahead_sols; + }; + // enumerator -> info + std::map< Node, UEnumInfo > d_uinfo; + void initialize( CegConjecturePbe * pbe, Node c ); + void getCurrentStrings( CegConjecturePbe * pbe, std::vector< Node >& vals, std::vector< CVC4::String >& ex_vals ); + bool getStringIncrement( CegConjecturePbe * pbe, bool isPrefix, std::vector< CVC4::String >& ex_vals, + std::vector< Node >& vals, std::vector< unsigned >& inc, unsigned& tot ); + bool isStringSolved( CegConjecturePbe * pbe, std::vector< CVC4::String >& ex_vals, std::vector< Node >& vals ); + }; + /** construct solution */ + Node constructSolution( Node c ); + Node constructSolution( Node c, Node e, UnifContext& x, int ind ); + Node constructBestSolvedTerm( std::vector< Node >& solved, UnifContext& x ); + Node constructBestStringSolvedTerm( std::vector< Node >& solved, UnifContext& x ); + Node constructBestSolvedConditional( std::vector< Node >& solved, UnifContext& x ); + Node constructBestConditional( std::vector< Node >& conds, UnifContext& x ); + Node constructBestStringToConcat( std::vector< Node > strs, + std::map< Node, unsigned > total_inc, + std::map< Node, std::vector< unsigned > > incr, + UnifContext& x ); + void getStringIncrement( bool isPrefix, Node c, Node v, + std::map< Node, unsigned > total_inc, + std::map< Node, std::vector< unsigned > > incr ); +public: + void registerCandidates( std::vector< Node >& candidates ); + void getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ); + // lems and candidate values are outputs + bool constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values, + std::vector< Node >& candidates, std::vector< Node >& candidate_values, + std::vector< Node >& lems ); +}; + + +}/* namespace CVC4::theory::quantifiers */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ + +#endif |