mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	Made DRQ objects public in Java and .NET APIs.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
		
							parent
							
								
									07c945718b
								
							
						
					
					
						commit
						4bed5183f8
					
				
					 32 changed files with 182 additions and 109 deletions
				
			
		| 
						 | 
				
			
			@ -229,7 +229,7 @@ public class AST extends Z3Object
 | 
			
		|||
        // Console.WriteLine("AST IncRef()");
 | 
			
		||||
        if (getContext() == null || o == 0)
 | 
			
		||||
            return;
 | 
			
		||||
        getContext().ast_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getASTDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -238,7 +238,7 @@ public class AST extends Z3Object
 | 
			
		|||
        // Console.WriteLine("AST DecRef()");
 | 
			
		||||
        if (getContext() == null || o == 0)
 | 
			
		||||
            return;
 | 
			
		||||
        getContext().ast_DRQ().add(o);
 | 
			
		||||
        getContext().getASTDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -124,13 +124,13 @@ class ASTMap extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().astmap_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getASTMapDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().astmap_DRQ().add(o);
 | 
			
		||||
        getContext().getASTMapDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -110,13 +110,13 @@ class ASTVector extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().astvector_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getASTVectorDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().astvector_DRQ().add(o);
 | 
			
		||||
        getContext().getASTVectorDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -81,13 +81,13 @@ public class ApplyResult extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().applyResult_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getApplyResultDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().applyResult_DRQ().add(o);
 | 
			
		||||
        getContext().getApplyResultDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -3674,77 +3674,77 @@ public class Context extends IDisposable
 | 
			
		|||
    private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10);
 | 
			
		||||
    private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10);
 | 
			
		||||
 | 
			
		||||
    ASTDecRefQueue ast_DRQ()
 | 
			
		||||
    public IDecRefQueue getASTDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_AST_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    ASTMapDecRefQueue astmap_DRQ()
 | 
			
		||||
    public IDecRefQueue getASTMapDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_ASTMap_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    ASTVectorDecRefQueue astvector_DRQ()
 | 
			
		||||
    public IDecRefQueue getASTVectorDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_ASTVector_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    ApplyResultDecRefQueue applyResult_DRQ()
 | 
			
		||||
    public IDecRefQueue getApplyResultDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_ApplyResult_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    FuncInterpEntryDecRefQueue funcEntry_DRQ()
 | 
			
		||||
    public IDecRefQueue getFuncEntryDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_FuncEntry_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    FuncInterpDecRefQueue funcInterp_DRQ()
 | 
			
		||||
    public IDecRefQueue getFuncInterpDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_FuncInterp_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    GoalDecRefQueue goal_DRQ()
 | 
			
		||||
    public IDecRefQueue getGoalDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_Goal_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    ModelDecRefQueue model_DRQ()
 | 
			
		||||
    public IDecRefQueue getModelDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_Model_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    ParamsDecRefQueue params_DRQ()
 | 
			
		||||
    public IDecRefQueue getParamsDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_Params_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    ParamDescrsDecRefQueue paramDescrs_DRQ()
 | 
			
		||||
    public IDecRefQueue getParamDescrsDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_ParamDescrs_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    ProbeDecRefQueue probe_DRQ()
 | 
			
		||||
    public IDecRefQueue getProbeDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_Probe_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    SolverDecRefQueue solver_DRQ()
 | 
			
		||||
    public IDecRefQueue getSolverDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_Solver_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    StatisticsDecRefQueue statistics_DRQ()
 | 
			
		||||
    public IDecRefQueue getStatisticsDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_Statistics_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    TacticDecRefQueue tactic_DRQ()
 | 
			
		||||
    public IDecRefQueue getTacticDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_Tactic_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    FixedpointDecRefQueue fixedpoint_DRQ()
 | 
			
		||||
    public IDecRefQueue getFixedpointDRQ()
 | 
			
		||||
    {
 | 
			
		||||
        return m_Fixedpoint_DRQ;
 | 
			
		||||
    }
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -334,13 +334,13 @@ public class Fixedpoint extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().fixedpoint_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getFixedpointDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().fixedpoint_DRQ().add(o);
 | 
			
		||||
        getContext().getFixedpointDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -93,13 +93,13 @@ public class FuncInterp extends Z3Object
 | 
			
		|||
 | 
			
		||||
        void incRef(long o) throws Z3Exception
 | 
			
		||||
        {
 | 
			
		||||
            getContext().funcEntry_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
            getContext().getFuncEntryDRQ().incAndClear(getContext(), o);
 | 
			
		||||
            super.incRef(o);
 | 
			
		||||
        }
 | 
			
		||||
 | 
			
		||||
        void decRef(long o) throws Z3Exception
 | 
			
		||||
        {
 | 
			
		||||
            getContext().funcEntry_DRQ().add(o);
 | 
			
		||||
            getContext().getFuncEntryDRQ().add(o);
 | 
			
		||||
            super.decRef(o);
 | 
			
		||||
        }
 | 
			
		||||
    };
 | 
			
		||||
