diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index d31bcb729..98759e81a 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -912,6 +912,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
@@ -1472,9 +1473,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)
@@ -1493,9 +1503,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)
@@ -4147,6 +4166,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):
diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp
index 6d0823a24..badf8a59d 100644
--- a/src/ast/dl_decl_plugin.cpp
+++ b/src/ast/dl_decl_plugin.cpp
@@ -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");
diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h
index a662de578..65b00235c 100644
--- a/src/ast/dl_decl_plugin.h
+++ b/src/ast/dl_decl_plugin.h
@@ -48,6 +48,8 @@ namespace datalog {
OP_RA_CLONE,
OP_DL_CONSTANT,
OP_DL_LT,
+ OP_DL_REP,
+ OP_DL_ABS,
LAST_RA_OP
};
diff --git a/src/ast/scoped_proof.h b/src/ast/scoped_proof.h
index 68c186e85..e23a6d92a 100644
--- a/src/ast/scoped_proof.h
+++ b/src/ast/scoped_proof.h
@@ -16,8 +16,8 @@ Author:
Revision History:
--*/
-#ifndef _SCOPED_PROOF_H_
-#define _SCOPED_PROOF_H_
+#ifndef _SCOPED_PROOF__H_
+#define _SCOPED_PROOF__H_
#include "ast.h"
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 4a51e4943..08a29e381 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -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) {
diff --git a/src/duality/duality.h b/src/duality/duality.h
index 4005adc1a..c315c5431 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -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);
}
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index c10d83603..59611c814 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -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 = static_cast<int>(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);
+ }
+
}
+
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index a0975a719..0e367129d 100644
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -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;
+ }
};
diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp
index 32fe33566..8f98a23f9 100755
--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@@ -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;
}
diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h
index 550c563af..956191290 100755
--- a/src/interp/iz3base.h
+++ b/src/interp/iz3base.h
@@ -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){
diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h
index 7616b8664..5d401d49f 100644
--- a/src/interp/iz3hash.h
+++ b/src/interp/iz3hash.h
@@ -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>
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 4ef594cee..3ec2c42d1 100755
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -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;
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index 5fe3338dc..e89aa1d6d 100755
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -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;
}
diff --git a/src/interp/iz3scopes.h b/src/interp/iz3scopes.h
index cd7203eeb..bf93f4726 100755
--- a/src/interp/iz3scopes.h
+++ b/src/interp/iz3scopes.h
@@ -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
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index a7c2125e7..26786d57a 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -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();
}
diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h
index 3f164f275..86429b1a2 100644
--- a/src/math/simplex/simplex.h
+++ b/src/math/simplex/simplex.h
@@ -174,10 +174,11 @@ namespace simplex {
var_t select_pivot_core(var_t x_i, bool is_below, scoped_numeral& out_a_ij);
int get_num_non_free_dep_vars(var_t x_j, int best_so_far);
- var_t pick_var_to_leave(var_t x_j, bool inc, scoped_eps_numeral& gain, scoped_numeral& new_a_ij);
+ var_t pick_var_to_leave(var_t x_j, bool is_pos,
+ scoped_eps_numeral& gain, scoped_numeral& new_a_ij, bool& inc);
- void select_pivot_primal(var_t v, var_t& x_i, var_t& x_j, scoped_numeral& a_ij, bool& inc);
+ void select_pivot_primal(var_t v, var_t& x_i, var_t& x_j, scoped_numeral& a_ij, bool& inc_x_i, bool& inc_x_j);
bool at_lower(var_t v) const;
diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index c1a4ec36e..cfd557b33 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -646,13 +646,13 @@ namespace simplex {
scoped_eps_numeral delta(em);
scoped_numeral a_ij(m);
var_t x_i, x_j;
- bool inc;
+ bool inc_x_i, inc_x_j;
while (true) {
if (m_cancel) {
return l_undef;
}
- select_pivot_primal(v, x_i, x_j, a_ij, inc);
+ select_pivot_primal(v, x_i, x_j, a_ij, inc_x_i, inc_x_j);
if (x_j == null_var) {
// optimal
return l_true;
@@ -660,12 +660,12 @@ namespace simplex {
TRACE("simplex", tout << "x_i: v" << x_i << " x_j: v" << x_j << "\n";);
var_info& vj = m_vars[x_j];
if (x_i == null_var) {
- if (inc && vj.m_upper_valid) {
+ if (inc_x_j && vj.m_upper_valid) {
delta = vj.m_upper;
delta -= vj.m_value;
update_value(x_j, delta);
}
- else if (!inc && vj.m_lower_valid) {
+ else if (!inc_x_j && vj.m_lower_valid) {
delta = vj.m_lower;
delta -= vj.m_value;
update_value(x_j, delta);
@@ -686,7 +686,7 @@ namespace simplex {
pivot(x_i, x_j, a_ij);
TRACE("simplex", display(tout << "after pivot\n"););
- move_to_bound(x_i, !inc);
+ move_to_bound(x_i, !inc_x_i);
SASSERT(well_formed_row(row(m_vars[x_j].m_base2row)));
TRACE("simplex", display(tout););
SASSERT(is_feasible());
@@ -705,7 +705,7 @@ namespace simplex {
em.sub(vi.m_upper, vi.m_value, delta);
}
TRACE("simplex", tout << "move " << (to_lower?"to_lower":"to_upper")
- << " v" << x << " " << em.to_string(delta) << "\n";);
+ << " v" << x << " delta: " << em.to_string(delta) << "\n";);
col_iterator it = M.col_begin(x), end = M.col_end(x);
for (; it != end && is_pos(delta); ++it) {
//
@@ -756,10 +756,11 @@ namespace simplex {
x_i - base variable of row(x_i) to become non-base
x_j - variable in row(v) to make a base variable
a_ij - coefficient to x_j in row(x_i)
- inc - whether to increment x_j (true if coefficient in row(v) is negative).
+ inc - whether to increment x_i
*/
template<typename Ext>
- void simplex<Ext>::select_pivot_primal(var_t v, var_t& x_i, var_t& x_j, scoped_numeral& a_ij, bool& inc) {
+ void simplex<Ext>::select_pivot_primal(var_t v, var_t& x_i, var_t& x_j, scoped_numeral& a_ij,
+ bool& inc_x_i, bool& inc_x_j) {
row r(m_vars[v].m_base2row);
row_iterator it = M.row_begin(r), end = M.row_end(r);
@@ -767,25 +768,27 @@ namespace simplex {
scoped_numeral new_a_ij(m);
x_i = null_var;
x_j = null_var;
- inc = false;
+ inc_x_i = false;
+ bool inc_y = false;
for (; it != end; ++it) {
var_t x = it->m_var;
if (x == v) continue;
- bool is_pos = m.is_pos(it->m_coeff) == m.is_pos(m_vars[v].m_base_coeff);
- if ((is_pos && at_upper(x)) || (!is_pos && at_lower(x))) {
- TRACE("simplex", tout << "v" << x << " pos: " << is_pos
+ bool inc_x = m.is_pos(it->m_coeff) == m.is_pos(m_vars[v].m_base_coeff);
+ if ((inc_x && at_upper(x)) || (!inc_x && at_lower(x))) {
+ TRACE("simplex", tout << "v" << x << " pos: " << inc_x
<< " at upper: " << at_upper(x)
<< " at lower: " << at_lower(x) << "\n";);
continue; // variable cannot be used for improving bounds.
// TBD check?
- }
- var_t y = pick_var_to_leave(x, is_pos, new_gain, new_a_ij);
+ }
+ var_t y = pick_var_to_leave(x, inc_x, new_gain, new_a_ij, inc_y);
if (y == null_var) {
// unbounded.
x_i = y;
x_j = x;
- inc = is_pos;
+ inc_x_i = inc_y;
+ inc_x_j = inc_x;
a_ij = new_a_ij;
break;
}
@@ -794,20 +797,39 @@ namespace simplex {
((is_zero(new_gain) && is_zero(gain) && (x_i == null_var || y < x_i)));
if (better) {
+ TRACE("simplex",
+ em.display(tout << "gain:", gain);
+ em.display(tout << " new gain:", new_gain);
+ tout << " base x_i: " << y << ", new base x_j: " << x << ", inc x_j: " << inc_x << "\n";);
+
x_i = y;
x_j = x;
- inc = is_pos;
+ inc_x_i = inc_y;
+ inc_x_j = inc_x;
gain = new_gain;
a_ij = new_a_ij;
}
}
}
+ //
+ // y is a base variable.
+ // v is a base variable.
+ // v*a_v + x*a_x + E = 0
+ // y*b_y + x*b_x + F = 0
+ // inc(x) := sign(a_v) == sign(a_x)
+ // sign_eq := sign(b_y) == sign(b_x)
+ // sign_eq => (inc(x) != inc(y))
+ // !sign_eq => (inc(x) = inc(y))
+ // ->
+ // inc(y) := sign_eq != inc(x)
+ //
+
template<typename Ext>
typename simplex<Ext>::var_t
simplex<Ext>::pick_var_to_leave(
- var_t x_j, bool inc,
- scoped_eps_numeral& gain, scoped_numeral& new_a_ij) {
+ var_t x_j, bool inc_x_j,
+ scoped_eps_numeral& gain, scoped_numeral& new_a_ij, bool& inc_x_i) {
var_t x_i = null_var;
gain.reset();
scoped_eps_numeral curr_gain(em);
@@ -818,10 +840,13 @@ namespace simplex {
var_info& vi = m_vars[s];
numeral const& a_ij = it.get_row_entry().m_coeff;
numeral const& a_ii = vi.m_base_coeff;
- bool inc_s = (m.is_pos(a_ii) != m.is_pos(a_ij)) ? inc : !inc;
- TRACE("simplex", tout << "v" << x_j << " base v" << s << " incs: " << inc_s
- << " upper valid:" << vi.m_upper_valid
- << " lower valid:" << vi.m_lower_valid << "\n";
+ bool sign_eq = (m.is_pos(a_ii) == m.is_pos(a_ij));
+ bool inc_s = sign_eq != inc_x_j;
+ TRACE("simplex", tout << "x_j: v" << x_j << ", base x_i: v" << s
+ << ", inc_x_i: " << inc_s
+ << ", inc_x_j: " << inc_x_j
+ << ", upper valid:" << vi.m_upper_valid
+ << ", lower valid:" << vi.m_lower_valid << "\n";
display_row(tout, r););
if ((inc_s && !vi.m_upper_valid) || (!inc_s && !vi.m_lower_valid)) {
continue;
@@ -841,6 +866,7 @@ namespace simplex {
x_i = s;
gain = curr_gain;
new_a_ij = a_ij;
+ inc_x_i = inc_s;
TRACE("simplex", tout << "x_j v" << x_j << " x_i v" << x_i << " gain: ";
tout << curr_gain << "\n";);
}
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 4a9767cb0..a6b9695b4 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -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;
}
}
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 51b54bc01..1952cc42f 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -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);
/**
diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index e201c2a19..5bfbba6b2 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -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'),
))
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 587a184bc..0584e6b58 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -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";
diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index c7a8d5aa0..cdb4a5b9e 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -205,7 +205,6 @@ namespace datalog {
for (unsigned i = 0; i < rules.size(); ++i) {
app* head = rules[i]->get_head();
expr_ref_vector conj(m);
- unsigned n = head->get_num_args()-1;
for (unsigned j = 0; j < head->get_num_args(); ++j) {
expr* arg = head->get_arg(j);
if (!is_var(arg)) {
diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp
new file mode 100644
index 000000000..7ef2eadc6
--- /dev/null
+++ b/src/opt/hitting_sets.cpp
@@ -0,0 +1,370 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+ hitting_sets.h
+
+Abstract:
+
+ Hitting set approximations.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2014-06-06
+
+Notes:
+
+--*/
+#include "vector.h"
+#include "util.h"
+#include "hitting_sets.h"
+#include "simplex.h"
+#include "sparse_matrix_def.h"
+#include "simplex_def.h"
+
+typedef simplex::simplex<simplex::mpz_ext> Simplex;
+typedef simplex::sparse_matrix<simplex::mpz_ext> sparse_matrix;
+
+
+namespace opt {
+
+ struct hitting_sets::imp {
+ typedef unsigned_vector set;
+ volatile bool m_cancel;
+ rational m_lower;
+ rational m_upper;
+ vector<rational> m_weights;
+ rational m_max_weight;
+ rational m_denominator;
+ vector<set> m_S;
+ svector<lbool> m_value;
+ unsigned_vector m_value_trail;
+ unsigned_vector m_value_lim;
+ vector<unsigned_vector> m_use_list;
+ unsynch_mpz_manager m;
+ Simplex m_simplex;
+ unsigned m_weights_var;
+
+ imp():m_cancel(false) {}
+ ~imp() {}
+
+ void add_weight(rational const& w) {
+ SASSERT(w.is_pos());
+ unsigned var = m_weights.size();
+ m_simplex.ensure_var(var);
+ m_simplex.set_lower(var, mpq_inf(mpq(0),mpq(0)));
+ m_simplex.set_upper(var, mpq_inf(mpq(1),mpq(0)));
+ m_weights.push_back(w);
+ m_value.push_back(l_undef);
+ m_use_list.push_back(unsigned_vector());
+ m_max_weight += w;
+ }
+
+ void add_set(unsigned sz, unsigned const* S) {
+ if (sz == 0) {
+ return;
+ }
+ for (unsigned i = 0; i < sz; ++i) {
+ m_use_list[S[i]].push_back(m_S.size());
+ }
+ init_weights();
+ m_S.push_back(unsigned_vector(sz, S));
+ add_simplex_row(sz, S);
+ }
+
+ bool compute_lower() {
+ m_lower.reset();
+ return L1() && L2() && L3();
+ }
+
+ bool compute_upper() {
+ m_upper = m_max_weight;
+ return U1();
+ }
+
+ rational get_lower() {
+ return m_lower/m_denominator;
+ }
+
+ rational get_upper() {
+ return m_upper/m_denominator;
+ }
+
+ void set_cancel(bool f) {
+ m_cancel = f;
+ m_simplex.set_cancel(f);
+ }
+
+ void collect_statistics(::statistics& st) const {
+ m_simplex.collect_statistics(st);
+ }
+
+ void reset() {
+ m_lower.reset();
+ m_upper = m_max_weight;
+ }
+
+ void init_weights() {
+ if (m_weights_var != 0) {
+ return;
+ }
+ m_weights_var = m_weights.size();
+ unsigned_vector vars;
+ scoped_mpz_vector coeffs(m);
+
+ // normalize weights to integral.
+ rational d(1);
+ for (unsigned i = 0; i < m_weights.size(); ++i) {
+ d = lcm(d, denominator(m_weights[i]));
+ }
+ m_denominator = d;
+ if (!d.is_one()) {
+ for (unsigned i = 0; i < m_weights.size(); ++i) {
+ m_weights[i] *= d;
+ }
+ }
+ // set up Simplex objective function.
+ for (unsigned i = 0; i < m_weights.size(); ++i) {
+ vars.push_back(i);
+ coeffs.push_back(m_weights[i].to_mpq().numerator());
+ }
+ m_simplex.ensure_var(m_weights_var);
+ vars.push_back(m_weights_var);
+ coeffs.push_back(mpz(-1));
+ m_simplex.add_row(m_weights_var, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
+ }
+
+ struct scoped_select {
+ imp& s;
+ unsigned sz;
+ scoped_select(imp& s):s(s), sz(s.m_value_trail.size()) {
+ }
+ ~scoped_select() {
+ s.undo_select(sz);
+ }
+ };
+
+ struct value_lt {
+ vector<rational> const& weights;
+ unsigned_vector const& scores;
+ value_lt(vector<rational> const& weights, unsigned_vector const& scores):
+ weights(weights), scores(scores) {}
+ bool operator()(int v1, int v2) const {
+ // - score1 / w1 < - score2 / w2
+ // <=>
+ // score1 / w1 > score2 / w2
+ // <=>
+ // score1*w2 > score2*w1
+ unsigned score1 = scores[v1];
+ unsigned score2 = scores[v2];
+ rational w1 = weights[v1];
+ rational w2 = weights[v2];
+ return rational(score1)*w2 > rational(score2)*w1;
+ }
+ };
+
+
+ // compute upper bound for hitting set.
+ bool U1() {
+ rational w(0);
+ scoped_select _sc(*this);
+
+ // score each variable by the number of
+ // unassigned sets they occur in.
+ unsigned_vector scores;
+ init_scores(scores);
+
+ //
+ // Sort indices.
+ // The least literals are those where -score/w is minimized.
+ //
+ unsigned_vector indices;
+ for (unsigned i = 0; i < m_value.size(); ++i) {
+ indices.push_back(i);
+ }
+ value_lt lt(m_weights, scores);
+ while (!m_cancel) {
+ std::sort(indices.begin(), indices.end(), lt);
+ unsigned idx = indices[0];
+ if (scores[idx] == 0) {
+ break;
+ }
+ update_scores(scores, idx);
+ select(idx);
+ w += m_weights[idx];
+ }
+ if (w < m_upper) {
+ m_upper = w;
+ }
+ return !m_cancel;
+ }
+
+ void init_scores(unsigned_vector & scores) {
+ scores.reset();
+ for (unsigned i = 0; i < m_value.size(); ++i) {
+ scores.push_back(0);
+ }
+ for (unsigned i = 0; i < m_S.size(); ++i) {
+ set const& S = m_S[i];
+ if (!has_selected(S)) {
+ for (unsigned j = 0; j < S.size(); ++j) {
+ scores[S[j]]++;
+ }
+ }
+ }
+ }
+
+ void update_scores(unsigned_vector& scores, unsigned v) {
+ unsigned_vector const& v_uses = m_use_list[v];
+ for (unsigned i = 0; i < v_uses.size(); ++i) {
+ set const& S = m_S[v_uses[i]];
+ if (!has_selected(S)) {
+ for (unsigned j = 0; j < S.size(); ++j) {
+ --scores[S[j]];
+ }
+ }
+ }
+ }
+
+ bool L1() {
+ rational w(0);
+ scoped_select _sc(*this);
+ for (unsigned i = 0; !m_cancel && i < m_S.size(); ++i) {
+ set const& S = m_S[i];
+ SASSERT(!S.empty());
+ if (!has_selected(S)) {
+ w += m_weights[select_min(S)];
+ for (unsigned j = 0; j < S.size(); ++j) {
+ select(S[j]);
+ }
+ }
+ }
+ if (m_lower < w) {
+ m_lower = w;
+ }
+ return !m_cancel;
+ }
+
+ bool L2() {
+ rational w(0);
+ scoped_select _sc(*this);
+ int n = 0;
+ for (unsigned i = 0; i < m_S.size(); ++i) {
+ if (!has_selected(m_S[i])) ++n;
+ }
+ unsigned_vector scores;
+ init_scores(scores);
+ unsigned_vector indices;
+ for (unsigned i = 0; i < m_value.size(); ++i) {
+ indices.push_back(i);
+ }
+ value_lt lt(m_weights, scores);
+
+ std::sort(indices.begin(), indices.end(), lt);
+ for(unsigned i = 0; i < indices.size() && n > 0; ++i) {
+ // deg(c) = score(c)
+ // wt(c) = m_weights[c]
+ unsigned idx = indices[i];
+ if (scores[idx] == 0) {
+ break;
+ }
+ if (scores[idx] < static_cast<unsigned>(n) || m_weights[idx].is_one()) {
+ w += m_weights[idx];
+ }
+ else {
+ w += div((rational(n)*m_weights[idx]), rational(scores[idx]));
+ }
+ n -= scores[idx];
+ }
+ if (m_lower < w) {
+ m_lower = w;
+ }
+ return !m_cancel;
+ }
+
+ bool L3() {
+ TRACE("simplex", m_simplex.display(tout););
+ VERIFY(l_true == m_simplex.make_feasible());
+ TRACE("simplex", m_simplex.display(tout););
+ VERIFY(l_true == m_simplex.minimize(m_weights_var));
+ mpq_inf const& val = m_simplex.get_value(m_weights_var);
+ unsynch_mpq_inf_manager mg;
+ unsynch_mpq_manager& mq = mg.mpq_manager();
+ scoped_mpq c(mq);
+ mg.ceil(val, c);
+ rational w = rational(c);
+ if (w > m_lower) {
+ m_lower = w;
+ }
+ return true;
+ }
+
+ void add_simplex_row(unsigned sz, unsigned const* S) {
+ unsigned_vector vars;
+ scoped_mpz_vector coeffs(m);
+ for (unsigned i = 0; i < sz; ++i) {
+ vars.push_back(S[i]);
+ coeffs.push_back(mpz(1));
+ }
+ unsigned base_var = m_S.size() + m_weights.size();
+ m_simplex.ensure_var(base_var);
+ vars.push_back(base_var);
+ coeffs.push_back(mpz(-1));
+ // S - base_var = 0
+ // base_var >= 1
+ m_simplex.set_lower(base_var, mpq_inf(mpq(1),mpq(0)));
+ m_simplex.add_row(base_var, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
+ }
+
+ void undo_select(unsigned sz) {
+ for (unsigned j = sz; j < m_value_trail.size(); ++j) {
+ m_value[m_value_trail[j]] = l_undef;
+ }
+ m_value_trail.resize(sz);
+ }
+
+ unsigned select_min(set const& S) {
+ unsigned result = S[0];
+ for (unsigned i = 1; i < S.size(); ++i) {
+ if (m_weights[result] > m_weights[S[i]]) {
+ result = S[i];
+ }
+ }
+ return result;
+ }
+
+
+ lbool selected(unsigned j) const {
+ return m_value[j];
+ }
+
+ void select(unsigned j) {
+ m_value[j] = l_true;
+ m_value_trail.push_back(j);
+ }
+
+ bool has_selected(set const& S) {
+ for (unsigned i = 0; i < S.size(); ++i) {
+ if (l_true == selected(S[i])) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ };
+ hitting_sets::hitting_sets() { m_imp = alloc(imp); }
+ hitting_sets::~hitting_sets() { dealloc(m_imp); }
+ void hitting_sets::add_weight(rational const& w) { m_imp->add_weight(w); }
+ void hitting_sets::add_set(unsigned sz, unsigned const* elems) { m_imp->add_set(sz, elems); }
+ bool hitting_sets::compute_lower() { return m_imp->compute_lower(); }
+ bool hitting_sets::compute_upper() { return m_imp->compute_upper(); }
+ rational hitting_sets::get_lower() { return m_imp->get_lower(); }
+ rational hitting_sets::get_upper() { return m_imp->get_upper(); }
+ void hitting_sets::set_cancel(bool f) { m_imp->set_cancel(f); }
+ void hitting_sets::collect_statistics(::statistics& st) const { m_imp->collect_statistics(st); }
+ void hitting_sets::reset() { m_imp->reset(); }
+
+
+};
diff --git a/src/opt/hitting_sets.h b/src/opt/hitting_sets.h
new file mode 100644
index 000000000..bea5559f9
--- /dev/null
+++ b/src/opt/hitting_sets.h
@@ -0,0 +1,47 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+ hitting_sets.h
+
+Abstract:
+
+ Hitting set approximations.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2014-06-06
+
+Notes:
+
+--*/
+#ifndef _HITTING_SETS_H_
+#define _HITTING_SETS_H_
+
+#include "rational.h"
+#include "statistics.h"
+
+namespace opt {
+
+ class hitting_sets {
+ struct imp;
+ imp* m_imp;
+ public:
+ hitting_sets();
+ ~hitting_sets();
+ void add_weight(rational const& w);
+ void add_set(unsigned sz, unsigned const* elems);
+ bool compute_lower();
+ bool compute_upper();
+ rational get_lower();
+ rational get_upper();
+ void set_cancel(bool f);
+ void collect_statistics(::statistics& st) const;
+ void reset();
+ };
+
+
+};
+
+#endif
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 6c4bbc1b4..12a922b01 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -38,8 +38,8 @@ Notes:
#include "cancel_eh.h"
#include "scoped_timer.h"
#include "optsmt.h"
+#include "hitting_sets.h"
-#define USE_SIMPLEX 0
namespace opt {
@@ -614,9 +614,7 @@ namespace opt {
};
scoped_ptr<maxsmt_solver_base> maxs;
- optsmt m_optsmt; // hitting set optimizer based on simplex.
- opt_solver m_solver;
- unsigned m_objective; // index of objective
+ hitting_sets m_hs;
expr_ref_vector m_aux; // auxiliary (indicator) variables.
expr_ref_vector m_iaux; // auxiliary integer (indicator) variables.
expr_ref_vector m_naux; // negation of auxiliary variables.
@@ -628,31 +626,29 @@ namespace opt {
pb_util pb;
arith_util a;
stats m_stats;
+ bool m_at_lower_bound;
public:
hsmax(solver* s, ast_manager& m, maxsmt_solver_base* maxs):
maxsmt_solver_base(s, m),
maxs(maxs),
- m_optsmt(m),
- m_solver(m, m_params, symbol()),
m_aux(m),
m_iaux(m),
m_naux(m),
pb(m),
- a(m) {
+ a(m),
+ m_at_lower_bound(false) {
}
virtual ~hsmax() {}
virtual void set_cancel(bool f) {
maxsmt_solver_base::set_cancel(f);
maxs->set_cancel(f);
- m_optsmt.set_cancel(f);
}
virtual void updt_params(params_ref& p) {
maxsmt_solver_base::updt_params(p);
- m_solver.updt_params(p);
}
virtual void collect_statistics(statistics& st) const {
@@ -685,8 +681,8 @@ namespace opt {
if (m_cancel) {
return l_undef;
}
- lbool core_found = generate_cores(hs);
+ lbool core_found = generate_cores(hs);
switch(core_found) {
case l_undef:
return l_undef;
@@ -698,20 +694,20 @@ namespace opt {
break;
case l_false:
TRACE("opt", tout << "no more seeds\n";);
- m_lower = m_upper;
- return l_true;
+ m_lower = m_upper;
+ return l_true;
case l_undef:
return l_undef;
- }
- break;
+ }
+ break;
}
- case l_false:
+ case l_false:
TRACE("opt", tout << "no more cores\n";);
m_lower = m_upper;
return l_true;
- }
- }
- return l_true;
+ }
+ }
+ return l_true;
}
private:
@@ -740,26 +736,16 @@ namespace opt {
m_aux_active.push_back(false);
m_core_activity.push_back(0);
m_aux2index.insert(m_aux.back(), i);
-#if USE_SIMPLEX
- m_aux2index.insert(m_iaux.back(), i);
- fml = m.mk_and(a.mk_le(a.mk_numeral(rational::zero(), true), iaux),
- a.mk_le(iaux, a.mk_numeral(rational::one(), true)));
- rational const& w = m_weights[i];
- sum.push_back(a.mk_mul(a.mk_numeral(w, w.is_int()), iaux));
- m_solver.assert_expr(fml);
-#endif
if (tt) {
m_asms.push_back(m_aux.back());
ensure_active(i);
}
}
-#if USE_SIMPLEX
- obj = a.mk_add(sum.size(), sum.c_ptr());
- m_objective = m_optsmt.add(obj);
- m_optsmt.setup(m_solver);
-#else
maxs->init_soft(m_weights, m_aux);
-#endif
+
+ for (unsigned i = 0; i < m_weights.size(); ++i) {
+ m_hs.add_weight(m_weights[i]);
+ }
TRACE("opt", print_seed(tout););
}
@@ -895,54 +881,51 @@ namespace opt {
}
}
+ lbool next_seed(ptr_vector<expr>& hs, lbool core_found) {
+
+ if (core_found == l_false && m_at_lower_bound) {
+ return l_true;
+ }
+ lbool is_sat = next_seed();
+ switch(is_sat) {
+ case l_true:
+ seed2hs(false, hs);
+ return m_at_lower_bound?l_true:l_false;
+ case l_false:
+ TRACE("opt", tout << "no more seeds\n";);
+ return l_true;
+ case l_undef:
+ return l_undef;
+ }
+ return l_undef;
+ }
+
//
// retrieve the next seed that satisfies state of maxs.
// state of maxs must be satisfiable before optimization is called.
//
- //
// find a satisfying assignment to maxs state, that
// minimizes objective function.
//
lbool next_seed() {
scoped_stopwatch _sw(m_stats.m_aux_sat_time);
TRACE("opt", tout << "\n";);
-#if USE_SIMPLEX
- m_solver.display(std::cout);
- lbool is_sat = m_optsmt.lex(m_objective);
- if (is_sat == l_true) {
- model_ref mdl;
- m_optsmt.get_model(mdl);
-
- for (unsigned i = 0; i < num_soft(); ++i) {
- if (is_active(i)) {
- m_seed[i] = is_one(mdl, m_iaux[i].get());
- }
- else {
- m_seed[i] = false;
- }
- }
- print_seed(std::cout);
- TRACE("opt", print_seed(tout););
- }
-
-#else
// min c_i*(not x_i) for x_i are soft clauses.
// max c_i*x_i for x_i are soft clauses
lbool is_sat = l_true;
+ m_at_lower_bound = false;
+ expr_ref fml(m);
if (m_lower.is_pos()) {
- expr_ref fml(m);
solver::scoped_push _scope(maxs->s());
fml = pb.mk_le(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_lower);
maxs->add_hard(fml);
- //fml = pb.mk_ge(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_lower);
- //maxs->add_hard(fml);
- std::cout << fml << "\n";
is_sat = maxs->s().check_sat(0,0);
if (is_sat == l_true) {
maxs->set_model();
extract_seed();
+ m_at_lower_bound = true;
return l_true;
}
}
@@ -951,17 +934,32 @@ namespace opt {
maxs->set_model();
}
else {
+ m_at_lower_bound = true;
return is_sat;
}
- is_sat = (*maxs)();
-
+ is_sat = (*maxs)();
+
if (is_sat == l_true) {
extract_seed();
}
-#endif
return is_sat;
}
+#if 0
+ if (!m_hs.compute_upper()) {
+ return l_undef;
+ }
+ solver::scoped_push _scope(maxs->s());
+ fml = pb.mk_le(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_hs.get_upper());
+ IF_VERBOSE(0, verbose_stream() << "upper: " << m_hs.get_upper() << " " << m_upper << "\n";);
+ maxs->add_hard(fml);
+ TRACE("opt", tout << "checking with upper bound: " << m_hs.get_upper() << "\n";);
+ is_sat = maxs->s().check_sat(0,0);
+ std::cout << is_sat << "\n";
+
+ // TBD: uper bound estimate does not include the negative constraints.
+#endif
+
void extract_seed() {
model_ref mdl;
maxs->get_model(mdl);
@@ -1140,16 +1138,6 @@ namespace opt {
}
expr_ref_vector fmls(m);
expr_ref fml(m);
-#if USE_SIMPLEX
- for (unsigned i = 0; i < num_soft(); ++i) {
- if (!indices.contains(i)) {
- fmls.push_back(m_iaux[i].get());
- }
- }
- fml = a.mk_ge(a.mk_add(fmls.size(), fmls.c_ptr()), a.mk_numeral(rational::one(), true));
- m_solver.assert_expr(fml);
-
-#else
for (unsigned i = 0; i < num_soft(); ++i) {
if (!indices.contains(i)) {
fmls.push_back(m_aux[i].get());
@@ -1158,7 +1146,6 @@ namespace opt {
fml = m.mk_or(fmls.size(), fmls.c_ptr());
maxs->add_hard(fml);
set_upper();
-#endif
TRACE("opt", tout << fml << "\n";);
}
@@ -1174,25 +1161,17 @@ namespace opt {
void block_up() {
expr_ref_vector fmls(m);
expr_ref fml(m);
-#if USE_SIMPLEX
- for (unsigned i = 0; i < m_asms.size(); ++i) {
- unsigned index = m_aux2index.find(m_asms[i]);
- m_core_activity[index]++;
- fmls.push_back(m_iaux[index].get());
- }
- fml = a.mk_lt(a.mk_add(fmls.size(), fmls.c_ptr()), a.mk_numeral(rational(fmls.size()), true));
- TRACE("opt", tout << fml << "\n";);
- m_solver.assert_expr(fml);
-#else
+ unsigned_vector indices;
for (unsigned i = 0; i < m_asms.size(); ++i) {
unsigned index = m_aux2index.find(m_asms[i]);
fmls.push_back(m.mk_not(m_asms[i]));
m_core_activity[index]++;
+ indices.push_back(index);
}
fml = m.mk_or(fmls.size(), fmls.c_ptr());
TRACE("opt", tout << fml << "\n";);
+ m_hs.add_set(indices.size(), indices.c_ptr());
maxs->add_hard(fml);
-#endif
}
@@ -1224,7 +1203,6 @@ namespace opt {
rational r;
expr_ref val(m);
VERIFY(mdl->eval(e, val));
- std::cout << mk_pp(e, m) << " |-> " << val << "\n";
return a.is_numeral(val, r) && r.is_one();
}
@@ -1684,10 +1662,12 @@ namespace opt {
m_maxsmt = alloc(bcd2, s.get(), m);
}
else if (m_engine == symbol("hsmax")) {
+ //m_params.set_bool("pb.enable_simplex", true);
ref<opt_solver> s0 = alloc(opt_solver, m, m_params, symbol());
s0->check_sat(0,0);
maxsmt_solver_base* s2 = alloc(pbmax, s0.get(), m); // , s0->get_context());
s2->set_converter(s0->mc_ref().get());
+
m_maxsmt = alloc(hsmax, s.get(), m, s2);
}
// NB: this is experimental one-round version of SLS
diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp
index 854e15493..b4a1a6a8b 100644
--- a/src/qe/qe_sat_tactic.cpp
+++ b/src/qe/qe_sat_tactic.cpp
@@ -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]);
}
diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
index 4799b8b9f..9ad787c2a 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/src/smt/params/preprocessor_params.cpp
@@ -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) {
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 3dec59d29..a0d7e7823 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -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'),
diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp
index a45b53155..3b0ec8e5f 100644
--- a/src/smt/proto_model/datatype_factory.cpp
+++ b/src/smt/proto_model/datatype_factory.cpp
@@ -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;
}
}
@@ -170,8 +191,10 @@ expr * datatype_factory::get_fresh_value(sort * s) {
// Approach 2)
// For recursive datatypes.
// search for constructor...
+ unsigned num_iterations = 0;
if (m_util.is_recursive(s)) {
while(true) {
+ ++num_iterations;
TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
ptr_vector<func_decl>::const_iterator it = constructors->begin();
@@ -181,12 +204,26 @@ 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);
+ expr * maybe_new_arg = 0;
+ if (num_iterations <= 1) {
+ maybe_new_arg = get_almost_fresh_value(s_arg);
+ }
+ else {
+ maybe_new_arg = get_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;
}
@@ -202,6 +239,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
if (found_sibling) {
expr_ref new_value(m_manager);
new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
+ TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
m_last_fresh_value.insert(s, new_value);
if (!set->contains(new_value)) {
register_value(new_value);
diff --git a/src/smt/proto_model/datatype_factory.h b/src/smt/proto_model/datatype_factory.h
index e8e1f2589..f70604ca8 100644
--- a/src/smt/proto_model/datatype_factory.h
+++ b/src/smt/proto_model/datatype_factory.h
@@ -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() {}
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 70287728e..26b35f0ed 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -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);
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 8303d05ac..568e9fca9 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -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;
}
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index cf22c3e3a..6c138fd57 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -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);
diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp
index 4ef1bd8e0..fc9138bf6 100644
--- a/src/smt/theory_dl.cpp
+++ b/src/smt/theory_dl.cpp
@@ -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);
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index cb52f0e79..7570a73c5 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -471,7 +471,7 @@ namespace smt {
break;
}
- if (c->k().is_one() && c->is_ge()) {
+ if (c->k().is_one() && c->is_ge() && !m_enable_simplex) {
literal_vector& lits = get_lits();
lits.push_back(~lit);
for (unsigned i = 0; i < c->size(); ++i) {
@@ -480,7 +480,7 @@ namespace smt {
ctx.mk_th_axiom(get_id(), lit, ~c->lit(i));
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
- // return true;
+ return true;
}
// maximal coefficient:
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 4912916a1..3b0179944 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -219,6 +219,7 @@ int main(int argc, char ** argv) {
TST(sorting_network);
TST(theory_pb);
TST(simplex);
+ //TST_ARGV(hs);
}
void initialize_mam() {}
diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h
index 052183dd1..d7202a79a 100644
--- a/src/util/mpq_inf.h
+++ b/src/util/mpq_inf.h
@@ -248,7 +248,7 @@ public:
void ceil(mpq_inf const & a, mpq & b) {
if (m.is_int(a.first)) {
// special cases for k - delta*epsilon where k is an integer
- if (m.is_pos(a.first))
+ if (m.is_pos(a.second))
m.add(a.first, mpq(1), b); // ceil(k + delta*epsilon) --> k+1
else
m.set(b, a.first);
@@ -276,6 +276,7 @@ public:
out << to_string(a);
}
+ mpq_manager<SYNCH>& mpq_manager() { return m; }
};
typedef mpq_inf_manager<true> synch_mpq_inf_manager;
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index d0a79cec6..c4a640009 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -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_)