From 2263be1b4dbeace9b9e8e452f3e45ffa2d237bea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 29 Jul 2016 17:24:14 -0700
Subject: [PATCH] adding consequence examples

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c++/example.cpp     | 19 +++++++++++++++++++
 src/api/c++/z3++.h           |  5 +++++
 src/smt/smt_consequences.cpp |  3 ++-
 3 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 2753e1475..a1240543f 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1111,6 +1111,24 @@ void param_descrs_example() {
     }
 }
 
+void consequence_example() {
+    std::cout << "consequence example\n";
+    context c;
+    expr A = c.bool_const("a");
+    expr B = c.bool_const("b");
+    expr C = c.bool_const("c");
+    solver s(c);
+    s.add(implies(A, B));
+    s.add(implies(B, C));
+    expr_vector assumptions(c), vars(c), consequences(c);
+    assumptions.push_back(!C);
+    vars.push_back(A);
+    vars.push_back(B);
+    vars.push_back(C);
+    std::cout << s.consequences(assumptions, vars, consequences) << "\n";
+    std::cout << consequences << "\n";
+}
+
 int main() {
 
     try {
@@ -1154,6 +1172,7 @@ int main() {
         extract_example(); std::cout << "\n";
         param_descrs_example(); std::cout << "\n";
         sudoku_example(); std::cout << "\n";
+        consequence_example(); std::cout << "\n";
         std::cout << "done\n";
     }
     catch (exception & ex) {
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index e0c520f5b..5d01ef5c2 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1723,6 +1723,11 @@ namespace z3 {
             return to_check_result(r);
         }
         model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
+        check_result consequences(expr_vector& assumptions, expr_vector& vars, expr_vector& conseq) {
+            Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
+            check_error();
+            return to_check_result(r);
+        }
         std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
         stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
         expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index 65204c2fc..1f528aaff 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -25,7 +25,8 @@ namespace smt {
         expr_ref_vector premises(m_manager);
         uint_set::iterator it = vars.begin(), end = vars.end();
         for (; it != end; ++it) {
-            premises.push_back(bool_var2expr(*it));
+            expr* e =  bool_var2expr(*it);
+            premises.push_back(get_assignment(*it) != l_false ? e : m_manager.mk_not(e));
         }
         return mk_and(premises);
     }