public API for spacer

src/CMakeLists.txt

@@ -14,6 +14,7 @@ set(Z3_API_HEADER_FILES_TO_SCAN
   z3_optimization.h
   z3_interp.h
   z3_fpa.h
+  z3_spacer.h
 )
 set(Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "")
 foreach (header_file ${Z3_API_HEADER_FILES_TO_SCAN})
@@ -169,6 +170,7 @@ set (libz3_public_headers
   z3_polynomial.h
   z3_rcf.h
   z3_v1.h
+  z3_spacer.h
 )
 foreach (header ${libz3_public_headers})
   set_property(TARGET libz3 APPEND PROPERTY

src/api/CMakeLists.txt

@@ -57,6 +57,7 @@ z3_add_component(api
     api_parsers.cpp
     api_pb.cpp
     api_polynomial.cpp
+    api_qe.cpp
     api_quant.cpp
     api_rcf.cpp
     api_seq.cpp

src/api/api_datalog.cpp

@@ -605,5 +605,6 @@ extern "C" {
 
     }
     
+#include "api_datalog_spacer.inc"
 
 };

src/api/api_datalog_spacer.inc

@@ -0,0 +1,113 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    api_datalog_spacer.inc
+
+Abstract:
+
+    Spacer-specific datalog API
+
+Author:
+
+    Arie Gurfinkel (arie) 
+
+Notes:
+  this file is included at the bottom of api_datalog.cpp
+
+--*/
+    Z3_lbool Z3_API Z3_fixedpoint_query_from_lvl (Z3_context c, Z3_fixedpoint d, Z3_ast q, unsigned lvl) {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_query_from_lvl (c, d, q, lvl);
+        RESET_ERROR_CODE();
+        lbool r = l_undef;
+        unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+        unsigned rlimit  = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
+        {
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
+            cancel_eh<reslimit> eh(mk_c(c)->m().limit());
+            api::context::set_interruptable si(*(mk_c(c)), eh);        
+            scoped_timer timer(timeout, &eh);
+            try {
+                r = to_fixedpoint_ref(d)->ctx().query_from_lvl (to_expr(q), lvl);
+            }
+            catch (z3_exception& ex) {
+                mk_c(c)->handle_exception(ex);
+                r = l_undef;
+            }
+            to_fixedpoint_ref(d)->ctx().cleanup();
+        }
+        return of_lbool(r);
+        Z3_CATCH_RETURN(Z3_L_UNDEF);
+    }
+
+    Z3_ast Z3_API Z3_fixedpoint_get_ground_sat_answer(Z3_context c, Z3_fixedpoint d) {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_get_ground_sat_answer(c, d);
+        RESET_ERROR_CODE();
+        expr* e = to_fixedpoint_ref(d)->ctx().get_ground_sat_answer();
+        mk_c(c)->save_ast_trail(e);
+        RETURN_Z3(of_expr(e));
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast_vector Z3_API Z3_fixedpoint_get_rules_along_trace(
+        Z3_context c,
+        Z3_fixedpoint d)
+    {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_get_rules_along_trace(c, d);
+        ast_manager& m = mk_c(c)->m();
+        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
+        mk_c(c)->save_object(v);
+        expr_ref_vector rules(m);
+        svector<symbol> names;
+        
+        to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names);
+        for (unsigned i = 0; i < rules.size(); ++i) {
+            v->m_ast_vector.push_back(rules[i].get());
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_symbol Z3_API Z3_fixedpoint_get_rule_names_along_trace(
+        Z3_context c,
+        Z3_fixedpoint d)
+    {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_get_rule_names_along_trace(c, d);
+        ast_manager& m = mk_c(c)->m();
+        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
+        mk_c(c)->save_object(v);
+        expr_ref_vector rules(m);
+        svector<symbol> names;
+        std::stringstream ss;
+        
+        to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names);
+        for (unsigned i = 0; i < names.size(); ++i) {
+            ss << ";" << names[i].str();
+        }
+        RETURN_Z3(of_symbol(symbol(ss.str().substr(1).c_str())));
+        Z3_CATCH_RETURN(0);
+    }
+
+    void Z3_API Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property) {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_add_invariant(c, d, pred, property);
+        RESET_ERROR_CODE();
+        to_fixedpoint_ref(d)->ctx ().add_invariant(to_func_decl(pred), to_expr(property));        
+        Z3_CATCH;
+    }
+
+    Z3_ast Z3_API Z3_fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_get_reachable(c, d, pred);
+        RESET_ERROR_CODE();
+        expr_ref r = to_fixedpoint_ref(d)->ctx().get_reachable(to_func_decl(pred));
+        mk_c(c)->save_ast_trail(r);        
+        RETURN_Z3(of_expr(r.get()));
+        Z3_CATCH_RETURN(0);
+    }
+

src/api/api_qe.cpp

