mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2023-03-13 07:37:17 +01:00
parent 233baf170c
commit 69fbfc3616
2 changed files with 20 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/math/polysat/polysat_ast.cpp
View file

@ -159,6 +159,20 @@ namespace polysat {
return b; return b;
} }
expr* polysat_ast::mk_op(op_constraint const& op, bool sign) {
expr* e = nullptr;
switch (op.get_op()) {
case op_constraint::code::inv_op:
e = mk_inv(op.p(), op.r());
break;
default:
return nullptr;
}
if (sign)
e = mk_not(e);
return e;
}
expr* polysat_ast::mk_not(expr* e) { expr* polysat_ast::mk_not(expr* e) {
return d->store(m().mk_not(e)); return d->store(m().mk_not(e));
} }
@ -193,15 +207,9 @@ namespace polysat {
return mk_ule(c->to_ule().lhs(), c->to_ule().rhs(), c.sign()); return mk_ule(c->to_ule().lhs(), c->to_ule().rhs(), c.sign());
if (c->is_umul_ovfl()) if (c->is_umul_ovfl())
return mk_umul_ovfl(c->to_umul_ovfl().p(), c->to_umul_ovfl().q(), c.sign()); return mk_umul_ovfl(c->to_umul_ovfl().p(), c->to_umul_ovfl().q(), c.sign());
if (c->is_op()) { if (c->is_op())
op_constraint& op = c->to_op(); if (expr* e = mk_op(c->to_op(), c.sign()))
switch (op.get_op()) { return e;
case op_constraint::code::inv_op:
return mk_inv(op.p(), op.r());
default:
break;
}
}
verbose_stream() << "polysat_ast not yet supported: " << c << "\n"; verbose_stream() << "polysat_ast not yet supported: " << c << "\n";
m_ok = false; m_ok = false;
// NOT_IMPLEMENTED_YET(); // NOT_IMPLEMENTED_YET();

4
src/math/polysat/polysat_ast.h
View file

@ -13,6 +13,7 @@ Author:
--*/ --*/
#pragma once #pragma once
#include "math/polysat/types.h" #include "math/polysat/types.h"
#include "math/polysat/constraint.h"
class expr; class expr;
class ast_manager; class ast_manager;
@ -21,7 +22,6 @@ class bv_util;
namespace polysat { namespace polysat {
struct polysat_ast_d; struct polysat_ast_d;
class signed_constraint;
class polysat_ast { class polysat_ast {
solver& s; solver& s;
@ -67,6 +67,8 @@ namespace polysat {
// p_inv = pseudo-inverse(p) // p_inv = pseudo-inverse(p)
expr* mk_inv(pdd const& p, pdd const& p_inv); expr* mk_inv(pdd const& p, pdd const& p_inv);
expr* mk_op(op_constraint const& op, bool sign);
expr* mk_not(expr* e); expr* mk_not(expr* e);
expr* mk_lit(sat::literal lit); expr* mk_lit(sat::literal lit);