From: bdemsky <bdemsky@uci.edu>
Date: Thu, 31 Aug 2017 02:32:48 +0000 (-0700)
Subject: Add convenience function
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=11cc56937134082a7e29b90e1376de589ee877ae;p=satune.git

Add convenience function
---

diff --git a/src/csolver.cc b/src/csolver.cc
index 310d535..d7003df 100644
--- 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 85da23e..00abc66 100644
--- 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; }