Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api

Conflicts:
	scripts/mk_project.py

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

examples/interp/iz3.cpp

@@ -0,0 +1,452 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <iostream>
+#include <string>
+#include <vector>
+#include "z3.h"
+
+
+
+int usage(const char **argv){
+  std::cerr << "usage: " << argv[0] << " [options] file.smt" << std::endl;
+  std::cerr << std::endl;
+  std::cerr << "options:" << std::endl;
+  std::cerr << "  -t,--tree        tree interpolation" << std::endl;
+  std::cerr << "  -c,--check       check result" << std::endl;
+  std::cerr << "  -p,--profile     profile execution" << std::endl;
+  std::cerr << "  -w,--weak        weak interpolants" << std::endl;
+  std::cerr << "  -f,--flat        ouput flat formulas" << std::endl;
+  std::cerr << "  -o <file>        ouput to SMT-LIB file" << std::endl;
+  std::cerr << "  -a,--anon        anonymize" << std::endl;
+  std::cerr << "  -s,--simple      simple proof mode" << std::endl;
+  std::cerr << std::endl;
+  return 1;
+}
+
+int main(int argc, const char **argv) {
+    
+  bool tree_mode = false;
+  bool check_mode = false;
+  bool profile_mode = false;
+  bool incremental_mode = false;
+  std::string output_file;
+  bool flat_mode = false;
+  bool anonymize = false;
+  bool write = false;
+
+  Z3_config cfg = Z3_mk_config();
+  // Z3_interpolation_options options = Z3_mk_interpolation_options();
+  Z3_params options = 0;
+
+  /* Parse the command line */
+  int argn = 1;
+  while(argn < argc-1){
+    std::string flag = argv[argn];
+    if(flag[0] == '-'){
+      if(flag == "-t" || flag == "--tree")
+	tree_mode = true;
+      else if(flag == "-c" || flag == "--check")
+	check_mode = true;
+      else if(flag == "-p" || flag == "--profile")
+	profile_mode = true;
+#if 0
+      else if(flag == "-w" || flag == "--weak")
+        Z3_set_interpolation_option(options,"weak","1");
+      else if(flag == "--secondary")
+        Z3_set_interpolation_option(options,"secondary","1");
+#endif
+      else if(flag == "-i" || flag == "--incremental")
+        incremental_mode = true;
+      else if(flag == "-o"){
+        argn++;
+        if(argn >= argc) return usage(argv);
+        output_file = argv[argn];
+      }
+      else if(flag == "-f" || flag == "--flat")
+        flat_mode = true;
+      else if(flag == "-a" || flag == "--anon")
+        anonymize = true;
+      else if(flag == "-w" || flag == "--write")
+        write = true;
+      else if(flag == "-s" || flag == "--simple")
+        Z3_set_param_value(cfg,"PREPROCESS","false");
+      else
+        return usage(argv);
+    }
+    argn++;
+  }
+  if(argn != argc-1)
+    return usage(argv);
+  const char *filename = argv[argn];
+
+
+  /* Create a Z3 context to contain formulas */
+  Z3_context ctx = Z3_mk_interpolation_context(cfg);
+
+  if(write || anonymize)
+    Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);
+  else if(!flat_mode)
+    Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB_COMPLIANT);
+  
+  /* Read an interpolation problem */
+
+  int num;
+  Z3_ast *constraints;
+  int *parents = 0;
+  const char *error;
+  bool ok;
+  int num_theory;
+  Z3_ast *theory;
+
+  ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory);
+
+  /* If parse failed, print the error message */
+
+  if(!ok){
+    std::cerr << error << "\n";
+    return 1;
+  }
+
+  /* if we get only one formula, and it is a conjunction, split it into conjuncts. */
+  if(!tree_mode && num == 1){
+    Z3_app app = Z3_to_app(ctx,constraints[0]);
+    Z3_func_decl func = Z3_get_app_decl(ctx,app);
+    Z3_decl_kind dk = Z3_get_decl_kind(ctx,func);
+    if(dk == Z3_OP_AND){
+      int nconjs = Z3_get_app_num_args(ctx,app);
+      if(nconjs > 1){
+	std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
+	num = nconjs;
+	constraints = new Z3_ast[num];
+	for(int k = 0; k < num; k++)
+	  constraints[k] = Z3_get_app_arg(ctx,app,k);
+      }
+    }
+  }
+
+  /* Write out anonymized version. */
+
+  if(write || anonymize){
+#if 0
+    Z3_anonymize_ast_vector(ctx,num,constraints);
+#endif
+    std::string ofn = output_file.empty() ? "iz3out.smt2" : output_file;
+    Z3_write_interpolation_problem(ctx, num, constraints, parents, ofn.c_str(), num_theory,  theory);
+    std::cout << "anonymized problem written to " << ofn << "\n";
+    exit(0);
+  }
+
+  /* Compute an interpolant, or get a model. */
+
+  Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
+  Z3_model model = 0;
+  Z3_lbool result;
+
+  if(!incremental_mode){
+    /* In non-incremental mode, we just pass the constraints. */
+    result = Z3_interpolate(ctx, num, constraints, (unsigned int *)parents,  options, interpolants, &model, 0, false, num_theory, theory);
+  }
+  else {
+
+    /* This is a somewhat useless demonstration of incremental mode.
+      Here, we assert the constraints in the context, then pass them to
+      iZ3 in an array, so iZ3 knows the sequence. Note it's safe to pass
+      "true", even though we haven't techically asserted if. */
+
+    Z3_push(ctx);
+    std::vector<Z3_ast> asserted(num);
+
+    /* We start with nothing asserted. */
+    for(int i = 0; i < num; i++)
+      asserted[i] = Z3_mk_true(ctx);
+
+    /* Now we assert the constrints one at a time until UNSAT. */
+
+    for(int i = 0; i < num; i++){
+      asserted[i] = constraints[i];
+      Z3_assert_cnstr(ctx,constraints[i]);  // assert one constraint
+      result = Z3_interpolate(ctx, num, &asserted[0], (unsigned int *)parents,  options, interpolants, &model, 0, true, 0, 0);
+      if(result == Z3_L_FALSE){
+	for(unsigned j = 0; j < num-1; j++)
+          /* Since we want the interpolant formulas to survive a "pop", we
+            "persist" them here. */
+          Z3_persist_ast(ctx,interpolants[j],1);
+        break;
+      }
+    }
+    Z3_pop(ctx,1);
+  }
+  
+  switch (result) {
+  
+    /* If UNSAT, print the interpolants */
+  case Z3_L_FALSE:
+    printf("unsat\n");
+    if(output_file.empty()){
+      printf("interpolant:\n");
+      for(int i = 0; i < num-1; i++)
+        printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
+    }
+    else {
+#if 0
+      Z3_write_interpolation_problem(ctx,num-1,interpolants,0,output_file.c_str());
+      printf("interpolant written to %s\n",output_file.c_str());
+#endif
+    }
+#if 1
+    if(check_mode){
+      std::cout << "Checking interpolant...\n";
+      bool chk;
+      chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory);  
+      if(chk)
+	std::cout << "Interpolant is correct\n";
+      else {
+        std::cout << "Interpolant is incorrect\n";
+        std::cout << error;
+        return 1;
+      }
+    }
+#endif
+    break;
+  case Z3_L_UNDEF:
+    printf("fail\n");
+    break;
+  case Z3_L_TRUE:
+    printf("sat\n");
+    printf("model:\n%s\n", Z3_model_to_string(ctx, model));
+    break;
+  }
+
+  if(profile_mode)
+    std::cout << Z3_interpolation_profile(ctx);
+
+  /* Delete the model if there is one */
+  
+  if (model)
+    Z3_del_model(ctx, model);
+  
+  /* Delete logical context. */
+
+  Z3_del_context(ctx);
+  free(interpolants);
+
+  return 0;
+}
+
+
+#if 0
+
+
+
+int test(){
+  int i;
+
+  /* Create a Z3 context to contain formulas */
+
+  Z3_config cfg = Z3_mk_config();
+  Z3_context ctx = iz3_mk_context(cfg);
+    
+  int num = 2;
+
+  Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast));
+
+#if 1
+  Z3_sort arr = Z3_mk_array_sort(ctx,Z3_mk_int_sort(ctx),Z3_mk_bool_sort(ctx)); 
+  Z3_symbol  as  = Z3_mk_string_symbol(ctx, "a");
+  Z3_symbol  bs  = Z3_mk_string_symbol(ctx, "b");
+  Z3_symbol  xs  = Z3_mk_string_symbol(ctx, "x");
+
+  Z3_ast a = Z3_mk_const(ctx,as,arr);
+  Z3_ast b = Z3_mk_const(ctx,bs,arr);
+  Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_int_sort(ctx));
+  
+  Z3_ast c1 = Z3_mk_eq(ctx,a,Z3_mk_store(ctx,b,x,Z3_mk_true(ctx)));
+  Z3_ast c2 = Z3_mk_not(ctx,Z3_mk_select(ctx,a,x));
+#else
+  Z3_symbol  xs  = Z3_mk_string_symbol(ctx, "x");
+  Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_bool_sort(ctx));
+  Z3_ast c1 = Z3_mk_eq(ctx,x,Z3_mk_true(ctx));
+  Z3_ast c2 = Z3_mk_eq(ctx,x,Z3_mk_false(ctx));
+
+#endif
+
+  constraints[0] = c1;
+  constraints[1] = c2;
+  
+  /* print out the result for grins. */
+
+  // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx));
+
+  // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]);
+  // Z3_string smtout = Z3_context_to_string(ctx);
+  // puts(smtout);
+
+  iz3_print(ctx,num,constraints,"iZ3temp.smt");
+
+  /* Make room for interpolants. */
+
+  Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
+
+  /* Make room for the model. */
+
+  Z3_model model = 0;
+
+  /* Call the prover */
+
+  Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model);
+
+  switch (result) {
+  
+    /* If UNSAT, print the interpolants */
+  case Z3_L_FALSE:
+    printf("unsat, interpolants:\n");
+    for(i = 0; i < num-1; i++)
+      printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
+    break;
+  case Z3_L_UNDEF:
+    printf("fail\n");
+    break;
+  case Z3_L_TRUE:
+    printf("sat\n");
+    printf("model:\n%s\n", Z3_model_to_string(ctx, model));
+    break;
+  }
+
+  /* Delete the model if there is one */
+  
+  if (model)
+    Z3_del_model(ctx, model);
+  
+  /* Delete logical context (note, we call iz3_del_context, not
+     Z3_del_context */
+
+  iz3_del_context(ctx);
+
+  return 1;
+}
+
+struct z3_error {
+  Z3_error_code c;
+  z3_error(Z3_error_code _c) : c(_c) {}
+};
+
+extern "C" {
+  static void throw_z3_error(Z3_error_code c){
+    throw z3_error(c);
+  }
+}
+
+int main(int argc, const char **argv) {
+
+  /* Create a Z3 context to contain formulas */
+
+  Z3_config cfg = Z3_mk_config();
+  Z3_context ctx = iz3_mk_context(cfg);
+  Z3_set_error_handler(ctx, throw_z3_error);
+    
+  /* Make some constraints, by parsing an smtlib formatted file given as arg 1 */
+
+  try {
+    Z3_parse_smtlib_file(ctx, argv[1], 0, 0, 0, 0, 0, 0);
+  }
+  catch(const z3_error &err){
+    std::cerr << "Z3 error: " << Z3_get_error_msg(err.c) << "\n";
+    std::cerr << Z3_get_smtlib_error(ctx) << "\n";
+    return(1);
+  } 
+
+  /* Get the constraints from the parser. */
+
+  int num = Z3_get_smtlib_num_formulas(ctx);
+
+  if(num == 0){
+    std::cerr << "iZ3 error: File contains no formulas.\n";
+    return 1;
+  }
+
+
+  Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast));
+
+  int i;
+  for (i = 0; i < num; i++)
+    constraints[i] = Z3_get_smtlib_formula(ctx, i);
+
+  /* if we get only one formula, and it is a conjunction, split it into conjuncts. */
+  if(num == 1){
+    Z3_app app = Z3_to_app(ctx,constraints[0]);
+    Z3_func_decl func = Z3_get_app_decl(ctx,app);
+    Z3_decl_kind dk = Z3_get_decl_kind(ctx,func);
+    if(dk == Z3_OP_AND){
+      int nconjs = Z3_get_app_num_args(ctx,app);
+      if(nconjs > 1){
+	std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
+	num = nconjs;
+	constraints = new Z3_ast[num];
+	for(int k = 0; k < num; k++)
+	  constraints[k] = Z3_get_app_arg(ctx,app,k);
+      }
+    }
+  }
+
+
+  /* print out the result for grins. */
+
+  // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx));
+
+  // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]);
+  // Z3_string smtout = Z3_context_to_string(ctx);
+  // puts(smtout);
+
+  // iz3_print(ctx,num,constraints,"iZ3temp.smt");
+
+  /* Make room for interpolants. */
+
+  Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
+
+  /* Make room for the model. */
+
+  Z3_model model = 0;
+
+  /* Call the prover */
+
+  Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model);
+
+  switch (result) {
+  
+    /* If UNSAT, print the interpolants */
+  case Z3_L_FALSE:
+    printf("unsat, interpolants:\n");
+    for(i = 0; i < num-1; i++)
+      printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
+    std::cout << "Checking interpolants...\n";
+    const char *error;
+    if(iZ3_check_interpolant(ctx, num, constraints, 0, interpolants, &error))
+      std::cout << "Interpolant is correct\n";
+    else {
+      std::cout << "Interpolant is incorrect\n";
+      std::cout << error << "\n";
+    }
+    break;
+  case Z3_L_UNDEF:
+    printf("fail\n");
+    break;
+  case Z3_L_TRUE:
+    printf("sat\n");
+    printf("model:\n%s\n", Z3_model_to_string(ctx, model));
+    break;
+  }
+
+  /* Delete the model if there is one */
+  
+  if (model)
+    Z3_del_model(ctx, model);
+  
+  /* Delete logical context (note, we call iz3_del_context, not
+     Z3_del_context */
+
+  iz3_del_context(ctx);
+
+  return 0;
+}
+
+#endif