| 
						 | 
				
			
			@ -194,13 +194,13 @@ public class FuncInterp extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().funcInterp_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getFuncInterpDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().funcInterp_DRQ().add(o);
 | 
			
		||||
        getContext().getFuncInterpDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -236,13 +236,13 @@ public class Goal extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().goal_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getGoalDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().goal_DRQ().add(o);
 | 
			
		||||
        getContext().getGoalDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -19,22 +19,24 @@ package com.microsoft.z3;
 | 
			
		|||
 | 
			
		||||
import java.util.LinkedList;
 | 
			
		||||
 | 
			
		||||
abstract class IDecRefQueue
 | 
			
		||||
public abstract class IDecRefQueue
 | 
			
		||||
{
 | 
			
		||||
    protected Object m_lock = new Object();
 | 
			
		||||
    protected LinkedList<Long> m_queue = new LinkedList<Long>();
 | 
			
		||||
    protected int m_move_limit;
 | 
			
		||||
 | 
			
		||||
    public IDecRefQueue() 
 | 
			
		||||
    {
 | 
			
		||||
    m_move_limit = 1024;
 | 
			
		||||
    protected IDecRefQueue() 
 | 
			
		||||
	{
 | 
			
		||||
    	m_move_limit = 1024;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    public IDecRefQueue(int move_limit) 
 | 
			
		||||
    protected IDecRefQueue(int move_limit) 
 | 
			
		||||
    {
 | 
			
		||||
    m_move_limit = move_limit;
 | 
			
		||||
    	m_move_limit = move_limit;
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
 
 | 
			
		||||
    public void setLimit(int l) { m_move_limit = l; }
 | 
			
		||||
 
 | 
			
		||||
    protected abstract void incRef(Context ctx, long obj);
 | 
			
		||||
 | 
			
		||||
    protected abstract void decRef(Context ctx, long obj);
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -303,13 +303,13 @@ public class Model extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().model_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getModelDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().model_DRQ().add(o);
 | 
			
		||||
        getContext().getModelDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -90,13 +90,13 @@ public class ParamDescrs extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().paramDescrs_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getParamDescrsDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().paramDescrs_DRQ().add(o);
 | 
			
		||||
        getContext().getParamDescrsDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -130,13 +130,13 @@ public class Params extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().params_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getParamsDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().params_DRQ().add(o);
 | 
			
		||||
        getContext().getParamsDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -53,13 +53,13 @@ public class Probe extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().probe_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getProbeDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().probe_DRQ().add(o);
 | 
			
		||||
        getContext().getProbeDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -337,13 +337,13 @@ public class Solver extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().solver_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getSolverDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().solver_DRQ().add(o);
 | 
			
		||||
        getContext().getSolverDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -199,13 +199,13 @@ public class Statistics extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().statistics_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getStatisticsDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().statistics_DRQ().add(o);
 | 
			
		||||
        getContext().getStatisticsDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -94,13 +94,13 @@ public class Tactic extends Z3Object
 | 
			
		|||
 | 
			
		||||
    void incRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().tactic_DRQ().incAndClear(getContext(), o);
 | 
			
		||||
        getContext().getTacticDRQ().incAndClear(getContext(), o);
 | 
			
		||||
        super.incRef(o);
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    void decRef(long o) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        getContext().tactic_DRQ().add(o);
 | 
			
		||||
        getContext().getTacticDRQ().add(o);
 | 
			
		||||
        super.decRef(o);
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue