From 7bd4a313dd7cdffa7d9369f7a555f5d07b9ac269 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Aug 2018 10:41:07 -0700
Subject: [PATCH] expr utilities for pb

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/Expr.cs | 44 ++++++++++++++++++++++++++++++++++++++++++
 src/sat/ba_solver.cpp  |  1 +
 2 files changed, 45 insertions(+)

diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 849d1af79..99baaa8e4 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -89,6 +89,15 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// The i'th argument of the expression.
+        /// </summary>
+        public Expr Arg(uint i)
+        {
+            Contract.Ensures(Contract.Result<Expr>() != null);
+            return Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
+        }
+
         /// <summary>
         /// Update the arguments of the expression using the arguments <paramref name="args"/>
         /// The number of new arguments should coincide with the current number of arguments.
@@ -315,6 +324,41 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsImplies { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
 
+        /// <summary>
+        /// Indicates whether the term is at-most
+        /// </summary>
+        public bool IsAtMost { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_MOST; } }
+
+        /// <summary>
+        /// Retrieve bound of at-most
+        /// </summary>
+        public uint AtMostBound { get { Contract.Requires(IsAtMost); return (uint)FuncDecl.Parameters[0].Int; } }
+
+        /// <summary>
+        /// Indicates whether the term is at-least
+        /// </summary>
+        public bool IsAtLeast { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_LEAST; } }
+
+        /// <summary>
+        /// Retrieve bound of at-least
+        /// </summary>
+        public uint AtLeastBound { get { Contract.Requires(IsAtLeast); return (uint)FuncDecl.Parameters[0].Int; } }
+
+        /// <summary>
+        /// Indicates whether the term is pbeq
+        /// </summary>
+        public bool IsPbEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_EQ; } }
+
+        /// <summary>
+        /// Indicates whether the term is pble
+        /// </summary>
+        public bool IsPbLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_LE; } }
+
+        /// <summary>
+        /// Indicates whether the term is pbge
+        /// </summary>
+        public bool IsPbGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_GE; } }        
+
         #endregion
 
         #region Arithmetic Terms
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 38cd07fa7..94d27a0c9 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1976,6 +1976,7 @@ namespace sat {
             for (unsigned i = 0; !found && i < c.k(); ++i) {
                 found = c[i] == l;
             }
+            CTRACE("ba",!found, tout << l << ": " << c << "\n";);
             SASSERT(found););
         
         // IF_VERBOSE(0, if (_debug_conflict) verbose_stream() << "ante " << l << " " << c << "\n");