mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
more stubs #6097
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7963ecaf63
commit
b93529997e
1 changed files with 55 additions and 0 deletions
55
src/api/java/UserPropagator.java
Normal file
55
src/api/java/UserPropagator.java
Normal file
|
@ -0,0 +1,55 @@
|
|||
/**
|
||||
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…
Add table
Add a link
Reference in a new issue