WIP: Debugging output and additional constraint

Author: tautschnig

src/solvers/flattening/boolbv_quantifier.cpp

@@ -8,6 +8,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
+#include <iostream>
+#include <util/format_expr.h>
+
 #include <util/arith_tools.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
@@ -169,11 +172,25 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
 
   if(expr.id()==ID_forall)
   {
-    return conjunction(expr_insts);
+#if 1
+    if(re.id() == ID_and)
+    {
+      expr_insts.push_back(binary_predicate_exprt(var_expr, ID_gt, from_integer(lb, var_expr.type())));
+      expr_insts.push_back(binary_predicate_exprt(var_expr, ID_le, from_integer(ub, var_expr.type())));
+    }
+#endif
+    return simplify_expr(conjunction(expr_insts), ns);
   }
   else if(expr.id() == ID_exists)
   {
-    return disjunction(expr_insts);
+#if 1
+    if(re.id() == ID_or)
+    {
+      expr_insts.push_back(binary_predicate_exprt(var_expr, ID_gt, from_integer(lb, var_expr.type())));
+      expr_insts.push_back(binary_predicate_exprt(var_expr, ID_le, from_integer(ub, var_expr.type())));
+    }
+#endif
+    return simplify_expr(disjunction(expr_insts), ns);
   }
 
   UNREACHABLE;
@@ -183,10 +200,12 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
 {
   PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
 
+  std::cerr << "Instantiate: " << format(src) << std::endl;
   const auto res = instantiate_quantifier(src, ns);
 
   if(res)
   {
+    std::cerr << "Instantiated: " << format(*res) << std::endl;
     return convert_bool(*res);
   }
   else