Lookahead for linear arith

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<Tableau::Polynomial> 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<Tableau::Polynomial> 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)
 {

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<Tableau::Polynomial> 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<PTRef>& 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

src/tsolvers/lasolver/LAVarMapper.cc

@@ -1,6 +1,9 @@
-//
-// Created by prova on 06.09.19.
-//
+/*
+ *  Copyright (c) 2019-2022, Antti Hyvarinen <[email protected]>
+ *  Copyright (c) 2019-2022, Martin Blicha <[email protected]>
+ *
+ *  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();
 }

src/tsolvers/lasolver/LAVarMapper.h

@@ -1,6 +1,9 @@
-//
-// Created by prova on 06.09.19.
-//
+/*
+ *  Copyright (c) 2019-2022, Antti Hyvarinen <[email protected]>
+ *  Copyright (c) 2019-2022, Martin Blicha <[email protected]>
+ *
+ *  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<LVRef>      leqToLavar;
-
     /** Mapping of linear Pterms to LVRefs */
     vec<LVRef>      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;