mirror of
https://github.com/Z3Prover/z3
synced 2025-10-09 09:21:56 +00:00
detangle mess
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
3c38ee2690
commit
1582e4616e
3 changed files with 145 additions and 71 deletions
84
.clang-format
Normal file
84
.clang-format
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
|
||||
# Z3 Theorem Prover clang-format configuration
|
||||
# Based on analysis of existing codebase style patterns
|
||||
|
||||
BasedOnStyle: LLVM
|
||||
|
||||
# Indentation
|
||||
IndentWidth: 4
|
||||
TabWidth: 4
|
||||
UseTab: Never
|
||||
|
||||
# Column width
|
||||
ColumnLimit: 120
|
||||
|
||||
# Braces
|
||||
Cpp11BracedListStyle: true
|
||||
|
||||
# Classes and structs
|
||||
BreakConstructorInitializers: BeforeColon
|
||||
ConstructorInitializerIndentWidth: 4
|
||||
AccessModifierOffset: -4
|
||||
|
||||
# Function definitions
|
||||
AlwaysBreakAfterReturnType: None
|
||||
AllowShortFunctionsOnASingleLine: Empty
|
||||
AllowShortIfStatementsOnASingleLine: false
|
||||
AllowShortLoopsOnASingleLine: false
|
||||
# Ensure function-opening brace is attached to the signature
|
||||
BreakBeforeBraces: Custom
|
||||
# Explicitly ensure function brace is not placed on a new line
|
||||
BraceWrapping:
|
||||
AfterFunction: false
|
||||
AfterClass: false
|
||||
AfterControlStatement: false
|
||||
AfterNamespace: false
|
||||
AfterStruct: false
|
||||
# Spacing
|
||||
SpaceAfterCStyleCast: false
|
||||
SpaceAfterLogicalNot: false
|
||||
SpaceBeforeParens: ControlStatements
|
||||
SpaceInEmptyParentheses: false
|
||||
SpacesInCStyleCastParentheses: false
|
||||
SpacesInParentheses: false
|
||||
SpacesInSquareBrackets: false
|
||||
IndentCaseLabels: false
|
||||
|
||||
# Alignment
|
||||
AlignConsecutiveAssignments: false
|
||||
AlignConsecutiveDeclarations: false
|
||||
AlignOperands: true
|
||||
AlignTrailingComments: true
|
||||
|
||||
# Line breaks
|
||||
AllowAllParametersOfDeclarationOnNextLine: true
|
||||
BinPackArguments: true
|
||||
BinPackParameters: true
|
||||
BreakBeforeBinaryOperators: None
|
||||
BreakBeforeTernaryOperators: true
|
||||
|
||||
# Includes
|
||||
SortIncludes: false # Z3 has specific include ordering conventions
|
||||
|
||||
# Namespaces
|
||||
NamespaceIndentation: All
|
||||
|
||||
# Comments and documentation
|
||||
ReflowComments: true
|
||||
SpacesBeforeTrailingComments: 2
|
||||
|
||||
# Language standards
|
||||
Standard: c++20
|
||||
|
||||
# Penalties (for line breaking decisions)
|
||||
PenaltyBreakAssignment: 2
|
||||
PenaltyBreakBeforeFirstCallParameter: 19
|
||||
PenaltyBreakComment: 300
|
||||
PenaltyBreakFirstLessLess: 120
|
||||
PenaltyBreakString: 1000
|
||||
PenaltyExcessCharacter: 1000000
|
||||
PenaltyReturnTypeOnItsOwnLine: 60
|
||||
|
||||
# Misc
|
||||
KeepEmptyLinesAtTheStartOfBlocks: false
|
||||
MaxEmptyLinesToKeep: 1
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
BasedOnStyle: Google
|
||||
IndentWidth: 4
|
||||
ColumnLimit: 0
|
||||
NamespaceIndentation: All
|
||||
BreakBeforeBraces: Attach
|
||||
|
|
@ -320,11 +320,12 @@ struct solver::imp {
|
|||
}
|
||||
|
||||
lbool check_assignment() {
|
||||
IF_VERBOSE(1, verbose_stream() << "nra::solver::check_assignment\n";);
|
||||
setup_solver();
|
||||
lbool r = l_undef;
|
||||
statistics& st = m_nla_core.lp_settings().stats().m_st;
|
||||
statistics &st = m_nla_core.lp_settings().stats().m_st;
|
||||
nlsat::literal_vector clause;
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
polynomial::manager &pm = m_nlsat->pm();
|
||||
try {
|
||||
nlsat::assignment rvalues(m_nlsat->am());
|
||||
for (auto [j, x] : m_lp2nl) {
|
||||
|
|
@ -334,7 +335,7 @@ struct solver::imp {
|
|||
}
|
||||
r = m_nlsat->check(rvalues, clause);
|
||||
}
|
||||
catch (z3_exception&) {
|
||||
catch (z3_exception &) {
|
||||
if (m_limit.is_canceled()) {
|
||||
r = l_undef;
|
||||
}
|
||||
|
|
@ -344,73 +345,67 @@ struct solver::imp {
|
|||
}
|
||||
}
|
||||
m_nlsat->collect_statistics(st);
|
||||
TRACE(nra,
|
||||
m_nlsat->display(tout << r << "\n");
|
||||
display(tout);
|
||||
tout << "m_lp2nl:\n";
|
||||
TRACE(nra, m_nlsat->display(tout << r << "\n"); display(tout); tout << "m_lp2nl:\n";
|
||||
for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";);
|
||||
switch (r) {
|
||||
case l_true:
|
||||
m_nla_core.set_use_nra_model(true);
|
||||
lra.init_model();
|
||||
validate_constraints();
|
||||
break;
|
||||
case l_false: {
|
||||
u_map<lp::lpvar> nl2lp = reverse_lp2nl();
|
||||
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
|
||||
for (nlsat::literal l : clause) {
|
||||
nlsat::atom* a = m_nlsat->bool_var2atom(l.var());
|
||||
TRACE(nra, tout << "atom: "; m_nlsat->display(tout, *a); tout << "\n";);
|
||||
SASSERT(!a->is_root_atom());
|
||||
SASSERT(a->is_ineq_atom());
|
||||
auto& ia = *to_ineq_atom(a);
|
||||
VERIFY(ia.size() == 1); // deal with factored polynomials later
|
||||
// a is an inequality atom, i.e., p > 0, p < 0, or p = 0.
|
||||
polynomial::polynomial const* p = ia.p(0);
|
||||
TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";);
|
||||
unsigned num_mon = pm.size(p);
|
||||
rational bound(0);
|
||||
lp::lar_term t;
|
||||
process_polynomial_check_assignment(num_mon, p, bound, nl2lp, t);
|
||||
|
||||
switch (a->get_kind()) {
|
||||
{
|
||||
// Introduce a single ineq variable and assign it per case; common handling after switch.
|
||||
nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below
|
||||
switch (a->get_kind()) {
|
||||
case nlsat::atom::EQ:
|
||||
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound);
|
||||
break;
|
||||
case nlsat::atom::LT:
|
||||
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound);
|
||||
break;
|
||||
case nlsat::atom::GT:
|
||||
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return l_undef;
|
||||
}
|
||||
if (m_nla_core.ineq_holds(inq))
|
||||
return l_undef;
|
||||
lemma |= inq;
|
||||
}
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return l_undef;
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
|
||||
m_nla_core.set_use_nra_model(true);
|
||||
break;
|
||||
}
|
||||
case l_undef:
|
||||
break;
|
||||
case l_true:
|
||||
m_nla_core.set_use_nra_model(true);
|
||||
lra.init_model();
|
||||
validate_constraints();
|
||||
m_nla_core.set_use_nra_model(true);
|
||||
break;
|
||||
case l_false:
|
||||
return add_lemma(clause);
|
||||
default:
|
||||
break;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool add_lemma(nlsat::literal_vector const &clause) {
|
||||
u_map<lp::lpvar> nl2lp = reverse_lp2nl();
|
||||
polynomial::manager &pm = m_nlsat->pm();
|
||||
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
|
||||
for (nlsat::literal l : clause) {
|
||||
nlsat::atom *a = m_nlsat->bool_var2atom(l.var());
|
||||
TRACE(nra, tout << "atom: "; m_nlsat->display(tout, *a); tout << "\n";);
|
||||
SASSERT(!a->is_root_atom());
|
||||
SASSERT(a->is_ineq_atom());
|
||||
auto &ia = *to_ineq_atom(a);
|
||||
VERIFY(ia.size() == 1); // deal with factored polynomials later
|
||||
// a is an inequality atom, i.e., p > 0, p < 0, or p = 0.
|
||||
polynomial::polynomial const *p = ia.p(0);
|
||||
TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";);
|
||||
unsigned num_mon = pm.size(p);
|
||||
rational bound(0);
|
||||
lp::lar_term t;
|
||||
process_polynomial_check_assignment(num_mon, p, bound, nl2lp, t);
|
||||
|
||||
// Introduce a single ineq variable and assign it per case; common handling after switch.
|
||||
nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below
|
||||
switch (a->get_kind()) {
|
||||
case nlsat::atom::EQ:
|
||||
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound);
|
||||
break;
|
||||
case nlsat::atom::LT:
|
||||
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound);
|
||||
break;
|
||||
case nlsat::atom::GT:
|
||||
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return l_undef;
|
||||
}
|
||||
// NSB review: what is this???
|
||||
if (m_nla_core.ineq_holds(inq))
|
||||
return l_undef;
|
||||
lemma |= inq;
|
||||
IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
|
||||
return l_false;
|
||||
}
|
||||
}
|
||||
|
||||
void constraint_core2ex(lp::explanation& ex) {
|
||||
vector<nlsat::assumption, false> core;
|
||||
m_nlsat->get_core(core);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue