mirror of
https://github.com/Z3Prover/z3
synced 2025-07-19 19:02:02 +00:00
commit
f2c263001c
5 changed files with 5 additions and 5 deletions
|
@ -475,7 +475,7 @@ namespace Microsoft.Z3
|
||||||
/// Update a datatype field at expression t with value v.
|
/// Update a datatype field at expression t with value v.
|
||||||
/// The function performs a record update at t. The field
|
/// The function performs a record update at t. The field
|
||||||
/// that is passed in as argument is updated with value v,
|
/// that is passed in as argument is updated with value v,
|
||||||
/// the remainig fields of t are unchanged.
|
/// the remaining fields of t are unchanged.
|
||||||
/// </summary>
|
/// </summary>
|
||||||
public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
|
public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
|
||||||
{
|
{
|
||||||
|
|
|
@ -25,7 +25,7 @@ using System.Linq;
|
||||||
namespace Microsoft.Z3
|
namespace Microsoft.Z3
|
||||||
{
|
{
|
||||||
/// <summary>
|
/// <summary>
|
||||||
/// Object for managing optimizization context
|
/// Object for managing optimization context
|
||||||
/// </summary>
|
/// </summary>
|
||||||
public class Optimize : Z3Object
|
public class Optimize : Z3Object
|
||||||
{
|
{
|
||||||
|
|
|
@ -4,7 +4,7 @@ instructions are as follows:
|
||||||
|
|
||||||
In the project properties of Microsoft.Z3.csproj:
|
In the project properties of Microsoft.Z3.csproj:
|
||||||
- Under 'Application': Change Target framework to .NET Framework 3.5
|
- Under 'Application': Change Target framework to .NET Framework 3.5
|
||||||
- Under 'Build': Add FRAMEWORK_LT_4 to the condidional compilation symbols
|
- Under 'Build': Add FRAMEWORK_LT_4 to the conditional compilation symbols
|
||||||
- Remove the reference to System.Numerics
|
- Remove the reference to System.Numerics
|
||||||
- Install the NuGet Package "Microsoft Code Contracts for Net3.5":
|
- Install the NuGet Package "Microsoft Code Contracts for Net3.5":
|
||||||
In the Package Manager Console enter Install-Package Code.Contract
|
In the Package Manager Console enter Install-Package Code.Contract
|
||||||
|
|
|
@ -253,7 +253,7 @@ namespace qe {
|
||||||
/**
|
/**
|
||||||
\brief Guarded definitions.
|
\brief Guarded definitions.
|
||||||
|
|
||||||
A realizer to a an existential quantified formula is a disjunction
|
A realizer to an existential quantified formula is a disjunction
|
||||||
together with a substitution from the existentially quantified variables
|
together with a substitution from the existentially quantified variables
|
||||||
to terms such that:
|
to terms such that:
|
||||||
1. The original formula (exists (vars) fml) is equivalent to the disjunction of guards.
|
1. The original formula (exists (vars) fml) is equivalent to the disjunction of guards.
|
||||||
|
|
|
@ -18,7 +18,7 @@ Copyright (c) 2015 Microsoft Corporation
|
||||||
// ADD_INITIALIZER('rational::initialize();')
|
// ADD_INITIALIZER('rational::initialize();')
|
||||||
// ADD_FINALIZER('rational::finalize();')
|
// ADD_FINALIZER('rational::finalize();')
|
||||||
// Thus, any executable or shared object (DLL) that depends on rational.h
|
// Thus, any executable or shared object (DLL) that depends on rational.h
|
||||||
// will have an automalically generated file mem_initializer.cpp containing
|
// will have an automatically generated file mem_initializer.cpp containing
|
||||||
// mem_initialize()
|
// mem_initialize()
|
||||||
// mem_finalize()
|
// mem_finalize()
|
||||||
// and these functions will include the statements:
|
// and these functions will include the statements:
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue