namespace arith {
-ArithStaticLearner::ArithStaticLearner(SubstitutionMap& pbSubstitutions) :
- d_miplibTrick(),
- d_miplibTrickKeys(),
- d_pbSubstitutions(pbSubstitutions),
+ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
+ d_miplibTrick(userContext),
+ d_minMap(userContext),
+ d_maxMap(userContext),
d_statistics()
{}
}
-void ArithStaticLearner::clear(){
- d_miplibTrick.clear();
- d_miplibTrickKeys.clear();
- // do not clear d_pbSubstitutions, as it is shared
-}
+
void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){
if(rewriteEqTo.getKind() == CONST_RATIONAL){
TNode var = n[1][0];
- if(d_miplibTrick.find(var) == d_miplibTrick.end()){
- d_miplibTrick.insert(make_pair(var, set<Node>()));
- d_miplibTrickKeys.push_back(var);
- }
- d_miplibTrick[var].insert(n);
+ Node current = (d_miplibTrick.find(var) == d_miplibTrick.end()) ?
+ mkBoolNode(false) : d_miplibTrick[var];
+ d_miplibTrick.insert(var, n.orNode(current));
Debug("arith::miplib") << "insert " << var << " const " << n << endl;
}
}
Debug("arith::static") << "iteConstant(" << n << ")" << endl;
if (d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) {
- DeltaRational min = std::min(d_minMap[n[1]], d_minMap[n[2]]);
- NodeToMinMaxMap::iterator minFind = d_minMap.find(n);
- if (minFind == d_minMap.end() || minFind->second < min) {
+ const DeltaRational& first = d_minMap[n[1]];
+ const DeltaRational& second = d_minMap[n[2]];
+ DeltaRational min = std::min(first, second);
+ CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n);
+ if (minFind == d_minMap.end() || (*minFind).second < min) {
d_minMap[n] = min;
Node nGeqMin;
if (min.getInfinitesimalPart() == 0) {
}
if (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end()) {
- DeltaRational max = std::max(d_maxMap[n[1]], d_maxMap[n[2]]);
- NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n);
- if (maxFind == d_maxMap.end() || maxFind->second > max) {
+ const DeltaRational& first = d_minMap[n[1]];
+ const DeltaRational& second = d_minMap[n[2]];
+ DeltaRational max = std::max(first, second);
+ CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
+ if (maxFind == d_maxMap.end() || (*maxFind).second > max) {
d_maxMap[n] = max;
Node nLeqMax;
if (max.getInfinitesimalPart() == 0) {
}
}
+std::set<Node> listToSet(TNode l){
+ std::set<Node> ret;
+ while(l.getKind() == OR){
+ Assert(l.getNumChildren() == 2);
+ ret.insert(l[0]);
+ l = l[1];
+ }
+ return ret;
+}
void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
// == 3-FINITE VALUE SET ==
- list<TNode>::iterator keyIter = d_miplibTrickKeys.begin();
- list<TNode>::iterator endKeys = d_miplibTrickKeys.end();
+ CDNodeToNodeListMap::const_iterator keyIter = d_miplibTrick.begin();
+ CDNodeToNodeListMap::const_iterator endKeys = d_miplibTrick.end();
while(keyIter != endKeys) {
- TNode var = *keyIter;
- const set<Node>& imps = d_miplibTrick[var];
+ TNode var = (*keyIter).first;
+ Node list = (*keyIter).second;
+ const set<Node> imps = listToSet(list);
+
+ if(imps.empty()){
+ ++keyIter;
+ continue;
+ }
Assert(!imps.empty());
vector<Node> conditions;
Result isTaut = PropositionalQuery::isTautology(possibleTaut);
if(isTaut == Result(Result::VALID)){
miplibTrick(var, values, learned);
- d_miplibTrick.erase(var);
- // also have to erase from keys list
- if(keyIter == endKeys) {
- // last element is special: exit loop
- d_miplibTrickKeys.erase(keyIter);
- break;
- } else {
- // non-last element: make sure iterator is incremented before erase
- list<TNode>::iterator eraseIter = keyIter++;
- d_miplibTrickKeys.erase(eraseIter);
- }
- } else {
- ++keyIter;
+ d_miplibTrick.insert(var, mkBoolNode(false));
}
+ ++keyIter;
}
}
void ArithStaticLearner::addBound(TNode n) {
- NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]);
- NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n[0]);
+ CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n[0]);
+ CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n[0]);
Rational constant = n[1].getConst<Rational>();
DeltaRational bound = constant;
bound = DeltaRational(constant, -1);
/* fall through */
case kind::LEQ:
- if (maxFind == d_maxMap.end() || maxFind->second > bound) {
+ if (maxFind == d_maxMap.end() || (*maxFind).second > bound) {
d_maxMap[n[0]] = bound;
Debug("arith::static") << "adding bound " << n << endl;
}
bound = DeltaRational(constant, 1);
/* fall through */
case kind::GEQ:
- if (minFind == d_minMap.end() || minFind->second < bound) {
+ if (minFind == d_minMap.end() || (*minFind).second < bound) {
d_minMap[n[0]] = bound;
Debug("arith::static") << "adding bound " << n << endl;
}
#include "util/statistics_registry.h"
#include "theory/arith/arith_utilities.h"
#include "theory/substitutions.h"
+
+#include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdhashmap.h"
#include <set>
-#include <list>
namespace CVC4 {
namespace theory {
class ArithStaticLearner {
private:
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
/* Maps a variable, x, to the set of defTrue nodes of the form
* (=> _ (= x c))
* where c is a constant.
*/
- typedef __gnu_cxx::hash_map<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap;
- VarToNodeSetMap d_miplibTrick;
- std::list<TNode> d_miplibTrickKeys;
-
- /**
- * Some integer variables are eligible to be replaced by
- * pseudoboolean variables. This map collects those eligible
- * substitutions.
- *
- * This is a reference to the substitution map in TheoryArith; as
- * it's not "owned" by this static learner, it isn't cleared on
- * clear(). This makes sense, as the static learner only
- * accumulates information in the substitution map, it never uses it
- * (i.e., it's write-only).
- */
- SubstitutionMap& d_pbSubstitutions;
+ //typedef __gnu_cxx::hash_map<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
+ // The domain is an implicit list OR(x, OR(y, ..., FALSE ))
+ // or FALSE
+ CDNodeToNodeListMap d_miplibTrick;
/**
* Map from a node to it's minimum and maximum.
*/
- typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
- NodeToMinMaxMap d_minMap;
- NodeToMinMaxMap d_maxMap;
+ //typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
+ typedef context::CDHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
+ CDNodeToMinMaxMap d_minMap;
+ CDNodeToMinMaxMap d_maxMap;
public:
- ArithStaticLearner(SubstitutionMap& pbSubstitutions);
+ ArithStaticLearner(context::Context* userContext);
void staticLearning(TNode n, NodeBuilder<>& learned);
void addBound(TNode n);
- void clear();
-
private:
void process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue);
//Sets of Nodes
typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
inline Node mkRationalNode(const Rational& q){
#pragma once
#include "expr/node.h"
-#include "expr/attribute.h"
#include "util/index.h"
#include "util/dense_map.h"
d_qflraStatus(Result::SAT_UNKNOWN),
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
- d_learner(d_pbSubstitutions),
+ d_learner(u),
d_setupLiteralCallback(this),
d_assertionsThatDoNotMatchTheirLiterals(c),
d_nextIntegerCheckVar(0),
d_tableau(),
d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack),
d_diosolver(c),
- d_pbSubstitutions(u),
d_restartsCounter(0),
d_tableauSizeHasBeenModified(false),
d_tableauResetDensity(1.6),
}
Node TheoryArith::ppRewrite(TNode atom) {
-
- if (!atom.getType().isBoolean()) {
- return atom;
- }
-
Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
- Node a = d_pbSubstitutions.apply(atom);
-
- if (a != atom) {
- Debug("pb") << "arith::preprocess() : after pb substitutions: " << a << endl;
- a = Rewriter::rewrite(a);
- Debug("pb") << "arith::preprocess() : after pb substitutions and rewriting: "
- << a << endl;
- Debug("arith::preprocess") << "arith::preprocess() :"
- << "after pb substitutions and rewriting: "
- << a << endl;
- }
-
- if (a.getKind() == kind::EQUAL && options::arithRewriteEq()) {
- Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1];
- Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1];
+ if (atom.getKind() == kind::EQUAL && options::arithRewriteEq()) {
+ Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
+ Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
Node rewritten = Rewriter::rewrite(leq.andNode(geq));
Debug("arith::preprocess") << "arith::preprocess() : returning "
<< rewritten << endl;
return rewritten;
+ } else {
+ return atom;
}
-
- return a;
}
Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
// d_out->lemma(lem);
// }
// }
-
- d_learner.clear();
}
EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
*/
DioSolver d_diosolver;
- /**
- * Some integer variables can be replaced with pseudoboolean
- * variables internally. This map is built up at static learning
- * time for top-level asserted expressions of the shape "x = 0 OR x
- * = 1". This substitution map is then applied in preprocess().
- *
- * Note that expressions of the shape "x >= 0 AND x <= 1" are
- * already substituted for PB versions at solve() time and won't
- * appear here.
- */
- SubstitutionMap d_pbSubstitutions;
-
/** Counts the number of notifyRestart() calls to the theory. */
uint32_t d_restartsCounter;
projects / cvc5.git / commitdiff