diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 1f5d55f2..31f4ff02 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)); @@ -274,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) @@ -284,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); @@ -340,8 +347,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); + registerArithmeticTerm(term); updateBound(leq_tr); } // DEBUG check @@ -562,9 +568,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); + registerArithmeticTerm(term); // Assumes that the LRA variable has been already declared setBound(leq_tr); @@ -623,6 +627,31 @@ 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) { + 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); + assert(boundStore[candidateRef].getType() == type); + return (not hasPolarity(getAsgnByBound(candidateRef).tr)); + } + }; + + 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 e22944d2..e8d718c1 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); @@ -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. @@ -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 diff --git a/src/tsolvers/lasolver/LAVarMapper.cc b/src/tsolvers/lasolver/LAVarMapper.cc index 7e71bd9f..8d7c6495 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" @@ -37,21 +40,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 +67,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 a590acca..8ebddeec 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 @@ -24,9 +27,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 +39,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;