1 /********************* */
2 /*! \file arith_static_learner.h
4 ** Original author: Tim King
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): Dejan Jovanovic
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
20 #ifndef __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
21 #define __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
24 #include "util/statistics_registry.h"
25 #include "theory/arith/arith_utilities.h"
26 #include "theory/substitutions.h"
28 #include "context/context.h"
29 #include "context/cdlist.h"
30 #include "context/cdtrail_hashmap.h"
37 class ArithStaticLearner
{
41 * Map from a node to it's minimum and maximum.
43 typedef context::CDTrailHashMap
<Node
, DeltaRational
, NodeHashFunction
> CDNodeToMinMaxMap
;
44 CDNodeToMinMaxMap d_minMap
;
45 CDNodeToMinMaxMap d_maxMap
;
48 ArithStaticLearner(context::Context
* userContext
);
49 void staticLearning(TNode n
, NodeBuilder
<>& learned
);
51 void addBound(TNode n
);
54 void process(TNode n
, NodeBuilder
<>& learned
, const TNodeSet
& defTrue
);
56 void iteMinMax(TNode n
, NodeBuilder
<>& learned
);
57 void iteConstant(TNode n
, NodeBuilder
<>& learned
);
59 /** These fields are designed to be accessible to ArithStaticLearner methods. */
62 IntStat d_iteMinMaxApplications
;
63 IntStat d_iteConstantApplications
;
69 Statistics d_statistics
;
71 };/* class ArithStaticLearner */
73 }/* CVC4::theory::arith namespace */
74 }/* CVC4::theory namespace */
77 #endif /* __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */