mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Merge pull request #1701 from agurfinkel/deep_space

Browse source 
Normalize lit0 in theory clause
This commit is contained in:
Nikolaj Bjorner 2018-06-25 07:35:34 -07:00 • committed by GitHub
commit 6804329661
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -285,6 +285,8 @@ namespace spacer {
unsigned num_params, unsigned num_params,
parameter const *params) { parameter const *params) {
SASSERT(num_params == parents.size() + 1 /* one param is missing */); SASSERT(num_params == parents.size() + 1 /* one param is missing */);
arith_util a(m);
th_rewriter rw(m);
// compute missing coefficient // compute missing coefficient
linear_combinator lcb(m); linear_combinator lcb(m);
@ -294,19 +296,22 @@ namespace spacer {
lcb.add_lit(p, r); lcb.add_lit(p, r);
} }
expr_ref lit0(m);
lit0 = m.get_fact(parents.get(0));
// put lit0 into canonical form
rw(lit0);
TRACE("spacer.fkab", TRACE("spacer.fkab",
tout << "lit0 is: " << mk_pp(m.get_fact(parents.get(0)), m) << "\n" tout << "lit0 is: " << lit0 << "\n"
<< "LCB is: " << lcb() << "\n";); << "LCB is: " << lcb() << "\n";);
expr_ref var(m), val1(m), val2(m); expr_ref var(m), val1(m), val2(m);
val1 = get_coeff(m.get_fact(parents.get(0)), var); val1 = get_coeff(lit0, var);
val2 = get_coeff(lcb(), var); val2 = get_coeff(lcb(), var);
TRACE("spacer.fkab", TRACE("spacer.fkab",
tout << "var: " << var tout << "var: " << var
<< " val1: " << val1 << " val2: " << val2 << "\n";); << " val1: " << val1 << " val2: " << val2 << "\n";);
rational rat1, rat2, coeff0; rational rat1, rat2, coeff0;
arith_util a(m);
CTRACE("spacer.fkab", !(val1 && val2), CTRACE("spacer.fkab", !(val1 && val2),
tout << "Failed to match variables\n";); tout << "Failed to match variables\n";);
if (val1 && val2 && if (val1 && val2 &&
@ -318,6 +323,7 @@ namespace spacer {
else { else {
IF_VERBOSE(1, verbose_stream() IF_VERBOSE(1, verbose_stream()
<< "\n\n\nFAILED TO FIND COEFFICIENT\n\n\n";); << "\n\n\nFAILED TO FIND COEFFICIENT\n\n\n";);
TRACE("spacer.fkab", tout << "FAILED TO FIND COEFFICIENT\n";);
// failed to find a coefficient // failed to find a coefficient
return proof_ref(m); return proof_ref(m);
} }