@@ -0,0 +1,179 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    api_qe.cpp
+
+Abstract:
+
+    Model-based Projection (MBP) and Quantifier Elimination (QE) API
+
+Author:
+
+    Arie Gurfinkel (arie)
+
+Notes:
+
+--*/
+
+#include <iostream>
+#include "z3.h"
+#include "api_log_macros.h"
+#include "api_context.h"
+#include "api_util.h"
+#include "api_model.h"
+#include "api_ast_map.h"
+#include "api_ast_vector.h"
+
+#include "qe_vartest.h"
+#include "qe_lite.h"
+#include "spacer_util.h"
+
+#include "expr_map.h"
+
+extern "C"
+{
+  Z3_ast Z3_API Z3_qe_model_project (Z3_context c,
+                                     Z3_model m,
+                                     unsigned num_bounds,
+                                     Z3_app const bound[],
+                                     Z3_ast body)
+  {
+    Z3_TRY;
+    LOG_Z3_qe_model_project (c, m, num_bounds, bound, body);
+    RESET_ERROR_CODE();
+
+    app_ref_vector vars(mk_c(c)->m ());
+    for (unsigned i = 0; i < num_bounds; ++i)
+    {
+      app *a = to_app (bound [i]);
+      if (a->get_kind () != AST_APP)
+      {
+        SET_ERROR_CODE (Z3_INVALID_ARG);
+        RETURN_Z3(0);
+      }
+      vars.push_back (a);
+    }
+
+    expr_ref result (mk_c(c)->m ());
+    result = to_expr (body);
+    model_ref model (to_model_ref (m));
+    spacer::qe_project (mk_c(c)->m (), vars, result, model);
+    mk_c(c)->save_ast_trail (result.get ());
+
+    return of_expr (result.get ());
+    Z3_CATCH_RETURN(0);
+  }
+
+  Z3_ast Z3_API Z3_qe_model_project_skolem (Z3_context c,
+                                       Z3_model m,
+                                       unsigned num_bounds,
+                                       Z3_app const bound[],
+                                       Z3_ast body,
+                                       Z3_ast_map map)
+    {
+      Z3_TRY;
+      LOG_Z3_qe_model_project_skolem (c, m, num_bounds, bound, body, map);
+      RESET_ERROR_CODE();
+
+      ast_manager& man = mk_c(c)->m ();
+      app_ref_vector vars(man);
+      for (unsigned i = 0; i < num_bounds; ++i)
+      {
+        app *a = to_app (bound [i]);
+        if (a->get_kind () != AST_APP)
+        {
+          SET_ERROR_CODE (Z3_INVALID_ARG);
+          RETURN_Z3(0);
+        }
+        vars.push_back (a);
+      }
+
+      expr_ref result (mk_c(c)->m ());
+      result = to_expr (body);
+      model_ref model (to_model_ref (m));
+      expr_map emap (man);
+
+      spacer::qe_project (mk_c(c)->m (), vars, result, model, emap);
+      mk_c(c)->save_ast_trail (result.get ());
+
+      obj_map<ast, ast*> &map_z3 = to_ast_map_ref(map);
+
+      for (expr_map::iterator it = emap.begin(), end = emap.end(); it != end; ++it){
+        man.inc_ref(&(it->get_key()));
+        man.inc_ref(it->get_value());
+        map_z3.insert(&(it->get_key()), it->get_value());
+      }
+
+      return of_expr (result.get ());
+      Z3_CATCH_RETURN(0);
+    }
+
+  Z3_ast Z3_API Z3_model_extrapolate (Z3_context c,
+                                      Z3_model m,
+                                      Z3_ast fml)
+  {
+    Z3_TRY;
+    LOG_Z3_model_extrapolate (c, m, fml);
+    RESET_ERROR_CODE();
+
+    model_ref model (to_model_ref (m));
+    expr_ref_vector facts (mk_c(c)->m ());
+    facts.push_back (to_expr (fml));
+    flatten_and (facts);
+
+    spacer::model_evaluator_util mev (mk_c(c)->m());
+    mev.set_model (*model);
+
+    expr_ref_vector lits (mk_c(c)->m());
+    spacer::compute_implicant_literals (mev, facts, lits);
+
+    expr_ref result (mk_c(c)->m ());
+    result = mk_and (lits);
+    mk_c(c)->save_ast_trail (result.get ());
+
+    return of_expr (result.get ());
+    Z3_CATCH_RETURN(0);
+  }
+
+  Z3_ast Z3_API Z3_qe_lite (Z3_context c, Z3_ast_vector vars, Z3_ast body)
+  {
+    Z3_TRY;
+    LOG_Z3_qe_lite (c, vars, body);
+    RESET_ERROR_CODE();
+    ast_ref_vector &vVars = to_ast_vector_ref (vars);
+
+    app_ref_vector vApps (mk_c(c)->m());
+    for (unsigned i = 0; i < vVars.size (); ++i)
+    {
+      app *a = to_app (vVars.get (i));
+      if (a->get_kind () != AST_APP)
+      {
+        SET_ERROR_CODE (Z3_INVALID_ARG);
+        RETURN_Z3(0);
+      }
+      vApps.push_back (a);
+    }
+
+    expr_ref result (mk_c(c)->m ());
+    result = to_expr (body);
+
+    params_ref p;
+    qe_lite qe (mk_c(c)->m (), p);
+    qe (vApps, result);
+
+    // -- copy back variables that were not eliminated
+    if (vApps.size () < vVars.size ())
+    {
+      vVars.reset ();
+      for (unsigned i = 0; i < vApps.size (); ++i)
+        vVars.push_back (vApps.get (i));
+    }
+
+    mk_c(c)->save_ast_trail (result.get ());
+    return of_expr (result);
+    Z3_CATCH_RETURN(0);
+  }
+
+}

