diff options
Diffstat (limited to 'src/theory/arith/nl/cad/cdcac.h')
| -rw-r--r-- | src/theory/arith/nl/cad/cdcac.h | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index bd64a9ceb..3434b23e6 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -58,6 +58,14 @@ class CDCAC void computeVariableOrdering(); /** + * Extract an initial assignment from the given model. + * This initial assignment is used to guide sampling if possible. + * The ran_variable should be the variable used to encode real algebraic + * numbers in the model and is simply passed on to node_to_value. + */ + void retrieveInitialAssignment(NlModel& model, const Node& ran_variable); + + /** * Returns the constraints as a non-const reference. Can be used to add new * constraints. */ @@ -82,6 +90,16 @@ class CDCAC std::vector<CACInterval> getUnsatIntervals(std::size_t cur_variable) const; /** + * Sample outside of the set of intervals. + * Uses a given initial value from mInitialAssignment if possible. + * Returns whether a sample was found (true) or the infeasible intervals cover + * the whole real line (false). + */ + bool sampleOutsideWithInitial(const std::vector<CACInterval>& infeasible, + poly::Value& sample, + std::size_t cur_variable); + + /** * Collects the coefficients required for projection from the given * polynomial. Implements Algorithm 6. */ @@ -155,6 +173,9 @@ class CDCAC /** The object computing the variable ordering. */ VariableOrdering d_varOrder; + + /** The linear assignment used as an initial guess. */ + std::vector<poly::Value> d_initialAssignment; }; } // namespace cad |