mirror of
https://github.com/Z3Prover/z3
synced 2025-04-25 01:55:32 +00:00
Tabs, formatting.
This commit is contained in:
Christoph M. Wintersteiger
parent
8871cb120a
commit
00651f8f21
63 changed files with 715 additions and 717 deletions
|
|
@ -21,6 +21,7 @@
|
|||
#pragma once
|
||||
|
||||
#include "duality/duality_wrapper.h"
|
||||
#include <vector>
|
||||
#include <list>
|
||||
#include <map>
|
||||
|
||||
|
|
@ -41,9 +42,9 @@ namespace Duality {
|
|||
typedef expr Term;
|
||||
|
||||
Z3User(context &_ctx) : ctx(_ctx){}
|
||||
|
||||
|
||||
const char *string_of_int(int n);
|
||||
|
||||
|
||||
Term conjoin(const std::vector<Term> &args);
|
||||
|
||||
Term sum(const std::vector<Term> &args);
|
||||
|
|
@ -130,58 +131,58 @@ namespace Duality {
|
|||
|
||||
/** This class represents a relation post-fixed point (RPFP) problem as
|
||||
* a "problem graph". The graph consists of Nodes and hyper-edges.
|
||||
*
|
||||
*
|
||||
* A node consists of
|
||||
* - Annotation, a symbolic relation
|
||||
* - Bound, a symbolic relation giving an upper bound on Annotation
|
||||
*
|
||||
*
|
||||
*
|
||||
* A hyper-edge consists of:
|
||||
* - Children, a sequence of children Nodes,
|
||||
* - F, a symbolic relational transformer,
|
||||
* - Parent, a single parent Node.
|
||||
*
|
||||
*
|
||||
* The graph is "solved" when:
|
||||
* - For every Node n, n.Annotation subseteq n.Bound
|
||||
* - For every hyperedge e, e.F(e.Children.Annotation) subseteq e.Parent.Annotation
|
||||
*
|
||||
*
|
||||
* where, if x is a sequence of Nodes, x.Annotation is the sequences
|
||||
* of Annotations of the nodes in the sequence.
|
||||
*
|
||||
*
|
||||
* A symbolic Transformer consists of
|
||||
* - RelParams, a sequence of relational symbols
|
||||
* - IndParams, a sequence of individual symbols
|
||||
* - Formula, a formula over RelParams and IndParams
|
||||
*
|
||||
*
|
||||
* A Transformer t represents a function that takes sequence R of relations
|
||||
* and yields the relation lambda (t.Indparams). Formula(R/RelParams).
|
||||
*
|
||||
*
|
||||
* As a special case, a nullary Transformer (where RelParams is the empty sequence)
|
||||
* represents a fixed relation.
|
||||
*
|
||||
*
|
||||
* An RPFP consists of
|
||||
* - Nodes, a set of Nodes
|
||||
* - Edges, a set of hyper-edges
|
||||
* - Context, a prover context that contains formula AST's
|
||||
*
|
||||
*
|
||||
* Multiple RPFP's can use the same Context, but you should be careful
|
||||
* that only one RPFP asserts constraints in the context at any time.
|
||||
*
|
||||
* that only one RPFP asserts constraints in the context at any time.
|
||||
*
|
||||
* */
|
||||
class RPFP : public Z3User
|
||||
{
|
||||
public:
|
||||
|
||||
|
||||
class Edge;
|
||||
class Node;
|
||||
bool HornClauses;
|
||||
|
||||
|
||||
|
||||
/** Interface class for interpolating solver. */
|
||||
|
||||
class LogicSolver {
|
||||
public:
|
||||
|
||||
|
||||
context *ctx; /** Z3 context for formulas */
|
||||
solver *slvr; /** Z3 solver */
|
||||
bool need_goals; /** Can the solver use the goal tree to optimize interpolants? */
|
||||
|
|
@ -191,7 +192,7 @@ namespace Duality {
|
|||
"assumptions" are currently asserted in the solver. The return
|
||||
value indicates whether the assertions are satisfiable. In the
|
||||
UNSAT case, a tree interpolant is returned in "interpolants".
|
||||
In the SAT case, a model is returned.
|
||||
In the SAT case, a model is returned.
|
||||
*/
|
||||
|
||||
virtual
|
||||
|
|
@ -201,7 +202,7 @@ namespace Duality {
|
|||
TermTree *goals = 0,
|
||||
bool weak = false
|
||||
) = 0;
|
||||
|
||||
|
||||
/** Declare a constant in the background theory. */
|
||||
virtual void declare_constant(const func_decl &f) = 0;
|
||||
|
||||
|
|
@ -319,7 +320,7 @@ namespace Duality {
|
|||
virtual void declare_constant(const func_decl &f){
|
||||
bckg.insert(f);
|
||||
}
|
||||
|
||||
|
||||
/** Is this a background constant? */
|
||||
virtual bool is_constant(const func_decl &f){
|
||||
return bckg.find(f) != bckg.end();
|
||||
|
|
@ -344,9 +345,9 @@ namespace Duality {
|
|||
static iZ3LogicSolver *CreateLogicSolver(config &_config){
|
||||
return new iZ3LogicSolver(_config);
|
||||
}
|
||||
#endif
|
||||
#endif
|
||||
|
||||
/** Create a logic solver from a low-level Z3 context.
|
||||
/** Create a logic solver from a low-level Z3 context.
|
||||
Only use this if you know what you're doing. */
|
||||
static iZ3LogicSolver *CreateLogicSolver(context c){
|
||||
return new iZ3LogicSolver(c);
|
||||
|
|
@ -357,7 +358,7 @@ namespace Duality {
|
|||
protected:
|
||||
int nodeCount;
|
||||
int edgeCount;
|
||||
|
||||
|
||||
class stack_entry
|
||||
{
|
||||
public:
|
||||
|
|
@ -365,8 +366,8 @@ namespace Duality {
|
|||
std::list<Node *> nodes;
|
||||
std::list<std::pair<Edge *,Term> > constraints;
|
||||
};
|
||||
|
||||
|
||||
|
||||
|
||||
public:
|
||||
model dualModel;
|
||||
protected:
|
||||
|
|
@ -375,14 +376,14 @@ namespace Duality {
|
|||
std::vector<Term> axioms; // only saved here for printing purposes
|
||||
solver &aux_solver;
|
||||
hash_set<ast> *proof_core;
|
||||
|
||||
|
||||
public:
|
||||
|
||||
/** Construct an RPFP graph with a given interpolating prover context. It is allowed to
|
||||
have multiple RPFP's use the same context, but you should never have teo RPFP's
|
||||
with the same conext asserting nodes or edges at the same time. Note, if you create
|
||||
axioms in one RPFP, them create a second RPFP with the same context, the second will
|
||||
inherit the axioms.
|
||||
inherit the axioms.
|
||||
*/
|
||||
|
||||
RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver)
|
||||
|
|
@ -396,7 +397,7 @@ namespace Duality {
|
|||
}
|
||||
|
||||
virtual ~RPFP();
|
||||
|
||||
|
||||
/** Symbolic representation of a relational transformer */
|
||||
class Transformer
|
||||
{
|
||||
|
|
@ -406,12 +407,12 @@ namespace Duality {
|
|||
Term Formula;
|
||||
RPFP *owner;
|
||||
hash_map<std::string,Term> labels;
|
||||
|
||||
|
||||
Transformer *Clone()
|
||||
{
|
||||
return new Transformer(*this);
|
||||
}
|
||||
|
||||
|
||||
void SetEmpty(){
|
||||
Formula = owner->ctx.bool_val(false);
|
||||
}
|
||||
|
|
@ -451,7 +452,7 @@ namespace Duality {
|
|||
void Complement(){
|
||||
Formula = !Formula;
|
||||
}
|
||||
|
||||
|
||||
void Simplify(){
|
||||
Formula = Formula.simplify();
|
||||
}
|
||||
|
|
@ -459,7 +460,7 @@ namespace Duality {
|
|||
Transformer(const std::vector<FuncDecl> &_RelParams, const std::vector<Term> &_IndParams, const Term &_Formula, RPFP *_owner)
|
||||
: RelParams(_RelParams), IndParams(_IndParams), Formula(_Formula) {owner = _owner;}
|
||||
};
|
||||
|
||||
|
||||
/** Create a symbolic transformer. */
|
||||
Transformer CreateTransformer(const std::vector<FuncDecl> &_RelParams, const std::vector<Term> &_IndParams, const Term &_Formula)
|
||||
{
|
||||
|
|
@ -469,13 +470,13 @@ namespace Duality {
|
|||
// t.labels = foo.Item2;
|
||||
return Transformer(_RelParams,_IndParams,_Formula,this);
|
||||
}
|
||||
|
||||
|
||||
/** Create a relation (nullary relational transformer) */
|
||||
Transformer CreateRelation(const std::vector<Term> &_IndParams, const Term &_Formula)
|
||||
{
|
||||
return CreateTransformer(std::vector<FuncDecl>(), _IndParams, _Formula);
|
||||
}
|
||||
|
||||
|
||||
/** A node in the RPFP graph */
|
||||
class Node
|
||||
{
|
||||
|
|
@ -491,17 +492,17 @@ namespace Duality {
|
|||
Term dual;
|
||||
Node *map;
|
||||
unsigned recursion_bound;
|
||||
|
||||
|
||||
Node(const FuncDecl &_Name, const Transformer &_Annotation, const Transformer &_Bound, const Transformer &_Underapprox, const Term &_dual, RPFP *_owner, int _number)
|
||||
: Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0; recursion_bound = UINT_MAX;}
|
||||
};
|
||||
|
||||
|
||||
/** Create a node in the graph. The input is a term R(v_1...v_n)
|
||||
* where R is an arbitrary relational symbol and v_1...v_n are
|
||||
* arbitary distinct variables. The names are only of mnemonic value,
|
||||
* however, the number and type of arguments determine the type
|
||||
* of the relation at this node. */
|
||||
|
||||
|
||||
Node *CreateNode(const Term &t)
|
||||
{
|
||||
std::vector<Term> _IndParams;
|
||||
|
|
@ -517,9 +518,9 @@ namespace Duality {
|
|||
nodes.push_back(n);
|
||||
return n;
|
||||
}
|
||||
|
||||
|
||||
/** Clone a node (can be from another graph). */
|
||||
|
||||
|
||||
Node *CloneNode(Node *old)
|
||||
{
|
||||
Node *n = new Node(old->Name,
|
||||
|
|
@ -534,7 +535,7 @@ namespace Duality {
|
|||
n->map = old;
|
||||
return n;
|
||||
}
|
||||
|
||||
|
||||
/** Delete a node. You can only do this if not connected to any edges.*/
|
||||
void DeleteNode(Node *node){
|
||||
if(node->Outgoing || !node->Incoming.empty())
|
||||
|
|
@ -549,7 +550,7 @@ namespace Duality {
|
|||
}
|
||||
|
||||
/** This class represents a hyper-edge in the RPFP graph */
|
||||
|
||||
|
||||
class Edge
|
||||
{
|
||||
public:
|
||||
|
|
@ -565,15 +566,15 @@ namespace Duality {
|
|||
Edge *map;
|
||||
Term labeled;
|
||||
std::vector<Term> constraints;
|
||||
|
||||
|
||||
Edge(Node *_Parent, const Transformer &_F, const std::vector<Node *> &_Children, RPFP *_owner, int _number)
|
||||
: F(_F), Parent(_Parent), Children(_Children), dual(expr(_owner->ctx)) {
|
||||
owner = _owner;
|
||||
number = _number;
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
|
||||
|
||||
/** Create a hyper-edge. */
|
||||
Edge *CreateEdge(Node *_Parent, const Transformer &_F, const std::vector<Node *> &_Children)
|
||||
{
|
||||
|
|
@ -584,8 +585,8 @@ namespace Duality {
|
|||
edges.push_back(e);
|
||||
return e;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
/** Delete a hyper-edge and unlink it from any nodes. */
|
||||
void DeleteEdge(Edge *edge){
|
||||
if(edge->Parent)
|
||||
|
|
@ -607,19 +608,19 @@ namespace Duality {
|
|||
}
|
||||
delete edge;
|
||||
}
|
||||
|
||||
|
||||
/** Create an edge that lower-bounds its parent. */
|
||||
Edge *CreateLowerBoundEdge(Node *_Parent)
|
||||
{
|
||||
return CreateEdge(_Parent, _Parent->Annotation, std::vector<Node *>());
|
||||
}
|
||||
|
||||
|
||||
|
||||
/** 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
|
||||
* the number of pushes we are inside. */
|
||||
|
||||
|
||||
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. */
|
||||
|
|
@ -629,19 +630,19 @@ namespace Duality {
|
|||
/** For incremental solving, asserts the negation of the upper bound associated
|
||||
* with a node.
|
||||
* */
|
||||
|
||||
|
||||
void AssertNode(Node *n);
|
||||
|
||||
/** Assert a constraint on an edge in the SMT context.
|
||||
/** Assert a constraint on an edge in the SMT context.
|
||||
*/
|
||||
void ConstrainEdge(Edge *e, const Term &t);
|
||||
|
||||
|
||||
/** Fix the truth values of atomic propositions in the given
|
||||
edge to their values in the current assignment. */
|
||||
void FixCurrentState(Edge *root);
|
||||
|
||||
|
||||
void FixCurrentStateFull(Edge *edge, const expr &extra);
|
||||
|
||||
|
||||
void FixCurrentStateFull(Edge *edge, const std::vector<expr> &assumps, const hash_map<ast,expr> &renaming);
|
||||
|
||||
/** Declare a constant in the background theory. */
|
||||
|
|
@ -660,78 +661,78 @@ namespace Duality {
|
|||
|
||||
#if 0
|
||||
/** Do not call this. */
|
||||
|
||||
|
||||
void RemoveAxiom(const Term &t);
|
||||
#endif
|
||||
|
||||
/** Solve an RPFP graph. This means either strengthen the annotation
|
||||
* so that the bound at the given root node is satisfied, or
|
||||
* show that this cannot be done by giving a dual solution
|
||||
* (i.e., a counterexample).
|
||||
*
|
||||
* show that this cannot be done by giving a dual solution
|
||||
* (i.e., a counterexample).
|
||||
*
|
||||
* In the current implementation, this only works for graphs that
|
||||
* are:
|
||||
* - tree-like
|
||||
*
|
||||
*
|
||||
* - closed.
|
||||
*
|
||||
*
|
||||
* In a tree-like graph, every nod has out most one incoming and one out-going edge,
|
||||
* and there are no cycles. In a closed graph, every node has exactly one out-going
|
||||
* edge. This means that the leaves of the tree are all hyper-edges with no
|
||||
* children. Such an edge represents a relation (nullary transformer) and thus
|
||||
* a lower bound on its parent. The parameter root must be the root of this tree.
|
||||
*
|
||||
*
|
||||
* If Solve returns LBool.False, this indicates success. The annotation of the tree
|
||||
* has been updated to satisfy the upper bound at the root.
|
||||
*
|
||||
* has been updated to satisfy the upper bound at the root.
|
||||
*
|
||||
* If Solve returns LBool.True, this indicates a counterexample. For each edge,
|
||||
* you can then call Eval to determine the values of symbols in the transformer formula.
|
||||
* You can also call Empty on a node to determine if its value in the counterexample
|
||||
* is the empty relation.
|
||||
*
|
||||
*
|
||||
* \param root The root of the tree
|
||||
* \param persist Number of context pops through which result should persist
|
||||
*
|
||||
*
|
||||
* \param persist Number of context pops through which result should persist
|
||||
*
|
||||
*
|
||||
*/
|
||||
|
||||
lbool Solve(Node *root, int persist);
|
||||
|
||||
|
||||
/** Same as Solve, but annotates only a single node. */
|
||||
|
||||
lbool SolveSingleNode(Node *root, Node *node);
|
||||
|
||||
/** Get the constraint tree (but don't solve it) */
|
||||
|
||||
|
||||
TermTree *GetConstraintTree(Node *root, Node *skip_descendant = 0);
|
||||
|
||||
|
||||
/** Dispose of the dual model (counterexample) if there is one. */
|
||||
|
||||
|
||||
void DisposeDualModel();
|
||||
|
||||
/** Check satisfiability of asserted edges and nodes. Same functionality as
|
||||
* Solve, except no primal solution (interpolant) is generated in the unsat case. */
|
||||
|
||||
check_result Check(Node *root, std::vector<Node *> underapproxes = std::vector<Node *>(),
|
||||
* Solve, except no primal solution (interpolant) is generated in the unsat case. */
|
||||
|
||||
check_result Check(Node *root, std::vector<Node *> underapproxes = std::vector<Node *>(),
|
||||
std::vector<Node *> *underapprox_core = 0);
|
||||
|
||||
/** Update the model, attempting to make the propositional literals in assumps true. If possible,
|
||||
return sat, else return unsat and keep the old model. */
|
||||
|
||||
|
||||
check_result CheckUpdateModel(Node *root, std::vector<expr> assumps);
|
||||
|
||||
/** Determines the value in the counterexample of a symbol occuring in the transformer formula of
|
||||
* a given edge. */
|
||||
|
||||
|
||||
Term Eval(Edge *e, Term t);
|
||||
|
||||
|
||||
/** Return the fact derived at node p in a counterexample. */
|
||||
|
||||
Term EvalNode(Node *p);
|
||||
|
||||
|
||||
/** 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. */
|
||||
|
||||
|
||||
bool Empty(Node *p);
|
||||
|
||||
/** Compute an underapproximation of every node in a tree rooted at "root",
|
||||
|
|
@ -747,11 +748,11 @@ namespace Duality {
|
|||
void InterpolateByCases(Node *root, Node *node);
|
||||
|
||||
/** Push a scope. Assertions made after Push can be undone by Pop. */
|
||||
|
||||
|
||||
void Push();
|
||||
|
||||
/** Exception thrown when bad clause is encountered */
|
||||
|
||||
|
||||
struct bad_clause {
|
||||
std::string msg;
|
||||
int i;
|
||||
|
|
@ -777,7 +778,7 @@ namespace Duality {
|
|||
// thrown on internal error
|
||||
struct Bad {
|
||||
};
|
||||
|
||||
|
||||
// thrown on more serious internal error
|
||||
struct ReallyBad {
|
||||
};
|
||||
|
|
@ -786,56 +787,56 @@ namespace Duality {
|
|||
struct greedy_reduce_failed {};
|
||||
|
||||
/** Pop a scope (see Push). Note, you cannot pop axioms. */
|
||||
|
||||
|
||||
void Pop(int num_scopes);
|
||||
|
||||
|
||||
/** Erase the proof by performing a Pop, Push and re-assertion of
|
||||
all the popped constraints */
|
||||
void PopPush();
|
||||
|
||||
/** Return true if the given edge is used in the proof of unsat.
|
||||
Can be called only after Solve or Check returns an unsat result. */
|
||||
|
||||
|
||||
bool EdgeUsedInProof(Edge *edge);
|
||||
|
||||
|
||||
/** Convert a collection of clauses to Nodes and Edges in the RPFP.
|
||||
|
||||
|
||||
Predicate unknowns are uninterpreted predicates not
|
||||
occurring in the background theory.
|
||||
|
||||
Clauses are of the form
|
||||
|
||||
|
||||
Clauses are of the form
|
||||
|
||||
B => P(t_1,...,t_k)
|
||||
|
||||
|
||||
where P is a predicate unknown and predicate unknowns
|
||||
occur only positivey in H and only under existential
|
||||
quantifiers in prenex form.
|
||||
|
||||
|
||||
Each predicate unknown maps to a node. Each clause maps to
|
||||
an edge. Let C be a clause B => P(t_1,...,t_k) where the
|
||||
sequence of predicate unknowns occurring in B (in order
|
||||
of occurrence) is P_1..P_n. The clause maps to a transformer
|
||||
T where:
|
||||
|
||||
|
||||
T.Relparams = P_1..P_n
|
||||
T.Indparams = x_1...x+k
|
||||
T.Formula = B /\ t_1 = x_1 /\ ... /\ t_k = x_k
|
||||
|
||||
|
||||
Throws exception bad_clause(msg,i) if a clause i is
|
||||
in the wrong form.
|
||||
|
||||
|
||||
*/
|
||||
|
||||
|
||||
struct label_struct {
|
||||
symbol name;
|
||||
expr value;
|
||||
bool pos;
|
||||
label_struct(const symbol &s, const expr &e, bool b)
|
||||
: name(s), value(e), pos(b) {}
|
||||
label_struct(const symbol &s, const expr &e, bool b)
|
||||
: name(s), value(e), pos(b) {}
|
||||
};
|
||||
|
||||
|
||||
|
||||
#ifdef _WINDOWS
|
||||
__declspec(dllexport)
|
||||
#endif
|
||||
|
|
@ -847,7 +848,7 @@ namespace Duality {
|
|||
|
||||
void WriteCounterexample(std::ostream &s, Node *node);
|
||||
|
||||
enum FileFormat {DualityFormat, SMT2Format, HornFormat};
|
||||
enum FileFormat {DualityFormat, SMT2Format, HornFormat};
|
||||
|
||||
/** Write the RPFP to a file (currently in SMTLIB 1.2 format) */
|
||||
void WriteProblemToFile(std::string filename, FileFormat format = DualityFormat);
|
||||
|
|
@ -870,9 +871,9 @@ namespace Duality {
|
|||
/** 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_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))
|
||||
*/
|
||||
|
||||
|
|
@ -921,7 +922,7 @@ namespace Duality {
|
|||
}
|
||||
|
||||
protected:
|
||||
|
||||
|
||||
void ClearProofCore(){
|
||||
if(proof_core)
|
||||
delete proof_core;
|
||||
|
|
@ -929,7 +930,7 @@ namespace Duality {
|
|||
}
|
||||
|
||||
Term SuffixVariable(const Term &t, int n);
|
||||
|
||||
|
||||
Term HideVariable(const Term &t, int n);
|
||||
|
||||
void RedVars(Node *node, Term &b, std::vector<Term> &v);
|
||||
|
|
@ -958,16 +959,16 @@ namespace Duality {
|
|||
|
||||
#if 0
|
||||
void WriteInterps(System.IO.StreamWriter f, TermTree t);
|
||||
#endif
|
||||
#endif
|
||||
|
||||
void WriteEdgeVars(Edge *e, hash_map<ast,int> &memo, const Term &t, std::ostream &s);
|
||||
|
||||
void WriteEdgeAssignment(std::ostream &s, Edge *e);
|
||||
|
||||
|
||||
|
||||
// Scan the clause body for occurrences of the predicate unknowns
|
||||
|
||||
Term ScanBody(hash_map<ast,Term> &memo,
|
||||
|
||||
Term ScanBody(hash_map<ast,Term> &memo,
|
||||
const Term &t,
|
||||
hash_map<func_decl,Node *> &pmap,
|
||||
std::vector<func_decl> &res,
|
||||
|
|
@ -1035,7 +1036,7 @@ namespace Duality {
|
|||
void ConstrainEdgeLocalized(Edge *e, const Term &t);
|
||||
|
||||
void GreedyReduce(solver &s, std::vector<expr> &conjuncts);
|
||||
|
||||
|
||||
void NegateLits(std::vector<expr> &lits);
|
||||
|
||||
expr SimplifyOr(std::vector<expr> &lits);
|
||||
|
|
@ -1053,7 +1054,7 @@ namespace Duality {
|
|||
void GetGroundLitsUnderQuants(hash_set<ast> *memo, const Term &f, std::vector<Term> &res, int under);
|
||||
|
||||
Term StrengthenFormulaByCaseSplitting(const Term &f, std::vector<expr> &case_lits);
|
||||
|
||||
|
||||
expr NegateLit(const expr &f);
|
||||
|
||||
expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox);
|
||||
|
|
@ -1065,7 +1066,7 @@ namespace Duality {
|
|||
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);
|
||||
|
|
@ -1081,7 +1082,7 @@ namespace Duality {
|
|||
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);
|
||||
|
|
@ -1089,11 +1090,11 @@ namespace Duality {
|
|||
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,
|
||||
|
|
@ -1105,14 +1106,14 @@ namespace Duality {
|
|||
virtual bool proof_core_contains(const expr &e);
|
||||
|
||||
};
|
||||
|
||||
|
||||
|
||||
/** RPFP solver base class. */
|
||||
|
||||
class Solver {
|
||||
|
||||
|
||||
public:
|
||||
|
||||
|
||||
class Counterexample {
|
||||
private:
|
||||
RPFP *tree;
|
||||
|
|
@ -1148,18 +1149,18 @@ namespace Duality {
|
|||
Counterexample &operator=(const Counterexample &);
|
||||
Counterexample(const Counterexample &);
|
||||
};
|
||||
|
||||
|
||||
/** Solve the problem. You can optionally give an old
|
||||
counterexample to use as a guide. This is chiefly useful for
|
||||
abstraction refinement metholdologies, and is only used as a
|
||||
heuristic. */
|
||||
|
||||
|
||||
virtual bool Solve() = 0;
|
||||
|
||||
|
||||
virtual Counterexample &GetCounterexample() = 0;
|
||||
|
||||
|
||||
virtual bool SetOption(const std::string &option, const std::string &value) = 0;
|
||||
|
||||
|
||||
/** Learn heuristic information from another solver. This
|
||||
is chiefly useful for abstraction refinement, when we want to
|
||||
solve a series of similar problems. */
|
||||
|
|
@ -1184,7 +1185,7 @@ namespace Duality {
|
|||
|
||||
/** Object thrown on cancellation */
|
||||
struct Canceled {};
|
||||
|
||||
|
||||
/** Object thrown on incompleteness */
|
||||
struct Incompleteness {};
|
||||
};
|
||||
|
|
@ -1235,16 +1236,16 @@ namespace Duality {
|
|||
public:
|
||||
|
||||
/** appends assumption literals for edge to lits. if with_children is true,
|
||||
includes that annotation of the edge's children.
|
||||
*/
|
||||
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);
|
||||
|
||||
|
|
@ -1287,7 +1288,7 @@ namespace Duality {
|
|||
uptr<solver> slvr;
|
||||
};
|
||||
hash_map<Edge *, edge_solver > edge_solvers;
|
||||
|
||||
|
||||
#ifdef LIMIT_STACK_WEIGHT
|
||||
struct weight_counter {
|
||||
int val;
|
||||
|
|
@ -1296,7 +1297,7 @@ namespace Duality {
|
|||
std::swap(val,other.val);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
struct big_stack_entry {
|
||||
weight_counter weight_added;
|
||||
std::vector<expr> new_alits;
|
||||
|
|
@ -1319,11 +1320,11 @@ namespace Duality {
|
|||
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,
|
||||
|
|
@ -1348,7 +1349,7 @@ namespace Duality {
|
|||
scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false, bool axioms = false){
|
||||
rpfp = _rpfp;
|
||||
orig_slvr = rpfp->ls->slvr;
|
||||
es = &(rpfp->SolverForEdge(edge,models,axioms));
|
||||
es = &(rpfp->SolverForEdge(edge,models,axioms));
|
||||
rpfp->ls->slvr = es->slvr.get();
|
||||
rpfp->AssumptionLits.swap(es->AssumptionLits);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -176,7 +176,7 @@ namespace Duality {
|
|||
m_datalog_fid = m().mk_family_id("datalog_relation");
|
||||
}
|
||||
~context() { }
|
||||
|
||||
|
||||
ast_manager &m() const {return *(ast_manager *)&mgr;}
|
||||
|
||||
void set(char const * param, char const * value) { m_config.set(param,value); }
|
||||
|
|
@ -186,13 +186,13 @@ namespace Duality {
|
|||
|
||||
symbol str_symbol(char const * s);
|
||||
symbol int_symbol(int n);
|
||||
|
||||
|
||||
sort bool_sort();
|
||||
sort int_sort();
|
||||
sort real_sort();
|
||||
sort bv_sort(unsigned sz);
|
||||
sort array_sort(sort d, sort r);
|
||||
|
||||
|
||||
func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
|
||||
func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
|
||||
func_decl function(char const * name, sort const & domain, sort const & range);
|
||||
|
|
@ -210,22 +210,22 @@ namespace Duality {
|
|||
expr int_const(char const * name);
|
||||
expr real_const(char const * name);
|
||||
expr bv_const(char const * name, unsigned sz);
|
||||
|
||||
|
||||
expr bool_val(bool b);
|
||||
|
||||
|
||||
expr int_val(int n);
|
||||
expr int_val(unsigned n);
|
||||
expr int_val(char const * n);
|
||||
|
||||
|
||||
expr real_val(int n, int d);
|
||||
expr real_val(int n);
|
||||
expr real_val(unsigned n);
|
||||
expr real_val(char const * n);
|
||||
|
||||
|
||||
expr bv_val(int n, unsigned sz);
|
||||
expr bv_val(unsigned n, unsigned sz);
|
||||
expr bv_val(char const * n, unsigned sz);
|
||||
|
||||
|
||||
expr num_val(int n, sort const & s);
|
||||
|
||||
expr mki(family_id fid, ::decl_kind dk, int n, ::expr **args);
|
||||
|
|
@ -281,17 +281,17 @@ namespace Duality {
|
|||
object(object const & s):m_ctx(s.m_ctx) {}
|
||||
context & ctx() const { return *m_ctx; }
|
||||
friend void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); }
|
||||
ast_manager &m() const {return m_ctx->m();}
|
||||
ast_manager &m() const {return m_ctx->m();}
|
||||
};
|
||||
|
||||
class symbol : public object {
|
||||
::symbol m_sym;
|
||||
public:
|
||||
symbol(context & c, ::symbol s):object(c), m_sym(s) {}
|
||||
symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
|
||||
symbol(context & c, ::symbol s):object(c), m_sym(s) {}
|
||||
symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
|
||||
symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
|
||||
operator ::symbol() const {return m_sym;}
|
||||
std::string str() const {
|
||||
operator ::symbol() const {return m_sym;}
|
||||
std::string str() const {
|
||||
if (m_sym.is_numerical()) {
|
||||
std::ostringstream buffer;
|
||||
buffer << m_sym.get_num();
|
||||
|
|
@ -300,13 +300,13 @@ namespace Duality {
|
|||
else {
|
||||
return m_sym.bare_str();
|
||||
}
|
||||
}
|
||||
friend std::ostream & operator<<(std::ostream & out, symbol const & s){
|
||||
}
|
||||
friend std::ostream & operator<<(std::ostream & out, symbol const & s) {
|
||||
return out << s.str();
|
||||
}
|
||||
friend bool operator==(const symbol &x, const symbol &y){
|
||||
}
|
||||
friend bool operator==(const symbol &x, const symbol &y) {
|
||||
return x.m_sym == y.m_sym;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
class params : public config {};
|
||||
|
|
@ -318,7 +318,7 @@ namespace Duality {
|
|||
public:
|
||||
::ast * const &raw() const {return _ast;}
|
||||
ast_i(context & c, ::ast *a = 0) : object(c) {_ast = a;}
|
||||
|
||||
|
||||
ast_i(){_ast = 0;}
|
||||
bool eq(const ast_i &other) const {
|
||||
return _ast == other._ast;
|
||||
|
|
@ -345,19 +345,19 @@ namespace Duality {
|
|||
operator ::ast*() const { return raw(); }
|
||||
friend bool eq(ast const & a, ast const & b) { return a.raw() == b.raw(); }
|
||||
|
||||
|
||||
|
||||
ast(context &c, ::ast *a = 0) : ast_i(c,a) {
|
||||
if(_ast)
|
||||
m().inc_ref(a);
|
||||
}
|
||||
|
||||
|
||||
ast() {}
|
||||
|
||||
|
||||
ast(const ast &other) : ast_i(other) {
|
||||
if(_ast)
|
||||
m().inc_ref(_ast);
|
||||
}
|
||||
|
||||
|
||||
ast &operator=(const ast &other) {
|
||||
if(_ast)
|
||||
m().dec_ref(_ast);
|
||||
|
|
@ -367,7 +367,7 @@ namespace Duality {
|
|||
m().inc_ref(_ast);
|
||||
return *this;
|
||||
}
|
||||
|
||||
|
||||
~ast(){
|
||||
if(_ast)
|
||||
m().dec_ref(_ast);
|
||||
|
|
@ -386,15 +386,15 @@ namespace Duality {
|
|||
sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
|
||||
|
||||
bool is_bool() const { return m().is_bool(*this); }
|
||||
bool is_int() const { return ctx().get_sort_kind(*this) == IntSort; }
|
||||
bool is_real() const { return ctx().get_sort_kind(*this) == RealSort; }
|
||||
bool is_int() const { return ctx().get_sort_kind(*this) == IntSort; }
|
||||
bool is_real() const { return ctx().get_sort_kind(*this) == RealSort; }
|
||||
bool is_arith() const;
|
||||
bool is_array() const { return ctx().get_sort_kind(*this) == ArraySort; }
|
||||
bool is_datatype() const;
|
||||
bool is_relation() const;
|
||||
bool is_finite_domain() const;
|
||||
bool is_array() const { return ctx().get_sort_kind(*this) == ArraySort; }
|
||||
bool is_datatype() const;
|
||||
bool is_relation() const;
|
||||
bool is_finite_domain() const;
|
||||
|
||||
|
||||
|
||||
sort array_domain() const;
|
||||
sort array_range() const;
|
||||
|
||||
|
|
@ -404,7 +404,7 @@ namespace Duality {
|
|||
}
|
||||
};
|
||||
|
||||
|
||||
|
||||
class func_decl : public ast {
|
||||
public:
|
||||
func_decl() : ast() {}
|
||||
|
|
@ -413,7 +413,7 @@ namespace Duality {
|
|||
func_decl(func_decl const & s):ast(s) {}
|
||||
operator ::func_decl*() const { return to_func_decl(*this); }
|
||||
func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
|
||||
|
||||
|
||||
unsigned arity() const;
|
||||
sort domain(unsigned i) const;
|
||||
sort range() const;
|
||||
|
|
@ -434,9 +434,9 @@ namespace Duality {
|
|||
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
|
||||
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
|
||||
|
||||
func_decl get_func_decl_parameter(unsigned idx){
|
||||
func_decl get_func_decl_parameter(unsigned idx){
|
||||
return func_decl(ctx(),to_func_decl(to_func_decl(raw())->get_parameters()[idx].get_ast()));
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
|
@ -447,8 +447,8 @@ namespace Duality {
|
|||
expr(context & c, ::ast *n):ast(c, n) {}
|
||||
expr(expr const & n):ast(n) {}
|
||||
expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
|
||||
operator ::expr*() const { return to_expr(raw()); }
|
||||
unsigned get_id() const {return to_expr(raw())->get_id();}
|
||||
operator ::expr*() const { return to_expr(raw()); }
|
||||
unsigned get_id() const {return to_expr(raw())->get_id();}
|
||||
|
||||
sort get_sort() const { return sort(ctx(),m().get_sort(to_expr(raw()))); }
|
||||
|
||||
|
|
@ -460,27 +460,27 @@ 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_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()));
|
||||
}
|
||||
bool is_app() const {return raw()->get_kind() == AST_APP;}
|
||||
}
|
||||
bool is_app() const {return raw()->get_kind() == AST_APP;}
|
||||
bool is_quantifier() const {return raw()->get_kind() == AST_QUANTIFIER;}
|
||||
bool is_var() const {return raw()->get_kind() == AST_VAR;}
|
||||
bool is_label (bool &pos,std::vector<symbol> &names) const ;
|
||||
bool is_ground() const {return to_app(raw())->is_ground();}
|
||||
bool has_quantifiers() const {return to_app(raw())->has_quantifiers();}
|
||||
bool has_free(int idx) const {
|
||||
bool is_label (bool &pos,std::vector<symbol> &names) const ;
|
||||
bool is_ground() const {return to_app(raw())->is_ground();}
|
||||
bool has_quantifiers() const {return to_app(raw())->has_quantifiers();}
|
||||
bool has_free(int idx) const {
|
||||
used_vars proc;
|
||||
proc.process(to_expr(raw()));
|
||||
return proc.contains(idx);
|
||||
}
|
||||
unsigned get_max_var_idx_plus_1() const {
|
||||
}
|
||||
unsigned get_max_var_idx_plus_1() const {
|
||||
used_vars proc;
|
||||
proc.process(to_expr(raw()));
|
||||
return proc.get_max_found_var_idx_plus_1();
|
||||
}
|
||||
}
|
||||
|
||||
// operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
|
||||
func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());}
|
||||
|
|
@ -493,11 +493,11 @@ namespace Duality {
|
|||
return 1;
|
||||
case AST_VAR:
|
||||
return 0;
|
||||
default:;
|
||||
default:;
|
||||
}
|
||||
SASSERT(0);
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
expr arg(unsigned i) const {
|
||||
ast_kind dk = raw()->get_kind();
|
||||
switch(dk){
|
||||
|
|
@ -509,25 +509,25 @@ namespace Duality {
|
|||
}
|
||||
assert(0);
|
||||
return expr();
|
||||
}
|
||||
}
|
||||
|
||||
expr body() const {
|
||||
return ctx().cook(to_quantifier(raw())->get_expr());
|
||||
}
|
||||
}
|
||||
|
||||
friend expr operator!(expr const & a) {
|
||||
// ::expr *e = a;
|
||||
return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_NOT,a));
|
||||
}
|
||||
}
|
||||
|
||||
friend expr operator&&(expr const & a, expr const & b) {
|
||||
return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_AND,a,b));
|
||||
}
|
||||
}
|
||||
|
||||
friend expr operator||(expr const & a, expr const & b) {
|
||||
return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_OR,a,b));
|
||||
}
|
||||
|
||||
|
||||
friend expr implies(expr const & a, expr const & b) {
|
||||
return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_IMPLIES,a,b));
|
||||
}
|
||||
|
|
@ -546,12 +546,12 @@ namespace Duality {
|
|||
|
||||
friend expr operator*(expr const & a, expr const & b) {
|
||||
return a.ctx().make(Times,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_MUL,a,b));
|
||||
}
|
||||
}
|
||||
|
||||
friend expr operator/(expr const & a, expr const & b) {
|
||||
return a.ctx().make(Div,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_DIV,a,b));
|
||||
}
|
||||
|
||||
|
||||
friend expr operator-(expr const & a) {
|
||||
return a.ctx().make(Uminus,a); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_UMINUS,a));
|
||||
}
|
||||
|
|
@ -562,71 +562,71 @@ namespace Duality {
|
|||
|
||||
friend expr operator<=(expr const & a, expr const & b) {
|
||||
return a.ctx().make(Leq,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LE,a,b));
|
||||
}
|
||||
}
|
||||
|
||||
friend expr operator>=(expr const & a, expr const & b) {
|
||||
return a.ctx().make(Geq,a,b); //expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GE,a,b));
|
||||
}
|
||||
|
||||
|
||||
friend expr operator<(expr const & a, expr const & b) {
|
||||
return a.ctx().make(Lt,a,b); expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LT,a,b));
|
||||
}
|
||||
|
||||
|
||||
friend expr operator>(expr const & a, expr const & b) {
|
||||
return a.ctx().make(Gt,a,b); expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GT,a,b));
|
||||
}
|
||||
}
|
||||
|
||||
expr simplify() const;
|
||||
|
||||
expr simplify(params const & p) const;
|
||||
|
||||
|
||||
expr qe_lite() const;
|
||||
|
||||
expr qe_lite(const std::set<int> &idxs, bool index_of_bound) 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 &, const expr &);
|
||||
|
||||
friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);
|
||||
|
||||
friend expr clone_quantifier(decl_kind, const expr &, const expr &);
|
||||
friend expr clone_quantifier(decl_kind, const expr &, const expr &);
|
||||
|
||||
friend std::ostream & operator<<(std::ostream & out, expr const & m){
|
||||
m.ctx().print_expr(out,m);
|
||||
return out;
|
||||
}
|
||||
}
|
||||
|
||||
void get_patterns(std::vector<expr> &pats) const ;
|
||||
void get_patterns(std::vector<expr> &pats) const ;
|
||||
|
||||
unsigned get_quantifier_num_bound() const {
|
||||
unsigned get_quantifier_num_bound() const {
|
||||
return to_quantifier(raw())->get_num_decls();
|
||||
}
|
||||
}
|
||||
|
||||
unsigned get_index_value() const {
|
||||
unsigned get_index_value() const {
|
||||
var* va = to_var(raw());
|
||||
return va->get_idx();
|
||||
}
|
||||
}
|
||||
|
||||
bool is_quantifier_forall() const {
|
||||
return to_quantifier(raw())->is_forall();
|
||||
}
|
||||
}
|
||||
|
||||
sort get_quantifier_bound_sort(unsigned n) const {
|
||||
sort get_quantifier_bound_sort(unsigned n) const {
|
||||
return sort(ctx(),to_quantifier(raw())->get_decl_sort(n));
|
||||
}
|
||||
}
|
||||
|
||||
symbol get_quantifier_bound_name(unsigned n) const {
|
||||
symbol get_quantifier_bound_name(unsigned n) const {
|
||||
return symbol(ctx(),to_quantifier(raw())->get_decl_names()[n]);
|
||||
}
|
||||
}
|
||||
|
||||
friend expr forall(const std::vector<expr> &quants, const expr &body);
|
||||
friend expr forall(const std::vector<expr> &quants, const expr &body);
|
||||
|
||||
friend expr exists(const std::vector<expr> &quants, const expr &body);
|
||||
friend expr exists(const std::vector<expr> &quants, const expr &body);
|
||||
|
||||
};
|
||||
|
||||
|
||||
|
||||
typedef ::decl_kind pfrule;
|
||||
|
||||
|
||||
class proof : public ast {
|
||||
public:
|
||||
proof(context & c):ast(c) {}
|
||||
|
|
@ -643,15 +643,15 @@ namespace Duality {
|
|||
unsigned num_prems() const {
|
||||
return to_app(raw())->get_num_args() - 1;
|
||||
}
|
||||
|
||||
|
||||
expr conc() const {
|
||||
return ctx().cook(to_app(raw())->get_arg(num_prems()));
|
||||
}
|
||||
|
||||
|
||||
proof prem(unsigned i) const {
|
||||
return proof(ctx(),to_app(to_app(raw())->get_arg(i)));
|
||||
}
|
||||
|
||||
|
||||
void get_assumptions(std::vector<expr> &assumps);
|
||||
};
|
||||
|
||||
|
|
@ -675,12 +675,12 @@ namespace Duality {
|
|||
T back() const { return operator[](size() - 1); }
|
||||
void pop_back() { assert(size() > 0); resize(size() - 1); }
|
||||
bool empty() const { return size() == 0; }
|
||||
ast_vector_tpl & operator=(ast_vector_tpl const & s) {
|
||||
Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
|
||||
ast_vector_tpl & operator=(ast_vector_tpl const & s) {
|
||||
Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
|
||||
// Z3_ast_vector_dec_ref(ctx(), m_vector);
|
||||
m_ctx = s.m_ctx;
|
||||
m_ctx = s.m_ctx;
|
||||
m_vector = s.m_vector;
|
||||
return *this;
|
||||
return *this;
|
||||
}
|
||||
friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
|
||||
};
|
||||
|
|
@ -705,9 +705,9 @@ namespace Duality {
|
|||
~func_interp() { }
|
||||
operator ::func_interp *() const { return m_interp; }
|
||||
func_interp & operator=(func_interp const & s) {
|
||||
m_ctx = s.m_ctx;
|
||||
m_ctx = s.m_ctx;
|
||||
m_interp = s.m_interp;
|
||||
return *this;
|
||||
return *this;
|
||||
}
|
||||
unsigned num_entries() const { return m_interp->num_entries(); }
|
||||
expr get_arg(unsigned ent, unsigned arg) const {
|
||||
|
|
@ -729,32 +729,32 @@ namespace Duality {
|
|||
m_model = m;
|
||||
}
|
||||
public:
|
||||
model(context & c, ::model * m = 0):object(c), m_model(m) { }
|
||||
model(model const & s):object(s), m_model(s.m_model) { }
|
||||
~model() { }
|
||||
model(context & c, ::model * m = 0):object(c), m_model(m) { }
|
||||
model(model const & s):object(s), m_model(s.m_model) { }
|
||||
~model() { }
|
||||
operator ::model *() const { return m_model.get(); }
|
||||
model & operator=(model const & s) {
|
||||
// ::model *_inc_ref(s.ctx(), s.m_model);
|
||||
// ::model *_dec_ref(ctx(), m_model);
|
||||
m_ctx = s.m_ctx;
|
||||
m_ctx = s.m_ctx;
|
||||
m_model = s.m_model.get();
|
||||
return *this;
|
||||
return *this;
|
||||
}
|
||||
model & operator=(::model *s) {
|
||||
m_model = s;
|
||||
return *this;
|
||||
m_model = s;
|
||||
return *this;
|
||||
}
|
||||
bool null() const {return !m_model;}
|
||||
|
||||
bool null() const {return !m_model;}
|
||||
|
||||
expr eval(expr const & n, bool model_completion=true) const {
|
||||
::model * _m = m_model.get();
|
||||
expr_ref result(ctx().m());
|
||||
_m->eval(n, result, model_completion);
|
||||
return expr(ctx(), result);
|
||||
}
|
||||
|
||||
|
||||
void show() const;
|
||||
void show_hash() const;
|
||||
void show_hash() const;
|
||||
|
||||
unsigned num_consts() const {return m_model.get()->get_num_constants();}
|
||||
unsigned num_funcs() const {return m_model.get()->get_num_functions();}
|
||||
|
|
@ -765,11 +765,11 @@ namespace Duality {
|
|||
|
||||
expr get_const_interp(func_decl f) const {
|
||||
return ctx().cook(m_model->get_const_interp(to_func_decl(f.raw())));
|
||||
}
|
||||
}
|
||||
|
||||
func_interp get_func_interp(func_decl f) const {
|
||||
return func_interp(ctx(),m_model->get_func_interp(to_func_decl(f.raw())));
|
||||
}
|
||||
}
|
||||
|
||||
#if 0
|
||||
friend std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
|
||||
|
|
@ -792,9 +792,9 @@ namespace Duality {
|
|||
stats & operator=(stats const & s) {
|
||||
Z3_stats_inc_ref(s.ctx(), s.m_stats);
|
||||
if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
|
||||
m_ctx = s.m_ctx;
|
||||
m_ctx = s.m_ctx;
|
||||
m_stats = s.m_stats;
|
||||
return *this;
|
||||
return *this;
|
||||
}
|
||||
unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
|
||||
std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
|
||||
|
|
@ -820,7 +820,7 @@ namespace Duality {
|
|||
void assert_cnst(const expr &cnst);
|
||||
};
|
||||
|
||||
inline std::ostream & operator<<(std::ostream & out, check_result r) {
|
||||
inline std::ostream & operator<<(std::ostream & out, check_result r) {
|
||||
if (r == unsat) out << "unsat";
|
||||
else if (r == sat) out << "sat";
|
||||
else out << "unknown";
|
||||
|
|
@ -837,54 +837,54 @@ namespace Duality {
|
|||
protected:
|
||||
::solver *m_solver;
|
||||
model the_model;
|
||||
bool canceled;
|
||||
proof_gen_mode m_mode;
|
||||
bool extensional;
|
||||
bool canceled;
|
||||
proof_gen_mode m_mode;
|
||||
bool extensional;
|
||||
public:
|
||||
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(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() {
|
||||
if(m_solver)
|
||||
dealloc(m_solver);
|
||||
}
|
||||
operator ::solver*() const { return m_solver; }
|
||||
solver & operator=(solver const & s) {
|
||||
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 {};
|
||||
void checkpoint(){
|
||||
operator ::solver*() const { return m_solver; }
|
||||
solver & operator=(solver const & s) {
|
||||
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 {};
|
||||
void checkpoint(){
|
||||
if(canceled)
|
||||
throw(cancel_exception());
|
||||
}
|
||||
}
|
||||
// void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
|
||||
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) { scoped_proof_mode spm(m(),m_mode); m_solver->assert_expr(e); }
|
||||
check_result check() {
|
||||
scoped_proof_mode spm(m(),m_mode);
|
||||
check_result check() {
|
||||
scoped_proof_mode spm(m(),m_mode);
|
||||
checkpoint();
|
||||
lbool r = m_solver->check_sat(0,0);
|
||||
model_ref m;
|
||||
m_solver->get_model(m);
|
||||
the_model = m.get();
|
||||
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);
|
||||
}
|
||||
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)
|
||||
the_model = old_model;
|
||||
return res;
|
||||
}
|
||||
}
|
||||
check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) {
|
||||
scoped_proof_mode spm(m(),m_mode);
|
||||
scoped_proof_mode spm(m(),m_mode);
|
||||
checkpoint();
|
||||
std::vector< ::expr *> _assumptions(n);
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
|
|
@ -892,7 +892,7 @@ namespace Duality {
|
|||
}
|
||||
the_model = 0;
|
||||
lbool r = m_solver->check_sat(n, VEC2PTR(_assumptions));
|
||||
|
||||
|
||||
if(core_size && core){
|
||||
ptr_vector< ::expr> _core;
|
||||
m_solver->get_unsat_core(_core);
|
||||
|
|
@ -905,20 +905,20 @@ namespace Duality {
|
|||
m_solver->get_model(m);
|
||||
the_model = m.get();
|
||||
|
||||
return to_check_result(r);
|
||||
return to_check_result(r);
|
||||
}
|
||||
#if 0
|
||||
check_result check(expr_vector assumptions) {
|
||||
scoped_proof_mode spm(m(),m_mode);
|
||||
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++) {
|
||||
check_context(*this, assumptions[i]);
|
||||
_assumptions[i] = assumptions[i];
|
||||
}
|
||||
Z3_lbool r = Z3_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
|
||||
check_error();
|
||||
return to_check_result(r);
|
||||
Z3_lbool r = Z3_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
|
||||
check_error();
|
||||
return to_check_result(r);
|
||||
}
|
||||
#endif
|
||||
model get_model() const { return model(ctx(), the_model); }
|
||||
|
|
@ -930,27 +930,26 @@ namespace Duality {
|
|||
#endif
|
||||
// expr proof() const { Z3_ast r = Z3_solver_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
|
||||
// friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
|
||||
|
||||
int get_num_decisions();
|
||||
int get_num_decisions();
|
||||
|
||||
void cancel(){
|
||||
scoped_proof_mode spm(m(),m_mode);
|
||||
void cancel(){
|
||||
scoped_proof_mode spm(m(),m_mode);
|
||||
canceled = true;
|
||||
m().limit().cancel();
|
||||
}
|
||||
}
|
||||
|
||||
unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); 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 print(const char *filename);
|
||||
void show_assertion_ids();
|
||||
void show();
|
||||
void print(const char *filename);
|
||||
void show_assertion_ids();
|
||||
|
||||
proof get_proof(){
|
||||
scoped_proof_mode spm(m(),m_mode);
|
||||
proof get_proof(){
|
||||
scoped_proof_mode spm(m(),m_mode);
|
||||
return proof(ctx(),m_solver->get_proof());
|
||||
}
|
||||
}
|
||||
|
||||
bool extensional_array_theory() {return extensional;}
|
||||
bool extensional_array_theory() {return extensional;}
|
||||
};
|
||||
|
||||
#if 0
|
||||
|
|
@ -969,20 +968,20 @@ namespace Duality {
|
|||
goal & operator=(goal const & s) {
|
||||
Z3_goal_inc_ref(s.ctx(), s.m_goal);
|
||||
Z3_goal_dec_ref(ctx(), m_goal);
|
||||
m_ctx = s.m_ctx;
|
||||
m_ctx = s.m_ctx;
|
||||
m_goal = s.m_goal;
|
||||
return *this;
|
||||
return *this;
|
||||
}
|
||||
void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
|
||||
unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
|
||||
expr operator[](unsigned i) const { Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
|
||||
Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
|
||||
bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
|
||||
unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
|
||||
unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
|
||||
void reset() { Z3_goal_reset(ctx(), m_goal); }
|
||||
unsigned num_exprs() const { Z3_goal_num_exprs(ctx(), m_goal); }
|
||||
bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
|
||||
bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
|
||||
bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
|
||||
bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
|
||||
friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
|
||||
};
|
||||
|
||||
|
|
@ -1000,15 +999,15 @@ namespace Duality {
|
|||
apply_result & operator=(apply_result const & s) {
|
||||
Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
|
||||
Z3_apply_result_dec_ref(ctx(), m_apply_result);
|
||||
m_ctx = s.m_ctx;
|
||||
m_ctx = s.m_ctx;
|
||||
m_apply_result = s.m_apply_result;
|
||||
return *this;
|
||||
return *this;
|
||||
}
|
||||
unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
|
||||
goal operator[](unsigned i) const { Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
|
||||
goal operator[](int i) const { assert(i >= 0); return this->operator[](static_cast<unsigned>(i)); }
|
||||
model convert_model(model const & m, unsigned i = 0) const {
|
||||
check_context(*this, m);
|
||||
model convert_model(model const & m, unsigned i = 0) const {
|
||||
check_context(*this, m);
|
||||
Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
|
||||
check_error();
|
||||
return model(ctx(), new_m);
|
||||
|
|
@ -1031,16 +1030,16 @@ namespace Duality {
|
|||
tactic & operator=(tactic const & s) {
|
||||
Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
|
||||
Z3_tactic_dec_ref(ctx(), m_tactic);
|
||||
m_ctx = s.m_ctx;
|
||||
m_ctx = s.m_ctx;
|
||||
m_tactic = s.m_tactic;
|
||||
return *this;
|
||||
return *this;
|
||||
}
|
||||
solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
|
||||
apply_result apply(goal const & g) const {
|
||||
apply_result apply(goal const & g) const {
|
||||
check_context(*this, g);
|
||||
Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
|
||||
check_error();
|
||||
return apply_result(ctx(), r);
|
||||
Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
|
||||
check_error();
|
||||
return apply_result(ctx(), r);
|
||||
}
|
||||
apply_result operator()(goal const & g) const {
|
||||
return apply(g);
|
||||
|
|
@ -1091,45 +1090,45 @@ namespace Duality {
|
|||
probe & operator=(probe const & s) {
|
||||
Z3_probe_inc_ref(s.ctx(), s.m_probe);
|
||||
Z3_probe_dec_ref(ctx(), m_probe);
|
||||
m_ctx = s.m_ctx;
|
||||
m_ctx = s.m_ctx;
|
||||
m_probe = s.m_probe;
|
||||
return *this;
|
||||
return *this;
|
||||
}
|
||||
double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
|
||||
double operator()(goal const & g) const { return apply(g); }
|
||||
friend probe operator<=(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
friend probe operator<=(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
}
|
||||
friend probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
|
||||
friend probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
|
||||
friend probe operator>=(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
friend probe operator>=(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
}
|
||||
friend probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
|
||||
friend probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
|
||||
friend probe operator<(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
friend probe operator<(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
}
|
||||
friend probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
|
||||
friend probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
|
||||
friend probe operator>(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
friend probe operator>(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
}
|
||||
friend probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
|
||||
friend probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
|
||||
friend probe operator==(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
friend probe operator==(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
}
|
||||
friend probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
|
||||
friend probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
|
||||
friend probe operator&&(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
friend probe operator&&(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
}
|
||||
friend probe operator||(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
friend probe operator||(probe const & p1, probe const & p2) {
|
||||
check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
|
||||
}
|
||||
friend probe operator!(probe const & p) {
|
||||
Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
|
||||
Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -1159,15 +1158,15 @@ namespace Duality {
|
|||
inline symbol context::int_symbol(int n) { ::symbol r = ::symbol(n); return symbol(*this, r); }
|
||||
|
||||
inline sort context::bool_sort() {
|
||||
::sort *s = m().mk_sort(m_basic_fid, BOOL_SORT);
|
||||
::sort *s = m().mk_sort(m_basic_fid, BOOL_SORT);
|
||||
return sort(*this, s);
|
||||
}
|
||||
inline sort context::int_sort() {
|
||||
::sort *s = m().mk_sort(m_arith_fid, INT_SORT);
|
||||
::sort *s = m().mk_sort(m_arith_fid, INT_SORT);
|
||||
return sort(*this, s);
|
||||
}
|
||||
inline sort context::real_sort() {
|
||||
::sort *s = m().mk_sort(m_arith_fid, REAL_SORT);
|
||||
::sort *s = m().mk_sort(m_arith_fid, REAL_SORT);
|
||||
return sort(*this, s);
|
||||
}
|
||||
inline sort context::array_sort(sort d, sort r) {
|
||||
|
|
@ -1188,7 +1187,7 @@ namespace Duality {
|
|||
inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
|
||||
return function(str_symbol(name), arity, domain, range);
|
||||
}
|
||||
|
||||
|
||||
inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
|
||||
sort args[1] = { domain };
|
||||
return function(name, 1, args, range);
|
||||
|
|
@ -1196,7 +1195,7 @@ namespace Duality {
|
|||
|
||||
inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
|
||||
sort args[2] = { d1, d2 };
|
||||
return function(name, 2, args, range);
|
||||
return function(name, 2, args, range);
|
||||
}
|
||||
|
||||
inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
|
||||
|
|
@ -1208,7 +1207,7 @@ namespace Duality {
|
|||
sort args[4] = { d1, d2, d3, d4 };
|
||||
return function(name, 4, args, range);
|
||||
}
|
||||
|
||||
|
||||
inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range) {
|
||||
sort args[5] = { d1, d2, d3, d4, d5 };
|
||||
return function(name, 5, args, range);
|
||||
|
|
@ -1217,7 +1216,7 @@ namespace Duality {
|
|||
|
||||
inline expr context::constant(symbol const & name, sort const & s) {
|
||||
::expr *r = m().mk_const(m().mk_const_decl(name, s));
|
||||
return expr(*this, r);
|
||||
return expr(*this, r);
|
||||
}
|
||||
inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
|
||||
inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
|
||||
|
|
@ -1250,11 +1249,11 @@ namespace Duality {
|
|||
expr args[5] = {a1,a2,a3,a4,a5};
|
||||
return operator()(5,args);
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
inline expr select(expr const & a, expr const & i) { return a.ctx().make(Select,a,i); }
|
||||
inline expr store(expr const & a, expr const & i, expr const & v) { return a.ctx().make(Store,a,i,v); }
|
||||
|
||||
|
||||
inline expr forall(const std::vector<expr> &quants, const expr &body){
|
||||
return body.ctx().make_quant(Forall,quants,body);
|
||||
}
|
||||
|
|
@ -1304,7 +1303,7 @@ namespace Duality {
|
|||
}
|
||||
|
||||
inline void setTerm(expr t){term = t;}
|
||||
|
||||
|
||||
inline void addTerm(expr t){terms.push_back(t);}
|
||||
|
||||
inline void setChildren(const std::vector<TermTree *> & _children){
|
||||
|
|
@ -1326,7 +1325,7 @@ namespace Duality {
|
|||
std::vector<TermTree *> children;
|
||||
int num;
|
||||
};
|
||||
|
||||
|
||||
typedef context interpolating_context;
|
||||
|
||||
class interpolating_solver : public solver {
|
||||
|
|
@ -1336,7 +1335,7 @@ namespace Duality {
|
|||
{
|
||||
weak_mode = false;
|
||||
}
|
||||
|
||||
|
||||
public:
|
||||
lbool interpolate(const std::vector<expr> &assumptions,
|
||||
std::vector<expr> &interpolants,
|
||||
|
|
@ -1344,41 +1343,41 @@ namespace Duality {
|
|||
literals &lits,
|
||||
bool incremental
|
||||
);
|
||||
|
||||
|
||||
lbool interpolate_tree(TermTree *assumptions,
|
||||
TermTree *&interpolants,
|
||||
model &_model,
|
||||
literals &lits,
|
||||
bool incremental
|
||||
);
|
||||
|
||||
|
||||
bool read_interpolation_problem(const std::string &file_name,
|
||||
std::vector<expr> &assumptions,
|
||||
std::vector<expr> &theory,
|
||||
std::string &error_message
|
||||
);
|
||||
|
||||
|
||||
void write_interpolation_problem(const std::string &file_name,
|
||||
const std::vector<expr> &assumptions,
|
||||
const std::vector<expr> &theory
|
||||
);
|
||||
|
||||
|
||||
void AssertInterpolationAxiom(const expr &expr);
|
||||
void RemoveInterpolationAxiom(const expr &expr);
|
||||
|
||||
|
||||
void SetWeakInterpolants(bool weak);
|
||||
void SetPrintToFile(const std::string &file_name);
|
||||
|
||||
|
||||
const std::vector<expr> &GetInterpolationAxioms() {return theory;}
|
||||
const char *profile();
|
||||
|
||||
|
||||
private:
|
||||
bool weak_mode;
|
||||
std::string print_filename;
|
||||
std::vector<expr> theory;
|
||||
};
|
||||
|
||||
|
||||
|
||||
|
||||
inline expr context::cook(::expr *a) {return expr(*this,a);}
|
||||
|
||||
inline std::vector<expr> context::cook(ptr_vector< ::expr> v) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue