mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
remove stub class, it may as well go into NativeStatic.txt as C++
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b93529997e
commit
2c21072c99
|
@ -179,7 +179,6 @@ set(Z3_JAVA_JAR_SOURCE_FILES
|
|||
Tactic.java
|
||||
TupleSort.java
|
||||
UninterpretedSort.java
|
||||
UserPropagator.java
|
||||
Version.java
|
||||
Z3Exception.java
|
||||
Z3Object.java
|
||||
|
|
|
@ -1,55 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2023 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
UserPropagator.java
|
||||
|
||||
Abstract:
|
||||
|
||||
User Propagator plugin
|
||||
|
||||
**/
|
||||
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import com.microsoft.z3.enumerations.Z3_lbool;
|
||||
import java.util.*;
|
||||
|
||||
/**
|
||||
* User Propagator
|
||||
**/
|
||||
@SuppressWarnings("unchecked")
|
||||
public class UserPropagator implements AutoCloseable {
|
||||
|
||||
Solver solver;
|
||||
Context ctx;
|
||||
|
||||
/**
|
||||
* Create a UserPropagator from a solver.
|
||||
**/
|
||||
public UserPropagator(Solver s)
|
||||
{
|
||||
this.solver = s;
|
||||
}
|
||||
|
||||
/**
|
||||
* Create a UserPropagator from a context.
|
||||
**/
|
||||
public UserPropagator(Context _ctx)
|
||||
{
|
||||
this.ctx = _ctx;
|
||||
}
|
||||
|
||||
/**
|
||||
* Disposes of the propagator.
|
||||
**/
|
||||
@Override
|
||||
public void close()
|
||||
{
|
||||
this.solver = null;
|
||||
this.ctx = null;
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in a new issue