examples/tptp/README

@@ -0,0 +1,18 @@
+TPTP front-end and utilities as a sample using the C++ bindings.
+To build the example execute
+   make examples
+in the build directory.
+
+This command will create the executable tptp.
+On Windows, you can just execute it.
+On OSX and Linux, you must install z3 first using 
+   sudo make install
+OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) 
+   with the build directory. You need that to be able to 
+   find the Z3 shared library.
+
+The sample illustrates using Z3 from the TPTP language.
+The TPTP language is documented on http://tptp.org
+It also exposes utilities for converting between SMT-LIB 
+and TPTP format.
+

examples/tptp/tptp5.h

@@ -0,0 +1,38 @@
+#ifndef TPTP5_H_
+#define TPTP5_H_
+
+
+class TreeNode;
+
+#if 0
+class named_formulas {
+    expr_ref_vector m_fmls;
+    svector<symbol> m_names;
+    bool m_has_conjecture;
+    unsigned m_conjecture_index;
+public:
+    named_formulas(ast_manager& m) : 
+        m_fmls(m), 
+        m_has_conjecture(false),
+        m_conjecture_index(0)
+        {}
+    void push_back(expr* fml, char const* name) {
+        m_fmls.push_back(fml);
+        m_names.push_back(symbol(name));
+    }
+    unsigned size() const { return m_fmls.size(); }
+    expr*const* c_ptr() const { return m_fmls.c_ptr(); }
+    expr* operator[](unsigned i) { return m_fmls[i].get(); }
+    symbol const& name(unsigned i) { return m_names[i]; }
+    void set_has_conjecture() { 
+        m_has_conjecture = true;
+        m_conjecture_index = m_fmls.size();
+    }
+    bool has_conjecture() const { return m_has_conjecture; }
+    unsigned conjecture_index() const { return m_conjecture_index; }
+};
+
+bool tptp5_parse(ast_manager& m, char const* filename, named_formulas& fmls);
+#endif
+
+#endif

