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 | |
parent | 360ad23aa7f04d7059aff6314066e47e975fe5be (diff) |
Add get instantiations utilities to API.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 37 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 11 |
2 files changed, 48 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f288c6c0a..e3a0533af 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5125,6 +5125,43 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) } } +void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) { + SmtScope smts(this); + if( d_theoryEngine ){ + std::vector< Node > qs_n; + d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n ); + for( unsigned i=0; i<qs_n.size(); i++ ){ + qs.push_back( qs_n[i].toExpr() ); + } + } +} + +void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) { + SmtScope smts(this); + if( d_theoryEngine ){ + std::vector< Node > insts_n; + d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n ); + for( unsigned i=0; i<insts_n.size(); i++ ){ + insts.push_back( insts_n[i].toExpr() ); + } + } +} + +void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) { + SmtScope smts(this); + if( d_theoryEngine ){ + std::vector< std::vector< Node > > tvecs_n; + d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n ); + for( unsigned i=0; i<tvecs_n.size(); i++ ){ + std::vector< Expr > tvec; + for( unsigned j=0; j<tvecs_n[i].size(); j++ ){ + tvec.push_back( tvecs_n[i][j].toExpr() ); + } + tvecs.push_back( tvec ); + } + } +} + vector<Expr> SmtEngine::getAssertions() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); 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. |