21 #ifndef _cvc3__include__theory_core_h_
22 #define _cvc3__include__theory_core_h_
225 bool atBottomScope =
false) = 0;
397 bool enumerate,
bool computeSize);
437 bool incomplete(std::vector<std::string>& reasons);
542 std::ostream&
operator<<(std::ostream& os,
const NotifyList& l);
CDO< bool > d_inconsistent
Inconsistent flag.
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
void setupTerm(const Expr &e, Theory *i, const Theorem &thm)
Setup additional terms within a theory-specific setup().
Theory * d_solver
The theory which has the solver (if any)
std::hash_map< Expr, Theorem > d_termTheorems
Map from active terms to theorems that introduced those terms.
const bool * d_simplifyInPlace
Command line flag whether to simplify in place.
EffortLevel
Effort level for processFactQueue.
CDList< Expr > d_terms
List of all active terms in the system (for quantifier instantiation)
Data structure of expressions in CVC3.
void assertFormula(const Theorem &e)
Process a newly derived formula.
void computeType(const Expr &e)
Compute and store the type of e.
ExprHashMap< Theorem > d_varAssignments
Mapping of intermediate variables to their values.
TheoremManager * getTM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
CoreProofRules * createProofRules(TheoremManager *tm)
Private method to get a new theorem producer.
unsigned d_timeBase
Time limit (0==unlimited, >0==total available cpu time in seconds).
Expr processCond(const Expr &e, int i)
An auxiliary recursive function to process COND expressions into ITE.
const CLFlags & getFlags() const
void enqueueFact(const Theorem &e)
Enqueue a new fact.
CoreProofRules * d_rules
Core proof rules.
ExprMap< Expr > & tccCache()
Access to tcc cache (needed by theory_bitvector)
void addToVarDB(const Expr &e)
Adds expression to var database.
const CDList< Expr > & getPredicates()
Get list of predicates.
TheoryCore(ContextManager *cm, ExprManager *em, TheoremManager *tm, Translator *tr, const CLFlags &flags, Statistics &statistics)
Constructor.
ostream & operator<<(ostream &os, const Expr &e)
const CLFlags & d_flags
Reference to command line flags.
void registerCoreSatAPI(CoreSatAPI *coreSatAPI)
Register a SatAPI for TheoryCore.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
void setupSubFormulas(const Expr &s, const Expr &e, const Theorem &thm)
Helper for registerAtom.
void setIncomplete(const std::string &reason)
Mark the branch as incomplete.
MS C++ specific settings.
TheoremManager * d_tm
Theorem manager.
ContextManager * d_cm
Context manager.
virtual void addLemma(const Theorem &thm, int priority=0, bool atBottomScope=false)=0
Add a new lemma derived by theory core.
CDList< Theorem > d_impliedLiterals
List of implied literals, based on registered atomic formulas of interest.
void initTimeLimit()
Initialize base time used for !setTimeLimit.
ExprMap< Expr > d_tccCache
Cache for tcc's.
void enqueueSE(const Theorem &thm)
Check if the current context is inconsistent.
Translator * getTranslator() const
std::vector< std::pair< std::string, Expr > > d_boundVarStack
Bound variable stack: a vector of pairs
Expr parseExpr(const Expr &e)
Parse the generic expression.
bool incomplete()
Check if the current decision branch is marked as incomplete.
virtual bool check(const Expr &e)=0
Check the validity of e in the current context.
Theorem simplifyOp(const Expr &e)
Recursive simplification step.
bool inconsistent()
Check if the current context is inconsistent.
Theorem rewriteLiteral(const Expr &e)
Called by search engine.
Description: Counters and flags for collecting run-time statistics.
unsigned getQuantLevelForTerm(const Expr &e)
Get quantification level at which this term was introduced.
Theorem callTheoryPreprocess(const Expr &e)
Call theory-specific preprocess routines.
bool inUpdate()
Whether updates are being processed.
CDMap< std::string, bool > d_incomplete
The set of reasons for incompleteness (empty when we are complete)
std::vector< Theory * > d_theories
Array of registered theories.
bool checkSATCore()
To be called by SearchEngine when it believes the context is satisfiable.
ExprTransform * d_exprTrans
Expr Transformer.
CoreProofRules * getCoreRules() const
std::map< std::string, Expr > d_globals
Database of declared identifiers.
Theorem getModelValue(const Expr &e)
Enqueue a fact to be sent to the SearchEngine.
std::hash_map< int, Theory * > d_theoryMap
Array mapping kinds to theories.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Theorem getImpliedLiteralByIndex(unsigned index)
Return an implied literal by index.
void setInPP()
Set the flag for the preprocessor.
void getResource()
Request a unit of resource.
std::vector< Theorem > d_update_thms
List of theorems from calls to update()
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
NotifyList d_notifyEq
Notify list that gets processed on every equality.
ExprHashMap< Theorem > d_simplifiedModelVars
Mapping of basic variables to simplified expressions (temp. storage)
void assignValue(const Expr &t, const Expr &val)
Assign t a concrete value val. Used in model generation.
Theorem simplify(const Expr &e)
Top-level simplifier.
virtual void addSplitter(const Expr &e, int priority)=0
Suggest a splitter to the Sat engine.
void refineCounterExample()
Calls for other theories to add facts to refine a coutnerexample.
ExprTransform * getExprTrans() const
ExprMap< Expr > * d_parseCache
Current cache being used for parser.
Abstract class for computing expr type.
Expr getAssignment()
Get the value of all :named terms.
Statistics & d_statistics
Reference to statistics.
const CDList< Expr > & getTerms()
Get list of terms.
StatCounter counter(const std::string &name)
CoreSatAPI * d_coreSatAPI
ExprManager::TypeComputer * d_typeComputer
Type Computer.
Theorem getImpliedLiteral(void)
Return the next implied literal (NULL Theorem if none)
void add(Theory *t, const Expr &e)
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
unsigned d_inUpdate
Whether we are in the middle of doing updates.
void collectModelValues(const Expr &e, ExprMap< Expr > &m)
Recursively build a compound-type variable assignment for e.
void assertFactCore(const Theorem &e)
The assumptions for e must be in H or phi. "Core" added to avoid conflict with theory interface funct...
CDO< Theorem > d_incThm
Proof of inconsistent.
Theorem rewriteCore(const Theorem &e)
Transitive composition of other rewrites with the above.
void collectBasicVars()
Split compound vars into basic type variables.
Interface class for callbacks to SAT from Core.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
void addSharedTerm(const Expr &e)
std::hash_map< std::string, Expr > d_boundVarMap
Map for bound vars.
void addNotifyEq(Theory *t, const Expr &e)
Register a callback for every equality.
std::vector< Expr > d_basicModelVars
List of basic variables (temporary storage for model generation)
ExprManager * getEM()
Access to ExprManager.
void checkEquation(const Theorem &thm)
Helper check functions for solve.
CDO< unsigned > d_impliedLiteralsIdx
Next index in d_impliedLiterals that has not yet been fetched.
Expr getValue(Expr e)
Get the value of an arbitrary formula or term.
void registerAtom(const Expr &e, const Theorem &thm)
Register an atomic formula of interest.
void checkType(const Expr &e)
Check that e is a valid Type expr.
void setInconsistent(const Theorem &e)
TheoryCore * d_theoryCore
bool processFactQueue(EffortLevel effort=NORMAL)
A helper function for addFact()
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
void setResourceLimit(unsigned limit)
Set the resource limit (0==unlimited).
ContextManager * getCM() const
Translator * d_translator
Translator.
void setup(const Expr &e)
ExprStream & printSmtLibShared(ExprStream &os, const Expr &e)
Generic API for Theories plus methods commonly used by theories.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
CoreNotifyObj d_notifyObj
void processUpdates()
Process updates recorded by calls to update()
Theorem getTheoremForTerm(const Expr &e)
Get theorem which was responsible for introducing this term.
ExprHashMap< std::vector< Expr > > d_varModelMap
Mapping of compound type variables to simpler types (model generation)
CoreNotifyObj(TheoryCore *tc, Context *context)
Theorem typePred(const Expr &e)
Return a theorem for the type predicate of e.
bool outOfResources()
Return true if resources are exhausted.
Theorem inconsistentThm()
Get the proof of inconsistency for the current context.
void assertEqualities(const Theorem &e)
Assert a system of equations (1 or more).
ExprMap< Expr > d_parseCacheTop
Top-level cache for parser.
std::vector< Theorem > d_queueSE
Queue of facts to be sent to the SearchEngine.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
CDList< Expr > d_predicates
List of all active non-equality atomic formulas in the system (for quantifier instantiation) ...
std::queue< Theorem > d_queue
Assertion queue.
unsigned d_resourceLimit
Resource limit (0==unlimited, 1==no more resources, >=2 - available).
Cardinality
Enum for cardinality of types.
void processNotify(const Theorem &e, NotifyList *L)
Process a notify list triggered as a result of new theorem e.
unsigned numImpliedLiterals()
Return total number of implied literals.
PrettyPrinter * d_printer
PrettyPrinter (we own it)
bool okToEnqueue()
Whether its OK to add new facts (for use in rewrites)
Manager for multiple contexts. Also holds current context.
Expr parseExprTop(const Expr &e)
Top-level call to parseExpr, clears the bound variable stack.
void setFindLiteral(const Theorem &thm)
Set the find pointer of an atomic formula and notify SearchEngine.
std::vector< Expr > d_vars
List of variables that were created up to this point.
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
void update(const Theorem &e, const Expr &d)
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Theorem solve(const Theorem &e)
std::vector< std::pair< Expr, Expr > > d_assignment
The set of named expressions to evaluate on a GET_ASSIGNMENT request.
ExprMap< Expr > d_parseCacheOther
Alternative cache for parser when not at top-level.
virtual Theorem addAssumption(const Expr &assump)=0
Add an assumption to the set of assumptions in the current context.
std::vector< Expr > d_update_data
List of data accompanying above theorems from calls to update()
Abstract API to a pretty-printer for Expr.
Statistics & getStatistics() const
bool isBasicKind(int kind)
Return true if no special parsing is required for this kind.
void buildModel(ExprMap< Expr > &m)
Calls theory specific computeModel, results are placed in map.
Theorem(TheoryCore::* d_currentRecursiveSimplifier)(const Expr &)
Which recursive simplifier to use.
Theorem rewriteLitCore(const Expr &e)
Core rewrites for literals (NOT and EQ)
unsigned getResourceLimit()
Get the resource limit.
void checkSolved(const Theorem &thm)
Helper check functions for solve.
void setTimeLimit(unsigned limit)
Set the time limit in seconds (0==unlimited).