summaryrefslogtreecommitdiff
path: root/src/theory/rewriterules/theory_rewriterules.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rewriterules/theory_rewriterules.h')
-rw-r--r--src/theory/rewriterules/theory_rewriterules.h226
1 files changed, 0 insertions, 226 deletions
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index 2cefe7f07..85cd9a85c 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -25,173 +25,17 @@
#include "theory/theory_engine.h"
#include "theory/quantifiers_engine.h"
#include "context/context_mm.h"
-#include "theory/rewriterules/rr_inst_match_impl.h"
-#include "theory/rewriterules/rr_trigger.h"
-#include "theory/rewriterules/rr_inst_match.h"
#include "util/statistics_registry.h"
-#include "theory/rewriterules/theory_rewriterules_preprocess.h"
namespace CVC4 {
namespace theory {
namespace rewriterules {
-using namespace CVC4::theory::rrinst;
-typedef CVC4::theory::rrinst::Trigger Trigger;
-
-typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache;
-
- enum Answer {ATRUE, AFALSE, ADONTKNOW};
-
- class TheoryRewriteRules; /** forward */
-
- class RewriteRule{
- public:
- // constant
- const size_t id; //for debugging
- const bool d_split;
- mutable Trigger trigger;
- std::vector<Node> guards;
- mutable std::vector<Node> to_remove; /** terms to remove */
- const Node body;
- const TNode new_terms; /** new terms included in the body */
- std::vector<Node> free_vars; /* free variable in the rule */
- std::vector<Node> inst_vars; /* corresponding vars in the triggers */
- /* After instantiating the body new match can appear (TNode
- because is a subterm of a body on the assicaited rewrite
- rule) */
- typedef context::CDList< std::pair<TNode,RewriteRule* > > BodyMatch;
- mutable BodyMatch body_match;
- mutable ApplyMatcher * trigger_for_body_match; // used because we can be matching
- // trigger when we need new match.
- // So currently we use another
- // trigger for that.
-
- //context dependent
- typedef InstMatchTrie2<true> CacheNode;
- mutable CacheNode d_cache;
-
- const bool directrr;
-
- RewriteRule(TheoryRewriteRules & re,
- Trigger & tr, ApplyMatcher * tr2,
- std::vector<Node> & g, Node b, TNode nt,
- std::vector<Node> & fv,std::vector<Node> & iv,
- std::vector<Node> & to_r, bool drr);
- RewriteRule(const RewriteRule & r) CVC4_UNUSED;
- RewriteRule& operator=(const RewriteRule &) CVC4_UNUSED;
- ~RewriteRule();
-
- bool noGuard()const throw () { return guards.size() == 0; };
- bool inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const;
-
- void toStream(std::ostream& out) const;
-
- /* statistics */
- mutable size_t nb_matched;
- mutable size_t nb_applied;
- mutable size_t nb_propagated;
-
- };
-
- class RuleInst{
- public:
- /** The rule has at least one guard */
- const RewriteRule* rule;
-
- /** the substitution */
- std::vector<Node> subst;
-
- /** the term matched (not null if mono-pattern and direct-rr) */
- Node d_matched;
-
- /** Rule an instantiation with the given match */
- RuleInst(TheoryRewriteRules & re, const RewriteRule* r,
- std::vector<Node> & inst_subst,
- Node matched);
- RuleInst():rule(NULL){} // Dumb
-
- Node substNode(const TheoryRewriteRules & re, TNode r, TCache cache) const;
- size_t findGuard(TheoryRewriteRules & re, size_t start)const;
-
- void toStream(std::ostream& out) const;
-
- bool alreadyRewritten(TheoryRewriteRules & re) const;
- };
-
-/** A pair? */
- class Guarded {
- public:
- /** The backtracking is done somewhere else */
- const size_t d_guard; /* the id of the guard */
-
- /** The shared instantiation data */
- const RuleInst* inst;
-
- void nextGuard(TheoryRewriteRules & re)const;
-
- /** start indicate the first guard which is not true */
- Guarded(const RuleInst* ri, const size_t start);
- Guarded(const Guarded & g);
- /** Should be ssigned by a good garded after */
- Guarded();
-
- ~Guarded(){};
- void destroy(){};
- };
-
-template<class T>
-class CleanUpPointer{
-public:
- inline void operator()(T** e){
- delete(*e);
- };
-};
class TheoryRewriteRules : public Theory {
private:
KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::rewriterules::theoryTime");
-
- /** list of all rewrite rules */
- /* std::vector< Node > d_rules; */
- // typedef std::vector< std::pair<Node, Trigger > > Rules;
- typedef context::CDList< RewriteRule *,
- CleanUpPointer<RewriteRule >,
- std::allocator< RewriteRule * > > Rules;
- Rules d_rules;
- typedef context::CDList< RuleInst *,
- CleanUpPointer<RuleInst>,
- std::allocator< RuleInst * > > RuleInsts;
- RuleInsts d_ruleinsts;
-
- /** The GList* will lead too memory leaks since that doesn't use
- CDChunckList */
- typedef context::CDList< Guarded > GList;
- typedef context::CDHashMap<Node, GList *, NodeHashFunction> GuardedMap;
- GuardedMap d_guardeds;
-
- /* In order to not monopolize, the system slow down himself: If a
- guard stored in d_guardeds become true or false, it waits
- checkSlowdown(=10) checks before checking again if some guard take a
- value. At FULL_EFFORT regardless of d_checkLevel it check the
- guards
- */
- context::CDO<size_t> d_checkLevel;
-
- /** explanation */
- typedef context::CDHashMap<Node, RuleInst , NodeHashFunction> ExplanationMap;
- ExplanationMap d_explanations;
-
- /** new instantiation must be cleared at each conflict used only
- inside check */
- typedef std::vector< RuleInst* > QRuleInsts;
- QRuleInsts d_ruleinsts_to_add;
- bool d_ppAssert_on; //Indicate if a ppAssert have been done
-
public:
- /** true and false for predicate */
- Node d_true;
- Node d_false;
-
/** Constructs a new instance of TheoryRewriteRules
w.r.t. the provided context.*/
TheoryRewriteRules(context::Context* c,
@@ -209,76 +53,6 @@ private:
return "THEORY_REWRITERULES";
}
- Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-
- bool ppDontRewriteSubterm(TNode atom) { return true; }
-
-
- private:
- void registerQuantifier( Node n );
-
- public:
- /* TODO modify when notification will be available */
- void notification( Node n, bool b);
-
- Trigger createTrigger( TNode n, std::vector<Node> & pattern );
-
- /** return if the guard (already substituted) is known true or false
- or unknown. In the last case it add the Guarded(rid,gid) to the watch
- list of this guard */
- Answer addWatchIfDontKnow(Node g, const RuleInst* r, const size_t gid);
-
- /** An instantiation of a rule is fired (all guards true) we
- propagate the body. That can be done by theory propagation if
- possible or by lemmas.
- */
- void propagateRule(const RuleInst * r, TCache cache);
-
- /** Auxiliary functions */
-private:
- /** A guard is verify, notify the Guarded */
- void notification(GList * const lpropa, bool b);
- /* If two guards becomes equals we should notify if one of them is
- already true */
- bool notifyIfKnown(const GList * const ltested, GList * const lpropa);
-
- void substGuards(const RuleInst * inst,
- TCache cache,
- NodeBuilder<> & conjunction);
-
- void addRewriteRule(const Node r);
- void computeMatchBody ( const RewriteRule * r, size_t start = 0);
- void addMatchRuleTrigger(const RewriteRule* r,
- rrinst::InstMatch & im, bool delay = true);
-
- Node normalizeConjunction(NodeBuilder<> & conjunction);
-
- /* rewrite pattern */
- typedef std::hash_map< Node, rewriter::RRPpRewrite*, NodeHashFunction > RegisterRRPpRewrite;
- RegisterRRPpRewrite d_registeredRRPpRewrite;
-
- bool addRewritePattern(TNode pattern, TNode body,
- rewriter::Subst & pvars,
- rewriter::Subst & vars);
-
- //create inst variable
- std::vector<Node> createInstVariable( Node r, std::vector<Node> & vars );
-
- /** statistics class */
- class Statistics {
- public:
- IntStat d_num_rewriterules;
- IntStat d_check;
- IntStat d_full_check;
- IntStat d_poll;
- IntStat d_match_found;
- IntStat d_cache_hit;
- IntStat d_cache_miss;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
-
};/* class TheoryRewriteRules */
}/* CVC4::theory::rewriterules namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback