fixing more bugs ...
authorHamed <hamed.gorjiara@gmail.com>
Mon, 10 Jul 2017 22:12:29 +0000 (15:12 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Mon, 10 Jul 2017 22:12:29 +0000 (15:12 -0700)
src/AST/order.c
src/Backend/constraint.c
src/Backend/satencoder.c
src/Test/buildconstraints.c

index 2f3de74478ef26928919c5a53aea039aa48cdd3a..b943392f81daba49e02539c46a4e2823f505e08a 100644 (file)
@@ -29,6 +29,7 @@ void setOrderEncodingType(Order* order, OrderEncodingType type){
 void deleteOrder(Order* order){
        deleteVectorArrayBoolean(& order->constraints);
        deleteOrderEncoding(& order->order);
-       deleteHashTableBoolConst(order->boolsToConstraints);
+       if(order->boolsToConstraints!= NULL)
+               deleteHashTableBoolConst(order->boolsToConstraints);
        ourfree(order);
 }
index b491ca30f2e94ba760a84c9ee1d09573d2b13eba..ef607099abf8c995c02424242c2d7390b17b658c 100644 (file)
@@ -159,6 +159,7 @@ void printConstraint(Constraint * This) {
                model_print("!t%u",This->numoperandsorvar);
                break;
        default:
+               model_print("In printingConstraint: %d", This->type);
                ASSERT(0);
        }
 }
index 4a72f0abd54d8cbac585d8d4e5d0310e740bc2c4..3c2d3e1eb6fae92802393a8596596262ea6a0de9 100644 (file)
@@ -82,9 +82,9 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
        for(uint i=0;i<size;i++) {
                Boolean *constraint=getVectorBoolean(constraints, i);
                Constraint* c= encodeConstraintSATEncoder(This, constraint);
-               addConstraintToSATSolver(c, This->satSolver);
                printConstraint(c);
                model_print("\n\n");
+               addConstraintToSATSolver(c, This->satSolver);
                //FIXME: When do we want to delete constraints? Should we keep an array of them
                // and delete them later, or it would be better to just delete them right away?
        }
index c91fd571294e276c65072854989be2eb38fea878..81f01b3988c38deac8bbd87ed16560bfeb2c5f70 100644 (file)
@@ -38,6 +38,6 @@ int main(int numargs, char ** argv) {
        Element* inputs2 [] = {e4, e3};
        Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
        addBoolean(solver, pred);
-//     startEncoding(solver);
+       startEncoding(solver);
        deleteSolver(solver);
 }