Adding a model based axiom instantiation scheme for multiplication. Merge commit for nlAlgMaster.

2 files changed, 9 insertions, 0 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 8fecaa78d..0ddc447be 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -136,6 +136,14 @@ Node QuantArith::mkNode( std::map< Node, Node >& msum ) {
   return children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
 }
 
+Node QuantArith::mkCoeffTerm( Node coeff, Node t ) {
+  if( coeff.isNull() ){
+    return t;
+  }else{
+    return NodeManager::currentNM()->mkNode( kind::MULT, coeff, t );
+  }
+}
+
 // given (msum <k> 0), solve (veq_c * v <k> val) or (val <k> veq_c * v), where:
 // veq_c is either null (meaning 1), or positive.
 // return value 1: veq_c*v is RHS, -1: veq_c*v is LHS, 0: failed.
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index b4264135c..fcc162a7a 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -91,6 +91,7 @@ public:
   static bool getMonomialSum( Node n, std::map< Node, Node >& msum );
   static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
   static Node mkNode( std::map< Node, Node >& msum );
+  static Node mkCoeffTerm( Node coeff, Node t );
   //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed
   static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k );
   static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false );