From cc01e2119801bbd4fd99548b79c297fa57a1977d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 9 May 2014 06:51:43 -0500 Subject: Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs. --- src/smt/options | 2 ++ src/smt/smt_engine.cpp | 4 ++++ src/smt/smt_engine.h | 5 +++++ 3 files changed, 11 insertions(+) (limited to 'src/smt') diff --git a/src/smt/options b/src/smt/options index f3429287f..7b749fc6c 100644 --- a/src/smt/options +++ b/src/smt/options @@ -35,6 +35,8 @@ option checkProofs check-proofs --check-proofs bool :link --proof :link-smt prod after UNSAT/VALID, machine-check the generated proof option dumpProofs --dump-proofs bool :default false :link --proof output proofs after every UNSAT/VALID response +option dumpInstantiations --dump-instantiations bool :default false + output instantiations of quantified formulas after every UNSAT/VALID response # this is just a placeholder for later; it doesn't show up in command-line options listings undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation (NOT YET SUPPORTED) 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 SmtEngine::getAssertions() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2991ab21b..88ba55b45 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -497,6 +497,11 @@ public: */ Proof* getProof() throw(ModalException); + /** + * Print all instantiations made by the quantifiers module. + */ + void printInstantiations(); + /** * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. -- cgit v1.2.3