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/smt/smt_engine.h | |
parent | 360ad23aa7f04d7059aff6314066e47e975fe5be (diff) |
Add get instantiations utilities to API.
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2741cea85..760c7c071 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -566,6 +566,17 @@ public: Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict=true) throw(TypeCheckingException, ModalException, LogicException); /** + * Get list of quantified formulas that were instantiated + */ + void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ); + + /** + * Get instantiations + */ + void getInstantiations( Expr q, std::vector< Expr >& insts ); + void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ); + + /** * Get an unsatisfiable core (only if immediately preceded by an * UNSAT or VALID query). Only permitted if CVC4 was built with * unsat-core support and produce-unsat-cores is on. |