From 4143c542571948368a6a36334a21392ed50ddb3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:06:26 -0800 Subject: [PATCH] add simplifier to java API --- src/api/dotnet/Simplifiers.cs | 2 +- src/api/java/CMakeLists.txt | 2 + src/api/java/Context.java | 115 ++++++++++++++++++++++++ src/api/java/Simplifier.java | 58 ++++++++++++ src/api/java/SimplifierDecRefQueue.java | 31 +++++++ 5 files changed, 207 insertions(+), 1 deletion(-) create mode 100644 src/api/java/Simplifier.java create mode 100644 src/api/java/SimplifierDecRefQueue.java diff --git a/src/api/dotnet/Simplifiers.cs b/src/api/dotnet/Simplifiers.cs index a7fbe185f..28469c1e5 100644 --- a/src/api/dotnet/Simplifiers.cs +++ b/src/api/dotnet/Simplifiers.cs @@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - Tactic.cs + Simplifiers.cs Abstract: diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index e0d6bd0a0..4b13a25b1 100644 --- a/src/api/java/CMakeLists.txt +++ b/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 diff --git a/src/api/java/Context.java b/src/api/java/Context.java index d48101235..0f15d9411 100644 --- a/src/api/java/Context.java +++ b/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 getSimplifierDRQ() + { + return m_Simplifier_DRQ; + } + public IDecRefQueue 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; diff --git a/src/api/java/Simplifier.java b/src/api/java/Simplifier.java new file mode 100644 index 000000000..b3fc89ccf --- /dev/null +++ b/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); + } +} \ No newline at end of file diff --git a/src/api/java/SimplifierDecRefQueue.java b/src/api/java/SimplifierDecRefQueue.java new file mode 100644 index 000000000..ba15dd5be --- /dev/null +++ b/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 { + public SimplifierDecRefQueue() + { + super(); + } + + @Override + protected void decRef(Context ctx, long obj) + { + Native.simplifierDecRef(ctx.nCtx(), obj); + } +}