diff options
author | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
commit | 2ba8bb701ce289ba60afec01b653b0930cc59298 (patch) | |
tree | 46df365b7b41ce662a0f94de5b11c3ed20829851 /src/proof/theory_proof.h | |
parent | 42b665f2a00643c81b42932fab1441987628c5a5 (diff) |
Adding listeners to Options.
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.
- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.
- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.
- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.
- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.
- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.
- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 86 |
1 files changed, 43 insertions, 43 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 3d700c388..d997d6e23 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -30,8 +30,6 @@ namespace CVC4 { -class SmtGlobals; - namespace theory { class Theory; } @@ -89,7 +87,7 @@ typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap; typedef std::vector<LetOrderElement> Bindings; -class TheoryProof; +class TheoryProof; typedef unsigned ClauseId; typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; @@ -99,67 +97,69 @@ class TheoryProofEngine { protected: ExprSet d_registrationCache; TheoryProofTable d_theoryProofTable; - + /** * Returns whether the theory is currently supported in proof * production mode. */ bool supportedTheory(theory::TheoryId id); public: - SmtGlobals* d_globals; - - TheoryProofEngine(SmtGlobals* globals); + + TheoryProofEngine(); virtual ~TheoryProofEngine(); - /** - * Print the theory term (could be atom) by delegating to the - * proper theory - * - * @param term - * @param os - * - * @return + + /** + * Print the theory term (could be an atom) by delegating to the proper theory. + * + * @param term + * @param os */ virtual void printLetTerm(Expr term, std::ostream& os) = 0; - virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map) = 0; - /** + virtual void printBoundTerm(Expr term, std::ostream& os, + const LetMap& map) = 0; + + /** * Print the proof representation of the given sort. - * - * @param os + * + * @param os */ - virtual void printSort(Type type, std::ostream& os) = 0; - /** + virtual void printSort(Type type, std::ostream& os) = 0; + + /** * Print the theory assertions (arbitrary formulas over * theory atoms) - * - * @param os + * + * @param os * @param paren closing parenthesis */ virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; - /** + + /** * Print proofs of all the theory lemmas (must prove * actual clause used in resolution proof). - * - * @param os - * @param paren + * + * @param os + * @param paren */ - virtual void printTheoryLemmas(const IdToSatClause& lemmas, - std::ostream& os, + virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) = 0; - /** - * Register theory atom (ensures all terms and atoms are declared). - * - * @param atom + + /** + * Register theory atom (ensures all terms and atoms are declared). + * + * @param atom */ void registerTerm(Expr atom); - /** - * Ensures that a theory proof class for the given theory - * is created. - * - * @param theory + + /** + * Ensures that a theory proof class for the given theory is created. + * + * @param theory */ void registerTheory(theory::Theory* theory); + theory::TheoryId getTheoryForLemma(ClauseId id); - TheoryProof* getTheoryProof(theory::TheoryId id); + TheoryProof* getTheoryProof(theory::TheoryId id); }; class LFSCTheoryProofEngine : public TheoryProofEngine { @@ -167,9 +167,9 @@ class LFSCTheoryProofEngine : public TheoryProofEngine { void printTheoryTerm(Expr term, std::ostream& os, const LetMap& map); void bind(Expr term, LetMap& map, Bindings& let_order); public: - LFSCTheoryProofEngine(SmtGlobals* globals) - : TheoryProofEngine(globals) {} - + LFSCTheoryProofEngine() + : TheoryProofEngine() {} + void printDeclarations(std::ostream& os, std::ostream& paren); virtual void printCoreTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printLetTerm(Expr term, std::ostream& os); @@ -178,7 +178,7 @@ public: virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren); - virtual void printSort(Type type, std::ostream& os); + virtual void printSort(Type type, std::ostream& os); }; class TheoryProof { |