Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Wrapper on linear solver
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/arith/linear/linear_solver.h"
      17                 :            : 
      18                 :            : #include "expr/attribute.h"
      19                 :            : #include "theory/arith/arith_rewriter.h"
      20                 :            : 
      21                 :            : namespace cvc5::internal {
      22                 :            : namespace theory {
      23                 :            : namespace arith::linear {
      24                 :            : 
      25                 :      49907 : LinearSolver::LinearSolver(Env& env,
      26                 :            :                            TheoryState& ts,
      27                 :            :                            InferenceManager& im,
      28                 :      49907 :                            BranchAndBound& bab)
      29                 :      49907 :     : EnvObj(env), d_im(im), d_internal(env, *this, ts, bab)
      30                 :            : {
      31                 :      49907 : }
      32                 :            : 
      33                 :      49907 : void LinearSolver::finishInit(eq::EqualityEngine* ee)
      34                 :            : {
      35                 :      49907 :   d_internal.finishInit(ee);
      36                 :      49907 : }
      37                 :    1719541 : void LinearSolver::preRegisterTerm(TNode n) { d_internal.preRegisterTerm(n); }
      38                 :    5382631 : void LinearSolver::propagate() { d_internal.propagate(); }
      39                 :            : 
      40                 :      16139 : TrustNode LinearSolver::explain(TNode n) { return d_internal.explain(n); }
      41                 :            : 
      42                 :     138308 : void LinearSolver::collectModelValues(const std::set<Node>& termSet,
      43                 :            :                                       std::map<Node, Node>& arithModel,
      44                 :            :                                       std::map<Node, Node>& arithModelIllTyped)
      45                 :            : {
      46                 :     138308 :   d_internal.collectModelValues(termSet, arithModel, arithModelIllTyped);
      47                 :     138308 : }
      48                 :            : 
      49                 :      49334 : void LinearSolver::presolve() { d_internal.presolve(); }
      50                 :            : 
      51                 :       3187 : void LinearSolver::notifyRestart() { d_internal.notifyRestart(); }
      52                 :            : 
      53                 :      55036 : bool LinearSolver::ppAssert(TrustNode tin,
      54                 :            :                             TrustSubstitutionMap& outSubstitutions)
      55                 :            : {
      56                 :      55036 :   return d_internal.ppAssert(tin, outSubstitutions);
      57                 :            : }
      58                 :     341338 : void LinearSolver::ppStaticLearn(TNode in, std::vector<TrustNode>& learned)
      59                 :            : {
      60                 :     341338 :   d_internal.ppStaticLearn(in, learned);
      61                 :     341338 : }
      62                 :          0 : EqualityStatus LinearSolver::getEqualityStatus(TNode a, TNode b)
      63                 :            : {
      64                 :          0 :   return d_internal.getEqualityStatus(a, b);
      65                 :            : }
      66                 :    1113048 : void LinearSolver::notifySharedTerm(TNode n) { d_internal.notifySharedTerm(n); }
      67                 :        677 : Node LinearSolver::getCandidateModelValue(TNode var)
      68                 :            : {
      69                 :        677 :   return d_internal.getCandidateModelValue(var);
      70                 :            : }
      71                 :      11382 : std::pair<bool, Node> LinearSolver::entailmentCheck(TNode lit)
      72                 :            : {
      73                 :      11382 :   return d_internal.entailmentCheck(lit);
      74                 :            : }
      75                 :    3320586 : bool LinearSolver::preCheck(bool newFacts)
      76                 :            : {
      77                 :    3320586 :   return d_internal.preCheck(newFacts);
      78                 :            : }
      79                 :   11534053 : void LinearSolver::preNotifyFact(TNode fact) { d_internal.preNotifyFact(fact); }
      80                 :    3320586 : bool LinearSolver::postCheck(Theory::Effort level)
      81                 :            : {
      82                 :    3320586 :   return d_internal.postCheck(level);
      83                 :            : }
      84                 :      59100 : bool LinearSolver::foundNonlinear() const
      85                 :            : {
      86                 :      59100 :   return d_internal.foundNonlinear();
      87                 :            : }
      88                 :      49907 : ArithCongruenceManager* LinearSolver::getCongruenceManager()
      89                 :            : {
      90                 :      49907 :   return d_internal.getCongruenceManager();
      91                 :            : }
      92                 :            : 
      93                 :     283388 : bool LinearSolver::outputTrustedLemma(TrustNode lemma, InferenceId id)
      94                 :            : {
      95                 :     283388 :   return d_im.trustedLemma(lemma, id);
      96                 :            : }
      97                 :            : 
      98                 :     122080 : void LinearSolver::outputTrustedConflict(TrustNode conf, InferenceId id)
      99                 :            : {
     100                 :     122080 :   d_im.trustedConflict(conf, id);
     101                 :     122080 : }
     102                 :            : 
     103                 :    2494025 : void LinearSolver::outputPropagate(TNode lit) { d_im.propagateLit(lit); }
     104                 :            : 
     105                 :     361993 : void LinearSolver::spendResource(Resource r) { d_im.spendResource(r); }
     106                 :            : 
     107                 :            : }  // namespace arith::linear
     108                 :            : }  // namespace theory
     109                 :            : }  // namespace cvc5::internal