Add convenience function

diff --git a/src/csolver.cc b/src/csolver.cc
index 310d535489f365cb6fddf73b4f6ccae8d99ff0ef..d7003df0e95872b579cc0179db7f2a08a1cefa6c 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -93,6 +93,11 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
        return set;
 }
 
+Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) {
+       Set *s = createRangeSet(type, lowrange, highrange);
+       return getElementVar(s);
+}
+
 MutableSet *CSolver::createMutableSet(VarType type) {
        MutableSet *set = new MutableSet(type);
        allSets.push(set);
@@ -214,6 +219,14 @@ Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, ui
        }
 }
 
+bool CSolver::isTrue(Boolean *b) {
+       return b->isTrue();
+}
+
+bool CSolver::isFalse(Boolean *b) {
+       return b->isFalse();
+}
+
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
        Boolean * newarray[asize];
        switch(op) {

diff --git a/src/csolver.h b/src/csolver.h
index 85da23e117e8c0e5b4f5c699bbc4f16209b8a3fc..00abc666d7eb3f0df4a33906ecd917103816b10b 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -17,6 +17,8 @@ public:
 
        Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
 
+       Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
+               
        /** This function creates a mutable set. */
 
        MutableSet *createMutableSet(VarType type);
@@ -106,6 +108,9 @@ public:
 
        HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
 
+       bool isTrue(Boolean *b);
+       bool isFalse(Boolean *b);
+       
        void setUnSAT() { unsat = true; }
 
        bool isUnSAT() { return unsat; }