Skip to content

LASolver: Small refactoring #827

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
blishko merged 2 commits into from
Mar 25, 2025
Merged

LASolver: Small refactoring #827

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2c1c249
LASolver: Small refactoring
blishko Feb 27, 2025
cbde920
LASolver: Skip redundant check
blishko Feb 27, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 9 additions & 24 deletions src/tsolvers/lasolver/LASolver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ void LASolver::addBound(PTRef leq_tr) {
LABoundRefPair boundRefs = [this, leq_tr]() -> LABoundRefPair {
auto [const_tr, sum_tr] = logic.leqToConstantAndTerm(leq_tr);
assert(logic.isNumConst(const_tr) && logic.isLinearTerm(sum_tr));
LVRef const v = laVarMapper.getVarByPTId(logic.getPterm(sum_tr).getId());
LVRef const v = getVarForTerm(sum_tr);
bool const isNegated = laVarMapper.isNegated(sum_tr);
auto values = isNegated ? getBoundsValue(v, -logic.getNumConst(const_tr), false)
: getBoundsValue(v, logic.getNumConst(const_tr), true);
Expand All @@ -38,6 +38,8 @@ void LASolver::addBound(PTRef leq_tr) {
}();

int const tid = Idx(logic.getPterm(leq_tr).getId());
// Must be a new inequality
assert(tid >= LeqToLABoundRefPair.size() or (LeqToLABoundRefPair[tid] == LABoundRefPair{LABoundRef_Undef, LABoundRef_Undef}));
if (LeqToLABoundRefPair.size() <= tid) {
LeqToLABoundRefPair.growTo(tid + 1);
Copy link
Copy Markdown
Member

@Tomaqa Tomaqa Mar 24, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess we already discussed this: Is it not performance bottleneck?

Copy link
Copy Markdown
Member Author

@blishko blishko Mar 25, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not for OpenSMT.
I am hitting this in Golem on a few occasions, but I think I can try some workaround on the model checker level.

Note also that we tried using maps in the past (#500), but there was a few percent performance hit for OpenSMT on SMT-LIB benchmarks.

}
Expand All @@ -52,18 +54,6 @@ void LASolver::addBound(PTRef leq_tr) {
LABoundRefToLeqAsgn[br_neg_idx] = PtAsgn(leq_tr, l_False);
}

void LASolver::updateBound(PTRef tr)
{
// If the bound already exists, do nothing.
int id = Idx(logic.getPterm(tr).getId());

if ((LeqToLABoundRefPair.size() > id) &&
!(LeqToLABoundRefPair[id] == LABoundRefPair{LABoundRef_Undef, LABoundRef_Undef})) {
return;
}
addBound(tr);
}

bool LASolver::isValid(PTRef tr)
{
return logic.isLeq(tr); // MB: LA solver expects only inequalities in LEQ form!
Expand Down Expand Up @@ -182,15 +172,12 @@ void LASolver::markVarAsInt(LVRef v) {
LVRef LASolver::getVarForLeq(PTRef ref) const {
assert(logic.isLeq(ref));
auto [constant, term] = logic.leqToConstantAndTerm(ref);
return laVarMapper.getVarByPTId(logic.getPterm(term).getId());
return getVarForTerm(term);
}

LVRef LASolver::getLAVar_single(PTRef expr_in) {

assert(logic.isLinearTerm(expr_in));
PTId id = logic.getPterm(expr_in).getId();

if (laVarMapper.hasVar(id)) {
if (laVarMapper.hasVar(expr_in)) {
return getVarForTerm(expr_in);
}

Expand Down Expand Up @@ -281,12 +268,10 @@ void LASolver::declareAtom(PTRef leq_tr)

if (status != INIT)
{
// Treat the PTRef as it is pushed on-the-fly
// status = INCREMENT;
assert( status == SAT );
assert(status == SAT);
PTRef term = logic.getPterm(leq_tr)[1];
registerArithmeticTerm(term);
updateBound(leq_tr);
addBound(leq_tr);
}
// DEBUG check
isProperLeq(leq_tr);
Expand Down Expand Up @@ -877,7 +862,7 @@ TRes LASolver::cutFromProof() {
}
auto getVarValue = [this](PTRef var) {
assert(this->logic.isVar(var));
LVRef lvar = this->laVarMapper.getVarByPTId(logic.getPterm(var).getId());
LVRef lvar = this->getVarForTerm(var);
Delta val = this->simplex.getValuation(lvar);
assert(not val.hasDelta());
return val.R();
Expand Down Expand Up @@ -912,7 +897,7 @@ vec<PTRef> LASolver::collectEqualitiesFor(vec<PTRef> const & vars, std::unordere
if (not laVarMapper.hasVar(var)) { // LASolver does not have any constraints on this LA var
continue;
}
LVRef v = laVarMapper.getVarByPTId(logic.getPterm(var).getId());
LVRef v = getVarForTerm(var);
auto value = simplex.getValuation(v);
eqClasses[value].push(var);
}
Expand Down
3 changes: 1 addition & 2 deletions src/tsolvers/lasolver/LASolver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,6 @@ class LASolver : public TSolver {
PTRef getVarPTRef(LVRef v) const { return laVarMapper.getVarPTRef(v); }

void addBound(PTRef leq_tr);
void updateBound(PTRef leq_tr);
LVRef registerArithmeticTerm(PTRef expr); // Ensures this term and all variables in it has corresponding LVAR.
// Returns the LAVar for the term.
void storeExplanation(Simplex::Explanation && explanationBounds);
Expand All @@ -118,7 +117,7 @@ class LASolver : public TSolver {

LVRef getLAVar_single(PTRef term); // Initialize a new LA var if needed, otherwise return the old var
LVRef getVarForLeq(PTRef ref) const;
LVRef getVarForTerm(PTRef ref) const { return laVarMapper.getVarByPTId(logic.getPterm(ref).getId()); }
LVRef getVarForTerm(PTRef ref) const { return laVarMapper.getVar(ref); }
void notifyVar(LVRef); // Notify the solver of the existence of the var. This is so that LIA can add it to
// integer vars list.

Expand Down
5 changes: 2 additions & 3 deletions src/tsolvers/lasolver/LAVarMapper.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ void LAVarMapper::registerNewMapping(LVRef lv, PTRef e_orig) {

PTId id_pos = logic.getPterm(e_orig).getId();
PTId id_neg = logic.getPterm(logic.mkNeg(e_orig)).getId();
assert(!hasVar(id_pos));
Comment thread
Tomaqa marked this conversation as resolved.
int max_id = std::max(Idx(id_pos), Idx(id_neg));

if (max_id >= ptermToLavar.size()) {
Expand All @@ -43,11 +42,11 @@ void LAVarMapper::registerNewMapping(LVRef lv, PTRef e_orig) {
ptermToLavar[Idx(id_neg)] = lv;
}

LVRef LAVarMapper::getVarByPTId(PTId i) const { return ptermToLavar[Idx(i)]; }
LVRef LAVarMapper::getVar(PTRef tr) const { return ptermToLavar[Idx(logic.getPterm(tr).getId())]; }

bool LAVarMapper::hasVar(PTRef tr) const { return hasVar(logic.getPterm(tr).getId()); }

bool LAVarMapper::hasVar(PTId i) const {
bool LAVarMapper::hasVar(PTId i) const {
return static_cast<unsigned int>(ptermToLavar.size()) > Idx(i) && ptermToLavar[Idx(i)] != LVRef::Undef;
}

Expand Down
23 changes: 13 additions & 10 deletions src/tsolvers/lasolver/LAVarMapper.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,29 +28,32 @@ class ArithLogic;
* instead of forcing to isolate the term from the constant and normalize it.
*/
class LAVarMapper {
private:
/** Mapping of linear Pterms to LVRefs */
vec<LVRef> ptermToLavar;

/** The inverse of ptermToLavar, mapping LVRefs to PTRefs */
vec<PTRef> laVarToPTRef;

ArithLogic& logic;
public:
LAVarMapper(ArithLogic &logic) : logic(logic) {}

void registerNewMapping(LVRef lv, PTRef e_orig);

LVRef getVarByPTId(PTId i) const;
LVRef getVar(PTRef tr) const;

bool hasVar(PTId i) const;
bool hasVar(PTRef tr) const;

inline PTRef getVarPTRef(LVRef ref) const { return laVarToPTRef[ref.x]; }

void clear();

bool isNegated(PTRef tr) const;

private:
bool hasVar(PTId i) const;

/** Mapping of linear Pterms to LVRefs */
vec<LVRef> ptermToLavar;

/** The inverse of ptermToLavar, mapping LVRefs to PTRefs */
vec<PTRef> laVarToPTRef;

ArithLogic& logic;

};

}
Expand Down