diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 560ee5885..98722022c 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -17,6 +17,7 @@ Revision History:
--*/
#include<iostream>
#include<sstream>
+#include<vector>
#include"z3.h"
#include"api_log_macros.h"
#include"api_context.h"
diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp
index 2a7de3176..7fd44c088 100644
--- a/src/cmd_context/interpolant_cmds.cpp
+++ b/src/cmd_context/interpolant_cmds.cpp
@@ -114,7 +114,7 @@ static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
- ptr_vector<ast> cnsts(end - it);
+ ptr_vector<ast> cnsts((unsigned)(end - it));
for (int i = 0; it != end; ++it, ++i)
cnsts[i] = *it;
@@ -139,10 +139,11 @@ static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) {
get_interpolant_and_maybe_check(ctx,t,m_params,false);
}
+#if 0
static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) {
get_interpolant_and_maybe_check(ctx,t,m_params,true);
}
-
+#endif
static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){
diff --git a/src/duality/duality.h b/src/duality/duality.h
index 979071639..8c469b9e4 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -36,12 +36,11 @@ namespace Duality {
struct Z3User {
context &ctx;
- solver &slvr;
typedef func_decl FuncDecl;
typedef expr Term;
- Z3User(context &_ctx, solver &_slvr) : ctx(_ctx), slvr(_slvr){}
+ Z3User(context &_ctx) : ctx(_ctx){}
const char *string_of_int(int n);
@@ -53,6 +52,8 @@ namespace Duality {
Term SubstRec(hash_map<ast, Term> &memo, const Term &t);
+ Term SubstRec(hash_map<ast, Term> &memo, hash_map<func_decl, func_decl> &map, const Term &t);
+
void Strengthen(Term &x, const Term &y);
// return the func_del of an app if it is uninterpreted
@@ -77,14 +78,14 @@ namespace Duality {
void Summarize(const Term &t);
- int CumulativeDecisions();
-
int CountOperators(const Term &t);
Term SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val);
Term RemoveRedundancy(const Term &t);
+ Term IneqToEq(const Term &t);
+
bool IsLiteral(const expr &lit, expr &atom, expr &val);
expr Negate(const expr &f);
@@ -98,7 +99,10 @@ namespace Duality {
bool IsClosedFormula(const Term &t);
Term AdjustQuantifiers(const Term &t);
-private:
+
+ FuncDecl RenumberPred(const FuncDecl &f, int n);
+
+protected:
void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
int CountOperatorsRec(hash_set<ast> &memo, const Term &t);
@@ -108,6 +112,7 @@ private:
expr ReduceAndOr(const std::vector<expr> &args, bool is_and, std::vector<expr> &res);
expr FinishAndOr(const std::vector<expr> &args, bool is_and);
expr PullCommonFactors(std::vector<expr> &args, bool is_and);
+ Term IneqToEqRec(hash_map<ast, Term> &memo, const Term &t);
};
@@ -256,9 +261,9 @@ private:
}
#endif
- iZ3LogicSolver(context &c) : LogicSolver(c) {
+ iZ3LogicSolver(context &c, bool models = true) : LogicSolver(c) {
ctx = ictx = &c;
- slvr = islvr = new interpolating_solver(*ictx);
+ slvr = islvr = new interpolating_solver(*ictx, models);
need_goals = false;
islvr->SetWeakInterpolants(true);
}
@@ -308,8 +313,8 @@ private:
}
LogicSolver *ls;
-
- private:
+
+ protected:
int nodeCount;
int edgeCount;
@@ -324,7 +329,7 @@ private:
public:
model dualModel;
- private:
+ protected:
literals dualLabels;
std::list<stack_entry> stack;
std::vector<Term> axioms; // only saved here for printing purposes
@@ -340,7 +345,7 @@ private:
inherit the axioms.
*/
- RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver)
+ RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver)
{
ls = _ls;
nodeCount = 0;
@@ -350,7 +355,7 @@ private:
proof_core = 0;
}
- ~RPFP();
+ virtual ~RPFP();
/** Symbolic representation of a relational transformer */
class Transformer
@@ -574,7 +579,7 @@ private:
* you must pop the context accordingly. The second argument is
* the number of pushes we are inside. */
- void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false);
+ virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false);
/* Constrain an edge by the annotation of one of its children. */
@@ -808,9 +813,31 @@ private:
/** Edges of the graph. */
std::vector<Edge *> edges;
+ /** Fuse a vector of transformers. If the total number of inputs of the transformers
+ is N, then the result is an N-ary transfomer whose output is the union of
+ the outputs of the given transformers. The is, suppose we have a vetor of transfoermers
+ {T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer
+
+ F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) =
+ T_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M))
+ */
+
+ Transformer Fuse(const std::vector<Transformer *> &trs);
+
+ /** Fuse edges so that each node is the output of at most one edge. This
+ transformation is solution-preserving, but changes the numbering of edges in
+ counterexamples.
+ */
+ void FuseEdges();
+
+ void RemoveDeadNodes();
+
Term SubstParams(const std::vector<Term> &from,
const std::vector<Term> &to, const Term &t);
+ Term SubstParamsNoCapture(const std::vector<Term> &from,
+ const std::vector<Term> &to, const Term &t);
+
Term Localize(Edge *e, const Term &t);
void EvalNodeAsConstraint(Node *p, Transformer &res);
@@ -829,7 +856,13 @@ private:
*/
void ComputeProofCore();
- private:
+ int CumulativeDecisions();
+
+ solver &slvr(){
+ return *ls->slvr;
+ }
+
+ protected:
void ClearProofCore(){
if(proof_core)
@@ -947,6 +980,8 @@ private:
expr SimplifyOr(std::vector<expr> &lits);
+ expr SimplifyAnd(std::vector<expr> &lits);
+
void SetAnnotation(Node *root, const expr &t);
void AddEdgeToSolver(Edge *edge);
@@ -959,9 +994,58 @@ private:
expr NegateLit(const expr &f);
+ expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox);
+
+ bool IsVar(const expr &t);
+
+ void GetVarsRec(hash_set<ast> &memo, const expr &cnst, std::vector<expr> &vars);
+
+ expr UnhoistPullRec(hash_map<ast,expr> & memo, const expr &w, hash_map<ast,expr> & init_defs, hash_map<ast,expr> & const_params, hash_map<ast,expr> &const_params_inv, std::vector<expr> &new_params);
+
+ void AddParamsToTransformer(Transformer &trans, const std::vector<expr> ¶ms);
+
+ expr AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector<expr> ¶ms);
+
+ expr GetRelRec(hash_set<ast> &memo, const expr &t, const func_decl &rel);
+
+ expr GetRel(Edge *edge, int child_idx);
+
+ void GetDefs(const expr &cnst, hash_map<ast,expr> &defs);
+
+ void GetDefsRec(const expr &cnst, hash_map<ast,expr> &defs);
+
+ void AddParamsToNode(Node *node, const std::vector<expr> ¶ms);
+
+ void UnhoistLoop(Edge *loop_edge, Edge *init_edge);
+
+ void Unhoist();
+
+ Term ElimIteRec(hash_map<ast,expr> &memo, const Term &t, std::vector<expr> &cnsts);
+
+ Term ElimIte(const Term &t);
+
+ void MarkLiveNodes(hash_map<Node *,std::vector<Edge *> > &outgoing, hash_set<Node *> &live_nodes, Node *node);
+
+ virtual void slvr_add(const expr &e);
+
+ virtual void slvr_pop(int i);
+
+ virtual void slvr_push();
+
+ virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0);
+
+ virtual lbool ls_interpolate_tree(TermTree *assumptions,
+ TermTree *&interpolants,
+ model &_model,
+ TermTree *goals = 0,
+ bool weak = false);
+
+ virtual bool proof_core_contains(const expr &e);
+
};
- /** RPFP solver base class. */
+
+ /** RPFP solver base class. */
class Solver {
@@ -1005,6 +1089,8 @@ private:
/** Object thrown on cancellation */
struct Canceled {};
+ /** Object thrown on incompleteness */
+ struct Incompleteness {};
};
}
@@ -1042,3 +1128,130 @@ namespace std {
}
};
}
+
+// #define LIMIT_STACK_WEIGHT 5
+
+
+namespace Duality {
+ /** Caching version of RPFP. Instead of asserting constraints, returns assumption literals */
+
+ class RPFP_caching : public RPFP {
+ public:
+
+ /** appends assumption literals for edge to lits. if with_children is true,
+ includes that annotation of the edge's children.
+ */
+ void AssertEdgeCache(Edge *e, std::vector<Term> &lits, bool with_children = false);
+
+ /** appends assumption literals for node to lits */
+ void AssertNodeCache(Node *, std::vector<Term> lits);
+
+ /** check assumption lits, and return core */
+ check_result CheckCore(const std::vector<Term> &assumps, std::vector<Term> &core);
+
+ /** Clone another RPFP into this one, keeping a map */
+ void Clone(RPFP *other);
+
+ /** Get the clone of a node */
+ Node *GetNodeClone(Node *other_node);
+
+ /** Get the clone of an edge */
+ Edge *GetEdgeClone(Edge *other_edge);
+
+ /** Try to strengthen the parent of an edge */
+ void GeneralizeCache(Edge *edge);
+
+ /** Try to propagate some facts from children to parents of edge.
+ Return true if success. */
+ bool PropagateCache(Edge *edge);
+
+ /** Construct a caching RPFP using a LogicSolver */
+ RPFP_caching(LogicSolver *_ls) : RPFP(_ls) {}
+
+ /** Constraint an edge by its child's annotation. Return
+ assumption lits. */
+ void ConstrainParentCache(Edge *parent, Node *child, std::vector<Term> &lits);
+
+#ifdef LIMIT_STACK_WEIGHT
+ virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false);
+#endif
+
+ virtual ~RPFP_caching(){}
+
+ protected:
+ hash_map<ast,expr> AssumptionLits;
+ hash_map<Node *, Node *> NodeCloneMap;
+ hash_map<Edge *, Edge *> EdgeCloneMap;
+ std::vector<expr> alit_stack;
+ std::vector<unsigned> alit_stack_sizes;
+ hash_map<Edge *, uptr<LogicSolver> > edge_solvers;
+
+#ifdef LIMIT_STACK_WEIGHT
+ struct weight_counter {
+ int val;
+ weight_counter(){val = 0;}
+ void swap(weight_counter &other){
+ std::swap(val,other.val);
+ }
+ };
+
+ struct big_stack_entry {
+ weight_counter weight_added;
+ std::vector<expr> new_alits;
+ std::vector<expr> alit_stack;
+ std::vector<unsigned> alit_stack_sizes;
+ };
+
+ std::vector<expr> new_alits;
+ weight_counter weight_added;
+ std::vector<big_stack_entry> big_stack;
+#endif
+
+
+
+ void GetAssumptionLits(const expr &fmla, std::vector<expr> &lits, hash_map<ast,expr> *opt_map = 0);
+
+ void GreedyReduceCache(std::vector<expr> &assumps, std::vector<expr> &core);
+
+ void FilterCore(std::vector<expr> &core, std::vector<expr> &full_core);
+ void ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector<expr> &lits);
+
+ virtual void slvr_add(const expr &e);
+
+ virtual void slvr_pop(int i);
+
+ virtual void slvr_push();
+
+ virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0);
+
+ virtual lbool ls_interpolate_tree(TermTree *assumptions,
+ TermTree *&interpolants,
+ model &_model,
+ TermTree *goals = 0,
+ bool weak = false);
+
+ virtual bool proof_core_contains(const expr &e);
+
+ void GetTermTreeAssertionLiterals(TermTree *assumptions);
+
+ void GetTermTreeAssertionLiteralsRec(TermTree *assumptions);
+
+ LogicSolver *SolverForEdge(Edge *edge, bool models);
+
+ public:
+ struct scoped_solver_for_edge {
+ LogicSolver *orig_ls;
+ RPFP_caching *rpfp;
+ scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){
+ rpfp = _rpfp;
+ orig_ls = rpfp->ls;
+ rpfp->ls = rpfp->SolverForEdge(edge,models);
+ }
+ ~scoped_solver_for_edge(){
+ rpfp->ls = orig_ls;
+ }
+ };
+
+ };
+
+}
diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp
index bec32c51a..a4e9e0240 100755
--- a/src/duality/duality_profiling.cpp
+++ b/src/duality/duality_profiling.cpp
@@ -25,7 +25,14 @@ Revision History:
#include <string.h>
#include <stdlib.h>
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#endif
+
#include "duality_wrapper.h"
+#include "iz3profiling.h"
namespace Duality {
@@ -103,6 +110,7 @@ namespace Duality {
output_time(*pfs, it->second.t);
(*pfs) << std::endl;
}
+ profiling::print(os); // print the interpolation stats
}
void timer_start(const char *name){
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index a5e2b9167..2d52ab283 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -21,13 +21,21 @@ Revision History:
-#include "duality.h"
-#include "duality_profiling.h"
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#endif
+
#include <algorithm>
#include <fstream>
#include <set>
#include <iterator>
+
+#include "duality.h"
+#include "duality_profiling.h"
+
#ifndef WIN32
// #define Z3OPS
#endif
@@ -104,7 +112,7 @@ namespace Duality {
lits.push_back(t);
}
- int Z3User::CumulativeDecisions(){
+ int RPFP::CumulativeDecisions(){
#if 0
std::string stats = Z3_statistics_to_string(ctx);
int pos = stats.find("decisions:");
@@ -113,7 +121,7 @@ namespace Duality {
std::string val = stats.substr(pos,end-pos);
return atoi(val.c_str());
#endif
- return slvr.get_num_decisions();
+ return slvr().get_num_decisions();
}
@@ -370,6 +378,38 @@ namespace Duality {
return res;
}
+ Z3User::Term Z3User::SubstRec(hash_map<ast, Term> &memo, hash_map<func_decl, func_decl> &map, const Term &t)
+ {
+ std::pair<ast,Term> foo(t,expr(ctx));
+ std::pair<hash_map<ast,Term>::iterator, bool> bar = memo.insert(foo);
+ Term &res = bar.first->second;
+ if(!bar.second) return res;
+ if (t.is_app())
+ {
+ func_decl f = t.decl();
+ std::vector<Term> args;
+ int nargs = t.num_args();
+ for(int i = 0; i < nargs; i++)
+ args.push_back(SubstRec(memo, map, t.arg(i)));
+ hash_map<func_decl,func_decl>::iterator it = map.find(f);
+ if(it != map.end())
+ f = it->second;
+ res = f(args.size(),&args[0]);
+ }
+ else if (t.is_quantifier())
+ {
+ std::vector<expr> pats;
+ t.get_patterns(pats);
+ for(unsigned i = 0; i < pats.size(); i++)
+ pats[i] = SubstRec(memo, map, pats[i]);
+ Term body = SubstRec(memo, map, t.body());
+ res = clone_quantifier(t, body, pats);
+ }
+ // res = CloneQuantifier(t,SubstRec(memo, t.body()));
+ else res = t;
+ return res;
+ }
+
bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){
if(!(lit.is_quantifier() && IsClosedFormula(lit))){
if(!lit.is_app())
@@ -519,6 +559,20 @@ namespace Duality {
const expr &lit = args[i];
expr atom, val;
if(IsLiteral(lit,atom,val)){
+ if(atom.is_app() && atom.decl().get_decl_kind() == Equal)
+ if(pol ? eq(val,ctx.bool_val(true)) : eq(val,ctx.bool_val(false))){
+ expr lhs = atom.arg(0), rhs = atom.arg(1);
+ if(lhs.is_numeral())
+ std::swap(lhs,rhs);
+ if(rhs.is_numeral() && lhs.is_app()){
+ for(unsigned j = 0; j < args.size(); j++)
+ if(j != i){
+ smemo.clear();
+ smemo[lhs] = rhs;
+ args[j] = SubstRec(smemo,args[j]);
+ }
+ }
+ }
for(unsigned j = 0; j < args.size(); j++)
if(j != i){
smemo.clear();
@@ -580,6 +634,50 @@ namespace Duality {
return t;
}
+ Z3User::Term Z3User::IneqToEqRec(hash_map<ast, Term> &memo, const Term &t)
+ {
+ std::pair<ast,Term> foo(t,expr(ctx));
+ std::pair<hash_map<ast,Term>::iterator, bool> bar = memo.insert(foo);
+ Term &res = bar.first->second;
+ if(!bar.second) return res;
+ if (t.is_app())
+ {
+ func_decl f = t.decl();
+ std::vector<Term> args;
+ int nargs = t.num_args();
+ for(int i = 0; i < nargs; i++)
+ args.push_back(IneqToEqRec(memo, t.arg(i)));
+
+ decl_kind k = f.get_decl_kind();
+ if(k == And){
+ for(int i = 0; i < nargs-1; i++){
+ if((args[i].is_app() && args[i].decl().get_decl_kind() == Geq &&
+ args[i+1].is_app() && args[i+1].decl().get_decl_kind() == Leq)
+ ||
+ (args[i].is_app() && args[i].decl().get_decl_kind() == Leq &&
+ args[i+1].is_app() && args[i+1].decl().get_decl_kind() == Geq))
+ if(eq(args[i].arg(0),args[i+1].arg(0)) && eq(args[i].arg(1),args[i+1].arg(1))){
+ args[i] = ctx.make(Equal,args[i].arg(0),args[i].arg(1));
+ args[i+1] = ctx.bool_val(true);
+ }
+ }
+ }
+ res = f(args.size(),&args[0]);
+ }
+ else if (t.is_quantifier())
+ {
+ Term body = IneqToEqRec(memo,t.body());
+ res = clone_quantifier(t, body);
+ }
+ else res = t;
+ return res;
+ }
+
+ Z3User::Term Z3User::IneqToEq(const Term &t){
+ hash_map<ast, Term> memo;
+ return IneqToEqRec(memo,t);
+ }
+
Z3User::Term Z3User::SubstRecHide(hash_map<ast, Term> &memo, const Term &t, int number)
{
std::pair<ast,Term> foo(t,expr(ctx));
@@ -618,6 +716,51 @@ namespace Duality {
return some_diff ? SubstRec(memo,t) : t;
}
+ RPFP::Term RPFP::SubstParamsNoCapture(const std::vector<Term> &from,
+ const std::vector<Term> &to, const Term &t){
+ hash_map<ast, Term> memo;
+ bool some_diff = false;
+ for(unsigned i = 0; i < from.size(); i++)
+ if(i < to.size() && !eq(from[i],to[i])){
+ memo[from[i]] = to[i];
+ // if the new param is not being mapped to anything else, we need to rename it to prevent capture
+ // note, if the new param *is* mapped later in the list, it will override this substitution
+ const expr &w = to[i];
+ if(memo.find(w) == memo.end()){
+ std::string old_name = w.decl().name().str();
+ func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), w.get_sort());
+ expr y = fresh();
+ memo[w] = y;
+ }
+ some_diff = true;
+ }
+ return some_diff ? SubstRec(memo,t) : t;
+ }
+
+
+
+ RPFP::Transformer RPFP::Fuse(const std::vector<Transformer *> &trs){
+ assert(!trs.empty());
+ const std::vector<expr> ¶ms = trs[0]->IndParams;
+ std::vector<expr> fmlas(trs.size());
+ fmlas[0] = trs[0]->Formula;
+ for(unsigned i = 1; i < trs.size(); i++)
+ fmlas[i] = SubstParamsNoCapture(trs[i]->IndParams,params,trs[i]->Formula);
+ std::vector<func_decl> rel_params = trs[0]->RelParams;
+ for(unsigned i = 1; i < trs.size(); i++){
+ const std::vector<func_decl> ¶ms2 = trs[i]->RelParams;
+ hash_map<func_decl,func_decl> map;
+ for(unsigned j = 0; j < params2.size(); j++){
+ func_decl rel = RenumberPred(params2[j],rel_params.size());
+ rel_params.push_back(rel);
+ map[params2[j]] = rel;
+ }
+ hash_map<ast,expr> memo;
+ fmlas[i] = SubstRec(memo,map,fmlas[i]);
+ }
+ return Transformer(rel_params,params,ctx.make(Or,fmlas),trs[0]->owner);
+ }
+
void Z3User::Strengthen(Term &x, const Term &y)
{
@@ -711,6 +854,33 @@ namespace Duality {
#endif
+ expr RPFP::GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox)
+ {
+ if (e->dual.null()) {
+ timer_start("ReducedDualEdge");
+ e->dual = ReducedDualEdge(e);
+ timer_stop("ReducedDualEdge");
+ timer_start("getting children");
+ if(underapprox){
+ std::vector<expr> cus(e->Children.size());
+ for(unsigned i = 0; i < e->Children.size(); i++)
+ cus[i] = !UnderapproxFlag(e->Children[i]) || GetUnderapprox(e->Children[i]);
+ expr cnst = conjoin(cus);
+ e->dual = e->dual && cnst;
+ }
+ timer_stop("getting children");
+ timer_start("Persisting");
+ std::list<stack_entry>::reverse_iterator it = stack.rbegin();
+ for(int i = 0; i < persist && it != stack.rend(); i++)
+ it++;
+ if(it != stack.rend())
+ it->edges.push_back(e);
+ timer_stop("Persisting");
+ //Console.WriteLine("{0}", cnst);
+ }
+ return e->dual;
+ }
+
/** For incremental solving, asserts the constraint associated
* with this edge in the SMT context. If this edge is removed,
* you must pop the context accordingly. The second argument is
@@ -732,45 +902,240 @@ namespace Duality {
{
if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty()))
return;
- if (e->dual.null())
- {
- timer_start("ReducedDualEdge");
- e->dual = ReducedDualEdge(e);
- timer_stop("ReducedDualEdge");
- timer_start("getting children");
- if(with_children)
- for(unsigned i = 0; i < e->Children.size(); i++)
- e->dual = e->dual && GetAnnotation(e->Children[i]);
- if(underapprox){
- std::vector<expr> cus(e->Children.size());
- for(unsigned i = 0; i < e->Children.size(); i++)
- cus[i] = !UnderapproxFlag(e->Children[i]) || GetUnderapprox(e->Children[i]);
- expr cnst = conjoin(cus);
- e->dual = e->dual && cnst;
- }
- timer_stop("getting children");
- timer_start("Persisting");
- std::list<stack_entry>::reverse_iterator it = stack.rbegin();
- for(int i = 0; i < persist && it != stack.rend(); i++)
- it++;
- if(it != stack.rend())
- it->edges.push_back(e);
-#if 0
- if(persist != 0)
- Z3_persist_ast(ctx,e->dual,persist);
-#endif
- timer_stop("Persisting");
- //Console.WriteLine("{0}", cnst);
- }
+ expr fmla = GetEdgeFormula(e, persist, with_children, underapprox);
timer_start("solver add");
- slvr.add(e->dual);
+ slvr_add(e->dual);
timer_stop("solver add");
+ if(with_children)
+ for(unsigned i = 0; i < e->Children.size(); i++)
+ ConstrainParent(e,e->Children[i]);
+ }
+
+
+#ifdef LIMIT_STACK_WEIGHT
+ void RPFP_caching::AssertEdge(Edge *e, int persist, bool with_children, bool underapprox)
+ {
+ unsigned old_new_alits = new_alits.size();
+ if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty()))
+ return;
+ expr fmla = GetEdgeFormula(e, persist, with_children, underapprox);
+ timer_start("solver add");
+ slvr_add(e->dual);
+ timer_stop("solver add");
+ if(old_new_alits < new_alits.size())
+ weight_added.val++;
+ if(with_children)
+ for(unsigned i = 0; i < e->Children.size(); i++)
+ ConstrainParent(e,e->Children[i]);
+ }
+#endif
+
+ // caching verion of above
+ void RPFP_caching::AssertEdgeCache(Edge *e, std::vector<Term> &lits, bool with_children){
+ if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty()))
+ return;
+ expr fmla = GetEdgeFormula(e, 0, with_children, false);
+ GetAssumptionLits(fmla,lits);
+ if(with_children)
+ for(unsigned i = 0; i < e->Children.size(); i++)
+ ConstrainParentCache(e,e->Children[i],lits);
+ }
+
+ void RPFP::slvr_add(const expr &e){
+ slvr().add(e);
+ }
+
+ void RPFP_caching::slvr_add(const expr &e){
+ GetAssumptionLits(e,alit_stack);
+ }
+
+ void RPFP::slvr_pop(int i){
+ slvr().pop(i);
+ }
+
+ void RPFP::slvr_push(){
+ slvr().push();
+ }
+
+ void RPFP_caching::slvr_pop(int i){
+ for(int j = 0; j < i; j++){
+#ifdef LIMIT_STACK_WEIGHT
+ if(alit_stack_sizes.empty()){
+ if(big_stack.empty())
+ throw "stack underflow";
+ for(unsigned k = 0; k < new_alits.size(); k++){
+ if(AssumptionLits.find(new_alits[k]) == AssumptionLits.end())
+ throw "foo!";
+ AssumptionLits.erase(new_alits[k]);
+ }
+ big_stack_entry &bsb = big_stack.back();
+ bsb.alit_stack_sizes.swap(alit_stack_sizes);
+ bsb.alit_stack.swap(alit_stack);
+ bsb.new_alits.swap(new_alits);
+ bsb.weight_added.swap(weight_added);
+ big_stack.pop_back();
+ slvr().pop(1);
+ continue;
+ }
+#endif
+ alit_stack.resize(alit_stack_sizes.back());
+ alit_stack_sizes.pop_back();
+ }
+ }
+
+ void RPFP_caching::slvr_push(){
+#ifdef LIMIT_STACK_WEIGHT
+ if(weight_added.val > LIMIT_STACK_WEIGHT){
+ big_stack.resize(big_stack.size()+1);
+ big_stack_entry &bsb = big_stack.back();
+ bsb.alit_stack_sizes.swap(alit_stack_sizes);
+ bsb.alit_stack.swap(alit_stack);
+ bsb.new_alits.swap(new_alits);
+ bsb.weight_added.swap(weight_added);
+ slvr().push();
+ for(unsigned i = 0; i < bsb.alit_stack.size(); i++)
+ slvr().add(bsb.alit_stack[i]);
+ return;
+ }
+#endif
+ alit_stack_sizes.push_back(alit_stack.size());
+ }
+
+ check_result RPFP::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){
+ return slvr().check(n, assumptions, core_size, core);
+ }
+
+ check_result RPFP_caching::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){
+ unsigned oldsiz = alit_stack.size();
+ if(n && assumptions)
+ std::copy(assumptions,assumptions+n,std::inserter(alit_stack,alit_stack.end()));
+ check_result res;
+ if(core_size && core){
+ std::vector<expr> full_core(alit_stack.size()), core1(n);
+ std::copy(assumptions,assumptions+n,core1.begin());
+ res = slvr().check(alit_stack.size(), &alit_stack[0], core_size, &full_core[0]);
+ full_core.resize(*core_size);
+ if(res == unsat){
+ FilterCore(core1,full_core);
+ *core_size = core1.size();
+ std::copy(core1.begin(),core1.end(),core);
+ }
+ }
+ else
+ res = slvr().check(alit_stack.size(), &alit_stack[0]);
+ alit_stack.resize(oldsiz);
+ return res;
+ }
+
+ lbool RPFP::ls_interpolate_tree(TermTree *assumptions,
+ TermTree *&interpolants,
+ model &_model,
+ TermTree *goals,
+ bool weak){
+ return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak);
+ }
+
+ lbool RPFP_caching::ls_interpolate_tree(TermTree *assumptions,
+ TermTree *&interpolants,
+ model &_model,
+ TermTree *goals,
+ bool weak){
+ GetTermTreeAssertionLiterals(assumptions);
+ return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak);
+ }
+
+ void RPFP_caching::GetTermTreeAssertionLiteralsRec(TermTree *assumptions){
+ std::vector<expr> alits;
+ hash_map<ast,expr> map;
+ GetAssumptionLits(assumptions->getTerm(),alits,&map);
+ std::vector<expr> &ts = assumptions->getTerms();
+ for(unsigned i = 0; i < ts.size(); i++)
+ GetAssumptionLits(ts[i],alits,&map);
+ assumptions->setTerm(ctx.bool_val(true));
+ ts = alits;
+ for(unsigned i = 0; i < alits.size(); i++)
+ ts.push_back(ctx.make(Implies,alits[i],map[alits[i]]));
+ for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
+ GetTermTreeAssertionLiterals(assumptions->getChildren()[i]);
+ return;
+ }
+
+ void RPFP_caching::GetTermTreeAssertionLiterals(TermTree *assumptions){
+ // optimize binary case
+ if(assumptions->getChildren().size() == 1
+ && assumptions->getChildren()[0]->getChildren().size() == 0){
+ hash_map<ast,expr> map;
+ TermTree *child = assumptions->getChildren()[0];
+ std::vector<expr> dummy;
+ GetAssumptionLits(child->getTerm(),dummy,&map);
+ std::vector<expr> &ts = child->getTerms();
+ for(unsigned i = 0; i < ts.size(); i++)
+ GetAssumptionLits(ts[i],dummy,&map);
+ std::vector<expr> assumps;
+ slvr().get_proof().get_assumptions(assumps);
+ if(!proof_core){ // save the proof core for later use
+ proof_core = new hash_set<ast>;
+ for(unsigned i = 0; i < assumps.size(); i++)
+ proof_core->insert(assumps[i]);
+ }
+ std::vector<expr> *cnsts[2] = {&child->getTerms(),&assumptions->getTerms()};
+ for(unsigned i = 0; i < assumps.size(); i++){
+ expr &ass = assumps[i];
+ expr alit = (ass.is_app() && ass.decl().get_decl_kind() == Implies) ? ass.arg(0) : ass;
+ bool isA = map.find(alit) != map.end();
+ cnsts[isA ? 0 : 1]->push_back(ass);
+ }
+ }
+ else
+ GetTermTreeAssertionLiteralsRec(assumptions);
+ }
+
+ void RPFP::AddToProofCore(hash_set<ast> &core){
+ std::vector<expr> assumps;
+ slvr().get_proof().get_assumptions(assumps);
+ for(unsigned i = 0; i < assumps.size(); i++)
+ core.insert(assumps[i]);
+ }
+
+ void RPFP::ComputeProofCore(){
+ if(!proof_core){
+ proof_core = new hash_set<ast>;
+ AddToProofCore(*proof_core);
+ }
+ }
+
+
+ void RPFP_caching::GetAssumptionLits(const expr &fmla, std::vector<expr> &lits, hash_map<ast,expr> *opt_map){
+ std::vector<expr> conjs;
+ CollectConjuncts(fmla,conjs);
+ for(unsigned i = 0; i < conjs.size(); i++){
+ const expr &conj = conjs[i];
+ std::pair<ast,Term> foo(conj,expr(ctx));
+ std::pair<hash_map<ast,Term>::iterator, bool> bar = AssumptionLits.insert(foo);
+ Term &res = bar.first->second;
+ if(bar.second){
+ func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort());
+ res = pred();
+#ifdef LIMIT_STACK_WEIGHT
+ new_alits.push_back(conj);
+#endif
+ slvr().add(ctx.make(Implies,res,conj));
+ // std::cout << res << ": " << conj << "\n";
+ }
+ if(opt_map)
+ (*opt_map)[res] = conj;
+ lits.push_back(res);
+ }
}
void RPFP::ConstrainParent(Edge *parent, Node *child){
ConstrainEdgeLocalized(parent,GetAnnotation(child));
}
+ void RPFP_caching::ConstrainParentCache(Edge *parent, Node *child, std::vector<Term> &lits){
+ ConstrainEdgeLocalizedCache(parent,GetAnnotation(child),lits);
+ }
+
/** For incremental solving, asserts the negation of the upper bound associated
* with a node.
@@ -782,10 +1147,60 @@ namespace Duality {
{
n->dual = GetUpperBound(n);
stack.back().nodes.push_back(n);
- slvr.add(n->dual);
+ slvr_add(n->dual);
}
}
+ // caching version of above
+ void RPFP_caching::AssertNodeCache(Node *n, std::vector<Term> lits){
+ if (n->dual.null())
+ {
+ n->dual = GetUpperBound(n);
+ stack.back().nodes.push_back(n);
+ GetAssumptionLits(n->dual,lits);
+ }
+ }
+
+ /** Clone another RPFP into this one, keeping a map */
+ void RPFP_caching::Clone(RPFP *other){
+#if 0
+ for(unsigned i = 0; i < other->nodes.size(); i++)
+ NodeCloneMap[other->nodes[i]] = CloneNode(other->nodes[i]);
+#endif
+ for(unsigned i = 0; i < other->edges.size(); i++){
+ Edge *edge = other->edges[i];
+ Node *parent = CloneNode(edge->Parent);
+ std::vector<Node *> cs;
+ for(unsigned j = 0; j < edge->Children.size(); j++)
+ // cs.push_back(NodeCloneMap[edge->Children[j]]);
+ cs.push_back(CloneNode(edge->Children[j]));
+ EdgeCloneMap[edge] = CreateEdge(parent,edge->F,cs);
+ }
+ }
+
+ /** Get the clone of a node */
+ RPFP::Node *RPFP_caching::GetNodeClone(Node *other_node){
+ return NodeCloneMap[other_node];
+ }
+
+ /** Get the clone of an edge */
+ RPFP::Edge *RPFP_caching::GetEdgeClone(Edge *other_edge){
+ return EdgeCloneMap[other_edge];
+ }
+
+ /** check assumption lits, and return core */
+ check_result RPFP_caching::CheckCore(const std::vector<Term> &assumps, std::vector<Term> &core){
+ core.resize(assumps.size());
+ unsigned core_size;
+ check_result res = slvr().check(assumps.size(),(expr *)&assumps[0],&core_size,&core[0]);
+ if(res == unsat)
+ core.resize(core_size);
+ else
+ core.clear();
+ return res;
+ }
+
+
/** Assert a constraint on an edge in the SMT context.
*/
@@ -799,9 +1214,15 @@ namespace Duality {
{
e->constraints.push_back(tl);
stack.back().constraints.push_back(std::pair<Edge *,Term>(e,tl));
- slvr.add(tl);
+ slvr_add(tl);
}
+ void RPFP_caching::ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector<expr> &lits)
+ {
+ e->constraints.push_back(tl);
+ stack.back().constraints.push_back(std::pair<Edge *,Term>(e,tl));
+ GetAssumptionLits(tl,lits);
+ }
/** Declare a constant in the background theory. */
@@ -829,7 +1250,7 @@ namespace Duality {
void RPFP::RemoveAxiom(const Term &t)
{
- slvr.RemoveInterpolationAxiom(t);
+ slvr().RemoveInterpolationAxiom(t);
}
#endif
@@ -878,7 +1299,7 @@ namespace Duality {
// if (dualLabels != null) dualLabels.Dispose();
timer_start("interpolate_tree");
- lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals,true);
+ lbool res = ls_interpolate_tree(tree, interpolant, dualModel,goals,true);
timer_stop("interpolate_tree");
if (res == l_false)
{
@@ -924,7 +1345,7 @@ namespace Duality {
ClearProofCore();
timer_start("interpolate_tree");
- lbool res = ls->interpolate_tree(tree, interpolant, dualModel,0,true);
+ lbool res = ls_interpolate_tree(tree, interpolant, dualModel,0,true);
timer_stop("interpolate_tree");
if (res == l_false)
{
@@ -970,26 +1391,27 @@ namespace Duality {
check_result RPFP::Check(Node *root, std::vector<Node *> underapproxes, std::vector<Node *> *underapprox_core )
{
+ timer_start("Check");
ClearProofCore();
// if (dualModel != null) dualModel.Dispose();
check_result res;
if(!underapproxes.size())
- res = slvr.check();
+ res = slvr_check();
else {
std::vector<expr> us(underapproxes.size());
for(unsigned i = 0; i < underapproxes.size(); i++)
us[i] = UnderapproxFlag(underapproxes[i]);
- slvr.check(); // TODO: no idea why I need to do this
+ slvr_check(); // TODO: no idea why I need to do this
if(underapprox_core){
std::vector<expr> unsat_core(us.size());
unsigned core_size = 0;
- res = slvr.check(us.size(),&us[0],&core_size,&unsat_core[0]);
+ res = slvr_check(us.size(),&us[0],&core_size,&unsat_core[0]);
underapprox_core->resize(core_size);
for(unsigned i = 0; i < core_size; i++)
(*underapprox_core)[i] = UnderapproxFlagRev(unsat_core[i]);
}
else {
- res = slvr.check(us.size(),&us[0]);
+ res = slvr_check(us.size(),&us[0]);
bool dump = false;
if(dump){
std::vector<expr> cnsts;
@@ -999,17 +1421,20 @@ namespace Duality {
ls->write_interpolation_problem("temp.smt",cnsts,std::vector<expr>());
}
}
- // check_result temp = slvr.check();
+ // check_result temp = slvr_check();
}
- dualModel = slvr.get_model();
+ dualModel = slvr().get_model();
+ timer_stop("Check");
return res;
}
check_result RPFP::CheckUpdateModel(Node *root, std::vector<expr> assumps){
- // check_result temp1 = slvr.check(); // no idea why I need to do this
+ // check_result temp1 = slvr_check(); // no idea why I need to do this
ClearProofCore();
- check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]);
- dualModel = slvr.get_model();
+ check_result res = slvr_check(assumps.size(),&assumps[0]);
+ model mod = slvr().get_model();
+ if(!mod.null())
+ dualModel = mod;;
return res;
}
@@ -1022,8 +1447,6 @@ namespace Duality {
return dualModel.eval(tl);
}
-
-
/** Returns true if the given node is empty in the primal solution. For proecudure summaries,
this means that the procedure is not called in the current counter-model. */
@@ -1301,7 +1724,7 @@ namespace Duality {
}
}
/* Unreachable! */
- throw "error in RPFP::GetLabelsRec";
+ // throw "error in RPFP::GetLabelsRec";
goto done;
}
else if(k == Not) {
@@ -1470,6 +1893,57 @@ namespace Duality {
return res;
}
+ RPFP::Term RPFP::ElimIteRec(hash_map<ast,expr> &memo, const Term &t, std::vector<expr> &cnsts){
+ std::pair<ast,Term> foo(t,expr(ctx));
+ std::pair<hash_map<ast,Term>::iterator, bool> bar = memo.insert(foo);
+ Term &res = bar.first->second;
+ if(bar.second){
+ if(t.is_app()){
+ int nargs = t.num_args();
+ std::vector<expr> args;
+ if(t.decl().get_decl_kind() == Equal){
+ expr lhs = t.arg(0);
+ expr rhs = t.arg(1);
+ if(rhs.decl().get_decl_kind() == Ite){
+ expr rhs_args[3];
+ lhs = ElimIteRec(memo,lhs,cnsts);
+ for(int i = 0; i < 3; i++)
+ rhs_args[i] = ElimIteRec(memo,rhs.arg(i),cnsts);
+ res = (rhs_args[0] && (lhs == rhs_args[1])) || ((!rhs_args[0]) && (lhs == rhs_args[2]));
+ goto done;
+ }
+ }
+ if(t.decl().get_decl_kind() == Ite){
+ func_decl sym = ctx.fresh_func_decl("@ite", t.get_sort());
+ res = sym();
+ cnsts.push_back(ElimIteRec(memo,ctx.make(Equal,res,t),cnsts));
+ }
+ else {
+ for(int i = 0; i < nargs; i++)
+ args.push_back(ElimIteRec(memo,t.arg(i),cnsts));
+ res = t.decl()(args.size(),&args[0]);
+ }
+ }
+ else if(t.is_quantifier())
+ res = clone_quantifier(t,ElimIteRec(memo,t.body(),cnsts));
+ else
+ res = t;
+ }
+ done:
+ return res;
+ }
+
+ RPFP::Term RPFP::ElimIte(const Term &t){
+ hash_map<ast,expr> memo;
+ std::vector<expr> cnsts;
+ expr res = ElimIteRec(memo,t,cnsts);
+ if(!cnsts.empty()){
+ cnsts.push_back(res);
+ res = ctx.make(And,cnsts);
+ }
+ return res;
+ }
+
void RPFP::Implicant(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits, hash_set<ast> &dont_cares){
hash_set<ast> done[2];
ImplicantRed(memo,f,lits,done,true, dont_cares);
@@ -1927,10 +2401,14 @@ namespace Duality {
for(int i = 0; i < num_args; i++)
CollectConjuncts(f.arg(i),lits,false);
}
- else if(pos)
- lits.push_back(f);
- else
- lits.push_back(!f);
+ else if(pos){
+ if(!eq(f,ctx.bool_val(true)))
+ lits.push_back(f);
+ }
+ else {
+ if(!eq(f,ctx.bool_val(false)))
+ lits.push_back(!f);
+ }
}
struct TermLt {
@@ -2253,6 +2731,45 @@ namespace Duality {
}
}
+ void RPFP_caching::FilterCore(std::vector<expr> &core, std::vector<expr> &full_core){
+ hash_set<ast> core_set;
+ std::copy(full_core.begin(),full_core.end(),std::inserter(core_set,core_set.begin()));
+ std::vector<expr> new_core;
+ for(unsigned i = 0; i < core.size(); i++)
+ if(core_set.find(core[i]) != core_set.end())
+ new_core.push_back(core[i]);
+ core.swap(new_core);
+ }
+
+ void RPFP_caching::GreedyReduceCache(std::vector<expr> &assumps, std::vector<expr> &core){
+ std::vector<expr> lits = assumps, full_core;
+ std::copy(core.begin(),core.end(),std::inserter(lits,lits.end()));
+
+ // verify
+ check_result res = CheckCore(lits,full_core);
+ if(res != unsat)
+ throw "should be unsat";
+ FilterCore(core,full_core);
+
+ std::vector<expr> dummy;
+ if(CheckCore(full_core,dummy) != unsat)
+ throw "should be unsat";
+
+ for(unsigned i = 0; i < core.size(); ){
+ expr temp = core[i];
+ std::swap(core[i],core.back());
+ core.pop_back();
+ lits.resize(assumps.size());
+ std::copy(core.begin(),core.end(),std::inserter(lits,lits.end()));
+ res = CheckCore(lits,full_core);
+ if(res != unsat){
+ core.push_back(temp);
+ std::swap(core[i],core.back());
+ i++;
+ }
+ }
+ }
+
expr RPFP::NegateLit(const expr &f){
if(f.is_app() && f.decl().get_decl_kind() == Not)
return f.arg(0);
@@ -2278,6 +2795,14 @@ namespace Duality {
return ctx.make(Or,lits);
}
+ expr RPFP::SimplifyAnd(std::vector<expr> &lits){
+ if(lits.size() == 0)
+ return ctx.bool_val(true);
+ if(lits.size() == 1)
+ return lits[0];
+ return ctx.make(And,lits);
+ }
+
// set up edge constraint in aux solver
void RPFP::AddEdgeToSolver(Edge *edge){
if(!edge->dual.null())
@@ -2289,6 +2814,7 @@ namespace Duality {
}
void RPFP::InterpolateByCases(Node *root, Node *node){
+ bool axioms_added = false;
aux_solver.push();
AddEdgeToSolver(node->Outgoing);
node->Annotation.SetEmpty();
@@ -2320,15 +2846,25 @@ namespace Duality {
std::vector<expr> case_lits;
itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
SetAnnotation(node,itp);
+ node->Annotation.Formula = node->Annotation.Formula.simplify();
}
if(node->Annotation.IsEmpty()){
- std::cout << "bad in InterpolateByCase -- core:\n";
- std::vector<expr> assumps;
- slvr.get_proof().get_assumptions(assumps);
- for(unsigned i = 0; i < assumps.size(); i++)
- assumps[i].show();
- throw "ack!";
+ if(!axioms_added){
+ // add the axioms in the off chance they are useful
+ const std::vector<expr> &theory = ls->get_axioms();
+ for(unsigned i = 0; i < theory.size(); i++)
+ aux_solver.add(theory[i]);
+ axioms_added = true;
+ }
+ else {
+ std::cout << "bad in InterpolateByCase -- core:\n";
+ std::vector<expr> assumps;
+ slvr().get_proof().get_assumptions(assumps);
+ for(unsigned i = 0; i < assumps.size(); i++)
+ assumps[i].show();
+ throw "ack!";
+ }
}
Pop(1);
node->Annotation.UnionWith(old_annot);
@@ -2340,6 +2876,7 @@ namespace Duality {
}
void RPFP::Generalize(Node *root, Node *node){
+ timer_start("Generalize");
aux_solver.push();
AddEdgeToSolver(node->Outgoing);
expr fmla = GetAnnotation(node);
@@ -2349,21 +2886,135 @@ namespace Duality {
aux_solver.pop(1);
NegateLits(conjuncts);
SetAnnotation(node,SimplifyOr(conjuncts));
+ timer_stop("Generalize");
}
+ RPFP::LogicSolver *RPFP_caching::SolverForEdge(Edge *edge, bool models){
+ uptr<LogicSolver> &p = edge_solvers[edge];
+ if(!p.get()){
+ scoped_no_proof no_proofs_please(ctx.m()); // no proofs
+ p.set(new iZ3LogicSolver(ctx,models)); // no models
+ }
+ return p.get();
+ }
+
+
+ // caching version of above
+ void RPFP_caching::GeneralizeCache(Edge *edge){
+ timer_start("Generalize");
+ scoped_solver_for_edge ssfe(this,edge);
+ Node *node = edge->Parent;
+ std::vector<expr> assumps, core, conjuncts;
+ AssertEdgeCache(edge,assumps);
+ for(unsigned i = 0; i < edge->Children.size(); i++){
+ expr ass = GetAnnotation(edge->Children[i]);
+ std::vector<expr> clauses;
+ if(!ass.is_true()){
+ CollectConjuncts(ass.arg(1),clauses);
+ for(unsigned j = 0; j < clauses.size(); j++)
+ GetAssumptionLits(ass.arg(0) || clauses[j],assumps);
+ }
+ }
+ expr fmla = GetAnnotation(node);
+ std::vector<expr> lits;
+ if(fmla.is_true()){
+ timer_stop("Generalize");
+ return;
+ }
+ assumps.push_back(fmla.arg(0).arg(0));
+ CollectConjuncts(!fmla.arg(1),lits);
+#if 0
+ for(unsigned i = 0; i < lits.size(); i++){
+ const expr &lit = lits[i];
+ if(lit.is_app() && lit.decl().get_decl_kind() == Equal){
+ lits[i] = ctx.make(Leq,lit.arg(0),lit.arg(1));
+ lits.push_back(ctx.make(Leq,lit.arg(1),lit.arg(0)));
+ }
+ }
+#endif
+ hash_map<ast,expr> lit_map;
+ for(unsigned i = 0; i < lits.size(); i++)
+ GetAssumptionLits(lits[i],core,&lit_map);
+ GreedyReduceCache(assumps,core);
+ for(unsigned i = 0; i < core.size(); i++)
+ conjuncts.push_back(lit_map[core[i]]);
+ NegateLits(conjuncts);
+ SetAnnotation(node,SimplifyOr(conjuncts));
+ timer_stop("Generalize");
+ }
+
+ // caching version of above
+ bool RPFP_caching::PropagateCache(Edge *edge){
+ timer_start("PropagateCache");
+ scoped_solver_for_edge ssfe(this,edge);
+ bool some = false;
+ {
+ std::vector<expr> candidates, skip;
+ Node *node = edge->Parent;
+ CollectConjuncts(node->Annotation.Formula,skip);
+ for(unsigned i = 0; i < edge->Children.size(); i++){
+ Node *child = edge->Children[i];
+ if(child->map == node->map){
+ CollectConjuncts(child->Annotation.Formula,candidates);
+ break;
+ }
+ }
+ if(candidates.empty()) goto done;
+ hash_set<ast> skip_set;
+ std::copy(skip.begin(),skip.end(),std::inserter(skip_set,skip_set.begin()));
+ std::vector<expr> new_candidates;
+ for(unsigned i = 0; i < candidates.size(); i++)
+ if(skip_set.find(candidates[i]) == skip_set.end())
+ new_candidates.push_back(candidates[i]);
+ candidates.swap(new_candidates);
+ if(candidates.empty()) goto done;
+ std::vector<expr> assumps, core, conjuncts;
+ AssertEdgeCache(edge,assumps);
+ for(unsigned i = 0; i < edge->Children.size(); i++){
+ expr ass = GetAnnotation(edge->Children[i]);
+ if(eq(ass,ctx.bool_val(true)))
+ continue;
+ std::vector<expr> clauses;
+ CollectConjuncts(ass.arg(1),clauses);
+ for(unsigned j = 0; j < clauses.size(); j++)
+ GetAssumptionLits(ass.arg(0) || clauses[j],assumps);
+ }
+ for(unsigned i = 0; i < candidates.size(); i++){
+ unsigned old_size = assumps.size();
+ node->Annotation.Formula = candidates[i];
+ expr fmla = GetAnnotation(node);
+ assumps.push_back(fmla.arg(0).arg(0));
+ GetAssumptionLits(!fmla.arg(1),assumps);
+ std::vector<expr> full_core;
+ check_result res = CheckCore(assumps,full_core);
+ if(res == unsat)
+ conjuncts.push_back(candidates[i]);
+ assumps.resize(old_size);
+ }
+ if(conjuncts.empty())
+ goto done;
+ SetAnnotation(node,SimplifyAnd(conjuncts));
+ some = true;
+ }
+ done:
+ timer_stop("PropagateCache");
+ return some;
+ }
+
+
/** Push a scope. Assertions made after Push can be undone by Pop. */
void RPFP::Push()
{
stack.push_back(stack_entry());
- slvr.push();
+ slvr_push();
}
/** Pop a scope (see Push). Note, you cannot pop axioms. */
void RPFP::Pop(int num_scopes)
{
- slvr.pop(num_scopes);
+ slvr_pop(num_scopes);
for (int i = 0; i < num_scopes; i++)
{
stack_entry &back = stack.back();
@@ -2381,15 +3032,15 @@ namespace Duality {
all the popped constraints */
void RPFP::PopPush(){
- slvr.pop(1);
- slvr.push();
+ slvr_pop(1);
+ slvr_push();
stack_entry &back = stack.back();
for(std::list<Edge *>::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it)
- slvr.add((*it)->dual);
+ slvr_add((*it)->dual);
for(std::list<Node *>::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it)
- slvr.add((*it)->dual);
+ slvr_add((*it)->dual);
for(std::list<std::pair<Edge *,Term> >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it)
- slvr.add((*it).second);
+ slvr_add((*it).second);
}
@@ -2407,6 +3058,17 @@ namespace Duality {
return ctx.function(name.c_str(), nargs, &sorts[0], t.get_sort());
}
+ Z3User::FuncDecl Z3User::RenumberPred(const FuncDecl &f, int n)
+ {
+ std::string name = f.name().str();
+ name = name.substr(0,name.rfind('_')) + "_" + string_of_int(n);
+ int arity = f.arity();
+ std::vector<sort> domain;
+ for(int i = 0; i < arity; i++)
+ domain.push_back(f.domain(i));
+ return ctx.function(name.c_str(), arity, &domain[0], f.range());
+ }
+
// Scan the clause body for occurrences of the predicate unknowns
RPFP::Term RPFP::ScanBody(hash_map<ast,Term> &memo,
@@ -2453,7 +3115,7 @@ namespace Duality {
bool Z3User::is_variable(const Term &t){
if(!t.is_app())
- return false;
+ return t.is_var();
return t.decl().get_decl_kind() == Uninterpreted
&& t.num_args() == 0;
}
@@ -2602,6 +3264,8 @@ namespace Duality {
arg.decl().get_decl_kind() == Uninterpreted);
}
+#define USE_QE_LITE
+
void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses){
hash_map<func_decl,Node *> pmap;
func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort());
@@ -2609,6 +3273,7 @@ namespace Duality {
std::vector<expr> clauses(unskolemized_clauses);
// first, skolemize the clauses
+#ifndef USE_QE_LITE
for(unsigned i = 0; i < clauses.size(); i++){
expr &t = clauses[i];
if (t.is_quantifier() && t.is_quantifier_forall()) {
@@ -2625,11 +3290,32 @@ namespace Duality {
t = SubstBound(subst,t.body());
}
}
+#else
+ std::vector<hash_map<int,expr> > substs(clauses.size());
+#endif
// create the nodes from the heads of the clauses
for(unsigned i = 0; i < clauses.size(); i++){
Term &clause = clauses[i];
+
+#ifdef USE_QE_LITE
+ Term &t = clause;
+ if (t.is_quantifier() && t.is_quantifier_forall()) {
+ int bound = t.get_quantifier_num_bound();
+ std::vector<sort> sorts;
+ std::vector<symbol> names;
+ for(int j = 0; j < bound; j++){
+ sort the_sort = t.get_quantifier_bound_sort(j);
+ symbol name = t.get_quantifier_bound_name(j);
+ expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
+ substs[i][bound-1-j] = skolem;
+ }
+ clause = t.body();
+ }
+
+#endif
+
if(clause.is_app() && clause.decl().get_decl_kind() == Uninterpreted)
clause = implies(ctx.bool_val(true),clause);
if(!canonical_clause(clause))
@@ -2661,6 +3347,13 @@ namespace Duality {
seen.insert(arg);
Indparams.push_back(arg);
}
+#ifdef USE_QE_LITE
+ {
+ hash_map<int,hash_map<ast,Term> > sb_memo;
+ for(unsigned j = 0; j < Indparams.size(); j++)
+ Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]);
+ }
+#endif
Node *node = CreateNode(R(Indparams.size(),&Indparams[0]));
//nodes.push_back(node);
pmap[R] = node;
@@ -2704,17 +3397,346 @@ namespace Duality {
Term labeled = body;
std::vector<label_struct > lbls; // TODO: throw this away for now
body = RemoveLabels(body,lbls);
+ // body = IneqToEq(body); // UFO converts x=y to (x<=y & x >= y). Undo this.
body = body.simplify();
+#ifdef USE_QE_LITE
+ std::set<int> idxs;
+ for(unsigned j = 0; j < Indparams.size(); j++)
+ if(Indparams[j].is_var())
+ idxs.insert(Indparams[j].get_index_value());
+ body = body.qe_lite(idxs,false);
+ hash_map<int,hash_map<ast,Term> > sb_memo;
+ body = SubstBoundRec(sb_memo,substs[i],0,body);
+ for(unsigned j = 0; j < Indparams.size(); j++)
+ Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]);
+#endif
+
// Create the edge
Transformer T = CreateTransformer(Relparams,Indparams,body);
Edge *edge = CreateEdge(Parent,T,Children);
edge->labeled = labeled;; // remember for label extraction
// edges.push_back(edge);
}
+
+ // undo hoisting of expressions out of loops
+ RemoveDeadNodes();
+ Unhoist();
+ // FuseEdges();
}
+ // The following mess is used to undo hoisting of expressions outside loops by compilers
+
+ expr RPFP::UnhoistPullRec(hash_map<ast,expr> & memo, const expr &w, hash_map<ast,expr> & init_defs, hash_map<ast,expr> & const_params, hash_map<ast,expr> &const_params_inv, std::vector<expr> &new_params){
+ if(memo.find(w) != memo.end())
+ return memo[w];
+ expr res;
+ if(init_defs.find(w) != init_defs.end()){
+ expr d = init_defs[w];
+ std::vector<expr> vars;
+ hash_set<ast> get_vars_memo;
+ GetVarsRec(get_vars_memo,d,vars);
+ hash_map<ast,expr> map;
+ for(unsigned j = 0; j < vars.size(); j++){
+ expr x = vars[j];
+ map[x] = UnhoistPullRec(memo,x,init_defs,const_params,const_params_inv,new_params);
+ }
+ expr defn = SubstRec(map,d);
+ res = defn;
+ }
+ else if(const_params_inv.find(w) == const_params_inv.end()){
+ std::string old_name = w.decl().name().str();
+ func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), w.get_sort());
+ expr y = fresh();
+ const_params[y] = w;
+ const_params_inv[w] = y;
+ new_params.push_back(y);
+ res = y;
+ }
+ else
+ res = const_params_inv[w];
+ memo[w] = res;
+ return res;
+ }
+
+ void RPFP::AddParamsToTransformer(Transformer &trans, const std::vector<expr> ¶ms){
+ std::copy(params.begin(),params.end(),std::inserter(trans.IndParams,trans.IndParams.end()));
+ }
+
+ expr RPFP::AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector<expr> ¶ms){
+ int n = app.num_args();
+ std::vector<expr> args(n);
+ for (int i = 0; i < n; i++)
+ args[i] = app.arg(i);
+ std::copy(params.begin(),params.end(),std::inserter(args,args.end()));
+ return new_decl(args);
+ }
+
+ expr RPFP::GetRelRec(hash_set<ast> &memo, const expr &t, const func_decl &rel){
+ if(memo.find(t) != memo.end())
+ return expr();
+ memo.insert(t);
+ if (t.is_app())
+ {
+ func_decl f = t.decl();
+ if(f == rel)
+ return t;
+ int nargs = t.num_args();
+ for(int i = 0; i < nargs; i++){
+ expr res = GetRelRec(memo,t.arg(i),rel);
+ if(!res.null())
+ return res;
+ }
+ }
+ else if (t.is_quantifier())
+ return GetRelRec(memo,t.body(),rel);
+ return expr();
+ }
+
+ expr RPFP::GetRel(Edge *edge, int child_idx){
+ func_decl &rel = edge->F.RelParams[child_idx];
+ hash_set<ast> memo;
+ return GetRelRec(memo,edge->F.Formula,rel);
+ }
+
+ void RPFP::GetDefsRec(const expr &cnst, hash_map<ast,expr> &defs){
+ if(cnst.is_app()){
+ switch(cnst.decl().get_decl_kind()){
+ case And: {
+ int n = cnst.num_args();
+ for(int i = 0; i < n; i++)
+ GetDefsRec(cnst.arg(i),defs);
+ break;
+ }
+ case Equal: {
+ expr lhs = cnst.arg(0);
+ expr rhs = cnst.arg(1);
+ if(IsVar(lhs))
+ defs[lhs] = rhs;
+ break;
+ }
+ default:
+ break;
+ }
+ }
+ }
+
+ void RPFP::GetDefs(const expr &cnst, hash_map<ast,expr> &defs){
+ // GetDefsRec(IneqToEq(cnst),defs);
+ GetDefsRec(cnst,defs);
+ }
+
+ bool RPFP::IsVar(const expr &t){
+ return t.is_app() && t.num_args() == 0 && t.decl().get_decl_kind() == Uninterpreted;
+ }
+
+ void RPFP::GetVarsRec(hash_set<ast> &memo, const expr &t, std::vector<expr> &vars){
+ if(memo.find(t) != memo.end())
+ return;
+ memo.insert(t);
+ if (t.is_app())
+ {
+ if(IsVar(t)){
+ vars.push_back(t);
+ return;
+ }
+ int nargs = t.num_args();
+ for(int i = 0; i < nargs; i++){
+ GetVarsRec(memo,t.arg(i),vars);
+ }
+ }
+ else if (t.is_quantifier())
+ GetVarsRec(memo,t.body(),vars);
+ }
+
+ void RPFP::AddParamsToNode(Node *node, const std::vector<expr> ¶ms){
+ int arity = node->Annotation.IndParams.size();
+ std::vector<sort> domain;
+ for(int i = 0; i < arity; i++)
+ domain.push_back(node->Annotation.IndParams[i].get_sort());
+ for(unsigned i = 0; i < params.size(); i++)
+ domain.push_back(params[i].get_sort());
+ std::string old_name = node->Name.name().str();
+ func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), domain, ctx.bool_sort());
+ node->Name = fresh;
+ AddParamsToTransformer(node->Annotation,params);
+ AddParamsToTransformer(node->Bound,params);
+ AddParamsToTransformer(node->Underapprox,params);
+ }
+
+ void RPFP::UnhoistLoop(Edge *loop_edge, Edge *init_edge){
+ loop_edge->F.Formula = IneqToEq(loop_edge->F.Formula);
+ init_edge->F.Formula = IneqToEq(init_edge->F.Formula);
+ expr pre = GetRel(loop_edge,0);
+ if(pre.null())
+ return; // this means the loop got simplified away
+ int nparams = loop_edge->F.IndParams.size();
+ hash_map<ast,expr> const_params, const_params_inv;
+ std::vector<expr> work_list;
+ // find the parameters that are constant in the loop
+ for(int i = 0; i < nparams; i++){
+ if(eq(pre.arg(i),loop_edge->F.IndParams[i])){
+ const_params[pre.arg(i)] = init_edge->F.IndParams[i];
+ const_params_inv[init_edge->F.IndParams[i]] = pre.arg(i);
+ work_list.push_back(pre.arg(i));
+ }
+ }
+ // get the definitions in the initialization
+ hash_map<ast,expr> defs,memo,subst;
+ GetDefs(init_edge->F.Formula,defs);
+ // try to pull them inside the loop
+ std::vector<expr> new_params;
+ for(unsigned i = 0; i < work_list.size(); i++){
+ expr v = work_list[i];
+ expr w = const_params[v];
+ expr def = UnhoistPullRec(memo,w,defs,const_params,const_params_inv,new_params);
+ if(!eq(def,v))
+ subst[v] = def;
+ }
+ // do the substitutions
+ if(subst.empty())
+ return;
+ subst[pre] = pre; // don't substitute inside the precondition itself
+ loop_edge->F.Formula = SubstRec(subst,loop_edge->F.Formula);
+ loop_edge->F.Formula = ElimIte(loop_edge->F.Formula);
+ init_edge->F.Formula = ElimIte(init_edge->F.Formula);
+ // add the new parameters
+ if(new_params.empty())
+ return;
+ Node *parent = loop_edge->Parent;
+ AddParamsToNode(parent,new_params);
+ AddParamsToTransformer(loop_edge->F,new_params);
+ AddParamsToTransformer(init_edge->F,new_params);
+ std::vector<Edge *> &incoming = parent->Incoming;
+ for(unsigned i = 0; i < incoming.size(); i++){
+ Edge *in_edge = incoming[i];
+ std::vector<Node *> &chs = in_edge->Children;
+ for(unsigned j = 0; j < chs.size(); j++)
+ if(chs[j] == parent){
+ expr lit = GetRel(in_edge,j);
+ expr new_lit = AddParamsToApp(lit,parent->Name,new_params);
+ func_decl fd = SuffixFuncDecl(new_lit,j);
+ int nargs = new_lit.num_args();
+ std::vector<Term> args;
+ for(int k = 0; k < nargs; k++)
+ args.push_back(new_lit.arg(k));
+ new_lit = fd(nargs,&args[0]);
+ in_edge->F.RelParams[j] = fd;
+ hash_map<ast,expr> map;
+ map[lit] = new_lit;
+ in_edge->F.Formula = SubstRec(map,in_edge->F.Formula);
+ }
+ }
+ }
+
+ void RPFP::Unhoist(){
+ hash_map<Node *,std::vector<Edge *> > outgoing;
+ for(unsigned i = 0; i < edges.size(); i++)
+ outgoing[edges[i]->Parent].push_back(edges[i]);
+ for(unsigned i = 0; i < nodes.size(); i++){
+ Node *node = nodes[i];
+ std::vector<Edge *> &outs = outgoing[node];
+ // if we're not a simple loop with one entry, give up
+ if(outs.size() == 2){
+ for(int j = 0; j < 2; j++){
+ Edge *loop_edge = outs[j];
+ Edge *init_edge = outs[1-j];
+ if(loop_edge->Children.size() == 1 && loop_edge->Children[0] == loop_edge->Parent){
+ UnhoistLoop(loop_edge,init_edge);
+ break;
+ }
+ }
+ }
+ }
+ }
+
+ void RPFP::FuseEdges(){
+ hash_map<Node *,std::vector<Edge *> > outgoing;
+ for(unsigned i = 0; i < edges.size(); i++){
+ outgoing[edges[i]->Parent].push_back(edges[i]);
+ }
+ hash_set<Edge *> edges_to_delete;
+ for(unsigned i = 0; i < nodes.size(); i++){
+ Node *node = nodes[i];
+ std::vector<Edge *> &outs = outgoing[node];
+ if(outs.size() > 1 && outs.size() <= 16){
+ std::vector<Transformer *> trs(outs.size());
+ for(unsigned j = 0; j < outs.size(); j++)
+ trs[j] = &outs[j]->F;
+ Transformer tr = Fuse(trs);
+ std::vector<Node *> chs;
+ for(unsigned j = 0; j < outs.size(); j++)
+ for(unsigned k = 0; k < outs[j]->Children.size(); k++)
+ chs.push_back(outs[j]->Children[k]);
+ CreateEdge(node,tr,chs);
+ for(unsigned j = 0; j < outs.size(); j++)
+ edges_to_delete.insert(outs[j]);
+ }
+ }
+ std::vector<Edge *> new_edges;
+ hash_set<Node *> all_nodes;
+ for(unsigned j = 0; j < edges.size(); j++){
+ if(edges_to_delete.find(edges[j]) == edges_to_delete.end()){
+#if 0
+ if(all_nodes.find(edges[j]->Parent) != all_nodes.end())
+ throw "help!";
+ all_nodes.insert(edges[j]->Parent);
+#endif
+ new_edges.push_back(edges[j]);
+ }
+ else
+ delete edges[j];
+ }
+ edges.swap(new_edges);
+ }
+
+ void RPFP::MarkLiveNodes(hash_map<Node *,std::vector<Edge *> > &outgoing, hash_set<Node *> &live_nodes, Node *node){
+ if(live_nodes.find(node) != live_nodes.end())
+ return;
+ live_nodes.insert(node);
+ std::vector<Edge *> &outs = outgoing[node];
+ for(unsigned i = 0; i < outs.size(); i++)
+ for(unsigned j = 0; j < outs[i]->Children.size(); j++)
+ MarkLiveNodes(outgoing, live_nodes,outs[i]->Children[j]);
+ }
+
+ void RPFP::RemoveDeadNodes(){
+ hash_map<Node *,std::vector<Edge *> > outgoing;
+ for(unsigned i = 0; i < edges.size(); i++)
+ outgoing[edges[i]->Parent].push_back(edges[i]);
+ hash_set<Node *> live_nodes;
+ for(unsigned i = 0; i < nodes.size(); i++)
+ if(!nodes[i]->Bound.IsFull())
+ MarkLiveNodes(outgoing,live_nodes,nodes[i]);
+ std::vector<Edge *> new_edges;
+ for(unsigned j = 0; j < edges.size(); j++){
+ if(live_nodes.find(edges[j]->Parent) != live_nodes.end())
+ new_edges.push_back(edges[j]);
+ else {
+ Edge *edge = edges[j];
+ for(unsigned int i = 0; i < edge->Children.size(); i++){
+ std::vector<Edge *> &ic = edge->Children[i]->Incoming;
+ for(std::vector<Edge *>::iterator it = ic.begin(), en = ic.end(); it != en; ++it){
+ if(*it == edge){
+ ic.erase(it);
+ break;
+ }
+ }
+ }
+ delete edge;
+ }
+ }
+ edges.swap(new_edges);
+ std::vector<Node *> new_nodes;
+ for(unsigned j = 0; j < nodes.size(); j++){
+ if(live_nodes.find(nodes[j]) != live_nodes.end())
+ new_nodes.push_back(nodes[j]);
+ else
+ delete nodes[j];
+ }
+ nodes.swap(new_nodes);
+ }
void RPFP::WriteSolution(std::ostream &s){
for(unsigned i = 0; i < nodes.size(); i++){
@@ -2854,26 +3876,26 @@ namespace Duality {
}
- void RPFP::AddToProofCore(hash_set<ast> &core){
- std::vector<expr> assumps;
- slvr.get_proof().get_assumptions(assumps);
- for(unsigned i = 0; i < assumps.size(); i++)
- core.insert(assumps[i]);
+
+ bool RPFP::proof_core_contains(const expr &e){
+ return proof_core->find(e) != proof_core->end();
}
-
- void RPFP::ComputeProofCore(){
- if(!proof_core){
- proof_core = new hash_set<ast>;
- AddToProofCore(*proof_core);
- }
+
+ bool RPFP_caching::proof_core_contains(const expr &e){
+ std::vector<expr> foo;
+ GetAssumptionLits(e,foo);
+ for(unsigned i = 0; i < foo.size(); i++)
+ if(proof_core->find(foo[i]) != proof_core->end())
+ return true;
+ return false;
}
bool RPFP::EdgeUsedInProof(Edge *edge){
ComputeProofCore();
- if(!edge->dual.null() && proof_core->find(edge->dual) != proof_core->end())
+ if(!edge->dual.null() && proof_core_contains(edge->dual))
return true;
for(unsigned i = 0; i < edge->constraints.size(); i++)
- if(proof_core->find(edge->constraints[i]) != proof_core->end())
+ if(proof_core_contains(edge->constraints[i]))
return true;
return false;
}
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 13c839186..973ad769c 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -19,6 +19,12 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#endif
+
#include "duality.h"
#include "duality_profiling.h"
@@ -26,6 +32,7 @@ Revision History:
#include <set>
#include <map>
#include <list>
+#include <iterator>
// TODO: make these official options or get rid of them
@@ -37,14 +44,18 @@ Revision History:
#define MINIMIZE_CANDIDATES
// #define MINIMIZE_CANDIDATES_HARDER
#define BOUNDED
-#define CHECK_CANDS_FROM_IND_SET
+// #define CHECK_CANDS_FROM_IND_SET
#define UNDERAPPROX_NODES
#define NEW_EXPAND
#define EARLY_EXPAND
// #define TOP_DOWN
// #define EFFORT_BOUNDED_STRAT
#define SKIP_UNDERAPPROX_NODES
-
+#define USE_RPFP_CLONE
+// #define KEEP_EXPANSIONS
+// #define USE_CACHING_RPFP
+// #define PROPAGATE_BEFORE_CHECK
+#define USE_NEW_GEN_CANDS
namespace Duality {
@@ -101,7 +112,7 @@ namespace Duality {
public:
Duality(RPFP *_rpfp)
: ctx(_rpfp->ctx),
- slvr(_rpfp->slvr),
+ slvr(_rpfp->slvr()),
nodes(_rpfp->nodes),
edges(_rpfp->edges)
{
@@ -115,8 +126,42 @@ namespace Duality {
Report = false;
StratifiedInlining = false;
RecursionBound = -1;
+ {
+ scoped_no_proof no_proofs_please(ctx.m());
+#ifdef USE_RPFP_CLONE
+ clone_ls = new RPFP::iZ3LogicSolver(ctx, false); // no models needed for this one
+ clone_rpfp = new RPFP_caching(clone_ls);
+ clone_rpfp->Clone(rpfp);
+#endif
+#ifdef USE_NEW_GEN_CANDS
+ gen_cands_ls = new RPFP::iZ3LogicSolver(ctx);
+ gen_cands_rpfp = new RPFP_caching(gen_cands_ls);
+ gen_cands_rpfp->Clone(rpfp);
+#endif
+ }
}
+ ~Duality(){
+#ifdef USE_RPFP_CLONE
+ delete clone_rpfp;
+ delete clone_ls;
+#endif
+#ifdef USE_NEW_GEN_CANDS
+ delete gen_cands_rpfp;
+ delete gen_cands_ls;
+#endif
+ }
+
+#ifdef USE_RPFP_CLONE
+ RPFP::LogicSolver *clone_ls;
+ RPFP_caching *clone_rpfp;
+#endif
+#ifdef USE_NEW_GEN_CANDS
+ RPFP::LogicSolver *gen_cands_ls;
+ RPFP_caching *gen_cands_rpfp;
+#endif
+
+
typedef RPFP::Node Node;
typedef RPFP::Edge Edge;
@@ -804,8 +849,10 @@ namespace Duality {
Node *child = chs[i];
if(TopoSort[child] < TopoSort[node->map]){
Node *leaf = LeafMap[child];
- if(!indset->Contains(leaf))
+ if(!indset->Contains(leaf)){
+ node->Outgoing->F.Formula = ctx.bool_val(false); // make this a proper leaf, else bogus cex
return node->Outgoing;
+ }
}
}
@@ -1085,7 +1132,8 @@ namespace Duality {
void ExtractCandidateFromCex(Edge *edge, RPFP *checker, Node *root, Candidate &candidate){
candidate.edge = edge;
for(unsigned j = 0; j < edge->Children.size(); j++){
- Edge *lb = root->Outgoing->Children[j]->Outgoing;
+ Node *node = root->Outgoing->Children[j];
+ Edge *lb = node->Outgoing;
std::vector<Node *> &insts = insts_of_node[edge->Children[j]];
#ifndef MINIMIZE_CANDIDATES
for(int k = insts.size()-1; k >= 0; k--)
@@ -1095,8 +1143,8 @@ namespace Duality {
{
Node *inst = insts[k];
if(indset->Contains(inst)){
- if(checker->Empty(lb->Parent) ||
- eq(checker->Eval(lb,NodeMarker(inst)),ctx.bool_val(true))){
+ if(checker->Empty(node) ||
+ eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){
candidate.Children.push_back(inst);
goto next_child;
}
@@ -1166,6 +1214,25 @@ namespace Duality {
#endif
+ Node *CheckerForEdgeClone(Edge *edge, RPFP_caching *checker){
+ Edge *gen_cands_edge = checker->GetEdgeClone(edge);
+ Node *root = gen_cands_edge->Parent;
+ root->Outgoing = gen_cands_edge;
+ GenNodeSolutionFromIndSet(edge->Parent, root->Bound);
+#if 0
+ if(root->Bound.IsFull())
+ return = 0;
+#endif
+ checker->AssertNode(root);
+ 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);
+ }
+ checker->AssertEdge(gen_cands_edge,1,true);
+ return root;
+ }
+
/** If the current proposed solution is not inductive,
use the induction failure to generate candidates for extension. */
void GenCandidatesFromInductionFailure(bool full_scan = false){
@@ -1175,6 +1242,7 @@ namespace Duality {
Edge *edge = edges[i];
if(!full_scan && updated_nodes.find(edge->Parent) == updated_nodes.end())
continue;
+#ifndef USE_NEW_GEN_CANDS
slvr.push();
RPFP *checker = new RPFP(rpfp->ls);
Node *root = CheckerForEdge(edge,checker);
@@ -1186,6 +1254,18 @@ namespace Duality {
}
slvr.pop(1);
delete checker;
+#else
+ RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */);
+ gen_cands_rpfp->Push();
+ Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
+ if(gen_cands_rpfp->Check(root) != unsat){
+ Candidate candidate;
+ ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate);
+ reporter->InductionFailure(edge,candidate.Children);
+ candidates.push_back(candidate);
+ }
+ gen_cands_rpfp->Pop(1);
+#endif
}
updated_nodes.clear();
timer_stop("GenCandIndFail");
@@ -1309,6 +1389,9 @@ namespace Duality {
node. */
bool SatisfyUpperBound(Node *node){
if(node->Bound.IsFull()) return true;
+#ifdef PROPAGATE_BEFORE_CHECK
+ Propagate();
+#endif
reporter->Bound(node);
int start_decs = rpfp->CumulativeDecisions();
DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand);
@@ -1412,13 +1495,77 @@ namespace Duality {
}
}
+ // Propagate conjuncts up the unwinding
+ void Propagate(){
+ reporter->Message("beginning propagation");
+ timer_start("Propagate");
+ std::vector<Node *> sorted_nodes = unwinding->nodes;
+ std::sort(sorted_nodes.begin(),sorted_nodes.end(),std::less<Node *>()); // sorts by sequence number
+ hash_map<Node *,std::set<expr> > facts;
+ for(unsigned i = 0; i < sorted_nodes.size(); i++){
+ Node *node = sorted_nodes[i];
+ std::set<expr> &node_facts = facts[node->map];
+ if(!(node->Outgoing && indset->Contains(node)))
+ continue;
+ std::vector<expr> conj_vec;
+ unwinding->CollectConjuncts(node->Annotation.Formula,conj_vec);
+ std::set<expr> conjs;
+ std::copy(conj_vec.begin(),conj_vec.end(),std::inserter(conjs,conjs.begin()));
+ if(!node_facts.empty()){
+ RPFP *checker = new RPFP(rpfp->ls);
+ slvr.push();
+ Node *root = checker->CloneNode(node);
+ Edge *edge = node->Outgoing;
+ // checker->AssertNode(root);
+ std::vector<Node *> cs;
+ for(unsigned j = 0; j < edge->Children.size(); j++){
+ Node *oc = edge->Children[j];
+ Node *nc = checker->CloneNode(oc);
+ nc->Annotation = oc->Annotation; // is this needed?
+ cs.push_back(nc);
+ }
+ Edge *checker_edge = checker->CreateEdge(root,edge->F,cs);
+ checker->AssertEdge(checker_edge, 0, true, false);
+ std::vector<expr> propagated;
+ for(std::set<expr> ::iterator it = node_facts.begin(), en = node_facts.end(); it != en;){
+ const expr &fact = *it;
+ if(conjs.find(fact) == conjs.end()){
+ root->Bound.Formula = fact;
+ slvr.push();
+ checker->AssertNode(root);
+ check_result res = checker->Check(root);
+ slvr.pop();
+ if(res != unsat){
+ std::set<expr> ::iterator victim = it;
+ ++it;
+ node_facts.erase(victim); // if it ain't true, nix it
+ continue;
+ }
+ propagated.push_back(fact);
+ }
+ ++it;
+ }
+ slvr.pop();
+ for(unsigned i = 0; i < propagated.size(); i++){
+ root->Annotation.Formula = propagated[i];
+ UpdateNodeToNode(node,root);
+ }
+ delete checker;
+ }
+ for(std::set<expr> ::iterator it = conjs.begin(), en = conjs.end(); it != en; ++it){
+ expr foo = *it;
+ node_facts.insert(foo);
+ }
+ }
+ timer_stop("Propagate");
+ }
/** This class represents a derivation tree. */
class DerivationTree {
public:
DerivationTree(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand)
- : slvr(rpfp->slvr),
+ : slvr(rpfp->slvr()),
ctx(rpfp->ctx)
{
duality = _duality;
@@ -1462,7 +1609,13 @@ namespace Duality {
constrained = _constrained;
false_approx = true;
timer_start("Derive");
+#ifndef USE_CACHING_RPFP
tree = _tree ? _tree : new RPFP(rpfp->ls);
+#else
+ RPFP::LogicSolver *cache_ls = new RPFP::iZ3LogicSolver(ctx);
+ cache_ls->slvr->push();
+ tree = _tree ? _tree : new RPFP_caching(cache_ls);
+#endif
tree->HornClauses = rpfp->HornClauses;
tree->Push(); // so we can clear out the solver later when finished
top = CreateApproximatedInstance(root);
@@ -1474,19 +1627,28 @@ namespace Duality {
timer_start("Pop");
tree->Pop(1);
timer_stop("Pop");
+#ifdef USE_CACHING_RPFP
+ cache_ls->slvr->pop(1);
+ delete cache_ls;
+ tree->ls = rpfp->ls;
+#endif
timer_stop("Derive");
return res;
}
#define WITH_CHILDREN
- Node *CreateApproximatedInstance(RPFP::Node *from){
- Node *to = tree->CloneNode(from);
- to->Annotation = from->Annotation;
+ void InitializeApproximatedInstance(RPFP::Node *to){
+ to->Annotation = to->map->Annotation;
#ifndef WITH_CHILDREN
tree->CreateLowerBoundEdge(to);
#endif
leaves.push_back(to);
+ }
+
+ Node *CreateApproximatedInstance(RPFP::Node *from){
+ Node *to = tree->CloneNode(from);
+ InitializeApproximatedInstance(to);
return to;
}
@@ -1555,13 +1717,23 @@ namespace Duality {
virtual void ExpandNode(RPFP::Node *p){
// tree->RemoveEdge(p->Outgoing);
- Edge *edge = duality->GetNodeOutgoing(p->map,last_decs);
- std::vector<RPFP::Node *> &cs = edge->Children;
- std::vector<RPFP::Node *> children(cs.size());
- for(unsigned i = 0; i < cs.size(); i++)
- children[i] = CreateApproximatedInstance(cs[i]);
- Edge *ne = tree->CreateEdge(p, p->map->Outgoing->F, children);
- ne->map = p->map->Outgoing->map;
+ Edge *ne = p->Outgoing;
+ if(ne) {
+ // reporter->Message("Recycling edge...");
+ std::vector<RPFP::Node *> &cs = ne->Children;
+ for(unsigned i = 0; i < cs.size(); i++)
+ InitializeApproximatedInstance(cs[i]);
+ // ne->dual = expr();
+ }
+ else {
+ Edge *edge = duality->GetNodeOutgoing(p->map,last_decs);
+ std::vector<RPFP::Node *> &cs = edge->Children;
+ std::vector<RPFP::Node *> children(cs.size());
+ for(unsigned i = 0; i < cs.size(); i++)
+ children[i] = CreateApproximatedInstance(cs[i]);
+ ne = tree->CreateEdge(p, p->map->Outgoing->F, children);
+ ne->map = p->map->Outgoing->map;
+ }
#ifndef WITH_CHILDREN
tree->AssertEdge(ne); // assert the edge in the solver
#else
@@ -1703,12 +1875,25 @@ namespace Duality {
void RemoveExpansion(RPFP::Node *p){
Edge *edge = p->Outgoing;
Node *parent = edge->Parent;
+#ifndef KEEP_EXPANSIONS
std::vector<RPFP::Node *> cs = edge->Children;
tree->DeleteEdge(edge);
for(unsigned i = 0; i < cs.size(); i++)
tree->DeleteNode(cs[i]);
+#endif
leaves.push_back(parent);
}
+
+ // remove all the descendants of tree root (but not root itself)
+ void RemoveTree(RPFP *tree, RPFP::Node *root){
+ Edge *edge = root->Outgoing;
+ std::vector<RPFP::Node *> cs = edge->Children;
+ tree->DeleteEdge(edge);
+ for(unsigned i = 0; i < cs.size(); i++){
+ RemoveTree(tree,cs[i]);
+ tree->DeleteNode(cs[i]);
+ }
+ }
};
class DerivationTreeSlow : public DerivationTree {
@@ -1730,13 +1915,14 @@ namespace Duality {
virtual bool Build(){
- stack.back().level = tree->slvr.get_scope_level();
+ stack.back().level = tree->slvr().get_scope_level();
+ bool was_sat = true;
while (true)
{
lbool res;
- unsigned slvr_level = tree->slvr.get_scope_level();
+ unsigned slvr_level = tree->slvr().get_scope_level();
if(slvr_level != stack.back().level)
throw "stacks out of sync!";
@@ -1756,14 +1942,22 @@ namespace Duality {
tree->SolveSingleNode(top,node);
if(expansions.size() == 1 && NodeTooComplicated(node))
SimplifyNode(node);
- tree->Generalize(top,node);
+ else
+ node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
+ Generalize(node);
if(RecordUpdate(node))
update_count++;
+ else
+ heuristic->Update(node->map); // make it less likely to expand this node in future
}
- if(update_count == 0)
+ if(update_count == 0){
+ if(was_sat)
+ throw Incompleteness();
reporter->Message("backtracked without learning");
+ }
}
tree->ComputeProofCore(); // need to compute the proof core before popping solver
+ bool propagated = false;
while(1) {
std::vector<Node *> &expansions = stack.back().expansions;
bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop
@@ -1787,28 +1981,42 @@ namespace Duality {
RemoveExpansion(node);
}
stack.pop_back();
- if(prev_level_used || stack.size() == 1) break;
+ if(stack.size() == 1)break;
+ if(prev_level_used){
+ Node *node = stack.back().expansions[0];
+ if(!Propagate(node)) break;
+ if(!RecordUpdate(node)) break; // shouldn't happen!
+ RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
+ propagated = true;
+ continue;
+ }
+ if(propagated) break; // propagation invalidates the proof core, so disable non-chron backtrack
RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
std::vector<Node *> &unused_ex = stack.back().expansions;
for(unsigned i = 0; i < unused_ex.size(); i++)
heuristic->Update(unused_ex[i]->map); // make it less likely to expand this node in future
}
HandleUpdatedNodes();
- if(stack.size() == 1)
+ if(stack.size() == 1){
+ if(top->Outgoing)
+ tree->DeleteEdge(top->Outgoing); // in case we kept the tree
return false;
+ }
+ was_sat = false;
}
else {
+ was_sat = true;
tree->Push();
std::vector<Node *> &expansions = stack.back().expansions;
for(unsigned i = 0; i < expansions.size(); i++){
tree->FixCurrentState(expansions[i]->Outgoing);
}
#if 0
- if(tree->slvr.check() == unsat)
+ if(tree->slvr().check() == unsat)
throw "help!";
#endif
stack.push_back(stack_entry());
- stack.back().level = tree->slvr.get_scope_level();
+ stack.back().level = tree->slvr().get_scope_level();
if(ExpandSomeNodes(false,1)){
continue;
}
@@ -1822,13 +2030,18 @@ namespace Duality {
}
bool NodeTooComplicated(Node *node){
+ int ops = tree->CountOperators(node->Annotation.Formula);
+ if(ops > 10) return true;
+ node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
return tree->CountOperators(node->Annotation.Formula) > 3;
}
void SimplifyNode(Node *node){
// have to destroy the old proof to get a new interpolant
+ timer_start("SimplifyNode");
tree->PopPush();
tree->InterpolateByCases(top,node);
+ timer_stop("SimplifyNode");
}
bool LevelUsedInProof(unsigned level){
@@ -1927,6 +2140,39 @@ namespace Duality {
throw "can't unmap node";
}
+ void Generalize(Node *node){
+#ifndef USE_RPFP_CLONE
+ tree->Generalize(top,node);
+#else
+ RPFP_caching *clone_rpfp = duality->clone_rpfp;
+ if(!node->Outgoing->map) return;
+ Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map);
+ Node *clone_node = clone_edge->Parent;
+ clone_node->Annotation = node->Annotation;
+ for(unsigned i = 0; i < clone_edge->Children.size(); i++)
+ clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation;
+ clone_rpfp->GeneralizeCache(clone_edge);
+ node->Annotation = clone_node->Annotation;
+#endif
+ }
+
+ bool Propagate(Node *node){
+#ifdef USE_RPFP_CLONE
+ RPFP_caching *clone_rpfp = duality->clone_rpfp;
+ Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map);
+ Node *clone_node = clone_edge->Parent;
+ clone_node->Annotation = node->map->Annotation;
+ for(unsigned i = 0; i < clone_edge->Children.size(); i++)
+ clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation;
+ bool res = clone_rpfp->PropagateCache(clone_edge);
+ if(res)
+ node->Annotation = clone_node->Annotation;
+ return res;
+#else
+ return false;
+#endif
+ }
+
};
@@ -1948,6 +2194,11 @@ namespace Duality {
Duality *parent;
bool some_updates;
+#define NO_CONJ_ON_SIMPLE_LOOPS
+#ifdef NO_CONJ_ON_SIMPLE_LOOPS
+ hash_set<Node *> simple_loops;
+#endif
+
Node *&covered_by(Node *node){
return cm[node].covered_by;
}
@@ -1982,6 +2233,24 @@ namespace Duality {
Covering(Duality *_parent){
parent = _parent;
some_updates = false;
+
+#ifdef NO_CONJ_ON_SIMPLE_LOOPS
+ hash_map<Node *,std::vector<Edge *> > outgoing;
+ for(unsigned i = 0; i < parent->rpfp->edges.size(); i++)
+ outgoing[parent->rpfp->edges[i]->Parent].push_back(parent->rpfp->edges[i]);
+ for(unsigned i = 0; i < parent->rpfp->nodes.size(); i++){
+ Node * node = parent->rpfp->nodes[i];
+ std::vector<Edge *> &outs = outgoing[node];
+ if(outs.size() == 2){
+ for(int j = 0; j < 2; j++){
+ Edge *loop_edge = outs[j];
+ if(loop_edge->Children.size() == 1 && loop_edge->Children[0] == loop_edge->Parent)
+ simple_loops.insert(node);
+ }
+ }
+ }
+#endif
+
}
bool IsCoveredRec(hash_set<Node *> &memo, Node *node){
@@ -2144,6 +2413,11 @@ namespace Duality {
}
bool CouldCover(Node *covered, Node *covering){
+#ifdef NO_CONJ_ON_SIMPLE_LOOPS
+ // Forsimple loops, we rely on propagation, not covering
+ if(simple_loops.find(covered->map) != simple_loops.end())
+ return false;
+#endif
#ifdef UNDERAPPROX_NODES
// if(parent->underapprox_map.find(covering) != parent->underapprox_map.end())
// return parent->underapprox_map[covering] == covered;
diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index 55883202f..cf2c803cb 100644
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -18,6 +18,13 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
#include "duality_wrapper.h"
#include <iostream>
#include "smt_solver.h"
@@ -30,10 +37,11 @@ Revision History:
namespace Duality {
- solver::solver(Duality::context& c, bool extensional) : object(c), the_model(c) {
+ solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) {
params_ref p;
p.set_bool("proof", true); // this is currently useless
- p.set_bool("model", true);
+ if(models)
+ p.set_bool("model", true);
p.set_bool("unsat_core", true);
p.set_bool("mbqi",true);
p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
@@ -44,6 +52,7 @@ namespace Duality {
m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
m_solver->updt_params(p); // why do we have to do this?
canceled = false;
+ m_mode = m().proof_mode();
}
expr context::constant(const std::string &name, const sort &ty){
@@ -338,6 +347,17 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
return ctx().cook(result);
}
+ expr expr::qe_lite(const std::set<int> &idxs, bool index_of_bound) const {
+ ::qe_lite qe(m());
+ expr_ref result(to_expr(raw()),m());
+ proof_ref pf(m());
+ uint_set uis;
+ for(std::set<int>::const_iterator it=idxs.begin(), en = idxs.end(); it != en; ++it)
+ uis.insert(*it);
+ qe(uis,index_of_bound,result);
+ return ctx().cook(result);
+ }
+
expr clone_quantifier(const expr &q, const expr &b){
return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw())));
}
@@ -362,6 +382,18 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
}
+ unsigned func_decl::arity() const {
+ return (to_func_decl(raw())->get_arity());
+ }
+
+ sort func_decl::domain(unsigned i) const {
+ return sort(ctx(),(to_func_decl(raw())->get_domain(i)));
+ }
+
+ sort func_decl::range() const {
+ return sort(ctx(),(to_func_decl(raw())->get_range()));
+ }
+
func_decl context::fresh_func_decl(char const * prefix, const std::vector<sort> &domain, sort const & range){
std::vector < ::sort * > _domain(domain.size());
for(unsigned i = 0; i < domain.size(); i++)
@@ -504,7 +536,10 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
add(linear_assumptions[i][j]);
}
- check_result res = check();
+ check_result res = unsat;
+
+ if(!m_solver->get_proof())
+ res = check();
if(res == unsat){
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index 3515194c0..891c4ca6f 100755
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -26,6 +26,7 @@ Revision History:
#include<sstream>
#include<vector>
#include<list>
+#include <set>
#include"version.h"
#include<limits.h>
@@ -50,6 +51,7 @@ Revision History:
#include"scoped_ctrl_c.h"
#include"cancel_eh.h"
#include"scoped_timer.h"
+#include"scoped_proof.h"
namespace Duality {
@@ -449,6 +451,7 @@ namespace Duality {
bool is_datatype() const { return get_sort().is_datatype(); }
bool is_relation() const { return get_sort().is_relation(); }
bool is_finite_domain() const { return get_sort().is_finite_domain(); }
+ bool is_true() const {return is_app() && decl().get_decl_kind() == True; }
bool is_numeral() const {
return is_app() && decl().get_decl_kind() == OtherArith && m().is_unique_value(to_expr(raw()));
@@ -560,6 +563,8 @@ namespace Duality {
expr qe_lite() const;
+ expr qe_lite(const std::set<int> &idxs, bool index_of_bound) const;
+
friend expr clone_quantifier(const expr &, const expr &);
friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);
@@ -718,6 +723,7 @@ namespace Duality {
m_model = s;
return *this;
}
+ bool null() const {return !m_model;}
expr eval(expr const & n, bool model_completion=true) const {
::model * _m = m_model.get();
@@ -811,8 +817,9 @@ namespace Duality {
::solver *m_solver;
model the_model;
bool canceled;
+ proof_gen_mode m_mode;
public:
- solver(context & c, bool extensional = false);
+ solver(context & c, bool extensional = false, bool models = true);
solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;}
solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;}
~solver() {
@@ -824,6 +831,7 @@ namespace Duality {
m_ctx = s.m_ctx;
m_solver = s.m_solver;
the_model = s.the_model;
+ m_mode = s.m_mode;
return *this;
}
struct cancel_exception {};
@@ -832,11 +840,12 @@ namespace Duality {
throw(cancel_exception());
}
// void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
- void push() { m_solver->push(); }
- void pop(unsigned n = 1) { m_solver->pop(n); }
+ void push() { scoped_proof_mode spm(m(),m_mode); m_solver->push(); }
+ void pop(unsigned n = 1) { scoped_proof_mode spm(m(),m_mode); m_solver->pop(n); }
// void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
- void add(expr const & e) { m_solver->assert_expr(e); }
+ void add(expr const & e) { scoped_proof_mode spm(m(),m_mode); m_solver->assert_expr(e); }
check_result check() {
+ scoped_proof_mode spm(m(),m_mode);
checkpoint();
lbool r = m_solver->check_sat(0,0);
model_ref m;
@@ -845,6 +854,7 @@ namespace Duality {
return to_check_result(r);
}
check_result check_keep_model(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) {
+ scoped_proof_mode spm(m(),m_mode);
model old_model(the_model);
check_result res = check(n,assumptions,core_size,core);
if(the_model == 0)
@@ -852,6 +862,7 @@ namespace Duality {
return res;
}
check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) {
+ scoped_proof_mode spm(m(),m_mode);
checkpoint();
std::vector< ::expr *> _assumptions(n);
for (unsigned i = 0; i < n; i++) {
@@ -876,6 +887,7 @@ namespace Duality {
}
#if 0
check_result check(expr_vector assumptions) {
+ scoped_proof_mode spm(m(),m_mode);
unsigned n = assumptions.size();
z3array<Z3_ast> _assumptions(n);
for (unsigned i = 0; i < n; i++) {
@@ -900,17 +912,19 @@ namespace Duality {
int get_num_decisions();
void cancel(){
+ scoped_proof_mode spm(m(),m_mode);
canceled = true;
if(m_solver)
m_solver->cancel();
}
- unsigned get_scope_level(){return m_solver->get_scope_level();}
+ unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();}
void show();
void show_assertion_ids();
proof get_proof(){
+ scoped_proof_mode spm(m(),m_mode);
return proof(ctx(),m_solver->get_proof());
}
@@ -1294,8 +1308,8 @@ namespace Duality {
class interpolating_solver : public solver {
public:
- interpolating_solver(context &ctx)
- : solver(ctx)
+ interpolating_solver(context &ctx, bool models = true)
+ : solver(ctx, true, models)
{
weak_mode = false;
}
@@ -1359,6 +1373,21 @@ namespace Duality {
typedef double clock_t;
clock_t current_time();
inline void output_time(std::ostream &os, clock_t time){os << time;}
+
+ template <class X> class uptr {
+ public:
+ X *ptr;
+ uptr(){ptr = 0;}
+ void set(X *_ptr){
+ if(ptr) delete ptr;
+ ptr = _ptr;
+ }
+ X *get(){ return ptr;}
+ ~uptr(){
+ if(ptr) delete ptr;
+ }
+ };
+
};
// to make Duality::ast hashable
@@ -1393,6 +1422,18 @@ namespace std {
};
}
+// to make Duality::ast usable in ordered collections
+namespace std {
+ template <>
+ class less<Duality::expr> {
+ public:
+ bool operator()(const Duality::expr &s, const Duality::expr &t) const {
+ // return s.raw() < t.raw();
+ return s.raw()->get_id() < t.raw()->get_id();
+ }
+ };
+}
+
// to make Duality::func_decl hashable
namespace hash_space {
template <>
@@ -1425,6 +1466,5 @@ namespace std {
};
}
-
#endif
diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp
index f316c22cf..26146bfa3 100755
--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@@ -18,6 +18,12 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
#include "iz3base.h"
#include <stdio.h>
diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp
index b4e55af20..d423ba48f 100755
--- a/src/interp/iz3checker.cpp
+++ b/src/interp/iz3checker.cpp
@@ -17,6 +17,13 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
#include "iz3base.h"
#include "iz3checker.h"
diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h
index 75d9aa604..94f282265 100755
--- a/src/interp/iz3hash.h
+++ b/src/interp/iz3hash.h
@@ -66,7 +66,7 @@ Revision History:
namespace stl_ext {
template <>
class hash<std::string> {
- stl_ext::hash<char *> H;
+ stl_ext::hash<const char *> H;
public:
size_t operator()(const std::string &s) const {
return H(s.c_str());
diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index 56dc1ccec..c204cc35d 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -18,6 +18,14 @@ Revision History:
--*/
/* Copyright 2011 Microsoft Research. */
+
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
#include <assert.h>
#include <algorithm>
#include <stdio.h>
diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index f35dae93f..6664cd2fe 100644
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -18,6 +18,15 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#pragma warning(disable:4805)
+#pragma warning(disable:4800)
+#endif
+
#include "iz3mgr.h"
#include <stdio.h>
@@ -172,7 +181,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){
std::vector<symbol> names;
- std::vector<sort *> types;
+ std::vector<class sort *> types;
std::vector<expr *> bound_asts;
unsigned num_bound = bvs.size();
@@ -485,7 +494,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<ast>& coeffs){
get_farkas_coeffs(proof,rats);
coeffs.resize(rats.size());
for(unsigned i = 0; i < rats.size(); i++){
- sort *is = m().mk_sort(m_arith_fid, INT_SORT);
+ class sort *is = m().mk_sort(m_arith_fid, INT_SORT);
ast coeff = cook(m_arith_util.mk_numeral(rats[i],is));
coeffs[i] = coeff;
}
@@ -640,9 +649,9 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rationa
/** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */
-void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q){
+void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
ast Qrhs;
- bool strict = op(P) == Lt;
+ bool qstrict = false;
if(is_not(Q)){
ast nQ = arg(Q,0);
switch(op(nQ)){
@@ -654,11 +663,11 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q){
break;
case Geq:
Qrhs = make(Sub,arg(nQ,1),arg(nQ,0));
- strict = true;
+ qstrict = true;
break;
case Leq:
Qrhs = make(Sub,arg(nQ,0),arg(nQ,1));
- strict = true;
+ qstrict = true;
break;
default:
throw "not an inequality";
@@ -674,28 +683,31 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q){
break;
case Lt:
Qrhs = make(Sub,arg(Q,1),arg(Q,0));
- strict = true;
+ qstrict = true;
break;
case Gt:
Qrhs = make(Sub,arg(Q,0),arg(Q,1));
- strict = true;
+ qstrict = true;
break;
default:
throw "not an inequality";
}
}
Qrhs = make(Times,c,Qrhs);
+ bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
+ if(pstrict && qstrict && round_off)
+ Qrhs = make(Sub,Qrhs,make_int(rational(1)));
if(strict)
P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
else
P = make(Leq,arg(P,0),make(Plus,arg(P,1),Qrhs));
}
-iz3mgr::ast iz3mgr::sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs){
+iz3mgr::ast iz3mgr::sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs, bool round_off){
ast zero = make_int("0");
ast thing = make(Leq,zero,zero);
for(unsigned i = 0; i < ineqs.size(); i++){
- linear_comb(thing,coeffs[i],ineqs[i]);
+ linear_comb(thing,coeffs[i],ineqs[i], round_off);
}
thing = simplify_ineq(thing);
return thing;
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 645c72ccb..e974a199b 100644
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -22,6 +22,7 @@ Revision History:
#include <assert.h>
+#include <vector>
#include "iz3hash.h"
#include"well_sorted.h"
@@ -262,6 +263,7 @@ class iz3mgr {
default:;
}
assert(0);
+ return 0;
}
ast arg(const ast &t, int i){
@@ -606,9 +608,9 @@ class iz3mgr {
return d;
}
- void linear_comb(ast &P, const ast &c, const ast &Q);
+ void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false);
- ast sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs);
+ ast sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs, bool round_off = false);
ast simplify_ineq(const ast &ineq){
ast res = make(op(ineq),arg(ineq,0),z3_simplify(arg(ineq,1)));
diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp
index df6fcaf53..31b375c0f 100644
--- a/src/interp/iz3pp.cpp
+++ b/src/interp/iz3pp.cpp
@@ -58,20 +58,20 @@ namespace stl_ext {
class free_func_visitor {
ast_manager& m;
func_decl_set m_funcs;
- obj_hashtable<sort> m_sorts;
+ obj_hashtable<class sort> m_sorts;
public:
free_func_visitor(ast_manager& m): m(m) {}
void operator()(var * n) { }
void operator()(app * n) {
m_funcs.insert(n->get_decl());
- sort* s = m.get_sort(n);
+ class sort* s = m.get_sort(n);
if (s->get_family_id() == null_family_id) {
m_sorts.insert(s);
}
}
void operator()(quantifier * n) { }
func_decl_set& funcs() { return m_funcs; }
- obj_hashtable<sort>& sorts() { return m_sorts; }
+ obj_hashtable<class sort>& sorts() { return m_sorts; }
};
class iz3pp_helper : public iz3mgr {
@@ -146,8 +146,8 @@ void iz3pp(ast_manager &m,
func_decl_set &funcs = visitor.funcs();
func_decl_set::iterator it = funcs.begin(), end = funcs.end();
- obj_hashtable<sort>& sorts = visitor.sorts();
- obj_hashtable<sort>::iterator sit = sorts.begin(), send = sorts.end();
+ obj_hashtable<class sort>& sorts = visitor.sorts();
+ obj_hashtable<class sort>::iterator sit = sorts.begin(), send = sorts.end();
diff --git a/src/interp/iz3profiling.cpp b/src/interp/iz3profiling.cpp
index 262254271..2c4a31d58 100755
--- a/src/interp/iz3profiling.cpp
+++ b/src/interp/iz3profiling.cpp
@@ -17,6 +17,13 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
#include "iz3profiling.h"
#include <map>
diff --git a/src/interp/iz3proof.cpp b/src/interp/iz3proof.cpp
index 968a4b25a..3fefea73f 100755
--- a/src/interp/iz3proof.cpp
+++ b/src/interp/iz3proof.cpp
@@ -18,6 +18,12 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
#include "iz3proof.h"
#include "iz3profiling.h"
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index 75d14bca1..61ed78463 100644
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -17,6 +17,13 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
#include "iz3proof_itp.h"
#ifndef WIN32
@@ -2170,7 +2177,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
for(unsigned i = 0; i < prem_cons.size(); i++){
const ast &lit = prem_cons[i];
if(get_term_type(lit) == LitA)
- linear_comb(thing,coeffs[i],lit);
+ // Farkas rule seems to assume strict integer inequalities are rounded
+ linear_comb(thing,coeffs[i],lit,true /*round_off*/);
}
thing = simplify_ineq(thing);
for(unsigned i = 0; i < prem_cons.size(); i++){
@@ -2195,9 +2203,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
/** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */
- void linear_comb(ast &P, const ast &c, const ast &Q){
+ void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false){
ast Qrhs;
- bool strict = op(P) == Lt;
+ bool qstrict = false;
if(is_not(Q)){
ast nQ = arg(Q,0);
switch(op(nQ)){
@@ -2209,11 +2217,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
break;
case Geq:
Qrhs = make(Sub,arg(nQ,1),arg(nQ,0));
- strict = true;
+ qstrict = true;
break;
case Leq:
Qrhs = make(Sub,arg(nQ,0),arg(nQ,1));
- strict = true;
+ qstrict = true;
break;
default:
throw proof_error();
@@ -2229,17 +2237,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
break;
case Lt:
Qrhs = make(Sub,arg(Q,1),arg(Q,0));
- strict = true;
+ qstrict = true;
break;
case Gt:
Qrhs = make(Sub,arg(Q,0),arg(Q,1));
- strict = true;
+ qstrict = true;
break;
default:
throw proof_error();
}
}
Qrhs = make(Times,c,Qrhs);
+ bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
+ if(pstrict && qstrict && round_off)
+ Qrhs = make(Sub,Qrhs,make_int(rational(1)));
if(strict)
P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
else
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index fae914292..6a1b665cf 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -17,6 +17,13 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
#include "iz3translate.h"
#include "iz3proof.h"
#include "iz3profiling.h"
@@ -1079,7 +1086,7 @@ public:
my_cons.push_back(mk_not(arg(con,i)));
my_coeffs.push_back(farkas_coeffs[i]);
}
- ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons));
+ ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */));
my_cons.push_back(mk_not(farkas_con));
my_coeffs.push_back(make_int("1"));
std::vector<Iproof::node> my_hyps;
@@ -1103,7 +1110,7 @@ public:
my_cons.push_back(conc(prem(proof,i-1)));
my_coeffs.push_back(farkas_coeffs[i]);
}
- ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons));
+ ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */));
std::vector<Iproof::node> my_hyps;
for(int i = 1; i < nargs; i++)
my_hyps.push_back(prems[i-1]);
@@ -1642,6 +1649,10 @@ public:
res = iproof->make_axiom(lits);
break;
}
+ case PR_IFF_TRUE: { // turns p into p <-> true, noop for us
+ res = args[0];
+ break;
+ }
default:
assert(0 && "translate_main: unsupported proof rule");
throw unsupported();
diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index 4b7d47e0f..a85c9a1c5 100755
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -20,6 +20,14 @@ Revision History:
--*/
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#pragma warning(disable:4390)
+#endif
+
#include "iz3translate.h"
#include "iz3proof.h"
#include "iz3profiling.h"
@@ -58,7 +66,9 @@ namespace stl_ext {
static int lemma_count = 0;
+#if 0
static int nll_lemma_count = 0;
+#endif
#define SHOW_LEMMA_COUNT -1
// One half of a resolution. We need this to distinguish
diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h
index 974aa7cfb..f7125588e 100644
--- a/src/math/simplex/simplex.h
+++ b/src/math/simplex/simplex.h
@@ -97,6 +97,7 @@ namespace simplex {
unsigned m_blands_rule_threshold;
random_gen m_random;
uint_set m_left_basis;
+ unsigned m_infeasible_var;
public:
simplex():
@@ -111,7 +112,8 @@ namespace simplex {
typedef typename matrix::col_iterator col_iterator;
void ensure_var(var_t v);
- row add_row(unsigned num_vars, var_t base, var_t const* vars, numeral const* coeffs);
+ row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
+ row get_infeasible_row();
void del_row(row const& r);
void set_lower(var_t var, eps_numeral const& b);
void set_upper(var_t var, eps_numeral const& b);
@@ -125,6 +127,9 @@ namespace simplex {
eps_numeral const& get_value(var_t v);
void display(std::ostream& out) const;
+ unsigned get_num_vars() const { return m_vars.size(); }
+
+
private:
var_t select_var_to_fix();
@@ -159,10 +164,11 @@ namespace simplex {
bool outside_bounds(var_t v) const { return below_lower(v) || above_upper(v); }
bool is_free(var_t v) const { return !m_vars[v].m_lower_valid && !m_vars[v].m_upper_valid; }
bool is_non_free(var_t v) const { return !is_free(v); }
- unsigned get_num_vars() const { return m_vars.size(); }
bool is_base(var_t x) const { return m_vars[x].m_is_base; }
+ void add_patch(var_t v);
bool well_formed() const;
+ bool well_formed_row(row const& r) const;
bool is_feasible() const;
};
diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index 46915695f..b08d4d0ff 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -24,19 +24,27 @@ namespace simplex {
template<typename Ext>
typename simplex<Ext>::row
simplex<Ext>::add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
- DEBUG_CODE(
- bool found = false;
- for (unsigned i = 0; !found && i < num_vars; ++i) found = vars[i] == base;
- SASSERT(found);
- );
scoped_numeral base_coeff(m);
+ scoped_eps_numeral value(em), tmp(em);
row r = M.mk_row();
for (unsigned i = 0; i < num_vars; ++i) {
- M.add(r, coeffs[i], vars[i]);
- if (vars[i] == base) {
- m.set(base_coeff, coeffs[i]);
+ if (!m.is_zero(coeffs[i])) {
+ var_t v = vars[i];
+ M.add_var(r, coeffs[i], v);
+ if (v == base) {
+ m.set(base_coeff, coeffs[i]);
+ }
+ else {
+ SASSERT(!is_base(v));
+ em.mul(m_vars[v].m_value, coeffs[i], tmp);
+ em.add(value, tmp, value);
+ }
}
}
+ em.neg(value);
+ em.div(value, base_coeff, value);
+ SASSERT(!m.is_zero(base_coeff));
+ SASSERT(!is_base(base));
while (m_row2base.size() <= r.id()) {
m_row2base.push_back(null_var);
}
@@ -44,9 +52,28 @@ namespace simplex {
m_vars[base].m_base2row = r.id();
m_vars[base].m_is_base = true;
m.set(m_vars[base].m_base_coeff, base_coeff);
+ em.set(m_vars[base].m_value, value);
+ add_patch(base);
+ SASSERT(well_formed_row(r));
return r;
}
+ template<typename Ext>
+ typename simplex<Ext>::row
+ simplex<Ext>::get_infeasible_row() {
+ SASSERT(is_base(m_infeasible_var));
+ unsigned row_id = m_vars[m_infeasible_var].m_base2row;
+ return row(row_id);
+ }
+
+ template<typename Ext>
+ void simplex<Ext>::add_patch(var_t v) {
+ SASSERT(is_base(v));
+ if (outside_bounds(v)) {
+ m_to_patch.insert(v);
+ }
+ }
+
template<typename Ext>
void simplex<Ext>::del_row(row const& r) {
m_vars[m_row2base[r.id()]].m_is_base = false;
@@ -114,8 +141,12 @@ namespace simplex {
if (vi.m_lower_valid) out << em.to_string(vi.m_lower); else out << "-oo";
out << ":";
if (vi.m_upper_valid) out << em.to_string(vi.m_upper); else out << "oo";
- out << "]";
- if (vi.m_is_base) out << " b:" << vi.m_base2row;
+ out << "] ";
+ if (vi.m_is_base) out << "b:" << vi.m_base2row << " ";
+ //col_iterator it = M.col_begin(i), end = M.col_end(i);
+ //for (; it != end; ++it) {
+ // out << "r" << it.get_row().id() << " ";
+ //}
out << "\n";
}
}
@@ -131,20 +162,23 @@ namespace simplex {
template<typename Ext>
lbool simplex<Ext>::make_feasible() {
m_left_basis.reset();
+ m_infeasible_var = null_var;
unsigned num_iterations = 0;
unsigned num_repeated = 0;
var_t v = null_var;
+ SASSERT(well_formed());
while ((v = select_var_to_fix()) != null_var) {
if (m_cancel || num_iterations > m_max_iterations) {
return l_undef;
}
check_blands_rule(v, num_repeated);
if (!make_var_feasible(v)) {
+ m_infeasible_var = v;
return l_false;
}
++num_iterations;
- SASSERT(well_formed());
}
+ SASSERT(well_formed());
return l_true;
}
@@ -188,18 +222,18 @@ namespace simplex {
m.set(x_jI.m_base_coeff, a_ij);
x_jI.m_is_base = true;
x_iI.m_is_base = false;
- if (outside_bounds(x_j)) {
- m_to_patch.insert(x_j);
- }
+ add_patch(x_j);
+ SASSERT(well_formed_row(row(r_i)));
+
col_iterator it = M.col_begin(x_j), end = M.col_end(x_j);
scoped_numeral a_kj(m), g(m);
for (; it != end; ++it) {
row r_k = it.get_row();
- if (r_k != r_i) {
+ if (r_k.id() != r_i) {
a_kj = it.get_row_entry().m_coeff;
a_kj.neg();
M.mul(r_k, a_ij);
- M.add(r_k, a_kj, r_i);
+ M.add(r_k, a_kj, row(r_i));
var_t s = m_row2base[r_k.id()];
numeral& coeff = m_vars[s].m_base_coeff;
m.mul(coeff, a_ij, coeff);
@@ -207,6 +241,7 @@ namespace simplex {
if (!m.is_one(g)) {
m.div(coeff, g, coeff);
}
+ SASSERT(well_formed_row(row(r_k)));
}
}
}
@@ -240,8 +275,8 @@ namespace simplex {
void simplex<Ext>::update_value_core(var_t v, eps_numeral const& delta) {
eps_numeral& val = m_vars[v].m_value;
em.add(val, delta, val);
- if (is_base(v) && outside_bounds(v)) {
- m_to_patch.insert(v);
+ if (is_base(v)) {
+ add_patch(v);
}
}
@@ -499,6 +534,7 @@ namespace simplex {
pivot(x_i, x_j, a_ij);
move_to_bound(x_i, inc == m.is_pos(a_ij));
+ SASSERT(well_formed_row(row(m_vars[x_j].m_base2row)));
}
return l_true;
}
@@ -705,18 +741,7 @@ namespace simplex {
var_t s = m_row2base[i];
if (s == null_var) continue;
SASSERT(i == m_vars[s].m_base2row);
- //
- // TBD: extract coefficient of base variable and compare
- // with m_vars[s].m_base_coeff;
- //
- // check that sum of assignments add up to 0 for every row.
- row_iterator it = M.row_begin(row(i)), end = M.row_end(row(i));
- scoped_eps_numeral sum(em), tmp(em);
- for (; it != end; ++it) {
- em.mul(m_vars[it->m_var].m_value, it->m_coeff, tmp);
- sum += tmp;
- }
- SASSERT(em.is_zero(sum));
+ SASSERT(well_formed_row(row(i)));
}
return true;
}
@@ -729,6 +754,25 @@ namespace simplex {
return true;
}
+ template<typename Ext>
+ bool simplex<Ext>::well_formed_row(row const& r) const {
+
+ //
+ // TBD: extract coefficient of base variable and compare
+ // with m_vars[s].m_base_coeff;
+ //
+ // check that sum of assignments add up to 0 for every row.
+ row_iterator it = M.row_begin(r), end = M.row_end(r);
+ scoped_eps_numeral sum(em), tmp(em);
+ for (; it != end; ++it) {
+ em.mul(m_vars[it->m_var].m_value, it->m_coeff, tmp);
+ sum += tmp;
+ }
+ SASSERT(em.is_zero(sum));
+
+ return true;
+ }
+
};
#endif
diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h
index 6a85d69f0..d16d1d1cf 100644
--- a/src/math/simplex/sparse_matrix.h
+++ b/src/math/simplex/sparse_matrix.h
@@ -92,8 +92,7 @@ namespace simplex {
void del_row_entry(unsigned idx);
void compress(manager& m, vector<column> & cols);
void compress_if_needed(manager& m, vector<column> & cols);
- void save_var_pos(svector<int> & result_map) const;
- void reset_var_pos(svector<int> & result_map) const;
+ void save_var_pos(svector<int> & result_map, unsigned_vector& idxs) const;
bool is_coeff_of(var_t v, numeral const & expected) const;
int get_idx_of(var_t v) const;
};
@@ -125,6 +124,7 @@ namespace simplex {
svector<unsigned> m_dead_rows; // rows to recycle
vector<column> m_columns; // per var
svector<int> m_var_pos; // temporary map from variables to positions in row
+ unsigned_vector m_var_pos_idx; // indices in m_var_pos
bool well_formed_row(unsigned row_id) const;
bool well_formed_column(unsigned column_id) const;
@@ -138,7 +138,7 @@ namespace simplex {
class row {
unsigned m_id;
public:
- row(unsigned r):m_id(r) {}
+ explicit row(unsigned r):m_id(r) {}
row():m_id(UINT_MAX) {}
bool operator!=(row const& other) const {
return m_id != other.m_id;
@@ -149,7 +149,7 @@ namespace simplex {
void ensure_var(var_t v);
row mk_row();
- void add(row r, numeral const& n, var_t var);
+ void add_var(row r, numeral const& n, var_t var);
void add(row r, numeral const& n, row src);
void mul(row r, numeral const& n);
void neg(row r);
diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h
index 20e9d676f..a170ee47f 100644
--- a/src/math/simplex/sparse_matrix_def.h
+++ b/src/math/simplex/sparse_matrix_def.h
@@ -134,31 +134,18 @@ namespace simplex {
\brief Fill the map var -> pos/idx
*/
template<typename Ext>
- inline void sparse_matrix<Ext>::_row::save_var_pos(svector<int> & result_map) const {
+ inline void sparse_matrix<Ext>::_row::save_var_pos(svector<int> & result_map, unsigned_vector& idxs) const {
typename vector<_row_entry>::const_iterator it = m_entries.begin();
typename vector<_row_entry>::const_iterator end = m_entries.end();
unsigned idx = 0;
for (; it != end; ++it, ++idx) {
if (!it->is_dead()) {
result_map[it->m_var] = idx;
+ idxs.push_back(it->m_var);
}
}
}
- /**
- \brief Reset the map var -> pos/idx. That is for all variables v in the row, set result[v] = -1
- This method can be viewed as the "inverse" of save_var_pos.
- */
- template<typename Ext>
- inline void sparse_matrix<Ext>::_row::reset_var_pos(svector<int> & result_map) const {
- typename vector<_row_entry>::const_iterator it = m_entries.begin();
- typename vector<_row_entry>::const_iterator end = m_entries.end();
- for (; it != end; ++it) {
- if (!it->is_dead()) {
- result_map[it->m_var] = -1;
- }
- }
- }
template<typename Ext>
int sparse_matrix<Ext>::_row::get_idx_of(var_t v) const {
@@ -316,7 +303,7 @@ namespace simplex {
}
template<typename Ext>
- void sparse_matrix<Ext>::add(row dst, numeral const& n, var_t v) {
+ void sparse_matrix<Ext>::add_var(row dst, numeral const& n, var_t v) {
_row& r = m_rows[dst.id()];
column& c = m_columns[v];
unsigned r_idx;
@@ -339,7 +326,7 @@ namespace simplex {
_row & r1 = m_rows[row1.id()];
_row & r2 = m_rows[row2.id()];
- r1.save_var_pos(m_var_pos);
+ r1.save_var_pos(m_var_pos, m_var_pos_idx);
//
// loop over variables in row2,
@@ -376,7 +363,6 @@ namespace simplex {
} \
} \
} \
-
((void) 0)
if (m.is_one(n)) {
@@ -394,7 +380,11 @@ namespace simplex {
m.add(r_entry.m_coeff, tmp, r_entry.m_coeff));
}
- r1.reset_var_pos(m_var_pos);
+ // reset m_var_pos:
+ for (unsigned i = 0; i < m_var_pos_idx.size(); ++i) {
+ m_var_pos[m_var_pos_idx[i]] = -1;
+ }
+ m_var_pos_idx.reset();
r1.compress_if_needed(m, m_columns);
}
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 12dd4ff3e..248aca163 100644
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -35,10 +35,15 @@ Revision History:
#include "model_smt2_pp.h"
#include "model_v2_pp.h"
#include "fixedpoint_params.hpp"
-#include "scoped_proof.h"
// template class symbol_table<family_id>;
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
#include "duality.h"
#include "duality_profiling.h"
@@ -213,6 +218,9 @@ lbool dl_interface::query(::expr * query) {
catch (Duality::solver::cancel_exception &exn){
throw default_exception("duality canceled");
}
+ catch (Duality::Solver::Incompleteness &exn){
+ throw default_exception("incompleteness");
+ }
// profile!
diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp
index def6f8be3..37d4501f7 100644
--- a/src/test/simplex.cpp
+++ b/src/test/simplex.cpp
@@ -3,11 +3,130 @@
#include "simplex.h"
#include "simplex_def.h"
#include "mpq_inf.h"
+#include "vector.h"
+#include "rational.h"
+#define R rational
typedef simplex::simplex<simplex::mpz_ext> Simplex;
+typedef simplex::sparse_matrix<simplex::mpz_ext> sparse_matrix;
+
+static vector<R> vec(int i, int j) {
+ vector<R> nv;
+ nv.resize(2);
+ nv[0] = R(i);
+ nv[1] = R(j);
+ return nv;
+}
+
+static vector<R> vec(int i, int j, int k) {
+ vector<R> nv = vec(i, j);
+ nv.push_back(R(k));
+ return nv;
+}
+
+static vector<R> vec(int i, int j, int k, int l) {
+ vector<R> nv = vec(i, j, k);
+ nv.push_back(R(l));
+ return nv;
+}
+
+static vector<R> vec(int i, int j, int k, int l, int x) {
+ vector<R> nv = vec(i, j, k, l);
+ nv.push_back(R(x));
+ return nv;
+}
+
+static vector<R> vec(int i, int j, int k, int l, int x, int y) {
+ vector<R> nv = vec(i, j, k, l, x);
+ nv.push_back(R(y));
+ return nv;
+}
+
+static vector<R> vec(int i, int j, int k, int l, int x, int y, int z) {
+ vector<R> nv = vec(i, j, k, l, x, y);
+ nv.push_back(R(z));
+ return nv;
+}
+
+
+
+void add_row(Simplex& S, vector<R> const& _v, R const& _b, bool is_eq = false) {
+ unsynch_mpz_manager m;
+ unsigned_vector vars;
+ vector<R> v(_v);
+ R b(_b);
+ R l(denominator(b));
+ scoped_mpz_vector coeffs(m);
+ for (unsigned i = 0; i < v.size(); ++i) {
+ l = lcm(l, denominator(v[i]));
+ vars.push_back(i);
+ S.ensure_var(i);
+ }
+ b *= l;
+ b.neg();
+ for (unsigned i = 0; i < v.size(); ++i) {
+ v[i] *= l;
+ coeffs.push_back(v[i].to_mpq().numerator());
+ }
+ unsigned nv = S.get_num_vars();
+ vars.push_back(nv);
+ vars.push_back(nv+1);
+ S.ensure_var(nv);
+ S.ensure_var(nv+1);
+ coeffs.push_back(mpz(-1));
+ coeffs.push_back(b.to_mpq().numerator());
+ mpq_inf one(mpq(1),mpq(0));
+ mpq_inf zero(mpq(0),mpq(0));
+ SASSERT(vars.size() == coeffs.size());
+ S.set_lower(nv, zero);
+ if (is_eq) S.set_upper(nv, zero);
+ S.set_lower(nv+1, one);
+ S.set_upper(nv+1, one);
+ S.add_row(nv, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
+}
+
+static void feas(Simplex& S) {
+ S.display(std::cout);
+ lbool is_sat = S.make_feasible();
+ std::cout << "feasible: " << is_sat << "\n";
+ S.display(std::cout);
+}
+
+static void test1() {
+ Simplex S;
+ add_row(S, vec(1,0), R(1));
+ add_row(S, vec(0,1), R(1));
+ add_row(S, vec(1,1), R(1));
+ feas(S);
+}
+
+static void test2() {
+ Simplex S;
+ add_row(S, vec(1, 0), R(1));
+ add_row(S, vec(0, 1), R(1));
+ add_row(S, vec(1, 1), R(1), true);
+ feas(S);
+}
+
+static void test3() {
+ Simplex S;
+ add_row(S, vec(-1, 0), R(-1));
+ add_row(S, vec(0, -1), R(-1));
+ add_row(S, vec(1, 1), R(1), true);
+ feas(S);
+}
+
+static void test4() {
+ Simplex S;
+ add_row(S, vec(1, 0), R(1));
+ add_row(S, vec(0, -1), R(-1));
+ add_row(S, vec(1, 1), R(1), true);
+ feas(S);
+}
+
+
void tst_simplex() {
- simplex::sparse_matrix<simplex::mpz_ext> M;
Simplex S;
std::cout << "simplex\n";
@@ -37,4 +156,9 @@ void tst_simplex() {
is_sat = S.make_feasible();
std::cout << "feasible: " << is_sat << "\n";
S.display(std::cout);
+
+ test1();
+ test2();
+ test3();
+ test4();
}