diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
| commit | cc01e2119801bbd4fd99548b79c297fa57a1977d (patch) | |
| tree | cf9c64efbc286089a898d93abb3150e79138e5a7 /src/smt/smt_engine.cpp | |
| parent | 88907b94e858b701e83bbee67f542ad0ee5ae626 (diff) | |
Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a411530e6..1397c10d3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3789,6 +3789,10 @@ Proof* SmtEngine::getProof() throw(ModalException) { #endif /* CVC4_PROOF */ } +void SmtEngine::printInstantiations() { + //TODO +} + vector<Expr> SmtEngine::getAssertions() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); |