For some reason, the nl subsolver for IAND did not annotate its lemmas with `Inference` types yet. This commit adds appropriate `Inference` values and makes the IAND solver use them.
Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE"
<< std::endl;
Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE"
<< std::endl;
+ lems.emplace_back(lem, Inference::IAND_INIT_REFINE);
Node lem = valueBasedLemma(i);
Trace("iand-lemma")
<< "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl;
Node lem = valueBasedLemma(i);
Trace("iand-lemma")
<< "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl;
+ lems.emplace_back(lem, Inference::IAND_VALUE_REFINE);
case Inference::T_MONOTONICITY: return "T_MONOTONICITY";
case Inference::T_SECANT: return "T_SECANT";
case Inference::T_TANGENT: return "T_TANGENT";
case Inference::T_MONOTONICITY: return "T_MONOTONICITY";
case Inference::T_SECANT: return "T_SECANT";
case Inference::T_TANGENT: return "T_TANGENT";
+ case Inference::IAND_INIT_REFINE: return "IAND_INIT_REFINE";
+ case Inference::IAND_VALUE_REFINE: return "IAND_VALUE_REFINE";
+ case Inference::CAD_CONFLICT: return "CAD_CONFLICT";
+ case Inference::CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL";
T_TANGENT,
// secant refinement, the dual of the above inference
T_SECANT,
T_TANGENT,
// secant refinement, the dual of the above inference
T_SECANT,
+ //-------------------- iand solver
+ // initial refinements (IAndSolver::checkInitialRefine)
+ IAND_INIT_REFINE,
+ // value refinements (IAndSolver::checkFullRefine)
+ IAND_VALUE_REFINE,
//-------------------- cad solver
// conflict / infeasible subset obtained from cad
CAD_CONFLICT,
//-------------------- cad solver
// conflict / infeasible subset obtained from cad
CAD_CONFLICT,