mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
moved examples to new examples folder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
12d7c3a187
commit
81fd292c66
19 changed files with 0 additions and 0 deletions
24
src/examples/c++/README.txt
Normal file
24
src/examples/c++/README.txt
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
This directory contains scripts to build the test application using
|
||||
Microsoft C compiler, or g++.
|
||||
|
||||
1) Using Microsoft C compiler
|
||||
|
||||
Use 'build.cmd' to build the test application using Microsoft C
|
||||
compiler.
|
||||
|
||||
Remark: The Microsoft C compiler (cl) must be in your path,
|
||||
or you can use the Visual Studio Command Prompt.
|
||||
|
||||
The script 'exec.cmd' adds the bin directory to the path. So,
|
||||
example.exe can find z3.dll.
|
||||
|
||||
2) Using gcc
|
||||
|
||||
You must install Z3 before running this example.
|
||||
To install Z3, execute the following command in the Z3 root directory.
|
||||
|
||||
sudo make install
|
||||
|
||||
Use 'build.sh' to build the test application using g++.
|
||||
It generates the executable 'example'.
|
||||
|
||||
1
src/examples/c++/build-external.cmd
Normal file
1
src/examples/c++/build-external.cmd
Normal file
|
|
@ -0,0 +1 @@
|
|||
cl /EHsc /I ..\..\include /I . ..\..\bin\z3.lib example.cpp
|
||||
1
src/examples/c++/build.cmd
Normal file
1
src/examples/c++/build.cmd
Normal file
|
|
@ -0,0 +1 @@
|
|||
cl /W3 /EHsc /I ..\lib ..\debug\z3_dbg.lib example.cpp
|
||||
9
src/examples/c++/build.sh
Executable file
9
src/examples/c++/build.sh
Executable file
|
|
@ -0,0 +1,9 @@
|
|||
if g++ -fopenmp -o example example.cpp -lz3; then
|
||||
echo "Example was successfully compiled."
|
||||
echo "To run example, execute:"
|
||||
echo " ./example"
|
||||
else
|
||||
echo "You must install Z3 before compiling this example."
|
||||
echo "To install Z3, execute the following command in the Z3 root directory."
|
||||
echo " sudo make install"
|
||||
fi
|
||||
701
src/examples/c++/example.cpp
Normal file
701
src/examples/c++/example.cpp
Normal file
|
|
@ -0,0 +1,701 @@
|
|||
#include"z3++.h"
|
||||
using namespace z3;
|
||||
|
||||
/**
|
||||
Demonstration of how Z3 can be used to prove validity of
|
||||
De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
|
||||
*/
|
||||
void demorgan() {
|
||||
std::cout << "de-Morgan example\n";
|
||||
|
||||
context c;
|
||||
|
||||
expr x = c.bool_const("x");
|
||||
expr y = c.bool_const("y");
|
||||
expr conjecture = !(x && y) == (!x || !y);
|
||||
|
||||
solver s(c);
|
||||
// adding the negation of the conjecture as a constraint.
|
||||
s.add(!conjecture);
|
||||
std::cout << s << "\n";
|
||||
switch (s.check()) {
|
||||
case unsat: std::cout << "de-Morgan is valid\n"; break;
|
||||
case sat: std::cout << "de-Morgan is not valid\n"; break;
|
||||
case unknown: std::cout << "unknown\n"; break;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Find a model for <tt>x >= 1 and y < x + 3</tt>.
|
||||
*/
|
||||
void find_model_example1() {
|
||||
std::cout << "find_model_example1\n";
|
||||
context c;
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
solver s(c);
|
||||
|
||||
s.add(x >= 1);
|
||||
s.add(y < x + 3);
|
||||
std::cout << s.check() << "\n";
|
||||
|
||||
model m = s.get_model();
|
||||
std::cout << m << "\n";
|
||||
// traversing the model
|
||||
for (unsigned i = 0; i < m.size(); i++) {
|
||||
func_decl v = m[i];
|
||||
// this problem contains only constants
|
||||
assert(v.arity() == 0);
|
||||
std::cout << v.name() << " = " << m.get_const_interp(v) << "\n";
|
||||
}
|
||||
// we can evaluate expressions in the model.
|
||||
std::cout << "x + y + 1 = " << m.eval(x + y + 1) << "\n";
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Prove <tt>x = y implies g(x) = g(y)</tt>, and
|
||||
disprove <tt>x = y implies g(g(x)) = g(y)</tt>.
|
||||
|
||||
This function demonstrates how to create uninterpreted types and
|
||||
functions.
|
||||
*/
|
||||
void prove_example1() {
|
||||
std::cout << "prove_example1\n";
|
||||
|
||||
context c;
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
sort I = c.int_sort();
|
||||
func_decl g = function("g", I, I);
|
||||
|
||||
solver s(c);
|
||||
expr conjecture1 = implies(x == y, g(x) == g(y));
|
||||
std::cout << "conjecture 1\n" << conjecture1 << "\n";
|
||||
s.add(!conjecture1);
|
||||
if (s.check() == unsat)
|
||||
std::cout << "proved" << "\n";
|
||||
else
|
||||
std::cout << "failed to prove" << "\n";
|
||||
|
||||
s.reset(); // remove all assertions from solver s
|
||||
|
||||
expr conjecture2 = implies(x == y, g(g(x)) == g(y));
|
||||
std::cout << "conjecture 2\n" << conjecture2 << "\n";
|
||||
s.add(!conjecture2);
|
||||
if (s.check() == unsat) {
|
||||
std::cout << "proved" << "\n";
|
||||
}
|
||||
else {
|
||||
std::cout << "failed to prove" << "\n";
|
||||
model m = s.get_model();
|
||||
std::cout << "counterexample:\n" << m << "\n";
|
||||
std::cout << "g(g(x)) = " << m.eval(g(g(x))) << "\n";
|
||||
std::cout << "g(y) = " << m.eval(g(y)) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Prove <tt>not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 </tt>.
|
||||
Then, show that <tt>z < -1</tt> is not implied.
|
||||
|
||||
This example demonstrates how to combine uninterpreted functions and arithmetic.
|
||||
*/
|
||||
void prove_example2() {
|
||||
std::cout << "prove_example1\n";
|
||||
|
||||
context c;
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
expr z = c.int_const("z");
|
||||
sort I = c.int_sort();
|
||||
func_decl g = function("g", I, I);
|
||||
|
||||
expr conjecture1 = implies(g(g(x) - g(y)) != g(z) && x + z <= y && y <= x,
|
||||
z < 0);
|
||||
|
||||
solver s(c);
|
||||
s.add(!conjecture1);
|
||||
std::cout << "conjecture 1:\n" << conjecture1 << "\n";
|
||||
if (s.check() == unsat)
|
||||
std::cout << "proved" << "\n";
|
||||
else
|
||||
std::cout << "failed to prove" << "\n";
|
||||
|
||||
expr conjecture2 = implies(g(g(x) - g(y)) != g(z) && x + z <= y && y <= x,
|
||||
z < -1);
|
||||
s.reset();
|
||||
s.add(!conjecture2);
|
||||
std::cout << "conjecture 2:\n" << conjecture2 << "\n";
|
||||
if (s.check() == unsat) {
|
||||
std::cout << "proved" << "\n";
|
||||
}
|
||||
else {
|
||||
std::cout << "failed to prove" << "\n";
|
||||
std::cout << "counterexample:\n" << s.get_model() << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Nonlinear arithmetic example 1
|
||||
*/
|
||||
void nonlinear_example1() {
|
||||
std::cout << "nonlinear example 1\n";
|
||||
config cfg;
|
||||
cfg.set(":auto-config", true);
|
||||
context c(cfg);
|
||||
|
||||
expr x = c.real_const("x");
|
||||
expr y = c.real_const("y");
|
||||
expr z = c.real_const("z");
|
||||
|
||||
solver s(c);
|
||||
|
||||
s.add(x*x + y*y == 1); // x^2 + y^2 == 1
|
||||
s.add(x*x*x + z*z*z < c.real_val("1/2")); // x^3 + z^3 < 1/2
|
||||
s.add(z != 0);
|
||||
std::cout << s.check() << "\n";
|
||||
model m = s.get_model();
|
||||
std::cout << m << "\n";
|
||||
c.set(":pp-decimal", true); // set decimal notation
|
||||
std::cout << "model in decimal notation\n";
|
||||
std::cout << m << "\n";
|
||||
c.set(":pp-decimal-precision", 50); // increase number of decimal places to 50.
|
||||
std::cout << "model using 50 decimal places\n";
|
||||
std::cout << m << "\n";
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Simple function that tries to prove the given conjecture using the following steps:
|
||||
1- create a solver
|
||||
2- assert the negation of the conjecture
|
||||
3- checks if the result is unsat.
|
||||
*/
|
||||
void prove(expr conjecture) {
|
||||
context & c = conjecture.ctx();
|
||||
solver s(c);
|
||||
s.add(!conjecture);
|
||||
std::cout << "conjecture:\n" << conjecture << "\n";
|
||||
if (s.check() == unsat) {
|
||||
std::cout << "proved" << "\n";
|
||||
}
|
||||
else {
|
||||
std::cout << "failed to prove" << "\n";
|
||||
std::cout << "counterexample:\n" << s.get_model() << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Simple bit-vector example. This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers
|
||||
*/
|
||||
void bitvector_example1() {
|
||||
std::cout << "bitvector example 1\n";
|
||||
context c;
|
||||
expr x = c.bv_const("x", 32);
|
||||
|
||||
// using signed <=
|
||||
prove((x - 10 <= 0) == (x <= 10));
|
||||
|
||||
// using unsigned <=
|
||||
prove(ule(x - 10, 0) == ule(x, 10));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Find x and y such that: x ^ y - 103 == x * y
|
||||
*/
|
||||
void bitvector_example2() {
|
||||
std::cout << "bitvector example 2\n";
|
||||
context c;
|
||||
expr x = c.bv_const("x", 32);
|
||||
expr y = c.bv_const("y", 32);
|
||||
solver s(c);
|
||||
// In C++, the operator == has higher precedence than ^.
|
||||
s.add((x ^ y) - 103 == x * y);
|
||||
std::cout << s << "\n";
|
||||
std::cout << s.check() << "\n";
|
||||
std::cout << s.get_model() << "\n";
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Mixing C and C++ APIs.
|
||||
*/
|
||||
void capi_example() {
|
||||
std::cout << "capi example\n";
|
||||
context c;
|
||||
expr x = c.bv_const("x", 32);
|
||||
expr y = c.bv_const("y", 32);
|
||||
// Invoking a C API function, and wrapping the result using an expr object.
|
||||
expr r = to_expr(c, Z3_mk_bvsrem(c, x, y));
|
||||
std::cout << "r: " << r << "\n";
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Demonstrate how to evaluate expressions in a model.
|
||||
*/
|
||||
void eval_example1() {
|
||||
std::cout << "eval example 1\n";
|
||||
context c;
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
solver s(c);
|
||||
|
||||
/* assert x < y */
|
||||
s.add(x < y);
|
||||
/* assert x > 2 */
|
||||
s.add(x > 2);
|
||||
|
||||
std::cout << s.check() << "\n";
|
||||
|
||||
model m = s.get_model();
|
||||
std::cout << "Model:\n" << m << "\n";
|
||||
std::cout << "x+y = " << m.eval(x+y) << "\n";
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Several contexts can be used simultaneously.
|
||||
*/
|
||||
void two_contexts_example1() {
|
||||
std::cout << "two contexts example 1\n";
|
||||
context c1, c2;
|
||||
|
||||
expr x = c1.int_const("x");
|
||||
expr n = x + 1;
|
||||
// We cannot mix expressions from different contexts, but we can copy
|
||||
// an expression from one context to another.
|
||||
// The following statement copies the expression n from c1 to c2.
|
||||
expr n1 = to_expr(c2, Z3_translate(c1, n, c2));
|
||||
std::cout << n1 << "\n";
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Demonstrates how to catch API usage errors.
|
||||
*/
|
||||
void error_example() {
|
||||
std::cout << "error example\n";
|
||||
|
||||
context c;
|
||||
expr x = c.bool_const("x");
|
||||
|
||||
// Error using the C API can be detected using Z3_get_error_code.
|
||||
// The next call fails because x is a constant.
|
||||
Z3_ast arg = Z3_get_app_arg(c, x, 0);
|
||||
if (Z3_get_error_code(c) != Z3_OK) {
|
||||
std::cout << "last call failed.\n";
|
||||
}
|
||||
|
||||
// The C++ layer converts API usage errors into exceptions.
|
||||
try {
|
||||
// The next call fails because x is a Boolean.
|
||||
expr n = x + 1;
|
||||
}
|
||||
catch (exception ex) {
|
||||
std::cout << "failed: " << ex << "\n";
|
||||
}
|
||||
|
||||
// The functions to_expr, to_sort and to_func_decl also convert C API errors into exceptions.
|
||||
try {
|
||||
expr arg = to_expr(c, Z3_get_app_arg(c, x, 0));
|
||||
}
|
||||
catch (exception ex) {
|
||||
std::cout << "failed: " << ex << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Demonstrate different ways of creating rational numbers: decimal and fractional representations.
|
||||
*/
|
||||
void numeral_example() {
|
||||
std::cout << "numeral example\n";
|
||||
context c;
|
||||
|
||||
expr n1 = c.real_val("1/2");
|
||||
expr n2 = c.real_val("0.5");
|
||||
expr n3 = c.real_val(1, 2);
|
||||
std::cout << n1 << " " << n2 << " " << n3 << "\n";
|
||||
prove(n1 == n2 && n1 == n3);
|
||||
|
||||
n1 = c.real_val("-1/3");
|
||||
n2 = c.real_val("-0.3333333333333333333333333333333333");
|
||||
std::cout << n1 << " " << n2 << "\n";
|
||||
prove(n1 != n2);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Test ite-term (if-then-else terms).
|
||||
*/
|
||||
void ite_example() {
|
||||
std::cout << "if-then-else example\n";
|
||||
context c;
|
||||
|
||||
expr f = c.bool_val(false);
|
||||
expr one = c.int_val(1);
|
||||
expr zero = c.int_val(0);
|
||||
expr ite = to_expr(c, Z3_mk_ite(c, f, one, zero));
|
||||
|
||||
std::cout << "term: " << ite << "\n";
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Unsat core example
|
||||
*/
|
||||
void unsat_core_example() {
|
||||
std::cout << "unsat core example\n";
|
||||
context c;
|
||||
expr p1 = c.bool_const("p1");
|
||||
expr p2 = c.bool_const("p2");
|
||||
expr p3 = c.bool_const("p3");
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
solver s(c);
|
||||
s.add(implies(p1, x > 10));
|
||||
s.add(implies(p1, y > x));
|
||||
s.add(implies(p2, y < 5));
|
||||
s.add(implies(p3, y > 0));
|
||||
expr assumptions[3] = { p1, p2, p3 };
|
||||
std::cout << s.check(3, assumptions) << "\n";
|
||||
expr_vector core = s.unsat_core();
|
||||
std::cout << core << "\n";
|
||||
std::cout << "size: " << core.size() << "\n";
|
||||
for (unsigned i = 0; i < core.size(); i++) {
|
||||
std::cout << core[i] << "\n";
|
||||
}
|
||||
// Trying again without p2
|
||||
expr assumptions2[2] = { p1, p3 };
|
||||
std::cout << s.check(2, assumptions2) << "\n";
|
||||
}
|
||||
|
||||
void tactic_example1() {
|
||||
/*
|
||||
Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic
|
||||
reasoning steps are represented as functions known as tactics, and tactics are composed
|
||||
using combinators known as tacticals. Tactics process sets of formulas called Goals.
|
||||
|
||||
When a tactic is applied to some goal G, four different outcomes are possible. The tactic succeeds
|
||||
in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible);
|
||||
produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn,
|
||||
we face the problem of model conversion. A model converter construct a model for G using a model for some subgoal Gi.
|
||||
|
||||
In this example, we create a goal g consisting of three formulas, and a tactic t composed of two built-in tactics:
|
||||
simplify and solve-eqs. The tactic simplify apply transformations equivalent to the ones found in the command simplify.
|
||||
The tactic solver-eqs eliminate variables using Gaussian elimination. Actually, solve-eqs is not restricted
|
||||
only to linear arithmetic. It can also eliminate arbitrary variables.
|
||||
Then, sequential composition combinator & applies simplify to the input goal and solve-eqs to each subgoal produced by simplify.
|
||||
In this example, only one subgoal is produced.
|
||||
*/
|
||||
std::cout << "tactic example 1\n";
|
||||
context c;
|
||||
expr x = c.real_const("x");
|
||||
expr y = c.real_const("y");
|
||||
goal g(c);
|
||||
g.add(x > 0);
|
||||
g.add(y > 0);
|
||||
g.add(x == y + 2);
|
||||
std::cout << g << "\n";
|
||||
tactic t1(c, "simplify");
|
||||
tactic t2(c, "solve-eqs");
|
||||
tactic t = t1 & t2;
|
||||
apply_result r = t(g);
|
||||
std::cout << r << "\n";
|
||||
}
|
||||
|
||||
void tactic_example2() {
|
||||
/*
|
||||
In Z3, we say a clause is any constraint of the form (f_1 || ... || f_n).
|
||||
The tactic split-clause will select a clause in the input goal, and split it n subgoals.
|
||||
One for each subformula f_i.
|
||||
*/
|
||||
std::cout << "tactic example 2\n";
|
||||
context c;
|
||||
expr x = c.real_const("x");
|
||||
expr y = c.real_const("y");
|
||||
goal g(c);
|
||||
g.add(x < 0 || x > 0);
|
||||
g.add(x == y + 1);
|
||||
g.add(y < 0);
|
||||
tactic t(c, "split-clause");
|
||||
apply_result r = t(g);
|
||||
for (unsigned i = 0; i < r.size(); i++) {
|
||||
std::cout << "subgoal " << i << "\n" << r[i] << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
void tactic_example3() {
|
||||
/*
|
||||
- The choice combinator t | s first applies t to the given goal, if it fails then returns the result of s applied to the given goal.
|
||||
- repeat(t) Keep applying the given tactic until no subgoal is modified by it.
|
||||
- repeat(t, n) Keep applying the given tactic until no subgoal is modified by it, or the number of iterations is greater than n.
|
||||
- try_for(t, ms) Apply tactic t to the input goal, if it does not return in ms millisenconds, it fails.
|
||||
- with(t, params) Apply the given tactic using the given parameters.
|
||||
*/
|
||||
std::cout << "tactic example 3\n";
|
||||
context c;
|
||||
expr x = c.real_const("x");
|
||||
expr y = c.real_const("y");
|
||||
expr z = c.real_const("z");
|
||||
goal g(c);
|
||||
g.add(x == 0 || x == 1);
|
||||
g.add(y == 0 || y == 1);
|
||||
g.add(z == 0 || z == 1);
|
||||
g.add(x + y + z > 2);
|
||||
// split all clauses
|
||||
tactic split_all = repeat(tactic(c, "split-clause") | tactic(c, "skip"));
|
||||
std::cout << split_all(g) << "\n";
|
||||
tactic split_at_most_2 = repeat(tactic(c, "split-clause") | tactic(c, "skip"), 1);
|
||||
std::cout << split_at_most_2(g) << "\n";
|
||||
// In the tactic split_solver, the tactic solve-eqs discharges all but one goal.
|
||||
// Note that, this tactic generates one goal: the empty goal which is trivially satisfiable (i.e., feasible)
|
||||
tactic split_solve = split_all & tactic(c, "solve-eqs");
|
||||
std::cout << split_solve(g) << "\n";
|
||||
}
|
||||
|
||||
void tactic_example4() {
|
||||
/*
|
||||
A tactic can be converted into a solver object using the method mk_solver().
|
||||
If the tactic produces the empty goal, then the associated solver returns sat.
|
||||
If the tactic produces a single goal containing False, then the solver returns unsat.
|
||||
Otherwise, it returns unknown.
|
||||
|
||||
In this example, the tactic t implements a basic bit-vector solver using equation solving,
|
||||
bit-blasting, and a propositional SAT solver.
|
||||
We use the combinator `with` to configure our little solver.
|
||||
We also include the tactic `aig` which tries to compress Boolean formulas using And-Inverted Graphs.
|
||||
*/
|
||||
std::cout << "tactic example 4\n";
|
||||
context c;
|
||||
params p(c);
|
||||
p.set(":mul2concat", true);
|
||||
tactic t =
|
||||
with(tactic(c, "simplify"), p) &
|
||||
tactic(c, "solve-eqs") &
|
||||
tactic(c, "bit-blast") &
|
||||
tactic(c, "aig") &
|
||||
tactic(c, "sat");
|
||||
solver s = t.mk_solver();
|
||||
expr x = c.bv_const("x", 16);
|
||||
expr y = c.bv_const("y", 16);
|
||||
s.add(x*32 + y == 13);
|
||||
// In C++, the operator < has higher precedence than &.
|
||||
s.add((x & y) < 10);
|
||||
s.add(y > -100);
|
||||
std::cout << s.check() << "\n";
|
||||
model m = s.get_model();
|
||||
std::cout << m << "\n";
|
||||
std::cout << "x*32 + y = " << m.eval(x*32 + y) << "\n";
|
||||
std::cout << "x & y = " << m.eval(x & y) << "\n";
|
||||
}
|
||||
|
||||
void tactic_example5() {
|
||||
/*
|
||||
The tactic smt wraps the main solver in Z3 as a tactic.
|
||||
*/
|
||||
std::cout << "tactic example 5\n";
|
||||
context c;
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
solver s = tactic(c, "smt").mk_solver();
|
||||
s.add(x > y + 1);
|
||||
std::cout << s.check() << "\n";
|
||||
std::cout << s.get_model() << "\n";
|
||||
}
|
||||
|
||||
void tactic_example6() {
|
||||
/*
|
||||
In this example, we show how to implement a solver for integer arithmetic using SAT.
|
||||
The solver is complete only for problems where every variable has a lower and upper bound.
|
||||
*/
|
||||
std::cout << "tactic example 6\n";
|
||||
context c;
|
||||
params p(c);
|
||||
p.set(":arith-lhs", true);
|
||||
p.set(":som", true); // sum-of-monomials normal form
|
||||
solver s =
|
||||
(with(tactic(c, "simplify"), p) &
|
||||
tactic(c, "normalize-bounds") &
|
||||
tactic(c, "lia2pb") &
|
||||
tactic(c, "pb2bv") &
|
||||
tactic(c, "bit-blast") &
|
||||
tactic(c, "sat")).mk_solver();
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
expr z = c.int_const("z");
|
||||
s.add(x > 0 && x < 10);
|
||||
s.add(y > 0 && y < 10);
|
||||
s.add(z > 0 && z < 10);
|
||||
s.add(3*y + 2*x == z);
|
||||
std::cout << s.check() << "\n";
|
||||
std::cout << s.get_model() << "\n";
|
||||
s.reset();
|
||||
s.add(3*y + 2*x == z);
|
||||
std::cout << s.check() << "\n";
|
||||
}
|
||||
|
||||
void tactic_example7() {
|
||||
/*
|
||||
Tactics can be combined with solvers.
|
||||
For example, we can apply a tactic to a goal, produced a set of subgoals,
|
||||
then select one of the subgoals and solve it using a solver.
|
||||
This example demonstrates how to do that, and
|
||||
how to use model converters to convert a model for a subgoal into a model for the original goal.
|
||||
*/
|
||||
std::cout << "tactic example 7\n";
|
||||
context c;
|
||||
tactic t =
|
||||
tactic(c, "simplify") &
|
||||
tactic(c, "normalize-bounds") &
|
||||
tactic(c, "solve-eqs");
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
expr z = c.int_const("z");
|
||||
goal g(c);
|
||||
g.add(x > 10);
|
||||
g.add(y == x + 3);
|
||||
g.add(z > y);
|
||||
apply_result r = t(g);
|
||||
// r contains only one subgoal
|
||||
std::cout << r << "\n";
|
||||
solver s(c);
|
||||
goal subgoal = r[0];
|
||||
for (unsigned i = 0; i < subgoal.size(); i++) {
|
||||
s.add(subgoal[i]);
|
||||
}
|
||||
std::cout << s.check() << "\n";
|
||||
model m = s.get_model();
|
||||
std::cout << "model for subgoal:\n" << m << "\n";
|
||||
std::cout << "model for original goal:\n" << r.convert_model(m) << "\n";
|
||||
}
|
||||
|
||||
void tactic_example8() {
|
||||
/*
|
||||
Probes (aka formula measures) are evaluated over goals.
|
||||
Boolean expressions over them can be built using relational operators and Boolean connectives.
|
||||
The tactic fail_if(cond) fails if the given goal does not satisfy the condition cond.
|
||||
Many numeric and Boolean measures are available in Z3.
|
||||
|
||||
In this example, we build a simple tactic using fail_if.
|
||||
It also shows that a probe can be applied directly to a goal.
|
||||
*/
|
||||
std::cout << "tactic example 8\n";
|
||||
context c;
|
||||
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
expr z = c.int_const("z");
|
||||
|
||||
goal g(c);
|
||||
g.add(x + y + z > 0);
|
||||
|
||||
probe p(c, "num-consts");
|
||||
std::cout << "num-consts: " << p(g) << "\n";
|
||||
|
||||
tactic t = fail_if(p > 2);
|
||||
try {
|
||||
t(g);
|
||||
}
|
||||
catch (exception) {
|
||||
std::cout << "tactic failed...\n";
|
||||
}
|
||||
std::cout << "trying again...\n";
|
||||
g.reset();
|
||||
g.add(x + y > 0);
|
||||
std::cout << t(g) << "\n";
|
||||
}
|
||||
|
||||
void tactic_example9() {
|
||||
/*
|
||||
The combinator (tactical) cond(p, t1, t2) is a shorthand for:
|
||||
|
||||
(fail_if(p) & t1) | t2
|
||||
|
||||
The combinator when(p, t) is a shorthand for:
|
||||
|
||||
cond(p, t, tactic(c, "skip"))
|
||||
|
||||
The tactic skip just returns the input goal.
|
||||
This example demonstrates how to use the cond combinator.
|
||||
*/
|
||||
std::cout << "tactic example 9\n";
|
||||
context c;
|
||||
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
expr z = c.int_const("z");
|
||||
|
||||
goal g(c);
|
||||
g.add(x*x - y*y >= 0);
|
||||
|
||||
probe p(c, "num-consts");
|
||||
tactic t = cond(p > 2, tactic(c, "simplify"), tactic(c, "factor"));
|
||||
std::cout << t(g) << "\n";
|
||||
|
||||
g.reset();
|
||||
g.add(x + x + y + z >= 0);
|
||||
g.add(x*x - y*y >= 0);
|
||||
std::cout << t(g) << "\n";
|
||||
}
|
||||
|
||||
void visit(expr const & e) {
|
||||
if (e.is_app()) {
|
||||
unsigned num = e.num_args();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
visit(e.arg(i));
|
||||
}
|
||||
// do something
|
||||
// Example: print the visited expression
|
||||
func_decl f = e.decl();
|
||||
std::cout << "application of " << f.name() << ": " << e << "\n";
|
||||
}
|
||||
else if (e.is_quantifier()) {
|
||||
visit(e.body());
|
||||
// do something
|
||||
}
|
||||
else {
|
||||
assert(e.is_var());
|
||||
// do something
|
||||
}
|
||||
}
|
||||
|
||||
void tst_visit() {
|
||||
std::cout << "visit example\n";
|
||||
context c;
|
||||
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
expr z = c.int_const("z");
|
||||
expr f = x*x - y*y >= 0;
|
||||
|
||||
visit(f);
|
||||
}
|
||||
|
||||
int main() {
|
||||
try {
|
||||
demorgan(); std::cout << "\n";
|
||||
find_model_example1(); std::cout << "\n";
|
||||
prove_example1(); std::cout << "\n";
|
||||
prove_example2(); std::cout << "\n";
|
||||
nonlinear_example1(); std::cout << "\n";
|
||||
bitvector_example1(); std::cout << "\n";
|
||||
bitvector_example2(); std::cout << "\n";
|
||||
capi_example(); std::cout << "\n";
|
||||
eval_example1(); std::cout << "\n";
|
||||
two_contexts_example1(); std::cout << "\n";
|
||||
error_example(); std::cout << "\n";
|
||||
numeral_example(); std::cout << "\n";
|
||||
ite_example(); std::cout << "\n";
|
||||
unsat_core_example(); std::cout << "\n";
|
||||
tactic_example1(); std::cout << "\n";
|
||||
tactic_example2(); std::cout << "\n";
|
||||
tactic_example3(); std::cout << "\n";
|
||||
tactic_example4(); std::cout << "\n";
|
||||
tactic_example5(); std::cout << "\n";
|
||||
tactic_example6(); std::cout << "\n";
|
||||
tactic_example7(); std::cout << "\n";
|
||||
tactic_example8(); std::cout << "\n";
|
||||
tactic_example9(); std::cout << "\n";
|
||||
tst_visit(); std::cout << "\n";
|
||||
std::cout << "done\n";
|
||||
}
|
||||
catch (exception & ex) {
|
||||
std::cout << "unexpected error: " << ex << "\n";
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
5
src/examples/c++/exec-external.cmd
Normal file
5
src/examples/c++/exec-external.cmd
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
@echo off
|
||||
SETLOCAL
|
||||
set PATH=..\..\bin;%PATH%
|
||||
example.exe
|
||||
ENDLOCAL
|
||||
1343
src/examples/c++/z3++.h
Normal file
1343
src/examples/c++/z3++.h
Normal file
File diff suppressed because it is too large
Load diff
16
src/examples/maxsat/README-external.txt
Normal file
16
src/examples/maxsat/README-external.txt
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
WARNING: this example still uses the old Z3 (version 3.x) C API.
|
||||
The current version is backward compatible.
|
||||
|
||||
This directory contains scripts to build the MaxSAT application using
|
||||
Microsoft C compiler, or gcc.
|
||||
|
||||
1) Using Microsoft C compiler (with binary release)
|
||||
|
||||
Use 'build.cmd' to build the MaxSAT application using Microsoft C compiler.
|
||||
|
||||
Remark: The Microsoft C compiler (cl) must be in your path,
|
||||
or you can use the Visual Studio Command Prompt.
|
||||
|
||||
The script 'exec.cmd' adds the bin directory to the path. So,
|
||||
maxsat.exe can find z3.dll.
|
||||
|
||||
28
src/examples/maxsat/README.txt
Normal file
28
src/examples/maxsat/README.txt
Normal file
|
|
@ -0,0 +1,28 @@
|
|||
WARNING: this example still uses the old Z3 (version 3.x) C API.
|
||||
The current version is backward compatible.
|
||||
|
||||
1) Using Visual Studio (with Z3 source code release)
|
||||
|
||||
The maxsat example application is automatically built when the z3-prover.sln is processed. The following command should be used to compile z3-prover.sln in the Z3 root directory
|
||||
|
||||
msbuild /p:configuration=external
|
||||
|
||||
The maxsat executable is located at
|
||||
|
||||
..\external\maxsat
|
||||
|
||||
To process ex.smt, use
|
||||
|
||||
..\external\maxsat ex.smt
|
||||
|
||||
2) Using gcc (on Linux or OSX)
|
||||
|
||||
Use 'build.sh' to build the MaxSAT application using gcc.
|
||||
|
||||
You must install Z3 before running this example.
|
||||
To install Z3, execute the following command in the Z3 root directory.
|
||||
|
||||
sudo make install
|
||||
|
||||
Use 'build.sh' to build the test application using gcc.
|
||||
It generates the executable 'maxsat'.
|
||||
1
src/examples/maxsat/build-external.cmd
Normal file
1
src/examples/maxsat/build-external.cmd
Normal file
|
|
@ -0,0 +1 @@
|
|||
cl /I ..\..\include ..\..\bin\z3.lib maxsat.c
|
||||
9
src/examples/maxsat/build.sh
Executable file
9
src/examples/maxsat/build.sh
Executable file
|
|
@ -0,0 +1,9 @@
|
|||
if gcc -fopenmp -o maxsat maxsat.c -lz3; then
|
||||
echo "maxsat example was successfully compiled."
|
||||
echo "To run example, execute:"
|
||||
echo " ./maxsat ex.smt"
|
||||
else
|
||||
echo "You must install Z3 before compiling this example."
|
||||
echo "To install Z3, execute the following command in the Z3 root directory."
|
||||
echo " sudo make install"
|
||||
fi
|
||||
11
src/examples/maxsat/ex.smt
Normal file
11
src/examples/maxsat/ex.smt
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
(benchmark ex
|
||||
:logic AUFLIA
|
||||
:extrafuns ((x Int) (y Int) (z Int))
|
||||
:assumption (> x 0)
|
||||
:assumption (<= x -1)
|
||||
:assumption (or (> x 0) (< y 1))
|
||||
:assumption (> y 2)
|
||||
:assumption (> y 3)
|
||||
:assumption (<= y -1)
|
||||
:formula (= z (+ x y)))
|
||||
|
||||
5
src/examples/maxsat/exec-external.cmd
Normal file
5
src/examples/maxsat/exec-external.cmd
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
@echo off
|
||||
SETLOCAL
|
||||
set PATH=..\..\bin;%PATH%
|
||||
maxsat.exe %1
|
||||
ENDLOCAL
|
||||
632
src/examples/maxsat/maxsat.c
Normal file
632
src/examples/maxsat/maxsat.c
Normal file
|
|
@ -0,0 +1,632 @@
|
|||
/*
|
||||
Simple MAXSAT solver on top of the Z3 API.
|
||||
*/
|
||||
#include<stdio.h>
|
||||
#include<stdlib.h>
|
||||
#include<memory.h>
|
||||
#include<z3.h>
|
||||
|
||||
/**
|
||||
\defgroup maxsat_ex MaxSAT/MaxSMT examples
|
||||
*/
|
||||
/*@{*/
|
||||
|
||||
/**
|
||||
\brief Exit gracefully in case of error.
|
||||
*/
|
||||
void error(char * msg)
|
||||
{
|
||||
fprintf(stderr, "%s\n", msg);
|
||||
exit(1);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a logical context.
|
||||
Enable model construction only.
|
||||
*/
|
||||
Z3_context mk_context()
|
||||
{
|
||||
Z3_config cfg;
|
||||
Z3_context ctx;
|
||||
cfg = Z3_mk_config();
|
||||
Z3_set_param_value(cfg, "MODEL", "true");
|
||||
ctx = Z3_mk_context(cfg);
|
||||
Z3_del_config(cfg);
|
||||
return ctx;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a variable using the given name and type.
|
||||
*/
|
||||
Z3_ast mk_var(Z3_context ctx, const char * name, Z3_sort ty)
|
||||
{
|
||||
Z3_symbol s = Z3_mk_string_symbol(ctx, name);
|
||||
return Z3_mk_const(ctx, s, ty);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a boolean variable using the given name.
|
||||
*/
|
||||
Z3_ast mk_bool_var(Z3_context ctx, const char * name)
|
||||
{
|
||||
Z3_sort ty = Z3_mk_bool_sort(ctx);
|
||||
return mk_var(ctx, name, ty);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a fresh boolean variable.
|
||||
*/
|
||||
Z3_ast mk_fresh_bool_var(Z3_context ctx)
|
||||
{
|
||||
return Z3_mk_fresh_const(ctx, "k", Z3_mk_bool_sort(ctx));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create an array with \c num_vars fresh boolean variables.
|
||||
*/
|
||||
Z3_ast * mk_fresh_bool_var_array(Z3_context ctx, unsigned num_vars)
|
||||
{
|
||||
Z3_ast * result = (Z3_ast *) malloc(sizeof(Z3_ast) * num_vars);
|
||||
unsigned i;
|
||||
for (i = 0; i < num_vars; i++) {
|
||||
result[i] = mk_fresh_bool_var(ctx);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Delete array of boolean variables.
|
||||
*/
|
||||
void del_bool_var_array(Z3_ast * arr)
|
||||
{
|
||||
free(arr);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a binary OR.
|
||||
*/
|
||||
Z3_ast mk_binary_or(Z3_context ctx, Z3_ast in_1, Z3_ast in_2)
|
||||
{
|
||||
Z3_ast args[2] = { in_1, in_2 };
|
||||
return Z3_mk_or(ctx, 2, args);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a ternary OR.
|
||||
*/
|
||||
Z3_ast mk_ternary_or(Z3_context ctx, Z3_ast in_1, Z3_ast in_2, Z3_ast in_3)
|
||||
{
|
||||
Z3_ast args[3] = { in_1, in_2, in_3 };
|
||||
return Z3_mk_or(ctx, 3, args);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a binary AND.
|
||||
*/
|
||||
Z3_ast mk_binary_and(Z3_context ctx, Z3_ast in_1, Z3_ast in_2)
|
||||
{
|
||||
Z3_ast args[2] = { in_1, in_2 };
|
||||
return Z3_mk_and(ctx, 2, args);
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Get hard constraints from a SMT-LIB file. We assume hard constraints
|
||||
are formulas preceeded with the keyword :formula.
|
||||
Return an array containing all formulas read by the last Z3_parse_smtlib_file invocation.
|
||||
It will store the number of formulas in num_cnstrs.
|
||||
*/
|
||||
Z3_ast * get_hard_constraints(Z3_context ctx, unsigned * num_cnstrs)
|
||||
{
|
||||
Z3_ast * result;
|
||||
unsigned i;
|
||||
*num_cnstrs = Z3_get_smtlib_num_formulas(ctx);
|
||||
result = (Z3_ast *) malloc(sizeof(Z3_ast) * (*num_cnstrs));
|
||||
for (i = 0; i < *num_cnstrs; i++) {
|
||||
result[i] = Z3_get_smtlib_formula(ctx, i);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Get soft constraints from a SMT-LIB file. We assume soft constraints
|
||||
are formulas preceeded with the keyword :assumption.
|
||||
Return an array containing all assumptions read by the last Z3_parse_smtlib_file invocation.
|
||||
It will store the number of formulas in num_cnstrs.
|
||||
*/
|
||||
Z3_ast * get_soft_constraints(Z3_context ctx, unsigned * num_cnstrs)
|
||||
{
|
||||
Z3_ast * result;
|
||||
unsigned i;
|
||||
*num_cnstrs = Z3_get_smtlib_num_assumptions(ctx);
|
||||
result = (Z3_ast *) malloc(sizeof(Z3_ast) * (*num_cnstrs));
|
||||
for (i = 0; i < *num_cnstrs; i++) {
|
||||
result[i] = Z3_get_smtlib_assumption(ctx, i);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Free the given array of cnstrs that was allocated using get_hard_constraints or get_soft_constraints.
|
||||
*/
|
||||
void free_cnstr_array(Z3_ast * cnstrs)
|
||||
{
|
||||
free(cnstrs);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Assert hard constraints stored in the given array.
|
||||
*/
|
||||
void assert_hard_constraints(Z3_context ctx, unsigned num_cnstrs, Z3_ast * cnstrs)
|
||||
{
|
||||
unsigned i;
|
||||
for (i = 0; i < num_cnstrs; i++) {
|
||||
Z3_assert_cnstr(ctx, cnstrs[i]);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Assert soft constraints stored in the given array.
|
||||
This funtion will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
|
||||
It will also return an array containing these fresh variables.
|
||||
*/
|
||||
Z3_ast * assert_soft_constraints(Z3_context ctx, unsigned num_cnstrs, Z3_ast * cnstrs)
|
||||
{
|
||||
unsigned i;
|
||||
Z3_ast * aux_vars;
|
||||
aux_vars = mk_fresh_bool_var_array(ctx, num_cnstrs);
|
||||
for (i = 0; i < num_cnstrs; i++) {
|
||||
Z3_ast assumption = cnstrs[i];
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, assumption, aux_vars[i]));
|
||||
}
|
||||
return aux_vars;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a full adder with inputs \c in_1, \c in_2 and \c cin.
|
||||
The output of the full adder is stored in \c out, and the carry in \c c_out.
|
||||
*/
|
||||
void mk_full_adder(Z3_context ctx, Z3_ast in_1, Z3_ast in_2, Z3_ast cin, Z3_ast * out, Z3_ast * cout)
|
||||
{
|
||||
*cout = mk_ternary_or(ctx, mk_binary_and(ctx, in_1, in_2), mk_binary_and(ctx, in_1, cin), mk_binary_and(ctx, in_2, cin));
|
||||
*out = Z3_mk_xor(ctx, Z3_mk_xor(ctx, in_1, in_2), cin);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create an adder for inputs of size \c num_bits.
|
||||
The arguments \c in1 and \c in2 are arrays of bits of size \c num_bits.
|
||||
|
||||
\remark \c result must be an array of size \c num_bits + 1.
|
||||
*/
|
||||
void mk_adder(Z3_context ctx, unsigned num_bits, Z3_ast * in_1, Z3_ast * in_2, Z3_ast * result)
|
||||
{
|
||||
Z3_ast cin, cout, out;
|
||||
unsigned i;
|
||||
cin = Z3_mk_false(ctx);
|
||||
for (i = 0; i < num_bits; i++) {
|
||||
mk_full_adder(ctx, in_1[i], in_2[i], cin, &out, &cout);
|
||||
result[i] = out;
|
||||
cin = cout;
|
||||
}
|
||||
result[num_bits] = cout;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Given \c num_ins "numbers" of size \c num_bits stored in \c in.
|
||||
Create floor(num_ins/2) adder circuits. Each circuit is adding two consecutive "numbers".
|
||||
The numbers are stored one after the next in the array \c in.
|
||||
That is, the array \c in has size num_bits * num_ins.
|
||||
Return an array of bits containing \c ceil(num_ins/2) numbers of size \c (num_bits + 1).
|
||||
If num_ins/2 is not an integer, then the last "number" in the output, is the last "number" in \c in with an appended "zero".
|
||||
*/
|
||||
void mk_adder_pairs(Z3_context ctx, unsigned num_bits, unsigned num_ins, Z3_ast * in, unsigned * out_num_ins, Z3_ast * out)
|
||||
{
|
||||
unsigned out_num_bits = num_bits + 1;
|
||||
unsigned i = 0;
|
||||
Z3_ast * _in = in;
|
||||
Z3_ast * _out = out;
|
||||
*out_num_ins = (num_ins % 2 == 0) ? (num_ins / 2) : (num_ins / 2) + 1;
|
||||
for (i = 0; i < num_ins / 2; i++) {
|
||||
mk_adder(ctx, num_bits, _in, _in + num_bits, _out);
|
||||
_in += num_bits;
|
||||
_in += num_bits;
|
||||
_out += out_num_bits;
|
||||
}
|
||||
if (num_ins % 2 != 0) {
|
||||
for (i = 0; i < num_bits; i++) {
|
||||
_out[i] = _in[i];
|
||||
}
|
||||
_out[num_bits] = Z3_mk_false(ctx);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a counter circuit to count the number of "ones" in lits.
|
||||
The function returns an array of bits (i.e. boolean expressions) containing the output of the circuit.
|
||||
The size of the array is stored in out_sz.
|
||||
*/
|
||||
Z3_ast * mk_counter_circuit(Z3_context ctx, unsigned n, Z3_ast * lits, unsigned * out_sz)
|
||||
{
|
||||
unsigned num_ins = n;
|
||||
unsigned num_bits = 1;
|
||||
Z3_ast * aux_1;
|
||||
Z3_ast * aux_2;
|
||||
if (n == 0)
|
||||
return 0;
|
||||
aux_1 = (Z3_ast *) malloc(sizeof(Z3_ast) * (n + 1));
|
||||
aux_2 = (Z3_ast *) malloc(sizeof(Z3_ast) * (n + 1));
|
||||
memcpy(aux_1, lits, sizeof(Z3_ast) * n);
|
||||
while (num_ins > 1) {
|
||||
unsigned new_num_ins;
|
||||
Z3_ast * tmp;
|
||||
mk_adder_pairs(ctx, num_bits, num_ins, aux_1, &new_num_ins, aux_2);
|
||||
num_ins = new_num_ins;
|
||||
num_bits++;
|
||||
#ifdef MAXSAT_DEBUG
|
||||
{
|
||||
unsigned i;
|
||||
printf("num_bits: %d, num_ins: %d \n", num_bits, num_ins);
|
||||
for (i = 0; i < num_ins * num_bits; i++) {
|
||||
printf("bit %d:\n%s\n", i, Z3_ast_to_string(ctx, aux_2[i]));
|
||||
}
|
||||
printf("-----------\n");
|
||||
}
|
||||
#endif
|
||||
tmp = aux_1;
|
||||
aux_1 = aux_2;
|
||||
aux_2 = tmp;
|
||||
}
|
||||
*out_sz = num_bits;
|
||||
free(aux_2);
|
||||
return aux_1;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return the \c idx bit of \c val.
|
||||
*/
|
||||
int get_bit(unsigned val, unsigned idx)
|
||||
{
|
||||
unsigned mask = 1 << (idx & 31);
|
||||
return (val & mask) != 0;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Given an integer val encoded in n bits (boolean variables), assert the constraint that val <= k.
|
||||
*/
|
||||
void assert_le_k(Z3_context ctx, unsigned n, Z3_ast * val, unsigned k)
|
||||
{
|
||||
Z3_ast i1, i2, not_val, out;
|
||||
unsigned idx;
|
||||
not_val = Z3_mk_not(ctx, val[0]);
|
||||
if (get_bit(k, 0))
|
||||
out = Z3_mk_true(ctx);
|
||||
else
|
||||
out = not_val;
|
||||
for (idx = 1; idx < n; idx++) {
|
||||
not_val = Z3_mk_not(ctx, val[idx]);
|
||||
if (get_bit(k, idx)) {
|
||||
i1 = not_val;
|
||||
i2 = out;
|
||||
}
|
||||
else {
|
||||
i1 = Z3_mk_false(ctx);
|
||||
i2 = Z3_mk_false(ctx);
|
||||
}
|
||||
out = mk_ternary_or(ctx, i1, i2, mk_binary_and(ctx, not_val, out));
|
||||
}
|
||||
// printf("at-most-k:\n%s\n", Z3_ast_to_string(ctx, out));
|
||||
Z3_assert_cnstr(ctx, out);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Assert that at most \c k literals in \c lits can be true,
|
||||
where \c n is the number of literals in lits.
|
||||
|
||||
We use a simple encoding using an adder (counter).
|
||||
An interesting exercise consists in implementing more sophisticated encodings.
|
||||
*/
|
||||
void assert_at_most_k(Z3_context ctx, unsigned n, Z3_ast * lits, unsigned k)
|
||||
{
|
||||
Z3_ast * counter_bits;
|
||||
unsigned counter_bits_sz;
|
||||
if (k >= n || n <= 1)
|
||||
return; /* nothing to be done */
|
||||
counter_bits = mk_counter_circuit(ctx, n, lits, &counter_bits_sz);
|
||||
assert_le_k(ctx, counter_bits_sz, counter_bits, k);
|
||||
del_bool_var_array(counter_bits);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Assert that at most one literal in \c lits can be true,
|
||||
where \c n is the number of literals in lits.
|
||||
*/
|
||||
void assert_at_most_one(Z3_context ctx, unsigned n, Z3_ast * lits)
|
||||
{
|
||||
assert_at_most_k(ctx, n, lits, 1);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Small test for the at-most-one constraint.
|
||||
*/
|
||||
void tst_at_most_one()
|
||||
{
|
||||
Z3_context ctx = mk_context();
|
||||
Z3_ast k1 = mk_bool_var(ctx, "k1");
|
||||
Z3_ast k2 = mk_bool_var(ctx, "k2");
|
||||
Z3_ast k3 = mk_bool_var(ctx, "k3");
|
||||
Z3_ast k4 = mk_bool_var(ctx, "k4");
|
||||
Z3_ast k5 = mk_bool_var(ctx, "k5");
|
||||
Z3_ast k6 = mk_bool_var(ctx, "k6");
|
||||
Z3_ast args1[5] = { k1, k2, k3, k4, k5 };
|
||||
Z3_ast args2[3] = { k4, k5, k6 };
|
||||
Z3_model m = 0;
|
||||
Z3_lbool result;
|
||||
printf("testing at-most-one constraint\n");
|
||||
assert_at_most_one(ctx, 5, args1);
|
||||
assert_at_most_one(ctx, 3, args2);
|
||||
printf("it must be sat...\n");
|
||||
result = Z3_check_and_get_model(ctx, &m);
|
||||
if (result != Z3_L_TRUE)
|
||||
error("BUG");
|
||||
printf("model:\n%s\n", Z3_model_to_string(ctx, m));
|
||||
if (m) {
|
||||
Z3_del_model(ctx, m);
|
||||
}
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, k2, k3));
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, k1, k6));
|
||||
printf("it must be sat...\n");
|
||||
result = Z3_check_and_get_model(ctx, &m);
|
||||
if (result != Z3_L_TRUE)
|
||||
error("BUG");
|
||||
printf("model:\n%s\n", Z3_model_to_string(ctx, m));
|
||||
if (m) {
|
||||
Z3_del_model(ctx, m);
|
||||
}
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, k4, k5));
|
||||
printf("it must be unsat...\n");
|
||||
result = Z3_check_and_get_model(ctx, &m);
|
||||
if (result != Z3_L_FALSE)
|
||||
error("BUG");
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return the number of soft-constraints that were disable by the given model.
|
||||
A soft-constraint was disabled if the associated auxiliary variable was assigned to true.
|
||||
*/
|
||||
unsigned get_num_disabled_soft_constraints(Z3_context ctx, Z3_model m, unsigned num_soft_cnstrs, Z3_ast * aux_vars)
|
||||
{
|
||||
unsigned i;
|
||||
unsigned num_disabled = 0;
|
||||
Z3_ast t = Z3_mk_true(ctx);
|
||||
for (i = 0; i < num_soft_cnstrs; i++) {
|
||||
Z3_ast val;
|
||||
if (Z3_eval(ctx, m, aux_vars[i], &val) == Z3_TRUE) {
|
||||
// printf("%s", Z3_ast_to_string(ctx, aux_vars[i]));
|
||||
// printf(" -> %s\n", Z3_ast_to_string(ctx, val));
|
||||
if (Z3_is_eq_ast(ctx, val, t)) {
|
||||
num_disabled++;
|
||||
}
|
||||
}
|
||||
}
|
||||
return num_disabled;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Naive maxsat procedure based on linear search and at-most-k
|
||||
constraint. Return the number of soft-constraints that can be
|
||||
satisfied. Return -1 if the hard-constraints cannot be
|
||||
satisfied. That is, the formula cannot be satisfied even if all
|
||||
soft-constraints are ignored.
|
||||
|
||||
Exercise: use binary search to implement MaxSAT.
|
||||
Hint: you will need to use an answer literal to retract the at-most-k constraint.
|
||||
*/
|
||||
int naive_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs)
|
||||
{
|
||||
Z3_ast * aux_vars;
|
||||
Z3_lbool is_sat;
|
||||
unsigned r, k;
|
||||
assert_hard_constraints(ctx, num_hard_cnstrs, hard_cnstrs);
|
||||
printf("checking whether hard constraints are satisfiable...\n");
|
||||
is_sat = Z3_check(ctx);
|
||||
if (is_sat == Z3_L_FALSE) {
|
||||
// It is not possible to make the formula satisfiable even when ignoring all soft constraints.
|
||||
return -1;
|
||||
}
|
||||
if (num_soft_cnstrs == 0)
|
||||
return 0; // nothing to be done...
|
||||
aux_vars = assert_soft_constraints(ctx, num_soft_cnstrs, soft_cnstrs);
|
||||
// Perform linear search.
|
||||
r = 0;
|
||||
k = num_soft_cnstrs - 1;
|
||||
for (;;) {
|
||||
Z3_model m;
|
||||
unsigned num_disabled;
|
||||
// at most k soft-constraints can be ignored.
|
||||
printf("checking whether at-most %d soft-constraints can be ignored.\n", k);
|
||||
assert_at_most_k(ctx, num_soft_cnstrs, aux_vars, k);
|
||||
is_sat = Z3_check_and_get_model(ctx, &m);
|
||||
if (is_sat == Z3_L_FALSE) {
|
||||
printf("unsat\n");
|
||||
return num_soft_cnstrs - k - 1;
|
||||
}
|
||||
num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars);
|
||||
if (num_disabled > k) {
|
||||
error("BUG");
|
||||
}
|
||||
if (m) {
|
||||
Z3_del_model(ctx, m);
|
||||
}
|
||||
printf("sat\n");
|
||||
k = num_disabled;
|
||||
if (k == 0) {
|
||||
// it was possible to satisfy all soft-constraints.
|
||||
return num_soft_cnstrs;
|
||||
}
|
||||
k--;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Implement one step of the Fu&Malik algorithm.
|
||||
See fu_malik_maxsat function for more details.
|
||||
|
||||
Input: soft constraints + aux-vars (aka answer literals)
|
||||
Output: done/not-done when not done return updated set of soft-constraints and aux-vars.
|
||||
- if SAT --> terminates
|
||||
- if UNSAT
|
||||
* compute unsat core
|
||||
* add blocking variable to soft-constraints in the core
|
||||
- replace soft-constraint with the one with the blocking variable
|
||||
- we should also add an aux-var
|
||||
- replace aux-var with a new one
|
||||
* add at-most-one constraint with blocking
|
||||
*/
|
||||
int fu_malik_maxsat_step(Z3_context ctx, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs, Z3_ast * aux_vars)
|
||||
{
|
||||
// create assumptions
|
||||
Z3_ast * assumptions = (Z3_ast*) malloc(sizeof(Z3_ast) * num_soft_cnstrs);
|
||||
Z3_ast * core = (Z3_ast*) malloc(sizeof(Z3_ast) * num_soft_cnstrs);
|
||||
unsigned core_size;
|
||||
Z3_ast dummy_proof; // we don't care about proofs in this example
|
||||
Z3_model m;
|
||||
Z3_lbool is_sat;
|
||||
unsigned i = 0;
|
||||
for (i = 0; i < num_soft_cnstrs; i++) {
|
||||
// Recall that we asserted (soft_cnstrs[i] \/ aux_vars[i])
|
||||
// So using (NOT aux_vars[i]) as an assumption we are actually forcing the soft_cnstrs[i] to be considered.
|
||||
assumptions[i] = Z3_mk_not(ctx, aux_vars[i]);
|
||||
core[i] = 0;
|
||||
}
|
||||
|
||||
is_sat = Z3_check_assumptions(ctx, num_soft_cnstrs, assumptions, &m, &dummy_proof, &core_size, core);
|
||||
if (is_sat != Z3_L_FALSE) {
|
||||
return 1; // done
|
||||
}
|
||||
else {
|
||||
Z3_ast * block_vars = (Z3_ast*) malloc(sizeof(Z3_ast) * core_size);
|
||||
unsigned k = 0;
|
||||
// update soft-constraints and aux_vars
|
||||
for (i = 0; i < num_soft_cnstrs; i++) {
|
||||
unsigned j;
|
||||
// check whether assumption[i] is in the core or not
|
||||
for (j = 0; j < core_size; j++) {
|
||||
if (assumptions[i] == core[j])
|
||||
break;
|
||||
}
|
||||
if (j < core_size) {
|
||||
// assumption[i] is in the unsat core... so soft_cnstrs[i] is in the unsat core
|
||||
Z3_ast block_var = mk_fresh_bool_var(ctx);
|
||||
Z3_ast new_aux_var = mk_fresh_bool_var(ctx);
|
||||
soft_cnstrs[i] = mk_binary_or(ctx, soft_cnstrs[i], block_var);
|
||||
aux_vars[i] = new_aux_var;
|
||||
block_vars[k] = block_var;
|
||||
k++;
|
||||
// Add new constraint containing the block variable.
|
||||
// Note that we are using the new auxiliary variable to be able to use it as an assumption.
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, soft_cnstrs[i], new_aux_var));
|
||||
}
|
||||
}
|
||||
assert_at_most_one(ctx, k, block_vars);
|
||||
return 0; // not done.
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Fu & Malik procedure for MaxSAT. This procedure is based on
|
||||
unsat core extraction and the at-most-one constraint.
|
||||
|
||||
Return the number of soft-constraints that can be
|
||||
satisfied. Return -1 if the hard-constraints cannot be
|
||||
satisfied. That is, the formula cannot be satisfied even if all
|
||||
soft-constraints are ignored.
|
||||
|
||||
For more information on the Fu & Malik procedure:
|
||||
|
||||
Z. Fu and S. Malik, On solving the partial MAX-SAT problem, in International
|
||||
Conference on Theory and Applications of Satisfiability Testing, 2006.
|
||||
*/
|
||||
int fu_malik_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs)
|
||||
{
|
||||
Z3_ast * aux_vars;
|
||||
Z3_lbool is_sat;
|
||||
unsigned k;
|
||||
assert_hard_constraints(ctx, num_hard_cnstrs, hard_cnstrs);
|
||||
printf("checking whether hard constraints are satisfiable...\n");
|
||||
is_sat = Z3_check(ctx);
|
||||
if (is_sat == Z3_L_FALSE) {
|
||||
// It is not possible to make the formula satisfiable even when ignoring all soft constraints.
|
||||
return -1;
|
||||
}
|
||||
if (num_soft_cnstrs == 0)
|
||||
return 0; // nothing to be done...
|
||||
/*
|
||||
Fu&Malik algorithm is based on UNSAT-core extraction.
|
||||
We accomplish that using auxiliary variables (aka answer literals).
|
||||
*/
|
||||
aux_vars = assert_soft_constraints(ctx, num_soft_cnstrs, soft_cnstrs);
|
||||
k = 0;
|
||||
for (;;) {
|
||||
printf("iteration %d\n", k);
|
||||
if (fu_malik_maxsat_step(ctx, num_soft_cnstrs, soft_cnstrs, aux_vars)) {
|
||||
return num_soft_cnstrs - k;
|
||||
}
|
||||
k++;
|
||||
}
|
||||
}
|
||||
|
||||
#define NAIVE_MAXSAT 0
|
||||
#define FU_MALIK_MAXSAT 1
|
||||
|
||||
/**
|
||||
\brief Finds the maximal number of assumptions that can be satisfied.
|
||||
An assumption is any formula preceeded with the :assumption keyword.
|
||||
"Hard" constraints can be supported by using the :formula keyword.
|
||||
|
||||
Input: file in SMT-LIB format, and MaxSAT algorithm to be used: 0 - Naive, 1 - Fu&Malik's algo.
|
||||
Output: the maximum number of assumptions that can be satisfied.
|
||||
*/
|
||||
int smtlib_maxsat(char * file_name, int approach)
|
||||
{
|
||||
Z3_context ctx;
|
||||
unsigned num_hard_cnstrs, num_soft_cnstrs;
|
||||
Z3_ast * hard_cnstrs, * soft_cnstrs;
|
||||
unsigned result;
|
||||
ctx = mk_context();
|
||||
Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0);
|
||||
hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs);
|
||||
soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs);
|
||||
switch (approach) {
|
||||
case NAIVE_MAXSAT:
|
||||
result = naive_maxsat(ctx, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);
|
||||
break;
|
||||
case FU_MALIK_MAXSAT:
|
||||
result = fu_malik_maxsat(ctx, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);
|
||||
break;
|
||||
default:
|
||||
/* Exercise: implement your own MaxSAT algorithm.*/
|
||||
error("Not implemented yet.");
|
||||
break;
|
||||
}
|
||||
free_cnstr_array(hard_cnstrs);
|
||||
free_cnstr_array(soft_cnstrs);
|
||||
return result;
|
||||
}
|
||||
|
||||
int main(int argc, char * argv[]) {
|
||||
#if 1
|
||||
int r;
|
||||
if (argc != 2) {
|
||||
error("usage: maxsat [filename.smt].");
|
||||
}
|
||||
r = smtlib_maxsat(argv[1], FU_MALIK_MAXSAT);
|
||||
printf("result: %d\n", r);
|
||||
#else
|
||||
tst_at_most_one();
|
||||
#endif
|
||||
return 0;
|
||||
}
|
||||
|
||||
/*@}*/
|
||||
|
||||
295
src/examples/maxsat/maxsat.vcxproj
Normal file
295
src/examples/maxsat/maxsat.vcxproj
Normal file
|
|
@ -0,0 +1,295 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
|
||||
<ItemGroup Label="ProjectConfigurations">
|
||||
<ProjectConfiguration Include="commercial|Win32">
|
||||
<Configuration>commercial</Configuration>
|
||||
<Platform>Win32</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="commercial|x64">
|
||||
<Configuration>commercial</Configuration>
|
||||
<Platform>x64</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="Debug|Win32">
|
||||
<Configuration>Debug</Configuration>
|
||||
<Platform>Win32</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="Debug|x64">
|
||||
<Configuration>Debug</Configuration>
|
||||
<Platform>x64</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="external|Win32">
|
||||
<Configuration>external</Configuration>
|
||||
<Platform>Win32</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="external|x64">
|
||||
<Configuration>external</Configuration>
|
||||
<Platform>x64</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="Release|Win32">
|
||||
<Configuration>Release</Configuration>
|
||||
<Platform>Win32</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="Release|x64">
|
||||
<Configuration>Release</Configuration>
|
||||
<Platform>x64</Platform>
|
||||
</ProjectConfiguration>
|
||||
</ItemGroup>
|
||||
<PropertyGroup Label="Globals">
|
||||
<ProjectGuid>{7C154132-AAAB-4F60-B652-F8C51A63D244}</ProjectGuid>
|
||||
<Keyword>Win32Proj</Keyword>
|
||||
<RootNamespace>maxsat</RootNamespace>
|
||||
</PropertyGroup>
|
||||
<Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<UseDebugLibraries>true</UseDebugLibraries>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<UseDebugLibraries>true</UseDebugLibraries>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<UseDebugLibraries>false</UseDebugLibraries>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<UseDebugLibraries>false</UseDebugLibraries>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='external|Win32'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<UseDebugLibraries>false</UseDebugLibraries>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='external|x64'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<UseDebugLibraries>false</UseDebugLibraries>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<UseDebugLibraries>false</UseDebugLibraries>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='commercial|x64'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<UseDebugLibraries>false</UseDebugLibraries>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />
|
||||
<ImportGroup Label="ExtensionSettings">
|
||||
</ImportGroup>
|
||||
<ImportGroup Label="PropertySheets" Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Label="PropertySheets" Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='external|Win32'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='external|x64'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='commercial|x64'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<PropertyGroup Label="UserMacros" />
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">
|
||||
<LinkIncremental>true</LinkIncremental>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">
|
||||
<LinkIncremental>true</LinkIncremental>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">
|
||||
<LinkIncremental>false</LinkIncremental>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'">
|
||||
<LinkIncremental>false</LinkIncremental>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='external|Win32'">
|
||||
<LinkIncremental>false</LinkIncremental>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='external|x64'">
|
||||
<LinkIncremental>false</LinkIncremental>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'">
|
||||
<LinkIncremental>false</LinkIncremental>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='commercial|x64'">
|
||||
<LinkIncremental>false</LinkIncremental>
|
||||
</PropertyGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">
|
||||
<ClCompile>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<Optimization>Disabled</Optimization>
|
||||
<PreprocessorDefinitions>WIN32;_DEBUG;_CONSOLE;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<AdditionalIncludeDirectories>..\lib</AdditionalIncludeDirectories>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<RandomizedBaseAddress>false</RandomizedBaseAddress>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">
|
||||
<ClCompile>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<Optimization>Disabled</Optimization>
|
||||
<PreprocessorDefinitions>WIN32;_DEBUG;_CONSOLE;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<AdditionalIncludeDirectories>..\lib</AdditionalIncludeDirectories>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<RandomizedBaseAddress>false</RandomizedBaseAddress>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">
|
||||
<ClCompile>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<Optimization>MaxSpeed</Optimization>
|
||||
<FunctionLevelLinking>true</FunctionLevelLinking>
|
||||
<IntrinsicFunctions>true</IntrinsicFunctions>
|
||||
<PreprocessorDefinitions>WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<AdditionalIncludeDirectories>..\lib</AdditionalIncludeDirectories>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'">
|
||||
<ClCompile>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<Optimization>MaxSpeed</Optimization>
|
||||
<FunctionLevelLinking>true</FunctionLevelLinking>
|
||||
<IntrinsicFunctions>true</IntrinsicFunctions>
|
||||
<PreprocessorDefinitions>WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<AdditionalIncludeDirectories>..\lib</AdditionalIncludeDirectories>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='external|Win32'">
|
||||
<ClCompile>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<Optimization>MaxSpeed</Optimization>
|
||||
<FunctionLevelLinking>true</FunctionLevelLinking>
|
||||
<IntrinsicFunctions>true</IntrinsicFunctions>
|
||||
<PreprocessorDefinitions>WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<AdditionalIncludeDirectories>..\lib</AdditionalIncludeDirectories>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='external|x64'">
|
||||
<ClCompile>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<Optimization>MaxSpeed</Optimization>
|
||||
<FunctionLevelLinking>true</FunctionLevelLinking>
|
||||
<IntrinsicFunctions>true</IntrinsicFunctions>
|
||||
<PreprocessorDefinitions>_AMD64_;WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<AdditionalIncludeDirectories>..\lib</AdditionalIncludeDirectories>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'">
|
||||
<ClCompile>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<Optimization>MaxSpeed</Optimization>
|
||||
<FunctionLevelLinking>true</FunctionLevelLinking>
|
||||
<IntrinsicFunctions>true</IntrinsicFunctions>
|
||||
<PreprocessorDefinitions>WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<AdditionalIncludeDirectories>..\lib</AdditionalIncludeDirectories>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='commercial|x64'">
|
||||
<ClCompile>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<Optimization>MaxSpeed</Optimization>
|
||||
<FunctionLevelLinking>true</FunctionLevelLinking>
|
||||
<IntrinsicFunctions>true</IntrinsicFunctions>
|
||||
<PreprocessorDefinitions>WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<AdditionalIncludeDirectories>..\lib</AdditionalIncludeDirectories>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemGroup>
|
||||
<ClCompile Include="maxsat.c" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<ProjectReference Include="..\lib\lib.vcxproj">
|
||||
<Project>{4a7e5a93-19d8-4382-8950-fb2edec7a76e}</Project>
|
||||
<Private>true</Private>
|
||||
<ReferenceOutputAssembly>false</ReferenceOutputAssembly>
|
||||
<CopyLocalSatelliteAssemblies>false</CopyLocalSatelliteAssemblies>
|
||||
<LinkLibraryDependencies>true</LinkLibraryDependencies>
|
||||
<UseLibraryDependencyInputs>false</UseLibraryDependencyInputs>
|
||||
</ProjectReference>
|
||||
</ItemGroup>
|
||||
<Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />
|
||||
<ImportGroup Label="ExtensionTargets">
|
||||
</ImportGroup>
|
||||
</Project>
|
||||
25
src/examples/test_capi/README.txt
Normal file
25
src/examples/test_capi/README.txt
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
WARNING: this example still uses the old Z3 (version 3.x) C API.
|
||||
The current version is backward compatible.
|
||||
|
||||
1) Using Visual Studio (with Z3 source code release)
|
||||
|
||||
The test_capi application is automatically built when the z3-prover.sln is processed. The following command should be used to compile z3-prover.sln in the Z3 root directory
|
||||
|
||||
msbuild /p:configuration=external
|
||||
|
||||
The maxsat executable is located at
|
||||
|
||||
..\external\test_capi
|
||||
|
||||
2) Using gcc (on Linux or OSX)
|
||||
|
||||
Use 'build.sh' to build the test application using gcc.
|
||||
|
||||
You must install Z3 before running this example.
|
||||
To install Z3, execute the following command in the Z3 root directory.
|
||||
|
||||
sudo make install
|
||||
|
||||
Use 'build.sh' to build the test application using gcc.
|
||||
It generates the executable 'test_capi'.
|
||||
|
||||
9
src/examples/test_capi/build.sh
Executable file
9
src/examples/test_capi/build.sh
Executable file
|
|
@ -0,0 +1,9 @@
|
|||
if gcc -fopenmp -o test_capi test_capi.c -lz3; then
|
||||
echo "test_capi applicatio was successfully compiled."
|
||||
echo "To try it, execute:"
|
||||
echo " ./test_capi"
|
||||
else
|
||||
echo "You must install Z3 before compiling this example."
|
||||
echo "To install Z3, execute the following command in the Z3 root directory."
|
||||
echo " sudo make install"
|
||||
fi
|
||||
2695
src/examples/test_capi/test_capi.c
Normal file
2695
src/examples/test_capi/test_capi.c
Normal file
File diff suppressed because it is too large
Load diff
430
src/examples/test_capi/test_capi.vcxproj
Normal file
430
src/examples/test_capi/test_capi.vcxproj
Normal file
|
|
@ -0,0 +1,430 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
|
||||
<ItemGroup Label="ProjectConfigurations">
|
||||
<ProjectConfiguration Include="commercial|Win32">
|
||||
<Configuration>commercial</Configuration>
|
||||
<Platform>Win32</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="commercial|x64">
|
||||
<Configuration>commercial</Configuration>
|
||||
<Platform>x64</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="Debug|Win32">
|
||||
<Configuration>Debug</Configuration>
|
||||
<Platform>Win32</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="Debug|x64">
|
||||
<Configuration>Debug</Configuration>
|
||||
<Platform>x64</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="external|Win32">
|
||||
<Configuration>external</Configuration>
|
||||
<Platform>Win32</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="external|x64">
|
||||
<Configuration>external</Configuration>
|
||||
<Platform>x64</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="release_mt|Win32">
|
||||
<Configuration>release_mt</Configuration>
|
||||
<Platform>Win32</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="release_mt|x64">
|
||||
<Configuration>release_mt</Configuration>
|
||||
<Platform>x64</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="Release|Win32">
|
||||
<Configuration>Release</Configuration>
|
||||
<Platform>Win32</Platform>
|
||||
</ProjectConfiguration>
|
||||
<ProjectConfiguration Include="Release|x64">
|
||||
<Configuration>Release</Configuration>
|
||||
<Platform>x64</Platform>
|
||||
</ProjectConfiguration>
|
||||
</ItemGroup>
|
||||
<PropertyGroup Label="Globals">
|
||||
<ProjectGuid>{9E76526D-EDA2-4B88-9616-A8FC08F31071}</ProjectGuid>
|
||||
<RootNamespace>test_capi</RootNamespace>
|
||||
<Keyword>Win32Proj</Keyword>
|
||||
</PropertyGroup>
|
||||
<Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='external|Win32'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='external|x64'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='commercial|x64'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
<WholeProgramOptimization>true</WholeProgramOptimization>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'" Label="Configuration">
|
||||
<ConfigurationType>Application</ConfigurationType>
|
||||
<CharacterSet>Unicode</CharacterSet>
|
||||
</PropertyGroup>
|
||||
<Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />
|
||||
<ImportGroup Label="ExtensionSettings">
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='external|Win32'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='external|x64'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='commercial|x64'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<ImportGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'" Label="PropertySheets">
|
||||
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
|
||||
</ImportGroup>
|
||||
<PropertyGroup Label="UserMacros" />
|
||||
<PropertyGroup>
|
||||
<_ProjectFileVersion>10.0.30319.1</_ProjectFileVersion>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">$(SolutionDir)$(Configuration)\</OutDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">$(Configuration)\</IntDir>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">true</LinkIncremental>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">$(SolutionDir)$(Platform)\$(Configuration)\</OutDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">$(Platform)\$(Configuration)\</IntDir>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">true</LinkIncremental>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'">$(SolutionDir)$(Configuration)\</OutDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'">$(Configuration)\</IntDir>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'">false</LinkIncremental>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'">$(SolutionDir)$(Platform)\$(Configuration)\</OutDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'">$(Platform)\$(Configuration)\</IntDir>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'">false</LinkIncremental>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">$(SolutionDir)$(Configuration)\</OutDir>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='external|Win32'">$(SolutionDir)$(Configuration)\</OutDir>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'">$(SolutionDir)$(Configuration)\</OutDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">$(Configuration)\</IntDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='external|Win32'">$(Configuration)\</IntDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'">$(Configuration)\</IntDir>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">false</LinkIncremental>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='external|Win32'">false</LinkIncremental>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'">false</LinkIncremental>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='Release|x64'">$(SolutionDir)$(Platform)\$(Configuration)\</OutDir>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='external|x64'">$(SolutionDir)$(Platform)\$(Configuration)\</OutDir>
|
||||
<OutDir Condition="'$(Configuration)|$(Platform)'=='commercial|x64'">$(SolutionDir)$(Platform)\$(Configuration)\</OutDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='Release|x64'">$(Platform)\$(Configuration)\</IntDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='external|x64'">$(Platform)\$(Configuration)\</IntDir>
|
||||
<IntDir Condition="'$(Configuration)|$(Platform)'=='commercial|x64'">$(Platform)\$(Configuration)\</IntDir>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='Release|x64'">false</LinkIncremental>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='external|x64'">false</LinkIncremental>
|
||||
<LinkIncremental Condition="'$(Configuration)|$(Platform)'=='commercial|x64'">false</LinkIncremental>
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'" />
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='Debug|x64'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='Debug|x64'" />
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'" />
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'" />
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='external|Win32'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='Release|Win32'" />
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='external|Win32'" />
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='Release|Win32'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='external|Win32'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'" />
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='Release|x64'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='external|x64'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRuleSet Condition="'$(Configuration)|$(Platform)'=='commercial|x64'">AllRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='Release|x64'" />
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='external|x64'" />
|
||||
<CodeAnalysisRules Condition="'$(Configuration)|$(Platform)'=='commercial|x64'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='Release|x64'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='external|x64'" />
|
||||
<CodeAnalysisRuleAssemblies Condition="'$(Configuration)|$(Platform)'=='commercial|x64'" />
|
||||
</PropertyGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">
|
||||
<ClCompile>
|
||||
<Optimization>Disabled</Optimization>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;_CONSOLE;Z3DEBUG;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<MinimalRebuild>true</MinimalRebuild>
|
||||
<BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>
|
||||
<RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>EditAndContinue</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<RandomizedBaseAddress>false</RandomizedBaseAddress>
|
||||
<DataExecutionPrevention>
|
||||
</DataExecutionPrevention>
|
||||
<TargetMachine>MachineX86</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">
|
||||
<Midl>
|
||||
<TargetEnvironment>X64</TargetEnvironment>
|
||||
</Midl>
|
||||
<ClCompile>
|
||||
<Optimization>Disabled</Optimization>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;_CONSOLE;Z3DEBUG;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<MinimalRebuild>true</MinimalRebuild>
|
||||
<BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>
|
||||
<RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<TargetMachine>MachineX64</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'">
|
||||
<ClCompile>
|
||||
<WholeProgramOptimization>false</WholeProgramOptimization>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;NDEBUG;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<RuntimeLibrary>MultiThreaded</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<AdditionalDependencies>psapi.lib;%(AdditionalDependencies)</AdditionalDependencies>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<StackReserveSize>8388608</StackReserveSize>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<RandomizedBaseAddress>false</RandomizedBaseAddress>
|
||||
<DataExecutionPrevention>
|
||||
</DataExecutionPrevention>
|
||||
<TargetMachine>MachineX86</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'">
|
||||
<Midl>
|
||||
<TargetEnvironment>X64</TargetEnvironment>
|
||||
</Midl>
|
||||
<ClCompile>
|
||||
<WholeProgramOptimization>false</WholeProgramOptimization>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;NDEBUG;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<RuntimeLibrary>MultiThreaded</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<AdditionalDependencies>psapi.lib;%(AdditionalDependencies)</AdditionalDependencies>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<StackReserveSize>8388608</StackReserveSize>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<TargetMachine>MachineX64</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">
|
||||
<ClCompile>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<RandomizedBaseAddress>false</RandomizedBaseAddress>
|
||||
<DataExecutionPrevention>
|
||||
</DataExecutionPrevention>
|
||||
<TargetMachine>MachineX86</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='external|Win32'">
|
||||
<ClCompile>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<RandomizedBaseAddress>false</RandomizedBaseAddress>
|
||||
<DataExecutionPrevention>
|
||||
</DataExecutionPrevention>
|
||||
<TargetMachine>MachineX86</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'">
|
||||
<ClCompile>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<RandomizedBaseAddress>false</RandomizedBaseAddress>
|
||||
<DataExecutionPrevention>
|
||||
</DataExecutionPrevention>
|
||||
<TargetMachine>MachineX86</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'">
|
||||
<Midl>
|
||||
<TargetEnvironment>X64</TargetEnvironment>
|
||||
</Midl>
|
||||
<ClCompile>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<TargetMachine>MachineX64</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='external|x64'">
|
||||
<Midl>
|
||||
<TargetEnvironment>X64</TargetEnvironment>
|
||||
</Midl>
|
||||
<ClCompile>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<TargetMachine>MachineX64</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='commercial|x64'">
|
||||
<Midl>
|
||||
<TargetEnvironment>X64</TargetEnvironment>
|
||||
</Midl>
|
||||
<ClCompile>
|
||||
<AdditionalIncludeDirectories>..\lib;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
|
||||
<PreprocessorDefinitions>WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
|
||||
<RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>
|
||||
<PrecompiledHeader>
|
||||
</PrecompiledHeader>
|
||||
<WarningLevel>Level3</WarningLevel>
|
||||
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
|
||||
</ClCompile>
|
||||
<Link>
|
||||
<GenerateDebugInformation>true</GenerateDebugInformation>
|
||||
<SubSystem>Console</SubSystem>
|
||||
<OptimizeReferences>true</OptimizeReferences>
|
||||
<EnableCOMDATFolding>true</EnableCOMDATFolding>
|
||||
<TargetMachine>MachineX64</TargetMachine>
|
||||
</Link>
|
||||
</ItemDefinitionGroup>
|
||||
<ItemGroup>
|
||||
<ClCompile Include="test_capi.c" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<ProjectReference Include="..\dll\dll.vcxproj">
|
||||
<Project>{0bf8cb94-61c7-4545-ae55-c58d858aa8b6}</Project>
|
||||
<ReferenceOutputAssembly>false</ReferenceOutputAssembly>
|
||||
</ProjectReference>
|
||||
<ProjectReference Include="..\lib\lib.vcxproj">
|
||||
<Project>{4a7e5a93-19d8-4382-8950-fb2edec7a76e}</Project>
|
||||
<ReferenceOutputAssembly>false</ReferenceOutputAssembly>
|
||||
</ProjectReference>
|
||||
</ItemGroup>
|
||||
<Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />
|
||||
<ImportGroup Label="ExtensionTargets">
|
||||
</ImportGroup>
|
||||
</Project>
|
||||
Loading…
Add table
Add a link
Reference in a new issue