diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-05 14:50:09 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-05 14:50:09 +0100 |
commit | 45b0ba984fde882d3cd762076de0f9ddce2485c7 (patch) | |
tree | 4a45d1ce4eb8d3230ee55136e6146be2ba6280a2 /src/theory/quantifiers/term_database.h | |
parent | 7b72e4d1914ce92b8d3ef108756a94349f6510d2 (diff) |
Working version of sygus solution reconstruction from single inv cegqi. Heuristics to fit syntax.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r-- | src/theory/quantifiers/term_database.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 0f730929c..5a3419cee 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -368,10 +368,14 @@ class TermDbSygus { private: std::map< TypeNode, std::vector< Node > > d_fv; std::map< Node, TypeNode > d_fv_stype; + std::map< Node, int > d_fv_num; 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(); } + int getVarNum( Node n ) { return d_fv_num[n]; } + bool getMatch( Node p, Node n, std::map< int, Node >& s ); + bool getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s ); private: //information for sygus types std::map< TypeNode, TypeNode > d_register; //stores sygus type @@ -389,6 +393,8 @@ private: //normalized map 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; + std::map< TypeNode, std::map< int, Node > > d_generic_base; public: TermDbSygus(){} bool isRegistered( TypeNode tn ); @@ -426,7 +432,9 @@ public: Node getTypeMaxValue( TypeNode tn ); TypeNode getSygusType( Node v ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); + Node getGenericBase( TypeNode tn, int c ); Node sygusToBuiltin( Node n, TypeNode tn ); + Node builtinToSygusConst( Node c, TypeNode tn ); 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 getTermSize( Node n ); |