Ported over the code for the command nullify-sys that I had dome in a…

… 'nullify' branch ... but I had so much cruft change in between it seemed safer to go through by hand and figure out what really was added.

interpreter/src/formula/formmanip.cpp

@@ -1025,4 +1025,21 @@ void getFactors(TFormRef F, std::set<IntPolyRef> &W)
   return;
 }
 
+TFormRef nullifySys(IntPolyRef p, VarSet S, PolyManager* pM) {
+  if (p->isZero()) return new TConstObj(TRUE);
+  VarSet Sp = S & p->getVars();
+  TAndRef F = new TAndObj();
+  if (Sp.isEmpty())
+    F->AND(makeAtom(*pM,p,EQOP));
+  else {
+    vector<IntPolyRef> V;
+    pM->nonZeroCoefficients(p,Sp,V);
+    for(int i = 0; i < V.size(); i++) {
+      TAtomRef a = makeAtom(*pM,V[i],EQOP);
+      F->AND(a);
+    }
+  }
+  return F;
+}
+
 }//end namespace tarski

interpreter/src/formula/formmanip.h

@@ -80,6 +80,13 @@ TFormRef evalFormulaAtRationalPoint(VarKeyedMap<GCWord> &value, TFormRef F);
  TFormRef splitNonStrict(TFormRef F);
 
  void getFactors(TFormRef F, std::set<IntPolyRef> &W);
-
+
+ /** nullifysys(p,S,pM)
+ * Input: p a polynomials and S a set of vars
+ * Output: formula F that is true iff p 
+ */
+ TFormRef nullifySys(IntPolyRef p, VarSet S, PolyManager* pM);
+
+
 }//end namespace tarski
 #endif

interpreter/src/poly/polymanager.cpp

@@ -280,20 +280,28 @@ IntPolyRef PolyManager::neg(IntPolyRef p)
 
 void PolyManager::nonZeroCoefficients(IntPolyRef p, VarSet Z, vector<IntPolyRef> &V)
 {
-  if (Z.none()) return;
+  // Zero has no non-zero coefficients!
+  if (p->isZero()) return;
+
+  // find x, the first var in Z s.t. p has positive degree in x
   VarSet::iterator itr = Z.begin();
+  while(itr != Z.end() && (*itr & p->svars).none())
+    ++itr;
+  if (itr == Z.end()) {
+    V.push_back(p);
+    return;
+  }
   VarSet x = *itr;
-  VarSet Zp = Z ^ x;
+
+  // Recurse on the coefficients of p as a polynomial in x
+  VarSet Zp = Z - x;
+  VarSet varsRemaining = p->getVars() - x;
   Word i = p->svars.positionInOrder(x);
-  if (i == 0) { return nonZeroCoefficients(p,Zp,V); }
   Word A = PMMVPO(p->slevel,p->sP,i);
   Word C = PCL(A);
-  if (Zp.none())
-    for(Word Cp = C; Cp != NIL; Cp = RED(Cp)) V.push_back(new IntPolyObj(p->slevel - 1,FIRST(Cp),Zp));
-  else
-    for(Word Cp = C; Cp != NIL; Cp = RED(Cp)) nonZeroCoefficients(new IntPolyObj(p->slevel - 1,FIRST(Cp),Zp),Zp,V);
-
-}
+  for(Word Cp = C; Cp != NIL; Cp = RED(Cp))
+    nonZeroCoefficients(new IntPolyObj(p->slevel - 1,FIRST(Cp),varsRemaining),Zp,V);
+} 
 
 // Special S-polynomial
 // Input: Polynomials p and q, variable x. deg_x(p) = deg_x(q) > 1.

interpreter/src/shell/einterpreter.cpp

@@ -1632,6 +1632,7 @@ void NewEInterpreter::init()
   add(new CommSolutionDimension(this));
   add(new CommDiscriminant(this));
   add(new CommSubDiscSeq(this));
+  add(new CommNullifySys(this));
 
   // add extended types
   addType(new RealAlgNumTypeObj(NULL));

interpreter/src/shell/misc-comms.cpp

@@ -108,8 +108,22 @@ namespace tarski {
     return res;
   }
 
+  SRef CommNullifySys::execute(SRef input, vector<SRef> &args) {
+    // Get polynomial p and varset S
+    AlgRef A = args[0]->alg();
+    IntPolyRef p = A->getVal();
+    LisRef vars = args[1]->lis();
+    VarSet S;
+    for(int i = 0; i < vars->length(); ++i)  {
+      if (vars->get(i)->type() != _sym) { 
+	return new ErrObj("Function 'nullify-sys' received as 2nd argument a list that contains non-symbol element '" + vars->get(i)->toStr() + "'."); 
+      }
+      S = S + interp->PM->getVar(vars->get(i)->sym()->val);
+    }
 
-
-
+    // (nullify-sys [ a x y^2 + y x - (a + y)] '(x))
+
+    return new TarObj(nullifySys(p,S,interp->PM));
+  }
 
 }

interpreter/src/shell/misc-comms.h

@@ -72,6 +72,23 @@ namespace tarski {
     string name() { return "sub-disc-seq"; }
   };
 
-}
+  class CommNullifySys : public EICommand
+  {
+  public:
+    CommNullifySys(NewEInterpreter* ptr) : EICommand(ptr) { }
+    SRef execute(SRef input, vector<SRef> &args);
+
+    string testArgs(vector<SRef> &args) {
+      return requirepre(args,_alg,_lis);
+    }
+    string doc() 
+    {
+      return "Returns formula F that is true exactly when all coefficients of P as a polynomial in v are zero.\
+Example: ";
+    }
+    string usage() { return "(nullify-sys P v)"; }
+    string name() { return "nullify-sys"; }
+  };
 
+}
 #endif