From 1eb1c9ae905ac8ce35c037b7437d2427ff054d20 Mon Sep 17 00:00:00 2001
From: Robin Steiger <robin.steiger@epfl.ch>
Date: Mon, 12 Jul 2010 20:17:32 +0000
Subject: [PATCH] BAPA (without Unifier) now relaxes the formula only until
 AFTER negation.

---
 src/orderedsets/Main.scala | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/orderedsets/Main.scala b/src/orderedsets/Main.scala
index 40a29f15c..be1bb3340 100644
--- a/src/orderedsets/Main.scala
+++ b/src/orderedsets/Main.scala
@@ -7,7 +7,7 @@ import Reconstruction.Model
 import RPrettyPrinter.rpp
 
 class Main(reporter: Reporter) extends Solver(reporter) {
-  import purescala.Trees.Expr
+  import purescala.Trees.{Expr,expandLets,negate}
   import AST.Formula
   val description = "BAPA with ordering"
   override val shortDescription = "BAPA<"
@@ -22,14 +22,14 @@ class Main(reporter: Reporter) extends Solver(reporter) {
   def solve(exprWithLets: Expr): Option[Boolean] = {
     //reporter.info("INPUT to Ordered BAPA\n" + rpp(exprWithLets))
 
-    val expr = purescala.Trees.expandLets(exprWithLets)
+    val expr = expandLets(exprWithLets)
 
     //reporter.info("INPUT to Ordered BAPA\n" + rpp(expr))
 
     //reporter.info("Sets: " + ExprToASTConverter.getSetTypes(expr))
     try {
       // Negate formula
-      (Some(!solve(!ExprToASTConverter(expr, reporter))), {
+      (Some(!solve(ExprToASTConverter(negate(expr), reporter))), {
 
         val sets = ExprToASTConverter.getSetTypes(expr)
         if (sets.size > 1)
@@ -55,7 +55,8 @@ class Main(reporter: Reporter) extends Solver(reporter) {
   // true means formula is SAT
   // false means formula is UNSAT
   def solve(formula: Formula): Boolean = {
-    //reporter.info("BAPA< formula to be shown unsat:\n" + NormalForms.nnf(formula).toString)
+    reporter.info("BAPA< formula to be shown unsat:\n" + formula.toString)
+//    reporter.info("BAPA< formula to be shown unsat:\n" + NormalForms.nnf(formula).toString)
 
     val z3 = new Context(formula, reporter)
     val startTime = System.nanoTime
@@ -217,7 +218,7 @@ object ExprToASTConverter {
         toFormula(expr)
       } catch {
         case ConversionException(badExpr, msg) =>
-          //reporter.warning("BAPA was relaxed : " + msg + " in " + badExpr.getClass + "\n" + rpp(badExpr))
+          reporter.warning("BAPA was relaxed : " + msg + " in " + badExpr.getClass + "\n" + rpp(badExpr))
           formulaRelaxed = true
           AST.True // Assuming the formula to be True
       }
-- 
GitLab