diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-10-01 18:24:55 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-01 11:24:55 -0500 |
| commit | 25aaeabe85f8c3f2c6701fcd48f00f221f8dfccf (patch) | |
| tree | d05317d4f4aeae7b3f70ea250ca146b00112a1b3 /src/theory/arith/nl/cad_solver.cpp | |
| parent | 874350b54bd0f275fa8af7ca7a7af186bde7c030 (diff) | |
Allow to use the initial assignment for CAD (#5177)
While the CAD subsolver already provided for a way to use the linear model to seed the model search, it was not actually used yet.
This PR now does use it, though it is disabled by a Boolean flag.
Diffstat (limited to 'src/theory/arith/nl/cad_solver.cpp')
| -rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 6ae75a837..b63a8398c 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -59,6 +59,7 @@ void CadSolver::initLastCall(const std::vector<Node>& assertions) d_CAC.getConstraints().addConstraint(a); } d_CAC.computeVariableOrdering(); + d_CAC.retrieveInitialAssignment(d_model, d_ranVariable); #else Warning() << "Tried to use CadSolver but libpoly is not available. Compile " "with --poly." |