src/api/z3.h

@@ -33,5 +33,6 @@ Notes:
 #include "api/z3_interp.h"
 #include "api/z3_fpa.h"
 
+#include"z3_spacer.h"
 #endif
 

src/api/z3_spacer.h

@@ -0,0 +1,143 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    z3_spacer.h
+
+Abstract:
+
+    Spacer API
+
+Author:
+
+    Arie Gurfinkel (arie)
+
+Notes:
+
+--*/
+#ifndef Z3_SPACER_H_
+#define Z3_SPACER_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif // __cplusplus
+
+    /** \defgroup capi C API */
+    /*@{*/
+
+    /** @name Spacer facilities */
+    /*@{*/
+    /**
+        \brief Pose a query against the asserted rules at the given level.
+
+        \code
+           query ::= (exists (bound-vars) query)
+                 |  literals
+        \endcode
+
+        query returns
+        - Z3_L_FALSE if the query is unsatisfiable.
+        - Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
+        - Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
+
+        def_API('Z3_fixedpoint_query_from_lvl', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST), _in(UINT)))
+    */
+    Z3_lbool Z3_API Z3_fixedpoint_query_from_lvl (Z3_context c,Z3_fixedpoint d, Z3_ast query, unsigned lvl);
+
+     /**
+       \brief Retrieve a bottom-up (from query) sequence of ground facts
+
+       The previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
+
+       def_API('Z3_fixedpoint_get_ground_sat_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
+    */
+    Z3_ast Z3_API Z3_fixedpoint_get_ground_sat_answer(Z3_context c,Z3_fixedpoint d);
+
+    /**
+       \brief Obtain the list of rules along the counterexample trace.
+
+       def_API('Z3_fixedpoint_get_rules_along_trace', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT)))
+    */
+    Z3_ast_vector Z3_API Z3_fixedpoint_get_rules_along_trace(Z3_context c,Z3_fixedpoint d);
+
+    /**
+       \brief Obtain the list of rules along the counterexample trace.
+
+       def_API('Z3_fixedpoint_get_rule_names_along_trace', SYMBOL, (_in(CONTEXT), _in(FIXEDPOINT)))
+    */
+    Z3_symbol Z3_API Z3_fixedpoint_get_rule_names_along_trace(Z3_context c,Z3_fixedpoint d);
+
+    /**
+       \brief Add an invariant for the predicate \c pred.
+       Add an assumed invariant of predicate \c pred.
+
+       Note: this functionality is Spacer specific.
+
+       def_API('Z3_fixedpoint_add_invariant', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL), _in(AST)))
+    */
+    void Z3_API Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property);
+
+
+    /**
+       Retrieve reachable states of a predicate.
+       Note: this functionality is Spacer specific.
+
+       def_API('Z3_fixedpoint_get_reachable', AST, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL)))
+     */
+    Z3_ast Z3_API Z3_fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred);
+
+    /**
+       \brief Project variables given a model
+
+       def_API('Z3_qe_model_project', AST, (_in(CONTEXT), _in(MODEL), _in(UINT), _in_array(2, APP), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_qe_model_project
+      (Z3_context c,
+       Z3_model m,
+       unsigned num_bounds,
+       Z3_app const bound[],
+       Z3_ast body);
+
+
+    /**
+       \brief Project variables given a model
+
+       def_API('Z3_qe_model_project_skolem', AST, (_in(CONTEXT), _in(MODEL), _in(UINT), _in_array(2, APP), _in(AST), _in(AST_MAP)))
+    */
+    Z3_ast Z3_API Z3_qe_model_project_skolem
+      (Z3_context c,
+       Z3_model m,
+       unsigned num_bounds,
+       Z3_app const bound[],
+       Z3_ast body,
+       Z3_ast_map map);
+
+    /**
+       \brief Extrapolates a model of a formula
+
+       def_API('Z3_model_extrapolate', AST, (_in(CONTEXT), _in(MODEL), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_model_extrapolate
+      (Z3_context c,
+       Z3_model m,
+       Z3_ast fml);
+
+    /**
+       \brief Best-effort quantifier elimination
+
+       def_API ('Z3_qe_lite', AST, (_in(CONTEXT), _in(AST_VECTOR), _in(AST)))
+    */
+    Z3_ast Z3_qe_lite
+      (Z3_context c,
+       Z3_ast_vector vars,
+       Z3_ast body);
+
+    /*@}*/
+    /*@}*/
+
+#ifdef __cplusplus
+}
+#endif // __cplusplus
+
+#endif