diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-28 17:14:04 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-28 17:14:04 -0500 |
commit | b1dea08db5a965d8d9d6f38bd05c280a8a126352 (patch) | |
tree | 5bd385da8faf2043da66ae1ff2230ca759c36a49 /src/theory/theory_engine.h | |
parent | 360ad23aa7f04d7059aff6314066e47e975fe5be (diff) |
Add get instantiations utilities to API.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4366f8d3a..fc98c6e3a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -786,9 +786,20 @@ public: void printSynthSolution( std::ostream& out ); /** - * Get instantiations + * Get list of quantified formulas that were instantiated */ + void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ); + + /** + * Get instantiation methods + * first inputs forall x.q[x] and returns ( q[a], ..., q[z] ) + * second inputs forall x.q[x] and returns ( a, ..., z ) + * third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) , ... , forall x.qn[x] -> ( qn[a]...qn[z] ) + */ + void getInstantiations( Node q, std::vector< Node >& insts ); + void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ); void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ); /** * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q. |