add simplifier to java API

src/api/dotnet/Simplifiers.cs

@@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation
 
 Module Name:
 
-    Tactic.cs
+    Simplifiers.cs
 
 Abstract:
 

src/api/java/CMakeLists.txt

@@ -165,6 +165,8 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   SeqExpr.java
   SeqSort.java
   SetSort.java
+  Simplifier.java
+  SimplifierDecRefQueue.java
   SolverDecRefQueue.java
   Solver.java
   Sort.java

src/api/java/Context.java

@@ -3081,6 +3081,106 @@ public class Context implements AutoCloseable {
         Native.interrupt(nCtx());
     }
 
+    /**
+     * The number of supported simplifiers.
+     **/
+    public int getNumSimplifiers()
+    {
+        return Native.getNumSimplifiers(nCtx());
+    }
+
+    /**
+     * The names of all supported simplifiers.
+     **/
+    public String[] getSimplifierNames()
+    {
+
+        int n = getNumSimplifiers();
+        String[] res = new String[n];
+        for (int i = 0; i < n; i++)
+            res[i] = Native.getSimplifierName(nCtx(), i);
+        return res;
+    }
+
+    /**
+     * Returns a string containing a description of the simplifier with the given
+     * name.
+     **/
+    public String getSimplifierDescription(String name)
+    {
+        return Native.simplifierGetDescr(nCtx(), name);
+    }
+
+    /**
+     * Creates a new Simplifier.
+     **/
+    public Simplifier mkSimplifier(String name)
+    {
+        return new Simplifier(this, name);
+    }
+
+    /**
+     * Create a simplifier that applies {@code t1} and then {@code t1}
+     **/
+    public Simplifier andThen(Simplifier t1, Simplifier t2, Simplifier... ts)
+
+    {
+        checkContextMatch(t1);
+        checkContextMatch(t2);
+        checkContextMatch(ts);
+
+        long last = 0;
+        if (ts != null && ts.length > 0)
+        {
+            last = ts[ts.length - 1].getNativeObject();
+            for (int i = ts.length - 2; i >= 0; i--) {
+                last = Native.simplifierAndThen(nCtx(), ts[i].getNativeObject(),
+                    last);
+            }
+        }
+        if (last != 0)
+        {
+            last = Native.simplifierAndThen(nCtx(), t2.getNativeObject(), last);
+            return new Simplifier(this, Native.simplifierAndThen(nCtx(),
+                    t1.getNativeObject(), last));
+        } else
+            return new Simplifier(this, Native.simplifierAndThen(nCtx(),
+                    t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Create a simplifier that applies {@code t1} and then {@code t2}
+     *
+     * Remarks:  Shorthand for {@code AndThen}. 
+     **/
+    public Simplifier then(Simplifier t1, Simplifier t2, Simplifier... ts)
+    {
+        return andThen(t1, t2, ts);
+    }
+
+    /**
+     * Create a simplifier that applies {@code t} using the given set of
+     * parameters {@code p}.
+     **/
+    public Simplifier usingParams(Simplifier t, Params p)
+    {
+        checkContextMatch(t);
+        checkContextMatch(p);
+        return new Simplifier(this, Native.simplifierUsingParams(nCtx(),
+                t.getNativeObject(), p.getNativeObject()));
+    }
+
+    /**
+     * Create a simplifier that applies {@code t} using the given set of
+     * parameters {@code p}.
+     * Remarks: Alias for
+     * {@code UsingParams}
+     **/
+    public Simplifier with(Simplifier t, Params p)
+    {
+        return usingParams(t, p);
+    }
+
     /**
      * The number of supported Probes.
      **/
@@ -3279,6 +3379,14 @@ public class Context implements AutoCloseable {
                 t.getNativeObject()));
     }
 
+    /**
+     * Creates a solver that is uses the simplifier pre-processing.
+     **/
+    public Solver mkSolver(Solver s, Simplifier simp)
+    {
+        return new Solver(this, Native.solverAddSimplifier(nCtx(), s.getNativeObject(), simp.getNativeObject()));
+    }
+
     /**
      * Create a Fixedpoint context.
      **/
@@ -4209,6 +4317,7 @@ public class Context implements AutoCloseable {
     private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
     private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
     private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
+    private SimplifierDecRefQueue m_Simplifier_DRQ = new SimplifierDecRefQueue();
     private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
     private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
     private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
@@ -4293,6 +4402,11 @@ public class Context implements AutoCloseable {
         return m_Tactic_DRQ;
     }
 
+    public IDecRefQueue<Simplifier> getSimplifierDRQ()
+    {
+        return m_Simplifier_DRQ;
+    }
+
     public IDecRefQueue<Fixedpoint> getFixedpointDRQ()
     {
         return m_Fixedpoint_DRQ;
@@ -4323,6 +4437,7 @@ public class Context implements AutoCloseable {
         m_Optimize_DRQ.forceClear(this);
         m_Statistics_DRQ.forceClear(this);
         m_Tactic_DRQ.forceClear(this);
+        m_Simplifier_DRQ.forceClear(this);
         m_Fixedpoint_DRQ.forceClear(this);
 
         m_boolSort = null;

src/api/java/Simplifier.java

@@ -0,0 +1,58 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    Simplifiers.cs
+
+Abstract:
+
+    Z3 Managed API: Simplifiers
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-21
+
+--*/
+
+package com.microsoft.z3;
+
+
+public class Simplifier extends Z3Object {
+    /*
+     * A string containing a description of parameters accepted by the simplifier.
+     */
+
+    public String getHelp()
+    {
+	return Native.simplifierGetHelp(getContext().nCtx(), getNativeObject());
+    }
+
+    /*
+     * Retrieves parameter descriptions for Simplifiers.
+     */
+    public ParamDescrs getParameterDescriptions() {
+	return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject())); 
+    }
+
+    Simplifier(Context ctx, long obj)
+    {
+	super(ctx, obj);
+    }
+
+    Simplifier(Context ctx, String name)
+    {
+	super(ctx, Native.mkSimplifier(ctx.nCtx(), name));
+    }
+
+    @Override
+    void incRef()
+    {
+	Native.simplifierIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
+        getContext().getSimplifierDRQ().storeReference(getContext(), this);
+    }
+}	

src/api/java/SimplifierDecRefQueue.java

@@ -0,0 +1,31 @@
+/**
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    SimplifierDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
+package com.microsoft.z3;
+
+class SimplifierDecRefQueue extends IDecRefQueue<Simplifier> {
+    public SimplifierDecRefQueue() 
+    {
+        super();
+    }
+
+    @Override
+    protected void decRef(Context ctx, long obj)
+    {
+        Native.simplifierDecRef(ctx.nCtx(), obj);
+    }
+}