ezSAT: Fixed handling of eliminated Literals, added auto-freeze for expressions

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 4389c7a62293cc7b9765d818121c2828ab462d14..bbebee74f6f3619ebeef2d96f5f05556ba2eb78e 100644 (file)
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -485,12 +485,16 @@ std::string ezSAT::cnfLiteralInfo(int idx) const
        return "<unnamed>";
 }
 
-int ezSAT::bind(int id)
+int ezSAT::bind(int id, bool auto_freeze)
 {
        if (id >= 0) {
                assert(0 < id && id <= int(literals.size()));
                cnfLiteralVariables.resize(literals.size());
-               if (cnfLiteralVariables[id-1] == 0 || eliminated(cnfLiteralVariables[id-1])) {
+               if (eliminated(cnfLiteralVariables[id-1])) {
+                       fprintf(stderr, "ezSAT: Missing freeze on literal `%s'.\n", to_string(id).c_str());
+                       abort();
+               }
+               if (cnfLiteralVariables[id-1] == 0) {
                        cnfLiteralVariables[id-1] = ++cnfVariableCount;
                        if (id == TRUE)
                                add_clause(+cnfLiteralVariables[id-1]);
@@ -503,7 +507,18 @@ int ezSAT::bind(int id)
        assert(0 < -id && -id <= int(expressions.size()));
        cnfExpressionVariables.resize(expressions.size());
 
-       if (cnfExpressionVariables[-id-1] == 0 || eliminated(cnfExpressionVariables[-id-1]))
+       if (eliminated(cnfExpressionVariables[-id-1]))
+       {
+               cnfExpressionVariables[-id-1] = 0;
+
+               // this will recursively call bind(id). within the recursion
+               // the cnf is pre-set to 0. an idx is allocated there, then it
+               // is frozen, then it returns here with the new idx already set.
+               if (auto_freeze)
+                       freeze(id);
+       }
+
+       if (cnfExpressionVariables[-id-1] == 0)
        {
                OpId op;
                std::vector<int> args;
@@ -520,7 +535,7 @@ int ezSAT::bind(int id)
                                                newArgs.push_back(OR(AND(args[i], NOT(args[i+1])), AND(NOT(args[i]), args[i+1])));
                                args.swap(newArgs);
                        }
-                       idx = bind(args.at(0));
+                       idx = bind(args.at(0), false);
                        goto assign_idx;
                }
 
@@ -528,17 +543,17 @@ int ezSAT::bind(int id)
                        std::vector<int> invArgs;
                        for (auto arg : args)
                                invArgs.push_back(NOT(arg));
-                       idx = bind(OR(expression(OpAnd, args), expression(OpAnd, invArgs)));
+                       idx = bind(OR(expression(OpAnd, args), expression(OpAnd, invArgs)), false);
                        goto assign_idx;
                }
 
                if (op == OpITE) {
-                       idx = bind(OR(AND(args[0], args[1]), AND(NOT(args[0]), args[2])));
+                       idx = bind(OR(AND(args[0], args[1]), AND(NOT(args[0]), args[2])), false);
                        goto assign_idx;
                }
 
                for (int i = 0; i < int(args.size()); i++)
-                       args[i] = bind(args[i]);
+                       args[i] = bind(args[i], false);
 
                switch (op)
                {

diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 16f940a1d98d403ced6852cf0483e9f85479a3b6..13b39d4ef81184bcc7e60a6e55d76baa408112d0 100644 (file)
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -143,7 +143,7 @@ public:
        virtual void freeze(int id);
        virtual bool eliminated(int idx);
        void assume(int id);
-       int bind(int id);
+       int bind(int id, bool auto_freeze = true);
        int bound(int id) const;
 
        int numCnfVariables() const { return cnfVariableCount; }