CVC3  2.4.1
decision_engine_caching.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file decision_engine_caching.h
4  *
5  * <hr>
6  *
7  * License to use, copy, modify, sell and/or distribute this software
8  * and its documentation for any purpose is hereby granted without
9  * royalty, subject to the terms and conditions defined in the \ref
10  * LICENSE file provided with this distribution.
11  *
12  * <hr>
13  *
14  */
15 /*****************************************************************************/
16 
17 #ifndef _cvc3__search__decision_engine_caching_h_
18 #define _cvc3__search__decision_engine_caching_h_
19 
20 #include "decision_engine.h"
21 
22 namespace CVC3 {
23 
25 
26  class CacheEntry
27  {
28  public:
30  int d_rank;
31  int d_trust;
32 
33  CacheEntry() : d_rank(0), d_trust(0) {}
34  };
35 
40  int d_height;
41 
42  std::vector<CacheEntry> d_cache;
44 
45 protected:
46  virtual bool isBetter(const Expr& e1, const Expr& e2);
47 
48 public:
50  virtual ~DecisionEngineCaching() { }
51 
52  virtual Expr findSplitter(const Expr& e);
53  virtual void goalSatisfied();
54 };
55 
56 }
57 
58 #endif
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
std::vector< CacheEntry > d_cache
virtual Expr findSplitter(const Expr &e)
Finds a splitter inside a non const expression. The expression passed in must not be a boolean consta...
virtual void goalSatisfied()
Search should call this when it derives 'false'.
virtual bool isBetter(const Expr &e1, const Expr &e2)
DecisionEngineCaching(TheoryCore *core, SearchImplBase *se)
API to to a generic proof search engine (a.k.a. SAT solver)
Definition: expr.cpp:35