- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work.
- Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver.
- Fix to an assertion in CDQueue.
- Implements a CDArithVarSet using a vector of booleans and CDList.
- Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.
// Some elements have been enqueued and dequeued in the same
// context and now the queue is empty we can destruct them.
CDList<T>::truncateList(d_lastsave);
- Assert(d_size == d_lastsave);
+ Assert(CDList<T>::d_size == d_lastsave);
d_iter = d_lastsave;
}
}
libarith_la_SOURCES = \
theory_arith_type_rules.h \
+ arithvar.h \
arith_rewriter.h \
arith_rewriter.cpp \
arith_static_learner.h \
#ifndef __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H
#define __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
#include "theory/arith/partial_model.h"
#include "context/cdhashmap.h"
#include "context/cdo.h"
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
using namespace CVC4::kind;
using namespace std;
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
bool ArithPropManager::isAsserted(TNode n) const{
Node satValue = d_valuation.getSatValue(n);
if(satValue.isNull()){
StatisticsRegistry::unregisterStat(&d_alreadyPropagatedNode);
StatisticsRegistry::unregisterStat(&d_addedPropagation);
}
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
#define __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H
#include "theory/valuation.h"
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "theory/arith/arithvar_node_map.h"
#include "theory/arith/atom_database.h"
#include "theory/arith/delta_rational.h"
#include <set>
#include <stack>
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
+namespace CVC4 {
+namespace theory {
+namespace arith {
bool isVariable(TNode t){
return t.getMetaKind() == kind::metakind::VARIABLE;
}
+bool ArithRewriter::isAtom(TNode n) {
+ return arith::isRelationOperator(n.getKind());
+}
+
RewriteResponse ArithRewriter::rewriteConstant(TNode t){
Assert(t.getMetaKind() == kind::metakind::CONSTANT);
Node val = coerceToRationalNode(t);
return RewriteResponse(REWRITE_AGAIN, mult);
}
}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief Rewriter for arithmetic.
**
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** Rewriter for the theory of arithmetic. This rewrites to the normal form for
+ ** arithmetic. See theory/arith/normal_form.h for more information.
**/
#include "cvc4_private.h"
#define __CVC4__THEORY__ARITH__ARITH_REWRITER_H
#include "theory/theory.h"
-#include "theory/arith/arith_utilities.h"
-#include "theory/arith/normal_form.h"
-
#include "theory/rewriter.h"
namespace CVC4 {
namespace arith {
class ArithRewriter {
+public:
+
+ static RewriteResponse preRewrite(TNode n);
+ static RewriteResponse postRewrite(TNode n);
+ static Node rewriteEquality(TNode equality) {
+ // Arithmetic owns the domain, so this is totally ok
+ return Rewriter::rewrite(equality);
+ }
+
+ static void init() { }
+
+ static void shutdown() { }
private:
static RewriteResponse postRewriteAtom(TNode t);
static RewriteResponse postRewriteAtomConstantRHS(TNode t);
-public:
-
- static RewriteResponse preRewrite(TNode n);
- static RewriteResponse postRewrite(TNode n);
- static Node rewriteEquality(TNode equality) {
- // Arithmetic owns the domain, so this is totally ok
- return Rewriter::rewrite(equality);
- }
-
- static void init() { }
-
- static void shutdown() { }
-
-private:
-
- static inline bool isAtom(TNode n) {
- return arith::isRelationOperator(n.getKind());
- }
+ static bool isAtom(TNode n);
static inline bool isTerm(TNode n) {
return !isAtom(n);
#include <vector>
using namespace std;
-
-using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
ArithStaticLearner::ArithStaticLearner(SubstitutionMap& pbSubstitutions) :
break;
}
}
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief Arith utilities are common inline functions for dealing with nodes.
**
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** Arith utilities are common functions for dealing with nodes.
**/
#include "cvc4_private.h"
#define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
#include "util/rational.h"
+#include "util/integer.h"
#include "expr/node.h"
-#include "expr/attribute.h"
#include "theory/arith/delta_rational.h"
#include "context/cdhashset.h"
-#include <vector>
-#include <stdint.h>
-#include <limits>
#include <ext/hash_map>
+#include <vector>
namespace CVC4 {
namespace theory {
namespace arith {
-
-typedef uint32_t ArithVar;
-//static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
-#define ARITHVAR_SENTINEL std::numeric_limits<ArithVar>::max()
-
-//Maps from Nodes -> ArithVars, and vice versa
-typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
-typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap;
-
//Sets of Nodes
typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
-typedef context::CDHashSet<ArithVar> CDArithVarSet;
-
-class ArithVarCallBack {
-public:
- virtual void callback(ArithVar x) = 0;
-};
-
-
-
inline Node mkRationalNode(const Rational& q){
return NodeManager::currentNM()->mkConst<Rational>(q);
}
* Given a relational kind, k, return the kind k' s.t.
* swapping the lefthand and righthand side is equivalent.
*
- * The following equivalence should hold,
+ * The following equivalence should hold,
* (k l r) <=> (k' r l)
*/
inline Kind reverseRelationKind(Kind k){
--- /dev/null
+/********************* */
+/*! \file arithvar.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Defines ArithVar which is the internal representation of variables in arithmetic
+ **
+ ** This defines ArithVar which is the internal representation of variables in
+ ** arithmetic. This is a typedef from uint32_t to ArithVar.
+ ** This file also provides utilities for ArithVars.
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITHVAR_H
+#define __CVC4__THEORY__ARITH__ARITHVAR_H
+
+#include <limits>
+#include <stdint.h>
+#include <ext/hash_map>
+#include "expr/node.h"
+#include "context/cdhashset.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+typedef uint32_t ArithVar;
+const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
+
+//Maps from Nodes -> ArithVars, and vice versa
+typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
+typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap;
+
+/**
+ * ArithVarCallBack provides a mechanism for agreeing on callbacks while
+ * breaking mutual recursion inclusion order problems.
+ */
+class ArithVarCallBack {
+public:
+ virtual void callback(ArithVar x) = 0;
+};
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__ARITHVAR_H */
#define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "context/context.h"
#include "context/cdlist.h"
#include "context/cdhashmap.h"
#define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
#include <vector>
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
+#include "context/context.h"
+#include "context/cdlist.h"
+
namespace CVC4 {
namespace theory {
}
}
- /** Invalidates iterators */
- /* void init(ArithVar x, bool val) { */
- /* Assert(x >= allocated()); */
- /* increaseSize(x); */
- /* if(val){ */
- /* add(x); */
- /* } */
- /* } */
-
/**
* Invalidates iterators.
*/
}
};
+class CDArithVarSet {
+private:
+
+ class RemoveIntWrapper{
+ private:
+ ArithVar d_var;
+ ArithVarCallBack& d_onDestruction;
+
+ public:
+ RemoveIntWrapper(ArithVar v, ArithVarCallBack& onDestruction):
+ d_var(v), d_onDestruction(onDestruction)
+ {}
+
+ ~RemoveIntWrapper(){
+ d_onDestruction.callback(d_var);
+ }
+ };
+
+ std::vector<bool> d_set;
+ context::CDList<RemoveIntWrapper> d_list;
+
+ class OnDestruction : public ArithVarCallBack {
+ private:
+ std::vector<bool>& d_set;
+ public:
+ OnDestruction(std::vector<bool>& set):
+ d_set(set)
+ {}
+
+ void callback(ArithVar x){
+ Assert(x < d_set.size());
+ d_set[x] = false;
+ }
+ };
+
+ OnDestruction d_callback;
+
+public:
+ CDArithVarSet(context::Context* c) :
+ d_list(c), d_callback(d_set)
+ { }
+
+ /** This cannot be const as garbage collection is done lazily. */
+ bool contains(ArithVar x) const{
+ if(x < d_set.size()){
+ return d_set[x];
+ }else{
+ return false;
+ }
+ }
+
+ void insert(ArithVar x){
+ Assert(!contains(x));
+ if(x >= d_set.size()){
+ d_set.resize(x+1, false);
+ }
+ d_list.push_back(RemoveIntWrapper(x, d_callback));
+ d_set[x] = true;
+ }
+};
+
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#include <list>
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-
+using namespace std;
using namespace CVC4::kind;
-using namespace std;
+namespace CVC4 {
+namespace theory {
+namespace arith {
ArithAtomDatabase::ArithAtomDatabase(context::Context* cxt, OutputChannel& out) :
d_arithOut(out), d_setsMap()
Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
return result;
}
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
#ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
#define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "theory/uf/equality_engine.h"
#include "context/cdo.h"
#include "context/cdlist.h"
#include "theory/arith/tableau.h"
#include "theory/arith/partial_model.h"
-#include "theory/arith/arith_utilities.h"
#include "util/rational.h"
#include "util/stats.h"
#define __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H
#include "theory/arith/delta_rational.h"
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/tableau.h"
typedef std::set<TNode, RightHandRationalLT> EqualValueSet;
-// struct SetCleanupStrategy{
-// static void cleanup(OrderedSet* l){
-// Debug("arithgc") << "cleaning up " << l << "\n";
-// delete l;
-// }
-// };
-
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
bool ArithPartialModel::boundsAreEqual(ArithVar x){
}
d_deltaIsSafe = true;
}
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
#include "context/context.h"
#include "context/cdvector.h"
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "theory/arith/delta_rational.h"
#include "expr/attribute.h"
#include "expr/node.h"
#ifndef __CVC4__THEORY__ARITH__SIMPLEX_H
#define __CVC4__THEORY__ARITH__SIMPLEX_H
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "theory/arith/arith_priority_queue.h"
#include "theory/arith/arithvar_set.h"
#include "theory/arith/delta_rational.h"
#include "expr/node.h"
#include "expr/attribute.h"
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "theory/arith/arithvar_set.h"
#include "theory/arith/normal_form.h"
#include <stdint.h>
using namespace std;
-
-using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
+namespace CVC4 {
+namespace theory {
+namespace arith {
-static const uint32_t RESET_START = 2;
+const uint32_t RESET_START = 2;
TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
d_learner(d_pbSubstitutions),
d_nextIntegerCheckVar(0),
d_constantIntegerVariables(c),
- d_CivIterator(c,0),
- d_varsInDioSolver(c),
d_diseq(c),
d_partialModel(c, d_differenceManager),
d_tableau(),
}
//TODO Relax to less than?
- if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
+ if(d_partialModel.lessThanLowerBound(x_i, c_i)){
return Node::null();
}
Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
- if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
+ if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
return Node::null(); //sat
}
}
Node TheoryArith::callDioSolver(){
- while(d_CivIterator < d_constantIntegerVariables.size()){
- ArithVar v = d_constantIntegerVariables[d_CivIterator];
- d_CivIterator = d_CivIterator + 1;
+ while(!d_constantIntegerVariables.empty()){
+ ArithVar v = d_constantIntegerVariables.front();
+ d_constantIntegerVariables.pop();
Debug("arith::dio") << v << endl;
Assert(isInteger(v));
Assert(d_partialModel.boundsAreEqual(v));
- if(d_varsInDioSolver.find(v) != d_varsInDioSolver.end()){
- continue;
- }else{
- d_varsInDioSolver.insert(v);
- }
-
TNode lb = d_partialModel.getLowerConstraint(v);
TNode ub = d_partialModel.getUpperConstraint(v);
propagateCandidate(candidate);
}
}
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
#include "context/context.h"
#include "context/cdlist.h"
#include "context/cdhashset.h"
+#include "context/cdqueue.h"
#include "expr/node.h"
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "theory/arith/arithvar_set.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
/**
* Queue of Integer variables that are known to be equal to a constant.
*/
- context::CDList<ArithVar> d_constantIntegerVariables;
- /** Iterator over d_constantIntegerVariables. */
- context::CDO<unsigned int> d_CivIterator;
+ context::CDQueue<ArithVar> d_constantIntegerVariables;
Node callDioSolver();
Node dioCutting();
Comparison mkIntegerEqualityFromAssignment(ArithVar v);
- //TODO Replace with a more efficient check
- CDArithVarSet d_varsInDioSolver;
-
/**
* If ArithVar v maps to the node n in d_removednode,
* then n = (= asNode(v) rhs) where rhs is a term that
projects / cvc5.git / commitdiff