examples/tptp/tptp5.tab.h

@@ -0,0 +1,138 @@
+/* A Bison parser, made by GNU Bison 2.4.2.  */
+
+/* Skeleton interface for Bison's Yacc-like parsers in C
+   
+      Copyright (C) 1984, 1989-1990, 2000-2006, 2009-2010 Free Software
+   Foundation, Inc.
+   
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+   
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+   
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
+
+/* As a special exception, you may create a larger work that contains
+   part or all of the Bison parser skeleton and distribute that work
+   under terms of your choice, so long as that work isn't itself a
+   parser generator using the skeleton or a modified version thereof
+   as a parser skeleton.  Alternatively, if you modify or redistribute
+   the parser skeleton itself, you may (at your option) remove this
+   special exception, which will cause the skeleton and the resulting
+   Bison output files to be licensed under the GNU General Public
+   License without this special exception.
+   
+   This special exception was added by the Free Software Foundation in
+   version 2.2 of Bison.  */
+
+
+/* Tokens.  */
+#ifndef YYTOKENTYPE
+# define YYTOKENTYPE
+   /* Put the tokens into the symbol table, so that GDB and other debuggers
+      know about them.  */
+   enum yytokentype {
+     AMPERSAND = 258,
+     AT_SIGN = 259,
+     AT_SIGN_MINUS = 260,
+     AT_SIGN_PLUS = 261,
+     CARET = 262,
+     COLON = 263,
+     COLON_EQUALS = 264,
+     COMMA = 265,
+     EQUALS = 266,
+     EQUALS_GREATER = 267,
+     EXCLAMATION = 268,
+     EXCLAMATION_EQUALS = 269,
+     EXCLAMATION_EXCLAMATION = 270,
+     EXCLAMATION_GREATER = 271,
+     LBRKT = 272,
+     LESS_EQUALS = 273,
+     LESS_EQUALS_GREATER = 274,
+     LESS_TILDE_GREATER = 275,
+     LPAREN = 276,
+     MINUS = 277,
+     MINUS_MINUS_GREATER = 278,
+     PERIOD = 279,
+     QUESTION = 280,
+     QUESTION_QUESTION = 281,
+     QUESTION_STAR = 282,
+     RBRKT = 283,
+     RPAREN = 284,
+     STAR = 285,
+     TILDE = 286,
+     TILDE_AMPERSAND = 287,
+     TILDE_VLINE = 288,
+     VLINE = 289,
+     _DLR_cnf = 290,
+     _DLR_fof = 291,
+     _DLR_fot = 292,
+     _DLR_itef = 293,
+     _DLR_itetf = 294,
+     _DLR_itett = 295,
+     _DLR_tff = 296,
+     _DLR_thf = 297,
+     _LIT_cnf = 298,
+     _LIT_fof = 299,
+     _LIT_include = 300,
+     _LIT_tff = 301,
+     _LIT_thf = 302,
+     arrow = 303,
+     comment = 304,
+     comment_line = 305,
+     decimal = 306,
+     decimal_exponent = 307,
+     decimal_fraction = 308,
+     distinct_object = 309,
+     dollar_dollar_word = 310,
+     dollar_word = 311,
+     dot_decimal = 312,
+     integer = 313,
+     less_sign = 314,
+     lower_word = 315,
+     plus = 316,
+     positive_decimal = 317,
+     rational = 318,
+     real = 319,
+     signed_integer = 320,
+     signed_rational = 321,
+     signed_real = 322,
+     single_quoted = 323,
+     star = 324,
+     unrecognized = 325,
+     unsigned_integer = 326,
+     unsigned_rational = 327,
+     unsigned_real = 328,
+     upper_word = 329,
+     vline = 330
+   };
+#endif
+
+
+
+#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
+typedef union YYSTYPE
+{
+
+/* Line 1685 of yacc.c  */
+#line 148 "tptp5.y"
+int ival; double dval; char* sval; TreeNode* pval;
+
+
+/* Line 1685 of yacc.c  */
+#line 130 "tptp5.tab.h"
+} YYSTYPE;
+# define YYSTYPE_IS_TRIVIAL 1
+# define yystype YYSTYPE /* obsolescent; will be withdrawn */
+# define YYSTYPE_IS_DECLARED 1
+#endif
+
+extern YYSTYPE yylval;
+
+