From ce9f176ea226940091975cb79652e65d4d23ec67 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Wed, 11 May 2022 14:32:45 +0200 Subject: [PATCH 1/6] LASolver: Remove redundant storage of information --- src/tsolvers/lasolver/LASolver.cc | 16 +++++++++------- src/tsolvers/lasolver/LASolver.h | 2 +- src/tsolvers/lasolver/LAVarMapper.cc | 14 -------------- src/tsolvers/lasolver/LAVarMapper.h | 6 ------ 4 files changed, 10 insertions(+), 28 deletions(-) diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 1f5d55f21..6e0b06dd9 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -29,8 +29,7 @@ LABoundStore::BoundInfo LASolver::addBound(PTRef leq_tr) { bool sum_term_is_negated = laVarMapper.isNegated(sum_tr); - LVRef v = laVarMapper.getVarByLeqId(logic.getPterm(leq_tr).getId()); - assert(v == laVarMapper.getVarByPTId(logic.getPterm(sum_tr).getId())); + LVRef v = laVarMapper.getVarByPTId(logic.getPterm(sum_tr).getId()); LABoundStore::BoundInfo bi; LABoundRef br_pos; @@ -242,6 +241,12 @@ bool LASolver::hasVar(PTRef expr) { return laVarMapper.hasVar(id); } +LVRef LASolver::getVarForLeq(PTRef ref) const { + assert(logic.isLeq(ref)); + auto [constant, term] = logic.leqToConstantAndTerm(ref); + return laVarMapper.getVarByPTId(logic.getPterm(term).getId()); +} + LVRef LASolver::getLAVar_single(PTRef expr_in) { assert(logic.isLinearTerm(expr_in)); @@ -340,8 +345,7 @@ void LASolver::declareAtom(PTRef leq_tr) // status = INCREMENT; assert( status == SAT ); PTRef term = logic.getPterm(leq_tr)[1]; - LVRef v = exprToLVar(term); - laVarMapper.addLeqVar(leq_tr, v); + exprToLVar(term); // MB: We need to build the representation, but we don't actually need the result updateBound(leq_tr); } // DEBUG check @@ -562,9 +566,7 @@ void LASolver::initSolver() PTRef term = leq_t[1]; // Ensure that all variables exists, build the polynomial, and update the occurrences. - LVRef v = exprToLVar(term); - - laVarMapper.addLeqVar(leq_tr, v); + exprToLVar(term); // MB: We need to build the representation, but we don't actually need the result // Assumes that the LRA variable has been already declared setBound(leq_tr); diff --git a/src/tsolvers/lasolver/LASolver.h b/src/tsolvers/lasolver/LASolver.h index e22944d20..6d6e2dfd0 100644 --- a/src/tsolvers/lasolver/LASolver.h +++ b/src/tsolvers/lasolver/LASolver.h @@ -148,7 +148,7 @@ class LASolver: public TSolver LVRef getLAVar_single(PTRef term); // Initialize a new LA var if needed, otherwise return the old var bool hasVar(PTRef expr); - LVRef getVarForLeq(PTRef ref) const { return laVarMapper.getVarByLeqId(logic.getPterm(ref).getId()); } + LVRef getVarForLeq(PTRef ref) const; LVRef getVarForTerm(PTRef ref) const { return laVarMapper.getVarByPTId(logic.getPterm(ref).getId()); } void notifyVar(LVRef); // Notify the solver of the existence of the var. This is so that LIA can add it to integer vars list. diff --git a/src/tsolvers/lasolver/LAVarMapper.cc b/src/tsolvers/lasolver/LAVarMapper.cc index 7e71bd9fb..552093e74 100644 --- a/src/tsolvers/lasolver/LAVarMapper.cc +++ b/src/tsolvers/lasolver/LAVarMapper.cc @@ -37,21 +37,8 @@ void LAVarMapper::registerNewMapping(LVRef lv, PTRef e_orig) { ptermToLavar[Idx(id_neg)] = lv; } -void LAVarMapper::addLeqVar(PTRef leq_tr, LVRef v) -{ - Pterm const & leq_t = logic.getPterm(leq_tr); - int idx = Idx(leq_t.getId()); - for (int i = leqToLavar.size(); i <= idx; i++) { - leqToLavar.push(LVRef::Undef); - } - assert(leqToLavar[idx] == LVRef::Undef); - leqToLavar[idx] = v; -} - LVRef LAVarMapper::getVarByPTId(PTId i) const { return ptermToLavar[Idx(i)]; } -LVRef LAVarMapper::getVarByLeqId(PTId i) const { return leqToLavar[Idx(i)]; } - bool LAVarMapper::hasVar(PTRef tr) const { return hasVar(logic.getPterm(tr).getId()); } bool LAVarMapper::hasVar(PTId i) const { @@ -77,7 +64,6 @@ bool LAVarMapper::isNegated(PTRef tr) const { } void LAVarMapper::clear() { - this->leqToLavar.clear(); this->laVarToPTRef.clear(); this->ptermToLavar.clear(); } diff --git a/src/tsolvers/lasolver/LAVarMapper.h b/src/tsolvers/lasolver/LAVarMapper.h index a590acca1..2470c7e79 100644 --- a/src/tsolvers/lasolver/LAVarMapper.h +++ b/src/tsolvers/lasolver/LAVarMapper.h @@ -24,9 +24,6 @@ class ArithLogic; */ class LAVarMapper { private: - /** Convenience mapping of inequalities to LVRef representing the linear term without constant in the inequality*/ - vec leqToLavar; - /** Mapping of linear Pterms to LVRefs */ vec ptermToLavar; @@ -39,10 +36,7 @@ class LAVarMapper { void registerNewMapping(LVRef lv, PTRef e_orig); - void addLeqVar(PTRef leq_tr, LVRef v); // Adds a binding from leq_tr to the "slack var" v - LVRef getVarByPTId(PTId i) const; - LVRef getVarByLeqId(PTId i) const; bool hasVar(PTId i) const; bool hasVar(PTRef tr) const; From d5e57ce2c07549615dd1a6dc04c42aac49ba08c2 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Wed, 11 May 2022 21:33:57 +0200 Subject: [PATCH 2/6] LASolver: Update license header --- src/tsolvers/lasolver/LAVarMapper.cc | 9 ++++++--- src/tsolvers/lasolver/LAVarMapper.h | 9 ++++++--- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/tsolvers/lasolver/LAVarMapper.cc b/src/tsolvers/lasolver/LAVarMapper.cc index 552093e74..8d7c64958 100644 --- a/src/tsolvers/lasolver/LAVarMapper.cc +++ b/src/tsolvers/lasolver/LAVarMapper.cc @@ -1,6 +1,9 @@ -// -// Created by prova on 06.09.19. -// +/* + * Copyright (c) 2019-2022, Antti Hyvarinen + * Copyright (c) 2019-2022, Martin Blicha + * + * SPDX-License-Identifier: MIT + */ #include "LAVarMapper.h" #include "ArithLogic.h" diff --git a/src/tsolvers/lasolver/LAVarMapper.h b/src/tsolvers/lasolver/LAVarMapper.h index 2470c7e79..8ebddeec4 100644 --- a/src/tsolvers/lasolver/LAVarMapper.h +++ b/src/tsolvers/lasolver/LAVarMapper.h @@ -1,6 +1,9 @@ -// -// Created by prova on 06.09.19. -// +/* + * Copyright (c) 2019-2022, Antti Hyvarinen + * Copyright (c) 2019-2022, Martin Blicha + * + * SPDX-License-Identifier: MIT + */ #ifndef OPENSMT_LAVARMAPPER_H #define OPENSMT_LAVARMAPPER_H From e49277138a5c456f88013baff5b3d38e8f4ca410 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Fri, 13 May 2022 11:09:17 +0200 Subject: [PATCH 3/6] Rename method for internalizing terms in LASolver --- src/tsolvers/lasolver/LASolver.cc | 12 +++++++----- src/tsolvers/lasolver/LASolver.h | 2 +- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 6e0b06dd9..d935847b3 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -279,8 +279,9 @@ std::unique_ptr LASolver::expressionToLVarPoly(PTRef term) // -// Get a possibly new LAVar for a PTRef term. We may assume that the term is of one of the following forms, -// where x is a real variable or ite, and p_i are products of a real variable or ite and a real constant +// Registers an arithmetic Pterm (polynomial) with the solver. +// We may assume that the term is of one of the following forms, +// where x is a variable or ite, and p_i are products of a variable or ite and a constant // // (1) x // (2a) (* x -1) @@ -289,7 +290,8 @@ std::unique_ptr LASolver::expressionToLVarPoly(PTRef term) // (4a) (* x -1) + p_1 + ... + p_n // (4b) (* -1 x) + p_1 + ... + p_n // -LVRef LASolver::exprToLVar(PTRef expr) { +// Returns internalized reference for the term +LVRef LASolver::registerArithmeticTerm(PTRef expr) { LVRef x = LVRef::Undef; if (laVarMapper.hasVar(expr)){ x = getVarForTerm(expr); @@ -345,7 +347,7 @@ void LASolver::declareAtom(PTRef leq_tr) // status = INCREMENT; assert( status == SAT ); PTRef term = logic.getPterm(leq_tr)[1]; - exprToLVar(term); // MB: We need to build the representation, but we don't actually need the result + registerArithmeticTerm(term); updateBound(leq_tr); } // DEBUG check @@ -566,7 +568,7 @@ void LASolver::initSolver() PTRef term = leq_t[1]; // Ensure that all variables exists, build the polynomial, and update the occurrences. - exprToLVar(term); // MB: We need to build the representation, but we don't actually need the result + registerArithmeticTerm(term); // Assumes that the LRA variable has been already declared setBound(leq_tr); diff --git a/src/tsolvers/lasolver/LASolver.h b/src/tsolvers/lasolver/LASolver.h index 6d6e2dfd0..43b9060ac 100644 --- a/src/tsolvers/lasolver/LASolver.h +++ b/src/tsolvers/lasolver/LASolver.h @@ -131,7 +131,7 @@ class LASolver: public TSolver LABoundStore::BoundInfo addBound(PTRef leq_tr); void updateBound(PTRef leq_tr); - LVRef exprToLVar(PTRef expr); // Ensures this term and all variables in it has corresponding LVAR. Returns the LAVar for the term. + 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); std::unique_ptr expressionToLVarPoly(PTRef term); From f47533be007aacdde84414d4e04b7ecaa5ab9d1f Mon Sep 17 00:00:00 2001 From: Antti Hyvarinen Date: Thu, 12 May 2022 14:48:06 +0200 Subject: [PATCH 4/6] Lookahead: checking wheter a bound propagates This commit introduces a simple check whether a given linear inequality would result in a propagation of another linear inequality. --- src/tsolvers/lasolver/LASolver.cc | 27 +++++++++++++++++++++++++++ src/tsolvers/lasolver/LASolver.h | 5 ++++- 2 files changed, 31 insertions(+), 1 deletion(-) diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index d935847b3..0794682a4 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -627,6 +627,33 @@ bool LASolver::setStatus( LASolverStatus s ) return getStatus( ); } +bool LASolver::wouldDeduce(PtAsgn asgn) const { + assert(status != INIT); + assert(logic.isLeq(asgn.tr)); + assert(not hasPolarity(asgn.tr)); + LVRef v = getVarForLeq(asgn.tr); + LABoundRef boundRef = asgn.sgn == l_False ? getBoundRefPair(asgn.tr).neg : getBoundRefPair(asgn.tr).pos; + LABound const & bound = boundStore[boundRef]; + + auto searchForUnassignedBound = [this, &bound, &v](BoundT type) { + for (int it = bound.getIdx().x - 1; it >= 0; -- it) { + LABoundRef candidateRef = boundStore.getBoundByIdx(v, it); + LABound const & candidate = boundStore[candidateRef]; + if (candidate.getType() != type) { + continue; + } else if (not hasPolarity(getAsgnByBound(candidateRef).tr)) { + return true; + } + } + return false; + }; + + if (bound.getType() == bound_l) { + return searchForUnassignedBound(bound_u); + } + assert(bound.getType() == bound_u); + return searchForUnassignedBound(bound_l); +} void LASolver::getSimpleDeductions(LVRef v, LABoundRef br) { diff --git a/src/tsolvers/lasolver/LASolver.h b/src/tsolvers/lasolver/LASolver.h index 43b9060ac..e8d718c10 100644 --- a/src/tsolvers/lasolver/LASolver.h +++ b/src/tsolvers/lasolver/LASolver.h @@ -160,6 +160,7 @@ class LASolver: public TSolver bool shouldTryCutFromProof() const; void getSuggestions( vec& dst, SolverId solver_id ); // find possible suggested atoms + bool wouldDeduce(PtAsgn pta) const; // Would setting this assignment deduce more bounds void getSimpleDeductions(LVRef v, LABoundRef); // find deductions from actual bounds position unsigned getIteratorByPTRef( PTRef e, bool ); // find bound iterator by the PTRef inline bool getStatus( ); // Read the status of the solver in lbool @@ -181,9 +182,11 @@ class LASolver: public TSolver inline int verbose ( ) const { return config.verbosity(); } + void deduce(LABoundRef bound_prop); + bool wouldDeduce(LABoundRef bound_prop) const; + // Debug stuff void isProperLeq(PTRef tr); // The Leq term conforms to the assumptions of its form. Only asserts. - void deduce(LABoundRef bound_prop); }; #endif From c2dbb3739afe29c90dd7d1b2dbf968a587888950 Mon Sep 17 00:00:00 2001 From: Antti Hyvarinen Date: Fri, 13 May 2022 15:10:27 +0200 Subject: [PATCH 5/6] Lookahead: fix bugs --- src/tsolvers/lasolver/LASolver.cc | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 0794682a4..9f397205d 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -636,16 +636,15 @@ bool LASolver::wouldDeduce(PtAsgn asgn) const { LABound const & bound = boundStore[boundRef]; auto searchForUnassignedBound = [this, &bound, &v](BoundT type) { - for (int it = bound.getIdx().x - 1; it >= 0; -- it) { - LABoundRef candidateRef = boundStore.getBoundByIdx(v, it); + int newId = bound.getIdx().x + (type == bound_l ? -2 : 2); + if (newId < 0 or newId > boundStore.getBounds(v).size() - 1) { + return false; + } else { + LABoundRef candidateRef = boundStore.getBoundByIdx(v, newId); LABound const & candidate = boundStore[candidateRef]; - if (candidate.getType() != type) { - continue; - } else if (not hasPolarity(getAsgnByBound(candidateRef).tr)) { - return true; - } + assert(candidate.getType() == type); + return (not hasPolarity(getAsgnByBound(candidateRef).tr)); } - return false; }; if (bound.getType() == bound_l) { From cceb9a3ae5f526561694e986c92584428984b4e5 Mon Sep 17 00:00:00 2001 From: Antti Hyvarinen Date: Fri, 13 May 2022 18:04:15 +0200 Subject: [PATCH 6/6] Lookahead: remove unused variable --- src/tsolvers/lasolver/LASolver.cc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 9f397205d..31f4ff023 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -641,8 +641,7 @@ bool LASolver::wouldDeduce(PtAsgn asgn) const { return false; } else { LABoundRef candidateRef = boundStore.getBoundByIdx(v, newId); - LABound const & candidate = boundStore[candidateRef]; - assert(candidate.getType() == type); + assert(boundStore[candidateRef].getType() == type); return (not hasPolarity(getAsgnByBound(candidateRef).tr)); } };