#ifndef CVC4__THEORY_ENGINE_H
#define CVC4__THEORY_ENGINE_H
-#include <deque>
#include <memory>
-#include <set>
-#include <unordered_map>
-#include <utility>
#include <vector>
#include "base/check.h"
-#include "context/cdhashset.h"
+#include "context/cdhashmap.h"
#include "expr/node.h"
-#include "options/options.h"
-#include "options/smt_options.h"
#include "options/theory_options.h"
-#include "prop/prop_engine.h"
#include "theory/atom_requests.h"
#include "theory/engine_output_channel.h"
#include "theory/interrupted.h"
#include "theory/rewriter.h"
#include "theory/sort_inference.h"
-#include "theory/term_registration_visitor.h"
#include "theory/theory.h"
#include "theory/theory_preprocessor.h"
#include "theory/trust_node.h"
#include "theory/uf/equality_engine.h"
#include "theory/valuation.h"
#include "util/hash.h"
-#include "util/resource_manager.h"
#include "util/statistics_registry.h"
#include "util/unsafe_interrupt_exception.h"
namespace CVC4 {
class ResourceManager;
+class OutputManager;
class TheoryEngineProofGenerator;
/**
class DecisionManager;
class RelevanceManager;
-namespace eq {
-class EqualityEngine;
-} // namespace eq
}/* CVC4::theory namespace */
+namespace prop {
+class PropEngine;
+}
+
/**
* This is essentially an abstraction for a collection of theories. A
* TheoryEngine provides services to a PropEngine, making various
/** The relevance manager */
std::unique_ptr<theory::RelevanceManager> d_relManager;
- /** Default visitor for pre-registration */
- PreRegisterVisitor d_preRegistrationVisitor;
-
/** are we in eager model building mode? (see setEagerModelBuilding). */
bool d_eager_model_building;
* @param p the properties of the lemma.
* @param atomsTo the theory that atoms of the lemma should be sent to
* @param from the theory that sent the lemma
- * @return a lemma status, containing the lemma and context information
- * about when it was sent.
*/
- theory::LemmaStatus lemma(theory::TrustNode node,
- theory::LemmaProperty p,
- theory::TheoryId atomsTo = theory::THEORY_LAST,
- theory::TheoryId from = theory::THEORY_LAST);
+ void lemma(theory::TrustNode node,
+ theory::LemmaProperty p,
+ theory::TheoryId atomsTo = theory::THEORY_LAST,
+ theory::TheoryId from = theory::THEORY_LAST);
/** Enusre that the given atoms are send to the given theory */
void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
*/
void setEagerModelBuilding() { d_eager_model_building = true; }
- /** get synth solutions
- *
- * This method returns true if there is a synthesis solution available. This
- * is the case if the last call to check satisfiability originated in a
- * check-synth call, and the synthesis solver successfully found a solution
- * for all active synthesis conjectures.
- *
- * This method adds entries to sol_map that map functions-to-synthesize with
- * their solutions, for all active conjectures. This should be called
- * immediately after the solver answers unsat for sygus input.
- *
- * For details on what is added to sol_map, see
- * SynthConjecture::getSynthSolutions.
- */
- bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
-
/**
* Get the theory associated to a given Node.
*
*/
Node getModelValue(TNode var);
- /**
- * Takes a literal and returns an equivalent literal that is guaranteed to be
- * a SAT literal. This rewrites and preprocesses n, which notice may involve
- * adding clauses to the SAT solver if preprocessing n involves introducing
- * new skolems.
- */
- Node ensureLiteral(TNode n);
- /**
- * This returns the theory-preprocessed form of term n. This rewrites and
- * preprocesses n, which notice may involve adding clauses to the SAT solver
- * if preprocessing n involves introducing new skolems.
- */
- Node getPreprocessedTerm(TNode n);
- /**
- * Print all instantiations made by the quantifiers module.
- */
- void printInstantiations( std::ostream& out );
-
- /**
- * Print solution for synthesis conjectures found by ce_guided_instantiation module
- */
- void printSynthSolution( std::ostream& out );
-
- /**
- * Get list of quantified formulas that were instantiated
- */
- void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
-
- /**
- * Get instantiation methods
- * the first given forall x.q[x] returns ( a, ..., z )
- * the second returns mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] )
- * , ... , forall x.qn[x] -> ( qn[a]...qn[z] )
- */
- void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
- void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
-
/**
* Forwards an entailment check according to the given theoryOfMode.
* See theory.h for documentation on entailmentCheck().
* This function is called from the smt engine's checkModel routine.
*/
void checkTheoryAssertionsWithModel(bool hardFailure);
- private:
- IntStat d_arithSubstitutionsAdded;
};/* class TheoryEngine */
}/* CVC4 namespace */