mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
This commit is contained in:
commit
634a93d699
|
@ -899,6 +899,7 @@ def _coerce_expr_merge(s, a):
|
|||
return s
|
||||
else:
|
||||
if __debug__:
|
||||
_z3_assert(s1.ctx == s.ctx, "context mismatch")
|
||||
_z3_assert(False, "sort mismatch")
|
||||
else:
|
||||
return s
|
||||
|
@ -1459,9 +1460,18 @@ def And(*args):
|
|||
>>> And(P)
|
||||
And(p__0, p__1, p__2, p__3, p__4)
|
||||
"""
|
||||
args = _get_args(args)
|
||||
ctx = _ctx_from_ast_arg_list(args)
|
||||
last_arg = None
|
||||
if len(args) > 0:
|
||||
last_arg = args[len(args)-1]
|
||||
if isinstance(last_arg, Context):
|
||||
ctx = args[len(args)-1]
|
||||
args = args[:len(args)-1]
|
||||
else:
|
||||
ctx = main_ctx()
|
||||
args = _get_args(args)
|
||||
ctx_args = _ctx_from_ast_arg_list(args, ctx)
|
||||
if __debug__:
|
||||
_z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
|
||||
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
|
||||
if _has_probe(args):
|
||||
return _probe_and(args, ctx)
|
||||
|
@ -1480,9 +1490,18 @@ def Or(*args):
|
|||
>>> Or(P)
|
||||
Or(p__0, p__1, p__2, p__3, p__4)
|
||||
"""
|
||||
args = _get_args(args)
|
||||
ctx = _ctx_from_ast_arg_list(args)
|
||||
last_arg = None
|
||||
if len(args) > 0:
|
||||
last_arg = args[len(args)-1]
|
||||
if isinstance(last_arg, Context):
|
||||
ctx = args[len(args)-1]
|
||||
args = args[:len(args)-1]
|
||||
else:
|
||||
ctx = main_ctx()
|
||||
args = _get_args(args)
|
||||
ctx_args = _ctx_from_ast_arg_list(args, ctx)
|
||||
if __debug__:
|
||||
_z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
|
||||
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
|
||||
if _has_probe(args):
|
||||
return _probe_or(args, ctx)
|
||||
|
@ -4128,6 +4147,7 @@ class Datatype:
|
|||
"""
|
||||
if __debug__:
|
||||
_z3_assert(isinstance(name, str), "String expected")
|
||||
_z3_assert(name != "", "Constructor name cannot be empty")
|
||||
return self.declare_core(name, "is_" + name, *args)
|
||||
|
||||
def __repr__(self):
|
||||
|
|
|
@ -599,7 +599,23 @@ namespace datalog {
|
|||
return 0;
|
||||
}
|
||||
result = mk_compare(OP_DL_LT, m_lt_sym, domain);
|
||||
break;
|
||||
break;
|
||||
|
||||
case OP_DL_REP: {
|
||||
if (!check_domain(0, 0, num_parameters) ||
|
||||
!check_domain(1, 1, arity)) return 0;
|
||||
func_decl_info info(m_family_id, k, 0, 0);
|
||||
result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info);
|
||||
break;
|
||||
}
|
||||
|
||||
case OP_DL_ABS: {
|
||||
if (!check_domain(0, 0, num_parameters) ||
|
||||
!check_domain(1, 1, arity)) return 0;
|
||||
func_decl_info info(m_family_id, k, 0, 0);
|
||||
result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info);
|
||||
break;
|
||||
}
|
||||
|
||||
default:
|
||||
m_manager->raise_exception("operator not recognized");
|
||||
|
|
|
@ -48,6 +48,8 @@ namespace datalog {
|
|||
OP_RA_CLONE,
|
||||
OP_DL_CONSTANT,
|
||||
OP_DL_LT,
|
||||
OP_DL_REP,
|
||||
OP_DL_ABS,
|
||||
LAST_RA_OP
|
||||
};
|
||||
|
||||
|
|
|
@ -17,7 +17,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
#ifndef _SCOPED_PROOF__H_
|
||||
#define _SCOPED_PROOF_H_
|
||||
#define _SCOPED_PROOF__H_
|
||||
|
||||
#include "ast.h"
|
||||
|
||||
|
|
|
@ -189,7 +189,7 @@ class psort_app : public psort {
|
|||
m.inc_ref(d);
|
||||
m.inc_ref(num_args, args);
|
||||
SASSERT(num_args == m_decl->get_num_params() || m_decl->has_var_params());
|
||||
DEBUG_CODE(for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this););
|
||||
DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); });
|
||||
}
|
||||
|
||||
virtual void finalize(pdecl_manager & m) {
|
||||
|
|
|
@ -29,7 +29,7 @@ using namespace stl_ext;
|
|||
|
||||
namespace Duality {
|
||||
|
||||
class implicant_solver;
|
||||
struct implicant_solver;
|
||||
|
||||
/* Generic operations on Z3 formulas */
|
||||
|
||||
|
@ -253,6 +253,27 @@ protected:
|
|||
}
|
||||
|
||||
void assert_axiom(const expr &axiom){
|
||||
#if 1
|
||||
// HACK: large "distict" predicates can kill the legacy SMT solver.
|
||||
// encode them with a UIF
|
||||
if(axiom.is_app() && axiom.decl().get_decl_kind() == Distinct)
|
||||
if(axiom.num_args() > 10){
|
||||
sort s = axiom.arg(0).get_sort();
|
||||
std::vector<sort> sv;
|
||||
sv.push_back(s);
|
||||
int nargs = axiom.num_args();
|
||||
std::vector<expr> args(nargs);
|
||||
func_decl f = ctx->fresh_func_decl("@distinct",sv,ctx->int_sort());
|
||||
for(int i = 0; i < nargs; i++){
|
||||
expr a = axiom.arg(i);
|
||||
expr new_cnstr = f(a) == ctx->int_val(i);
|
||||
args[i] = new_cnstr;
|
||||
}
|
||||
expr cnstr = ctx->make(And,args);
|
||||
islvr->AssertInterpolationAxiom(cnstr);
|
||||
return;
|
||||
}
|
||||
#endif
|
||||
islvr->AssertInterpolationAxiom(axiom);
|
||||
}
|
||||
|
||||
|
|
|
@ -100,6 +100,7 @@ namespace Duality {
|
|||
};
|
||||
|
||||
Reporter *CreateStdoutReporter(RPFP *rpfp);
|
||||
Reporter *CreateConjectureFileReporter(RPFP *rpfp, const std::string &fname);
|
||||
|
||||
/** Object we throw in case of catastrophe. */
|
||||
|
||||
|
@ -125,6 +126,7 @@ namespace Duality {
|
|||
{
|
||||
rpfp = _rpfp;
|
||||
reporter = 0;
|
||||
conj_reporter = 0;
|
||||
heuristic = 0;
|
||||
unwinding = 0;
|
||||
FullExpand = false;
|
||||
|
@ -274,6 +276,7 @@ namespace Duality {
|
|||
|
||||
RPFP *rpfp; // the input RPFP
|
||||
Reporter *reporter; // object for logging
|
||||
Reporter *conj_reporter; // object for logging conjectures
|
||||
Heuristic *heuristic; // expansion heuristic
|
||||
context &ctx; // Z3 context
|
||||
solver &slvr; // Z3 solver
|
||||
|
@ -297,6 +300,7 @@ namespace Duality {
|
|||
int last_decisions;
|
||||
hash_set<Node *> overapproxes;
|
||||
std::vector<Proposer *> proposers;
|
||||
std::string ConjectureFile;
|
||||
|
||||
#ifdef BOUNDED
|
||||
struct Counter {
|
||||
|
@ -310,6 +314,7 @@ namespace Duality {
|
|||
/** Solve the problem. */
|
||||
virtual bool Solve(){
|
||||
reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp);
|
||||
conj_reporter = ConjectureFile.empty() ? 0 : CreateConjectureFileReporter(rpfp,ConjectureFile);
|
||||
#ifndef LOCALIZE_CONJECTURES
|
||||
heuristic = !cex.get_tree() ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex);
|
||||
#else
|
||||
|
@ -340,6 +345,8 @@ namespace Duality {
|
|||
delete heuristic;
|
||||
// delete unwinding; // keep the unwinding for future mining of predicates
|
||||
delete reporter;
|
||||
if(conj_reporter)
|
||||
delete conj_reporter;
|
||||
for(unsigned i = 0; i < proposers.size(); i++)
|
||||
delete proposers[i];
|
||||
return res;
|
||||
|
@ -449,6 +456,9 @@ namespace Duality {
|
|||
if(option == "recursion_bound"){
|
||||
return SetIntOption(RecursionBound,value);
|
||||
}
|
||||
if(option == "conjecture_file"){
|
||||
ConjectureFile = value;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
@ -728,6 +738,13 @@ namespace Duality {
|
|||
return ctx.constant(name.c_str(),ctx.bool_sort());
|
||||
}
|
||||
|
||||
/** Make a boolean variable to act as a "marker" for a pair of nodes. */
|
||||
expr NodeMarker(Node *node1, Node *node2){
|
||||
std::string name = std::string("@m_") + string_of_int(node1->number);
|
||||
name += std::string("_") + string_of_int(node2->number);
|
||||
return ctx.constant(name.c_str(),ctx.bool_sort());
|
||||
}
|
||||
|
||||
/** Union the annotation of dst into src. If with_markers is
|
||||
true, we conjoin the annotation formula of dst with its
|
||||
marker. This allows us to discover which disjunct is
|
||||
|
@ -1136,19 +1153,19 @@ namespace Duality {
|
|||
}
|
||||
|
||||
|
||||
void GenNodeSolutionWithMarkersAux(Node *node, RPFP::Transformer &annot, expr &marker_disjunction){
|
||||
void GenNodeSolutionWithMarkersAux(Node *node, RPFP::Transformer &annot, expr &marker_disjunction, Node *other_node){
|
||||
#ifdef BOUNDED
|
||||
if(RecursionBound >= 0 && NodePastRecursionBound(node))
|
||||
return;
|
||||
#endif
|
||||
RPFP::Transformer temp = node->Annotation;
|
||||
expr marker = NodeMarker(node);
|
||||
expr marker = (!other_node) ? NodeMarker(node) : NodeMarker(node, other_node);
|
||||
temp.Formula = (!marker || temp.Formula);
|
||||
annot.IntersectWith(temp);
|
||||
marker_disjunction = marker_disjunction || marker;
|
||||
}
|
||||
|
||||
bool GenNodeSolutionWithMarkers(Node *node, RPFP::Transformer &annot, bool expanded_only = false){
|
||||
bool GenNodeSolutionWithMarkers(Node *node, RPFP::Transformer &annot, bool expanded_only = false, Node *other_node = 0){
|
||||
bool res = false;
|
||||
annot.SetFull();
|
||||
expr marker_disjunction = ctx.bool_val(false);
|
||||
|
@ -1156,7 +1173,7 @@ namespace Duality {
|
|||
for(unsigned j = 0; j < insts.size(); j++){
|
||||
Node *node = insts[j];
|
||||
if(indset->Contains(insts[j])){
|
||||
GenNodeSolutionWithMarkersAux(node, annot, marker_disjunction); res = true;
|
||||
GenNodeSolutionWithMarkersAux(node, annot, marker_disjunction, other_node); res = true;
|
||||
}
|
||||
}
|
||||
annot.Formula = annot.Formula && marker_disjunction;
|
||||
|
@ -1253,7 +1270,7 @@ namespace Duality {
|
|||
Node *inst = insts[k];
|
||||
if(indset->Contains(inst)){
|
||||
if(checker->Empty(node) ||
|
||||
eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){
|
||||
eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst,node)),ctx.bool_val(true))){
|
||||
candidate.Children.push_back(inst);
|
||||
goto next_child;
|
||||
}
|
||||
|
@ -1336,7 +1353,7 @@ namespace Duality {
|
|||
for(unsigned j = 0; j < edge->Children.size(); j++){
|
||||
Node *oc = edge->Children[j];
|
||||
Node *nc = gen_cands_edge->Children[j];
|
||||
GenNodeSolutionWithMarkers(oc,nc->Annotation,true);
|
||||
GenNodeSolutionWithMarkers(oc,nc->Annotation,true,nc);
|
||||
}
|
||||
checker->AssertEdge(gen_cands_edge,1,true);
|
||||
return root;
|
||||
|
@ -1462,6 +1479,8 @@ namespace Duality {
|
|||
bool Update(Node *node, const RPFP::Transformer &fact, bool eager=false){
|
||||
if(!node->Annotation.SubsetEq(fact)){
|
||||
reporter->Update(node,fact,eager);
|
||||
if(conj_reporter)
|
||||
conj_reporter->Update(node,fact,eager);
|
||||
indset->Update(node,fact);
|
||||
updated_nodes.insert(node->map);
|
||||
node->Annotation.IntersectWith(fact);
|
||||
|
@ -2201,7 +2220,7 @@ namespace Duality {
|
|||
#endif
|
||||
int expand_max = 1;
|
||||
if(0&&duality->BatchExpand){
|
||||
int thing = stack.size() * 0.1;
|
||||
int thing = stack.size() / 10; // * 0.1;
|
||||
expand_max = std::max(1,thing);
|
||||
if(expand_max > 1)
|
||||
std::cout << "foo!\n";
|
||||
|
@ -3043,6 +3062,7 @@ namespace Duality {
|
|||
};
|
||||
};
|
||||
|
||||
static int stop_event = -1;
|
||||
|
||||
class StreamReporter : public Reporter {
|
||||
std::ostream &s;
|
||||
|
@ -3052,6 +3072,9 @@ namespace Duality {
|
|||
int event;
|
||||
int depth;
|
||||
void ev(){
|
||||
if(stop_event == event){
|
||||
std::cout << "stop!\n";
|
||||
}
|
||||
s << "[" << event++ << "]" ;
|
||||
}
|
||||
virtual void Extend(RPFP::Node *node){
|
||||
|
@ -3129,4 +3152,28 @@ namespace Duality {
|
|||
Reporter *CreateStdoutReporter(RPFP *rpfp){
|
||||
return new StreamReporter(rpfp, std::cout);
|
||||
}
|
||||
|
||||
class ConjectureFileReporter : public Reporter {
|
||||
std::ofstream s;
|
||||
public:
|
||||
ConjectureFileReporter(RPFP *_rpfp, const std::string &fname)
|
||||
: Reporter(_rpfp), s(fname.c_str()) {}
|
||||
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update, bool eager){
|
||||
s << "(define-fun " << node->Name.name() << " (";
|
||||
for(unsigned i = 0; i < update.IndParams.size(); i++){
|
||||
if(i != 0)
|
||||
s << " ";
|
||||
s << "(" << update.IndParams[i] << " " << update.IndParams[i].get_sort() << ")";
|
||||
}
|
||||
s << ") Bool \n";
|
||||
s << update.Formula << ")\n";
|
||||
s << std::endl;
|
||||
}
|
||||
};
|
||||
|
||||
Reporter *CreateConjectureFileReporter(RPFP *rpfp, const std::string &fname){
|
||||
return new ConjectureFileReporter(rpfp, fname);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
|
|
@ -397,6 +397,11 @@ namespace Duality {
|
|||
|
||||
sort array_domain() const;
|
||||
sort array_range() const;
|
||||
|
||||
friend std::ostream & operator<<(std::ostream & out, sort const & m){
|
||||
m.ctx().print_expr(out,m);
|
||||
return out;
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
|
|
|
@ -260,7 +260,7 @@ void iz3base::check_interp(const std::vector<ast> &itps, std::vector<ast> &theor
|
|||
#endif
|
||||
}
|
||||
|
||||
bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof){
|
||||
bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof, std::vector<ast> &vars){
|
||||
|
||||
params_ref p;
|
||||
p.set_bool("proof", true); // this is currently useless
|
||||
|
@ -277,6 +277,15 @@ bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof){
|
|||
::ast *proof = s.get_proof();
|
||||
_proof = cook(proof);
|
||||
}
|
||||
else if(vars.size()) {
|
||||
model_ref(_m);
|
||||
s.get_model(_m);
|
||||
for(unsigned i = 0; i < vars.size(); i++){
|
||||
expr_ref r(m());
|
||||
_m.get()->eval(to_expr(vars[i].raw()),r,true);
|
||||
vars[i] = cook(r.get());
|
||||
}
|
||||
}
|
||||
dealloc(m_solver);
|
||||
return res != l_false;
|
||||
}
|
||||
|
|
|
@ -113,7 +113,7 @@ class iz3base : public iz3mgr, public scopes {
|
|||
void check_interp(const std::vector<ast> &itps, std::vector<ast> &theory);
|
||||
|
||||
/** For convenience -- is this formula SAT? */
|
||||
bool is_sat(const std::vector<ast> &consts, ast &_proof);
|
||||
bool is_sat(const std::vector<ast> &consts, ast &_proof, std::vector<ast> &vars);
|
||||
|
||||
/** Interpolator for clauses, to be implemented */
|
||||
virtual void interpolate_clause(std::vector<ast> &lits, std::vector<ast> &itps){
|
||||
|
|
|
@ -29,6 +29,10 @@ Revision History:
|
|||
#ifndef IZ3_HASH_H
|
||||
#define IZ3_HASH_H
|
||||
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4267)
|
||||
#endif
|
||||
|
||||
#include <string>
|
||||
#include <vector>
|
||||
#include <iterator>
|
||||
|
|
|
@ -387,10 +387,13 @@ class iz3mgr {
|
|||
return UnknownTheory;
|
||||
}
|
||||
|
||||
enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,UnknownKind};
|
||||
enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,ArithMysteryKind,UnknownKind};
|
||||
|
||||
lemma_kind get_theory_lemma_kind(const ast &proof){
|
||||
symb s = sym(proof);
|
||||
if(s->get_num_parameters() < 2) {
|
||||
return ArithMysteryKind; // Bad -- Z3 hasn't told us
|
||||
}
|
||||
::symbol p0;
|
||||
bool ok = s->get_parameter(1).is_symbol(p0);
|
||||
if(!ok) return UnknownKind;
|
||||
|
|
|
@ -607,7 +607,29 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
return res;
|
||||
}
|
||||
|
||||
ast distribute_coeff(const ast &coeff, const ast &s){
|
||||
if(sym(s) == sum){
|
||||
if(sym(arg(s,2)) == sum)
|
||||
return make(sum,
|
||||
distribute_coeff(coeff,arg(s,0)),
|
||||
make_int(rational(1)),
|
||||
distribute_coeff(make(Times,coeff,arg(s,1)), arg(s,2)));
|
||||
else
|
||||
return make(sum,
|
||||
distribute_coeff(coeff,arg(s,0)),
|
||||
make(Times,coeff,arg(s,1)),
|
||||
arg(s,2));
|
||||
}
|
||||
if(op(s) == Leq && arg(s,1) == make_int(rational(0)) && arg(s,2) == make_int(rational(0)))
|
||||
return s;
|
||||
return make(sum,make(Leq,make_int(rational(0)),make_int(rational(0))),coeff,s);
|
||||
}
|
||||
|
||||
ast simplify_sum(std::vector<ast> &args){
|
||||
if(args[1] != make_int(rational(1))){
|
||||
if(sym(args[2]) == sum)
|
||||
return make(sum,args[0],make_int(rational(1)),distribute_coeff(args[1],args[2]));
|
||||
}
|
||||
ast Aproves = mk_true(), Bproves = mk_true();
|
||||
ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves);
|
||||
if(!is_normal_ineq(ineq)) throw cannot_simplify();
|
||||
|
@ -757,6 +779,22 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
ast Bcond = my_implies(Bproves1,my_and(Aproves1,z3_simplify(ineq2)));
|
||||
// if(!is_true(Aproves1) || !is_true(Bproves1))
|
||||
// std::cout << "foo!\n";;
|
||||
if(y == make_int(rational(0)) && op(x) == Plus && num_args(x) == 2){
|
||||
if(get_term_type(arg(x,0)) == LitA){
|
||||
ast iter = z3_simplify(make(Plus,arg(x,0),get_ineq_rhs(xleqy)));
|
||||
ast rewrite1 = make_rewrite(LitA,pos_add(0,top_pos),Acond,make(Equal,arg(x,0),iter));
|
||||
iter = make(Plus,iter,arg(x,1));
|
||||
ast rewrite2 = make_rewrite(LitB,top_pos,Bcond,make(Equal,iter,y));
|
||||
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
|
||||
}
|
||||
if(get_term_type(arg(x,1)) == LitA){
|
||||
ast iter = z3_simplify(make(Plus,arg(x,1),get_ineq_rhs(xleqy)));
|
||||
ast rewrite1 = make_rewrite(LitA,pos_add(1,top_pos),Acond,make(Equal,arg(x,1),iter));
|
||||
iter = make(Plus,arg(x,0),iter);
|
||||
ast rewrite2 = make_rewrite(LitB,top_pos,Bcond,make(Equal,iter,y));
|
||||
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
|
||||
}
|
||||
}
|
||||
if(get_term_type(x) == LitA){
|
||||
ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy)));
|
||||
ast rewrite1 = make_rewrite(LitA,top_pos,Acond,make(Equal,x,iter));
|
||||
|
@ -1014,6 +1052,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
coeff = argpos ? make_int(rational(-1)) : make_int(rational(1));
|
||||
break;
|
||||
case Not:
|
||||
coeff = make_int(rational(-1));
|
||||
case Plus:
|
||||
break;
|
||||
case Times:
|
||||
|
@ -2568,12 +2607,17 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
break;
|
||||
default: { // mixed equality
|
||||
if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed){
|
||||
// std::cerr << "WARNING: mixed term in leq2eq\n";
|
||||
std::vector<ast> lits;
|
||||
lits.push_back(con);
|
||||
lits.push_back(make(Not,xleqy));
|
||||
lits.push_back(make(Not,yleqx));
|
||||
return make_axiom(lits);
|
||||
if(y == make_int(rational(0)) && op(x) == Plus && num_args(x) == 2){
|
||||
// std::cerr << "WARNING: untested case in leq2eq\n";
|
||||
}
|
||||
else {
|
||||
// std::cerr << "WARNING: mixed term in leq2eq\n";
|
||||
std::vector<ast> lits;
|
||||
lits.push_back(con);
|
||||
lits.push_back(make(Not,xleqy));
|
||||
lits.push_back(make(Not,yleqx));
|
||||
return make_axiom(lits);
|
||||
}
|
||||
}
|
||||
std::vector<ast> conjs; conjs.resize(3);
|
||||
conjs[0] = mk_not(con);
|
||||
|
@ -2655,8 +2699,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
};
|
||||
|
||||
std::vector<LocVar> localization_vars; // localization vars in order of creation
|
||||
hash_map<ast,ast> localization_map; // maps terms to their localization vars
|
||||
hash_map<ast,ast> localization_pf_map; // maps terms to proofs of their localizations
|
||||
|
||||
struct locmaps {
|
||||
hash_map<ast,ast> localization_map; // maps terms to their localization vars
|
||||
hash_map<ast,ast> localization_pf_map; // maps terms to proofs of their localizations
|
||||
};
|
||||
|
||||
hash_map<prover::range,locmaps> localization_maps_per_range;
|
||||
|
||||
/* "localize" a term e to a given frame range, creating new symbols to
|
||||
represent non-local subterms. This returns the localized version e_l,
|
||||
|
@ -2677,7 +2726,24 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
return make(Equal,x,y);
|
||||
}
|
||||
|
||||
bool range_is_global(const prover::range &r){
|
||||
if(pv->range_contained(r,rng))
|
||||
return false;
|
||||
if(!pv->ranges_intersect(r,rng))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
ast localize_term(ast e, const prover::range &rng, ast &pf){
|
||||
|
||||
// we need to memoize this function separately for A, B and global
|
||||
prover::range map_range = rng;
|
||||
if(range_is_global(map_range))
|
||||
map_range = pv->range_full();
|
||||
locmaps &maps = localization_maps_per_range[map_range];
|
||||
hash_map<ast,ast> &localization_map = maps.localization_map;
|
||||
hash_map<ast,ast> &localization_pf_map = maps.localization_pf_map;
|
||||
|
||||
ast orig_e = e;
|
||||
pf = make_refl(e); // proof that e = e
|
||||
|
||||
|
@ -2764,6 +2830,21 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
ast bar = make_assumption(frame,foo);
|
||||
pf = make_transitivity(new_var,e,orig_e,bar,pf);
|
||||
localization_pf_map[orig_e] = pf;
|
||||
|
||||
// HACK: try to bias this term in the future
|
||||
if(!pv->range_is_full(rng)){
|
||||
prover::range rf = pv->range_full();
|
||||
locmaps &fmaps = localization_maps_per_range[rf];
|
||||
hash_map<ast,ast> &flocalization_map = fmaps.localization_map;
|
||||
hash_map<ast,ast> &flocalization_pf_map = fmaps.localization_pf_map;
|
||||
// if(flocalization_map.find(orig_e) == flocalization_map.end())
|
||||
{
|
||||
flocalization_map[orig_e] = new_var;
|
||||
flocalization_pf_map[orig_e] = pf;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
return new_var;
|
||||
}
|
||||
|
||||
|
|
|
@ -23,6 +23,7 @@ Revision History:
|
|||
|
||||
#include <vector>
|
||||
#include <limits.h>
|
||||
#include "iz3hash.h"
|
||||
|
||||
class scopes {
|
||||
|
||||
|
@ -63,6 +64,11 @@ class scopes {
|
|||
return rng.hi < rng.lo;
|
||||
}
|
||||
|
||||
/** is this range full? */
|
||||
bool range_is_full(const range &rng){
|
||||
return rng.lo == SHRT_MIN && rng.hi == SHRT_MAX;
|
||||
}
|
||||
|
||||
/** return an empty range */
|
||||
range range_empty(){
|
||||
range res;
|
||||
|
@ -194,4 +200,23 @@ class scopes {
|
|||
|
||||
|
||||
};
|
||||
|
||||
// let us hash on ranges
|
||||
|
||||
#ifndef FULL_TREE
|
||||
namespace hash_space {
|
||||
template <>
|
||||
class hash<scopes::range> {
|
||||
public:
|
||||
size_t operator()(const scopes::range &p) const {
|
||||
return (size_t)p.lo + (size_t)p.hi;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
inline bool operator==(const scopes::range &x, const scopes::range &y){
|
||||
return x.lo == y.lo && x.hi == y.hi;
|
||||
}
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
|
|
@ -1058,36 +1058,66 @@ public:
|
|||
}
|
||||
|
||||
|
||||
rational get_first_coefficient(const ast &t, ast &v){
|
||||
if(op(t) == Plus){
|
||||
unsigned best_id = UINT_MAX;
|
||||
rational best_coeff(0);
|
||||
int nargs = num_args(t);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
if(op(arg(t,i)) != Numeral){
|
||||
ast lv = get_linear_var(arg(t,i));
|
||||
unsigned id = ast_id(lv);
|
||||
if(id < best_id) {
|
||||
v = lv;
|
||||
best_id = id;
|
||||
best_coeff = get_coeff(arg(t,i));
|
||||
}
|
||||
}
|
||||
return best_coeff;
|
||||
}
|
||||
else
|
||||
if(op(t) != Numeral)
|
||||
return(get_coeff(t));
|
||||
return rational(0);
|
||||
}
|
||||
|
||||
ast divide_inequalities(const ast &x, const ast&y){
|
||||
std::vector<rational> xcoeffs,ycoeffs;
|
||||
get_linear_coefficients(arg(x,1),xcoeffs);
|
||||
get_linear_coefficients(arg(y,1),ycoeffs);
|
||||
if(xcoeffs.size() != ycoeffs.size() || xcoeffs.size() == 0)
|
||||
ast xvar, yvar;
|
||||
rational xcoeff = get_first_coefficient(arg(x,0),xvar);
|
||||
rational ycoeff = get_first_coefficient(arg(y,0),yvar);
|
||||
if(xcoeff == rational(0) || ycoeff == rational(0) || xvar != yvar)
|
||||
throw "bad assign-bounds lemma";
|
||||
rational ratio = xcoeff/ycoeff;
|
||||
if(denominator(ratio) != rational(1))
|
||||
throw "bad assign-bounds lemma";
|
||||
rational ratio = xcoeffs[0]/ycoeffs[0];
|
||||
return make_int(ratio); // better be integer!
|
||||
}
|
||||
|
||||
ast AssignBounds2Farkas(const ast &proof, const ast &con){
|
||||
std::vector<ast> farkas_coeffs;
|
||||
get_assign_bounds_coeffs(proof,farkas_coeffs);
|
||||
std::vector<ast> lits;
|
||||
int nargs = num_args(con);
|
||||
if(nargs != (int)(farkas_coeffs.size()))
|
||||
throw "bad assign-bounds theory lemma";
|
||||
#if 0
|
||||
for(int i = 1; i < nargs; i++)
|
||||
lits.push_back(mk_not(arg(con,i)));
|
||||
ast sum = sum_inequalities(farkas_coeffs,lits);
|
||||
ast conseq = rhs_normalize_inequality(arg(con,0));
|
||||
ast d = divide_inequalities(sum,conseq);
|
||||
std::vector<ast> my_coeffs;
|
||||
my_coeffs.push_back(d);
|
||||
for(unsigned i = 0; i < farkas_coeffs.size(); i++)
|
||||
my_coeffs.push_back(farkas_coeffs[i]);
|
||||
if(farkas_coeffs[0] != make_int(rational(1)))
|
||||
farkas_coeffs[0] = make_int(rational(1));
|
||||
#else
|
||||
std::vector<ast> my_coeffs;
|
||||
std::vector<ast> lits, lit_coeffs;
|
||||
for(int i = 1; i < nargs; i++){
|
||||
lits.push_back(mk_not(arg(con,i)));
|
||||
lit_coeffs.push_back(farkas_coeffs[i]);
|
||||
}
|
||||
ast sum = normalize_inequality(sum_inequalities(lit_coeffs,lits));
|
||||
ast conseq = normalize_inequality(arg(con,0));
|
||||
ast d = divide_inequalities(sum,conseq);
|
||||
#if 0
|
||||
if(d != farkas_coeffs[0])
|
||||
std::cout << "wow!\n";
|
||||
#endif
|
||||
farkas_coeffs[0] = d;
|
||||
#endif
|
||||
std::vector<ast> my_coeffs;
|
||||
std::vector<ast> my_cons;
|
||||
for(int i = 1; i < nargs; i++){
|
||||
my_cons.push_back(mk_not(arg(con,i)));
|
||||
|
@ -1107,10 +1137,27 @@ public:
|
|||
ast AssignBoundsRule2Farkas(const ast &proof, const ast &con, std::vector<Iproof::node> prems){
|
||||
std::vector<ast> farkas_coeffs;
|
||||
get_assign_bounds_rule_coeffs(proof,farkas_coeffs);
|
||||
std::vector<ast> lits;
|
||||
int nargs = num_prems(proof)+1;
|
||||
if(nargs != (int)(farkas_coeffs.size()))
|
||||
throw "bad assign-bounds theory lemma";
|
||||
#if 0
|
||||
if(farkas_coeffs[0] != make_int(rational(1)))
|
||||
farkas_coeffs[0] = make_int(rational(1));
|
||||
#else
|
||||
std::vector<ast> lits, lit_coeffs;
|
||||
for(int i = 1; i < nargs; i++){
|
||||
lits.push_back(conc(prem(proof,i-1)));
|
||||
lit_coeffs.push_back(farkas_coeffs[i]);
|
||||
}
|
||||
ast sum = normalize_inequality(sum_inequalities(lit_coeffs,lits));
|
||||
ast conseq = normalize_inequality(con);
|
||||
ast d = divide_inequalities(sum,conseq);
|
||||
#if 0
|
||||
if(d != farkas_coeffs[0])
|
||||
std::cout << "wow!\n";
|
||||
#endif
|
||||
farkas_coeffs[0] = d;
|
||||
#endif
|
||||
std::vector<ast> my_coeffs;
|
||||
std::vector<ast> my_cons;
|
||||
for(int i = 1; i < nargs; i++){
|
||||
|
@ -1278,6 +1325,17 @@ public:
|
|||
return make(Plus,args);
|
||||
}
|
||||
|
||||
void get_sum_as_vector(const ast &t, std::vector<rational> &coeffs, std::vector<ast> &vars){
|
||||
if(!(op(t) == Plus)){
|
||||
coeffs.push_back(get_coeff(t));
|
||||
vars.push_back(get_linear_var(t));
|
||||
}
|
||||
else {
|
||||
int nargs = num_args(t);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
get_sum_as_vector(arg(t,i),coeffs,vars);
|
||||
}
|
||||
}
|
||||
|
||||
ast replace_summands_with_fresh_vars(const ast &t, hash_map<ast,ast> &map){
|
||||
if(op(t) == Plus){
|
||||
|
@ -1294,6 +1352,99 @@ public:
|
|||
return map[t];
|
||||
}
|
||||
|
||||
rational lcd(const std::vector<rational> &rats){
|
||||
rational res = rational(1);
|
||||
for(unsigned i = 0; i < rats.size(); i++){
|
||||
res = lcm(res,denominator(rats[i]));
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
Iproof::node reconstruct_farkas_with_dual(const std::vector<ast> &prems, const std::vector<Iproof::node> &pfs, const ast &con){
|
||||
int nprems = prems.size();
|
||||
std::vector<ast> npcons(nprems);
|
||||
hash_map<ast,ast> pain_map; // not needed
|
||||
for(int i = 0; i < nprems; i++){
|
||||
npcons[i] = painfully_normalize_ineq(conc(prems[i]),pain_map);
|
||||
if(op(npcons[i]) == Lt){
|
||||
ast constval = z3_simplify(make(Sub,arg(npcons[i],1),make_int(rational(1))));
|
||||
npcons[i] = make(Leq,arg(npcons[i],0),constval);
|
||||
}
|
||||
}
|
||||
ast ncon = painfully_normalize_ineq(mk_not(con),pain_map);
|
||||
npcons.push_back(ncon);
|
||||
|
||||
hash_map<ast,ast> dual_map;
|
||||
std::vector<ast> cvec, vars_seen;
|
||||
ast rhs = make_real(rational(0));
|
||||
for(unsigned i = 0; i < npcons.size(); i++){
|
||||
ast c= mk_fresh_constant("@c",real_type());
|
||||
cvec.push_back(c);
|
||||
ast lhs = arg(npcons[i],0);
|
||||
std::vector<rational> coeffs;
|
||||
std::vector<ast> vars;
|
||||
get_sum_as_vector(lhs,coeffs,vars);
|
||||
for(unsigned j = 0; j < coeffs.size(); j++){
|
||||
rational coeff = coeffs[j];
|
||||
ast var = vars[j];
|
||||
if(dual_map.find(var) == dual_map.end()){
|
||||
dual_map[var] = make_real(rational(0));
|
||||
vars_seen.push_back(var);
|
||||
}
|
||||
ast foo = make(Plus,dual_map[var],make(Times,make_real(coeff),c));
|
||||
dual_map[var] = foo;
|
||||
}
|
||||
rhs = make(Plus,rhs,make(Times,c,arg(npcons[i],1)));
|
||||
}
|
||||
std::vector<ast> cnstrs;
|
||||
for(unsigned i = 0; i < vars_seen.size(); i++)
|
||||
cnstrs.push_back(make(Equal,dual_map[vars_seen[i]],make_real(rational(0))));
|
||||
cnstrs.push_back(make(Leq,rhs,make_real(rational(0))));
|
||||
for(unsigned i = 0; i < cvec.size() - 1; i++)
|
||||
cnstrs.push_back(make(Geq,cvec[i],make_real(rational(0))));
|
||||
cnstrs.push_back(make(Equal,cvec.back(),make_real(rational(1))));
|
||||
ast new_proof;
|
||||
|
||||
// greedily reduce the core
|
||||
for(unsigned i = 0; i < cvec.size() - 1; i++){
|
||||
std::vector<ast> dummy;
|
||||
cnstrs.push_back(make(Equal,cvec[i],make_real(rational(0))));
|
||||
if(!is_sat(cnstrs,new_proof,dummy))
|
||||
cnstrs.pop_back();
|
||||
}
|
||||
|
||||
std::vector<ast> vals = cvec;
|
||||
if(!is_sat(cnstrs,new_proof,vals))
|
||||
throw "Proof error!";
|
||||
std::vector<rational> rat_farkas_coeffs;
|
||||
for(unsigned i = 0; i < cvec.size(); i++){
|
||||
ast bar = vals[i];
|
||||
rational r;
|
||||
if(is_numeral(bar,r))
|
||||
rat_farkas_coeffs.push_back(r);
|
||||
else
|
||||
throw "Proof error!";
|
||||
}
|
||||
rational the_lcd = lcd(rat_farkas_coeffs);
|
||||
std::vector<ast> farkas_coeffs;
|
||||
std::vector<Iproof::node> my_prems;
|
||||
std::vector<ast> my_pcons;
|
||||
for(unsigned i = 0; i < prems.size(); i++){
|
||||
ast fc = make_int(rat_farkas_coeffs[i] * the_lcd);
|
||||
if(!(fc == make_int(rational(0)))){
|
||||
farkas_coeffs.push_back(fc);
|
||||
my_prems.push_back(pfs[i]);
|
||||
my_pcons.push_back(conc(prems[i]));
|
||||
}
|
||||
}
|
||||
farkas_coeffs.push_back(make_int(the_lcd));
|
||||
my_prems.push_back(iproof->make_hypothesis(mk_not(con)));
|
||||
my_pcons.push_back(mk_not(con));
|
||||
|
||||
Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
|
||||
return res;
|
||||
}
|
||||
|
||||
ast painfully_normalize_ineq(const ast &ineq, hash_map<ast,ast> &map){
|
||||
ast res = normalize_inequality(ineq);
|
||||
ast lhs = arg(res,0);
|
||||
|
@ -1318,7 +1469,8 @@ public:
|
|||
npcons.push_back(ncon);
|
||||
// ast assumps = make(And,pcons);
|
||||
ast new_proof;
|
||||
if(is_sat(npcons,new_proof))
|
||||
std::vector<ast> dummy;
|
||||
if(is_sat(npcons,new_proof,dummy))
|
||||
throw "Proof error!";
|
||||
pfrule dk = pr(new_proof);
|
||||
int nnp = num_prems(new_proof);
|
||||
|
@ -1334,7 +1486,7 @@ public:
|
|||
farkas_coeffs.push_back(make_int(rational(1)));
|
||||
}
|
||||
else
|
||||
throw "cannot reconstruct farkas proof";
|
||||
return reconstruct_farkas_with_dual(prems,pfs,con);
|
||||
|
||||
for(int i = 0; i < nnp; i++){
|
||||
ast p = conc(prem(new_proof,i));
|
||||
|
@ -1348,7 +1500,7 @@ public:
|
|||
my_pcons.push_back(mk_not(con));
|
||||
}
|
||||
else
|
||||
throw "cannot reconstruct farkas proof";
|
||||
return reconstruct_farkas_with_dual(prems,pfs,con);
|
||||
}
|
||||
Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
|
||||
return res;
|
||||
|
@ -1378,7 +1530,8 @@ public:
|
|||
npcons.push_back(ncon);
|
||||
// ast assumps = make(And,pcons);
|
||||
ast new_proof;
|
||||
if(is_sat(npcons,new_proof))
|
||||
std::vector<ast> dummy;
|
||||
if(is_sat(npcons,new_proof,dummy))
|
||||
throw "Proof error!";
|
||||
pfrule dk = pr(new_proof);
|
||||
int nnp = num_prems(new_proof);
|
||||
|
@ -1408,7 +1561,7 @@ public:
|
|||
my_pcons.push_back(mk_not(con));
|
||||
}
|
||||
else
|
||||
throw "cannot reconstruct farkas proof";
|
||||
return painfully_reconstruct_farkas(prems,pfs,con);
|
||||
}
|
||||
Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
|
||||
return res;
|
||||
|
@ -1433,6 +1586,12 @@ public:
|
|||
return res;
|
||||
}
|
||||
|
||||
ast ArithMysteryRule(const ast &con, const std::vector<ast> &prems, const std::vector<Iproof::node> &args){
|
||||
// Hope for the best!
|
||||
Iproof::node guess = reconstruct_farkas(prems,args,con);
|
||||
return guess;
|
||||
}
|
||||
|
||||
struct CannotCombineEqPropagate {};
|
||||
|
||||
void CombineEqPropagateRec(const ast &proof, std::vector<ast> &prems, std::vector<Iproof::node> &args, ast &eqprem){
|
||||
|
@ -1552,6 +1711,13 @@ public:
|
|||
if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or)
|
||||
std::cout << "foo!\n";
|
||||
|
||||
// no idea why this shows up
|
||||
if(dk == PR_MODUS_PONENS_OEQ)
|
||||
if(conc(prem(proof,0)) == con){
|
||||
res = translate_main(prem(proof,0),expect_clause);
|
||||
return res;
|
||||
}
|
||||
|
||||
#if 0
|
||||
if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
|
||||
Iproof::node clause = translate_main(prem(proof,0),true);
|
||||
|
@ -1737,6 +1903,14 @@ public:
|
|||
res = EqPropagate(con,prems,args);
|
||||
break;
|
||||
}
|
||||
case ArithMysteryKind: {
|
||||
// Z3 hasn't told us what kind of lemma this is -- maybe we can guess
|
||||
std::vector<ast> prems(nprems);
|
||||
for(unsigned i = 0; i < nprems; i++)
|
||||
prems[i] = prem(proof,i);
|
||||
res = ArithMysteryRule(con,prems,args);
|
||||
break;
|
||||
}
|
||||
default:
|
||||
throw unsupported();
|
||||
}
|
||||
|
|
|
@ -530,7 +530,7 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C,
|
|||
upm.mul(A_lifted.size(), A_lifted.c_ptr(), B_lifted.size(), B_lifted.c_ptr(), test1);
|
||||
upm.sub(C.size(), C.c_ptr(), test1.size(), test1.c_ptr(), test1);
|
||||
to_zp_manager(br_upm, test1);
|
||||
if (!test1.size() == 0) {
|
||||
if (test1.size() != 0) {
|
||||
TRACE("polynomial::factorization::bughunt",
|
||||
tout << "sage: R.<x> = ZZ['x']" << endl;
|
||||
tout << "sage: A = "; upm.display(tout, A); tout << endl;
|
||||
|
|
|
@ -133,7 +133,9 @@ bool model::eval(expr * e, expr_ref & result, bool model_completion) {
|
|||
ev(e, result);
|
||||
return true;
|
||||
}
|
||||
catch (model_evaluator_exception &) {
|
||||
catch (model_evaluator_exception & ex) {
|
||||
(void)ex;
|
||||
TRACE("model_evaluator", tout << ex.msg() << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -278,6 +278,12 @@ namespace datalog {
|
|||
|
||||
void register_variable(func_decl* var);
|
||||
|
||||
/*
|
||||
Replace constants that have been registered as
|
||||
variables by de-Bruijn indices and corresponding
|
||||
universal (if is_forall is true) or existential
|
||||
quantifier.
|
||||
*/
|
||||
expr_ref bind_variables(expr* fml, bool is_forall);
|
||||
|
||||
/**
|
||||
|
|
|
@ -77,6 +77,7 @@ def_module_params('fixedpoint',
|
|||
('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'),
|
||||
('batch_expand', BOOL, False, 'DUALITY: use batch expansion'),
|
||||
('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
|
||||
('conjecture_file', STRING, '', 'DUALITY: save conjectures to file'),
|
||||
))
|
||||
|
||||
|
||||
|
|
|
@ -35,6 +35,7 @@ Revision History:
|
|||
#include "model_smt2_pp.h"
|
||||
#include "model_v2_pp.h"
|
||||
#include "fixedpoint_params.hpp"
|
||||
#include "used_vars.h"
|
||||
|
||||
// template class symbol_table<family_id>;
|
||||
|
||||
|
@ -164,6 +165,20 @@ lbool dl_interface::query(::expr * query) {
|
|||
clauses.push_back(e);
|
||||
}
|
||||
|
||||
std::vector<sort> b_sorts;
|
||||
std::vector<symbol> b_names;
|
||||
used_vars uv;
|
||||
uv.process(query);
|
||||
unsigned nuv = uv.get_max_found_var_idx_plus_1();
|
||||
for(int i = nuv-1; i >= 0; i--){ // var indices are backward
|
||||
::sort * s = uv.get(i);
|
||||
if(!s)
|
||||
s = _d->ctx.m().mk_bool_sort(); // missing var, whatever
|
||||
b_sorts.push_back(sort(_d->ctx,s));
|
||||
b_names.push_back(symbol(_d->ctx,::symbol(i))); // names?
|
||||
}
|
||||
|
||||
#if 0
|
||||
// turn the query into a clause
|
||||
expr q(_d->ctx,m_ctx.bind_variables(query,false));
|
||||
|
||||
|
@ -177,6 +192,9 @@ lbool dl_interface::query(::expr * query) {
|
|||
}
|
||||
q = q.arg(0);
|
||||
}
|
||||
#else
|
||||
expr q(_d->ctx,query);
|
||||
#endif
|
||||
|
||||
expr qc = implies(q,_d->ctx.bool_val(false));
|
||||
qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc);
|
||||
|
@ -211,6 +229,7 @@ lbool dl_interface::query(::expr * query) {
|
|||
rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0");
|
||||
rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
|
||||
rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
|
||||
rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file());
|
||||
unsigned rb = m_ctx.get_params().recursion_bound();
|
||||
if(rb != UINT_MAX){
|
||||
std::ostringstream os; os << rb;
|
||||
|
@ -350,7 +369,9 @@ void dl_interface::display_certificate_non_const(std::ostream& out) {
|
|||
if(_d->status == StatusModel){
|
||||
ast_manager &m = m_ctx.get_manager();
|
||||
model_ref md = get_model();
|
||||
out << "(fixedpoint \n";
|
||||
model_smt2_pp(out, m, *md.get(), 0);
|
||||
out << ")\n";
|
||||
}
|
||||
else if(_d->status == StatusRefutation){
|
||||
out << "(derivation\n";
|
||||
|
|
|
@ -200,7 +200,22 @@ namespace datalog {
|
|||
func_decl_set::iterator it = pruned_preds.begin();
|
||||
extension_model_converter* mc0 = alloc(extension_model_converter, m);
|
||||
for (; it != end; ++it) {
|
||||
mc0->insert(*it, m.mk_true());
|
||||
const rule_vector& rules = source.get_predicate_rules(*it);
|
||||
expr_ref_vector fmls(m);
|
||||
for (unsigned i = 0; i < rules.size(); ++i) {
|
||||
app* head = rules[i]->get_head();
|
||||
expr_ref_vector conj(m);
|
||||
for (unsigned j = 0; j < head->get_num_args(); ++j) {
|
||||
expr* arg = head->get_arg(j);
|
||||
if (!is_var(arg)) {
|
||||
conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg));
|
||||
}
|
||||
}
|
||||
fmls.push_back(m.mk_and(conj.size(), conj.c_ptr()));
|
||||
}
|
||||
expr_ref fml(m);
|
||||
fml = m.mk_or(fmls.size(), fmls.c_ptr());
|
||||
mc0->insert(*it, fml);
|
||||
}
|
||||
m_context.add_model_converter(mc0);
|
||||
}
|
||||
|
|
|
@ -226,7 +226,7 @@ namespace qe {
|
|||
return alloc(sat_tactic, m);
|
||||
}
|
||||
|
||||
~sat_tactic() {
|
||||
virtual ~sat_tactic() {
|
||||
for (unsigned i = 0; i < m_solvers.size(); ++i) {
|
||||
dealloc(m_solvers[i]);
|
||||
}
|
||||
|
|
|
@ -23,6 +23,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
|
|||
smt_params_helper p(_p);
|
||||
m_macro_finder = p.macro_finder();
|
||||
m_pull_nested_quantifiers = p.pull_nested_quantifiers();
|
||||
m_refine_inj_axiom = p.refine_inj_axioms();
|
||||
}
|
||||
|
||||
void preprocessor_params::updt_params(params_ref const & p) {
|
||||
|
|
|
@ -14,6 +14,7 @@ def_module_params(module_name='smt',
|
|||
('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
|
||||
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
|
||||
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
|
||||
('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
|
||||
('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
|
||||
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
|
||||
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
|
||||
|
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#include"proto_model.h"
|
||||
#include"ast_pp.h"
|
||||
#include"ast_ll_pp.h"
|
||||
#include"expr_functors.h"
|
||||
|
||||
datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
|
||||
struct_factory(m, m.mk_family_id("datatype"), md),
|
||||
|
@ -47,8 +48,10 @@ expr * datatype_factory::get_some_value(sort * s) {
|
|||
*/
|
||||
expr * datatype_factory::get_last_fresh_value(sort * s) {
|
||||
expr * val = 0;
|
||||
if (m_last_fresh_value.find(s, val))
|
||||
if (m_last_fresh_value.find(s, val)) {
|
||||
TRACE("datatype_factory", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
|
||||
return val;
|
||||
}
|
||||
value_set * set = get_value_set(s);
|
||||
if (set->empty())
|
||||
val = get_some_value(s);
|
||||
|
@ -59,6 +62,17 @@ expr * datatype_factory::get_last_fresh_value(sort * s) {
|
|||
return val;
|
||||
}
|
||||
|
||||
bool datatype_factory::is_subterm_of_last_value(app* e) {
|
||||
expr* last;
|
||||
if (!m_last_fresh_value.find(m_manager.get_sort(e), last)) {
|
||||
return false;
|
||||
}
|
||||
contains_app contains(m_manager, e);
|
||||
bool result = contains(last);
|
||||
TRACE("datatype_factory", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";);
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create an almost fresh value. If s is recursive, then the result is not 0.
|
||||
It also updates m_last_fresh_value
|
||||
|
@ -105,11 +119,18 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
|
|||
}
|
||||
}
|
||||
if (recursive || found_fresh_arg) {
|
||||
expr * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
|
||||
app * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
|
||||
SASSERT(!found_fresh_arg || !set->contains(new_value));
|
||||
register_value(new_value);
|
||||
if (m_util.is_recursive(s))
|
||||
m_last_fresh_value.insert(s, new_value);
|
||||
if (m_util.is_recursive(s)) {
|
||||
if (is_subterm_of_last_value(new_value)) {
|
||||
new_value = static_cast<app*>(m_last_fresh_value.find(s));
|
||||
}
|
||||
else {
|
||||
m_last_fresh_value.insert(s, new_value);
|
||||
}
|
||||
}
|
||||
TRACE("datatype_factory", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";);
|
||||
return new_value;
|
||||
}
|
||||
}
|
||||
|
@ -181,12 +202,20 @@ expr * datatype_factory::get_fresh_value(sort * s) {
|
|||
expr_ref_vector args(m_manager);
|
||||
bool found_sibling = false;
|
||||
unsigned num = constructor->get_arity();
|
||||
TRACE("datatype_factory", tout << "checking constructor: " << constructor->get_name() << "\n";);
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
sort * s_arg = constructor->get_domain(i);
|
||||
TRACE("datatype_factory", tout << mk_pp(s, m_manager) << " "
|
||||
<< mk_pp(s_arg, m_manager) << " are_siblings "
|
||||
<< m_util.are_siblings(s, s_arg) << " is_datatype "
|
||||
<< m_util.is_datatype(s_arg) << " found_sibling "
|
||||
<< found_sibling << "\n";);
|
||||
if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
|
||||
found_sibling = true;
|
||||
expr * maybe_new_arg = get_almost_fresh_value(s_arg);
|
||||
if (!maybe_new_arg) {
|
||||
TRACE("datatype_factory",
|
||||
tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
|
||||
maybe_new_arg = m_model.get_some_value(s_arg);
|
||||
found_sibling = false;
|
||||
}
|
||||
|
|
|
@ -29,6 +29,8 @@ class datatype_factory : public struct_factory {
|
|||
expr * get_last_fresh_value(sort * s);
|
||||
expr * get_almost_fresh_value(sort * s);
|
||||
|
||||
bool is_subterm_of_last_value(app* e);
|
||||
|
||||
public:
|
||||
datatype_factory(ast_manager & m, proto_model & md);
|
||||
virtual ~datatype_factory() {}
|
||||
|
|
|
@ -247,6 +247,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
|
|||
new_t = mk_some_interp_for(f);
|
||||
}
|
||||
else {
|
||||
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
|
||||
is_ok = false;
|
||||
}
|
||||
}
|
||||
|
@ -294,6 +295,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
|
|||
// f is an uninterpreted function, there is no need to use m_simplifier.mk_app
|
||||
new_t = m_manager.mk_app(f, num_args, args.c_ptr());
|
||||
trail.push_back(new_t);
|
||||
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
|
||||
is_ok = false;
|
||||
}
|
||||
}
|
||||
|
@ -326,6 +328,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
|
|||
todo.pop_back();
|
||||
break;
|
||||
case AST_QUANTIFIER:
|
||||
TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";);
|
||||
is_ok = false; // evaluator does not handle quantifiers.
|
||||
SASSERT(a != 0);
|
||||
eval_cache.insert(a, a);
|
||||
|
|
|
@ -396,7 +396,7 @@ namespace smt {
|
|||
|
||||
// Support for evaluating expressions in the current model.
|
||||
proto_model * m_model;
|
||||
obj_map<expr, expr *> m_eval_cache;
|
||||
obj_map<expr, expr *> m_eval_cache[2];
|
||||
expr_ref_vector m_eval_cache_range;
|
||||
|
||||
ptr_vector<node> m_root_nodes;
|
||||
|
@ -409,7 +409,8 @@ namespace smt {
|
|||
}
|
||||
|
||||
void reset_eval_cache() {
|
||||
m_eval_cache.reset();
|
||||
m_eval_cache[0].reset();
|
||||
m_eval_cache[1].reset();
|
||||
m_eval_cache_range.reset();
|
||||
}
|
||||
|
||||
|
@ -468,6 +469,7 @@ namespace smt {
|
|||
|
||||
~auf_solver() {
|
||||
flush_nodes();
|
||||
reset_eval_cache();
|
||||
}
|
||||
|
||||
void set_context(context * ctx) {
|
||||
|
@ -547,7 +549,7 @@ namespace smt {
|
|||
for (obj_map<expr, unsigned>::iterator it = elems.begin(); it != elems.end(); it++) {
|
||||
expr * n = it->m_key;
|
||||
expr * n_val = eval(n, true);
|
||||
if (!m_manager.is_value(n_val))
|
||||
if (!n_val || !m_manager.is_value(n_val))
|
||||
to_delete.push_back(n);
|
||||
}
|
||||
for (ptr_vector<expr>::iterator it = to_delete.begin(); it != to_delete.end(); it++) {
|
||||
|
@ -569,16 +571,19 @@ namespace smt {
|
|||
|
||||
virtual expr * eval(expr * n, bool model_completion) {
|
||||
expr * r = 0;
|
||||
if (m_eval_cache.find(n, r)) {
|
||||
if (m_eval_cache[model_completion].find(n, r)) {
|
||||
return r;
|
||||
}
|
||||
expr_ref tmp(m_manager);
|
||||
if (!m_model->eval(n, tmp, model_completion))
|
||||
if (!m_model->eval(n, tmp, model_completion)) {
|
||||
r = 0;
|
||||
else
|
||||
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n-----> null\n";);
|
||||
}
|
||||
else {
|
||||
r = tmp;
|
||||
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
|
||||
m_eval_cache.insert(n, r);
|
||||
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
|
||||
}
|
||||
m_eval_cache[model_completion].insert(n, r);
|
||||
m_eval_cache_range.push_back(r);
|
||||
return r;
|
||||
}
|
||||
|
|
|
@ -102,6 +102,7 @@ namespace smt {
|
|||
if (th && th->build_models()) {
|
||||
if (r->get_th_var(th->get_id()) != null_theory_var) {
|
||||
proc = th->mk_value(r, *this);
|
||||
SASSERT(proc);
|
||||
}
|
||||
else {
|
||||
TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
|
||||
|
@ -110,6 +111,7 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
proc = mk_model_value(r);
|
||||
SASSERT(proc);
|
||||
}
|
||||
}
|
||||
SASSERT(proc);
|
||||
|
|
|
@ -193,7 +193,7 @@ namespace smt {
|
|||
return true;
|
||||
}
|
||||
|
||||
if (!r.get_base_var() == x && x > y) {
|
||||
if (r.get_base_var() != x && x > y) {
|
||||
std::swap(x, y);
|
||||
k.neg();
|
||||
}
|
||||
|
|
|
@ -162,7 +162,7 @@ namespace smt {
|
|||
m.register_factory(alloc(dl_factory, m_util, m.get_model()));
|
||||
}
|
||||
|
||||
virtual smt::model_value_proc * mk_value(smt::enode * n) {
|
||||
virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) {
|
||||
return alloc(dl_value_proc, *this, n);
|
||||
}
|
||||
|
||||
|
@ -201,9 +201,8 @@ namespace smt {
|
|||
if(!m_reps.find(s, r) || !m_vals.find(s,v)) {
|
||||
SASSERT(!m_reps.contains(s));
|
||||
sort* bv = b().mk_sort(64);
|
||||
// TBD: filter these from model.
|
||||
r = m().mk_fresh_func_decl("rep",1, &s,bv);
|
||||
v = m().mk_fresh_func_decl("val",1, &bv,s);
|
||||
r = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_REP, 0, 0, 1, &s, bv);
|
||||
v = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_ABS, 0, 0, 1, &bv, s);
|
||||
m_reps.insert(s, r);
|
||||
m_vals.insert(s, v);
|
||||
add_trail(r);
|
||||
|
|
|
@ -70,7 +70,9 @@ struct scoped_timer::imp {
|
|||
pthread_t m_thread_id;
|
||||
pthread_attr_t m_attributes;
|
||||
unsigned m_interval;
|
||||
pthread_mutex_t m_mutex;
|
||||
pthread_cond_t m_condition_var;
|
||||
struct timespec m_end_time;
|
||||
#elif defined(_LINUX_) || defined(_FREEBSD_)
|
||||
// Linux & FreeBSD
|
||||
timer_t m_timerid;
|
||||
|
@ -93,35 +95,15 @@ struct scoped_timer::imp {
|
|||
static void * thread_func(void * arg) {
|
||||
scoped_timer::imp * st = static_cast<scoped_timer::imp*>(arg);
|
||||
|
||||
pthread_mutex_t mutex;
|
||||
clock_serv_t host_clock;
|
||||
struct timespec abstime;
|
||||
mach_timespec_t now;
|
||||
unsigned long long nano = static_cast<unsigned long long>(st->m_interval) * 1000000ull;
|
||||
pthread_mutex_lock(&st->m_mutex);
|
||||
|
||||
host_get_clock_service(mach_host_self(), CALENDAR_CLOCK, &host_clock);
|
||||
|
||||
if (pthread_mutex_init(&mutex, NULL) != 0)
|
||||
throw default_exception("failed to initialize timer mutex");
|
||||
if (pthread_cond_init(&st->m_condition_var, NULL) != 0)
|
||||
throw default_exception("failed to initialize timer condition variable");
|
||||
|
||||
abstime.tv_sec = nano / 1000000000ull;
|
||||
abstime.tv_nsec = nano % 1000000000ull;
|
||||
|
||||
pthread_mutex_lock(&mutex);
|
||||
clock_get_time(host_clock, &now);
|
||||
ADD_MACH_TIMESPEC(&abstime, &now);
|
||||
int e = pthread_cond_timedwait(&st->m_condition_var, &mutex, &abstime);
|
||||
int e = pthread_cond_timedwait(&st->m_condition_var, &st->m_mutex, &st->m_end_time);
|
||||
if (e != 0 && e != ETIMEDOUT)
|
||||
throw default_exception("failed to start timed wait");
|
||||
st->m_eh->operator()();
|
||||
pthread_mutex_unlock(&mutex);
|
||||
|
||||
if (pthread_mutex_destroy(&mutex) != 0)
|
||||
throw default_exception("failed to destroy pthread mutex");
|
||||
if (pthread_cond_destroy(&st->m_condition_var) != 0)
|
||||
throw default_exception("failed to destroy pthread condition variable");
|
||||
pthread_mutex_unlock(&st->m_mutex);
|
||||
|
||||
return st;
|
||||
}
|
||||
#elif defined(_LINUX_) || defined(_FREEBSD_)
|
||||
|
@ -150,6 +132,22 @@ struct scoped_timer::imp {
|
|||
m_interval = ms;
|
||||
if (pthread_attr_init(&m_attributes) != 0)
|
||||
throw default_exception("failed to initialize timer thread attributes");
|
||||
if (pthread_cond_init(&m_condition_var, NULL) != 0)
|
||||
throw default_exception("failed to initialize timer condition variable");
|
||||
if (pthread_mutex_init(&m_mutex, NULL) != 0)
|
||||
throw default_exception("failed to initialize timer mutex");
|
||||
|
||||
clock_serv_t host_clock;
|
||||
mach_timespec_t now;
|
||||
unsigned long long nano = static_cast<unsigned long long>(m_interval) * 1000000ull;
|
||||
|
||||
host_get_clock_service(mach_host_self(), CALENDAR_CLOCK, &host_clock);
|
||||
m_end_time.tv_sec = nano / 1000000000ull;
|
||||
m_end_time.tv_nsec = nano % 1000000000ull;
|
||||
clock_get_time(host_clock, &now);
|
||||
ADD_MACH_TIMESPEC(&m_end_time, &now);
|
||||
|
||||
|
||||
if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
|
||||
throw default_exception("failed to start timer thread");
|
||||
#elif defined(_LINUX_) || defined(_FREEBSD_)
|
||||
|
@ -183,9 +181,25 @@ struct scoped_timer::imp {
|
|||
INVALID_HANDLE_VALUE);
|
||||
#elif defined(__APPLE__) && defined(__MACH__)
|
||||
// Mac OS X
|
||||
pthread_cond_signal(&m_condition_var); // this is okay to fail
|
||||
|
||||
// If the waiting-thread is not up and waiting yet,
|
||||
// we can make sure that it finishes quickly by
|
||||
// setting the end-time to zero.
|
||||
m_end_time.tv_sec = 0;
|
||||
m_end_time.tv_nsec = 0;
|
||||
|
||||
// Otherwise it's already up and waiting, and
|
||||
// we can send a signal on m_condition_var:
|
||||
pthread_mutex_lock(&m_mutex);
|
||||
pthread_cond_signal(&m_condition_var);
|
||||
pthread_mutex_unlock(&m_mutex);
|
||||
|
||||
if (pthread_join(m_thread_id, NULL) != 0)
|
||||
throw default_exception("failed to join thread");
|
||||
if (pthread_mutex_destroy(&m_mutex) != 0)
|
||||
throw default_exception("failed to destroy pthread mutex");
|
||||
if (pthread_cond_destroy(&m_condition_var) != 0)
|
||||
throw default_exception("failed to destroy pthread condition variable");
|
||||
if (pthread_attr_destroy(&m_attributes) != 0)
|
||||
throw default_exception("failed to destroy pthread attributes object");
|
||||
#elif defined(_LINUX_) || defined(_FREEBSD_)
|
||||
|
|
Loading…
Reference in a new issue