mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable
This commit is contained in:
commit
6f0d76a62e
|
@ -1,3 +1,5 @@
|
|||
# Copyright (c) Microsoft Corporation 2015
|
||||
|
||||
import os
|
||||
import shutil
|
||||
import re
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include<vector>
|
||||
#include"z3++.h"
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include<stdio.h>
|
||||
#include<stdlib.h>
|
||||
#include<stdarg.h>
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
#include <iostream>
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
/*
|
||||
Simple MAXSAT solver on top of the Z3 API.
|
||||
*/
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Linq;
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Linq;
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Linq;
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Linq;
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Text;
|
||||
using Microsoft.SolverFoundation.Services;
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using Microsoft.SolverFoundation.Services;
|
||||
using System;
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Threading;
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using Microsoft.SolverFoundation.Services;
|
||||
using System;
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using Microsoft.SolverFoundation.Services;
|
||||
using System;
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Diagnostics;
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using Microsoft.SolverFoundation.Services;
|
||||
using System;
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using Microsoft.SolverFoundation.Services;
|
||||
using System;
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Threading;
|
||||
using System.Globalization;
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.IO;
|
||||
using System.Linq;
|
||||
|
|
|
@ -1,3 +1,5 @@
|
|||
# Copyright (c) Microsoft Corporation 2015
|
||||
|
||||
from z3 import *
|
||||
|
||||
x = Real('x')
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include <string>
|
||||
#include <cstring>
|
||||
#include <list>
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef TPTP5_H_
|
||||
#define TPTP5_H_
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#line 2 "tptp5.lex.cpp"
|
||||
|
||||
#line 4 "tptp5.lex.cpp"
|
||||
|
|
57
scripts/mk_copyright.py
Normal file
57
scripts/mk_copyright.py
Normal file
|
@ -0,0 +1,57 @@
|
|||
# Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
import os
|
||||
import re
|
||||
|
||||
cr = re.compile("Copyright")
|
||||
aut = re.compile("Automatically generated")
|
||||
|
||||
cr_notice = """
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
"""
|
||||
|
||||
def has_cr(file):
|
||||
ins = open(file)
|
||||
lines = 0
|
||||
line = ins.readline()
|
||||
while line and lines < 20:
|
||||
m = cr.search(line)
|
||||
if m:
|
||||
ins.close()
|
||||
return True
|
||||
m = aut.search(line)
|
||||
if m:
|
||||
ins.close()
|
||||
return True
|
||||
line = ins.readline()
|
||||
ins.close()
|
||||
return False
|
||||
|
||||
def add_cr(file):
|
||||
tmp = "%s.tmp" % file
|
||||
ins = open(file)
|
||||
ous = open(tmp,'w')
|
||||
ous.write(cr_notice)
|
||||
line = ins.readline()
|
||||
while line:
|
||||
ous.write(line)
|
||||
line = ins.readline()
|
||||
ins.close()
|
||||
ous.close()
|
||||
os.system("move %s %s" % (tmp, file))
|
||||
|
||||
def add_missing_cr(dir):
|
||||
for root, dirs, files in os.walk(dir):
|
||||
for f in files:
|
||||
if f.endswith('.cpp') or f.endswith('.h') or f.endswith('.c') or f.endswith('.cs'):
|
||||
path = "%s\\%s" % (root, f)
|
||||
if not has_cr(path):
|
||||
print "Missing CR for %s" % path
|
||||
add_cr(path)
|
||||
|
||||
add_missing_cr('src')
|
||||
add_missing_cr('examples')
|
|
@ -1,7 +1,9 @@
|
|||
#!/bin/bash
|
||||
|
||||
# Copyright (c) 2015 Microsoft Corporation
|
||||
# Script for "cloning" (and tracking) all branches at codeplex.
|
||||
# On Windows, this script must be executed in the "git Bash" console.
|
||||
|
||||
for branch in `git branch -a | grep remotes | grep -v HEAD | grep -v master`; do
|
||||
git branch --track ${branch##*/} $branch
|
||||
done
|
||||
|
|
|
@ -516,6 +516,11 @@ extern "C" {
|
|||
memory::initialize(0);
|
||||
}
|
||||
|
||||
void Z3_API Z3_finalize_memory(void) {
|
||||
LOG_Z3_finalize_memory();
|
||||
memory::finalize();
|
||||
}
|
||||
|
||||
Z3_error_code Z3_API Z3_get_error_code(Z3_context c) {
|
||||
LOG_Z3_get_error_code(c);
|
||||
return mk_c(c)->get_error_code();
|
||||
|
|
|
@ -712,7 +712,7 @@ extern "C" {
|
|||
|
||||
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_ebits(c, s);
|
||||
LOG_Z3_fpa_get_sbits(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(s, 0);
|
||||
return mk_c(c)->fpautil().get_sbits(to_sort(s));
|
||||
|
@ -765,7 +765,30 @@ extern "C" {
|
|||
mpqm.display_decimal(ss, q, sbits);
|
||||
return mk_c(c)->mk_external_string(ss.str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
|
||||
scoped_mpf val(mpfm);
|
||||
bool r = plugin->is_numeral(to_expr(t), val);
|
||||
if (!r) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
const mpz & z = mpfm.sig(val);
|
||||
if (!mpzm.is_uint64(z)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
*n = mpzm.get_uint64(z);
|
||||
return 1;
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
|
||||
|
@ -794,7 +817,7 @@ extern "C" {
|
|||
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_exponent_string(c, t);
|
||||
LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#ifdef _WINDOWS
|
||||
|
||||
#include<windows.h>
|
||||
|
|
|
@ -59,6 +59,25 @@ namespace Microsoft.Z3
|
|||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The significand value of a floating-point numeral as a UInt64
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// This function extracts the significand bits, without the
|
||||
/// hidden bit or normalization. Throws an exception if the
|
||||
/// significand does not fit into a UInt64.
|
||||
/// </remarks>
|
||||
public UInt64 SignificandUInt64
|
||||
{
|
||||
get
|
||||
{
|
||||
UInt64 result = 0;
|
||||
if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
|
||||
throw new Z3Exception("Significand is not a 64 bit unsigned integer");
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Return the exponent value of a floating-point numeral as a string
|
||||
/// </summary>
|
||||
|
|
|
@ -208,6 +208,21 @@ namespace Microsoft.Z3
|
|||
return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Goal to BoolExpr conversion.
|
||||
/// </summary>
|
||||
/// <returns>A string representation of the Goal.</returns>
|
||||
public BoolExpr AsBoolExpr() {
|
||||
uint n = Size;
|
||||
if (n == 0)
|
||||
return Context.MkTrue();
|
||||
else if (n == 1)
|
||||
return Formulas[0];
|
||||
else {
|
||||
return Context.MkAnd(Formulas);
|
||||
}
|
||||
}
|
||||
|
||||
#region Internal
|
||||
internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Linq;
|
||||
|
|
|
@ -43,6 +43,21 @@ public class FPNum extends FPExpr
|
|||
return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* The significand value of a floating-point numeral as a UInt64
|
||||
* Remarks: This function extracts the significand bits, without the
|
||||
* hidden bit or normalization. Throws an exception if the
|
||||
* significand does not fit into a UInt64.
|
||||
* @throws Z3Exception
|
||||
**/
|
||||
public long getSignificandUInt64()
|
||||
{
|
||||
Native.LongPtr res = new Native.LongPtr();
|
||||
if (Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res) ^ true)
|
||||
throw new Z3Exception("Significand is not a 64 bit unsigned integer");
|
||||
return res.value;
|
||||
}
|
||||
|
||||
/**
|
||||
* Return the exponent value of a floating-point numeral as a string
|
||||
* @throws Z3Exception
|
||||
|
|
|
@ -43,7 +43,7 @@ public class FPSort extends Sort
|
|||
* The number of significand bits.
|
||||
*/
|
||||
public int getSBits() {
|
||||
return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());
|
||||
return Native.fpaGetSbits(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -221,6 +221,22 @@ public class Goal extends Z3Object
|
|||
return "Z3Exception: " + e.getMessage();
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Goal to BoolExpr conversion.
|
||||
*
|
||||
* Returns a string representation of the Goal.
|
||||
**/
|
||||
public BoolExpr AsBoolExpr() {
|
||||
int n = size();
|
||||
if (n == 0)
|
||||
return getContext().mkTrue();
|
||||
else if (n == 1)
|
||||
return getFormulas()[0];
|
||||
else {
|
||||
return getContext().mkAnd(getFormulas());
|
||||
}
|
||||
}
|
||||
|
||||
Goal(Context ctx, long obj)
|
||||
{
|
||||
|
|
|
@ -2059,6 +2059,8 @@ struct
|
|||
(Z3native.fpa_get_numeral_sign (context_gno ctx) (Expr.gno t))
|
||||
let get_numeral_significand_string ( ctx : context ) ( t : expr ) =
|
||||
(Z3native.fpa_get_numeral_significand_string (context_gno ctx) (Expr.gno t))
|
||||
let get_numeral_significand_uint ( ctx : context ) ( t : expr ) =
|
||||
(Z3native.fpa_get_numeral_significand_uint64 (context_gno ctx) (Expr.gno t))
|
||||
let get_numeral_exponent_string ( ctx : context ) ( t : expr ) =
|
||||
(Z3native.fpa_get_numeral_exponent_string (context_gno ctx) (Expr.gno t))
|
||||
let get_numeral_exponent_int ( ctx : context ) ( t : expr ) =
|
||||
|
@ -2197,6 +2199,15 @@ struct
|
|||
create ctx (Z3native.mk_goal (context_gno ctx) models unsat_cores proofs)
|
||||
|
||||
let to_string ( x : goal ) = Z3native.goal_to_string (z3obj_gnc x) (z3obj_gno x)
|
||||
|
||||
let as_expr ( x : goal ) =
|
||||
let n = get_size x in
|
||||
if n = 0 then
|
||||
(Boolean.mk_true (z3obj_gc x))
|
||||
else if n = 1 then
|
||||
(List.hd (get_formulas x))
|
||||
else
|
||||
(Boolean.mk_and (z3obj_gc x) (get_formulas x))
|
||||
end
|
||||
|
||||
|
||||
|
|
|
@ -2161,6 +2161,12 @@ sig
|
|||
(** Return the significand value of a floating-point numeral as a string. *)
|
||||
val get_numeral_significand_string : context -> Expr.expr -> string
|
||||
|
||||
(** Return the significand value of a floating-point numeral as a uint64.
|
||||
Remark: This function extracts the significand bits, without the
|
||||
hidden bit or normalization. Throws an exception if the
|
||||
significand does not fit into a uint64. *)
|
||||
val get_numeral_significand_uint : context -> Expr.expr -> bool * int
|
||||
|
||||
(** Return the exponent value of a floating-point numeral as a string *)
|
||||
val get_numeral_exponent_string : context -> Expr.expr -> string
|
||||
|
||||
|
@ -2647,6 +2653,9 @@ sig
|
|||
|
||||
(** A string representation of the Goal. *)
|
||||
val to_string : goal -> string
|
||||
|
||||
(** Goal to BoolExpr conversion. *)
|
||||
val as_expr : goal -> Expr.expr
|
||||
end
|
||||
|
||||
(** Models
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
/* File generated from z3.idl */
|
||||
|
||||
#include <stddef.h>
|
||||
|
|
|
@ -5617,7 +5617,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> len(st)
|
||||
2
|
||||
4
|
||||
"""
|
||||
return int(Z3_stats_size(self.ctx.ref(), self.stats))
|
||||
|
||||
|
@ -5631,7 +5631,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> len(st)
|
||||
2
|
||||
4
|
||||
>>> st[0]
|
||||
('nlsat propagations', 2)
|
||||
>>> st[1]
|
||||
|
@ -5655,7 +5655,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> st.keys()
|
||||
['nlsat propagations', 'nlsat stages']
|
||||
['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
|
||||
"""
|
||||
return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
|
||||
|
||||
|
@ -5692,7 +5692,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> st.keys()
|
||||
['nlsat propagations', 'nlsat stages']
|
||||
['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
|
||||
>>> st.nlsat_propagations
|
||||
2
|
||||
>>> st.nlsat_stages
|
||||
|
@ -8194,23 +8194,24 @@ def FP(name, fpsort, ctx=None):
|
|||
>>> eq(x, x2)
|
||||
True
|
||||
"""
|
||||
ctx = fpsort.ctx
|
||||
if isinstance(fpsort, FPSortRef):
|
||||
ctx = fpsort.ctx
|
||||
else:
|
||||
ctx = _get_ctx(ctx)
|
||||
return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
|
||||
|
||||
def FPs(names, fpsort, ctx=None):
|
||||
"""Return an array of floating-point constants.
|
||||
|
||||
>>> x, y, z = BitVecs('x y z', 16)
|
||||
>>> x.size()
|
||||
16
|
||||
>>> x, y, z = FPs('x y z', FPSort(8, 24))
|
||||
>>> x.sort()
|
||||
BitVec(16)
|
||||
>>> Sum(x, y, z)
|
||||
0 + x + y + z
|
||||
>>> Product(x, y, z)
|
||||
1*x*y*z
|
||||
>>> simplify(Product(x, y, z))
|
||||
x*y*z
|
||||
FPSort(8, 24)
|
||||
>>> x.sbits()
|
||||
24
|
||||
>>> x.ebits()
|
||||
8
|
||||
>>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
|
||||
fpMul(RNE(), fpAdd(RNE(), x, y), z)
|
||||
"""
|
||||
ctx = z3._get_ctx(ctx)
|
||||
if isinstance(names, str):
|
||||
|
|
|
@ -1,3 +1,10 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Z3 Python interface
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
import z3, doctest
|
||||
|
||||
r = doctest.testmod(z3)
|
||||
|
|
|
@ -1,3 +1,11 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Z3 Python interface
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
|
||||
import ctypes, z3core
|
||||
|
||||
class Z3Exception(Exception):
|
||||
|
|
|
@ -1,3 +1,10 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Z3 Python interface
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
"""
|
||||
Usage:
|
||||
import common_z3 as CM_Z3
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef _Z3_API_H_
|
||||
#define _Z3_API_H_
|
||||
|
||||
|
@ -5365,7 +5371,19 @@ END_MLAPI_EXCLUDE
|
|||
*/
|
||||
void Z3_API Z3_reset_memory(void);
|
||||
#endif
|
||||
|
||||
|
||||
#ifdef CorML3
|
||||
/**
|
||||
\brief Destroy all allocated resources.
|
||||
|
||||
Any pointers previously returned by the API become invalid.
|
||||
Can be used for memory leak detection.
|
||||
|
||||
def_API('Z3_finalize_memory', VOID, ())
|
||||
*/
|
||||
void Z3_API Z3_finalize_memory(void);
|
||||
#endif
|
||||
|
||||
/*@}*/
|
||||
|
||||
#ifdef CorML3
|
||||
|
@ -6933,7 +6951,7 @@ END_MLAPI_EXCLUDE
|
|||
|
||||
def_API('Z3_tactic_apply_ex', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL), _in(PARAMS)))
|
||||
*/
|
||||
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
|
||||
Z3_apply_result Z3_API Z3_tactic_apply_ex(__in Z3_context c, __in Z3_tactic t, __in Z3_goal g, __in Z3_params p);
|
||||
|
||||
#ifdef CorML3
|
||||
/**
|
||||
|
|
|
@ -858,6 +858,20 @@ extern "C" {
|
|||
*/
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Return the significand value of a floating-point numeral as a uint64.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
Remarks: This function extracts the significand bits in `t`, without the
|
||||
hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the
|
||||
significand does not fit into a uint64.
|
||||
|
||||
def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n);
|
||||
|
||||
/**
|
||||
\brief Return the exponent value of a floating-point numeral as a string
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef __in
|
||||
#define __in
|
||||
#endif
|
||||
|
|
|
@ -501,13 +501,17 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
|
|||
func_decl * r = mk_func_decl(k, bv_size);
|
||||
if (r != 0) {
|
||||
if (arity != r->get_arity()) {
|
||||
m_manager->raise_exception("declared arity mismatches supplied arity");
|
||||
return 0;
|
||||
if (r->get_info()->is_associative())
|
||||
arity = r->get_arity();
|
||||
else {
|
||||
m_manager->raise_exception("declared arity mismatches supplied arity");
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < arity; ++i) {
|
||||
if (domain[i] != r->get_domain(i)) {
|
||||
m_manager->raise_exception("declared sorts do not match supplied sorts");
|
||||
return 0;
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
return r;
|
||||
|
@ -566,6 +570,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
|
|||
|
||||
func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned num_args, expr * const * args, sort * range) {
|
||||
ast_manager& m = *m_manager;
|
||||
int bv_size;
|
||||
if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
|
||||
// bv_size is filled in.
|
||||
|
@ -589,11 +594,35 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
|
|||
return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
|
||||
}
|
||||
else if (num_args == 0 || !get_bv_size(args[0], bv_size)) {
|
||||
m_manager->raise_exception("operator is applied to arguments of the wrong sort");
|
||||
m.raise_exception("operator is applied to arguments of the wrong sort");
|
||||
return 0;
|
||||
}
|
||||
func_decl * r = mk_func_decl(k, bv_size);
|
||||
if (r != 0) {
|
||||
if (num_args != r->get_arity()) {
|
||||
if (r->get_info()->is_associative()) {
|
||||
sort * fs = r->get_domain(0);
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
if (m.get_sort(args[i]) != fs) {
|
||||
m_manager->raise_exception("declared sorts do not match supplied sorts");
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
else {
|
||||
m.raise_exception("declared arity mismatches supplied arity");
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
if (m.get_sort(args[i]) != r->get_domain(i)) {
|
||||
std::ostringstream buffer;
|
||||
buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m);
|
||||
m.raise_exception(buffer.str().c_str());
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
|
||||
|
|
|
@ -44,7 +44,8 @@ namespace datalog {
|
|||
m_num_sym("N"),
|
||||
m_lt_sym("<"),
|
||||
m_le_sym("<="),
|
||||
m_rule_sym("R")
|
||||
m_rule_sym("R"),
|
||||
m_min_sym("min")
|
||||
{
|
||||
}
|
||||
|
||||
|
@ -490,6 +491,66 @@ namespace datalog {
|
|||
return m_manager->mk_func_decl(m_clone_sym, 1, &s, s, info);
|
||||
}
|
||||
|
||||
/**
|
||||
In SMT2 syntax, we can write \c ((_ min R N) v_0 v_1 ... v_k)) where 0 <= N <= k,
|
||||
R is a relation of sort V_0 x V_1 x ... x V_k and each v_i is a zero-arity function
|
||||
(also known as a "constant" in SMT2 parlance) whose range is of sort V_i.
|
||||
|
||||
Example:
|
||||
|
||||
(define-sort number_t () (_ BitVec 2))
|
||||
(declare-rel numbers (number_t number_t))
|
||||
(declare-rel is_min (number_t number_t))
|
||||
|
||||
(declare-var x number_t)
|
||||
(declare-var y number_t)
|
||||
|
||||
(rule (numbers #b00 #b11))
|
||||
(rule (numbers #b00 #b01))
|
||||
|
||||
(rule (=> (and (numbers x y) ((_ min numbers 1) x y)) (is_min x y)))
|
||||
|
||||
This says that we want to find the mininum y grouped by x.
|
||||
*/
|
||||
func_decl * dl_decl_plugin::mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters) {
|
||||
if (num_parameters < 2) {
|
||||
m_manager->raise_exception("invalid min aggregate definition due to missing parameters");
|
||||
return 0;
|
||||
}
|
||||
|
||||
parameter const & relation_parameter = parameters[0];
|
||||
if (!relation_parameter.is_ast() || !is_func_decl(relation_parameter.get_ast())) {
|
||||
m_manager->raise_exception("invalid min aggregate definition, first parameter is not a function declaration");
|
||||
return 0;
|
||||
}
|
||||
|
||||
func_decl* f = to_func_decl(relation_parameter.get_ast());
|
||||
if (!m_manager->is_bool(f->get_range())) {
|
||||
m_manager->raise_exception("invalid min aggregate definition, first paramater must be a predicate");
|
||||
return 0;
|
||||
}
|
||||
|
||||
parameter const & min_col_parameter = parameters[1];
|
||||
if (!min_col_parameter.is_int()) {
|
||||
m_manager->raise_exception("invalid min aggregate definition, second parameter must be an integer");
|
||||
return 0;
|
||||
}
|
||||
|
||||
if (min_col_parameter.get_int() < 0) {
|
||||
m_manager->raise_exception("invalid min aggregate definition, second parameter must be non-negative");
|
||||
return 0;
|
||||
}
|
||||
|
||||
if ((unsigned)min_col_parameter.get_int() >= f->get_arity()) {
|
||||
m_manager->raise_exception("invalid min aggregate definition, second parameter exceeds the arity of the relation");
|
||||
return 0;
|
||||
}
|
||||
|
||||
func_decl_info info(m_family_id, k, num_parameters, parameters);
|
||||
SASSERT(f->get_info() == 0);
|
||||
return m_manager->mk_func_decl(m_min_sym, f->get_arity(), f->get_domain(), f->get_range(), info);
|
||||
}
|
||||
|
||||
func_decl * dl_decl_plugin::mk_func_decl(
|
||||
decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
|
@ -617,6 +678,9 @@ namespace datalog {
|
|||
break;
|
||||
}
|
||||
|
||||
case OP_DL_MIN:
|
||||
return mk_min(k, num_parameters, parameters);
|
||||
|
||||
default:
|
||||
m_manager->raise_exception("operator not recognized");
|
||||
return 0;
|
||||
|
@ -627,7 +691,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void dl_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
|
||||
|
||||
op_names.push_back(builtin_name(m_min_sym.bare_str(), OP_DL_MIN));
|
||||
}
|
||||
|
||||
void dl_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
|
||||
|
|
|
@ -50,6 +50,7 @@ namespace datalog {
|
|||
OP_DL_LT,
|
||||
OP_DL_REP,
|
||||
OP_DL_ABS,
|
||||
OP_DL_MIN,
|
||||
LAST_RA_OP
|
||||
};
|
||||
|
||||
|
@ -71,6 +72,7 @@ namespace datalog {
|
|||
symbol m_lt_sym;
|
||||
symbol m_le_sym;
|
||||
symbol m_rule_sym;
|
||||
symbol m_min_sym;
|
||||
|
||||
bool check_bounds(char const* msg, unsigned low, unsigned up, unsigned val) const;
|
||||
bool check_domain(unsigned low, unsigned up, unsigned val) const;
|
||||
|
@ -94,12 +96,69 @@ namespace datalog {
|
|||
func_decl * mk_compare(decl_kind k, symbol const& sym, sort*const* domain);
|
||||
func_decl * mk_clone(sort* r);
|
||||
func_decl * mk_rule(unsigned arity);
|
||||
func_decl * mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters);
|
||||
|
||||
sort * mk_finite_sort(unsigned num_params, parameter const* params);
|
||||
sort * mk_relation_sort(unsigned num_params, parameter const* params);
|
||||
sort * mk_rule_sort();
|
||||
|
||||
public:
|
||||
/**
|
||||
Is \c decl a min aggregation function?
|
||||
*/
|
||||
static bool is_aggregate(const func_decl* const decl)
|
||||
{
|
||||
return decl->get_decl_kind() == OP_DL_MIN;
|
||||
}
|
||||
|
||||
/**
|
||||
\pre: is_aggregate(aggregate)
|
||||
|
||||
\returns function declaration of predicate which is subject to min aggregation function
|
||||
*/
|
||||
static func_decl * min_func_decl(const func_decl* const aggregate)
|
||||
{
|
||||
SASSERT(is_aggregate(aggregate));
|
||||
parameter const & relation_parameter = aggregate->get_parameter(0);
|
||||
return to_func_decl(relation_parameter.get_ast());
|
||||
}
|
||||
|
||||
/**
|
||||
\pre: is_aggregate(aggregate)
|
||||
|
||||
\returns column identifier (starting at zero) which is minimized by aggregation function
|
||||
*/
|
||||
static unsigned min_col(const func_decl* const aggregate)
|
||||
{
|
||||
SASSERT(is_aggregate(aggregate));
|
||||
return (unsigned)aggregate->get_parameter(1).get_int();
|
||||
}
|
||||
|
||||
/**
|
||||
\pre: is_aggregate(aggregate)
|
||||
|
||||
\returns column identifiers for the "group by" in the given min aggregation function
|
||||
*/
|
||||
static unsigned_vector group_by_cols(const func_decl* const aggregate)
|
||||
{
|
||||
SASSERT(is_aggregate(aggregate));
|
||||
unsigned _min_col = min_col(aggregate);
|
||||
if (aggregate->get_arity() == 0U)
|
||||
return unsigned_vector();
|
||||
|
||||
unsigned col_num = 0;
|
||||
unsigned_vector cols(aggregate->get_arity() - 1U);
|
||||
for (unsigned i = 0; i < cols.size(); ++i, ++col_num)
|
||||
{
|
||||
if (col_num == _min_col)
|
||||
++col_num;
|
||||
|
||||
cols[i] = col_num;
|
||||
}
|
||||
|
||||
return cols;
|
||||
}
|
||||
|
||||
dl_decl_plugin();
|
||||
virtual ~dl_decl_plugin() {}
|
||||
|
||||
|
|
|
@ -93,6 +93,20 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
|
|||
mk_fp(sgn, e, s, result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
// Note: in SMT there is only one NaN, so multiple of them are considered
|
||||
// equal, thus (distinct NaN NaN) is false, even if the two NaNs have
|
||||
// different bitwise representations (see also mk_eq).
|
||||
result = m.mk_true();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
for (unsigned j = i+1; j < num; j++) {
|
||||
expr_ref eq(m);
|
||||
mk_eq(args[i], args[j], eq);
|
||||
m_simp.mk_and(result, m.mk_not(eq), result);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 0);
|
||||
SASSERT(f->get_num_parameters() == 1);
|
||||
|
@ -1403,14 +1417,20 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
|
||||
res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
|
||||
|
||||
sticky_raw = m_bv_util.mk_extract(sbits-5, 0, sig_abs);
|
||||
sticky = m_bv_util.mk_zero_extend(sbits+3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()));
|
||||
if (sbits > 5) {
|
||||
sticky_raw = m_bv_util.mk_extract(sbits - 5, 0, sig_abs);
|
||||
sticky = m_bv_util.mk_zero_extend(sbits + 3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()));
|
||||
expr * res_or_args[2] = { m_bv_util.mk_extract(2 * sbits - 1, sbits - 4, sig_abs), sticky };
|
||||
res_sig = m_bv_util.mk_bv_or(2, res_or_args);
|
||||
}
|
||||
else {
|
||||
unsigned too_short = 6 - sbits;
|
||||
sig_abs = m_bv_util.mk_concat(sig_abs, m_bv_util.mk_numeral(0, too_short));
|
||||
res_sig = m_bv_util.mk_extract(sbits + 3, 0, sig_abs);
|
||||
}
|
||||
dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
|
||||
|
||||
expr * res_or_args[2] = { m_bv_util.mk_extract(2*sbits-1, sbits-4, sig_abs), sticky };
|
||||
res_sig = m_bv_util.mk_bv_or(2, res_or_args);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4);
|
||||
|
||||
expr_ref is_zero_sig(m), nil_sbits4(m);
|
||||
nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4);
|
||||
m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig);
|
||||
|
@ -1761,11 +1781,19 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
m_simp.mk_ite(c52, v52, res_sig, res_sig);
|
||||
m_simp.mk_ite(c51, v51, res_sig, res_sig);
|
||||
res_sig = m_bv_util.mk_concat(res_sig, m_bv_util.mk_numeral(0, 3)); // rounding bits are all 0.
|
||||
res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), m_bv_util.mk_extract(ebits+1, 0, shift));
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(res_exp) == ebits);
|
||||
SASSERT(m_bv_util.get_bv_size(shift) == sbits + 1);
|
||||
|
||||
expr_ref e_shift(m);
|
||||
e_shift = (ebits + 2 <= sbits + 1) ? m_bv_util.mk_extract(ebits + 1, 0, shift) :
|
||||
m_bv_util.mk_sign_extend((ebits + 2) - (sbits + 1), shift);
|
||||
SASSERT(m_bv_util.get_bv_size(e_shift) == ebits + 2);
|
||||
res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), e_shift);
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(res_sgn) == 1);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4);
|
||||
SASSERT(m_bv_util.get_bv_size(res_exp) == ebits+2);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
|
||||
SASSERT(m_bv_util.get_bv_size(res_exp) == ebits + 2);
|
||||
|
||||
// CMW: We use the rounder for normalization.
|
||||
round(f->get_range(), rm, res_sgn, res_sig, res_exp, v6);
|
||||
|
@ -2953,9 +2981,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
|
|||
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
|
||||
SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2);
|
||||
SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2);
|
||||
SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
|
||||
dbg_decouple("fpa2bv_to_sbv_shift", shift);
|
||||
dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
|
||||
SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
|
||||
dbg_decouple("fpa2bv_to_sbv_shift", shift);
|
||||
|
||||
// sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long
|
||||
// [1][ ... sig ... ][r][g][ ... s ...]
|
||||
|
@ -2964,34 +2991,48 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
|
|||
max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
|
||||
shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
|
||||
SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
|
||||
dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
|
||||
|
||||
expr_ref c_in_limits(m);
|
||||
c_in_limits = m_bv_util.mk_sle(shift, m_bv_util.mk_numeral(0, ebits + 2));
|
||||
dbg_decouple("fpa2bv_to_sbv_in_limits", c_in_limits);
|
||||
|
||||
expr_ref shifted_sig(m);
|
||||
shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs);
|
||||
dbg_decouple("fpa2bv_to_sbv_shifted_sig", shifted_sig);
|
||||
expr_ref huge_sig(m), huge_shift(m), huge_shifted_sig(m);
|
||||
huge_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_sz));
|
||||
huge_shift = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sig_sz), shift_abs);
|
||||
huge_shifted_sig = m_bv_util.mk_bv_lshr(huge_sig, huge_shift);
|
||||
dbg_decouple("fpa2bv_to_sbv_huge_shifted_sig", huge_shifted_sig);
|
||||
SASSERT(m_bv_util.get_bv_size(huge_shifted_sig) == 2 * sig_sz);
|
||||
|
||||
expr_ref upper_hss(m), lower_hss(m);
|
||||
upper_hss = m_bv_util.mk_extract(2 * sig_sz - 1, sig_sz + 1, huge_shifted_sig);
|
||||
lower_hss = m_bv_util.mk_extract(sig_sz, 0, huge_shifted_sig);
|
||||
SASSERT(m_bv_util.get_bv_size(upper_hss) == sig_sz - 1);
|
||||
SASSERT(m_bv_util.get_bv_size(lower_hss) == sig_sz + 1);
|
||||
dbg_decouple("fpa2bv_to_sbv_upper_hss", upper_hss);
|
||||
dbg_decouple("fpa2bv_to_sbv_lower_hss", lower_hss);
|
||||
|
||||
expr_ref last(m), round(m), sticky(m);
|
||||
last = m_bv_util.mk_extract(sig_sz - bv_sz - 0, sig_sz - bv_sz - 0, shifted_sig);
|
||||
round = m_bv_util.mk_extract(sig_sz - bv_sz - 1, sig_sz - bv_sz - 1, shifted_sig);
|
||||
sticky = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(sig_sz - bv_sz - 2, 0, shifted_sig),
|
||||
m_bv_util.mk_numeral(0, sig_sz - (bv_sz + 3) + 2)),
|
||||
bv0,
|
||||
bv1);
|
||||
last = m_bv_util.mk_extract(1, 1, upper_hss);
|
||||
round = m_bv_util.mk_extract(0, 0, upper_hss);
|
||||
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lower_hss.get());
|
||||
dbg_decouple("fpa2bv_to_sbv_last", last);
|
||||
dbg_decouple("fpa2bv_to_sbv_round", round);
|
||||
dbg_decouple("fpa2bv_to_sbv_sticky", sticky);
|
||||
|
||||
expr_ref upper_hss_w_sticky(m);
|
||||
upper_hss_w_sticky = m_bv_util.mk_concat(upper_hss, sticky);
|
||||
dbg_decouple("fpa2bv_to_sbv_upper_hss_w_sticky", upper_hss_w_sticky);
|
||||
SASSERT(m_bv_util.get_bv_size(upper_hss_w_sticky) == sig_sz);
|
||||
|
||||
expr_ref rounding_decision(m);
|
||||
rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky);
|
||||
SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1);
|
||||
dbg_decouple("fpa2bv_to_sbv_rounding_decision", rounding_decision);
|
||||
|
||||
expr_ref unrounded_sig(m), pre_rounded(m), inc(m);
|
||||
unrounded_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz, shifted_sig));
|
||||
inc = m_bv_util.mk_zero_extend(1, m_bv_util.mk_zero_extend(bv_sz - 1, rounding_decision));
|
||||
unrounded_sig = m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz - 1, upper_hss_w_sticky);
|
||||
inc = m_bv_util.mk_zero_extend(bv_sz, rounding_decision);
|
||||
pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc);
|
||||
dbg_decouple("fpa2bv_to_sbv_inc", inc);
|
||||
dbg_decouple("fpa2bv_to_sbv_unrounded_sig", unrounded_sig);
|
||||
|
@ -3409,6 +3450,17 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
|
|||
}
|
||||
|
||||
expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky) {
|
||||
expr_ref rmr(rm, m);
|
||||
expr_ref sgnr(sgn, m);
|
||||
expr_ref lastr(last, m);
|
||||
expr_ref roundr(round, m);
|
||||
expr_ref stickyr(sticky, m);
|
||||
dbg_decouple("fpa2bv_rnd_dec_rm", rmr);
|
||||
dbg_decouple("fpa2bv_rnd_dec_sgn", sgnr);
|
||||
dbg_decouple("fpa2bv_rnd_dec_last", lastr);
|
||||
dbg_decouple("fpa2bv_rnd_dec_round", roundr);
|
||||
dbg_decouple("fpa2bv_rnd_dec_sticky", stickyr);
|
||||
|
||||
expr_ref last_or_sticky(m), round_or_sticky(m), not_last(m), not_round(m), not_sticky(m), not_lors(m), not_rors(m), not_sgn(m);
|
||||
expr * last_sticky[2] = { last, sticky };
|
||||
expr * round_sticky[2] = { round, sticky };
|
||||
|
@ -3446,6 +3498,7 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la
|
|||
m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2);
|
||||
m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, res);
|
||||
|
||||
dbg_decouple("fpa2bv_rnd_dec_res", res);
|
||||
return res;
|
||||
}
|
||||
|
||||
|
|
|
@ -80,6 +80,7 @@ public:
|
|||
|
||||
void mk_eq(expr * a, expr * b, expr_ref & result);
|
||||
void mk_ite(expr * c, expr * t, expr * f, expr_ref & result);
|
||||
void mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
void mk_rounding_mode(func_decl * f, expr_ref & result);
|
||||
void mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
|
|
@ -103,8 +103,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
|
|||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
if (m().is_ite(f)) {
|
||||
else if (m().is_ite(f)) {
|
||||
SASSERT(num == 3);
|
||||
if (m_conv.is_float(args[1])) {
|
||||
m_conv.mk_ite(args[0], args[1], args[2], result);
|
||||
|
@ -112,6 +111,14 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
|
|||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
else if (m().is_distinct(f)) {
|
||||
sort * ds = f->get_domain()[0];
|
||||
if (m_conv.is_float(ds) || m_conv.is_rm(ds)) {
|
||||
m_conv.mk_distinct(f, num, args, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
if (m_conv.is_float_family(f)) {
|
||||
switch (f->get_decl_kind()) {
|
||||
|
|
|
@ -154,7 +154,7 @@ class func_decl_dependencies::top_sort {
|
|||
case OPEN:
|
||||
set_color(cf, IN_PROGRESS);
|
||||
if (visit_children(cf)) {
|
||||
SASSERT(m_todo.back() == f);
|
||||
SASSERT(m_todo.back() == cf);
|
||||
m_todo.pop_back();
|
||||
set_color(cf, CLOSED);
|
||||
}
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include "proof_checker.h"
|
||||
#include "ast_ll_pp.h"
|
||||
#include "ast_pp.h"
|
||||
|
|
|
@ -49,17 +49,23 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
|
|||
app* c = to_app(a);
|
||||
unsigned n = c->get_num_args();
|
||||
m_args.reset();
|
||||
bool arg_differs = false;
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
if (m_cache.find(c->get_arg(i), d)) {
|
||||
m_args.push_back(d);
|
||||
arg_differs |= c->get_arg(i) != d;
|
||||
}
|
||||
else {
|
||||
m_todo.push_back(c->get_arg(i));
|
||||
}
|
||||
}
|
||||
if (m_args.size() == n) {
|
||||
b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
|
||||
m_refs.push_back(b);
|
||||
if (arg_differs) {
|
||||
b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
|
||||
m_refs.push_back(b);
|
||||
} else {
|
||||
b = a;
|
||||
}
|
||||
m_cache.insert(a, b);
|
||||
m_todo.pop_back();
|
||||
}
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include "bv_elim.h"
|
||||
#include "bv_decl_plugin.h"
|
||||
#include "var_subst.h"
|
||||
|
|
|
@ -621,6 +621,7 @@ void cmd_context::init_manager_core(bool new_manager) {
|
|||
register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq());
|
||||
register_plugin(symbol("pb"), alloc(pb_decl_plugin), !has_logic());
|
||||
register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa());
|
||||
register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
|
||||
}
|
||||
else {
|
||||
// the manager was created by an external module
|
||||
|
|
|
@ -4075,7 +4075,7 @@ namespace realclosure {
|
|||
|
||||
void refine_rational_interval(rational_value * v, unsigned prec) {
|
||||
mpbqi & i = interval(v);
|
||||
if (!i.lower_is_open() && !i.lower_is_open()) {
|
||||
if (!i.lower_is_open() && !i.upper_is_open()) {
|
||||
SASSERT(bqm().eq(i.lower(), i.upper()));
|
||||
return;
|
||||
}
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
/**
|
||||
|
||||
Example from Boogie:
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
/**
|
||||
|
||||
output :: derivation model
|
||||
|
|
|
@ -346,6 +346,13 @@ namespace datalog {
|
|||
|
||||
bool is_neg_tail(unsigned i) const { SASSERT(i < m_tail_size); return GET_TAG(m_tail[i]) == 1; }
|
||||
|
||||
/**
|
||||
A predicate P(Xj) can be annotated by adding an interpreted predicate of the form ((_ min P N) ...)
|
||||
where N is the column number that should be used for the min aggregation function.
|
||||
Such an interpreted predicate is an example for which this function returns true.
|
||||
*/
|
||||
bool is_min_tail(unsigned i) const { return dl_decl_plugin::is_aggregate(get_tail(i)->get_decl()); }
|
||||
|
||||
/**
|
||||
Check whether predicate p is in the interpreted tail.
|
||||
|
||||
|
|
|
@ -400,7 +400,7 @@ namespace datalog {
|
|||
SASSERT(!is_closed()); //the rule_set is not already closed
|
||||
m_deps.populate(*this);
|
||||
m_stratifier = alloc(rule_stratifier, m_deps);
|
||||
if (!stratified_negation()) {
|
||||
if (!stratified_negation() || !check_min()) {
|
||||
m_stratifier = 0;
|
||||
m_deps.reset();
|
||||
return false;
|
||||
|
@ -441,6 +441,49 @@ namespace datalog {
|
|||
return true;
|
||||
}
|
||||
|
||||
bool rule_set::check_min() {
|
||||
// For now, we check the following:
|
||||
//
|
||||
// if a min aggregation function occurs in an SCC, is this SCC
|
||||
// free of any other non-monotonic functions, e.g. negation?
|
||||
const unsigned NEG_BIT = 1U << 0;
|
||||
const unsigned MIN_BIT = 1U << 1;
|
||||
|
||||
ptr_vector<rule>::const_iterator it = m_rules.c_ptr();
|
||||
ptr_vector<rule>::const_iterator end = m_rules.c_ptr() + m_rules.size();
|
||||
unsigned_vector component_status(m_stratifier->get_strats().size());
|
||||
|
||||
for (; it != end; it++) {
|
||||
rule * r = *it;
|
||||
app * head = r->get_head();
|
||||
func_decl * head_decl = head->get_decl();
|
||||
unsigned head_strat = get_predicate_strat(head_decl);
|
||||
unsigned n = r->get_tail_size();
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
func_decl * tail_decl = r->get_tail(i)->get_decl();
|
||||
unsigned strat = get_predicate_strat(tail_decl);
|
||||
|
||||
if (r->is_neg_tail(i)) {
|
||||
SASSERT(strat < component_status.size());
|
||||
component_status[strat] |= NEG_BIT;
|
||||
}
|
||||
|
||||
if (r->is_min_tail(i)) {
|
||||
SASSERT(strat < component_status.size());
|
||||
component_status[strat] |= MIN_BIT;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
const unsigned CONFLICT = NEG_BIT | MIN_BIT;
|
||||
for (unsigned k = 0; k < component_status.size(); ++k) {
|
||||
if (component_status[k] == CONFLICT)
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
void rule_set::replace_rules(const rule_set & src) {
|
||||
if (this != &src) {
|
||||
reset();
|
||||
|
|
|
@ -179,6 +179,7 @@ namespace datalog {
|
|||
void compute_deps();
|
||||
void compute_tc_deps();
|
||||
bool stratified_negation();
|
||||
bool check_min();
|
||||
public:
|
||||
rule_set(context & ctx);
|
||||
rule_set(const rule_set & rs);
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
/*--
|
||||
Module Name:
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include "dl_util.h"
|
||||
#include "proof_utils.h"
|
||||
#include "ast_smt2_pp.h"
|
||||
|
|
|
@ -142,7 +142,7 @@ void rule_properties::check_existential_tail() {
|
|||
todo.push_back(e2);
|
||||
}
|
||||
else if (is_quantifier(e)) {
|
||||
todo.push_back(to_quantifier(e)->get_expr());
|
||||
tocheck.push_back(to_quantifier(e)->get_expr());
|
||||
}
|
||||
else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
|
||||
m.is_true(e1)) {
|
||||
|
@ -194,7 +194,6 @@ void rule_properties::operator()(app* n) {
|
|||
}
|
||||
}
|
||||
else {
|
||||
std::cout << mk_pp(n, m) << "\n";
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -1,4 +1,10 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#include"datalog_parser.h"
|
||||
#include"string_buffer.h"
|
||||
#include"str_hashtable.h"
|
||||
|
@ -95,9 +101,10 @@ public:
|
|||
resize_data(0);
|
||||
#if _WINDOWS
|
||||
errno_t err = fopen_s(&m_file, fname, "rb");
|
||||
m_ok = err == 0;
|
||||
m_ok = (m_file != NULL) && (err == 0);
|
||||
#else
|
||||
m_file = fopen(fname, "rb");
|
||||
m_ok = (m_file != NULL);
|
||||
#endif
|
||||
}
|
||||
~line_reader() {
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include "check_relation.h"
|
||||
#include "dl_relation_manager.h"
|
||||
#include "qe_util.h"
|
||||
|
|
|
@ -485,4 +485,125 @@ namespace datalog {
|
|||
brw.mk_or(disjs.size(), disjs.c_ptr(), fml);
|
||||
}
|
||||
|
||||
class table_plugin::min_fn : public table_min_fn{
|
||||
table_signature m_sig;
|
||||
const unsigned_vector m_group_by_cols;
|
||||
const unsigned m_col;
|
||||
public:
|
||||
min_fn(const table_signature & t_sig, const unsigned_vector& group_by_cols, const unsigned col)
|
||||
: m_sig(t_sig),
|
||||
m_group_by_cols(group_by_cols),
|
||||
m_col(col) {}
|
||||
|
||||
virtual table_base* operator()(table_base const& t) {
|
||||
//return reference_implementation(t);
|
||||
return reference_implementation_with_hash(t);
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
/**
|
||||
Reference implementation with negation:
|
||||
|
||||
T1 = join(T, T) by group_cols
|
||||
T2 = { (t1,t2) in T1 | t1[col] > t2[col] }
|
||||
T3 = { t1 | (t1,t2) in T2 }
|
||||
T4 = T \ T3
|
||||
|
||||
The point of this reference implementation is to show
|
||||
that the minimum requires negation (set difference).
|
||||
This is relevant for fixed point computations.
|
||||
*/
|
||||
virtual table_base * reference_implementation(const table_base & t) {
|
||||
relation_manager & manager = t.get_manager();
|
||||
scoped_ptr<table_join_fn> join_fn = manager.mk_join_fn(t, t, m_group_by_cols, m_group_by_cols);
|
||||
scoped_rel<table_base> join_table = (*join_fn)(t, t);
|
||||
|
||||
table_base::iterator join_table_it = join_table->begin();
|
||||
table_base::iterator join_table_end = join_table->end();
|
||||
table_fact row;
|
||||
|
||||
table_element i, j;
|
||||
|
||||
for (; join_table_it != join_table_end; ++join_table_it) {
|
||||
join_table_it->get_fact(row);
|
||||
i = row[m_col];
|
||||
j = row[t.num_columns() + m_col];
|
||||
|
||||
if (i > j) {
|
||||
continue;
|
||||
}
|
||||
|
||||
join_table->remove_fact(row);
|
||||
}
|
||||
|
||||
unsigned_vector cols(t.num_columns());
|
||||
for (unsigned k = 0; k < cols.size(); ++k) {
|
||||
cols[k] = cols.size() + k;
|
||||
SASSERT(cols[k] < join_table->num_columns());
|
||||
}
|
||||
|
||||
scoped_ptr<table_transformer_fn> project_fn = manager.mk_project_fn(*join_table, cols);
|
||||
scoped_rel<table_base> gt_table = (*project_fn)(*join_table);
|
||||
|
||||
for (unsigned k = 0; k < cols.size(); ++k) {
|
||||
cols[k] = k;
|
||||
SASSERT(cols[k] < t.num_columns());
|
||||
SASSERT(cols[k] < gt_table->num_columns());
|
||||
}
|
||||
|
||||
table_base * result = t.clone();
|
||||
scoped_ptr<table_intersection_filter_fn> diff_fn = manager.mk_filter_by_negation_fn(*result, *gt_table, cols, cols);
|
||||
(*diff_fn)(*result, *gt_table);
|
||||
return result;
|
||||
}
|
||||
|
||||
typedef map < table_fact, table_element, svector_hash_proc<table_element_hash>,
|
||||
vector_eq_proc<table_fact> > group_map;
|
||||
|
||||
// Thanks to Nikolaj who kindly helped with the second reference implementation!
|
||||
virtual table_base * reference_implementation_with_hash(const table_base & t) {
|
||||
group_map group;
|
||||
table_base::iterator it = t.begin();
|
||||
table_base::iterator end = t.end();
|
||||
table_fact row, row2;
|
||||
table_element current_value, min_value;
|
||||
for (; it != end; ++it) {
|
||||
it->get_fact(row);
|
||||
current_value = row[m_col];
|
||||
group_by(row, row2);
|
||||
group_map::entry* entry = group.find_core(row2);
|
||||
if (!entry) {
|
||||
group.insert(row2, current_value);
|
||||
}
|
||||
else if (entry->get_data().m_value > current_value) {
|
||||
entry->get_data().m_value = current_value;
|
||||
}
|
||||
}
|
||||
table_base* result = t.get_plugin().mk_empty(m_sig);
|
||||
table_base::iterator it2 = t.begin();
|
||||
for (; it2 != end; ++it2) {
|
||||
it2->get_fact(row);
|
||||
current_value = row[m_col];
|
||||
group_by(row, row2);
|
||||
VERIFY(group.find(row2, min_value));
|
||||
if (min_value == current_value) {
|
||||
result->add_fact(row);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
void group_by(table_fact const& in, table_fact& out) {
|
||||
out.reset();
|
||||
for (unsigned i = 0; i < m_group_by_cols.size(); ++i) {
|
||||
out.push_back(in[m_group_by_cols[i]]);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
table_min_fn * table_plugin::mk_min_fn(const table_base & t,
|
||||
unsigned_vector & group_by_cols, const unsigned col) {
|
||||
return alloc(table_plugin::min_fn, t.get_signature(), group_by_cols, col);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -192,6 +192,29 @@ namespace datalog {
|
|||
virtual base_object * operator()(const base_object & t1, const base_object & t2) = 0;
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Aggregate minimum value
|
||||
|
||||
Informally, we want to group rows in a table \c t by \c group_by_cols and
|
||||
return the minimum value in column \c col among each group.
|
||||
|
||||
Let \c t be a table with N columns.
|
||||
Let \c group_by_cols be a set of column identifers for table \c t such that |group_by_cols| < N.
|
||||
Let \c col be a column identifier for table \c t such that \c col is not in \c group_by_cols.
|
||||
|
||||
Let R_col be a set of rows in table \c t such that, for all rows r_i, r_j in R_col
|
||||
and column identifiers k in \c group_by_cols, r_i[k] = r_j[k].
|
||||
|
||||
For each R_col, we want to restrict R_col to those rows whose value in column \c col is minimal.
|
||||
|
||||
min_fn(R, group_by_cols, col) =
|
||||
{ row in R | forall row' in R . row'[group_by_cols] = row[group_by_cols] => row'[col] >= row[col] }
|
||||
*/
|
||||
class min_fn : public base_fn {
|
||||
public:
|
||||
virtual base_object * operator()(const base_object & t) = 0;
|
||||
};
|
||||
|
||||
class transformer_fn : public base_fn {
|
||||
public:
|
||||
virtual base_object * operator()(const base_object & t) = 0;
|
||||
|
@ -856,6 +879,7 @@ namespace datalog {
|
|||
|
||||
typedef table_infrastructure::base_fn base_table_fn;
|
||||
typedef table_infrastructure::join_fn table_join_fn;
|
||||
typedef table_infrastructure::min_fn table_min_fn;
|
||||
typedef table_infrastructure::transformer_fn table_transformer_fn;
|
||||
typedef table_infrastructure::union_fn table_union_fn;
|
||||
typedef table_infrastructure::mutator_fn table_mutator_fn;
|
||||
|
@ -1020,6 +1044,7 @@ namespace datalog {
|
|||
|
||||
class table_plugin : public table_infrastructure::plugin_object {
|
||||
friend class relation_manager;
|
||||
class min_fn;
|
||||
protected:
|
||||
table_plugin(symbol const& n, relation_manager & manager) : plugin_object(n, manager) {}
|
||||
public:
|
||||
|
@ -1027,6 +1052,9 @@ namespace datalog {
|
|||
virtual bool can_handle_signature(const table_signature & s) { return s.functional_columns()==0; }
|
||||
|
||||
protected:
|
||||
virtual table_min_fn * mk_min_fn(const table_base & t,
|
||||
unsigned_vector & group_by_cols, const unsigned col);
|
||||
|
||||
/**
|
||||
If the returned value is non-zero, the returned object must take ownership of \c mapper.
|
||||
Otherwise \c mapper must remain unmodified.
|
||||
|
|
|
@ -73,6 +73,12 @@ namespace datalog {
|
|||
vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result));
|
||||
}
|
||||
|
||||
void compiler::make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols,
|
||||
const unsigned min_col, instruction_block & acc) {
|
||||
target = get_register(m_reg_signatures[source], true, source);
|
||||
acc.push_back(instruction::mk_min(source, target, group_by_cols, min_col));
|
||||
}
|
||||
|
||||
void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
|
||||
const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc) {
|
||||
SASSERT(!removed_cols.empty());
|
||||
|
@ -440,6 +446,30 @@ namespace datalog {
|
|||
get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res);
|
||||
}
|
||||
|
||||
void compiler::find_min_aggregates(const rule * r, ptr_vector<func_decl>& min_aggregates) {
|
||||
unsigned ut_len = r->get_uninterpreted_tail_size();
|
||||
unsigned ft_len = r->get_tail_size(); // full tail
|
||||
func_decl * aggregate;
|
||||
for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) {
|
||||
aggregate = r->get_tail(tail_index)->get_decl();
|
||||
if (dl_decl_plugin::is_aggregate(aggregate)) {
|
||||
min_aggregates.push_back(aggregate);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool compiler::prepare_min_aggregate(const func_decl * decl, const ptr_vector<func_decl>& min_aggregates,
|
||||
unsigned_vector & group_by_cols, unsigned & min_col) {
|
||||
for (unsigned i = 0; i < min_aggregates.size(); ++i) {
|
||||
if (dl_decl_plugin::min_func_decl(min_aggregates[i]) == decl) {
|
||||
group_by_cols = dl_decl_plugin::group_by_cols(min_aggregates[i]);
|
||||
min_col = dl_decl_plugin::min_col(min_aggregates[i]);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs,
|
||||
reg_idx delta_reg, bool use_widening, instruction_block & acc) {
|
||||
|
||||
|
@ -465,6 +495,12 @@ namespace datalog {
|
|||
// whether to dealloc the previous result
|
||||
bool dealloc = true;
|
||||
|
||||
// setup information for min aggregation
|
||||
ptr_vector<func_decl> min_aggregates;
|
||||
find_min_aggregates(r, min_aggregates);
|
||||
unsigned_vector group_by_cols;
|
||||
unsigned min_col;
|
||||
|
||||
if(pt_len == 2) {
|
||||
reg_idx t1_reg=tail_regs[0];
|
||||
reg_idx t2_reg=tail_regs[1];
|
||||
|
@ -473,6 +509,14 @@ namespace datalog {
|
|||
SASSERT(m_reg_signatures[t1_reg].size()==a1->get_num_args());
|
||||
SASSERT(m_reg_signatures[t2_reg].size()==a2->get_num_args());
|
||||
|
||||
if (prepare_min_aggregate(a1->get_decl(), min_aggregates, group_by_cols, min_col)) {
|
||||
make_min(t1_reg, single_res, group_by_cols, min_col, acc);
|
||||
}
|
||||
|
||||
if (prepare_min_aggregate(a2->get_decl(), min_aggregates, group_by_cols, min_col)) {
|
||||
make_min(t2_reg, single_res, group_by_cols, min_col, acc);
|
||||
}
|
||||
|
||||
variable_intersection a1a2(m_context.get_manager());
|
||||
a1a2.populate(a1,a2);
|
||||
|
||||
|
@ -514,6 +558,10 @@ namespace datalog {
|
|||
single_res = tail_regs[0];
|
||||
dealloc = false;
|
||||
|
||||
if (prepare_min_aggregate(a->get_decl(), min_aggregates, group_by_cols, min_col)) {
|
||||
make_min(single_res, single_res, group_by_cols, min_col, acc);
|
||||
}
|
||||
|
||||
SASSERT(m_reg_signatures[single_res].size() == a->get_num_args());
|
||||
|
||||
unsigned n=a->get_num_args();
|
||||
|
@ -597,7 +645,8 @@ namespace datalog {
|
|||
unsigned ft_len = r->get_tail_size(); // full tail
|
||||
ptr_vector<expr> tail;
|
||||
for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) {
|
||||
tail.push_back(r->get_tail(tail_index));
|
||||
if (!r->is_min_tail(tail_index))
|
||||
tail.push_back(r->get_tail(tail_index));
|
||||
}
|
||||
|
||||
expr_ref_vector binding(m);
|
||||
|
|
|
@ -120,6 +120,22 @@ namespace datalog {
|
|||
instruction_observer m_instruction_observer;
|
||||
expr_free_vars m_free_vars;
|
||||
|
||||
/**
|
||||
\brief Finds all the min aggregation functions in the premise of a given rule.
|
||||
*/
|
||||
static void find_min_aggregates(const rule * r, ptr_vector<func_decl>& min_aggregates);
|
||||
|
||||
/**
|
||||
\brief Decides whether a predicate is subject to a min aggregation function.
|
||||
|
||||
If \c decl is subject to a min aggregation function, the output parameters are written
|
||||
with the neccessary information.
|
||||
|
||||
\returns true if the output paramaters have been written
|
||||
*/
|
||||
static bool prepare_min_aggregate(const func_decl * decl, const ptr_vector<func_decl>& min_aggregates,
|
||||
unsigned_vector & group_by_cols, unsigned & min_col);
|
||||
|
||||
/**
|
||||
If true, the union operation on the underlying structure only provides the information
|
||||
whether the updated relation has changed or not. In this case we do not get anything
|
||||
|
@ -146,6 +162,8 @@ namespace datalog {
|
|||
|
||||
void make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result,
|
||||
bool reuse_t1, instruction_block & acc);
|
||||
void make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols,
|
||||
const unsigned min_col, instruction_block & acc);
|
||||
void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars,
|
||||
const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc);
|
||||
void make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
|
||||
|
|
|
@ -25,6 +25,7 @@ Revision History:
|
|||
#include"rel_context.h"
|
||||
#include"debug.h"
|
||||
#include"warning.h"
|
||||
#include"dl_table_relation.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
@ -552,7 +553,7 @@ namespace datalog {
|
|||
if (r.fast_empty()) {
|
||||
ctx.make_empty(m_reg);
|
||||
}
|
||||
TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n"););
|
||||
//TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n"););
|
||||
|
||||
return true;
|
||||
}
|
||||
|
@ -609,7 +610,7 @@ namespace datalog {
|
|||
if (ctx.reg(m_res)->fast_empty()) {
|
||||
ctx.make_empty(m_res);
|
||||
}
|
||||
TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n"););
|
||||
//TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n"););
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -883,6 +884,59 @@ namespace datalog {
|
|||
removed_cols, result);
|
||||
}
|
||||
|
||||
class instr_min : public instruction {
|
||||
reg_idx m_source_reg;
|
||||
reg_idx m_target_reg;
|
||||
unsigned_vector m_group_by_cols;
|
||||
unsigned m_min_col;
|
||||
public:
|
||||
instr_min(reg_idx source_reg, reg_idx target_reg, const unsigned_vector & group_by_cols, unsigned min_col)
|
||||
: m_source_reg(source_reg),
|
||||
m_target_reg(target_reg),
|
||||
m_group_by_cols(group_by_cols),
|
||||
m_min_col(min_col) {
|
||||
}
|
||||
virtual bool perform(execution_context & ctx) {
|
||||
log_verbose(ctx);
|
||||
if (!ctx.reg(m_source_reg)) {
|
||||
ctx.make_empty(m_target_reg);
|
||||
return true;
|
||||
}
|
||||
|
||||
const relation_base & s = *ctx.reg(m_source_reg);
|
||||
if (!s.from_table()) {
|
||||
throw default_exception("relation is not a table %s",
|
||||
s.get_plugin().get_name().bare_str());
|
||||
}
|
||||
++ctx.m_stats.m_min;
|
||||
const table_relation & tr = static_cast<const table_relation &>(s);
|
||||
const table_base & source_t = tr.get_table();
|
||||
relation_manager & r_manager = s.get_manager();
|
||||
|
||||
const relation_signature & r_sig = s.get_signature();
|
||||
scoped_ptr<table_min_fn> fn = r_manager.mk_min_fn(source_t, m_group_by_cols, m_min_col);
|
||||
table_base * target_t = (*fn)(source_t);
|
||||
|
||||
TRACE("dl",
|
||||
tout << "% ";
|
||||
target_t->display(tout);
|
||||
tout << "\n";);
|
||||
|
||||
relation_base * target_r = r_manager.mk_table_relation(r_sig, target_t);
|
||||
ctx.set_reg(m_target_reg, target_r);
|
||||
return true;
|
||||
}
|
||||
virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const {
|
||||
out << " MIN AGGR ";
|
||||
}
|
||||
virtual void make_annotations(execution_context & ctx) {
|
||||
}
|
||||
};
|
||||
|
||||
instruction * instruction::mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols,
|
||||
const unsigned min_col) {
|
||||
return alloc(instr_min, source, target, group_by_cols, min_col);
|
||||
}
|
||||
|
||||
class instr_select_equal_and_project : public instruction {
|
||||
reg_idx m_src;
|
||||
|
|
|
@ -93,6 +93,7 @@ namespace datalog {
|
|||
unsigned m_filter_interp_project;
|
||||
unsigned m_filter_id;
|
||||
unsigned m_filter_eq;
|
||||
unsigned m_min;
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
@ -284,6 +285,8 @@ namespace datalog {
|
|||
static instruction * mk_join_project(reg_idx rel1, reg_idx rel2, unsigned joined_col_cnt,
|
||||
const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt,
|
||||
const unsigned * removed_cols, reg_idx result);
|
||||
static instruction * mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols,
|
||||
const unsigned min_col);
|
||||
static instruction * mk_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle,
|
||||
reg_idx tgt);
|
||||
static instruction * mk_filter_by_negation(reg_idx tgt, reg_idx neg_rel, unsigned col_cnt,
|
||||
|
|
|
@ -108,7 +108,7 @@ namespace datalog {
|
|||
|
||||
void relation_manager::store_relation(func_decl * pred, relation_base * rel) {
|
||||
SASSERT(rel);
|
||||
relation_map::entry * e = m_relations.insert_if_not_there2(pred, 0);
|
||||
relation_map::obj_map_entry * e = m_relations.insert_if_not_there2(pred, 0);
|
||||
if (e->get_data().m_value) {
|
||||
e->get_data().m_value->deallocate();
|
||||
}
|
||||
|
@ -354,7 +354,9 @@ namespace datalog {
|
|||
return product_relation_plugin::get_plugin(*this).mk_empty(s);
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
The newly created object takes ownership of the \c table object.
|
||||
*/
|
||||
relation_base * relation_manager::mk_table_relation(const relation_signature & s, table_base * table) {
|
||||
SASSERT(s.size()==table->get_signature().size());
|
||||
return get_table_relation_plugin(table->get_plugin()).mk_from_table(s, table);
|
||||
|
@ -1021,6 +1023,11 @@ namespace datalog {
|
|||
return res;
|
||||
}
|
||||
|
||||
table_min_fn * relation_manager::mk_min_fn(const table_base & t,
|
||||
unsigned_vector & group_by_cols, const unsigned col)
|
||||
{
|
||||
return t.get_plugin().mk_min_fn(t, group_by_cols, col);
|
||||
}
|
||||
|
||||
class relation_manager::auxiliary_table_transformer_fn {
|
||||
table_fact m_row;
|
||||
|
|
|
@ -73,7 +73,7 @@ namespace datalog {
|
|||
typedef map<const relation_plugin *, finite_product_relation_plugin *, ptr_hash<const relation_plugin>,
|
||||
ptr_eq<const relation_plugin> > rp2fprp_map;
|
||||
|
||||
typedef map<func_decl *, relation_base *, ptr_hash<func_decl>, ptr_eq<func_decl> > relation_map;
|
||||
typedef obj_map<func_decl, relation_base *> relation_map;
|
||||
typedef ptr_vector<table_plugin> table_plugin_vector;
|
||||
typedef ptr_vector<relation_plugin> relation_plugin_vector;
|
||||
|
||||
|
@ -251,6 +251,9 @@ namespace datalog {
|
|||
return mk_join_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr(), allow_product_relation);
|
||||
}
|
||||
|
||||
table_min_fn * mk_min_fn(const table_base & t,
|
||||
unsigned_vector & group_by_cols, const unsigned col);
|
||||
|
||||
/**
|
||||
\brief Return functor that transforms a table into one that lacks columns listed in
|
||||
\c removed_cols array.
|
||||
|
|
|
@ -63,6 +63,9 @@ namespace datalog {
|
|||
return alloc(table_relation, *this, s, t);
|
||||
}
|
||||
|
||||
/**
|
||||
The newly created object takes ownership of the \c t object.
|
||||
*/
|
||||
relation_base * table_relation_plugin::mk_from_table(const relation_signature & s, table_base * t) {
|
||||
if (&t->get_plugin() == &m_table_plugin)
|
||||
return alloc(table_relation, *this, s, t);
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include "karr_relation.h"
|
||||
#include "bool_rewriter.h"
|
||||
|
||||
|
|
|
@ -290,19 +290,27 @@ namespace datalog {
|
|||
return res;
|
||||
}
|
||||
|
||||
#define _MIN_DONE_ 1
|
||||
|
||||
void rel_context::transform_rules() {
|
||||
rule_transformer transf(m_context);
|
||||
#ifdef _MIN_DONE_
|
||||
transf.register_plugin(alloc(mk_coi_filter, m_context));
|
||||
#endif
|
||||
transf.register_plugin(alloc(mk_filter_rules, m_context));
|
||||
transf.register_plugin(alloc(mk_simple_joins, m_context));
|
||||
if (m_context.unbound_compressor()) {
|
||||
transf.register_plugin(alloc(mk_unbound_compressor, m_context));
|
||||
}
|
||||
#ifdef _MIN_DONE_
|
||||
if (m_context.similarity_compressor()) {
|
||||
transf.register_plugin(alloc(mk_similarity_compressor, m_context));
|
||||
}
|
||||
#endif
|
||||
transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
|
||||
#ifdef _MIN_DONE_
|
||||
transf.register_plugin(alloc(mk_rule_inliner, m_context));
|
||||
#endif
|
||||
transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
|
||||
transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
|
||||
|
||||
|
|
|
@ -1065,7 +1065,7 @@ namespace datalog {
|
|||
t1.get_signature().size() == joined_col_cnt &&
|
||||
t2.get_signature().size() == joined_col_cnt) {
|
||||
for (unsigned i = 0; i < removed_col_cnt; ++i) {
|
||||
if (removed_cols[i] != i)
|
||||
if (removed_cols[i] != i || cols1[i] != cols2[i])
|
||||
goto general_fn;
|
||||
}
|
||||
return alloc(join_project_and_fn);
|
||||
|
|
|
@ -31,6 +31,7 @@ Notes:
|
|||
#include "propagate_values_tactic.h"
|
||||
#include "solve_eqs_tactic.h"
|
||||
#include "elim_uncnstr_tactic.h"
|
||||
#include "elim_term_ite_tactic.h"
|
||||
#include "tactical.h"
|
||||
#include "model_smt2_pp.h"
|
||||
#include "card2bv_tactic.h"
|
||||
|
@ -650,17 +651,19 @@ namespace opt {
|
|||
and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_elim_term_ite_tactic(m),
|
||||
// NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
|
||||
mk_simplify_tactic(m));
|
||||
opt_params optp(m_params);
|
||||
tactic_ref tac2, tac3;
|
||||
tactic_ref tac2, tac3, tac4;
|
||||
if (optp.elim_01()) {
|
||||
tac2 = mk_elim01_tactic(m);
|
||||
tac3 = mk_lia2card_tactic(m);
|
||||
tac4 = mk_elim_term_ite_tactic(m);
|
||||
params_ref lia_p;
|
||||
lia_p.set_bool("compile_equality", optp.pb_compile_equality());
|
||||
tac3->updt_params(lia_p);
|
||||
set_simplify(and_then(tac0.get(), tac2.get(), tac3.get()));
|
||||
set_simplify(and_then(tac0.get(), tac2.get(), tac3.get(), tac4.get()));
|
||||
}
|
||||
else {
|
||||
set_simplify(tac0.get());
|
||||
|
|
|
@ -42,7 +42,7 @@ namespace opt {
|
|||
m_context(mgr, m_params),
|
||||
m(mgr),
|
||||
m_fm(fm),
|
||||
m_objective_sorts(m),
|
||||
m_objective_terms(m),
|
||||
m_dump_benchmarks(false),
|
||||
m_first(true) {
|
||||
m_params.updt_params(p);
|
||||
|
@ -213,11 +213,13 @@ namespace opt {
|
|||
}
|
||||
else {
|
||||
SASSERT(has_shared);
|
||||
decrement_value(i, val);
|
||||
decrement_value(i, val);
|
||||
}
|
||||
m_objective_values[i] = val;
|
||||
TRACE("opt", { tout << val << "\n";
|
||||
tout << blocker << "\n";
|
||||
TRACE("opt", {
|
||||
tout << "objective: " << mk_pp(m_objective_terms[i].get(), m) << "\n";
|
||||
tout << "maximal value: " << val << "\n";
|
||||
tout << "new condition: " << blocker << "\n";
|
||||
model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); });
|
||||
}
|
||||
|
||||
|
@ -240,7 +242,7 @@ namespace opt {
|
|||
TRACE("opt", tout << is_sat << "\n";);
|
||||
if (is_sat != l_true) {
|
||||
// cop-out approximation
|
||||
if (arith_util(m).is_real(m_objective_sorts[i].get())) {
|
||||
if (arith_util(m).is_real(m_objective_terms[i].get())) {
|
||||
val -= inf_eps(inf_rational(rational(0), true));
|
||||
}
|
||||
else {
|
||||
|
@ -304,7 +306,7 @@ namespace opt {
|
|||
smt::theory_var v = get_optimizer().add_objective(term);
|
||||
m_objective_vars.push_back(v);
|
||||
m_objective_values.push_back(inf_eps(rational(-1), inf_rational()));
|
||||
m_objective_sorts.push_back(m.get_sort(term));
|
||||
m_objective_terms.push_back(term);
|
||||
m_valid_objectives.push_back(true);
|
||||
m_models.push_back(0);
|
||||
return v;
|
||||
|
@ -363,7 +365,7 @@ namespace opt {
|
|||
void opt_solver::reset_objectives() {
|
||||
m_objective_vars.reset();
|
||||
m_objective_values.reset();
|
||||
m_objective_sorts.reset();
|
||||
m_objective_terms.reset();
|
||||
m_valid_objectives.reset();
|
||||
}
|
||||
|
||||
|
|
|
@ -76,7 +76,7 @@ namespace opt {
|
|||
svector<smt::theory_var> m_objective_vars;
|
||||
vector<inf_eps> m_objective_values;
|
||||
sref_vector<model> m_models;
|
||||
sort_ref_vector m_objective_sorts;
|
||||
expr_ref_vector m_objective_terms;
|
||||
svector<bool> m_valid_objectives;
|
||||
bool m_dump_benchmarks;
|
||||
static unsigned m_dump_count;
|
||||
|
|
|
@ -141,6 +141,7 @@ namespace opt {
|
|||
ors.push_back(m_s->mk_ge(i, m_upper[i]));
|
||||
}
|
||||
|
||||
|
||||
fml = m.mk_or(ors.size(), ors.c_ptr());
|
||||
tmp = m.mk_fresh_const("b", m.mk_bool_sort());
|
||||
fml = m.mk_implies(tmp, fml);
|
||||
|
@ -150,6 +151,7 @@ namespace opt {
|
|||
solver::scoped_push _push(*m_s);
|
||||
while (!m_cancel) {
|
||||
m_s->assert_expr(fml);
|
||||
TRACE("opt", tout << fml << "\n";);
|
||||
is_sat = m_s->check_sat(1,vars);
|
||||
if (is_sat == l_true) {
|
||||
disj.reset();
|
||||
|
@ -343,6 +345,7 @@ namespace opt {
|
|||
m_lower[i] = m_s->saved_objective_value(i);
|
||||
}
|
||||
}
|
||||
TRACE("opt", tout << "strengthen bound: " << block << "\n";);
|
||||
m_s->assert_expr(block);
|
||||
|
||||
// TBD: only works for simplex
|
||||
|
|
|
@ -1,4 +1,10 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#include"smtlib.h"
|
||||
#include"ast_pp.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include "ast.h"
|
||||
#include "nlarith_util.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
|
|
|
@ -1,4 +1,10 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#ifndef __QE_ARITH_H_
|
||||
#define __QE_ARITH_H_
|
||||
|
||||
|
|
|
@ -1,4 +1,10 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#include "qe.h"
|
||||
#include "array_decl_plugin.h"
|
||||
#include "expr_safe_replace.h"
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include "qe_cmd.h"
|
||||
#include "qe.h"
|
||||
#include "cmd_context.h"
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
// ---------------------
|
||||
// datatypes
|
||||
// Quantifier elimination routine for recursive data-types.
|
||||
|
|
|
@ -1,4 +1,10 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#include "qe.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "dl_decl_plugin.h"
|
||||
|
|
|
@ -1,48 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qe_mbp.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Model-based projection utilities
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2015-5-28
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef __QE_MBP_H__
|
||||
#define __QE_MBP_H__
|
||||
|
||||
#include "ast.h"
|
||||
#include "params.h"
|
||||
|
||||
namespace qe {
|
||||
class mbp {
|
||||
class impl;
|
||||
impl * m_impl;
|
||||
public:
|
||||
mbp(ast_manager& m);
|
||||
|
||||
~mbp();
|
||||
|
||||
/**
|
||||
\brief
|
||||
Apply model-based qe on constants provided as vector of variables.
|
||||
Return the updated formula and updated set of variables that were not eliminated.
|
||||
|
||||
*/
|
||||
void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml);
|
||||
|
||||
void set_cancel(bool f);
|
||||
};
|
||||
}
|
||||
|
||||
#endif
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include "qe_util.h"
|
||||
#include "bool_rewriter.h"
|
||||
|
||||
|
|
281
src/qe/qsat.cpp
281
src/qe/qsat.cpp
|
@ -1,281 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qsat.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Quantifier Satisfiability Solver.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2015-5-28
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include "qsat.h"
|
||||
#include "smt_kernel.h"
|
||||
#include "qe_mbp.h"
|
||||
#include "smt_params.h"
|
||||
#include "ast_util.h"
|
||||
|
||||
using namespace qe;
|
||||
|
||||
struct qdef_t {
|
||||
expr_ref m_pred;
|
||||
expr_ref m_expr;
|
||||
expr_ref_vector m_vars;
|
||||
bool m_is_forall;
|
||||
qdef_t(expr_ref& p, expr_ref& e, expr_ref_vector const& vars, bool is_forall):
|
||||
m_pred(p),
|
||||
m_expr(e),
|
||||
m_vars(vars),
|
||||
m_is_forall(is_forall) {}
|
||||
};
|
||||
|
||||
typedef vector<qdef_t> qdefs_t;
|
||||
|
||||
struct pdef_t {
|
||||
expr_ref m_pred;
|
||||
expr_ref m_atom;
|
||||
pdef_t(expr_ref& p, expr* a):
|
||||
m_pred(p),
|
||||
m_atom(a, p.get_manager())
|
||||
{}
|
||||
};
|
||||
|
||||
class qsat::impl {
|
||||
ast_manager& m;
|
||||
qe::mbp mbp;
|
||||
smt_params m_smtp;
|
||||
smt::kernel m_kernel;
|
||||
expr_ref m_fml_pred; // predicate that encodes top-level formula
|
||||
expr_ref_vector m_atoms; // predicates that encode atomic subformulas
|
||||
|
||||
|
||||
lbool check_sat() {
|
||||
// TBD main procedure goes here.
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate.
|
||||
*/
|
||||
void remove_quantifiers(expr_ref_vector& fmls, qdefs_t& defs) {
|
||||
|
||||
}
|
||||
|
||||
/**
|
||||
\brief create propositional abstration of formula by replacing atomic sub-formulas by fresh
|
||||
propositional variables, and adding definitions for each propositional formula on the side.
|
||||
Assumption is that the formula is quantifier-free.
|
||||
*/
|
||||
void mk_abstract(expr_ref& fml, vector<pdef_t>& pdefs) {
|
||||
expr_ref_vector todo(m), trail(m);
|
||||
obj_map<expr,expr*> cache;
|
||||
ptr_vector<expr> args;
|
||||
expr_ref r(m);
|
||||
todo.push_back(fml);
|
||||
while (!todo.empty()) {
|
||||
expr* e = todo.back();
|
||||
if (cache.contains(e)) {
|
||||
todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
SASSERT(is_app(e));
|
||||
app* a = to_app(e);
|
||||
if (a->get_family_id() == m.get_basic_family_id()) {
|
||||
unsigned sz = a->get_num_args();
|
||||
args.reset();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr* f = a->get_arg(i);
|
||||
if (cache.find(f, f)) {
|
||||
args.push_back(f);
|
||||
}
|
||||
else {
|
||||
todo.push_back(f);
|
||||
}
|
||||
}
|
||||
if (args.size() == sz) {
|
||||
r = m.mk_app(a->get_decl(), sz, args.c_ptr());
|
||||
cache.insert(e, r);
|
||||
trail.push_back(r);
|
||||
todo.pop_back();
|
||||
}
|
||||
}
|
||||
else if (is_uninterp_const(a)) {
|
||||
cache.insert(e, e);
|
||||
}
|
||||
else {
|
||||
// TBD: nested Booleans.
|
||||
|
||||
r = m.mk_fresh_const("p",m.mk_bool_sort());
|
||||
trail.push_back(r);
|
||||
cache.insert(e, r);
|
||||
pdefs.push_back(pdef_t(r, e));
|
||||
}
|
||||
}
|
||||
fml = cache.find(fml);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief use dual propagation to minimize model.
|
||||
*/
|
||||
bool minimize_assignment(expr_ref_vector& assignment, expr* not_fml) {
|
||||
bool result = false;
|
||||
assignment.push_back(not_fml);
|
||||
lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
|
||||
switch (res) {
|
||||
case l_true:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
case l_undef:
|
||||
break;
|
||||
case l_false:
|
||||
result = true;
|
||||
get_core(assignment, not_fml);
|
||||
break;
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
lbool check_sat(expr_ref_vector& assignment, expr* fml) {
|
||||
assignment.push_back(fml);
|
||||
lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
|
||||
switch (res) {
|
||||
case l_true: {
|
||||
model_ref mdl;
|
||||
expr_ref tmp(m);
|
||||
assignment.reset();
|
||||
m_kernel.get_model(mdl);
|
||||
for (unsigned i = 0; i < m_atoms.size(); ++i) {
|
||||
expr* p = m_atoms[i].get();
|
||||
if (mdl->eval(p, tmp)) {
|
||||
if (m.is_true(tmp)) {
|
||||
assignment.push_back(p);
|
||||
}
|
||||
else if (m.is_false(tmp)) {
|
||||
assignment.push_back(m.mk_not(p));
|
||||
}
|
||||
}
|
||||
}
|
||||
expr_ref not_fml = mk_not(fml);
|
||||
if (!minimize_assignment(assignment, not_fml)) {
|
||||
res = l_undef;
|
||||
}
|
||||
break;
|
||||
}
|
||||
case l_undef:
|
||||
break;
|
||||
case l_false:
|
||||
get_core(assignment, fml);
|
||||
break;
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
void get_core(expr_ref_vector& core, expr* exclude) {
|
||||
unsigned sz = m_kernel.get_unsat_core_size();
|
||||
core.reset();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr* e = m_kernel.get_unsat_core_expr(i);
|
||||
if (e != exclude) {
|
||||
core.push_back(e);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref mk_not(expr* e) {
|
||||
return expr_ref(::mk_not(m, e), m);
|
||||
}
|
||||
|
||||
public:
|
||||
impl(ast_manager& m):
|
||||
m(m),
|
||||
mbp(m),
|
||||
m_kernel(m, m_smtp),
|
||||
m_fml_pred(m),
|
||||
m_atoms(m) {}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
}
|
||||
|
||||
void collect_param_descrs(param_descrs & r) {
|
||||
}
|
||||
|
||||
void operator()(/* in */ goal_ref const & in,
|
||||
/* out */ goal_ref_buffer & result,
|
||||
/* out */ model_converter_ref & mc,
|
||||
/* out */ proof_converter_ref & pc,
|
||||
/* out */ expr_dependency_ref & core) {
|
||||
|
||||
}
|
||||
|
||||
void collect_statistics(statistics & st) const {
|
||||
|
||||
}
|
||||
void reset_statistics() {
|
||||
}
|
||||
|
||||
void cleanup() {
|
||||
}
|
||||
|
||||
void set_logic(symbol const & l) {
|
||||
}
|
||||
|
||||
void set_progress_callback(progress_callback * callback) {
|
||||
}
|
||||
|
||||
tactic * translate(ast_manager & m) {
|
||||
return 0;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
qsat::qsat(ast_manager& m) {
|
||||
m_impl = alloc(impl, m);
|
||||
}
|
||||
|
||||
qsat::~qsat() {
|
||||
dealloc(m_impl);
|
||||
}
|
||||
|
||||
void qsat::updt_params(params_ref const & p) {
|
||||
m_impl->updt_params(p);
|
||||
}
|
||||
void qsat::collect_param_descrs(param_descrs & r) {
|
||||
m_impl->collect_param_descrs(r);
|
||||
}
|
||||
void qsat::operator()(/* in */ goal_ref const & in,
|
||||
/* out */ goal_ref_buffer & result,
|
||||
/* out */ model_converter_ref & mc,
|
||||
/* out */ proof_converter_ref & pc,
|
||||
/* out */ expr_dependency_ref & core) {
|
||||
(*m_impl)(in, result, mc, pc, core);
|
||||
}
|
||||
|
||||
void qsat::collect_statistics(statistics & st) const {
|
||||
m_impl->collect_statistics(st);
|
||||
}
|
||||
void qsat::reset_statistics() {
|
||||
m_impl->reset_statistics();
|
||||
}
|
||||
void qsat::cleanup() {
|
||||
m_impl->cleanup();
|
||||
}
|
||||
void qsat::set_logic(symbol const & l) {
|
||||
m_impl->set_logic(l);
|
||||
}
|
||||
void qsat::set_progress_callback(progress_callback * callback) {
|
||||
m_impl->set_progress_callback(callback);
|
||||
}
|
||||
tactic * qsat::translate(ast_manager & m) {
|
||||
return m_impl->translate(m);
|
||||
}
|
||||
|
||||
|
|
@ -1,52 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qsat.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Quantifier Satisfiability Solver.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2015-5-28
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef __QE_QSAT_H__
|
||||
#define __QE_QSAT_H__
|
||||
|
||||
#include "tactic.h"
|
||||
|
||||
namespace qe {
|
||||
class qsat : public tactic {
|
||||
class impl;
|
||||
impl * m_impl;
|
||||
public:
|
||||
qsat(ast_manager& m);
|
||||
~qsat();
|
||||
|
||||
virtual void updt_params(params_ref const & p);
|
||||
virtual void collect_param_descrs(param_descrs & r);
|
||||
virtual void operator()(/* in */ goal_ref const & in,
|
||||
/* out */ goal_ref_buffer & result,
|
||||
/* out */ model_converter_ref & mc,
|
||||
/* out */ proof_converter_ref & pc,
|
||||
/* out */ expr_dependency_ref & core);
|
||||
|
||||
virtual void collect_statistics(statistics & st) const;
|
||||
virtual void reset_statistics();
|
||||
virtual void cleanup() = 0;
|
||||
virtual void set_logic(symbol const & l);
|
||||
virtual void set_progress_callback(progress_callback * callback);
|
||||
virtual tactic * translate(ast_manager & m);
|
||||
|
||||
};
|
||||
};
|
||||
|
||||
#endif
|
|
@ -210,6 +210,7 @@ namespace sat {
|
|||
public:
|
||||
bool inconsistent() const { return m_inconsistent; }
|
||||
unsigned num_vars() const { return m_level.size(); }
|
||||
unsigned num_clauses() const;
|
||||
bool is_external(bool_var v) const { return m_external[v] != 0; }
|
||||
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
|
||||
unsigned scope_lvl() const { return m_scope_lvl; }
|
||||
|
@ -447,7 +448,6 @@ namespace sat {
|
|||
protected:
|
||||
void display_binary(std::ostream & out) const;
|
||||
void display_units(std::ostream & out) const;
|
||||
unsigned num_clauses() const;
|
||||
bool is_unit(clause const & c) const;
|
||||
bool is_empty(clause const & c) const;
|
||||
bool check_missed_propagation(clause_vector const & cs) const;
|
||||
|
|
|
@ -163,6 +163,9 @@ void parse_cmd_line_args(int argc, char ** argv) {
|
|||
else if (strcmp(opt_name, "smt2") == 0) {
|
||||
g_input_kind = IN_SMTLIB_2;
|
||||
}
|
||||
else if (strcmp(opt_name, "dl") == 0) {
|
||||
g_input_kind = IN_DATALOG;
|
||||
}
|
||||
else if (strcmp(opt_name, "in") == 0) {
|
||||
g_standard_input = true;
|
||||
}
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include<fstream>
|
||||
#include<signal.h>
|
||||
#include<time.h>
|
||||
|
|
|
@ -1,4 +1,10 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
/**
|
||||
\page cmdline Command line options
|
||||
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
static char const g_pattern_database[] =
|
||||
"(benchmark patterns \n"
|
||||
" :status unknown \n"
|
||||
|
|
|
@ -885,6 +885,7 @@ namespace smt {
|
|||
void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v);
|
||||
enum max_min_t { UNBOUNDED, AT_BOUND, OPTIMIZED, BEST_EFFORT};
|
||||
max_min_t max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared);
|
||||
bool has_interface_equality(theory_var v);
|
||||
bool max_min(svector<theory_var> const & vars);
|
||||
|
||||
max_min_t max_min(row& r, bool max, bool maintain_integrality, bool& has_shared);
|
||||
|
|
|
@ -1545,6 +1545,25 @@ namespace smt {
|
|||
return is_tighter;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Check if bound change affects interface equality.
|
||||
*/
|
||||
template<typename Ext>
|
||||
bool theory_arith<Ext>::has_interface_equality(theory_var x) {
|
||||
theory_var num = get_num_vars();
|
||||
context& ctx = get_context();
|
||||
enode* r = get_enode(x)->get_root();
|
||||
for (theory_var v = 0; v < num; v++) {
|
||||
if (v == x) continue;
|
||||
enode* n = get_enode(v);
|
||||
if (ctx.is_shared(n) && n->get_root() == r) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Maximize (Minimize) the given temporary row.
|
||||
Return true if succeeded.
|
||||
|
@ -1660,13 +1679,23 @@ namespace smt {
|
|||
SASSERT(!maintain_integrality || valid_assignment());
|
||||
continue;
|
||||
}
|
||||
if (ctx.is_shared(get_enode(x_j))) {
|
||||
#if 0
|
||||
if (ctx.is_shared(get_enode(x_j)) && has_interface_equality(x_j)) {
|
||||
++best_efforts;
|
||||
}
|
||||
else {
|
||||
SASSERT(unbounded_gain(max_gain));
|
||||
has_shared = false;
|
||||
best_efforts = 0;
|
||||
}
|
||||
#endif
|
||||
//
|
||||
// NB. As it stands this is a possibly unsound conclusion for shared theories.
|
||||
// the tradeoff is non-termination for unbounded objectives in the
|
||||
// presence of sharing.
|
||||
//
|
||||
has_shared = false;
|
||||
best_efforts = 0;
|
||||
result = UNBOUNDED;
|
||||
break;
|
||||
}
|
||||
|
|
Some files were not shown because too many files have changed in this diff Show more
Loading…
Reference in a new issue