From b9c38b2a878841a1288b1e2279b1ecb74727eeab Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 27 Oct 2020 13:57:55 +0100 Subject: Enable --nl-cad by default (#5345) This PR enables `--nl-cad` for QF_NRA (and QF_UFNRA) by default to improve nonlinear arithmetic solving. Furthermore, it takes care of disabling it when libpoly is not available. It also adds a fix to the CadSolver that avoids incorrect SATs in the presence of theory combination. --- src/theory/arith/nl/cad_solver.cpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'src/theory/arith/nl/cad_solver.cpp') diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index b63a8398c..d12a861ac 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -18,6 +18,7 @@ #include #endif +#include "options/arith_options.h" #include "theory/arith/inference_id.h" #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/poly_conversion.h" @@ -145,10 +146,15 @@ bool CadSolver::constructModelIfAvailable(std::vector& assertions) { return false; } - assertions.clear(); + bool foundNonVariable = false; for (const auto& v : d_CAC.getVariableOrdering()) { Node variable = d_CAC.getConstraints().varMapper()(v); + if (!variable.isVar()) + { + Trace("nl-cad") << "Not a variable: " << variable << std::endl; + foundNonVariable = true; + } Node value = value_to_node(d_CAC.getModel().get(v), d_ranVariable); if (value.isConst()) { @@ -160,6 +166,16 @@ bool CadSolver::constructModelIfAvailable(std::vector& assertions) } Trace("nl-cad") << "-> " << v << " = " << value << std::endl; } + if (foundNonVariable) + { + Trace("nl-cad") + << "Some variable was an extended term, don't clear list of assertions." + << std::endl; + return false; + } + Trace("nl-cad") << "Constructed a full assignment, clear list of assertions." + << std::endl; + assertions.clear(); return true; #else Warning() << "Tried to use CadSolver but libpoly is not available. Compile " -- cgit v1.2.3