diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 15:25:16 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 15:25:16 +0100 |
| commit | 42f269065fbb9204627a2ce483b27d3bc6fd91f4 (patch) | |
| tree | 4e15f3844e8303c9f3bbdbc06c9673c27b39d870 /src/theory/quantifiers/term_database.h | |
| parent | 97e30c1089e42b668a914472b986f2d986190fc6 (diff) | |
Work on solution reconstruction for single inv. Fix compiler error found by Tim regarding Trace.isOn
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index ce3a52d1c..0f730929c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -388,6 +388,7 @@ private: std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status; //normalized map std::map< TypeNode, std::map< Node, Node > > d_normalized; + std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin; public: TermDbSygus(){} bool isRegistered( TypeNode tn ); @@ -425,8 +426,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 sygusToBuiltin( Node n, 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 ); + Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true ); int getTermSize( Node n ); }; |