From a79143bc592a6a8932f2384a8b61ad3b2b3cbd86 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Fri, 29 Sep 2017 13:43:27 -0700 Subject: [PATCH] Adding pring option for AST --- src/AST/element.cc | 21 +++++++++++++++++++++ src/AST/function.cc | 11 +++++++++++ src/AST/order.cc | 6 ++++++ src/AST/order.h | 1 + src/AST/predicate.cc | 6 ++++++ src/AST/predicate.h | 3 +++ src/AST/set.cc | 15 +++++++++++++++ src/AST/set.h | 1 + src/AST/table.cc | 14 ++++++++++++++ src/AST/table.h | 1 + src/Backend/satencoder.cc | 1 + src/common.h | 8 ++++---- 12 files changed, 84 insertions(+), 4 deletions(-) diff --git a/src/AST/element.cc b/src/AST/element.cc index ed0a741..fb5b822 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -77,6 +77,12 @@ void ElementSet::serialize(Serializer* serializer){ serializer->mywrite(&set, sizeof(Set*)); } +void ElementSet::print(){ + model_println("{ElementSet:"); + set->print(); + model_println("}\n"); +} + void ElementConst::serialize(Serializer* serializer){ if(serializer->isSerialized(this)) return; @@ -92,6 +98,10 @@ void ElementConst::serialize(Serializer* serializer){ serializer->mywrite(&value, sizeof(uint64_t)); } +void ElementConst::print(){ + model_println("{ElementConst: %lu}", value); +} + void ElementFunction::serialize(Serializer* serializer){ if(serializer->isSerialized(this)) return; @@ -118,3 +128,14 @@ void ElementFunction::serialize(Serializer* serializer){ serializer->mywrite(&overflowstat, sizeof(Boolean*)); } +void ElementFunction::print(){ + model_println("{ElementFunction:"); + function->print(); + model_println("Elements:"); + uint size = inputs.getSize(); + for(uint i=0; iprint(); + } + model_println("}\n"); +} diff --git a/src/AST/function.cc b/src/AST/function.cc index 96b0797..26decd0 100644 --- a/src/AST/function.cc +++ b/src/AST/function.cc @@ -82,6 +82,13 @@ void FunctionTable::serialize(Serializer* serializer){ } +void FunctionTable::print(){ + model_println("{FunctionTable:"); + table->print(); + model_println("}\n"); + +} + void FunctionOperator::serialize(Serializer* serializer){ if(serializer->isSerialized(this)) return; @@ -106,4 +113,8 @@ void FunctionOperator::serialize(Serializer* serializer){ } serializer->mywrite(&range, sizeof(Set *)); serializer->mywrite(&overflowbehavior, sizeof(OverFlowBehavior)); +} + +void FunctionOperator::print(){ + model_println("{FunctionOperator: %s}", op == SATC_ADD? "ADD": "SUB" ); } \ No newline at end of file diff --git a/src/AST/order.cc b/src/AST/order.cc index 3920d3b..96e7be5 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -58,3 +58,9 @@ void Order::serialize(Serializer* serializer){ serializer->mywrite(&type, sizeof(OrderType)); serializer->mywrite(&set, sizeof(Set *)); } + +void Order::print(){ + model_println("{Order on Set:"); + set->print(); + model_println("}\n"); +} diff --git a/src/AST/order.h b/src/AST/order.h index b8ca724..e2e0b43 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -17,6 +17,7 @@ public: OrderGraph *graph; Order *clone(CSolver *solver, CloneMap *map); void serialize(Serializer *serializer ); + void print(); Vector constraints; OrderEncoding encoding; void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;}; diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc index e3ae1db..659a3e3 100644 --- a/src/AST/predicate.cc +++ b/src/AST/predicate.cc @@ -66,6 +66,12 @@ void PredicateTable::serialize(Serializer* serializer){ serializer->mywrite(&undefinedbehavior, sizeof(UndefinedBehavior)); } +void PredicateTable::print(){ + model_println("{PredicateTable:"); + table->print(); + model_println("}\n"); +} + void PredicateOperator::serialize(Serializer* serializer){ if(serializer->isSerialized(this)) return; diff --git a/src/AST/predicate.h b/src/AST/predicate.h index beaebc9..94a7e2e 100644 --- a/src/AST/predicate.h +++ b/src/AST/predicate.h @@ -13,6 +13,7 @@ public: virtual ~Predicate() {} virtual Predicate *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;} virtual void serialize(Serializer* serializer) = 0; + virtual void print() =0; PredicateType type; CMEMALLOC; }; @@ -23,6 +24,7 @@ public: bool evalPredicateOperator(uint64_t *inputs); Predicate *clone(CSolver *solver, CloneMap *map); virtual void serialize(Serializer* serializer); + virtual void print(); Array domains; CompOp getOp() {return op;} CMEMALLOC; @@ -35,6 +37,7 @@ public: PredicateTable(Table *table, UndefinedBehavior undefBehavior); Predicate *clone(CSolver *solver, CloneMap *map); virtual void serialize(Serializer* serializer); + virtual void print(); Table *table; UndefinedBehavior undefinedbehavior; CMEMALLOC; diff --git a/src/AST/set.cc b/src/AST/set.cc index d3801f8..25ccd05 100644 --- a/src/AST/set.cc +++ b/src/AST/set.cc @@ -142,3 +142,18 @@ void Set::serialize(Serializer* serializer){ serializer->mywrite(&mem, sizeof(uint64_t)); } } + +void Set::print(){ + model_print("{Set:"); + if(isRange){ + model_print("Range: low=%lu, high=%lu}\n\n", low, high); + } else { + uint size = members->getSize(); + model_print("Members: "); + for(uint i=0; iget(i); + model_print("%lu, ", mem); + } + model_println("}\n"); + } +} diff --git a/src/AST/set.h b/src/AST/set.h index ad89504..a0bd449 100644 --- a/src/AST/set.h +++ b/src/AST/set.h @@ -28,6 +28,7 @@ public: virtual bool isMutableSet() {return false;} virtual Set *clone(CSolver *solver, CloneMap *map); virtual void serialize(Serializer* serializer); + virtual void print(); CMEMALLOC; protected: VarType type; diff --git a/src/AST/table.cc b/src/AST/table.cc index 838a53a..f6494f4 100644 --- a/src/AST/table.cc +++ b/src/AST/table.cc @@ -97,3 +97,17 @@ void Table::serialize(Serializer* serializer){ } +void Table::print(){ + model_println("{Table:"); + SetIteratorTableEntry* iterator = getEntries(); + while(iterator->hasNext()){ + TableEntry* entry = iterator->next(); + model_print("<"); + for(uint i=0; iinputSize; i++){ + model_print("%lu, ", entry->inputs[i]); + } + model_print(" == %lu>", entry->output); + } + model_println("}\n"); + delete iterator; +} diff --git a/src/AST/table.h b/src/AST/table.h index db8d188..d8c7829 100644 --- a/src/AST/table.h +++ b/src/AST/table.h @@ -11,6 +11,7 @@ public: TableEntry *getTableEntry(uint64_t *inputs, uint inputSize); Table *clone(CSolver *solver, CloneMap *map); void serialize(Serializer *serializer); + void print(); ~Table(); Set * getRange() {return range;} diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index fdeee9e..3a30362 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -29,6 +29,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) { SetIteratorBooleanEdge *iterator = csolver->getConstraints(); while (iterator->hasNext()) { BooleanEdge constraint = iterator->next(); + constraint.getBoolean()->print(); Edge c = encodeConstraintSATEncoder(constraint); addConstraintCNF(cnf, c); } diff --git a/src/common.h b/src/common.h index 4ebd816..d52924c 100644 --- a/src/common.h +++ b/src/common.h @@ -18,7 +18,7 @@ #include "config.h" #include "time.h" -/* + extern int model_out; extern int model_err; extern int switch_alloc; @@ -26,12 +26,12 @@ #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0) #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0) - +#define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0) #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0) - */ -#define model_print printf + +//#define model_print printf #define NEXTPOW2(x) ((x == 1) ? 1 : (1 << (sizeof(uint) * 8 - __builtin_clz(x - 1)))) #define NUMBITS(x) ((x == 0) ? 0 : 8 * sizeof(x) - __builtin_clz(x)) -- 2.34.1